Boolean satisfiability in electronic design automation

ABSTRACT

Boolean Satisfiability (SAT) is often used as the underlying model for a significant and increasing number of applications in Electronic Design Automation (EDA) as well as in many other fields of Computer Science and Engineering. In recent years, new and efficient algorithms for SAT have been developed, allowing much larger problem instances to be solved. SAT “packages” are currently expected to have an impact on EDA applications similar to that of BDD packages since their introduction more than a decade ago. This tutorial paper is aimed at introducing the EDA professional to the Boolean satisfiability problem. Specifically, we highlight the use of SAT models to formulate a number of EDA problems in such diverse areas as test pattern generation, circuit delay computation, logic optimization, combinational equivalence checking, bounded model checking and functional test vector generation, among others. In addition, we provide an overview of the algorithmic techniques commonly used for solving SAT, including those that have seen widespread use in specific EDA applications. We categorize these algorithmic techniques, indicating which have been shown to be best suited for which tasks.

REFERENCES

• 1: M. Abramovici, M. A. Breuer and A. D. Friedman, Digital Systems Testing and Testable Design, Computer Science Press, 1990.
• 2: Miron Abramovici , Jose T. de Sousa , Daniel Saab, A massively-parallel easily-scalable satisfiability solver using reconfigurable hardware, Proceedings of the 36th ACM/IEEE conference on Design automation, p.684-690, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.310028]
• 3: E Barth, "A Davis-Putnam Based Enumeration Algorithm for Linear pseudo-Boolean Optimization," Technical Report MPI-I-95-2-003, Max-Planck-Institut fur Informatik, 1995.
• 4: R. Bayardo Jr. and R. Schrag, "Using CSP Look-Back Techniques to Solve Real-World SAT Instances," in Proceedings of the National Conference on Artificial Intelligence (AAAI-97), 1997.
• 5: 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
• 6: Miroslav N. Velev , Randal E. Bryant, Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.37-53, September 27-29, 1999
• 7: Chih-Ang Chen , Sandeep K. Gupta, A satisfiability-based test generator for path delay faults in combinational circuits, Proceedings of the 33rd annual conference on Design automation, p.209-214, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240557]
• 8: Pinhong Chen , Kurt Keutzer, Towards true crosstalk noise analysis, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.132-138, November 07-11, 1999, San Jose, California, United States
• 9: Olivier Coudert, On solving covering problems, Proceedings of the 33rd annual conference on Design automation, p.197-202, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240555]
• 10: 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]
• 11: 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]
• 12: Luis Entrena , Kwang-Ting Cheng, Sequential logic optimization by redundancy addition and removal, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.310-315, November 07-11, 1993, Santa Clara, California, United States
• 13: Farzan Fallah , Srinivas Devadas , Kurt Keutzer, Functional vector generation for HDL models using linear programming and 3-satisfiability, Proceedings of the 35th annual conference on Design automation, p.528-533, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277187]
• 14: Carla P. Gomes , Bart Selman , Henry Kautz, Boosting combinatorial search through randomization, Proceedings of the fifteenth national/tenth conference on Artificial intelligence/Innovative applications of artificial intelligence, p.431-437, July 1998, Madison, Wisconsin, United States
• 15: Jan F Groote , Joost P. Warners, The propositional formula checker HeerHugo, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, 1999
• 16: Aarti Gupta , Pranav Ashar, Integrating a Boolean Satisfiability Checker and BDDs for Combinational Equivalence Checking, Proceedings of the Eleventh International Conference on VLSI Design: VLSI for Signal Processing, p.222, January 04-07, 1998
• 17: J. Kim, J. Marques-Silva, H. Savoj and K. A. Sakallah, "RID-GRASP: Redundancy Identification and Removal Using GRASP", in International Workshop on Logic Synthesis, May 1997.
• 18: Joonyoung Kim , Jesse Whittemore , João P. Marques-Silva , Karem Sakallah, On applying incremental satisfiability to delay fault testing, Proceedings of the conference on Design, automation and test in Europe, p.380-384, March 27-30, 2000, Paris, France [doi>10.1145/343647.343801]
• 19: Wolfgang Kunz , Dominik Stoffel , Vishwani D. Agrawal , Randal E. Bryant, Reasoning in Boolean Networks: Logic Synthesis and Verification Using Testing Techniques, Kluwer Academic Publishers, Norwell, MA, 1997
• 20: T. Larrabee, "Test Pattern Generation Using Boolean Satisfiability," IEEE Transactions on Computer-Aided Design, vol. 11, no. 1, pp. 4-15, January 1992.
• 21: C.-M. Li, "Equivalency Reasoning to Solve a Class of Hard SAT Problems," Submitted for publication. (Available from http://www.research.att.com/^-kautz/challenge/cli.ps.)
• 22: V. Manquinho, A. Oliveira and J. Marques-Silva, "Models and Algorithms for Computing Minimum-Size Prime Implicants," in Proceedings of the International Workshop on Boolean Problems, September 1998.
• 23: Vasco M. Manquinho , João Marques-Silva, On using satisfiability-based pruning techniques in covering algorithms, Proceedings of the conference on Design, automation and test in Europe, p.356-363, March 27-30, 2000, Paris, France [doi>10.1145/343647.343797]
• 24: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• 25: Joao P. Marques Silva , Karem A. Sakallah, Robust Search Algorithms for Test Pattern Generation, Proceedings of the 27th International Symposium on Fault-Tolerant Computing (FTCS '97), p.152, June 25-27, 1997
• 26: 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]
• 27: 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]
• 28: E McGeer, A. Saldanha, E R. Stephan, R. K. Brayton and A. L. Sangiovanni-Vincentelli, "Timing Analysis and Delay-Test Generation Using Path Recursive Functions," in Proceedings of the International Conference on Computer- Aided Design, November 1991.
• 29: Gi-Joon Nam , Karem A. Sakallah , Rob A. Rutenbar, Satisfiability-Based Detailed FPGA Routing, Proceedings of the 12th International Conference on VLSI Design - 'VLSI for the Information Appliance', p.574, January 10-13, 1999
• 30: Gi-Joon Nam , Karem A. Sakallah , Rob A. Rutenbar, Satisfiability-based layout revisited: detailed routing of complex FPGAs via search-based Boolean SAT, Proceedings of the 1999 ACM/SIGDA seventh international symposium on Field programmable gate arrays, p.167-175, February 21-23, 1999, Monterey, California, United States [doi>10.1145/296399.296450]
• 31: A. Saldanha and V. Singhal, "Solving Satisfiability in CAD Problems," in Proceedings of the Cadence Technical Conference, May 1997.
• 32: B. Selman, H. Levesque and D. Mitchell, "A New Method for Solving Hard Satisfiability Problems," in Proceedings of the National Conference on Artificial Intelligence (AAAI- 92), pp. 440-446, 1992.
• 33: Yi Shang , Benjamin W. Wah, A Discrete Lagrangian-Based Global-SearchMethod for Solving Satisfiability Problems, Journal of Global Optimization, v.12 n.1, p.61-99, January 1998 [doi>10.1023/A:1008287028851]
• 34: Mary Sheeran , Gunnar Stålmarck, A Tutorial on Stålmarcks's Proof Procedure for Propositional Logic, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.82-99, November 04-06, 1998
• 35: Naveed A. Sherwani, Algorithms for VLSI Physical Design Automation, Kluwer Academic Publishers, Norwell, MA, 1995
• 36: L. G. Silva, J. E Marques-Silva, L. M. Silveira and K. A. Sakallah, "Satisfiability Models and Algorithms for Circuit Delay Computation," in Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, December 1997.
• 37: Luís Guerra e Silva , L. Miguel Silveira , Joöa Marques-Silva, Algorithms for solving Boolean satisfiability in combinational circuits, Proceedings of the conference on Design, automation and test in Europe, p.107-es, January 1999, Munich, Germany [doi>10.1145/307418.307557]
• 38: E R. Stephan, R. K. Brayton and A. L. Sangiovanni-Vincentelli, "Combinational Test Generation Using Satisfiability," IEEE Transactions on Computer-Aided Design, vol. 15, no. 9, pp. 1167-1176, September 1996.
• 39: Paul Tafertshofer , Andreas Ganz , Manfred Henftling, A SAT-based implication engine for efficient ATPG, equivalence checking, and optimization of netlists, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.648-655, November 09-13, 1997, San Jose, California, United States
• 40: Paul Tafertshofer , Andreas Ganz, SAT based ATPG using fast justification and propagation in the implication graph, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.139-146, November 07-11, 1999, San Jose, California, United States
• 41: R. Zabih and D. A. McAllester, "A Rearrangement Search Strategy for Determining Propositional Satisfiability," in Proceedings of the National Conference on Artificial Intelligence, pp. 155-160, 1988.
• 42: Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997
• 43: Peixin Zhong , Pranav Ashar , Sharad Malik , Margaret Martonosi, Using reconfigurable computing techniques to accelerate problems in the CAD domain: a case study with Boolean satisfiability, Proceedings of the 35th annual conference on Design automation, p.194-199, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277098]

INDEX TERMS

Primary Classification:
  J. Computer Applications

Additional Classification:
  B. Hardware
  B.8 Performance and Reliability

  C. Computer Systems Organization

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

  J. Computer Applications
  J.1 ADMINISTRATIVE DATA PROCESSING
      Subjects: Manufacturing
  J.2 PHYSICAL SCIENCES AND ENGINEERING
      Subjects: Electronics

General Terms:
Algorithms, Design, Management, Performance, Theory, Verification