Automatic error correction of large circuits using Boolean decomposition and abstraction

Abstract

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 produced 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.