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)
DOI: 10.1109/DATE.2003.1253784
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.
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