Verification of a Simple Pipelined Machine Model

Abstract

The difficulty of pipelined machine verification derives from the fact that there is a complex time-abstraction between the pipelined implementation and its specification which executes instructions sequentially. To study this problem, we define a simple three-stage pipelined machine in ACL2. We prove that this pipelined machine returns the same result as its specification machine. In order to ease the proof, we define an intermediate abstraction called MAETT. This abstraction models the behavior of instructions in the pipelined architecture, and it allows us to define directly and verify invariant conditions about executed instructions. The author used a similar approach to verify a more realistic pipelined machine. This chapter serves as an introduction to the verification of pipelined machines.