Combining Algebraic and Algorithmic Verification of Microarchitectures

Nancy Day, Mark Aagaard, Byron Cook

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


Algebraic verification techniques manipulate the structure of a circuit while preserving its behavior. Algorithmic verification techniques verify properties about the behavior of a circuit. These two techniques have complementary strengths, which makes it desirable to exploit both of them in the same verification. However, algebraic techniques typically use stream-based descriptions of circuits, while algorithmic techniques use state-based descriptions. We describe a technique for calculating a state machine from a stream-based model by reinterpreting the primitives for constructing models. We prove that the technique preserves the behavior of the model and apply the technique to combine algebraic rewriting, symbolic model checking, and symbolic simulation based validity checking to verify a pipelined microarchitecture with speculative execution.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:39
Start Conference Manager
Conference Systems