YosysHQ / eqy

Equivalence checking with Yosys
https://yosyshq.readthedocs.io/projects/eqy/en/latest/
Other
29 stars 5 forks source link

Unrelated cells sharing the same name can cause conflicting drivers in an amended partition (triggerd by the default ghdl-yosys-plugin output) #37

Open fayalalebrun opened 1 year ago

fayalalebrun commented 1 year ago

I am trying to use eqy in conjuction with ghdl-yosys-plugin. However, I get the following error:

ERROR: conflicting matches for gold bit $auto$ghdl.cc:806:import_module$28: $auto$ghdl.cc:806:import_module$100 vs $auto$ghdl.cc:806:import_module$42

There are many such auto-generated names in the netlist, so the next thing I tried was to add the following:

[match *]
nodefault
gold-match /^((?!import_module).)*$/

However, this has no effect on the error.

I am not sure if preventing those signals from being matched would fix the issue, or what the implications would be.

Therefore, I am wondering whether it is possible to use eqy with ghdl-yosys-plugin? If not, is this a limitation of eqy, or of ghdl-yosys-plugin?

jix commented 1 year ago

Can you share the complete .eqy file and design you are using?

fayalalebrun commented 1 year ago

I was using it for a cache controller which is rather complex. However, I transcribed one of the examples to vhdl and it seems to fail with a similar error: https://gist.github.com/fayalalebrun/055de56382081b62b47fe2639ae8e000

jix commented 11 months ago

Just for reference, since you mentioned "a similar error" and I'm not sure I'm getting the same error, with EQY, yosys and the ghdl-plugin from the latest nightly oss-cad-suite build I get:

EQY 14:26:23 [ex_amend] partition: Warning: multiple conflicting drivers for gate.top.Y.\__cp_X [1]:
EQY 14:26:23 [ex_amend] partition: module input __cp_X[1]
EQY 14:26:23 [ex_amend] partition: module input __cp_auto$ghdl.cc:806:import_module$1[0]
EQY 14:26:23 [ex_amend] partition: ERROR: Found 1 problems in 'check -assert'.

While looking into the cause, I noticed that the ghdl plugin uses public RTLIL names for auto-generated sequential cell names. This can result in EQY trying to align the design along completely unrelated cells that happen to receive the same sequential name. Ideally the ghdl plugin would generate private RTLIL names, but a workaround is to manually hide the public names for those cells, which can be done by running rename -hide */[0123456789]* after the ghdl plugin command. This hides all names starting with a digit.

With that done, the example doesn't reproduce the issue and this might also avoid the issue in your larger use case. It's still an actual bug that this can confuse the partitioning into generating multiple drivers for the same signal, but I haven't tracked down the exact reason for that happening yet.

jix commented 11 months ago

I reduced it further to the following eqy file directly containing two smaller netlists that reproduce this without needing to use the ghdl plugin: https://gist.github.com/jix/ff72778c03cd6769a277b3c98658441e

gold gold

gate gate

The cells named "13" and "2" have the same name although they were unrelated even in the ghdl example.

@clairexen Any idea how that gets the partitioning code to produce conflicting drivers?

clairexen commented 11 months ago

First attempt at a fix for this issue: