Optimization
Equivalence checking
The proof that a rewrite still does the same thing, and when it cannot be produced.
Anything can be made smaller by making it wrong. The equivalence check is what stops that: the original and the rewrite are compared as logic, and the run has to show they cannot be told apart before a win is reported.
How the check works
The two versions are synthesised and wired together so their outputs are compared for every possible input; then the tool tries to find any input that makes them differ. Failing to find one, exhaustively, is a proof. Finding one is a counterexample, and it is shown to you.
The original side always comes from the untouched copy of your project, resolved from the source list recorded when the baseline was taken. It is never taken from anything the run nominates for itself; a reference the run could choose is a reference it could game.
Three ways it can be settled
| Method | What it establishes |
|---|---|
| Combinational | For designs with no state: the outputs are identical for every input. A complete proof. |
| Temporal induction | For sequential designs: equivalence for any number of cycles, without a bound. Tried first, and it does not always converge. |
| Bounded | Equivalence for the first N cycles. Strong evidence, and not a proof for all time. N is reported with the result. |
Note
Induction failing to settle is not a counterexample. Induction reasons from states the design may never actually reach, so a failed step means the argument did not close, not that a difference was found. When that happens the run falls through to the bounded check, and only the bounded check is allowed to report a design as not equivalent.
The verdicts
| Verdict | What it means for you |
|---|---|
| Equivalent | The rewrite behaves identically. Check whether the result is marked bounded; a bounded result is a strong check over a window rather than a proof for all time. |
| Not equivalent | A difference was found, and the counterexample is shown. The rewrite is not safe to apply as it stands. |
| Inconclusive | The check could not settle it, usually because the design is too large or too deeply stateful. This is not a pass and is never presented as one. |
| Not applicable | The change deliberately alters cycle-by-cycle behaviour, so a cycle-accurate comparison cannot judge it. See below. |
| Unavailable | The tooling needed for the check was not present on this deployment. |
Changes a proof cannot judge
Some correct and valuable optimizations change when things happen rather than what happens. Adding a pipeline stage to break a long path is the classic one; re-encoding a state machine is another. A cycle-accurate comparison will call these different, because they are.
When a rewrite does that, it is declared as a timing change, the equivalence result comes back as not applicable, and the run falls back to simulation to support it. That is labelled clearly and is never counted as a proof. A rewrite in this category deserves more of your attention than a proved one, not less.
Heads up
This declaration exists for changes that genuinely alter timing. It is not an escape hatch for a proof that failed for some other reason; using it that way would turn a caught bug into a labelled unknown, which is worse than the bug.
Where you see it
The proposal card carries an equivalence proved or behaviour unproved badge, and the full result with its method and bound sits in the optimization panel. The badge only reflects a proof that ran after the last edit; a proof from before the final change says nothing about that change.