Abstract


We consider the problem of synthesizing digital designs from their LTL specification. In spite of the theoretical double exponential lower bound, we show that for many expressive specifications of hardware designs the problem can be solved in time N3. 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:

(G F p1   /\   ...   /\   G F pm) -> (G F q1   /\   ...   /\   G F qn)

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.