Digital Circuit Verification using Partially-Ordered State Models

<p> </p><p> </p><p>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</p> <p><em><em>X </em></em>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.</p> <p></p> <p></p>