Assertion -checker synthesis for hardware verification, in -circuit debugging and on-line monitoring

Producing error-free circuits is of paramount importance in the semiconductor industry. Assertions are becoming an indispensable means of verifying the correctness of increasingly complex digital designs. Assertions model the proper behavior of a design, and are expressed in a high level language based on temporal logic. In dynamic verification, simulation is used to exercise a circuit in order to assess its behavior. For large designs, simulation times are often prohibitively excessive, and designs are instead emulated in hardware. Because of their high-level temporal operators, assertion statements do not lend themselves directly to hardware implementations such as emulation.;Checkers are circuit-level implementations of assertions, and thus allow assertions to be used in hardware emulation and simulation acceleration. The checkers are not only beneficial in pre-fabrication functional verification, but can also be used for debugging fabricated silicon, at speed, where timing issues are most prevalent. Using checkers beyond verification and silicon debug is also explored, by proposing the use of assertions and a checker generator to automate the design of certain types of circuits. A variety of enhancements are also introduced to improve the debugging process with assertion checkers. These enhancements range from additional observability and metric-reporting features, to behavioral modifications to the checkers.;The tool developed in this work outperforms the best-known checker generator, namely the FoCs Property Checkers Generator from IBM. Important improvements compared to FoCs are demonstrated in terms of the circuit-size of checkers, the behavioral correctness of checkers and the number of operators supported.;This thesis introduces techniques and algorithms for generating resource-efficient circuit-level checkers from hardware assertion statements. These checkers are added to the source design, where they monitor the appropriate circuit signals to find faulty execution sequences. In this work, a finite automaton framework and a set of algorithms are developed and used extensively to create an intermediate representation of assertions. Implementing the large variety of temporal operators found in properties is also performed using specially designed rewrite rules.