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:
(GF p1 & ... & GF pm) -> (GF
q1 &
... & GF 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.
See also synthesis homepage and Anzu, another tool implementing our approach.