Formal Verification of Digital Circuits Using Symbolic Ternary System Models
Randal E. Bryant
Carl-Johan Seger
10.1184/R1/6605804.v1
https://kilthub.cmu.edu/articles/journal_contribution/Formal_Verification_of_Digital_Circuits_Using_Symbolic_Ternary_System_Models/6605804
Ternary system modeling involves extending the traditional set of binary values { 0,1}
with
a third value X indicating an unknown or indeterminate condition. By making this extension,
we can model a wider range of circuit phenomena. We can also efficiently verify sequential
circuits in which the effect of a given operation depends on only a subset of the total system
state.
This paper presents a formal methodology for verifying synchronous digital circuits using
a ternary system model. The desired behavior of the circuit is expressed as assertions in
a notation using a combination of Boolean expressions and temporal logic operators. An
assertion is verified by translating it into a sequence of patterns and checks for a ternary
symbolic simulator. This methodology has been used to verify a number of full scale circuit
designs.
1988-01-01 00:00:00
computer sciences