Abstract
Making formal verification a practicality in industrial environments is still difficult. The capacity of most verification tools is too small, their integration in a design process is difficult and the methodology that should guide their usage is unclear.
This paper describes a step-by-step methodology which was developed for the practical application of formal verification. The methodology was successfully realized in a production environment of hardware design. The realization involved the development of a system consisting of several tools, while using the SMV [McM93] verification tool as the system core.
This system was used in the verification of eight designs. We specifically elaborate on the verification of a bus-bridge design, which was particularly successful in uncovering and eliminating many hardware design errors.
Chapter PDF
Similar content being viewed by others
References
I. Beer, “Formal Verification of Hardware”, M.Sc. Thesis, EE Department, Technion, 1992 (in Hebrew).
R.E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Trans. Computers, Vol. C-35, August 1986.
E.M. Clarke and E.A. Emerson, “Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic”, in: Proceedings of the Workshop on Logic of Programs, LNCS 131, 1981. Temporal Logic Specifications: A Practical Approach”, Tenth ACM Symposium on Principles of Programming Languages, Austin, Texas, 1983.
E.M. Clarke, E.A. Emerson and A.P. Sistla, “Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications: A Practical Approach”, Tenth ACM Symposium on Principles of Programming Languages, Austin, Texas, 1983.
M. Clint, “Program Proving: Coroutines”, Acta informatica, 2(1), 50–63, 1973.
E.A. Emerson, “Temporal and Modal Logic”, in: Handbook of Theoretical Computer Science, J. van Leeuwen, ed., North-Holland, 1989.
D. Geist and I. Beer, “Efficient Model Checking by Automated Ordering of Transition Relation Partitions”, submitted for publication, 1994.
O. Grumberg and D.E. Long, “Model Checking and Modular Verification”, in: LNCS 527, 1991.
R.P. Kurshan, “Reducibility in Analysis of Coordination”, in: LNCS 103, 1987.
D.E. Long, “Model Checking, Abstraction and Compositional Verification”, Ph.D. Thesis, CMU, 1993.
K.L. McMillan, “Symbolic Model Checking”, Kluwer Academic Publishers, 1993.
Z. Manna and A. Pnueli, “The Temporal Logic of Reactive and Concurrent Systems; Specification”, Springer-Verlag, 1991.
“PCI Local Bus Specification, Revision 2.0”, PCI Special Interest Group, 1993.
A. Pnueli, “Applications of Temporal Logic to the Specification and Verification of Recative Systems: A Survey of Current Trends”, in: Current Trends in Concurrency, J.W.de Bakker et al., eds., LNCS 224, 1986.
G. Shurek and O. Grumberg, “The modular Framework of Computer-Aided Verification: Motivation, Solutions and Evaluation Criteria”, CAV90.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beer, I., Ben-David, S., Geist, D., Gewirtzman, R., Yoeli, M. (1994). Methodology and system for practical formal verification of reactive hardware. In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_53
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_53
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive