Correctness of Pipelined Machines
In W. A. Hunt, Jr. and S. D. Johnson, editors, Formal Methods in Computer-Aided Design, FMCAD 2000,
volume 1954 of LNCS, pages 161-178. © Springer-Verlag, 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 notion of correctness. As new features are modeled, e.g., 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 (Well-founded Equivalence Bisimulations). 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 CTL*\X 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. 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 us to prove the correctness of the more
elaborate machines in manageable stages.
Gzipped Postscript (85K) © Springer-Verlag