Efficient Equivalence Checking Using Output Grouping and Circuit SAT Solver

A new combinational equivalence checking technique using Circuit SAT is proposed in the paper.By the algorithm,a heuristic is used to do output grouping for complex problem first,then the equivalence checking problem is converted into some Circuit SAT problems.To reduce the search space,useful learned information of some sub-problem is shared.Experimental results show the efficiency of the proposed algorithm.