KIT | KIT-Bibliothek | Impressum | Datenschutz
Open Access Logo

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

Hoffmann, Dirk W.; Kropf, Thomas

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

Zugehörige Institution(en) am KIT Institut für Rechnerentwurf und Fehlertoleranz (IRF)
Publikationstyp Forschungsbericht
Jahr 1999
Sprache Englisch
Identifikator ISSN: 1432-7864
URN: urn:nbn:de:swb:90-AAA96998
KITopen-ID: 9699
Verlag Karlsruhe
Serie Interner Bericht. Fakultät für Informatik, Universität Karlsruhe ; 1999,6
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page