SATORI - A Fast Sequential SAT Engine for Circuits

ABSTRACT

We describe the design and implementation of SATORI - a fast sequentialjustification engine based on state-of-the-art SAT and ATPG techniques.We present several novel techniques that propel SATORI to ademonstrable 10x improvement over a commercial engine. Traditionalsequential justification based on ATPG or, on a bounded model of thesequential circuit using SAT, has diverging strengths and weaknesses. Inthis paper, we contrast these techniques and describe how their strengthsare combined in SATORI. We use conflict-based learning in each time-frameand illegal state learning across time-frames. This enables bothcombinational and sequential back-jumping. We experimentally analyzethe main features of SATORI by comparing SATORI's performanceagainst a state-of-the-art SAT solver - ZCHAFF using a boundedmodel, and a commercial sequential ATPG engine performing justification.Additional results are presented for SATORI versus the commercialATPG engine and VIS on ISCAS ý89 and ITC'99 benchmark circuitsfor an application to assertion checking.

REFERENCES

• 1: 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]
• 2: Jacob A. Abraham , Vivekananda M. Vedula , Daniel G. Saab, Verifying Properties Using Sequential ATPG, Proceedings of the 2002 IEEE International Test Conference, p.194, October 07-10, 2002
• 3: [3] M. Abramovici, M. A. Breuer, and A. D. Friedman. Digital Systems Testing and Testable Design. CS Press, 1st ed., 1990.
• 4: 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]
• 5: Vamsi Boppana , Sreeranga P. Rajan , Koichiro Takayama , Masahiro Fujita, Model Checking Based on Sequential ATPG, Proceedings of the 11th International Conference on Computer Aided Verification, p.418-430, July 06-10, 1999
• 6: Xinghao Chen , Michael L. Bushnell, Sequential circuit test generation using dynamic justification equivalence, Journal of Electronic Testing: Theory and Applications, v.8 n.1, p.9-33, Feb. 1996 [doi>10.1007/BF00136073]
• 7: K.-T. Cheng , H.-K. T. Ma, On the over-specification problem in sequential ATPG algorithms, Proceedings of the 29th ACM/IEEE conference on Design automation, p.16-21, June 08-12, 1992, Anaheim, California, United States
• 8: Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
• 9: G. Parthasarathy , Kwang-Ting Cheng , Chung-Yang Huang, An Analysis of ATPG and SAT algorithms for Formal Verification, Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop (HLDVT'01), p.177, December 07-09, 2001
• 10: Chung-Yang (Ric) Huang , Bwolen Yang , Huan-Chih Tsai , Kwang-Ting (Tim) Cheng, Static Property Checking Using ATPG v.s. BDD Techniques, Proceedings of the 2000 IEEE International Test Conference, p.309, October 03-05, 2000
• 11: João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
• 12: 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]
• 13: 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]
• 14: 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
• 15: [15] P. Tafertshofer, A. Ganz, and K. Antreich. IGRAINE - An Implication-Graph based Engine for Fast Implication, Justification and Propagation. IEEE Trans. on Computer-Aided Design, 19(8):907-927, August 2000.
• 16: 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

INDEX TERMS

Primary Classification:
  B. Hardware
  B.8 Performance and Reliability
      B.8.2 Performance Analysis and Design Aids

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.1 Design Styles
          Subjects: Combinational logic

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures