Automatic error correction of large circuits using boolean decomposition and abstraction

摘要

Boolean equivalence checking has turned out to be a powerful method for verifying compbinatorial 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 producted 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.