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 verify a fabricated ATM communications chip: the Fairisle 4×4 switch fabric.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Trans. on Computers, C-35(8):677–691, 1986.
R. Brayton et. al. VIS: A System for Verification and Synthesis In R. Alur and T. Henzinger, eds, Computer Aided Verification, LNCS 1102, 428–432, Springer-Verlag, 1996.
F. Corella, Z. Zhou, X. Song, M. Langevin, and E. Cerny. Multiway Decision Graphs for Automated Hardware Verification. Formal Methods in System Design, 10(1):7–46, 1997.
P. Curzon and I.M. Leslie. Improving Hardware Designs whilst Simplifying their Proof. Designing Correct Circuits, Workshops in Comp., Springer-Verlag, 1996.
K. Edgcombe. The Qudos Quick Chip User Guide. Qudos Limited.
E. Garcez and W. Rosenstiel. The Verification of an ATM Switching Fabric using the HSIS Tool. In IX Brazilian Symp. on the Design of Integrated Circuits, 1996.
M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher-order Logic. Cambridge University Press, 1993.
L. Jakubiec, S. Coupet-Grimal, and P. Curzon. A Comparison of the Coq and HOL Proof Systems for Specifying Hardware. In E. Gunter and A. Felty, eds, Theorem Proving in Higher Order Logics: Short Presentations, 63–78, 1997.
I.M. Leslie and D.R. McAuley. Fairisle: An ATM Network for the Local Area. ACM Communication Review, 19(4):327–336, 1991.
D.E. Long. Model Checking, Abstraction and Compositional Verification. Ph.D thesis, Carnegie Mellon University, July 1993.
J. Lu and S. Tahar. Practical Approaches to the Automatic Verification of an ATM Switch Fabric using VIS. In Proc. IEEE Great Lakes Symp. on VLSI, 368–373, 1998.
K. Schneider and T. Kropf. Verifying Hardware Correctness by Combining Theorem Proving and Model Checking. In J. Alves-Foss, editor, Higher Order Logic Theorem Proving and Its Applications: Short Presentations, 89–104, 1995.
S. Tahar, Z. Zhou, X. Song, E. Cerny, and M. Langevin. Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs. In Proc. IEEE Great Lakes Symp. on VLSI, 106–111, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tahar, S., Lu, J., Curzon, P. (1998). Three Approaches to Hardware Verification: HOL, MDG, and VIS Compared. In: Gopalakrishnan, G., Windley, P. (eds) Formal Methods in Computer-Aided Design. FMCAD 1998. Lecture Notes in Computer Science, vol 1522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49519-3_28
Download citation
DOI: https://doi.org/10.1007/3-540-49519-3_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65191-8
Online ISBN: 978-3-540-49519-2
eBook Packages: Springer Book Archive