Abstract
We describe a hybrid formal hardware verification tool that links the HOL interactive proof system and the MDG automated hardware verification tool. It supports a hierarchical verification approach that mirrors the hierarchical structure of designs. We obtain advantages of both verification paradigms. We illustrate its use by considering a component of a communications chip. Verification with the hybrid tool is significantly faster and more tractable than using either tool alone.
Chapter PDF
Similar content being viewed by others
References
M.D. Aagaard, M. Leeser, and P. Windley. Toward a super duper hardware tactic. In J.J. Joyce and C.H. Seger, editors, Higher Order Logic Theorem Proving and Its Applications, LNCS 780, pages 400–413. Springer-Verlag, 1993.
M.D. Aagaard, R.B. Jones, and C-J.H. Seger. Lifted-FL:A Pragmatic Implementation of Combined Model Checking and Theorem Proving. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, LNCS 1690, pages 323–340. Springer-Verlag, 1999.
S. Balakrishnan and S. Tahar. A Hierarchical Approach to the Formal Verification of Embedded Systems Using MDGs. In Proceedings IEEE 9th Great Lakes Symposium on VLSI, Ann Arbor, Michigan, USA, March 1999, pages 284–287.
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, S. Tahar, and O. Ait-Mohamed. Verification of the MDG Components Library in HOL. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics:Emerging Trends, pages 31–45, Australian National University, 1998.
P. Curzon. The Formal Verification of the Fairisle ATM Switching Element. Technical Report 329, Computer Laboratory, University of Cambridge, U.K., 1994.
L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham. The PROSPER Toolkit. In Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS 1785, Springer Verlag, 2000.
M.J.C. Gordon. Combining Deductive Theorem Proving with Symbolic State Enumeration. 21 Years of Hardware Verification, December 1998. Royal Society Workshop to mark 21 years of BCS FACS.
M.J.C. Gordon and T.F. Melham. Introduction to HOL:A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, U.K., 1993.
J. Hurd. Integrating Gandalf and HOL. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, LNCS 1690, pages 311–321. Springer Verlag, 1999.
J.J. Joyce and C.J.H. Seger. Linking BDD-based Symbolic Evaluation to Interactive Theorem Proving. In Proceedings of the 30th Design Automation Conference, pages 469–474, Dallas, TX, June 1993.
R. Kumar, K. Schneider and T. Kropf. Structuring and Automating Hardware Proofs in a Higher-Order Theorem-Proving Environment. Formal Methods in System Design, 2:165–223, 1993.
I.M. Leslie and D.R. McAuley. Fairisle:An ATM Network for the Local Area. A CM Communication Review, 19(4):327–336, 1991.
S. Rajan, N. Shankar, and M.K. Srivas. An Integration of Model-checking with Automated Proof Checking. In Pierre Wolper, editor, Computer Aided Verification, Lecture Notes in Computer Science 939, pages 84–97. Springer Verlag, 1995.
K. Schneider and D.W. Hoffmann. A HOL Conversion for Translating Linear Time Temporal Logic to ú-Automata. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, LNCS 1690. Springer Verlag, 1999.
S. Tahar, X. Song, E. Cerny, Z. Zhou, M. Langevin and O. Ait-Mohamed. Modeling and Verification of the Fairisle ATM Switch Fabric using MDGs. IEEE Transactions on CAD of Integrated Circuits and Systems, 18(7):956–972, 1999.
H. Xiong, P. Curzon, and S. Tahar. Importing MDG Results into HOL. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, LNCS 1690, 293–310. Springer Verlag, 1999.
M.H. Zobair and S. Tahar. On the Modeling and Verification of a Telecom System Block Using MDGs. Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kort, I., Tahar, S., Curzon, P. (2001). Hierarchical Verification Using an MDG-HOL Hybrid Tool. In: Margaria, T., Melham, T. (eds) Correct Hardware Design and Verification Methods. CHARME 2001. Lecture Notes in Computer Science, vol 2144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44798-9_21
Download citation
DOI: https://doi.org/10.1007/3-540-44798-9_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42541-0
Online ISBN: 978-3-540-44798-6
eBook Packages: Springer Book Archive