Verifying memory arrays such as on-chip caches and register files is a difficult part of designing a microprocessor.Current tools cannot verify the equivalence of the arrays to their behavioral or RTL models, nor their correct functioning at the transistor level.It is infeasible to run the number of simulation cycles required, and most formal verification tools break down due to the enormous number of state-holding elements in the arrays.The formal method of symbolic trajectory evaluation (STE) appears to offer a solution, however.STE verifies that a circuit satisfies a formula in a carefully restricted temporal logic.For arrays, it requires only a number of variables approximately logarithmic in the number of memory locations.The circuit is modeled at the switch level, so the verification is done on the actual design.We have used STE to verify two arrays from PowerPC microprocessors: a register file, and a data cache tag unit.The tag unit contains over 12,000 latches.We believe it is the largest circuit to have been formally verified, without abstracting away significant detail, in the industry.We also describe an automated technique for identifying state-holding elements in the arrays, a technique which should greatly assist the widespread application of STE.

The paper describes a new technique for extracting clock level finite state machines (FSMs) from transistor netlists using symbolic simulation. The transistor netlist is preprocessed to produce a gate level representation of the netlist. Given specifications of the circuit clocking and input and output timing, simulation patterns are derived for a symbolic simulator. The result of the symbolic simulation and extraction process is the next state and output function of the equivalent FSM, represented as Ordered Binary Decision Diagrams. Compared to previous techniques, our extraction process yields an order of magnitude improvement in both space and time, is fully automated and can handle static storage structures and time multiplexed inputs and outputs

Formal verification is becoming a useful means of validating designs. We have developed a methodology for formally verifying dataintensive circuits (e.g., processors) with sophisticated timing (e.g., pipelining) against high-level declarative specifications. Previously, formally verifying a microprocessor required the use of an automatic theorem prover, but our technique requires little more than a symbolic simulator. We have formally verified a pre-existing 16-bit CISC microprocessor circuit extracted from the fabricated layout. Introduction Previously, symbolic switch-level simulation has been used to verify some small or simple data-intensive circuits (RAMs, stacks, register files, ALUs, and simple pipelines) [2, 3]. In doing so, the necessary simulation patterns were developed by hand or by using ad-hoc techniques, and it was then argued that the patterns were sufficient, and that their generation could be automated. We have developed sufficient theory to fully support such claims...

Symbolic trajectory evaluation is a new approach to formal hardware verification combining the circuit modeling capabilities of symbolic logic simulation with some of the analytic methods found in temporal logic model checkers.We have created such an evaluator by extending the symbolic switch-level simulator COSMOS.This program gains added efficiency by exploiting the ability of COSMOS to evaluate circuit operation over a ternary logic model, where the third value X represents an unknown logic value.This program can formally verify systems containing complex featurea such as switch-level models, detailed timing, and pipelining.

The COSMOS simulator provides fast and accurate switch-level modeling of MOS digital circuits. It attains high performance by preprocessing the transistor network into a functionally equivalent Boolean representation. This description, produced by the symbolic analyzer ANAMOS, captures all aspects of switch-level networks including bidirectional transistors, stored charge, different signal strengths, and indeterminate (X) logic values. The LGCC program translates the Boolean representation into a set of machine language evaluation procedures and initialized data structures. These procedures and data structures are compiled along with code implementing the simulation kernel and user interface to produce the simulation program. The simulation program runs an order of magnitude faster than our previous simulator MOSSIM II.