Refinement strategies for verification methods based on datapath abstraction

ABSTRACT

In this paper we explore the application of Counter example-Guided Abstraction Refinement (CEGAR) in the context of microprocessor correspondence checking. The approach utilizes automatic datapath abstraction, augmented with automatic refinement based on 1) localization, 2) generalization, and 3) minimal unsatisfiable subset (MUS) extraction. We introduce several refinement strategies and empirically evaluate their effectiveness on a set of microprocessor benchmarks. The data suggest that localization, generalization, and MUS extraction from both the abstract and concrete models are essential for effective verification. Additionally, refinement tends to converge faster when multiple MUses are extracted in each iteration.

REFERENCES

• 1: W. Ackerman, "Solvable Cases of the Decision Problem." North-Holland, Amsterdam, 1954.
• 2: 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]
• 3: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, Validity Checking for Combinations of Theories with Equality, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.187-201, November 06-08, 1996
• 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: 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
• 6: 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
• 7: Randal E. Bryant , Steven German , Miroslav N. Velev, Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.93-134, Jan. 2001 [doi>10.1145/371282.371364]
• 8: 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
• 9: 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
• 10: N. Een and A. Biere, "Improved Subsumption Techniques for Variables Elimination in SAT," SAT 2005.
• 11: 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
• 12: 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]
• 13: David A. Patterson , John L. Hennessy, Computer architecture: a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1990
• 14: H. Jain, D. Kroening and E. Clarke, "Predicate Abstraction and Verification of Verilog," Technical Report CMUCS-04-139.
• 15: Matt Kaufmann , J. S. Moore, An Industrial Strength Theorem Prover for a Logic Based on Common Lisp, IEEE Transactions on Software Engineering, v.23 n.4, p.203-213, April 1997 [doi>10.1109/32.588534 ]
• 16: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 17: Edmund Clarke , Daniel Kroening , Karen Yorav, Behavioral consistency of C and verilog programs using bounded model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775928]
• 18: Shuvendu K. Lahiri , Sanjit A. Seshia , Randal E. Bryant, Modeling and Verification of Out-of-Order Microprocessors in UCLID, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.142-159, November 06-08, 2002
• 19: M. H. Liffiton, M. D. Moffitt, M. E. Pollack, and K. A. Sakallah, "Identifying Conflicts in Overconstrained Temporal Problems," in Proc. 19th International Joint Conference on Artificial Intelligence (IJCAI-05), pp. 205--211, Edinburgh, Scotland, 2005.
• 20: K. L. McMillan and N. Amla, "Automatic Abstraction without Counterexamples." In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'03), pp. 2--17, Warsaw, Poland, April, 2003, LNCS 2619.
• 21: S. A. Seshia, S. K. Lahiri, R. E. Bryant, "A User's Guide to UCLID version 0.1".
• 22: Donald E. Thomas , Philip R. Moorby, The VERILOG Hardware Description Language, Kluwer Academic Publishers, Norwell, MA, 1991
• 23: L. Zhang and S. Malik, "Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formulas." In SAT, Springer-Verlag, 2003.
• 24: www-2.cs.cmu.edu/~uclid
• 25: vlsi.colorado.edu/~vis

INDEX TERMS

Primary Classification:
  B. Hardware
  B.8 Performance and Reliability
      B.8.1 Reliability, Testing, and Fault-Tolerance

Additional Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.1 Design
          Subjects: Data-path design
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
          Subjects: Microprocessors and microcomputers
  B.8 Performance and Reliability
      B.8.2 Performance Analysis and Design Aids

General Terms:
Design, Performance, Verification