Dynamic abstraction using SAT-based BMC

ABSTRACT

We propose a new dynamic method of abstraction, which can be applied during successive steps of the model checking algorithm to further reduce the model produced by traditional static abstraction methods. This is facilitated by information gathered from an analysis of the proof of unsatisfiability of SAT-based bounded model checking problems formulated on the original design. The dynamic abstraction effectively allows the model checker to work with smaller abstract models. Experiments on several industrial benchmarks demonstrate that dynamic abstraction can significantly improve both the performance and the capacity of typical abstraction refinement flows.

REFERENCES

• 1: Per Bjesse , James Kukula, Using Counter Example Guided Abstraction Refinement to Find Complex Bugs, Proceedings of the conference on Design, automation and test in Europe, p.10156, February 16-20, 2004
• 2: Chao Wang , Bing Li , HoonSang Jin , Gary D. Hachtel , Fabio Somenzi, Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.408, November 09-13, 2003 [doi>10.1109/ICCAD.2003.83]
• 3: Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001 [doi>10.1023/A:1011276507260]
• 4: Edmund M. Clarke , Anubhav Gupta , James H. Kukula , Ofer Shrichman, SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques, Proceedings of the 14th International Conference on Computer Aided Verification, p.265-279, July 27-31, 2002
• 5: Dong Wang , Pei-Hsin Jiang , James Kukula , Yunshan Zhu , Tony Ma , Robert Damiano, Formal property verification by abstraction refinement with formal, simulation and hybrid engines, Proceedings of the 38th conference on Design automation, p.35-40, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378260]
• 6: Aarti Gupta , Malay Ganai , Zijiang Yang , Pranav Ashar, Iterative Abstraction using SAT-based BMC with Proof Analysis, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.416, November 09-13, 2003 [doi>10.1109/ICCAD.2003.87]
• 7: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 8: Bing Li , F. Somenzi, Efficient computation of small abstraction refinements, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.518-525, November 07-11, 2004 [doi>10.1109/ICCAD.2004.1382632]
• 9: M. Glusman et al. Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation. In Tools and Algorithms for the Construction and Analysis of Systems, pages 176--191, April 2003.
• 10: Freddy Y.C. Mang , Pei-Hsin Ho, Abstraction refinement by controllability and cooperativeness analysis, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996630]
• 11: K. L. McMillan and N. Amla. Automatic abstraction without counterexamples. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2619, pages 2--17, April 2003.
• 12: Pankaj Chauhan , Edmund M. Clarke , James H. Kukula , Samir Sapra , Helmut Veith , Dong Wang, Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.33-51, November 06-08, 2002
• 13: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 14: http://ee.princeton.edu/~chaff/zchaff.php, Dec. 2003.
• 15: 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

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.2 Reliability and Testing**

General Terms:
Design, Verification

Keywords:
SAT, abstraction refinement, model checking