Word level predicate abstraction and refinement for verifying RTL verilog

ABSTRACT

Model checking techniques applied to large industrial circuits suffer from the state space explosion problem. A major technique to address this problem is abstraction. The most commonly used abstraction technique for hardware verification is localization reduction, which removes latches that are not relevant to the property. However, localization reduction fails to reduce the size of the model if the property actually depends on most of the latches. This paper proposes to use predicate abstraction for verifying RTL Verilog, a technique successfully used for software verification. The main challenge when using predicate abstraction is the discovery of suitable predicates. We propose to use weakest preconditions of Verilog statements in order to obtain new predicates during abstraction refinement. This technique has not been applied to circuits before. On benchmarks taken from an industrial microprocessor, we successfully verified safety properties with more than 32,000 latches in the cone of influence. We compare the performance of our technique with a modern model checker that implements localization reduction.

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, B. Cook, S. Das, and S.K. Rajamani. Refining approximations in software predicate abstraction. In TACAS, pages 388--403, 2004.
• 3: T. Ball and S.K. Rajamani. Boolean programs: A model and process for software analysis. Technical Report 2000-14, Microsoft Research, 2000.
• 4: 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
• 5: 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
• 6: 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
• 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 Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM (JACM), v.50 n.5, p.752-794, September 2003 [doi>10.1145/876638.876643]
• 9: 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]
• 10: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 11: 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.
• 12: Edmund Clarke , Daniel Kroening , Natasha Sharygina , Karen Yorav, Predicate Abstraction of ANSI-C Programs Using SAT, Formal Methods in System Design, v.25 n.2-3, p.105-127, September-November 2004 [doi>10.1023/B:FORM.0000040025.89719.f3]
• 13: E. Clarke, M. Talupur, and D. Wang. SAT based predicate abstraction for hardware verification. In SAT, 2003.
• 14: www-cad.eecs.berkeley.edu/~kenmcmil/smv/.
• 15: Satyaki Das , David L. Dill, Successive Approximation of Abstract Transition Relations, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.51, June 16-19, 2001
• 16: 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
• 17: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 18: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 19: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 20: Kedar S. Namjoshi , Robert P. Kurshan, Syntactic Program Transformations for Automatic Abstraction, Proceedings of the 12th International Conference on Computer Aided Verification, p.435-449, July 15-19, 2000
• 21: http://nusmv.irst.itc.it/.
• 22: http://www.cs.sfu.ca/~loryan/personal.
• 23: http://www.sun.com/processors/technologies.html.
• 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: L. Zhang and S. Malik. Extracting small unsatisfiable cores from unsatisfiable boolean formulas. In SAT, 2003.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids

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

General Terms:
Verification

Keywords:
SAT, predicate abstraction, verilog