Edinburgh Research Explorer

Experiments in Automating Hardware Verification using Inductive Proof Planning

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Open Access permissions

Open

Original languageEnglish
Title of host publicationFormal Methods in Computer-Aided Design, First International Conference, FMCAD '96, Palo Alto, California, USA
PublisherSpringer-Verlag
ISBN (Print)3-540-61937-2
StatePublished - 1996

Abstract

We present a new approach to automating the verification of hardware designs based on planning techniques. A database of methods is developed that combines tactics, which construct proofs, using specifications of their behaviour. Given a verification problem, a planner uses the method database to build automatically a specialised tactic to solve the given problem. User interaction is limited to specifying circuits and their properties and, in some cases, suggesting lemmas. We have implemented our work in an extension of the Clam proof planning system. We report on this and its application to verifying a variety of combinational and synchronous sequential circuits including a parameterised multiplier design and a simple computer microprocessor.

Download statistics

No data available

ID: 403345