Verification of a Simple Pipelined Machine Model

  • Jun Sawada
Part of the Advances in Formal Methods book series (ADFM, volume 4)


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.


Commutative Diagram Register File Program Counter Trace Field Pipeline Implementation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 2000

Authors and Affiliations

  • Jun Sawada
    • 1
  1. 1.Department of Computer SciencesUniversity of Texas at AustinUSA

Personalised recommendations