Formal verification at higher levels of abstraction

ABSTRACT

Most formal verification tools on the market convert a high-level register transfer level (RTL) design into a bit-level model. Algorithms that operate at the bit-level are unable to exploit the structure provided by the higher abstraction levels, and thus, are less scalable.

This tutorial surveys recent advances in formal verification using high-level models. We present word-level verification with predicate abstraction and satisfiability modulo theories (SMT) solvers. We then describe techniques for term-level modeling and ways to combine word-level and term-level approaches for scalable verification.

REFERENCES

• 1: Zaher S. Andraus , Mark H. Liffiton , Karem A. Sakallah, Refinement strategies for verification methods based on datapath abstraction, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan [doi>10.1145/1118299.1118306]
• 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: D. Babić and M. Musuvathi. Modular Arithmetic Decision Procedure. Technical report, Microsoft Research, Redmond, 2005.
• 4: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 5: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, A decision procedure for bit-vector arithmetic, Proceedings of the 35th annual conference on Design automation, p.522-527, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277186]
• 6: S. Berezin, V. Ganesh, and D. Dill. A decision procedure for fixed-width bit-vectors. Technical report, Computer Science Department, Stanford University, April 2005.
• 7: 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
• 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: Raik Brinkmann , Rolf Drechsler, RTL-Datapath Verification using Integer Linear Programming, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.741, January 07-11, 2002
• 10: R. Bruttomesso, A. Cimatti, A. Franzen, A. Griggio, Z. Hanna, A. Nadel, A. Palti, and R. Sebastiani. A lazy and layered SMT(BV) solver for hard industrial verification problems. In Computer Aided Verification (CAV), LNCS. Springer, 2007.
• 11: R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady. Deciding bit-vector arithmetic with abstraction. In O. Grumberg and M. Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4424 of LNCS, pages 358--372. Springer, 2007.
• 12: 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
• 13: Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , Dawson R. Engler, EXE: automatically generating inputs of death, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180405.1180445]
• 14: 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
• 15: 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]
• 16: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 17: 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]
• 18: E. Clarke, M. Talupur, and D. Wang. SAT based predicate abstraction for hardware verification. In SAT, 2003.
• 19: 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
• 20: E. M. Clarke and H. Veith. Counterexamples revisited: Principles, algorithms, applications. In Verification: Theory and Practice, pages 208--224. Springer, 2003.
• 21: B. Cook, D. Kroening, and N. Sharygina. Cogent: Accurate theorem proving for program verification. In Proceedings of CAV 2005, pages 296--300. Springer, 2005.
• 22: Cadence SMV, http://www.kenmcmil.com/smv.html.
• 23: David Cyrluk , M. Oliver Möller , Harald Rueß, An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors, Proceedings of the 9th International Conference on Computer Aided Verification, p.60-71, June 22-25, 1997
• 24: B. Dutertre and L. de Moura. The Yices SMT solver. Available at http://yices.csl.sri.com/tool-paper.pdf, September 2006.
• 25: V. Ganesh and D. Dill. A decision procedure for bit-vectors and arrays. In Computer Aided Verification (CAV), LNCS. Springer, 2007.
• 26: 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
• 27: Chung-Yang Huang , Kwang-Ting Cheng, Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques, Proceedings of the 37th conference on Design automation, p.118-123, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337333]
• 28: 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]
• 29: Daniel Kroening , Ofer Strichman, Efficient Computation of Recurrence Diameters, Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, p.298-309, January 09-11, 2002
• 30: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 31: 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
• 32: Panagiotis Manolios , Sudarshan K. Srinivasan , Daron Vroon, Automatic memory reductions for RTL model verification, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California [doi>10.1145/1233501.1233663]
• 33: K. L. McMillan. An interpolating theorem prover. In TACAS, pages 16--30. Springer, 2004.
• 34: MiniSat. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/.
• 35: G. Parthasarathy , M. K. Iyer , K.-T. Cheng , L.-C. Wang, An efficient finite-domain constraint solver for circuits, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996628]
• 36: Markus Wedler , Dominik Stoffel , Wolfgang Kunz, Normalization at the arithmetic bit level, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065699]