@inProceedings{ gitina-et-al-iccd-2013,
author = "Karina Gitina and Sven Reimer and Matthias Sauer
and Ralf Wimmer and Christoph Scholl and Bernd Becker",
title = "Equivalence Checking of Partial Designs Using Dependency
Quantified Boolean Formulae",
year = "2013",
month = oct,
booktitle = "Proceedings of the 31\textsuperscript{st} IEEE International
Conference on Computer Design",
address = "Asheville, NC, USA",
publisher = "IEEE Computer Society Press",
abstract = "We consider the partial equivalence checking problem (PEC), i. e.,
checking whether a given partial implementation of a combinational
circuit can (still) be extended to a complete design that is
equivalent to a given full specification. To solve PEC, we give a
linear transformation from PEC to the question whether a dependency
quantified Boolean formula (DQBF) is satisfied.
Our novel algorithm to solve DQBF based on quantifier elimination can
therefore be applied to solve PEC. We also present first experimental
results showing the feasibility of our approach and the inaccuracy of
QBF approximations, which are usually used for deciding the PEC so far.",
pages = "396--403",
isbn = "978-1-4799-2987-0",
doi = "http://dx.doi.org/10.1109/ICCD.2013.6657071",
}