期刊
JOURNAL OF SIGNAL PROCESSING SYSTEMS FOR SIGNAL IMAGE AND VIDEO TECHNOLOGY
卷 91, 期 11-12, 页码 1259-1272出版社
SPRINGER
DOI: 10.1007/s11265-018-1435-y
关键词
Resolution proof checking; Accelerator; FPGA; Hybrid Memory Cube
资金
- German Research Foundation (DFG) within the Collaborative Research Centre On-The-Fly Computing [SFB 901]
Modern Boolean satisfiability solvers can emit proofs of unsatisfiability. There is substantial interest in being able to verify such proofs and also in using them for further computations. In this paper, we present an FPGA accelerator for checking resolution proofs, a popular proof format. Our accelerator exploits parallelism at the low level by implementing the basic resolution step in hardware, and at the high level by instantiating a number of parallel modules for proof checking. Since proof checking involves highly irregular memory accesses, we employ Hybrid Memory Cube technology for accelerator memory. The results show that while the accelerator is scalable and achieves speedups for all benchmark proofs, performance improvements are currently limited by the overhead of transitioning the proof into the accelerator memory.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据