SMT Solver With Hardware Acceleration
Yean-Ru Chen, Sihan Chen, Shang‐Wei Lin · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · 2022
Satisfiability modulo theories (SMTs), an extension of Boolean satisfiability (SAT) problem, is widely used in many application domains because of its rich expressiveness. Thus, there are many works trying to speedup the process of SAT/SMT solving. In this work, we develop a framework by proposing a new hardware architecture to solve the SMT problem for the theory of quantifier free linear real arithmetic (QF-LRA) to speedup the SMT solving process. The new proposed architecture framework consists of a hardware SAT solver and a hardware Simplex solver. Our hardware SAT solver has an optimized Boolean constraint propagation process with a pipeline structure and a nonchronological backtracking mechanism, while our hardware Simplex solver supports parallel operation flow inside the Simplex iteration to execute the selection operations parallelly with the pivot operation and the row selection mechanism to avoid unnecessary row computation and increase the resource utilization. According to our experimental results, the proposed framework can achieve from 2.539 up to 1561.181 times speedup compared with software SMT solvers in our selected 40 benchmarks.