Digital Circuit Verification using Partially-Ordered State Models

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.