A Mathematically Precise Two-Level Formal Hardware Verification Methodology*

ID
TR-92-34
Authors
Carl-Johan H. Seger and Jeffrey J. Joyce
Publishing date
December 1992
Length
34 pages
Abstract

Theorem-proving and symbolic trajectory evaluation are both described as methods for the formal verification of hardware. They are both used to achieve a common goal -- correctly designed hardware -- and both are intended to be an alternative to conventional methods based on non-exhaustive simulation. However, they have different strengths and weaknesses. The main significance of this paper is the description of a two-level approach to formal hardware verification, where the HOL theorem prover is combined with the Voss verification system. From symbolic trajectory evaluation we inherit a high degree of automation and accurate models of circuit behavior and timing. From interactive theorem-proving we gain access to powerful mathematical tools such as induction and abstraction. The interface between the HOL and Voss is, however, more than just an ad hoc translation of verification results obtained by one tool into input for the other tool. We have developed a "mathematical" interface where the results of the Voss system is embedded in HOL. We have also prototyped a hybrid tool and used this tool to obtain verification results that could not be easily obtained with previously published techniques.