Accelerating SAT-based boolean matching for heterogeneous FPGAS using one-hot encoding and CEGAR technique

Research output: Contribution to journalArticle

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.

Original languageEnglish
Pages (from-to)1374-1380
Number of pages7
JournalIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
VolumeE99A
Issue number7
DOIs
Publication statusPublished - Jul 1 2016

Fingerprint

Program processors
Counterexample
Encoding
Refinement
Networks (circuits)
Binary
Constraint Propagation
Matching Problem
CPU Time
Speedup
Assignment
Abstraction

All Science Journal Classification (ASJC) codes

  • Signal Processing
  • Computer Graphics and Computer-Aided Design
  • Applied Mathematics
  • Electrical and Electronic Engineering

Cite this

@article{a2ed01d21ad043bfab8468965217c752,
title = "Accelerating SAT-based boolean matching for heterogeneous FPGAS using one-hot encoding and CEGAR technique",
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.",
author = "Yusuke Matsunaga",
year = "2016",
month = "7",
day = "1",
doi = "10.1587/transfun.E99.A.1374",
language = "English",
volume = "E99A",
pages = "1374--1380",
journal = "IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences",
issn = "0916-8508",
publisher = "Maruzen Co., Ltd/Maruzen Kabushikikaisha",
number = "7",

}

TY - JOUR

T1 - Accelerating SAT-based boolean matching for heterogeneous FPGAS using one-hot encoding and CEGAR technique

AU - Matsunaga, Yusuke

PY - 2016/7/1

Y1 - 2016/7/1

N2 - 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.

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.

UR - http://www.scopus.com/inward/record.url?scp=84976885402&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84976885402&partnerID=8YFLogxK

U2 - 10.1587/transfun.E99.A.1374

DO - 10.1587/transfun.E99.A.1374

M3 - Article

VL - E99A

SP - 1374

EP - 1380

JO - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

JF - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

SN - 0916-8508

IS - 7

ER -