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 formalises 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 the heuristics that specify general-purpose tactics, and AI planning mechanisms. Search is controlled by a type of annotated rewriting called rippling, which controls the selective application of rewrite scaled 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 formal proof for system design and verification. We propose a proof engineering methodology which consists of partitioning the automation of formal proof into three different kind of tasks: user, proof and systems tasks. User tasks have to do with formalising 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. We conjecture that our approach is widely applicable and can be integrated into formal verification environments to improve automation facilities, and be utilised to verify commercial and safety-critical hardware systems in industrial settings.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:561702 |
| Date | January 1997 |
| Creators | Cantu-Ortiz, Francisco Javier |
| Contributors | Bundy, Alan. ; Smaill, Alan. ; Basin, David |
| Publisher | University of Edinburgh |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://hdl.handle.net/1842/588 |
Page generated in 0.0024 seconds