Proof Strategies for Hardware Verification

Ascertaining correctness of digital hardware designs through simulation does not scale-up for large designs because of the sheer combinatorics of the problem. Formal verification of hardware designs holds promise because its computational complexity is of the order of number of different types of components (and not number of components in the design). This approach requires the specification of the behavior and the design in a formal language, and reason with them using a theorem prover. In this paper we attempt to develop a methodology for writing and using these specifications for some important classes of hardware circuits. We examine digital hardware verification in the HOL-90 environment. (HOL-90 is a proof checker written in Standard ML which assists in mechanically checking a formal proof of hardware correctness.) In particular, we analyze proofs for a variety of circuits, and develop proof strategies for combinational circuits and restricted sequential circuits. Overall, this approach makes the theorem proving task less tedious and provides guidance to the user in carrying out proofs.