A verification algorithm for logic circuits with internal variables
T. Nakaoka, Shin’ichi Wakabayashi, Tetsushi Koide, N. Yoshida · 2002
In this paper, we present a formal verification method based on internal variables of a given circuit. In this method, the problem of deciding the logical equivalence of two logic circuits is transformed to the satisfiability problem, which is solved by constructing a set of BDDs, each of which is corresponding to an internal variable of the circuit. Experimental results showed the effectiveness of the proposed method.