An FPGA Solver for SAT-Encoded Formal Verification Problems

Formal verification is one of the most important applications of the satisfiability (SAT) problem. WSAT and its variants are one of the best performing stochastic local search algorithms. In this paper, we propose an FPGA solver for SAT-encoded verification problems based on a WSAT algorithm. The size of the verification problems is very large, and most of the data used in the algorithm have to be placed in off-chip DRAMs. The performance of the solver is limited by the throughput and access delay of the DRAMs, not by the parallelism in FPGA. We show how much speed-up is possible under this situation using the memory throughput, memory access delay and the operational frequency of FPGA as parameters.