An Approach for Solving SAT/MaxSAT-Encoded Formal Verification Problems on FPGA

• KANAZAWA Kenji

  Division of Information Engineering, Faculty of Engineering, Information and Systems, University of Tsukuba

• MARUYAMA Tsutomu

  Division of Intelligent Interaction Technologies, Faculty of Engineering, Information and Systems, University of Tsukuba

抄録

WalkSAT (WSAT) is one of the best performing stochastic local search algorithms for the Boolean Satisfiability (SAT) and the Maximum Boolean Satisfiability (MaxSAT). WSAT is very suitable for hardware acceleration because of its high inherent parallelism. Formal verification of digital circuits is one of the most important applications of SAT and MaxSAT. Structural knowledge such as logic gates and their dependencies can be derived from SAT/MaxSAT instances generated from formal verification of digital circuits. Such that knowledge is useful to solve these instances efficiently. In this paper, we first discuss a heuristic to utilize the structural knowledge for solving these problems by using WSAT. Then, we show its implementation on FPGA. The problem size of the formal verification is typically very large, and most data have to be placed in off-chip DRAMs. In this situation, the acceleration by FPGA is limited by the throughput and access latency of the DRAMs. In our implementation, data are carefully mapped on the on-chip memory banks and off-chip DRAMs so that most data in the off-chip DRAMs can be continuously accessed using burst-read. Furthermore, a variable-way cache memory comprised of the on-chip memory banks is used in order to hide the DRAM access latency by caching the head portion of the continuous read from the DRAMs and giving them to the circuit till the rest portion is started to be given by the burst-read. We evaluate the performance of our proposed method by changing configuration of the variable-way cache and the processing parallelism, and discuss how much acceleration can be achieved.

収録刊行物

• IEICE Transactions on Information and Systems

  IEICE Transactions on Information and Systems E100.D (8), 1807-1818, 2017

  一般社団法人 電子情報通信学会

キーワード

• FPGA
• SAT
• MaxSAT
• WalkSAT

詳細情報

• CRID: 1390001204377333632
• NII論文ID: 130005875991
• NII書誌ID: AA10826272
• DOI: 10.1587/transinf.2016edp7487
• ISSN: 17451361
• ISSN: 09168532
• HANDLE: 2241/00147401
• Web Site: https://tsukuba.repo.nii.ac.jp/records/42499
• Web Site: https://www.jstage.jst.go.jp/article/transinf/E100.D/8/E100.D_2016EDP7487/_pdf
• 本文言語コード: en
• データソース種別:
  • JaLC
  • IRDB
  • Crossref
  • CiNii Articles
• 抄録ライセンスフラグ: 使用不可