A Mathematically Precise Two-Level Formal Hardware Verification Methodology*
Carl-Johan H. Seger, Jeffrey J. Joyce · 1992
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" inte...