Previous results show that both flat and hierarchical methodologies present obstacles to effectively completing combinational equivalence checking. A new approach that combines the benefits while effectively dealing with the pitfalls of both styles of equivalence checking is presented.

An important step in using combinational equivalence checkers to verify sequential designs is identifying and matching corresponding compare-points in the two sequential designs to be verified. Both non-function and function-based matching methods are usually employed in commercial verification tools. In this paper, we describe a heuristic algorithm using ATPG for matching comparepoints based on the functionality of the combinational blocks in the sequential designs. Results on industrial-sized circuits show our methods are both practical and efficient.