Efficient reachability checking using sequential SAT

ABSTRACT

Reachability checking and Pre-image computation are fundamental problems in ATPG and formal verification. Traditional sequential search techniques based on ATPG/SAT, or on OBDDS have diverging strengths and weaknesses. In this paper, we describe how structural analysis and conflict-based learning are combined in order to improve the efficiency of sequential search. We use conflict-based learning and illegal state learning across time-frames. We also address issues in efficiently bounding the search space in a single time-frame and across time-frames. We analyze each of these techniques experimentally and demonstrate the advantages of each technique. We compare performance against a commercial sequential ATPG engine and VIS [13] on a set of standard benchmarks.

REFERENCES

• 1: Amit Narayan , Adrian J. Isles , Jawahar Jain , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Reachability analysis using partitioned-ROBDDs, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.388-393, November 09-13, 1997, San Jose, California, United States
• 2: Armin Biere , Wolfgang Kunz, SAT and ATPG: Boolean engines for formal hardware verification, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.782-785, November 10-14, 2002, San Jose, California [doi>10.1145/774572.774687]
• 3: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 4: FUJIWARA, H. FAN: a Fanout-oriented Test Pattern Generation Algorithm. In Proc. of ISCAS (June 1985), pp. 671--674.
• 5: Aarti Gupta , Zijiang Yang , Pranav Ashar , Lintao Zhang , Sharad Malik, Partition-based decision heuristics for image computation using SAT and BDDs, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 6: John Giraldi , Michael L. Bushnell, Search State Equivalence for Redundancy Identification and Test Generation, Proceedings of the IEEE International Test Conference on Test: Faster, Better, Sooner, p.184-193, October 26-30, 1991
• 7: Kwang-Ting Cheng , Angela Krstic, Current Directions in Automatic Test-Pattern Generation, Computer, v.32 n.11, p.58-64, November 1999 [doi>10.1109/2.803642]
• 8: Hyeong-Ju Kang , In-Cheol Park, SAT-based unbounded symbolic model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.776043]
• 9: 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]
• 10: MARCHOK, T., EL-MALEH, A., MALY, W., AND RAJSKI, J. A Complexity Analysis of Sequential ATPG. IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems. 15 n 11 (Nov. 1996), 1409--1423.
• 11: Kenneth L. McMillan, Applying SAT Methods in Unbounded Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.250-264, July 27-31, 2002
• 12: M. K. Iyer , G. Parthasarathy , K.-T. Cheng, SATORI - A Fast Sequential SAT Engine for Circuits, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.320, November 09-13, 2003 [doi>10.1109/ICCAD.2003.122]
• 13: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 14: RUDELL, R., AND SANGIOVANNI-VINCENTELLI, A. Exact Minimization of Multiple-valued Functions for PLA optimization. In Proc. of the IEEE/ACM ICCAD (Nov. 1986), pp. 354--360.
• 15: Shuo Sheng , Michael Hsiao, Efficient Preimage Computation Using A Novel Success-Driven ATPG, Proceedings of the conference on Design, Automation and Test in Europe, p.10822, March 03-07, 2003
• 16: Poul Frederick Williams , Armin Biere , Edmund M. Clarke , Anubhav Gupta, Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking, Proceedings of the 12th International Conference on Computer Aided Verification, p.124-138, July 15-19, 2000
• 17: Lintao Zhang , Sharad Malik, Conflict driven learning in a quantified Boolean Satisfiability solver, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.442-449, November 10-14, 2002, San Jose, California [doi>10.1145/774572.774637]