Formal verification of digital circuits using hybrid simulation

A description is given of PROVE (PROlog-based VErifier), a computer-aided design (CAD) system, written in PROLOG, that verifies the functional correctness of digital circuits. The primary verification mechanism in PROVE is to compare two symbolic expressions generated from the implementation being verified and the specification, respectively. Concepts of hierarchical verification, hybrid simulation, and pattern matching are incorporated to allow verification of large circuits. Hybrid simulation, whereby properly selected signals are specified numerically, while others stay in symbolic form, helps control the size of symbolic expressions within a level of hierarchy. Control signals, like clock, can also be treated numerically. At the Boolean gate level, several pattern-matching rules are used to eliminate a large number of terms in the symbolic expressions even before the expressions are expanded for logical comparison.<>