An Efficient, Scalable Hardware Engine for Boolean SATisfiability

Boolean Satisfiability (SAT) is a core NP-complete problem in logic synthesis. Several heuristic software and hardware approaches have been proposed to solve this problem. In this paper, we present a hardware solution to the SAT problem. We propose a custom IC to implement our approach, in which the traversal of the implication graph as well conflict clause generation are performed in hardware, in parallel. In our approach, clause literals are stored in specially designed cells. Clauses are implemented in banks, in a manner that allows clauses of variable width to be accommodated in these banks. To maximize the utilization of these banks, we initially partition the SAT problem. Our design is flexible in that it can implement various Boolean Constraint Propagation (BCP) engines on the same die, at the same time, allowing the user to switch BCP engines dynamically. Our solution has significantly larger capacity than existing hardware SAT solvers, and is scalable in the sense that several ICs can be used to simultaneously operate on the same SAT instance, effectively increasing capacity further. Our area and performance figures are derived from layout and SPICE (using extracted parasitics) estimates. Additionally, the approach presented in this paper have been functionally validated in Verilog. Preliminary results demonstrate that our approach can accommodate instances with approximately 63K clauses on a single IC of size 1.5cmx 1.5cm. The approach re suits in over 4 orders of magnitude speed improvement over BCP based software SAT approaches (2-3 orders of magnitude over other hardware SAT approaches). The capacity of our approach is significantly higher than most hardware based approaches.