AbstractInteractive formal proof and automated verification based on decision graphs are two contrasting formal hardware verification techniques. In this paper, we compare these two approaches. In particular, we consider HOL and MDG. The former is an interactive theorem-proving system based on higher-order logic, while the latter is an automatic system based on Multiway Decision Graphs. As the basis for our comparison we have used both systems to independently verify a fabricated ATM communications chip, the Fairisle 4 by 4 switch fabric.
Categories and Subject Descriptors: B.4.4 [Input/Output and Data Communications]: Performance Analysis and Design Aids; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic
Additional Key Words and Phrases: hardware verification, formal methods, tools comparison, theorem proving, equivalence checking, property checking, HOL, MDG, ATM