@INPROCEEDINGS{Cantu96,
AUTHOR = "Francisco Cantu and Alan Bundy and Alan Smaill and David Basin",
TITLE = "Experiments in Automating Hardware Verification using Inductive Proof Planning",
BOOKTITLE = "Formal Methods in Computer-Aided Design (FMCAD-96)",
YEAR = 1996,
ADDRESS = "Palo Alto, USA",
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.  },
}