@InCollection{wimmer-et-al-synthesisBook-2017,
author = "Ralf Wimmer and Karina Wimmer and Christoph Scholl and Bernd Becker",
publisher = "Springer",
editor = "Andr{\'e} Ignacio Reis and Rolf Drechsler",
booktitle = "Advanced Logic Synthesis",
year = "2017",
isbn = "978-3-319-67294-6",
pages = "151--168",
doi = "10.1007/978-3-319-67295-3_7",
title = "Analysis of Incomplete Circuits using Dependency Quantified {Boolean} Formulas",
abstract = "We consider Dependency Quantified Boolean Formulas (DQBFs), a generalization
of Quantified Boolean Formulas (QBFs), and demonstrate that DQBFs are a natural
calculus to exactly express the realizability problem of incomplete
combinational and sequential circuits with an arbitrary number of
(combinational or bounded-memory) black boxes.
In contrast to usual approaches for controller synthesis, restrictions to
the interfaces of missing circuit parts in distributed architectures are
strictly taken into account. We present a solution method for DQBFs
together with the extraction of Skolem functions for existential variables,
which can directly serve as implementations for the black boxes. First
experimental results are provided.",
}