Hierarchical Verification Using an MDG-HOL Hybrid Tool

  • Iskander Kort
  • Sofiene Tahar
  • Paul Curzon
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


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.


  1. 1.
    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.Google Scholar
  2. 2.
    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.CrossRefGoogle Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    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.CrossRefGoogle Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    P. Curzon. The Formal Verification of the Fairisle ATM Switching Element. Technical Report 329, Computer Laboratory, University of Cambridge, U.K., 1994.Google Scholar
  7. 7.
    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.CrossRefGoogle Scholar
  8. 8.
    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.Google Scholar
  9. 9.
    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.zbMATHGoogle Scholar
  10. 10.
    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.CrossRefGoogle Scholar
  11. 11.
    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.Google Scholar
  12. 12.
    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.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    I.M. Leslie and D.R. McAuley. Fairisle:An ATM Network for the Local Area. A CM Communication Review, 19(4):327–336, 1991.CrossRefGoogle Scholar
  14. 14.
    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.Google Scholar
  15. 15.
    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.CrossRefGoogle Scholar
  16. 16.
    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.CrossRefGoogle Scholar
  17. 17.
    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.CrossRefGoogle Scholar
  18. 18.
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Iskander Kort
    • 1
  • Sofiene Tahar
    • 1
  • Paul Curzon
    • 2
  1. 1.Concordia UniversityCanada
  2. 2.Middlesex UniversityUK

Personalised recommendations