Patent ID: 8484591

Claim:
A method, in a data processing system, for simplifying a netlist before computational resources are exceeded, the method comprising: receiving, by a processor, input that identifies a netlist to be validated and at least one of a set of equivalences or a set of equivalence classes; building, by the processor, a proof graph without any edges and with at least two of a node for each equivalence in a set of equivalences at least two of a node for each equivalence class in a set of equivalence classes; performing, by the processor, 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 suspected equivalence of the set of suspected equivalences in the proof graph of the netlist: determining, by the processor, whether the suspected 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, recording, by the processor, a proof dependency as an edge in the proof graph; and for each node in the proof graph; determining, by the processor, whether the node has a falsified dependency; responsive to the node failing to have a falsified dependency, identifying, by the processor, that all dependencies for the node are satisfied and that the equivalences represented by the node in the proof graph are sequential equivalences; and simplifying, by the processor, the netlist by consuming the sequential equivalences.