The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

PhD Thesis #9709

Title:Proof Planning for Automating Hardware Verification
Authors:Cantu Ortiz,F
Date: 1997
Presented:
Keywords:
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 proven in the search for a proof. We have addresssed 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, mulltipliers, 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.
Download:NO ONLINE COPY

[Search These Pages] [DAI Home Page] [Comment]