## 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 *N*^{3}. 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** p_{1} /\ ... /\
**G F** p_{m}) -> (**G F** q_{1} /\
... /\ **G F** q_{n})

For this class of formulas, we present an N^{3}-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.