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