2014 | OriginalPaper | Buchkapitel
Suraq — A Controller Synthesis Tool Using Uninterpreted Functions
verfasst von : Georg Hofferek, Ashutosh Gupta
Erschienen in: Hardware and Software: Verification and Testing
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 first-order 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.