Synthesizing multiple boolean functions using interpolation on a single proof Conference Paper


Author(s): Hofferek, Georg; Gupta, Ashutosh K; Könighofer, Bettina; Jiang, Jie-Hong R; Bloem, Roderick
Title: Synthesizing multiple boolean functions using interpolation on a single proof
Affiliation IST Austria
Abstract: 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.
Keywords: craig interpolation; First-order formulas; Pipelined processor; Uninterpreted Functions; Back substitutions; Iterative learning; Pipelined systems; Reference systems
Conference Title: FMCAD: Formal Methods in Computer-Aided Design
Volume: Article number: 6679394
Conference Dates: October 20 - 23, 2013
Conference Location: Portland, OR, USA
Publisher: Springer  
Date Published: 2013-01-01
Start Page: 77
End Page: 84
URL:
Notes: This research was supported by the European Commission through project DIAMOND (FP7-2009-IST-4-248613), the Austrian Science Fund (FWF) through projects RiSE (S11406-N23) and QUAINT (I774-N23), and ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).
Open access: yes (repository)
IST Austria Authors
  1. Ashutosh Gupta
    16 Gupta