Accelerating SAT-based Boolean matching for heterogeneous FPGAs using one-hot encoding and CEGAR technique

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

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
Title of host publication20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages255-260
Number of pages6
ISBN (Electronic)9781479977925
DOIs
Publication statusPublished - Mar 11 2015
Event2015 20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015 - Chiba, Japan
Duration: Jan 19 2015Jan 22 2015

Publication series

Name20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015

Other

Other2015 20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015
CountryJapan
CityChiba
Period1/19/151/22/15

Fingerprint

Field Programmable Gate Array
Program processors
Counterexample
Field programmable gate arrays (FPGA)
Encoding
Refinement
Networks (circuits)
Binary
Constraint Propagation
Matching Problem
CPU Time
Speedup
Assignment
Abstraction

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Electrical and Electronic Engineering
  • Control and Systems Engineering
  • Modelling and Simulation

Cite this

Matsunaga, Y. (2015). Accelerating SAT-based Boolean matching for heterogeneous FPGAs using one-hot encoding and CEGAR technique. In 20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015 (pp. 255-260). [7059014] (20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ASPDAC.2015.7059014

Accelerating SAT-based Boolean matching for heterogeneous FPGAs using one-hot encoding and CEGAR technique. / Matsunaga, Yusuke.

20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015. Institute of Electrical and Electronics Engineers Inc., 2015. p. 255-260 7059014 (20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Matsunaga, Y 2015, Accelerating SAT-based Boolean matching for heterogeneous FPGAs using one-hot encoding and CEGAR technique. in 20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015., 7059014, 20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015, Institute of Electrical and Electronics Engineers Inc., pp. 255-260, 2015 20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015, Chiba, Japan, 1/19/15. https://doi.org/10.1109/ASPDAC.2015.7059014
Matsunaga Y. Accelerating SAT-based Boolean matching for heterogeneous FPGAs using one-hot encoding and CEGAR technique. In 20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015. Institute of Electrical and Electronics Engineers Inc. 2015. p. 255-260. 7059014. (20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015). https://doi.org/10.1109/ASPDAC.2015.7059014
Matsunaga, Yusuke. / Accelerating SAT-based Boolean matching for heterogeneous FPGAs using one-hot encoding and CEGAR technique. 20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015. Institute of Electrical and Electronics Engineers Inc., 2015. pp. 255-260 (20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015).
@inproceedings{4bd7a82f76704733bb064dd3450a9922,
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 = "2015",
month = "3",
day = "11",
doi = "10.1109/ASPDAC.2015.7059014",
language = "English",
series = "20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "255--260",
booktitle = "20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015",
address = "United States",

}

TY - GEN

T1 - Accelerating SAT-based Boolean matching for heterogeneous FPGAs using one-hot encoding and CEGAR technique

AU - Matsunaga, Yusuke

PY - 2015/3/11

Y1 - 2015/3/11

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=84926490243&partnerID=8YFLogxK

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

U2 - 10.1109/ASPDAC.2015.7059014

DO - 10.1109/ASPDAC.2015.7059014

M3 - Conference contribution

AN - SCOPUS:84926490243

T3 - 20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015

SP - 255

EP - 260

BT - 20th Asia and South Pacific Design Automation Conference, ASP-DAC 2015

PB - Institute of Electrical and Electronics Engineers Inc.

ER -