Automatic Verification of Pipelined Microprocessors

We address the problem of automatically verifying large digital designs at the logic level, against high-level specifications. In this paper, we present a methodology which allows for the verification of a specific class of synchronous machines, namely pipelined microprocessors. The specification is the instruction set of the microprocessor with respect to which the correctness property is to be verified. A relation, namely the β-relation, is established between the input/output behavior of the implementation and specification. The relation corresponds to changes in the input/output behavior that result from pipelining, and takes into account data hazards and control transfer instructions that modify pipelined execution. The correctness requirement is that the β-relation hold between the implementation and specification. We use symbolic simulation of the specification and implementation to verify their functional equivalence. We characterize the pipelined and unpipelined microprocessors as definite machines (i.e. a machine in which for some constant k, the output of the machine depends only on the last k inputs) for verification purposes. We show that only a small number of cycles, rather than exhaustive state transition graph traversal and state enumeration, have to be simulated for each machine to verify whether the implementation is in β-relation with the specification. Experimental results are presented.