FPGA acceleration of SAT/Max-SAT solving using variable-way cache

WalkSAT (WSAT) is a stochastic local search algorithms for Boolean Satisfiability (SAT) and Maximum Boolean Satisfiability (MaxSAT) problems, and it is very suitable for hardware acceleration because of its high inherent parallelism. Formal verification is one of the most important applications of SAT and MaxSAT, however, the size of the formal verification problems is significantly larger than on-chip memory size, and most of the data have to be placed in off-chip DRAM. In this paper, we propose a method to hide the access delay by using on-chip memory banks as a variable-way associative cache memory. The size of data blocks that are frequently fetched from the DRAM considerably varies in the WSAT algorithm. This cache memory aims to hold whole block when it is small enough, and only the head portion when it is large, to hide the DRAM access delay. With this cache memory, up to 60% DRAM access delay can be hidden, and the performance can be improved up to 26%.