Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs

ABSTRACT

Automated abstraction is the enabling technique for model checking large circuits. Predicate Abstraction is one of the most promising abstraction techniques. It relies on the efficient computation of predicate images and the right choice of predicates. Existing algorithms use a net-list-level circuit model for computing predicate images. 1) This paper describes a proof-based algorithm that computes an over-approximation of the predicate image at the word-level, and thus, scales to larger circuits. 2) The previous work relies on the computation of the weakest preconditions in order to refine the set of predicates. In contrast to that, we propose to extract predicates from a word-level proof to refine the set of predicates.

REFERENCES

• 1: Zaher S. Andraus , Karem A. Sakallah, Automatic abstraction and verification of verilog models, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996629]
• 2: T. Ball and S. Rajamani. Boolean programs: A model and process for software analysis. Technical Report 2000--14, Microsoft Research, 2000.
• 3: Randal E. Bryant , Shuvendu K. Lahiri , Sanjit A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proceedings of the 14th International Conference on Computer Aided Verification, p.78-92, July 27-31, 2002
• 4: 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
• 5: 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
• 6: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143235]
• 7: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 8: E. Clarke, H. Jain, and D. Kroening. Predicate Abstraction and Refinement Techniques for Verifying Verilog. Technical Report CMU-CS-04-139, Carnegie Mellon University, 2004.
• 9: E. Clarke, M. Talupur, and D. Wang. SAT based predicate abstraction for hardware verification. In SAT, 2003.
• 10: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 11: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-244, January 14-16, 2004, Venice, Italy
• 12: Himanshu Jain , Daniel Kroening , Natasha Sharygina , Edmund Clarke, Word level predicate abstraction and refinement for verifying RTL verilog, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065697]
• 13: R. Jhala and K. L. McMillan. Interpolant-based transition relation approximation. In CAV, pages 39--64. Springer, 2005.
• 14: R. Jhala and K. L. McMillan. A practical and complete approach to predicate refinement. In TACAS, volume 3920 of LNCS, pages 459--473. Springer, 2006.
• 15: D. Kroening and N. Sharygina. Approximating predicate images for bit-vector logic. In TACAS, LNCS, pages 242--256. Springer, 2006.
• 16: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 17: K. L. McMillan. An interpolating theorem prover. In Proceedings of TACS, volume 2988, pages 16--30. Springer, 2004.
• 18: Ofer Strichman, On Solving Presburger and Linear Arithmetic with SAT, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.160-170, November 06-08, 2002
• 19: http://www.sun.com/processors/technologies.html.
• 20: 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]