| 摘要 |
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.
|
