Abstract
As described in chapter 9 the aim of formal verification is to prove the correctness of a circuit implementation with respect to its specification. In theory the proof of correctness can be carried out by simulating the circuit for all possible input samples and comparing the results with the specification. However, in practice such a verification by exhaustive simulation is too time consuming. Using formal verification the same information can be obtained in less time.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bryant, R. E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, Vol. C-35, No. 8, 1986
Eveking, H.: Applied Formal Hardware Verification Methods. Tutorial, DATE’99, 1999
Gordon, M. J. C.; Melham, T. F.: Introduction to HOL. Cambridge University Press, 1993
Hsieh, Y.-W.; Levitan, S. P.: Model Abstraction for Formal Verification. DATE’98, 1998
Meinel, C.; Stangier, C.: Increasing Efficiency of Symbolic Model Checking by Accelerating Dynamic Variable Reordering. DATE’99,1999
Melham, T. F.: Abstraction Mechanisms for Hardware Verification. Technical Report No. 106, University of Cambridge Computer Laboratory, 1987
Mohnke, J.: A Signature-Based Approach to Formal Logic Verification. Dissertation, University of Halle, 1999
Payer, M.; Voges, J.: How We Cracked the PENTIUM Bug within 5 Minutes with CVE. Technical Report, Siemens AG, HL CAD SV, Mch B, München, 1997
Reetz, R.; Schneider, K.; Kropf, T.: Formal Specification in VHDL for Hardware Verification. DATE’98, 1998
Thornton, M. A.; Williams, J. P.; Drechsler, R.; Drechsler, N.: Variable Reordering for Shared Binary Decision Diagrams Using Output Probabilities. DATE’99, 1999
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer Science+Business Media New York
About this chapter
Cite this chapter
Rülling, W. (2003). Formal Verification. In: Jansen, D. (eds) The Electronic Design Automation Handbook. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-73543-6_14
Download citation
DOI: https://doi.org/10.1007/978-0-387-73543-6_14
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-5369-8
Online ISBN: 978-0-387-73543-6
eBook Packages: Springer Book Archive