Suraq - a controller synthesis tool using uninterpreted functions Conference Paper

Author(s): Hofferek, Georg; Gupta, Ashutosh K
Title: Suraq - a controller synthesis tool using uninterpreted functions
Title Series: LNCS
Affiliation IST Austria
Abstract: Boolean controllers for systems with complex datapaths are often very difficult to implement correctly, in particular when concurrency is involved. Yet, in many instances it is easy to formally specify correctness. For example, the specification for the controller of a pipelined processor only has to state that the pipelined processor gives the same results as a non-pipelined reference design. This makes such controllers a good target for automated synthesis. However, an efficient abstraction for the complex datapath elements is needed, as a bit-precise description is often infeasible. We present Suraq, the first controller synthesis tool which uses uninterpreted functions for the abstraction. Quantified firstorder formulas (with specific quantifier structure) serve as the specification language from which Suraq synthesizes Boolean controllers. Suraq transforms the specification into an unsatisfiable SMT formula, and uses Craig interpolation to compute its results. Using Suraq, we were able to synthesize a controller (consisting of two Boolean signals) for a five-stage pipelined DLX processor in roughly one hour and 15 minutes.
Keywords: verification; craig interpolation; Controller synthesis; Abstracting; Concurrency control; Pipeline processing systems; Software testing; Specification languages; Specifications; Automated synthesis; Data paths; First-order formulas; Pipelined processor; Reference designs; Uninterpreted Functions; Controllers
Conference Title: HVC: Haifa Verification Conference
Volume: 8855
Conference Dates: November 18-20, 2014
Conference Location: Haifa, Israel
ISBN: 0302-9743
Publisher: Springer  
Date Published: 2014-01-01
Start Page: 68
End Page: 74
Sponsor: The work presented in this paper was supported in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM) and the Austrian Science Fund (FWF) through projects RiSE (S11406-N23) and QUAINT (I774-N23)
DOI: 10.1007/978-3-319-13338-6_6
Open access: no
IST Austria Authors
  1. Ashutosh Gupta
    16 Gupta
Related IST Austria Work