Efficient Verification of Bit-Level Pipelined Machines Using Refinement

Refinement;Microprocessor pipelines;Formal verification;Hardware verification

Srinivasan, Sudarshan Kumar ; Electrical and Computer Engineering

University:Georgia Institute of Technology

Department:Electrical and Computer Engineering

关键词: Refinement;    Microprocessor pipelines;    Formal verification;    Hardware verification;   

Others  :  https://smartech.gatech.edu/bitstream/1853/19815/1/srinivasan_sudarshan_k_200712_phd.pdf

美国|英语

来源: SMARTech Repository

【 摘 要 】

Functional verification is a critical problem facing the semiconductorindustry: hardware designs are extremely complex and highly optimized,and even a single bug in deployed systems can cost more than $10billion.We focus on the verification of pipelining, a keyoptimization that appears extensively in hardware systems such asmicroprocessors, multicore systems, and cache coherence protocols.Existing techniques for verifying pipelined machines either consumeexcessive amounts of time, effort, and resources, or are notapplicable at the bit-level, the level of abstraction at whichcommercial systems are designed and functionally verified.We present a highly automated, efficient, compositional, and scalablerefinement-based approach for the verification of bit-level pipelinedmachines.Our contributions include:(1) A complete compositional reasoning framework based on refinement.Our notion of refinement guarantees that pipelined machines satisfythe same safety and liveness properties as their instruction setarchitectures.In addition, our compositional framework can be used to decomposecorrectness proofs into smaller, more manageable pieces, leading todrastic reductions in verification times and a high-degree ofscalability.(2) The development of ACL2-SMT, a verification system that integratesthe popular ACL2 theorem prover (winner of the 2005 ACM SoftwareSystem Award) with decision procedures.ACL2-SMT allows us toseamlessly take advantage of the two main approaches to hardwareverification: theorem proving and decision procedures.(3) A proof methodology based on our compositional reasoning frameworkand ACL2-SMT that allows us to reduce the bit-level verificationproblem to a sequence of highly automated proof steps.(4) A collection of general-purpose refinement maps, functions thatrelate pipelined machine states to instruction set architecturestates.These refinement maps provide more flexibility and lead toincreased verification efficiency.The effectiveness of our approach is demonstrated by verifying variouspipelined machine models, including a bit-level, Intel XScale inspiredprocessor that implements 593 instructions and includes features suchas branch prediction, precise exceptions, and predicated instructionexecution.