Properly specify and reimplement opt_clean/clean

[nakengelhardt]

The behavior of opt_clean is frequently adjusted to fix some issues, which then causes other issues, etc. In the latest iteration, unused wires with public names are now retained, but their driving circuit is removed, which leads to wrong behavior displayed in traces.

@clairexen suggested that we need to write an actual specification of what opt_clean is supposed to do, and then write a new implementation that complies with that specification.

[nakengelhardt]

Some elements that come to mind:

• If any wire or cell is kept (explicitly via (* keep *) or implicitly because of a public name), anything that is driving this wire/cell should no longer be considered unused.

• The -purge argument may not be differentiated enough. I can think of three use cases:

  1. Formal or other close-to-the-original-code uses: don't remove any public nets, or their drivers. Only delete internal nets.
  2. Synthesis and the like: remove any unused public nets (and their drivers) unless (* keep *) is specified
  3. Ruthless optimization: remove anything unused, even ignoring (* keep *)

  Are there other use cases?

[whitequark]

This would very much help CXXRTL!

[eddiehung]

See #2003 and #2076 (comment) -- the latter a case where private wires with (* init *) are replaced with a public wire -- for two more wishlist items to bear in mind.

[clairexen]

I don't think that a wire without (* keep *) on it should be kept if it's unused, in the general case. That would be a big issue in synthesis flows imo.

For single bit wires:

1. if (* keep *) then handle as if it would be a primary output and always keep it
2. if it is driven by a constant then we should keep it (unless -purge)
3. if it is driven by a non-constant and not used then we should remove it

In some cases there's a "race between" 2. and 3., depending of if we first const fold the driver or first optimize away the user we may or may not keep the wire. I don't quite know if there's a good way to resolve that.

For multi-bit wires:
What do we do if some bits are unused? If we only strip those drivers then we again end up with formal traces where some of the wire bits are (falsely) unconstrained.

For SBY / prep it might be worth considering to use a form of clean that bevahes as if every wire with a public name has the keep attribute.

[whitequark]

That would be a big issue in synthesis flows imo.

Would it be? The reason I want that in synthesis flows as well is so that I can insert scan cells and have the retrieved data mapped back to all levels of hierarchy in a flattened design, not just to one (random, or topmost) level.

[nakengelhardt]

I'm fairly sure we should just have flags that let you specify the behavior you need in a certain situation, as clearly the objectives are contradictory depending on how you intend to use the design. The more interesting question is how granular they should be. Can you think of a use case where it is critical that you do keep wires driven by constants but do not keep other public wires? For maximum flexibility we could of course just have separate arguments for every decision, -keep-public-wires -keep-constant-wires -ignore-keep -ignore-init -split-wires (yes|no) and whatever other cases we identify, but that might get a little unwieldy.

[nakengelhardt]

Discussed this with @mwkmwkmwk and we came up with the following proposal:

Expected behavior:

• change buf to assignment
• remove unused cells
• remove wires that are neither used nor driven by a cell port (even if public)
• remove non-public wires that are redundant (magic coolness score decides which wire stays)

Options:

• remove redundant public names (-purge, but with a better name, and actually doing what the description says)

Behavior changes vs. current:

• if a different redundant wire is selected as Q output of a FF, also move the init attribute to that wire
• coolness score should also prefer wires with (* keep *) attribute
• an init attribute on an unused undriven wire (i.e. not on Q port) should never happen, it is a warning but no longer stops the wire from being optimized away
• unused wires driven by constants can be removed
• currently iteration order changes behavior, this should not happen

Other points:

• opt_clean will not split nets, a single used bit means a wire counts as used. Use cases that cannot deal with undriven bits should run splitnets and then opt_clean again.

Larger discussions that reach beyond opt_clean:

• There are more passes than just opt_clean that can affect the semantics of wires, e.g. opt_dff and opt_muxtree. A new invariant is proposed: if the behavior of (parts or all of) a public wire is changed by a pass to anything other than Z for unused bits, the name should be changed so that it is not accidentally addressed externally, e.g. in constraints, when it is no longer the same thing. (optimizing away unused bits is not considered changing the semantics)
• (* keep *) adds an even stronger guarantee that the semantics of this wire will be strictly preserved. Unused bits will not get optimized away. Other passes should also respect that, and e.g. not move parts of the logic to the other side of the wire.
• Because of the above two, instead of adding options for treating public wires differently just in opt_clean, use cases such as formal that need to conserve public internal wires should run setattr -set keep 1 w:\\* at the beginning of the flow. Introduce prep -formal that will do this?

[nakengelhardt]

Two additions from @clairexen:

• for init attributes on unused undriven wires, make sure to consider the case where the wire was originally driven, but the FF was just removed earlier in the opt_clean invocation because it was an unused cell, so that we don't accidentally emit a warning there
• for partially used wires, the "used" status should not transitively be applied to cells, e.g. if only the lower bits of a wire are used, the wire is used but the drivers of the upper bits can still be optimized away.

[jix]

From today's JF discussion: The way opt_clean tries to replace unused bits in the middle of wires with 'x is unwanted in the context of formal verification (and I think it's only not been much of an issue in practice because it's rare to trigger, or at least to trigger in ways that would be confusing to users, given that we don't do any aggressive optimizations in the FV flows). We still want the opton of removing completely unused wires (not connected to anything with the keep attribute or in the input cone of an assertion), as you can end up with things like loop variables that were handled completely by constant evaluation in the frontend but still get emitted into the netlist (at least with verific) and those are useless and can be a bit annoying in FV traces.

(@povik I think you might have had an additional reason to only have the full signal cleaning behavior without replacing intermediate bits with 'x values. When I said I can write this down I was only thinking of this reason that we had discussed just before.)

[povik]

@povik I think you might have had an additional reason to only have the full signal cleaning behavior

I don't like the opt_clean behavior because it violates the principle that if a public wire is named the same, it is functionally equivalent (it's the same function of the current and past module inputs). I guess other than in formal verification this principle is useful when interpreting post-synthesis simulation, or results from any instrumentation implanted into the design.

[whitequark]

I don't like the opt_clean behavior because it violates the principle that if a public wire is named the same, it is functionally equivalent (it's the same function of the current and past module inputs).

CXXRTL debug server relies on this principle for not misleading its users.

[jix]

Might be worth mentioning that we do have other opt passes that violate this property (IIRC opt_share) and AFAIK other synthesis tools sadly do the same, which has been causing ongoing issues with using name based matching when doing equivalence checks with EQY. Unlike opt_clean, those are easier to avoid though, so while I'd prefer all of them to uphold this principle, I consider opt_clean not doing so to be the more severe issue.