Automatic Verification of Pipelined Microprocessors

10 years 8 months ago
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...
Vishal Bhagwati, Srinivas Devadas
Added 09 Aug 2010
Updated 09 Aug 2010
Type Conference
Year 1994
Where DAC
Authors Vishal Bhagwati, Srinivas Devadas
Comments (0)