Correctness of Pipelined Machines

Panagiotis Manolios

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


The correctness of pipelined machines is a subject that has been studied extensively. Most of the recent work has used variants of the Burch and Dill (\cite{Burch94}) notion of correctness. As new features are modeled, \eg interrupts, new notions of correctness are developed. Given the plethora of correctness conditions, the question arises: what is a reasonable notion of correctness? We discuss the issue at length and show, by mechanical proof, that variants of the Burch and Dill notion of correctness are flawed. We propose a notion of correctness based on \webs\ (\cite{Manoliosetal99,Namjoshi97}). Briefly, our notion of correctness implies that the ISA (instruction set architecture) and MA (micro-architecture) machines have the same observable infinite paths, up-to stuttering. This implies that the two machines satisfy the same \ctlsx\ properties and the same safety and liveness properties (up-to stuttering). To test the utility of the idea, we use ACL2 to verify several variants of the simple pipelined machine described by Sawada in \cite{Sawada99,Sawada00}. Our variants extend the basic machine by adding exceptions (to deal with overflows), interrupts, and fleshed-out 128-bit ALUs (one of which is described in a netlist language). In all cases, we prove the same final theorem. We develop a methodology with mechanical support that we used to verify Sawada's machine. The resulting proof is substantially shorter than the original and does not require any intermediate abstractions; in fact, given the definitions and some general-purpose books (collections of theorems), the proof is automatic. A practical and noteworthy feature of \webs\ is their compositionality. This allows one to prove the equivalence of machines in manageable stages and to reuse previous proofs; an example of using \webs\ compositionally is given.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:39
Start Conference Manager
Conference Systems