Design constraints are artifacts that model an environment of a design under verification by restricting input stimuli to plausible valuations. Judicious usage of design constraints can be effective in eliminating false verification results. Given a particular verification problem, however, it is a difficult proposition to write down all the necessary constraints. We present a technique for automatic generation of design constraints from simple user-provided information about potential design environments. Our method generates a set of design constraints representing varying degrees of assumptions about potential environments of a dynamic circuit. We also present experimental results on verification of custom designed embedded dynamic circuits taken from the Motorola MPC7455 microprocessor.

Equivalence checking between Register Transfer Level (RTL) descriptions and transistor level descriptions of custom memories is an important step in the design flow of high performance microprocessors. Equivalence checking can be done with or without the knowledge of state mapping between the two descriptions. We present evidence that because of state mapping, our verification technique exercises system behavior that exposes hard-to-detect bugs that might otherwise go undetected. This paper defines Crossover Bugs (CB's) that can be present in scan-based custom designs and that are inherently hard-to-detect without state mapping. We demonstrate that such bugs can be missed by equivalence checking techniques that do not have state mappings between the two descriptions. By identifying the state correspondences between the RTL and the transistor implementation of custom memories, a more rigorous equivalence check can be performed compared to traditional equivalence checking methods such as product machine constructions. We also compare the time and memory complexities of crossover bug detection capability of the two equivalence checking approaches. We conclude with experimental results of CB detection on some of the custom designed embedded memories of Motorola's MPC 7455 microprocessor (compliant with IBM's PowerPC instruction set architecture).

This paper describes the use of Symbolic Trajectory Evaluation (STE), a modified form of symbolic simulation, to verify the equivalence between RTL and transistor-level representations of on-chip custom memories for the latest PowerPC microprocessor. The validation of embedded memories and their associated control logic poses a special problem for traditional formal equivalence checking tools due to the inherently sequential and self-timed nature of the internal control logic and the large number of state-holding elements. The use of the VERSYS STE engine to validate these custom memories is illustrated. We present our array verification methodology, discuss some of the results of our approach, and outline plans for future development.

This paper evaluates the concurrent error detection capabilities of system-level checks, using fault and error injection. The checks comprise application and system level mechanisms to detect control flow errors. We propose Enhanced Control-Flow Checking Using Assertions (ECCA). In ECCA, branch-free intervals (BFI) in a given high or intermediate level program are identified and the entry and exit points of the intervals are determined. BFls are then grouped into blocks, the size of which is determined through a performance/overhead analysis. The blocks are then fortified with preinserted assertions. For the high level ECCA, we describe an implementation of ECCA through a preprocessor that will automatically insert the necessary assertions into the program. Then, we describe the intermediate implementation possible through modifications made on gee to make it ECCA capable. The fault detection capabilities of the checks are evaluated both analytically and experimentally. Fault injection experiments are conducted using FERRARI to determine the fault coverage of the proposed techniques.