Are BDDs still alive within sequential verification?
Tóm tắt
This work proposes a fully BDD-based approach based on: mixing forward and backward traversals, dovetailing approximate and exact methods, adopting guided and partitioned searches, and using conjunctive decompositions and generalized-cofactor-based BDD simplifications. The method is exact, i.e., it does not produce false negatives or positives, and reaps relevant performance enhancements from an appropriate tradeoff among the component methodologies. The resulting verification strategy is able, on one hand, to improve standard BDD-based algorithms, and, on the other hand, to compete with SAT-based tools on a broader range of circuit sizes. We experimentally compare our approach with three state-of-the-art freely available techniques. The first and second ones are SAT-based strategies, i.e., bounded model checking implemented within the NuSMV and the VIS tools (using Chaff as SAT engine). The third one is a BDD-based methodology, i.e., approximate reachability don’t cares model checking implemented within the VIS tool. Results show interesting improvements in terms of both efficiency and power. They demonstrate how BDDs are able to accomplish larger verification tasks and to efficiently deal with high sequential depths.
Tài liệu tham khảo
Cabodi G (2001) Meta-BDDs: a decomposed representation for layered symbolic manipulation of Boolean functions. In: Berry G, Comon H, Finkel A (eds) Proc. 17th conference international conference on computer-aided verification, Paris, July 2001. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp 118–130
Cabodi G, Camurati P, Quer S (1994) Efficient state space pruning in symbolic backward traversal. In: Proc. international conference on computer design, Cambridge, MA, October 1994, pp 230–235
Cabodi G, Camurati P, Quer S (1999) Improving the efficiency of BDD–based operators by means of partitioning. IEEE Trans Comput-Aided Des 18(5):545–556
Cabodi G, Camurati P, Quer S (2000) Improving symbolic reachability analysis by means of activity profiles. IEEE Trans Comput-Aided Des 19(9):1065–1075
Cabodi G, Camurati P, Quer S (2000) Symbolic forward/backward traversals of large finite state machines. J Syst Architect EUROMICRO J 46(12):1137–1158
Cabodi G, Camurati P, Quer S (2002) Can BDDs compete with SAT solvers on bounded model checking? In: Proc. 39th conference on design automation, New Orleans, June 2002
Cabodi G, Nocco S, Quer S (2002) Mixing forward and backward traversals in guided-prioritized BDD-based verification. In: Brinksma E, Larsen KG (eds) Proc. international conference on computer-aided verification, Copenhagen, Denmark, July 2002. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp 471–484
Cabodi G, Nocco S, Quer S (2005) Improving SAT-based bounded model checking by means of BDD-based approximate traversals. J Universal Comput Sci (in press)
Chauhan P, Clarke E, Kukula J, Sapra S, Veith H, Wang D (2002) Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Aagaard MD, O’Leary JW (eds) Proc. 4th international conference on formal methods in computer-aided design, November 2002. Lecture notes in computer science, vol 2517. Springer, Berlin Heidelberg New York, pp 35–51
Cho H, Hatchel GD, Macii E, Plessier B, Somenzi F (1996) Algorithms for approximate FSM traversal based on state space decomposition. IEEE Trans Comput-Aided Des 15(12):1465–1478
Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NuSMV: a new symbolic model verifier. In: Proc. 13th international conference on computer-aided verification, July 1999. Lecture notes in computer science, vol 1633. Springer, Berlin Heidelberg New York, pp 495–499
Copty F, Fix L, Fraer R, Giunchiglia E, Kamhi G, Tacchella A, Vardi MY (2001) Benefits of bounded model checking at an industrial setting. In: Berry G, Comon H, Finkel A (eds) Proc. 17th international conference on computer-aided verification, Paris, July 2001. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp 435–453
Brayton RK, Hachtel GD, Sangiovanni-Vincentelli A, Somenzi F, Aziz A, Cheng S-T, Edwards SA, Khatri SP, Kuykimoto Y, Pardo A, Qadeer Q, Ranjan RK, Sarwary A, Shiple TR, Swamy G, Villa T (1996) VIS. In: Srivas M, Camilleri A (eds) Proc. international conference on formal methods in computer-aided design, Palo Alto, CA, November 1996. Lecture notes in computer science, vol 1166. Springer, Berlin Heidelberg New York, pp 248–256
Fraer R, Kamhi G, Ziv B, Vardi MY, Fix L (2000) Prioritized traversal: efficient reachability analysis for verification and falsification. In: Emerson EA, Prasad Sistla A (eds) Proc. 12th international conference on computer-aided verification, Chicago, July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 389–402
Ganai MK, Aziz A, Kuehlmann A (1999) Enhancing simulation with BDDs and ATPG. In: Proc. 36th conference on design automation, New Orleans, November 1999, pp 385–390
Goldberg E, Novikov Y (2002) BerkMin: a fast and robust SAT-solver. In: Proc. Design, Automation and Test in Europe, Paris, February 2002, pp 142–149
Govindaraju SG, Dill DL (1998) Verification by approximate forward and backward reachability. In: Proc. international conference on computer-aided design, San Jose, CA, November 1998, pp 366–370
IBM Formal Verification Benchmark Library. http://www.haifa.il.ibm.com/projects/verification/rb_homepage/fvbenchmarks.html
Moon I, Jang J, Hachtel GD, Somenzi F, Yuan J, Pixley C (1998) Approximate reachability don’t cares for CTL model checking. In: Proc. international conference on computer-aided design, San Jose, CA, November 1998, pp 351–358
Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proc. 38th conference on design automation, Las Vegas, June 2001
Narayan A, Isles AJ, Jain J, Brayton RK, Sangiovanni-Vincentelli A (1997) Reachability analysis using partitioned–ROBDDs. In: Proc. international conference on computer-aided design, San Jose, CA, November 1997, pp 388–393
Ravi K, Somenzi F (1995) High-density reachability analysis. In: Proc. international conference on computer-aided design, San Jose, CA, November, pp 154–158
Ravi K, Somenzi F (1999) Hints to accelerate symbolic traversal. In: conference on correct hardware design and verification methods (CHARME’99), Berlin, September 1999. Lecture notes in computer science, vol 1703. Springer, Berlin Heidelberg New York, pp 250–264
Ryan L (2003) Siege SAT Solver. http://www.cs.sfu.ca/∼loryan/personal/
Wang D, Ho P, Long J, Kukula J, Zhu Y, Ma T, Damiano R (2001) Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In: Proc. 38th conference on design automation, Las Vegas, June 2001