Synthesis of reactive (1) designs
N Piterman, A Pnueli, Y Sa'ar - … 2006, Charleston, SC, USA, January 8-10 …, 2006 - Springer
N Piterman, A Pnueli, Y Sa'ar
Verification, Model Checking, and Abstract Interpretation: 7th International …, 2006•SpringerWe 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 N 3, 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 …
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 N 3, 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 …
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 N 3, 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.
Springer