Using BDD-based decomposition for automatic error correction of combinatorial circuits

Boolean equivalence checking has turned out to be a powerful
method for verifying combinatorial circuits and has been widely
accepted both in academia and industry.
In this paper, we present a method for localizing and correcting
errors in combinatorial circuits for which equivalence checking
has failed. Our approach is general and does not assume any
error model. Working directly on BDDs, the approach is well
suited for integration into commonly used equivalence checkers.
Since circuits can be corrected fully automatically, our
approach can save considerable debugging time and therefore
will speed up the whole design cycle.
We have implemented a prototype verification tool and evaluated
our method with the Berkeley benchmark circuits. In addition, we
have applied it successfully to a real life example taken from
[DrFe96].