Refinement and Theorem Proving
International School on Formal Methods for the Design of Computer, Communication, and Software Systems: Hardware Verification, 2006. © Springer Verlag
In this chapter, we describe the ACL2 theorem proving system and show how it can be used to model and verify hardware using refinement.
This is a timely problem, as the ever-increasing complexity of microprocessor designs and the potentially devastating economic consequences of shipping defective products has made functional verification a bottleneck in the microprocessor design cycle, requiring a large amount of time, human effort, and resources. For example, the 1994 Pentium FDIV bug cost Intel $475 million and it is estimated that a similar bug in the current generation Intel Pentium processor would cost Intel $12 billion.
One of the key optimizations
used in these designs is pipelining, a topic that has received a
fair amount of interest from the research community. In this
chapter, we show how to define a pipelined machine in ACL2 and
how to use refinement to verify that it correctly implements its
instruction set architecture. We discuss how to automate such
proofs using theorem proving, decision procedures, and hybrid
approaches that combine these two methods. We also outline future
PDF (260K) © ACM
Proof scripts. Tarred, Gzipped, 12K