Method for determining functional equivalence between design models

摘要

The present invention determines whether two design files have identical functionality by attempting to create a binary decision diagram (BDD) for corresponding verification output pairs(302). When the BDD creations are not successful for all evaluated output pairs a set of cutpoint pair candidates are identified(303). An automatic test program generator (ATPG) is used to determine whether or not the cutpoint pair candidates are invalid cutpoints(304). The invalid cutpoints are removed from the set of cutpoint pair candidates(305). A cutpoint pair candidate having known support is selected(306). An exclusive-or of the outputs of the selected candidate is formed (307). A BDD for the resulting XOR function is attempted (308). If a BDD having a zero or one value is built then the selected candidate is valid indicating equivalence (310). If the BDD is neither the zero function nor the one function, the cutpoint pair is invalid if all of its inputs are verification inputs (311). If one or more of the inputs are cutpoint variable inputs, the function for a cutpoint variable input is substituted (309), and the flow continues to build a new BDD for the evaluation XOR having the substituted function.