SAT-based techniques in system synthesis

Beitrag bei einer Tagung

Details zur Publikation

Autor(en): Haubelt C, Teich J, Feldmann R, Monien B
Jahr der Veröffentlichung: 2003
Tagungsband: Proceedings of Design, Automation and Test in Europe (DATE 2003)
Seitenbereich: 1168-1169


SAT-based verification of electronic systems has become very popular in recent years. In this paper, we show that SAT-techniques are also applicable and helpful during the synthesis and the optimization of a system. Therefore, we must consider two questions: (i) how to represent specifications; and (ii) how to quantify properties of embedded systems by boolean formulas. Thus, we reduce the well known binding problem to the Boolean satisfiability problem. Next, we show how to quantify the degree of fault tolerance of a system using quantified Boolean formulas (QBFs). These problems correspond to typical subroutines often used during design space exploration. We show by experiment that problem instances of reasonable size are easily solved by the QBF solver QSOLVE. © 2003 IEEE.

FAU-Autoren / FAU-Herausgeber

Haubelt, Christian Prof. Dr.-Ing.
Technische Fakultät
Teich, Jürgen Prof. Dr.-Ing.
Lehrstuhl für Informatik 12 (Hardware-Software-Co-Design)

Autor(en) der externen Einrichtung(en)
Universität Paderborn


Haubelt, C., Teich, J., Feldmann, R., & Monien, B. (2003). SAT-based techniques in system synthesis. In Proceedings of Design, Automation and Test in Europe (DATE 2003) (pp. 1168-1169). Munich, DE.

Haubelt, Christian, et al. "SAT-based techniques in system synthesis." Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, DATE 2003, Munich 2003. 1168-1169.


Zuletzt aktualisiert 2018-03-11 um 13:50