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.
