Carnegie Mellon University
file.pdf (102.8 kB)

Digital Circuit Verification using Partially-Ordered State Models

Download (102.8 kB)
journal contribution
posted on 1984-01-01, 00:00 authored by Randal E. Bryant, Carl-Johan H Seger
Many aspects of digital circuit operation can be efficiently verified by simulating circuit operation over “weakened” state values. This technique has long been practiced with logic simulators, using the value X to indicate a signal that could be either 0 or 1. This concept can be formally extended to a wider class of circuit models and signal values, yielding lattice-structured state domains. For more precise modeling of circuit operation, these values can be encoded in binary and hence represented symbolically as Ordered Binary Decision Diagrams. The net result is a tool for formal verification that can apply a hybrid of symbolic and partially-ordered evaluation


Publisher Statement

All Rights Reserved



Usage metrics