I will argue that proofs and proof assistants in some form, in combination with automated methods, are necessary to close this gap. However, the considerations that drive the disign of a proof assistant for hardware verification and not necessarily those that have shaped existing generalpurpose proof assistants. In particular, for a hardware proff assistant, the requirements in terms of logical expressiveness and the power of its deductive machinerey are minimal. For example, the ability to reason about higher-order objects like sets and functions is probably superfluous in the hardware domain.

Rather, the primary consideration in constructing proofs of complex systems is that proofs be concise and maintainable. This means that a proof system must take maximum advantage of the strengths of model checking and automated decision procedures in order to minimize the need for manual decomposition of proofs. It is thus important to concider how inference rules and dicision procedures (e.g., model checking) interact to allow concise proof decompositions in a particular domain of application. As an example, I will show how model checking combined with a few simple but domain-tailored inference rules allows surprisingly concise proofs about out-of-order instruction processors. This is chiefly because basing the proof on model checking eliminates the need to state and prove global invariants.

Along the way, I will also discuss some practical considerations for the design of large, formally verified, hardware systems. In particular, the most concise proof decompositions for hardware systems are often non-hierarchical. Rather, profs often decompose most naturally according to the paths followed by data and control through the system under various conditions, rather than according to structural hierarchy. Further, design for compositional verification differs strongly from the paradigm of design-by-debugging that is currently prevalent. The debugging approach leads to complex (and often unknown) interactions between design componets, whereas the formal approach favors the disign of “bulletproof” components, that implement a given abstract model without any assumptions about environment behavior.