Accelerating SAT-Based Boolean Matching for Heterogeneous FPGAs Using One-Hot Encoding and CEGAR Technique

Yusuke MATSUNAGA

doi:10.1587/transfun.E99.A.1374

Accelerating SAT-Based Boolean Matching for Heterogeneous FPGAs Using One-Hot Encoding and CEGAR Technique

Yusuke MATSUNAGA

Full Text Views

0

Share
Cite this

Summary :

This paper describes two speed-up techniques for Boolean matching of LUT-based circuits. One is one-hot encoding technique for variables representing input assignments. Though it requires more variables than existing binary encoding technique, almost all added clauses using one-hot encoding are binary clauses, which are suitable for efficient Boolean constraint propagation. The other is CEGAR (counter example guided abstraction refinement) technique which reduces the CPU time significantly. With both techniques, we can solve Boolean matching problem with 9 input function in 20 milliseconds on average, which is faster than the existing algorithms more than one order of magnitude.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E99-A No.7 pp.1374-1380

Publication Date: 2016/07/01

Publicized

Online ISSN: 1745-1337

DOI: 10.1587/transfun.E99.A.1374

Type of Manuscript: Special Section PAPER (Special Section on Design Methodologies for System on a Chip)

Category

Authors

Yusuke MATSUNAGA
Kyushu University

Keyword

logic synthesis, technology mapping, FPGA, SAT

Cite this

Copy

Yusuke MATSUNAGA, "Accelerating SAT-Based Boolean Matching for Heterogeneous FPGAs Using One-Hot Encoding and CEGAR Technique" in IEICE TRANSACTIONS on Fundamentals, vol. E99-A, no. 7, pp. 1374-1380, July 2016, doi: 10.1587/transfun.E99.A.1374.
Abstract: This paper describes two speed-up techniques for Boolean matching of LUT-based circuits. One is one-hot encoding technique for variables representing input assignments. Though it requires more variables than existing binary encoding technique, almost all added clauses using one-hot encoding are binary clauses, which are suitable for efficient Boolean constraint propagation. The other is CEGAR (counter example guided abstraction refinement) technique which reduces the CPU time significantly. With both techniques, we can solve Boolean matching problem with 9 input function in 20 milliseconds on average, which is faster than the existing algorithms more than one order of magnitude.
URL: https://globals.ieice.org/en_transactions/fundamentals/10.1587/transfun.E99.A.1374/_p

Copy

@ARTICLE{e99-a_7_1374,
author={Yusuke MATSUNAGA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Accelerating SAT-Based Boolean Matching for Heterogeneous FPGAs Using One-Hot Encoding and CEGAR Technique},
year={2016},
volume={E99-A},
number={7},
pages={1374-1380},
abstract={This paper describes two speed-up techniques for Boolean matching of LUT-based circuits. One is one-hot encoding technique for variables representing input assignments. Though it requires more variables than existing binary encoding technique, almost all added clauses using one-hot encoding are binary clauses, which are suitable for efficient Boolean constraint propagation. The other is CEGAR (counter example guided abstraction refinement) technique which reduces the CPU time significantly. With both techniques, we can solve Boolean matching problem with 9 input function in 20 milliseconds on average, which is faster than the existing algorithms more than one order of magnitude.},
keywords={},
doi={10.1587/transfun.E99.A.1374},
ISSN={1745-1337},
month={July},}

Copy

TY - JOUR
TI - Accelerating SAT-Based Boolean Matching for Heterogeneous FPGAs Using One-Hot Encoding and CEGAR Technique
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1374
EP - 1380
AU - Yusuke MATSUNAGA
PY - 2016
DO - 10.1587/transfun.E99.A.1374
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E99-A
IS - 7
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - July 2016
AB - This paper describes two speed-up techniques for Boolean matching of LUT-based circuits. One is one-hot encoding technique for variables representing input assignments. Though it requires more variables than existing binary encoding technique, almost all added clauses using one-hot encoding are binary clauses, which are suitable for efficient Boolean constraint propagation. The other is CEGAR (counter example guided abstraction refinement) technique which reduces the CPU time significantly. With both techniques, we can solve Boolean matching problem with 9 input function in 20 milliseconds on average, which is faster than the existing algorithms more than one order of magnitude.
ER -