SAT-based techniques in system synthesis

Haubelt C, Teich J, Feldmann R, Monien B (2003)

Publication Status: Published

Publication Type: Conference contribution, Conference Contribution

Publication year: 2003

Pages Range: 1168-1169

Article Number: 1253784

Conference Proceedings Title: Proceedings of Design, Automation and Test in Europe (DATE 2003)

Event location: Munich DE

DOI: 10.1109/DATE.2003.1253784

Abstract

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.

Authors with CRIS profile

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

Involved external institutions

Universität Paderborn DE Germany (DE)

How to cite

APA:

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.

MLA:

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.

BibTeX: Download