Proof methodologies for processor verification

There are two broad classes of tools used in the verification of hardware circuits: fully automated tools such as model checkers, and semi-automated tools such as theorem provers. Modern hardware processors have reached a level of complexity that is currently beyond the capabilities of fully automated verification. This thesis presents techniques that make the task of verifying processors using a theorem prover much more systematic and automatic. Our goal is to make processor verification accessible to the practicing hardware engineer.; We contribute towards the automation of processor verification in three ways: (1) We present a new temporal logic, GTL, that is appropriate for specifying properties of hardware at the register-transfer level. GTL extends propositional temporal logic by allowing uninterpreted function symbols. This logic allows hardware components to be verified in a hierarchical manner and therefore represents an improvement over model checking for some classes of hardware verification problems. The validity problem for this logic is undecidable. However, a useful decidable fragment of the logic, GTL2, can encode the correctness of pipelined microprocessors. (2) The utility of GTL2 depends on deciding the combination of a number of theories, such as linear arithmetic, arrays, and bit-vectors. This thesis corrects mistakes in Shostak's classical decision procedure for combinations of theories. We present a correctness proof of the corrected Shostak procedure. We also develop procedures for specific theories that are important for hardware verification. (3) The effective verification of GTL2 formulas in a theorem prover requires an efficient high-level methodology for guiding the proof process. We develop a methodology for verifying the correctness of pipelined microprocessors based on the identification of useful Finally we have employed the above techniques to successfully verify the correctness of a super-scalar version of Hennessy and Patterson's DLX pipeline using the PVS verification system.