Guiding simulation with increasingly refined abstract traces

ABSTRACT

We combine abstraction refinement and simulation to provide a more efficient approach to checking invariant properties whose only counterexamples are very long traces. We allow each transition of an abstract error trace to map to multiple transitions of the concrete error trace and simulate pseudorandom vectors to build segments of the concrete trace. This approach addresses the capacity limitation of the formal verification engine as well as the short-sightedness of the simulator, thus providing a more effective technique for deep, subtle bugs.

REFERENCES

• 1: Jules P. Bergmann , Mark A. Horowitz, Improving coverage analysis and test generation for large designs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.580-583, November 07-11, 1999, San Jose, California, United States
• 2: 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
• 3: 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
• 4: Gianpiero Cabodi , Sergio Nocco , Stefano Quer, Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals, Proceedings of the conference on Design, Automation and Test in Europe, p.10898, March 03-07, 2003
• 5: 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
• 6: Y. Choueka. Theories of automata on Ω-tapes: A simplified approach. J. Comput. Syst. Sci., 8:117--141, 1974.
• 7: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 8: 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
• 9: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 10: Daniel Geist , Monica Farkas , Avner Landver , Yossi Lichtenstein , Shmuel Ur , Yaron Wolfsthal, Coverage-Directed Test Generation Using Symbolic Techniques, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.143-158, November 06-08, 1996
• 11: Aarti Gupta , Malay Ganai , Chao Wang , Zijiang Yang , Pranav Ashar, Learning from BDDs in SAT-based bounded model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.776040]
• 12: Scott Hazelhurst , Osnat Weissberg , Gila Kamhi , Limor Fix, A hybrid verification approach: getting deep into the design, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.513948]
• 13: Pei Hsin Ho , Thomas Shiple , Kevin Harer , James Kukula , Robert Damiano , Valeria Bertacco , Jerry Taylor , Jiang Long, Smart simulation using collaborative formal and simulation engines, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
• 14: URL: http://www.cad.polito.it/tools/itc99.html.
• 15: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 16: B. Li, C. Wang, and F. Somenzi. A satisfiability-based approach to abstraction refinement in model checking. ENTCS, 89(4), BMC 2003.
• 17: K. L. McMillan and N. Amla. Automatic abstraction without counterexamples. In TACAS, pages 2--17, Apr. 2003.
• 18: S. Shyam and V. Bertacco. Guido: Hybrid verification by distance-guided simulation. IWLS 2005.
• 19: Serdar Tasiran , Yuan Yu , Brannon Batson, Using a formal specification and a model checker to monitor and direct simulation, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775926]
• 20: URL: http://vlsi.colorado.edu/~vis.
• 21: Chao Wang , Roderick Bloem , Gary D. Hachtel , Kavita Ravi , Fabio Somenzi, Divide and Compose: SCC Refinement for Language Emptiness, Proceedings of the 12th International Conference on Concurrency Theory, p.456-471, August 20-25, 2001
• 22: Chao Wang , Gary D. Hachtel , Fabio Somenzi, Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking, Proceedings of the IEEE International Conference on Computer Design (ICCD'04), p.112-118, October 11-13, 2004
• 23: 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]
• 24: 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]
• 25: C. Han Yang , David L. Dill, Validation with guided search of the state space, Proceedings of the 35th annual conference on Design automation, p.599-604, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277201]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Algorithms, Verification

Keywords:
abstraction refinement, model checking, simulation