Abstract
Formal hardware verification systems can be split into two categories: theorem proving systems and automatic finite state machine based systems. Each approach has its own complementary advantages and disadvantages. In this paper, we consider the combination of two such systems: HOL (a theorem proving system) and MDG (an automatic system). As HOL hardware verification proofs are based on the hierarchical structure of the design, submodules can be verified using other systems such as MDG. However, the results of MDG are not in the appropriate form for this. We have proved a set of theorems that express how results proved using MDG can be converted into the form used in traditional HOL hardware verification.
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. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computer Surveys, 24(3), September 1992.
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. The formal verification of the Fairisle ATM switching element. Technical Report 329, University of Cambridge, Computer Laboratory, March 1994.
P. Curzon. Tracking design changes with formal machine-checked proof. The Computer Journal, 38(2), July 1995.
P. Curzon, S. Tahar, and O. Aït-Mohamed. The verification of aspects of a decision diagram based verification system. In Jim Grundy and Malcolm Newey, editors, Theorem Proving in Higher-Order Logics: Emerging Trends, pages 31–46. Department of Computer Science, The Australian National University, 1998.
M. J. C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design: the 1985 Edinburgh Workshop on VLSI, pages 153–177. North-Holland, 1986.
M. J. C. Gordon. Combining deductive theorem proving with symbolic state enumeration. Presented at 21 Years of Hardware Verification, Royal Society Workshop to mark 21 years of BCS FACS, http://www.cl.cam.ac.uk/users/mjcg/BDD, December 1998.
M. J. C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher-order Logic. Cambridge University Press, 1993.
K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal methods Europe FME’ 96, number 1051 in Lecture Notes in Computer Science, pages 662–682, March 1996.
J. Joyce and C. Seger. Linking BDD-based symbolic evaluation to interactive theorem-proving. In the 30th Design Automation Conference, 1993.
S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Pierre Wolper, editor, Computer-Aided Verification, number 939 in Lecture Notes in Computer Science, pages 84–97. Springer-Verlag, 1995.
S. Tahar and P. Curzon. Comparing HOL and MDG: A case study on the verification of an ATM switch fabric. To appear in the Nordic Journal of Computing.
S. Tahar, X. Song, E. Cerny, Z. Zhou, M. Langevin, and O. Aït-Mohamed. Modeling and automatic formal verification of the Fairisle ATM switch fabric using MDGs. To appear in IEEE Transactions on CAD of Integrated Circuits and Systems.
H. Xiong and P. Curzon. The verification of a translator for MDG’s components in HOL. In MUCORT98, Third Middlesex University Conference on Research in Technology, pages 55–59, April 1998.
Z. Zhou and N. Boulerice. MDG Tools (V1.0) User Manual. University of Montreal, Dept. D’IRO, 1996.
Z. Zhu, J. Joyce, and C. Seger. Verification of the Tamarack-3 microprocessor in a hybrid verification environment. In Higher-Order Logic theorem proving and Its Applications, The 6th International Workshop, number 780 in Lecture Notes in Computer Science, pages 252–266. B. C., Canada, August 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xiong, H., Curzon, P., Tahar, S. (1999). Importing MDG Verification Results into HOL. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1999. Lecture Notes in Computer Science, vol 1690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48256-3_20
Download citation
DOI: https://doi.org/10.1007/3-540-48256-3_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66463-5
Online ISBN: 978-3-540-48256-7
eBook Packages: Springer Book Archive