Formal Verification

  • Wolfgang Rülling


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.


Model Check Output Function State Diagram Equivalence Check Binary Decision Diagram 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [14.1]
    Bryant, R. E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, Vol. C-35, No. 8, 1986Google Scholar
  2. [14.2]
    Eveking, H.: Applied Formal Hardware Verification Methods. Tutorial, DATE’99, 1999Google Scholar
  3. [14.3]
    Gordon, M. J. C.; Melham, T. F.: Introduction to HOL. Cambridge University Press, 1993Google Scholar
  4. [14.4]
    Hsieh, Y.-W.; Levitan, S. P.: Model Abstraction for Formal Verification. DATE’98, 1998Google Scholar
  5. [14.5]
    Meinel, C.; Stangier, C.: Increasing Efficiency of Symbolic Model Checking by Accelerating Dynamic Variable Reordering. DATE’99,1999Google Scholar
  6. [14.6]
    Melham, T. F.: Abstraction Mechanisms for Hardware Verification. Technical Report No. 106, University of Cambridge Computer Laboratory, 1987Google Scholar
  7. [14.7]
    Mohnke, J.: A Signature-Based Approach to Formal Logic Verification. Dissertation, University of Halle, 1999Google Scholar
  8. [14.8]
    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, 1997Google Scholar
  9. [14.9]
    Reetz, R.; Schneider, K.; Kropf, T.: Formal Specification in VHDL for Hardware Verification. DATE’98, 1998Google Scholar
  10. [14.10]
    Thornton, M. A.; Williams, J. P.; Drechsler, R.; Drechsler, N.: Variable Reordering for Shared Binary Decision Diagrams Using Output Probabilities. DATE’99, 1999Google Scholar

Copyright information

© Springer Science+Business Media New York 2003

Authors and Affiliations

  • Wolfgang Rülling

There are no affiliations available

Personalised recommendations