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.
What the check establishes
The rewrite is compared against your original as logic rather than as text. Either the two cannot be told apart by any input, in which case you have a proof, or a case exists where they differ, in which case that case is shown to you and the rewrite is not safe to apply.
The side it compares against is always your original design, exactly as you supplied it. It is never anything produced during the run; a reference a run could nominate for itself is a reference it could game.
Proved, and proved how far
For a design with no state, a proof covers every input and there is nothing more to say. For a design with state, a check can sometimes be settled for all time and sometimes only for a window of cycles. The panel is explicit about which one you got:
- Behaviour unchanged, with nothing after it, means the check settled without a bound.
- Behaviour unchanged — bounded to N cycles means the two designs agree for the first N cycles of operation. That is strong evidence rather than a proof for all time, and the number is there so you can judge it.
Note
A check that runs out of room is never reported as a pass. If the question could not be settled, the panel says so and the result is presented as unverified; see the verdicts below.
The verdicts
| Verdict | What it means for you |
|---|---|
| Behaviour unchanged | The rewrite cannot be told apart from your original. Check whether it is marked bounded; a bounded result covers a window of cycles rather than all time. |
| Behaviour CHANGED | A case was found where the two differ, and it is shown to you. The rewrite is not safe to apply as it stands. |
| Could not be proved | The question could not be settled, usually because the design is large or deeply stateful. This is not a pass and is never presented as one. |
| Not provable for this change | The change deliberately alters cycle-by-cycle behaviour, so a cycle-accurate comparison cannot judge it. See below. |
| Checker unavailable | The check could not be run here at all. |
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 result comes back as not provable for this change, and simulation is used to support it instead. 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.