Solving SAT-encoded Formal Verification Problems on SoC Based on a WSAT Algorithm with a New Heuristic for Hardware Acceleration
Kenji Kanazawa, Tsutomu Maruyama · 2013
In this paper, we describe a heuristic in a Walk SAT (WSAT) algorithm for solving SAT-encoded formal verification problems efficiently on hardware, and its expected performance on system on chip (SoC). In WSAT algorithms, an assignment of binary values to the variables which satisfy all clauses is searched by repeatedly choosing a variable in an unsatisfied clause using a heuristic, and flipping its value. In the SAT-encoded formal verification problems, logic gates and their functional dependencies can be reconstructed from their propositional conjunctive normal form. In our heuristic, first, the output signals of logic gates are flipped preferentially to propagate the changes in the upper stream to their down-stream efficiently. Secondly, a search direction control mechanism is introduced to change the data propagation direction automatically: from the upper to the lower or from the lower to the upper. We show how our heuristic on SoC can improve the performance of WSAT algorithms.