KIT | KIT-Bibliothek | Impressum | Datenschutz

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

Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Rechnerentwurf und Fehlertoleranz (IRF)
Publikationstyp Forschungsbericht/Preprint
Publikationsjahr 1999
Sprache Englisch
Identifikator ISSN: 1432-7864
KITopen-ID: 9699
Verlag Universität Karlsruhe (TH)
Serie Interner Bericht. Fakultät für Informatik, Universität Karlsruhe ; 1999,6
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page