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.
