Patent ID: 8413091

Claim:
A computer program product comprising a non-transitory computer readable storage medium having a computer readable program stored therein, wherein the computer readable program, when executed on a computing device, causes the computing device to: receive input that identifies a netlist to be validated and at least one of a set of equivalences or a set of equivalence classes; build a proof graph without any edges and with at least two of a node for each equivalence in a set of equivalences or at least two of a node for each equivalence class in a set of equivalence classes; perform speculative reduction on an unrolled version of the netlist, wherein the speculative reduction asserts a set of suspected equivalences in the set of equivalences or in the set of equivalence classes; for each of the set of suspected equivalences in the proof graph of the netlist: determine whether equivalence holds for at least one of the equivalence or the equivalence class by identifying whether the equivalence or equivalence class is either affecting of a second equivalence or a second equivalence class or non-affecting of the second equivalence or the second equivalence class; and responsive to the equivalence or equivalence class being affecting of the second equivalence or the second equivalence class, record a proof dependency as an edge in the proof graph; and for each node in the proof graph: determine whether the node has a falsified dependency; responsive to the node failing to have a falsified dependency, identify that all dependencies are satisfied and that the equivalences represented by the node in the proof graph are sequential equivalences; and simplify the netlist by consuming the sequential equivalences.