EVBCS: new equivalence verification algorithm based on OBDD and circuit structure

In this paper, an algorithm, EVBCS, for formal verification of combinational logic circuits, is proposed. It combines BDD and structure isomorphism techniques. It also uses a heuristic method to select a set of internal signals (cutline) to reduce the size of BDDs to be created. The algorithm is demonstrated on ISCAS'85 benchmarks using synthesis and optimization tools. The experiment results show that the algorithm is very effective for circuits with structure similarities which are often created by using local synthesis tools and local optimization tools.