ACL2 Seminar
Ben Selfridge
Sept. 16, 2016

Proving Correctness of a Simple Microprocessor Pipeline

We discuss a Ph.D. thesis by Jun Sawada, "Formal Verification of an
Advanced Pipeline Machine." This work provides a blueprint for proving
formal correctness of a pipelined microprocessor. We demonstrate the
proof methodology described in this work by proving correctness of an
extremely simple pipeline machine. The correctness theorem is stated
in terms of a specification of an instruction set architecture (ISA):
when the pipelined machine is "flushed" (i.e. there is no instruction
in the intermediate "latch" registers), then we can project out the
state of the program counter, the memory, and the register file. The
theorem states that stepping the pipelined machine for n cycles is
equivalent (via the above projection) to stepping the ISA "machine"
specification for m cycles, where m is a function of n and the
initial state of the pipelined machine. After describing the basic
methodology (due to Sawada), we discuss plans to extend this work to
account for more complex memory systems, which will be a potentially
fruitful area for the speaker's Ph.D. research. Finally, we invite a
discussion on the novelty and potential directions of this research,
and input from the audience will be requested.