Efficient Debugging in a Formal Verification Environment

  • Fady Copty
  • Amitai Irron
  • Osnat Weissberg
  • Nathan Kropp
  • Gila Kamhi 
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


In this paper, we emphasize the importance of efficient debugging in formal verification and present capabilities that we have developed in order to augment debugging in Intel’s Formal Verification Environment. We have given the name the “counter-example wizard” to the bundle of capabilities that we have developed to address the needs of the verification engineer in context of counter-example diagnosis and rectification. The novel features of the counterexample wizard are the “multi-value counter-example annotation,” “multiple root cause detection,” and “constraint-based debugging” mechanisms. Our experience with the verification of real-life Intel designs shows that these capabilities complement one another and can considerably help the verification engineer diagnose and fix a reported failure. We use real-life verification cases to illustrate how our system solution can significantly reduce the time spent in the loop of model checking, specification and design modification.


Model Check Formal Verification Multiple Root Symbolic Model Check Sequential Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [1]
    R. Bryant, “Graph-based Algorithms for Boolean Function Manipulations”,, IEEE Transactions on Computers, C-35:677–691, August 1986.Google Scholar
  2. [2]
    K.L. McMillan. “Symbolic Model Checking”, Kluwer Academics, 1993.Google Scholar
  3. [3]
    K. Ravi, F. Somenzi, “Efficient Fixpoint Computation for Invariant Checking”, In Proceedings of ICCD’9, pp. 467–474.Google Scholar
  4. [4]
    R. Fraer, G. Kamhi, L. Fix, M. Vardi. “Evaluating Semi-Exhaustive Verification Techniques for Bug-Hunting” in Proceedings of SMC’99.Google Scholar
  5. [5]
    R. Fraer, G. Kamhi, B. Ziv, M. Vardi, L. Fix. “Prioritized Traversal: Efficient Reachability Computation for Verification and Falsification”, in Proceedings of CAV’00,Chicago,IL.Google Scholar
  6. [6]
    I. Beer, S. Ben-Davis, A. Landver. “On-the-Fly Model Checking” of RCTL Formulas”, in Proceedings of CAV’98.Google Scholar
  7. [7]
    R.H. Hardin, R. P. Kurshan, K.L. McMillan, J.A. Reeds and N.J.A. Sloane, “Efficient Regression Verification”, Int’l Workshop on Discrete Event Systems (WODES’ 96)Google Scholar
  8. [8]
    E. Clarke, O. Grumberg, K. McMillan, X. Zhao, ‘‘Efficient generation of counterexamples and witnesses in symbolic model checking”, in the proceeding of DAC’95.Google Scholar
  9. [9]
    B. Kurshan, “Formal Verification in a Commercial Setting”, In Proceedings of DAC’97.Google Scholar
  10. [10]
    J. Jang, S. Quader, M. Kaufmann, C. Pixley,“Formal Verification of FIRE: A Case Study”, in Proceedings of Design Automation Conference, 1997, Anaheim, CAGoogle Scholar
  11. [11]
    R.K. Brayton, G.D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R.K. Ranjan, S. Sarwary, T.R. Shiple, G. Swamy, T. Villa, “VIS: A system for Verification and Synthesis”, in Proc. of DAC’94.Google Scholar
  12. [12]
    I. Beer, S. Ben-David, C. Eisner, A. Landver. “RuleBase: An industry-oriented formal verification tool”. In Proc. of Design Automation Conference 1996 (DAC’96)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Fady Copty
    • 1
  • Amitai Irron
    • 1
  • Osnat Weissberg
    • 1
  • Nathan Kropp
    • 1
    • 2
  • Gila Kamhi 
    • 1
  1. 1.Logic and Validation TechnologyIntel CorporationHaifaIsrael
  2. 2.Microprocessor GroupIntel CorporationUSA

Personalised recommendations