A Two-Level Formal Verification Methodology using HOL and COSMOS

ID
TR-91-10
Authors
Carl-Johan Seger and Jeffrey J. Joyce
Publishing date
June 1991
Abstract
Theorem-proving and symbolic simulation 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--and its most original contribution--is the suggestion that symbolic simulation and theorem-proving can be combined in a complementary manner. We also outline our plans for the development of a mathematical interface between the two approaches--in particular, a semantic link between the formulation of higher-order logic used in the Cambridge HOL system and the specification language used in the COSMOS system. We believe that this combination offers great potential as a practical formal verification methodology which combines the ability to accurately model circuit level behavior with the ability to reason about digital hardware at higher levels of abstraction.