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

Kenji KANAZAWA; Tsutomu MARUYAMA

doi:10.1587/transinf.2016EDP7487

IEICE TRANSACTIONS on Information

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

Kenji KANAZAWA, Tsutomu MARUYAMA

Full Text Views

0

Cite this

Summary :

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.

Publication: IEICE TRANSACTIONS on Information Vol.E100-D No.8 pp.1807-1818

Publication Date: 2017/08/01

Publicized: 2017/05/12

Online ISSN: 1745-1361

DOI: 10.1587/transinf.2016EDP7487

Type of Manuscript: PAPER

Category: Computer System

Authors

Kenji KANAZAWA
University of Tsukuba
Tsutomu MARUYAMA
University of Tsukuba

Keyword

FPGA, SAT, MaxSAT, WalkSAT

Cite this

Copy

Kenji KANAZAWA, Tsutomu MARUYAMA, "An Approach for Solving SAT/MaxSAT-Encoded Formal Verification Problems on FPGA" in IEICE TRANSACTIONS on Information, vol. E100-D, no. 8, pp. 1807-1818, August 2017, doi: 10.1587/transinf.2016EDP7487.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2016EDP7487/_p

Copy

@ARTICLE{e100-d_8_1807,
author={Kenji KANAZAWA, Tsutomu MARUYAMA, },
journal={IEICE TRANSACTIONS on Information},
title={An Approach for Solving SAT/MaxSAT-Encoded Formal Verification Problems on FPGA},
year={2017},
volume={E100-D},
number={8},
pages={1807-1818},
abstract={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.},
keywords={},
doi={10.1587/transinf.2016EDP7487},
ISSN={1745-1361},
month={August},}

Copy

TY - JOUR
TI - An Approach for Solving SAT/MaxSAT-Encoded Formal Verification Problems on FPGA
T2 - IEICE TRANSACTIONS on Information
SP - 1807
EP - 1818
AU - Kenji KANAZAWA
AU - Tsutomu MARUYAMA
PY - 2017
DO - 10.1587/transinf.2016EDP7487
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E100-D
IS - 8
JA - IEICE TRANSACTIONS on Information
Y1 - August 2017
AB - 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.
ER -

IEICE TRANSACTIONS on Information