Department of Computer Sciences 1999 ACL2 Workshop March 29 - March 31, 1999

Verifying A Simple Pipelined Machine Model

I have been working on the verification of pipelined machines for my dissertation work. I have designed a pipelined machine, which is finally named FM9801, and verified that its pipelined implementation matches the non-pipelined specification. This machine contained various features that have not been subjected to formal verification in the past, such as speculative execution, internal and external interrupts, memory write buffers, Tomasulo's algorithm and so on. I wish I can give this work as a example to the ACL2 workshop, but it is a little:-) bit larger than what we can discuss in detail.

Instead, I will discuss a much smaller machine with only three stages without data-memory, and illustrate a complete proof of our criterion. My hope is once you understand what is going on in this little example, you will have a good insight into the proof I constructed for the large FM9801 proof, that took about 1.7MByte of ACL2 script.

I will introduce this small machine and describe how the behaviors at the ISA and MA levels are specified. Then, we will talk about our correctness criterion. And finally we will discuss the intermediate abstraction MAETT and invariants defined over it. I will also give a brief sketch of the final correctness proof.

Jun Sawada