US 8,413,091 B2Granted

Enhancing redundancy removal with early merging

AssigneeInternational Business Machines Corporation

InventorsJason R. Baumgartner, Michael L. Case, Robert L. Kanzelman, Hari Mony

Life of this patent

Estimating the term…

Loading patent…

Abstract

A mechanism is provided for simplifying a netlist before computational resources are exceeded. For each of a set of suspected equivalences in a proof graph of a netlist, a determination is made as to whether equivalence holds for at least one of an equivalence or an equivalence class by identifying whether the equivalence or equivalence class is either affecting or non-affecting. Responsive to the equivalence or equivalence class being affecting, a proof dependency is recorded as an edge in a proof graph. For each node in the proof graph, a determination is made as to whether the node has a falsified dependency. Responsive to the node failing to have a falsified dependency, identification is made that all dependencies are satisfied and that the equivalences represented by the node in the proof graph are sequential equivalences. The netlist is then simplified by consuming the sequential equivalences.

Claims10

Dependent claims

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.

10 more elements

An apparatus, comprising:

a processor;
and
a memory coupled to the processor, wherein the memory comprises instructions which, when executed by the processor, cause the processor 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.

13 more elements

Dependencies are inferred from the claim text.