Formal hardware verification by integrating HOL and MDG

ABSTRACT

In order to overcome the limitations of automated tools and the cumbersome proof process of interactive theorem proving, we adopt a hybrid approach for formal hardware verification which uses the strengths of theorem proving (HOL) with powerful mathematical tools such as induction and abstraction, and the advantages of automated tools (MDG) which support equivalence checking and model checking. The MDG system is a decision diagram based verification tool, primarily designed for hardware verification. HOL is a theorem prover built on higher-order logic.

REFERENCES

• 1: Carl Seger, An Introduction to Formal Hardware Verification, University of British Columbia, Vancouver, BC, Canada, 1992
• 2: F. Corella , Z. Zhou , X. Song , M. Langevin , E. Cerny, Multiway Decision Graphs for Automated Hardware Verification, Formal Methods in System Design, v.10 n.1, p.7-46, February 1997 [doi>10.1023/A:1008663530211 ]
• 3: M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
• 4: K. Schneider and T. Kropf, "Verifying Hardware Correctness by Combining Theorem Proving and Model Checking," Tech. Rep. SFB358-C2-5/95, University of Karlsruhe, Karlsruhe, Germany, December 1995.
• 5: S. Rajan , Natarajan Shankar , Mandayam K. Srivas, An Integration of Model Checking with Automated Proof Checking, Proceedings of the 7th International Conference on Computer Aided Verification, p.84-97, July 03-05, 1995
• 6: Jeffrey J. Joyce , Carl-Johan H. Seger, Linking BDD-based symbolic evaluation to interactive theorem-proving, Proceedings of the 30th international conference on Design automation, p.469-474, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164981]
• 7: M. 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.
• 8: Ying Xu , Eduard Cerny , Xiaoyu Song , Francisco Corella , Otmane Aït Mohamed, Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs, Proceedings of the 10th International Conference on Computer Aided Verification, p.219-231, June 28-July 02, 1998
• 9: Z. Zhou and i. Boulerice, MDG Tools (VI.0) User's Manual. Dept. of Computer Science, University of Montreal, Montreal, Canada, June 1996.
• 10: P. Curzon, S. Tahar, and O. Ait-Mohamed, "Verification of the MDG Components Library in HOL," in Theorem Proving in Higher Order Logics: Emerging Trends (J. Grundy and M. Newey, eds.), (Australian National University, Canberra, Australia), pp. 31-45, September 1998.
• 11: Haiyan Xiong , Paul Curzon , Sofiène Tahar, Importing MDG Verification Results into HOL, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, p.293-310, September 01, 1999
• 12: Ian Leslie , Derek McAuley, Fairisle: an ATM network for the local area, ACM SIGCOMM Computer Communication Review, v.21 n.4, p.327, Sept. 1991
• 13: P. Curzon, "The Formal Verification of the Fairisle ATM Switching Element," Techical Report 329, Computer Laboratory, University of Cambridge, U.K., March 1994.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN

General Terms:
Performance, Theory, Verification