Formal Hardware Verification In Hol And In Boyer-moore: A Comparative Analysis
Catia M. Angelo, Diederik Verkest, Luc Claesen, H. De Man · 2005
Different types of problems in the hardware verification field have inspired different methodologies to tackle them. When different approaches can verify the same class of circuits, at a given level of abstraction, it is often the case that each one has advantages and drawbacks with respect to the others. Comparing different methodologies is important, not only to identify the right tool for the right task, but also to evaluate the compromises of different approaches. This paper summarises a comparison between the theorem proving environments HOL and Boyer-Moore, based on a practical experience with both systems for the verification of a parameterised module from the CATHE DRAL Silicon Compiler library.