Formal methods in system design vol:2 issue:1 pages:45-72
Faced with the challenge of designing correct circuits, the research community has been applying alternative verification methodologies instead of only traditional methods like ad hoc simulation. The best choice among alternatives like tautology checking, symbolic simulation, and theorem proving depends very much on the kind of circuit to be verified and on the level of abstraction considered. When theorem proving is best applicable, one is faced with the problem of choosing a formalism. This article compares the proof assistant HOL and the theorem-prover Boyer-Moore based on a practical experience with both systems in order to verify a combinatorial and parameterized hardware module from the CATHEDRAL II Silicon Compiler library. Although the comparison is based on a specific application, the general features, advantages, and drawbacks of both systems are discussed, with consideration given to the verification of other kinds of circuits.