Counterexample-guided abstraction refinement for symbolic model checking

ABSTRACT

The state explosion problem remains a major hurdle in applying symbolic model checking to large hardware designs. State space abstraction, having been essential for verifying designs of industrial complexity, is typically a manual process, requiring considerable creativity and insight.In this article, we present an automatic iterative abstraction-refinement methodology that extends symbolic model checking. In our method, the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or "spurious") counterexamples. We devise new symbolic techniques that analyze such counterexamples and refine the abstract model correspondingly. We describe aSMV, a prototype implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach.

REFERENCES

• 1: Parosh Aziz Abdulla , Aurore Annichini , Saddek Bensalem , Ahmed Bouajjani , Peter Habermehl , Yassine Lakhnech, Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis, Proceedings of the 11th International Conference on Computer Aided Verification, p.146-159, July 06-10, 1999
• 2: Felice Balarin , Alberto L. Sangiovanni-Vincentelli, An Iterative Approach to Language Containment, Proceedings of the 5th International Conference on Computer Aided Verification, p.29-40, June 28-July 01, 1993
• 3: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 4: Mihir Bellare , Oded Goldreich , Madhu Sudan, Free Bits, PCPs, and Nonapproximability---Towards Tight Results, SIAM Journal on Computing, v.27 n.3, p.804-915, June 1998 [doi>10.1137/S0097539796302531]
• 5: Saddek Bensalem , Ahmed Bouajjani , Claire Loiseaux , Joseph Sifakis, Property Preserving Simulations, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.260-273, June 29-July 01, 1992
• 6: Saddek Bensalem , Yassine Lakhnech , Sam Owre, Computing Abstractions of Infinite State Systems Compositionally and Automatically, Proceedings of the 10th International Conference on Computer Aided Verification, p.319-331, June 28-July 02, 1998
• 7: Sergey Berezin , Armin Biere , Edmund M. Clarke , Yunshan Zhu, Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.369-386, November 04-06, 1998
• 8: A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309942]
• 9: Nikolaj Bjørner , Anca Browne , Zohar Manna, Automatic generation of invariants and intermediate assertions, Theoretical Computer Science, v.173 n.1, p.49-87, Feb. 1997 [doi>10.1016/S0304-3975(96)00191-0]
• 10: Glenn Bruns , Patrice Godefroid, Model Checking Partial State Spaces with 3-Valued Temporal Logics, Proceedings of the 11th International Conference on Computer Aided Verification, p.274-287, July 06-10, 1999
• 11: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 12: Randal E. Bryant, On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication, IEEE Transactions on Computers, v.40 n.2, p.205-213, February 1991 [doi>10.1109/12.73590]
• 13: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 14: Burch, J. R., Clarke, E. M., and Long, D. E. 1991. Symbolic model checking with partitioned transition relations. In Proceedings of the 1991 International Conference on Very Large Scale Integration, A. Halaas and P. B. Denyer, Eds. Winner of the Sidney Michaelson Best Paper Award.
• 15: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 16: Cimatti, A., Clarke, E., Giunchiglia, F., and Roveri, M. 1998. NuSMV: A new symbolic model checker. In Software Tools for Technology Transfer.
• 17: E. M. Clarke , R. Enders , T. Filkorn , S. Jha, Exploiting symmetry in temporal logic model checking, Formal Methods in System Design, v.9 n.1-2, p.77-104, Aug. 1996 [doi>10.1007/BF00625969]
• 18: Edmund M. Clarke , Somesh Jha , Yuan Lu , Dong Wang, Abstract BDDs: A Technque for Using Abstraction in Model Checking, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.172-186, September 27-29, 1999
• 19: Clarke, E., Lu, Y., Jha, S., and Veith, H. 2001. Counterexamples in model checking. Tech. Rep., Carngie Mellon University. CMU-CS-01-106.
• 20: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 21: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.117-126, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567080]
• 22: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 23: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 24: Michael Colón , Tomás E. Uribe, Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures, Proceedings of the 10th International Conference on Computer Aided Verification, p.293-304, June 28-July 02, 1998
• 25: O. Coudert , C. Berthet , J. C. Madre, Verification of synchronous sequential machines based on symbolic execution, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.365-373, February 1990, Grenoble, France
• 26: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 27: Patrick Cousot , Radhia Cousot, Refining Model Checking by Abstract Interpretation, Automated Software Engineering, v.6 n.1, p.69-95, January 1999 [doi>10.1023/A:1008649901864]
• 28: Dennis Dams , Rob Gerth , Orna Grumberg, Abstract interpretation of reactive systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.253-291, March 1997 [doi>10.1145/244795.244800]
• 29: Dennis Dams , Orna Grumberg , Rob Gerth, Generation of Reduced Models for Checking Fragments of CTL, Proceedings of the 5th International Conference on Computer Aided Verification, p.479-490, June 28-July 01, 1993
• 30: Dams, D. R., Grumberg, O., and Gerth, R. 1997b. Abstract interpretation of reactive systems: Abstractions preserving ∀CTL*, &exists;CTL*, CTL*. In Proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET 94).
• 31: 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
• 32: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• 33: Jürgen Dingel , Thomas Filkorn, Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving, Proceedings of the 7th International Conference on Computer Aided Verification, p.54-69, July 03-05, 1995
• 34: Matthew B. Dwyer , John Hatcliff , Roby Joehanes , Shawn Laubach , Corina S. Păsăreanu , Hongjun Zheng , Willem Visser, Tool-supported program abstraction for finite-state verification, Proceedings of the 23rd International Conference on Software Engineering, p.177-187, May 12-19, 2001, Toronto, Ontario, Canada
• 35: E. Allen Emerson , A. Prasad Sistla, Symmetry and model checking, Formal Methods in System Design, v.9 n.1-2, p.105-131, Aug. 1996 [doi>10.1007/BF00625970]
• 36: E. Allen Emerson , Richard J. Trefler, From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.142-156, September 27-29, 1999
• 37: Uriel Feige , Joe Kilian, Zero Knowledge and the Chromatic Number, Proceedings of the 11th Annual IEEE Conference on Computational Complexity, p.278, May 24-27, 1996
• 38: Joan Feigenbaum , Sampath Kannan , Moshe Y. Vardi , Mahesh Viswanathan, Complexity of Problems on Graphs Represented as OBDDs (Extended Abstract), Proceedings of the 15th Annual Symposium on Theoretical Aspects of Computer Science, p.216-226, February 25-27, 1998
• 39: Fujitsu. 1996. Fujitsu aims media processor at DVD. MicroProcessor Rep. 11--13.
• 40: David A. Fura , Phillip J. Windley , Arun K. Somani, Abstraction Techniques for Modeling Real-World Interface Chips, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.267-280, August 11-13, 1993
• 41: Michael R. Garey , David S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman & Co., New York, NY, 1979
• 42: Patrice Godefroid , Doron Peled , Mark Staskauskas, Using partial-order methods in the formal validation of industrial concurrent programs, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.261-269, January 08-10, 1996, San Diego, California, United States
• 43: Gottlob, G., Leone, N., and Veith, H. 1999. Succinctness as a source of complexity in logical formalisms. Ann. Pure Appl. Logic 97, 1--3, 231--260.
• 44: Shankar G. Govindaraju , David L. Dill, Verification by approximate forward and backward reachability, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.366-370, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289055]
• 45: Shankar G. Govindaraju , David L. Dill, Counterexample-guided choice of projections in approximate symbolic model checking, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
• 46: Susanne Graf, Verification of a Distributed Cache Memory by Using Abstractions, Proceedings of the 6th International Conference on Computer Aided Verification, p.207-219, June 21-23, 1994
• 47: 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
• 48: Pei-Hsin Ho , Adrian J. Isles , Timothy Kam, Formal verification of pipeline control using controlled token nets and abstract interpretation, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.529-536, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289082]
• 49: Ramin Hojati , Robert K. Brayton, Automatic Datapath Abstraction In Hardware Systems, Proceedings of the 7th International Conference on Computer Aided Verification, p.98-113, July 03-05, 1995
• 50: C. Norris Ip , David L. Dill, Better verification through symmetry, Formal Methods in System Design, v.9 n.1-2, p.41-75, Aug. 1996 [doi>10.1007/BF00625968]
• 51: Kurt Jensen, Condensed state spaces for symmetrical coloured Petri nets, Formal Methods in System Design, v.9 n.1-2, p.7-40, Aug. 1996 [doi>10.1007/BF00625967]
• 52: Robert B. Jones , Jens U. Skakkebæk , David L. Dill, Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.2-17, November 04-06, 1998
• 53: Karp, R. 1972. Reducibility among combinatorial problems. In Complexity of Computer Computations, R. Miller and J. Thatcher, Eds. 85--103.
• 54: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 55: Woohyuk Lee , Abelardo Pardo , Jae-Young Jang , Gary Hachtel , Fabio Somenzi, Tearing based automatic abstraction for CTL model checking, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.76-81, November 10-14, 1996, San Jose, California, United States
• 56: Lesens, D., and Saïdi, H. 1997. Automatic verification of parameterized networks of processes by abstraction. In Proceedings of the International Workshop on Verification of Infinite State Systems (INFINITY). Bologna.
• 57: Jørn Lind-Nielsen , Henrik Reif Andersen, Stepwise CTL Model Checking of State/Event Systems, Proceedings of the 11th International Conference on Computer Aided Verification, p.316-327, July 06-10, 1999
• 58: C. Loiseaux , S. Graf , J. Sifakis , A. Bouajjani , S. Bensalem, Property preserving abstractions for the verification of concurrent systems, Formal Methods in System Design, v.6 n.1, p.11-44, Jan. 1995 [doi>10.1007/BF01384313]
• 59: David Esley Long, Model checking, abstraction, and compositional verification, Carnegie Mellon University, Pittsburgh, PA, 1993
• 60: Zohar Manna , Michael Colón , Bernd Finkbeiner , Henny Sipma , Tomás E. Uribe, Abstraction and Modular Verification of Infinite-State Reactive Systems, Proceedings of the International Workshop on Requirements Targeting Software and Systems Engineering, p.273-292, October 12-14, 1997
• 61: Kenneth L. McMillan, A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.13-25, August 03, 1996
• 62: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 63: Kenneth L. McMillan, Verification of Infinite State Systems by Compositional Model Checking, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.219-234, September 27-29, 1999
• 64: Kenneth L. McMillan, Verification of Infinite State Systems by Compositional Model Checking, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.219-234, September 27-29, 1999
• 65: Pardo, A. 1997. Automatic abstraction techniques for formal verification of digital systems. Ph.D. dissertation, Dept. of Computer Science, University of Colorado at Boulder, Boulder Colo.
• 66: Abelardo Pardo , Gary D. Hachtel, Incremental CTL model checking using BDD subsetting, Proceedings of the 35th annual conference on Design automation, p.457-462, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277171]
• 67: Doron Peled, All from One, One for All: on Model Checking Using Representatives, Proceedings of the 5th International Conference on Computer Aided Verification, p.409-423, June 28-July 01, 1993
• 68: Carl Pixley, Introduction to a Computational Theory and Implementation of Sequential Hardware Equivalence, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.54-64, June 18-21, 1990
• 69: Carl Pixley , Gary Beihl , Ernesto Pacas-Skewes, Automatic Derivation of FSM Specification to Implementation Encoding, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.245-249, October 14-16, 1991
• 70: C. Pixley , S.-W. Jeong , G. D. Hachtel, Exact calculation of synchronization sequences based on binary decision diagrams, Proceedings of the 29th ACM/IEEE conference on Design automation, p.620-623, June 08-12, 1992, Anaheim, California, United States
• 71: John M. Rushby, Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.1-11, September 21-24, 1999
• 72: Vlad Rusu , Eli Singerman, On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.178-192, March 22-28, 1999
• 73: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
• 74: Hassen Saïdi , Natarajan Shankar, Abstract and Model Check While You Prove, Proceedings of the 11th International Conference on Computer Aided Verification, p.443-454, July 06-10, 1999
• 75: Joseph Sifakis, Property Preserving Homomorphisms of Transition Systems, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.458-473, June 06-08, 1983
• 76: Somenzi, F. 2001. CUDD: CU decision diagram package. http://vlsi.colorado.edu/fabio/.
• 77: An Approach to Verify a Large Scale System-on-a-chip Using Symbolic Model Checking, Proceedings of the International Conference on Computer Design, p.308, October 05-05, 1998
• 78: Filip Van Aelten , Stan Y. Liao , Jonathan Allen , Srinivas Devadas, Automatic generation and verification of sufficient correctness properties for synchronous processors, Proceedings of the 1992 IEEE/ACM international conference on Computer-aided design, p.183-187, November 1992, Santa Clara, California, United States
• 79: Helmut Veith, Languages represented by Boolean formulas, Information Processing Letters, v.63 n.5, p.251-256, Sept. 15, 1997 [doi>10.1016/S0020-0190(97)00134-8]
• 80: H. Veith, How to Encode a Logical Structure by an OBDD, Proceedings of the Thirteenth Annual IEEE Conference on Computational Complexity, p.122, June 15-18, 1998
• 81: Helmut Veith, Succinct representation, leaf languages, and projection reductions, Information and Computation, v.142 n.2, p.207-236, May 2, 1998 [doi>10.1006/inco.1997.2696]
• 82: P. Wolper , V. Lovinfosse, Verifying properties of large sets of processes with network invariants, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.68-80, February 1990, Grenoble, France
• 83: Bwolen Yang , Randal E. Bryant , David R. O'Hallaron , Armin Biere , Olivier Coudert , Geert Janssen , Rajeev K. Ranjan , Fabio Somenzi, A Performance Study of BDD-Based Model Checking, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.255-289, November 04-06, 1998

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

General Terms:
Verification

Keywords:
Abstraction, hardware verification, symbolic model checking, temporal logic