conference paper published yes Georg Hofferek author Ashutosh Gupta author 335E5684-F248-11E8-B48F-1D18A9856A87 Bettina Könighofer author Jie Jiang author Roderick Bloem author ToHe department FMCAD: Formal Methods in Computer-Aided Design Rigorous Systems Engineering project Quantitative Reactive Modeling project It is often difficult to correctly implement a Boolean controller for a complex system, especially when concurrency is involved. Yet, it may be easy to formally specify a controller. For instance, for a pipelined processor it suffices to state that the visible behavior of the pipelined system should be identical to a non-pipelined reference system (Burch-Dill paradigm). We present a novel procedure to efficiently synthesize multiple Boolean control signals from a specification given as a quantified first-order formula (with a specific quantifier structure). Our approach uses uninterpreted functions to abstract details of the design. We construct an unsatisfiable SMT formula from the given specification. Then, from just one proof of unsatisfiability, we use a variant of Craig interpolation to compute multiple coordinated interpolants that implement the Boolean control signals. Our method avoids iterative learning and back-substitution of the control functions. We applied our approach to synthesize a controller for a simple two-stage pipelined processor, and present first experimental results. IEEE2013Portland, OR, United States eng 1308.476710.1109/FMCAD.2013.6679394 77 - 84 Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. Synthesizing multiple boolean functions using interpolation on a single proof. In: <i>2013 Formal Methods in Computer-Aided Design</i>. IEEE; 2013:77-84. doi:<a href="https://doi.org/10.1109/FMCAD.2013.6679394">10.1109/FMCAD.2013.6679394</a> G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, R. Bloem, in:, 2013 Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 77–84. G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, and R. Bloem, “Synthesizing multiple boolean functions using interpolation on a single proof,” in <i>2013 Formal Methods in Computer-Aided Design</i>, Portland, OR, United States, 2013, pp. 77–84. Hofferek, Georg, Ashutosh Gupta, Bettina Könighofer, Jie Jiang, and Roderick Bloem. “Synthesizing Multiple Boolean Functions Using Interpolation on a Single Proof.” In <i>2013 Formal Methods in Computer-Aided Design</i>, 77–84. IEEE, 2013. <a href="https://doi.org/10.1109/FMCAD.2013.6679394">https://doi.org/10.1109/FMCAD.2013.6679394</a>. Hofferek, Georg, et al. “Synthesizing Multiple Boolean Functions Using Interpolation on a Single Proof.” <i>2013 Formal Methods in Computer-Aided Design</i>, IEEE, 2013, pp. 77–84, doi:<a href="https://doi.org/10.1109/FMCAD.2013.6679394">10.1109/FMCAD.2013.6679394</a>. Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. 2013. Synthesizing multiple boolean functions using interpolation on a single proof. 2013 Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 77–84. Hofferek, G., Gupta, A., Könighofer, B., Jiang, J., &#38; Bloem, R. (2013). Synthesizing multiple boolean functions using interpolation on a single proof. In <i>2013 Formal Methods in Computer-Aided Design</i> (pp. 77–84). Portland, OR, United States: IEEE. <a href="https://doi.org/10.1109/FMCAD.2013.6679394">https://doi.org/10.1109/FMCAD.2013.6679394</a> 13852018-12-11T11:51:43Z2024-10-21T06:02:56Z