Synthesis of reactive(1) designs

Abstract

We consider the problem of synthesizing digital designs from their LTL specification. In spite of the theoretical double exponential lower bound for the general case, we show that for many expressive specifications of hardware designs the problem can be solved in time N3, where N is the size of the state space of the design. We describe the context of the problem, as part of the Prosyd European Project which aims to provide a property-based development flow for hardware designs. Within this project, synthesis plays an important role, first in order to check whether a given specification is realizable, and then for synthesizing part of the developed system. The class of LTL formulas considered is that of Generalized Reactivity(1) (generalized Streett(1)) formulas, i.e., formulas of the form: (□ ◇ p 1∧⋯∧□ ◇pm) →(□ ◇ q1 ∧⋯∧ □◇qn) where each p i qi is a boolean combination of atomic propositions. We also consider the more general case in which each pi, qi is an arbitrary past LTL formula over atomic propositions. For this class of formulas, we present an N3-time algorithm which checks whether such a formula is realizable, i.e., there exists a circuit which satisfies the formula under any set of inputs provided by the environment. In the case that the specification is realizable, the algorithm proceeds to construct an automaton which represents one of the possible implementing circuits. The automaton is computed and presented symbolically. © Springer-Verlag Berlin Heidelberg 2006.