SAT and ATPG: Boolean engines for formal hardware verification

ABSTRACT

In this survey, we outline basic SAT- and ATPG- procedures as well as their applications in formal hardware verification. We attempt to give the reader a trace trough literature and provide a basic orientation concerning the problem formulations and known approaches in this active field of research.

REFERENCES

• 1: {AB90} M. Abramovici, M. Breuer, and A. Friedman, Digital Systems Testing and Testable Design. Computer Science Press, New York, 1990.
• 2: {AS01} F. A. Aloul and K. A. Sakallah, "SAT using ZBDDs," in Dagstuhl Seminar 01051 on Computer Aided Design and Test -- BDDs versus SAT, Schloss Dagstuhl, Germany, Jan/Feb. 01.
• 3: 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
• 4: {BS97} R. Bayardo Jr. and R. Schrag, "Using CSP look-back techniques to solve real-world SAT instances," in Proc. Natl. Conf. on Artificial Intelligence, pp. 203--208, 1997.
• 5: {BT89} C.L. Berman, and L.H. Trevillyan, "Functional Comparison of Logic Designs for VLSI Circuits", in Proc. Intl. Conf. on Comp.-Aided Design (ICCAD), pp. 456--459, 1989.
• 6: Daniel Brand, Verification of large synthesized designs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.534-537, November 07-11, 1993, Santa Clara, California, United States
• 7: Robert King Brayton , Alberto L. Sangiovanni-Vincentelli , Curtis T. McMullen , Gary D. Hachtel, Logic Minimization Algorithms for VLSI Synthesis, Kluwer Academic Publishers, Norwell, MA, 1984
• 8: Jason Baumgartner , Andreas Kuehlmann , Jacob A. Abraham, Property Checking via Structural Analysis, Proceedings of the 14th International Conference on Computer Aided Verification, p.151-165, July 27-31, 2002
• 9: {CA93} S. Chakradhar, V. D. Agrawal, and S. Rothweiler, "A transitive closure algorithm for test generation," IEEE Trans. on CAD, vol. 12, pp. 1015--1028, July 1993.
• 10: 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
• 11: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 12: 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]
• 13: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 14: {FS83} H. Fujiwara and T. Shimono, "On the acceleration of test generation algorithms," IEEE Trans. on Comp., pp. 1137--1144, Dec. 1983.
• 15: Malay K. Ganai , Pranav Ashar , Aarti Gupta , Lintao Zhang , Sharad Malik, Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514105]
• 16: 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
• 17: Emil Gizdarski , Hideo Fujiwara, SPIRIT: A Highly Robust Combinational Test Generation Algorithm, Proceedings of the 19th IEEE VLSI Test Symposium, p.346, March 29-April 03, 2001
• 18: {Go81} P. Goel, "An implicit enumeration algorithm to generate tests for combinational logic circuits," IEEE Trans. on Comp., vol. C-30, pp. 215--222, March 1981.
• 19: Jawahar Jain , Rajarshi Mukherjee , Masahiro Fujita, Advanced verification techniques based on learning, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.420-426, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217564]
• 20: T. Kirkland , M. R. Mercer, A topological search algorithm for ATPG, Proceedings of the 24th ACM/IEEE conference on Design automation, p.502-508, June 28-July 01, 1987, Miami Beach, Florida, United States [doi>10.1145/37888.37963]
• 21: Hans K. Buning , T. Letterman, Propositional Logic: Deduction and Algorithms, Cambridge University Press, New York, NY, 1999
• 22: Andreas Kuehlmann , Florian Krohm, Equivalence checking using cuts and heaps, Proceedings of the 34th annual conference on Design automation, p.263-268, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266090]
• 23: Andreas Kuehlmann , Malay K. Ganai , Viresh Paruthi, Circuit-based Boolean Reasoning, Proceedings of the 38th conference on Design automation, p.232-237, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378470]
• 24: Wolfgang Kunz , Dhiraj K. Pradhan, Recursive Learning: An Attractive Alternative to the Decision Tree for Test Genration in Digital Circuits, Proceedings of the IEEE International Test Conference on Discover the New World of Test and Design, p.816-825, September 20-24, 1992
• 25: Wolfgang Kunz, HANNIBAL: an efficient tool for logic verification based on recursive learning, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.538-543, November 07-11, 1993, Santa Clara, California, United States
• 26: Wolfgang Kunz , João Marques-Silva , Sharad Malik, SAT and ATPG: algorithms for Boolean decision problems, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
• 27: {La89} T. Larrabee, "Efficient generation of test patterns using Boolean difference," in Proc. Intl. Test Conference, pp. 795--801, 1989.
• 28: Ralph Marlett, An effective test generation system for sequential circuits, Proceedings of the 23rd ACM/IEEE conference on Design automation, p.250-256, July 1986, Las Vegas, Nevada, United States
• 29: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 30: 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
• 31: {MW85} S. Mallela and S. Wu, "A sequential circuit test generation system," in Proc. Intl. Test Conf., pp. 57--61, 1985.
• 32: João Marques-Silva , Thomas Glass, Combinational equivalence checking using satisfiability and recursive learning, Proceedings of the conference on Design, automation and test in Europe, p.33-es, January 1999, Munich, Germany [doi>10.1145/307418.307477]
• 33: 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]
• 34: Yusuke Matsunaga, An efficient equivalence checker for combinational circuits, Proceedings of the 33rd annual conference on Design automation, p.629-634, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240637]
• 35: 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]
• 36: {RC90} J. Rajski and H. Cox, "A method to calculate necessary assignments in algorithmic test pattern generation," in Proc. Intl. Test Conference, pp. 25--34, 1990.
• 37: {Ro66} J. P. Roth, "Diagnosis of automata failures: A calculus and a method," IBM Journal of Research and Development, vol. 10, pp. 278--291, July 1966.
• 38: {SA89} M. Schulz and E. Auth, "Improved deterministic test pattern generation with applications to redundancy identification," IEEE Trans. on CAD, vol. 8, pp. 811--816, July 1989.
• 39: {St89} G. Stålmarck, "A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula," 1989, Swedish Patent 467 076, US Patent 5 276 897, European Patent 0 403454.
• 40: {SB96} P. Stephan, R. Brayton, and A. Sangiovanni-Vincentelli, "Combinational test generation using satisfiability," IEEE Trans. on CAD, 1996.
• 41: Mary Sheeran , Satnam Singh , Gunnar Stålmarck, Checking Safety Properties Using Induction and a SAT-Solver, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.108-125, November 01-03, 2000
• 42: {TG00} P. Tafertshofer, A. Ganz, and K. Antreich, "Igraine - an implication graph based engine for fast implication, justification, and propagation," IEEE Trans. on CAD, vol. 19, pp. 907--927, August 2000.
• 43: {Ts70} G.S. Tseitin, "On the Complexity of Derivation in Propositional Calculus", in A.O. Slikenko (Ed.): Studies in Constructive Mathematics and Mathematical Logic
• 44: Chen Wang , Sudhakar M. Reddy , Irith Pomeranz , Xijiang Lin , Janusz Rajski, Conflict driven techniques for improving deterministic test pattern generation, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.87-93, November 10-14, 2002, San Jose, California [doi>10.1145/774572.774585]
• 45: Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification

Additional Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms
          Subjects: Analysis of algorithms
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Answer/reason extraction

General Terms:
Algorithms, Theory, Verification