Technical Report

Comparing HOL, MDG and VIS: A Case Study on the Verification of an ATM Switch Fabric

P. Curzon, S. Tahar, and J. Lu


ABSTRACT

There exist a wide range of hardware verification tools, some based on interactive theorem proving and other more automated tools based on decision diagrams. In this paper, we compare three different verification systems covering the spectrum of today's verification technology. In particular, we consider HOL, MDG and VIS. HOL is an interactive theorem proving system based on higher-order logic. VIS is an automatic system based on ROBDDs and integrating verification with simulation and synthesis. The MDG system is an intermediate approach based on Multiway Decision Graphs providing automation while accommodating abstract data sorts, uninterpreted functions and rewriting. As the basis for our comparison we used all three systems to independently model and verify a fabricated ATM communications chip: the Fairisle 4x4 switch fabric.

 


Download postscript file (PS File)
Send comments and suggestions to: tahar@ece.concordia.ca