Inconsistent simulation before and after synthesis of complex assignment expressions

[FSY369]

Version

Yosys 0.48

On which OS did this happen?

Linux

Reproduction Steps

Run the script in the terminal (after removing the .log suffix from the filename)：
yosys：
read_verilog rtl.v
synth
write_verilog syn_yosys1.v

    iverilog -o wave -y syn_yosys1.v yosys_testbench.v
    vvp wave > file1.txt

    iverilog -o wave1 -y rtl.v yosys_testbench1.v
    vvp wave1 > file2.txt

rtl.v.log
yosys_testbench.v.log
yosys_testbench1.v.log

Expected Behavior

Pre-synthesis simulation and post-synthesis simulation should be consistent

Actual Behavior

Inconsistency between pre-synthesis re-simulation and post-synthesis simulation

[whitequark]

You are submitting a bug report produced using fuzzing tools. With such bug reports, it is often hard to tell whether the issue reported is an issue in Yosys or an issue with the test harness.

Unless you submit a minimized example clearly demonstrating the construct that causes the inconsistent behavior your bug report will be closed as invalid.

[FSY369]

Ok thanks a lot for your suggestion, I have simplified the code and implemented only some reg and wire definition and instantiation modules in the code again and found that the problem is in this code in the top module:
always @(posedge clk) begin reg259 <= (($signed((wire250[(5'h11):(5'h10)] ? (~&reg251) : $signed(wire237))) - $signed(($unsigned(wire234) ? (wire3 * reg248) : (wire246 ~^ reg251)))) ? $unsigned((wire242 >>> (~{wire243, wire237}))) : wire238); end
It was found to cause inconsistencies in the simulation function before and after synthesis
rtl1.txt

[whitequark]

Please submit another complete RTL file with only the offending construct in it. It should be only a few lines long.

[FSY369]

rtl2.txt

[whitequark]

This is an improvement but it still contains redundant code that does not appear to be core to the issue. For example, param280 and param281 are never used inside of the body of the module, and are clearly redundant.

Please submit a complete RTL file without every construct that is not relevant to the issue at hand.

[georgerennie]

See #997 for an example of a well reported bug found by fuzzing. Note that it includes the following

• A short human readable testcase that contains nothing but the constructs needed to trigger the bug
• A hypothesis about what constructs Yosys is treating incorrectly and what the expected behaviour should be
• The testcase is small enough to be put in a small markdown block in the github issue instead of requiring a download. This generally makes it easier for people to look at the issue and see if its something they are likely to be able to fix. Having a big testcase that requires a separate download reduces the amount of people that will bother to look at your issue

[whitequark]

• Having a big testcase that requires a separate download reduces the amount of people that will bother to look at your issue

This is true, but we also must keep in mind the overall dynamics of the issue. Fuzzer authors derive substantial benefit from the amount of fuzzer-found issues that are acknowledged by the project being fuzzed, such as publishing of academic papers and procurement of funding. Because of this they are incentivized to submit as many issues as they can in the lowest possible time, often not investigating the causes or minimizing the reproducer at all (e.g. this issue). Many such bugs are actually already known ones (fuzzers tend to have a very high rediscovery rate), and as a result, the project suffers from having to dedicate triage resources while often deriving no benefit from the report at all.

I see this pattern as exploitative and believe we must not encourage it.

John Regehr has previously written on this topic more broadly.

[georgerennie]

This is true, but we also must keep in mind the overall dynamics of the issue

Maybe we are talking past each other here, I am totally in agreement and my points were meant as guidance towards what practical steps in submitting a fuzzer found bug make it easy to be quickly triaged/fixed if appropriate

[whitequark]

I meant to add to what you said, not to contradict it, apologies.

[FSY369]

thank you very much for your patient reply. This will not bother me, but will let me learn how to submit bugs, which will improve efficiency and achieve a win-win situation. Thank you again for your help and support.

…

---- Replied Message ---- | From | ***@***.***> | | Date | 12/31/2024 18:36 | | To | ***@***.***> | | Cc | ***@***.***>***@***.***> | | Subject | Re: [YosysHQ/yosys] Inconsistent simulation before and after synthesis of complex assignment expressions (Issue #4828) | I meant to add to what you said, not to contradict it, apologies. — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you authored the thread.Message ID: ***@***.***>

[FSY369]

rel3.txt

[whitequark]

This is still not minimized enough as your testbench includes a lot of random data and your rel3.txt file includes far too much code, including obviously extraneous constructs like $unsigned($unsigned(...)).

You should:

1. Use tools like C-Reduce to further reduce the amount of code in the testcase.
2. Remove lines from your testbench until only a single line remains that triggers the issue.
3. Subset the synth script to determine which pass(es) are responsible for causing the mismatch.
4. Manually remove parts of the RTL until the module consists of only a few Verilog operators (the issue almost certainly can be reproduced with 1 or 2 operators).
5. Simplify the very large constants used in the testbench so that the values of inputs can be easily understood by a human without having to decipher code generated by your fuzzing tools.