1999 | OriginalPaper | Chapter
Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction
Authors : Dirk W. Hoffmann, Thomas Kropf
Published in: Correct Hardware Design and Verification Methods
Publisher: Springer Berlin Heidelberg
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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. Thus, it allows the detection of arbitrary design errors. Since our method is not structure-based, the pro]duced results are independent of any structural similarities between the implementation circuit and its specification. It can even be applied if the specification is given, e.g., as a propositional formula, a BDD, or in form of a truth table.Furthermore, we discuss two kinds of circuit abstractions and prove compatibility with our rectification method. In combination with abstractions, we show that our method can be used to rectify large circuits.We have implemented our approach in the AC/3 equivalence checker and circuit rectifier and evaluated it with the Berkeley benchmark circuits [6] and the ISCAS85 benchmarks [7] to show its practical strength.