file.pdf (102.8 kB)
Digital Circuit Verification using Partially-Ordered State Models
journal contribution
posted on 1984-01-01, 00:00 authored by Randal E. Bryant, Carl-Johan H SegerMany 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