HW-BCP: A Custom Hardware Accelerator for SAT Suitable for Single Chip Implementation for Large Benchmarks
HW-BCP: A Custom Hardware Accelerator for SAT Suitable for Single Chip Implementation for Large Benchmarks
复制标题
HW-BCP：适用于大型基准的单芯片实施的 SAT 定制硬件加速器
DOI：
10.1145/3394885.3431413
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Gupta, Sandeep K.
中科院分区：
文献类型：
--
作者：
Park, Soowang;Nam, Jae-Won;Gupta, Sandeep K.
布尔可满足性(SAT)在电子设计自动化(EDA)、人工智能(AI)和理论研究中有着广泛的应用。此外，作为一个NP完全问题，SAT的加速也将使一系列组合问题的加速成为可能。我们提出了一种全新的定制硬件设计来加速SAT。从布尔约束传播(BCP)占用大部分SAT求解时间(80%-90%)这一众所周知的事实开始，我们专注于加速BCP。通过分析广泛使用的软件SAT求解器MiniSAT v2.2.0(MiniSAT2)[1]，我们发现了通过并行化和消除von Neumann开销，特别是数据移动来加速BCP的机会。建议的BCP硬件(HW-BCP)通过定制内容可寻址存储器(CAM)单元、SRAM单元、逻辑电路和优化互连的组合来实现这些目标。在65 nm技术中，在SAT竞赛2017基准套件中最大的SAT实例上，我们的HW-BCP显著加速了BCP(模拟中每个BCP 4.5 ns)，因此与运行在通用处理器上的优化软件实现相比，提供了62-185倍的加速比。最后，我们将HW-BCP设计推断为7 nm技术，并估计了面积和延迟。分析表明，在7 nm的实际芯片大小下，HW-BCP将足够大，可以容纳基准测试套件中最大的SAT实例。
Boolean Satisfiability (SAT) has broad usage in Electronic Design Automation (EDA), artificial intelligence (AI), and theoretical studies. Further, as an NP-complete problem, acceleration of SAT will also enable acceleration of a wide range of combinatorial problems.We propose a completely new custom hardware design to accelerate SAT. Starting with the well-known fact that Boolean Constraint Propagation (BCP) takes most of the SAT solving time (80-90%), we focus on accelerating BCP. By profiling a widely-used software SAT solver, MiniSAT v2.2.0 (MiniSAT2) [1], we identify opportunities to accelerate BCP via parallelization and elimination of von Neumann overheads, especially data movement. The proposed hardware for BCP (HW-BCP) achieves these goals via a customized combination of content-addressable memory (CAM) cells, SRAM cells, logic circuitry, and optimized interconnects.In 65nm technology, on the largest SAT instances in the SAT Competition 2017 benchmark suite, our HW-BCP dramatically accelerates BCP (4.5ns per BCP in simulations) and hence provides a 62-185x speedup over optimized software implementation running on general purpose processors.Finally, we extrapolate our HW-BCP design to 7nm technology and estimate area and delay. The analysis shows that in 7nm, in a realistic chip size, HW-BCP would be large enough for the largest SAT instances in the benchmark suite.
DOI：
10.1109/tvlsi.2017.2754192
发表时间：
2016-06
影响因子：
2.8
作者：
Xunzhao Yin;B. Sedighi;M. Varga;M. Ercsey-Ravasz;Z. Toroczkai;X. Hu
通讯作者：
Xunzhao Yin;B. Sedighi;M. Varga;M. Ercsey-Ravasz;Z. Toroczkai;X. Hu
SAT 求解器的增强型布尔约束传播的 FPGA 加速
DOI：
--
发表时间：
2013
期刊：
2013 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)
影响因子：
--
作者：
J. Thong;N. Nicolici
通讯作者：
N. Nicolici