SAT-based techniques in system synthesis

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.