Title :
Formal verification of digital circuits using hybrid simulation
Author :
Srinivas, Nagendra C E ; Agrawal, Vishwani D.
Author_Institution :
AT&T Bell Labs., Murray Hill, NJ, USA
Abstract :
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.<>
Keywords :
circuit CAD; hybrid simulation; logic CAD; Boolean gate level; CAD system; PROVE; computer-aided design; digital circuits; formal verification; hierarchical verification; hybrid simulation; logic design; pattern-matching rules; Adders; Analytical models; Circuit simulation; Combinational circuits; Digital circuits; Formal verification; Logic; Pattern matching; Registers; Timing;
Journal_Title :
Circuits and Devices Magazine, IEEE
