Efficient Verification of Bit-Level Pipelined Machines Using Refinement

Functional verification is a critical problem facing the semiconductor industry: hardware designs are extremely complex and highly optimized, and even a single bug in deployed systems can cost more than $10 billion. We focus on the verification of pipelining, a key optimization that appears extensively in hardware systems such as microprocessors, multicore systems, and cache coherence protocols. Existing techniques for verifying pipelined machines either consume excessive amounts of time, effort, and resources, or are not applicable at the bit-level, the level of abstraction at which commercial systems are designed and functionally verified. We present a highly automated, efficient, compositional, and scalable refinement-based approach for the verification of bit-level pipelined machines. Our contributions include: (1) A complete compositional reasoning framework based on refinement. Our notion of refinement guarantees that pipelined machines satisfy the same safety and liveness properties as their instruction set architectures. In addition, our compositional framework can be used to decompose correctness proofs into smaller, more manageable pieces, leading to drastic reductions in verification times and a high-degree of scalability. (2) The development of ACL2-SMT, a verification system that integrates the popular ACL2 theorem prover (winner of the 2005 ACM Software System Award) with decision procedures. ACL2-SMT allows us to seamlessly take advantage of the two main approaches to hardware verification: theorem proving and decision procedures. (3) A proof methodology based on our compositional reasoning framework and ACL2-SMT that allows us to reduce the bit-level verification problem to a sequence of highly automated proof steps. (4) A collection of general-purpose refinement maps, functions that relate pipelined machine states to instruction set architecture states. These refinement maps provide more flexibility and lead to increased verification efficiency. The effectiveness of our approach is demonstrated by verifying various pipelined machine models, including a bit-level, Intel XScale inspired processor that implements 593 instructions and includes features such as branch prediction, precise exceptions, and predicated instruction execution.Ph.D.Committee Chair: Manolios, Panagiotis; Committee Member: Chatterjee, Abhijit; Committee Member: Gopalakrishnan, Ganesh; Committee Member: Lim, Sung-Kyu; Committee Member: Yalamanchili, Sudhaka