Automatic Verification of Pipelined Microprocessors

Abstract - 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 micro...

• Type: Conference
• Year: 1994
• Where: DAC
• Authors: Vishal Bhagwati, Srinivas Devadas
• Keywords: Computer Architecture, DAC 1994, Implementation, Input/output Behavior, Large Digital Designs