Method and system for formal verification of a circuit model using binary decision diagrams

摘要

The present invention provides a method and system for comparing a pair of circuit models without the need for performing a false negative check when cut-points are introduced. An exemplary method includes generating a BDD for each of a plurality of signals of each circuit model from an initial cut-point frontier towards an output of each circuit model until a BDD of one of the plurality of signals reaches a predetermined maximum size, selecting a new cut-point signal frontier, and generating a normalized function for each cut-point signal on the new cut-point frontier of each circuit model.