Verification of Pipelined Machines in ACL2
ACL2 Workshop 2000.
We describe the ACL2 techniques used in a new approach to the
verification of pipelined machines. Our notion of correctness is
based on WEBs (Well-founded Equivalence Bisimulations) and implies
that the pipelined machine and the machine defined by the instruction
set architecture have the same computations up to finite stuttering.
We verify various variants of Sawada's simple machine, including
machines with exceptions, interrupts, non-determinism, and ALUs
described in part at the netlist level. Our proofs contain no
intermediate abstractions and are almost automatic, e.g., the
verification of the base machine does not require any user supplied
theorems. To motivate the need for a new notion of correctness we
show that the variant of the Burch and Dill notion of correctness used
by Sawada can be satisfied by incorrect machines.
Gzipped Postscript (88K)