Method and apparatus for structural input/output matching for design verification

Abstract

In the design of digital integrated circuits, it is often desirable to formally verify whether an implementation design is equivalent to a reference design. The present invention facilitates such formal verification by determining “necessary correspondences” between inputs or outputs of the two circuits to be compared for equivalency. Necessary correspondences are so called because while they establish necessary conditions for equivalency to occur, they are not sufficient to determine that equivalency actually exists. Once such necessary correspondences have been determined, algorithms to determine actual equivalency can be more strategically applied. It is often cost-effective (i.e. more efficient), as part of an equivalency-determining circuit design tool, to first apply the teachings of the present invention in order to lessen subsequent application of an equivalency determining method. The present invention finds necessary correspondences between the combinational portions of two circuits by utilizing a graph-coloring algorithmic approach applied to a simplified bipartite representation. The bipartite representation is determined for each circuit to be compared. Each bipartite representation is comprised of a left set of nodes (representing inputs), a right set of nodes (representing outputs) and a set of edges which connect the nodes of the left and right sets. The bipartite representation is “primed” by coloring the nodes of each circuits' left and right sets on the basis of information known about the circuits. The basic cycle by which the invention operates comprises the performance of a recoloring procedure followed by the performance of consistency and progress checks. The consistency and progress checks analyze the results of the recolorings to identify necessary correspondences and to determine whether further searching for additional necessary correspondences should be performed.