Carnegie Mellon University
Browse

Formal Verification of Digital Circuits Using Symbolic Ternary System Models

Download (177.71 kB)
journal contribution
posted on 1988-01-01, 00:00 authored by Randal E. Bryant, Carl-Johan Seger
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.

History

Publisher Statement

All Rights Reserved

Date

1988-01-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC