Optimize mode

It is worth being precise about this, because it shapes everything else. A synthesis tool does not optimize Verilog; it optimizes the netlist it builds from your Verilog. Running one and handing you its output would give you a flattened wall of gates, locked to one target and impossible to maintain; that would be a worse outcome than changing nothing at all.

So the rewriting is done at the source level, the way an engineer would do it. Yosys is used for two other jobs instead:

The transformations that pay off in RTL are unglamorous and quite predictable. Roughly in order of how often they help:

• Sharing an expensive operator across branches that can never happen at the same time: one adder and a multiplexer instead of three adders.
• Turning a priority chain of if / else if into a parallel case where the conditions really are mutually exclusive. This is the big one for logic depth.
• Removing pipeline or holding registers that no longer feed anything.
• Narrowing counters, accumulators and datapaths that are wider than their range can ever need.
• Strength reduction: a constant multiply becomes shifts and adds, division and modulo by a power of two become a shift and a mask.
• Folding constants and dropping logic that the parameters make dead but the synthesiser cannot see through.
• Rebalancing a deep adder or comparator chain into a tree when depth is what you asked to reduce.

The obvious way to make a design smaller is to make it do less. That risk is handled mechanically, not by asking nicely.

• The interface never changes. Port names, widths and directions stay exactly as they are; everything that instantiates the module depends on them, and the equivalence check cannot even run once they differ.
• No check, assertion or test is removed or weakened. The change set is scanned for this independently of what the run reports.
• The testbench is not edited. It is the measuring instrument; if it needs to change, the rewrite is not behaviour-preserving.
• No vendor primitives are hand-instantiated unless you asked for them. Trading portability for a number is your decision, not the run's.
• Nothing unrelated is reformatted or renamed. Every extra diff line is a line you have to review.

1. 1

   From an existing chat

   Once a chat has produced code, an Optimize toggle appears next to the composer. It carries the module across for you and keeps the conversation going, so the run knows what the design is meant to do.

2. 2

   From a cold start

   Pick the Optimize tab on the New chat screen and upload the project as a zip. Include the testbench if you have one; it is not required for the proof, and it is what makes a fallback possible when the proof cannot be run.

Like Debug mode, the work happens in a throwaway copy of your project and the result is a proposal. You read the diff, look at the numbers, and decide. See Applying a proposed fix; the same card and the same apply behaviour are used, with wording that reflects that this is a choice rather than a repair.