A Cofactor Based Logic Coverage Equivalence Checking Algorithm for Combinational Circuits

Coverage equivalence checking of combinational circuits means to check whether two circuits with different expansions implement the same function.By expending the conception of cofactor,a logic coverage equivalence checking algorithm for combinational circuits is proposed which is based on decomposition and tautology determination of product term’s cofactors.Equivalence checking problem is firstly decomposed into two containment checking sub-problems.Cofactors of one circuit to each product term of the other circuit are calculated one by one,and then tautology checking is executed on each of these cofactors by developing their Shannon diagrams.Based on results of tautology checking,it will be finally deduced whether the two circuits are coverage equivalent.During calculation of product term’s cofactors,decomposition and order reduction of the logic functions are implemented which lead to speedup of the equivalence checking.Experimental results show that the proposed algorithm is stable and effective.And,data on MCNC Benchmark couples optimized by the three algorithms embodied in EXPRESSO indicated that the proposed algorithm has an obvious speed advantage over the other two equivalence checking algorithms which are based on truth table and BDD,respectively.