SMT Solver With Hardware Acceleration

Yean Ru Chen, Si Han Chen, Shang Wei Lin

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish
Pages (from-to)2055-2068
Number of pages14
JournalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Volume42
Issue number6
DOIs
Publication statusPublished - 2023 Jun 1

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

Fingerprint

Dive into the research topics of 'SMT Solver With Hardware Acceleration'. Together they form a unique fingerprint.

Cite this