Proof Planning for Automating Hardware Verification

From bibtex.

Abstract

In this thesis we investigate the applicability of proof planning to automate the verification of hardware systems. Proof planning is a meta-level reasoning technique which captures patterns of proof common to a family of theorems. It contributes to the automation of proof by incorporating and extending heuristics found in the Nqthm theorem prover and using them to guide a tactic-based theorem prover in the search for a proof. We have addressed the automation of proof for hardware verification from a proof planning perspective, and have applied the strategies and search control mechanisms of proof planning to generate automatically customised tactics which prove conjectures about the correctness of many types of circuits. The contributions of this research can be summarised as follows: (1) we show by experimentation the applicability of the proof planning ideas to verify automatically hardware designs; (2) we develop and use a methodology based on the concept of proof engineering using proof planning to verify various combinational and sequential circuits which include: arithmetic circuits (adders, subtracters, multipliers, dividers, factorials), data-path components (arithmetic logic units, shifters, processing units), and a simple microprocessor system; and (3) we contribute to the profiling of the Clam proof planning system by improving its robustness and efficiency in handling large terms and proofs. In verifying hardware, the user formallises a problem by writing the specification, the implementation and the conjecture, using a logic language, and asks Clam to compose a tactic to prove the conjecture. This tactic is then executed by the Oyster prover. To compose a tactic, Clam uses a set of methods which implement heuristics that specify general-purpose tactics, aand AI planning mechanisms. Search is controlled by a type of annotated rewriting called rippling, which controls the selective application of rewrites called wave rules. We have extended some of the Clam's methods to verify circuits. The size of the proofs were orders of magnitude larger than the proofs that had been attempted before with proof planning, and are comparable with similar verification proofs obtained by other systems, but using fewer lemmas and less interaction. Proof engineering refers to the application of formall proof for system design and verification. We propose a proof engineering methodology which consists of partitioning the automation of formall proof into three different kind of tasks: user, proof and systems tasks. User tasks have to do with formallising a particular verification problem and using a formal tool to obtain a proof. Proof tasks refer to the tuning of proof techniques (e.g. methods and tactics) to help obtain a proof. Systems tasks have to do with the modification of a formal tool system. By making this distinction explicit, proof development is more manageable.