Formal verification of pipelined processors with precise exceptions

Verification of pipelined processors is a complex and challenging issue. In this paper, we develop a methodology based on translation validation for the verification of pipelined processors that support precise exceptions and out-of-order executions. We have developed a tool integrated with STeP theorem prover for the automatic verification of pipelined architectures. Formal verification of DLX processor is illustrated using our methodology. It is shown that the precise exception modelling is preserved over a range of pipeline instructions of DLX pipeline, like, integer, floating point, branch instructions, etc. The methodology is also illustrated with examples from DLX processor. A comparative evaluation of our method with other approaches is done and a structure of the tool is also provided.