File(s) stored somewhere else
Please note: Linked content is NOT stored on Carnegie Mellon University and we can't guarantee its availability, quality, security or accept any liability.
Formal Verification of Digital Circuits Using Symbolic Ternary System Models
Ternary system modeling involves extending the traditional set of binary values {01} 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.