Decomposing the Proof of Correctness of pipelined Microprocessors

We present a systematic approach to decompose and incrementally build the proof of correctness of pipelined microprocessors. The central idea is to construct the abstraction function using completion functions, one per un nished instruction, each of which specify the e ect (on the observables) of completing the instruction. In addition to avoiding term-size and case explosion as could happen for deep and complex pipelines during ushing and helping localize errors, our method can also handle stages with iterative loops. The technique is illustrated on pipelined- as well as a superscalar pipelined implementations of a subset of the DLX architecture.

• Type: Conference
• Year: 1998
• Where: CAV
• Authors: Ravi Hosabettu, Mandayam K. Srivas, Ganesh Gopalakrishnan
• Keywords: Abstraction Function, CAV 1998, Hardware, Superscalar Pipelined Implementations, Systematic Approach