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.
| Identifer | oai:union.ndltd.org:GATECH/oai:smartech.gatech.edu:1853/19815 |
| Date | 24 August 2007 |
| Creators | Srinivasan, Sudarshan Kumar |
| Publisher | Georgia Institute of Technology |
| Source Sets | Georgia Tech Electronic Thesis and Dissertation Archive |
| Detected Language | English |
| Type | Dissertation |
Page generated in 0.0017 seconds