Using reconfigurable computing techniques to accelerate problems in the CAD domain: a case study with Boolean satisfiability

ABSTRACT

The Boolean satisfiability problem lies at the core of several CAD applications, including automatic test pattern generation and logic synthesis. This paper describes and evaluates an approach for accelerating Boolean satisfiability using configurable hardware. Our approach harnesses the increasing speed and capacity of field-programmable gate arrays by tailoring the SAT-solver circuit to the particular formula being solved. This input-specific technique gets high performance due both to (i) a direct mapping of Boolean operations to logic gates, and (ii) large amounts of fine-grain parallelism in the implication processing. Overall, these strategies yields impressive speedups (>200X in many cases) compared to current software approaches, and they require only modest amounts of hardware. In a broader sense, this paper alerts the hardware design community to the increasing importance of input-specific designs, and documents their promise via a quantitative study of input-specific SAT solving.

REFERENCES

• 1: Miron Abramovici , Daniel G. Saab, Satisfiability on reconfigurable hardware, Proceedings of the 7th International Workshop on Field-Programmable Logic and Applications, p.448-456, September 01-03, 1997
• 2: J. Babb, R. Tessler, 8nd A. Agarwal. Virtual Wires: Overcoming pin limitations in FPGA-based logic emulators. In Proc. IEEE Workshop on FPGA-baaed Cusgom Computing Machines, pages 142-151, Apr. 1993.
• 3: S. Chakradhar, V. Agr&wal, 8nd S. Rothweiler. A transitire closure algorithm for test generation. IEEE Trans. on Computer-Aided Design of Integrated Circuit8 and Systems, 12(7):1015-1028, July 1993.
• 4: 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]
• 5: DIMACS. DIMACS Challenge benchmarks 8nd UCSC benchmarks. Available at ftp://Dimacs. Rutgers.EDU/pub/challenge/sat/benchmarks/cnf.
• 6: P. Goel. An Implicit Enumeration Algorithm to Generate Tests for Combinational Logic Circuits. IEEE 7~un. on Computers, C30(3):215-222, March 1981.
• 7: IKOS Systems. Virtual Logic SLI Documentation. Version 1.6.
• 8: T. Larrabee. Test Pattern Generation Using Boolean Sarisfiability. In IE EE Trans. on Go,rater-Aided Design, volume 11, pages 4-15, January 1992.
• 9: Azra Rashid , Jason Leonard , William H. Mangione-Smith, Dynamic Circuit Generation for Solving Specific Problem Instances of Boolean Satisfiability, Proceedings of the IEEE Symposium on FPGAs for Custom Computing Machines, p.196, April 15-17, 1998
• 10: Jonathan Rose , Dwight Hill, Architectural and physical design challenges for one-million gate FPGAs and beyond, Proceedings of the 1997 ACM fifth international symposium on Field-programmable gate arrays, p.129-132, February 09-11, 1997, Monterey, California, United States [doi>10.1145/258305.258324]
• 11: 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
• 12: P. Stephan, R. Brayton, 8nd A. Sangiovanni-Vincentelli. Combinational Test Generation Using $atisfiabilitlt. Department of Electrical Engineering 8nd Computer Sciences, University of California at Berkeley, 1992. UCB/ERL Memo M92/112.
• 13: Takayuki Suyama , Makoto Yokoo , Hiroshi Sawada, Solving Satisfiability Problems on FPGAs, Proceedings of the 6th International Workshop on Field-Programmable Logic, Smart Applications, New Paradigms and Compilers, p.136-145, September 23-25, 1996
• 14: Xillnx Corp. The Programmable Logic Data Book. Xilinx Corp. San Jose, CA, 1996.

INDEX TERMS

Primary Classification:
  J. Computer Applications

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
          Subjects: Gate arrays
  B.8 Performance and Reliability

  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.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

General Terms:
Algorithms, Design, Measurement, Performance, Theory

Keywords:
emulation, functional simulation, reconstruction, visibility