Equivalence checking of partial designs using dependency quantified Boolean formulae

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 q...

Full description

Saved in:
Bibliographic Details
Main Authors: Gitina, Karina, Reimer, Sven, Sauer, Matthias, Wimmer, Ralf, Scholl, Christoph, Becker, Bernd
Format: Conference Proceeding
Language:English
Subjects:
Algorithm design and analysis
Approximation algorithms
Approximation methods
Combinational circuits
Complexity theory
Logic gates
System analysis and design
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1063-6404
2576-6996
DOI:10.1109/ICCD.2013.6657071