YosysHQ / yosys

Yosys Open SYnthesis Suite
https://yosyshq.net/yosys/
ISC License
3.48k stars 890 forks source link

Properly specify and reimplement opt_clean/clean #2165

Open nakengelhardt opened 4 years ago

nakengelhardt commented 4 years ago

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 commented 4 years ago

Some elements that come to mind:

whitequark commented 4 years ago

This would very much help CXXRTL!

eddiehung commented 4 years ago

See #2003 and https://github.com/YosysHQ/yosys/pull/2076#issuecomment-636231300 -- 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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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

Expected behavior:

nakengelhardt commented 4 years ago

Two additions from @clairexen:

jix commented 5 months ago

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 commented 5 months ago

@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 commented 5 months ago

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 commented 5 months ago

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.