Efficient verification of bit-level pipelined machines using refinement

In this work, we want to defend the following thesis: Using refinement and a combination of deductive reasoning and decision procedures enables the verification of bit-level pipelined machines in a highly automated, efficient, and scalable manner.; Functional verification is a critical problem facing the semiconductor industry as hardware designs are extremely complex and highly optimized, and as the cost of bugs in deployed systems can be colossal. Pipelining is a key optimization that appears extensively in hardware systems such as microprocessors, multicore systems, and cache coherence protocols. Verifying pipelined machines---models that describe the pipelined behavior of hardware designs---entails showing that these machines behave like their instruction set architectures (ISAs). Existing approaches for verifying bit-level pipelined machines are based on deductive reasoning and require extraordinary expert user effort, as the problem involves reasoning about the difference in time-scale between the pipeline and its ISA and the intricate control circuitry involved in optimized pipeline designs. More automatic approaches are based on the use of decision procedures, but are applicable only to very abstract, high-level models, known as term-level models.; We present a novel, highly automated, efficient, and scalable refinement-based approach for the verification of bit-level pipelined machines. The notion of refinement that we use is compositional and guarantees that pipelined machines satisfy the same safety and liveness properties as their instruction set architectures (ISAs). The high-level idea of the verification approach is to use a deductive reasoning engine, such as the ACL2 theorem proving system, to reduce the bit-level pipelined machine verification problem to a term-level problem. This drastically reduces the amount of expert user effort required when compared to approaches based on the use of deductive reasoning. The verification of term-level models is automated by providing techniques to express correctness statements in a decidable fragment of first-order logic, which can be handled with existing decision procedures. The verification time required for term-level problems is reduced by optimizing parameters of the refinement framework such as refinement maps, which are functions that map pipelined machine states to instruction set architecture states. We have also developed a complete compositional reasoning framework that can be used to decompose correctness proofs into smaller manageable pieces leading to drastic reductions in verification times and a high-degree of scalability. The verification is discharged using the ACL2-SMT system, which we developed by combining the ACL2 theorem prover with a decision procedure.; The methods developed for term-level verification are evaluated using a large number of complex, highly pipelined machine models. The term-level models incorporate various features such as branch prediction, an instruction queue, an instruction cache, a data cache, and a write buffer. The effectiveness of our verification approach for bit-level pipelined machines is demonstrated using an Intel XScale inspired processor model that implements 593 instructions and has features such as branch prediction, precise exceptions, and predicated instruction execution.