Patent ID: 7159201

Claim:
A method comprising: using a divide-and-conquer approach to formal equivalence verification, the divide-and-conquer approach including building normalized binary decision diagrams (BDDs); determining that a specification circuit model and an implementation circuit model are inequivalent based on the normalized BDDs; and generating a counter-example for the inequivalent models, wherein generating the counter-example comprises: determining values of a first set of variables that cause binary decision diagrams for the models to be inequivalent; while the first set of variables includes eigenvariables, selecting an eigenvariable; substituting the determined values into a binary decision diagram associated with a node associated with the selected eigenvariable; substituting the determined values into a normalized binary decision diagram associated with a node associated with the selected eigenvariable; identifying values of a second set of variables that cause the binary decision diagram and normalized binary decision diagram into which the determined values were substituted to be equal; and returning the identified values for the first and second sets of variables.