Title: On the comparison of hol and boyer-moore for formal hardware verification
Authors: Angelo, Cm ×
Verkest, Diederik
Claesen, Luc
De Man, Hugo #
Issue Date: Feb-1993
Publisher: Kluwer academic publ
Series Title: Formal methods in system design vol:2 issue:1 pages:45-72
Abstract: 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.
ISSN: 0925-9856
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Electrical Engineering - miscellaneous
× corresponding author
# (joint) last author

Files in This Item:

There are no files associated with this item.

Request a copy


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science