2013/08/22 by Georg Hofferek, Hofferek, Georg, Ashutosh Gupta +7
Computer Science · Engineering · #Advanced Control Systems Optimization #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Machine Learning and Algorithms #VLSI and Analog Circuit Testing
paper · pdf · doi:10.48550/arxiv.1308.4767
openalex publication_date 2013/08/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
It is often difficult to correctly implement a Boolean controller for a\ncomplex system, especially when concurrency is involved. Yet, it may be easy to\nformally specify a controller. For instance, for a pipelined processor it\nsuffices to state that the visible behavior of the pipelined system should be\nidentical to a non-pipelined reference system (Burch-Dill paradigm). We present\na novel procedure to efficiently synthesize multiple Boolean control signals\nfrom a specification given as a quantified first-order formula (with a specific\nquantifier structure). Our approach uses uninterpreted functions to abstract\ndetails of the design. We construct an unsatisfiable SMT formula from the given\nspecification. Then, from just one proof of unsatisfiability, we use a variant\nof Craig interpolation to compute multiple coordinated interpolants that\nimplement the Boolean control signals. Our method avoids iterative learning and\nback-substitution of the control functions. We applied our approach to\nsynthesize a controller for a simple two-stage pipelined processor, and present\nfirst experimental results.\n