FUNCTIONAL VERIFICATION OF DIGITAL MOS CIRCUITS.

A major goal of the Snap CAD system for automatically generating signal-processing circuits is to prove that the designs are functionally correct. The function of a MOS circuit is extracted using techniques due to R. Bryant (1985). This functional characterization is compared to the high-level description of the circuit to determine correctness. Important aspects of the verifier are: 1) paths in the switch graph are compiled statically; 2) cells in a hierarchical design are functionally meaningful and may be abstracted for use in verifying the entire design; and 3) optimized algorithms make interactive verification feasible. Experimental results are presented.