Automatic Hardware Verification Automatic Hardware Verification

Proposer: Alan Bundy, 50-2716, bundy@ed.ac.uk, University of Edinburgh.

Suggested Supervisors: Alan Bundy

Principal goal of the project: To test proof planning on hardware verification problems of `industrial strength'.

Description:

Hardware can be mathematically verified to meet a specification of its intended behaviour. Formal verification can increase confidence that the hardware will behave reliably, safely and securely in use. Both the implementation of the hardware and its specification must be presented as mathematical formulae (usually in a suitable logic) and the verification problem represented as a theorem proving problem. Usually the proofs are not deep, but are long and complicated. Machine assistance is required reduce the tedium and error rate. Verification of a typical piece of industrial hardware usually requires a human user to guide an interactive theorem prover. It can take months or even years and require hundreds or thousands of interactions. The long time delays and high skill levels required in formal verification have meant that this technology has not been taken up by industry except in exceptional circumstances.

Proof planning is a technique, developed at Edinburgh, for guiding the search for a proof using a global outline. We have studied the common patterns in inductive proofs, represented these patterns in proof plans and used them sucessfully to guide large numbers of proof attempts. Francisco Cantu, a PhD student at Edinburgh, has applied proof planning to hardware verification with some success. He has been able to prove many of the verification theorems with no or little user interaction. Typical development times are a few weeks to: study the hardware; represent the specification and implementation in logical form; and prove the theorem. The plans for the proofs are developed automatically in a few minutes. So far, Francisco has applied these to textbook examples of circuits, ranging from an n-bit adder, via a multiplier, shifter and ALU to a complete microprocessor: the Gordon computer.

The next step is to see if this promising start will scale up to real hardware. We have several suppliers who have promised example hardware designs. We also have contacts with Mike Gordon's HOL project at the University of Cambridge. Our plan is to interface our proof planner, CLAM, to guide the HOL interactive theorem prover. HOL has been used for interactive verification of a number of commercial pieces of hardware. These would then become available as test examples for the project.

The PhD student will use CLAM to prove a number of verification theorems. Comparisons will be made with similar proos on rival systems to see if a significant reduction in development time and skill levels can be achieved with proof planning. It will be necessary to tune our proof planner to this domain, eg developing new, domain specific, proof plans; improving the efficiency of CLAM when faced with very large proofs; developing techniques for interaction to patch failed proof attempts. A start has already been made on this tuning, but more will probably be required as more difficult problems are attempted. Work is going on at Cambridge and other labs on the translation from existing commercial specification languages into the logical form required for automatic theorem proving. The student will draw on, and possibly add to, this work.

Resources Required: Access to the CLAM proof planner.

Degree of Difficulty: The basic project is a fairly straightforward application of existing techniques. However, when these prove to be inadequate (as they surely will) there is considerable scope for ingenuity in adapting them to solve the problems that arise.

Background Needed: Knowledge of automated theorem proving. This would suit a student looking for practical applications of formal techniques.

References: