# Correctness of Pipelined Machines

Panagiotis Manolios.

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.

# Abstract

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