Contradictory antecedent debugging in bounded model checking

ABSTRACT

In the context of formal verification Bounded Model Checking (BMC) has shown to be very powerful for large industrial designs. BMC is used to check whether a circuit satisfies a temporal property or not. Typically, such a property is formulated as an implication. In the antecedent of the property the verification engineer specifies the assumptions about the design environment and joins the respective expressions by logical AND. However, the overall conjunction may have no solution, i.e. the antecedent is contradictory. Since in this case a property trivially holds this situation has to be avoided. Furthermore, the root cause of a contradictory antecedent has to be identified which is a manual and very time-consuming process. In this paper we propose a fully automatic approach for presenting all reasons of a contradictory antecedent to the verification engineer, i.e. the approach pinpoints to the sub-expressions in the antecedent that form a contradiction. Hence, our approach reduces the debugging time of a contradictory antecedent significantly.

REFERENCES

• 1: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 2: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 3: Mary Sheeran , Satnam Singh , Gunnar Stålmarck, Checking Safety Properties Using Induction and a SAT-Solver, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.108-125, November 01-03, 2000
• 4: Klaus Winkelmann , Hans-Joachim Trylus , Dominik Stoffel , Görschwin Fey, Cost-Efficient Block Verification for a UMTS Up-Link Chip-Rate Coprocessor, Proceedings of the conference on Design, automation and test in Europe, p.10162, February 16-20, 2004
• 5: D. Große, R. Wille, R. Siegmund, and R. Drechsler. Contradiction analysis for constraint-based random simulation. In Forum on Specification and Design Languages, pages 130--135, 2008.
• 6: Ilan Beer , Shoham Ben-David , Cindy Eisner , Yoav Rodeh, Efficient Detection of Vacuity in ACTL Formulas, Proceedings of the 9th International Conference on Computer Aided Verification, p.279-290, June 22-25, 1997
• 7: Derek L. Beatty , Randal E. Bryant, Formally verifying a microprocessor using a simulation methodology, Proceedings of the 31st annual Design Automation Conference, p.596-602, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196575]
• 8: Ilan Beer , Shoham Ben-David , Cindy Eisner , Yoav Rodeh, Efficient Detection of Vacuity in Temporal Model Checking, Formal Methods in System Design, v.18 n.2, p.141-163, March 1, 2001 [doi>10.1023/A:1008779610539]
• 9: Orna Kupferman , Moshe Y. Vardi, Vacuity Detection in Temporal Model Checking, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.82-96, September 27-29, 1999
• 10: Mitra Purandare , Fabio Somenzi, Vacuum Cleaning CTL Formulae, Proceedings of the 14th International Conference on Computer Aided Verification, p.485-499, July 27-31, 2002
• 11: Hana Chockler , Ofer Strichman, Easier and More Informative Vacuity Checks, Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign, p.189-198, May 30-June 02, 2007 [doi>10.1109/MEMCOD.2007.371225]
• 12: Jocelyn Simmonds , Jessica Davies , Arie Gurfinkel , Marsha Chechik, Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC, Proceedings of the Formal Methods in Computer Aided Design, p.3-12, November 11-14, 2007 [doi>10.1109/FMCAD.2007.20]
• 13: S. Ben-David, D. Fisman, and S. Ruah. Temporal antecedent failure: Refining vacuity. In CONCUR, pages 492--506, 2007.
• 14: R. R. Bakker, F. Dikker, F. Tempelman, and P. M. Wognum. Diagnosing and solving over-determined constraint satisfaction problems. In International Joint Conference on Artificial Intelligence, pages 276--281, 1993.
• 15: Evgueni Goldberg , Yakov Novikov, Verification of Proofs of Unsatisfiability for CNF Formulas, Proceedings of the conference on Design, Automation and Test in Europe, p.10886, March 03-07, 2003
• 16: Lintao Zhang , Sharad Malik, Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications, Proceedings of the conference on Design, Automation and Test in Europe, p.10880, March 03-07, 2003
• 17: Yoonna Oh , Maher N. Mneimneh , Zaher S. Andraus , Karem A. Sakallah , Igor L. Markov, AMUSE: a minimally-unsatisfiable subformula extractor, Proceedings of the 41st annual Design Automation Conference, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996710]
• 18: Jinbo Huang, MUP: a minimal unsatisfiability prover, Proceedings of the 2005 Asia and South Pacific Design Automation Conference, January 18-21, 2005, Shanghai, China [doi>10.1145/1120725.1120907]
• 19: M. N. Mneimneh, I. Lynce, Z. S. Andraus, J. P. Marques-Silva, and K. A. Sakallah. A branch and bound algorithm for extracting smallest minimal unsatisfiable formulas. pages 467--474, 2005.
• 20: M.H. Liffiton and K.A. Sakallah. On finding all minimally unsatisfiable subformulas. In Theory and Applications of Satisfiablity Testing Conference, volume 3569 of LNCS, pages 173--186. Berlin: Springer-Verlag, 2005.
• 21: M.D. Nguyen, M. Thalmaier, M. Wedler, J. Bormann, D. Stoffel, and W. Kunz. Unbounded protocol compliance verification using interval property checking with invariants. IEEE Trans. on CAD, 27(11):2068--2082, Nov 2008.
• 22: Accellera Property Specification Language Reference Manual, version 1.1. http://www.pslsugar.org, 2005.
• 23: Kenneth L. McMillan, Applying SAT Methods in Unbounded Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.250-264, July 27-31, 2002
• 24: David A. Patterson , John Hennessy, Computer Organization and Design, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2004

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)

General Terms:
Verification

Keywords:
bounded model checking, debugging, formal verification, psl