TY - GEN
T1 - Accelerating Boolean satisfiability with configurable hardware
AU - Zhong, Peixin
AU - Martonosi, Margaret Rose
AU - Ashar, P.
AU - Malik, Sharad
N1 - Funding Information:
The authors thank Joshua Toub for his help mapping this SAT algorithm to the Pamette board. This work was supported in part by DARPA grant DABT63-97-1-0001, by an NSF Career Award (Martonosi) and by a research donation from NEC.
Publisher Copyright:
© 1998 IEEE.
PY - 1998
Y1 - 1998
N2 - This paper describes and evaluates methods for implementing formula-specific Boolean satisfiability (SAT) solver circuits in configurable hardware. Starting from a general template design, our approach automatically generates VHDL for a circuit that is specific to the particular Boolean formula being solved. Such an approach tightly customizes the circuit to a particular problem instance. Thus, it represents an ideal use for dynamically-reconfigurable hardware, since it would be impractical to fabricate an ASIC for each Boolean formula being solved. Our approach also takes advantage of direct gate mappings and large degrees of fine-grained parallelism in the algorithm's Boolean logic evaluations. We compile our designs to two hardware targets: an IKOS logic emulation system, and Digital SRC's Pamette configurable computing board. Performance evaluations on the DIMACS SAT benchmark suite indicate that our approach offers speedups from 17X to more than a thousand times. Overall, this SAT solver demonstrates promising performance speedups on an important and complex problem with extensive applications in the CAD and AI communities.
AB - This paper describes and evaluates methods for implementing formula-specific Boolean satisfiability (SAT) solver circuits in configurable hardware. Starting from a general template design, our approach automatically generates VHDL for a circuit that is specific to the particular Boolean formula being solved. Such an approach tightly customizes the circuit to a particular problem instance. Thus, it represents an ideal use for dynamically-reconfigurable hardware, since it would be impractical to fabricate an ASIC for each Boolean formula being solved. Our approach also takes advantage of direct gate mappings and large degrees of fine-grained parallelism in the algorithm's Boolean logic evaluations. We compile our designs to two hardware targets: an IKOS logic emulation system, and Digital SRC's Pamette configurable computing board. Performance evaluations on the DIMACS SAT benchmark suite indicate that our approach offers speedups from 17X to more than a thousand times. Overall, this SAT solver demonstrates promising performance speedups on an important and complex problem with extensive applications in the CAD and AI communities.
UR - http://www.scopus.com/inward/record.url?scp=84956858537&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84956858537&partnerID=8YFLogxK
U2 - 10.1109/FPGA.1998.707896
DO - 10.1109/FPGA.1998.707896
M3 - Conference contribution
AN - SCOPUS:84956858537
T3 - Proceedings - IEEE Symposium on FPGAs for Custom Computing Machines, FCCM 1998
SP - 1
EP - 10
BT - Proceedings - IEEE Symposium on FPGAs for Custom Computing Machines, FCCM 1998
A2 - Pocek, Kenneth L.
A2 - Arnold, Jeffrey M.
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 1998 IEEE Symposium on FPGAs for Custom Computing Machines, FCCM 1998
Y2 - 15 April 1998 through 17 April 1998
ER -