SAT-based methods for circuit synthesis

Roderick Paul Bloem; Uwe Egly; Patrick Klampfl; Robert Könighofer; Florian Lonsing

doi:10.1109/FMCAD.2014.6987592

SAT-based methods for circuit synthesis

Roderick Paul Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing

Institute of Applied Information Processing and Communications (7050)

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

Abstract

Reactive synthesis supports designers by automatically constructing correct hardware from declarative specifications. Synthesis algorithms usually compute a strategy, and then construct a circuit that implements it. In this work, we study SAT- and QBF-based methods for the second step, i.e., computing circuits from strategies. This includes methods based on QBF-certification, interpolation, and computational learning. We present optimizations, efficient implementations, and experimental results for synthesis from safety specifications, where we outperform BDDs both regarding execution time and circuit size

Original language	English
Title of host publication	Formal Methods in Computer-Aided Design
Publisher	Institute of Electrical and Electronics Engineers
Pages	31-34
ISBN (Print)	978-0-9835678-4-4
DOIs	https://doi.org/10.1109/FMCAD.2014.6987592
Publication status	Published - 2014
Event	International Conference on Formal Methods in Computer-Aided Design - Lausanne, Switzerland Duration: 21 Oct 2014 → 24 Oct 2014

Conference

Conference	International Conference on Formal Methods in Computer-Aided Design
Country/Territory	Switzerland
City	Lausanne
Period	21/10/14 → 24/10/14

Fields of Expertise

Information, Communication & Computing

Treatment code (Nähere Zuordnung)

Application

Access to Document

10.1109/FMCAD.2014.6987592

extended.pdfAccepted author manuscript, 486 KB

EU - STANCE - A Source code analysis Toolbox for software security AssuraNCE
Tögl, R., Könighofer, R. & Bloem, R.
1/10/12 → 30/09/15
Project: Research project
FWF - QUAINT - Quantified Decision Procedures and Interpolation for Error Correction
Hofferek, G., Könighofer, R. & Bloem, R.
1/01/12 → 30/09/15
Project: Research project
FWF - RiSE - Rigorous Systems Engineering
Könighofer, R., Khalimov, A., Bloem, R., Könighofer, B. & Jacobs, S.
1/03/11 → 31/08/19
Project: Research project

Cite this

@inproceedings{bb84d979e17841ad8e1837bce62ba5bb,

title = "SAT-based methods for circuit synthesis",

abstract = "Reactive synthesis supports designers by automatically constructing correct hardware from declarative specifications. Synthesis algorithms usually compute a strategy, and then construct a circuit that implements it. In this work, we study SAT- and QBF-based methods for the second step, i.e., computing circuits from strategies. This includes methods based on QBF-certification, interpolation, and computational learning. We present optimizations, efficient implementations, and experimental results for synthesis from safety specifications, where we outperform BDDs both regarding execution time and circuit size",

author = "Bloem, {Roderick Paul} and Uwe Egly and Patrick Klampfl and Robert K{\"o}nighofer and Florian Lonsing",

year = "2014",

doi = "10.1109/FMCAD.2014.6987592",

language = "English",

isbn = "978-0-9835678-4-4",

pages = "31--34",

booktitle = "Formal Methods in Computer-Aided Design",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

note = "International Conference on Formal Methods in Computer-Aided Design ; Conference date: 21-10-2014 Through 24-10-2014",

}

TY - GEN

T1 - SAT-based methods for circuit synthesis

AU - Bloem, Roderick Paul

AU - Egly, Uwe

AU - Klampfl, Patrick

AU - Könighofer, Robert

AU - Lonsing, Florian

PY - 2014

Y1 - 2014

N2 - Reactive synthesis supports designers by automatically constructing correct hardware from declarative specifications. Synthesis algorithms usually compute a strategy, and then construct a circuit that implements it. In this work, we study SAT- and QBF-based methods for the second step, i.e., computing circuits from strategies. This includes methods based on QBF-certification, interpolation, and computational learning. We present optimizations, efficient implementations, and experimental results for synthesis from safety specifications, where we outperform BDDs both regarding execution time and circuit size

AB - Reactive synthesis supports designers by automatically constructing correct hardware from declarative specifications. Synthesis algorithms usually compute a strategy, and then construct a circuit that implements it. In this work, we study SAT- and QBF-based methods for the second step, i.e., computing circuits from strategies. This includes methods based on QBF-certification, interpolation, and computational learning. We present optimizations, efficient implementations, and experimental results for synthesis from safety specifications, where we outperform BDDs both regarding execution time and circuit size

U2 - 10.1109/FMCAD.2014.6987592

DO - 10.1109/FMCAD.2014.6987592

M3 - Conference paper

SN - 978-0-9835678-4-4

SP - 31

EP - 34

BT - Formal Methods in Computer-Aided Design

PB - Institute of Electrical and Electronics Engineers

T2 - International Conference on Formal Methods in Computer-Aided Design

Y2 - 21 October 2014 through 24 October 2014

ER -

SAT-based methods for circuit synthesis

Abstract

Conference

Fields of Expertise

Treatment code (Nähere Zuordnung)

Access to Document

Fingerprint

Projects

EU - STANCE - A Source code analysis Toolbox for software security AssuraNCE

FWF - QUAINT - Quantified Decision Procedures and Interpolation for Error Correction

FWF - RiSE - Rigorous Systems Engineering

Cite this