Optimization Sequence Induces Synthesis Errors Leading to Simulation Inconsistencies

[LoSyTe]

Version

yosys 0.41+126

On which OS did this happen?

Linux

Reproduction Steps

Hello,

I have encountered an inconsistency issue during synthesis with Yosys.

My Icarus Verilog version is: Icarus Verilog version 13.0 (devel) (s20221226-221-g272771d18), and my Yosys version is 0.41+126.

During synthesis, we did not use the default Yosys synthesis process but employed a custom pass optimization sequence. The synthesis commands for both processes are as follows:

1、Using Yosys' default synthesis process:
read_verilog rtl.v
synth
write_verilog syn_yosys.v
2、Custom optimization sequence:
read_verilog rtl.v
prep -ifx; hierarchy; flatten; proc -ifx; opt_dff -nodffe; opt_lut; opt_expr -noclkinv; memory_libmap; opt_lut; opt_dff -sat; opt_expr -undriven; memory_dff; opt_merge -share_all; memory_collect; opt_muxtree; fsm_map; opt_expr -mux_bool; opt_mem_priority; opt_dff -keepdc; memory_bmux2rom; opt_expr -noclkinv; opt_lut_ins; opt_expr -undriven; check; check; opt_muxtree; opt_expr -mux_undef; opt_merge; opt_mem; memory_bram; fsm_recode; opt_clean; opt_clean -purge;
write_verilog new_syn_yosys.v

The changes in the optimization sequence should not affect the consistency of the code. However, we have observed inconsistencies in the simulation outputs when using the synthesized files generated by these two different synthesis processes with Icarus Verilog (as highlighted in the red box in the attached image).
Default synthesis process，the first line of output is:

Custom optimization sequence，the first line of output is:

This inconsistency suggests that the optimization sequence may be causing synthesis errors, leading to inconsistent simulation results.

I would appreciate your assistance in identifying the root cause of this issue.

Attached is my design file (rtl.v) and the executable script file (yosys.sh).

Thank you.
yosys_project.zip

Expected Behavior

The simulation results are consistent

Actual Behavior

Simulation results are inconsistent

[widlarizer]

Hi, thanks for the report. #4445 (comment) applies here as well. Since this is randomly generated code, please report this as a part of the issue. Are you capable of reducing it further with your tools? By which I mean:

• reducing the verilog code
• removing commands from the custom opt sequence
• removing commands that synth runs by adding as many of these options: -nofsm -noabc -noalumacc -nordff -noshare

such that a difference between the two flows remains?

[LoSyTe]

Simulation results are inconsistent

Thank you for your response. I am currently working on minimizing the optimization sequence as much as possible.

[LoSyTe]

Custom optimization sequence:
read_verilog rtl.v
prep -ifx; hierarchy; flatten; proc -ifx; opt_dff -nodffe; opt_lut; opt_expr -noclkinv; memory_libmap; opt_lut; opt_dff -sat; opt_expr -undriven; memory_dff; opt_merge -share_all; memory_collect; opt_muxtree; fsm_map; opt_expr -mux_bool; opt_mem_priority; opt_dff -keepdc; memory_bmux2rom; opt_expr -noclkinv; opt_lut_ins; opt_expr -undriven; check; check; opt_muxtree; opt_expr -mux_undef; opt_merge; opt_mem; memory_bram; fsm_recode; opt_clean; opt_clean -purge;
write_verilog new_syn_yosys.v

Hi, widlarizer, I have reduced my design file（rtl.v） as well as the optimization sequence as follows：

module top (y, clk, wire3, wire2, wire1, wire0);
output wire [(32'ha23):(32'h0)] y;
input wire [(1'h0):(1'h0)] clk;
input wire signed [(2'h3):(1'h0)] wire3;
input wire signed [(4'hc):(1'h0)] wire2;
input wire [(4'hd):(1'h0)] wire1;
input wire signed [(4'hc):(1'h0)] wire0;
wire [(4'hb):(1'h0)] wire4;
reg signed [(3'h6):(1'h0)] reg10 = (1'h0);
reg [(2'h3):(1'h0)] reg32 = (1'h0);
reg signed [(4'hf):(1'h0)] reg48 = (1'h0);
reg signed [(5'h10):(1'h0)] reg116 = (1'h0);
reg [(4'h9):(1'h0)] reg143 = (1'h0);
assign y = {reg48,reg143,(1'h0)};
always
@(posedge clk) begin
reg48 <= ($unsigned((reg10 >> 8'haf)) ? reg32 : reg32);
end
always
@(posedge clk) begin
reg143 = reg48 <= ($signed(reg116) | $unsigned(wire4[1:1]));
end
endmodule

The test script is：

    yosys -p "
        read_verilog rtl.v         
        synth
        write_verilog syn_yosys.v"
    iverilog -o wave_1 -y syn_yosys.v yosys_testbench.v
    vvp -n wave_1 -lxt2 >> file1.txt
    sed -i 's/wave_1/wave_2/g' file1.txt;
    mv syn_yosys.v old_syn_yosys.v
    
    yosys -p "
        read_verilog rtl.v         
    hierarchy; proc; opt_dff -nodffe; opt_share; opt_clean; abc;
        write_verilog syn_yosys.v"
    iverilog -o wave_2 -y syn_yosys.v yosys_testbench.v
    vvp -n wave_2 -lxt2

However, as shown in the red box in the figure below, the simulation results are inconsistent. We look forward to your next reply.

Using Yosys' default synthesis process，the first line of output is:

Using Custom optimization sequence，the first line of output is:

[georgerennie]

Please consider how this is very difficult for us to debug and given it is not coming from a real world use case there is limited motivation to put that effort in. Although you have minimised the design and script somewhat, the testbench still uses a large amount of randomly generated input.

Ideally please try to extract the core essence of the failure into a handwritten (and thus sensibly structured) testcase that clearly demonstrates an error. This makes it much easier for then debugging where synthesis has gone wrong in Yosys as time can be spent debugging Yosys rather than trying to understand your confusing testcase. If you can say something like "I think opt_expr misoptimizes multiplication between a signed and unsigned input because of this testcase showing unexpected behaviour" that is far more useful than "Here is a load of verilog and somewhere something gets misoptimized".

Assuming you are doing this work in preparation for an academic publication or similar, you will be able to get better statistics about bugs actually being fixed as the result of your work if you help us by providing testcases that can actually be debugged.

Also as a side note, you can wrap code in two sets of 3 backticks and a language name (e.g. verilog) to make it display better on github

[georgerennie]

I haven't been able to understand your testbench much but this case does look like it may be that both optimized versions are valid, they just exploit the fact that wire4 is undriven differently, with one propagating an x forwards and one treating it as a don't care and refining to a concrete value.

[LoSyTe]

Please consider how this is very difficult for us to debug and given it is not coming from a real world use case there is limited motivation to put that effort in. Although you have minimised the design and script somewhat, the testbench still uses a large amount of randomly generated input.

Ideally please try to extract the core essence of the failure into a handwritten (and thus sensibly structured) testcase that clearly demonstrates an error. This makes it much easier for then debugging where synthesis has gone wrong in Yosys as time can be spent debugging Yosys rather than trying to understand your confusing testcase. If you can say something like "I think opt_expr misoptimizes multiplication between a signed and unsigned input because of this testcase showing unexpected behaviour" that is far more useful than "Here is a load of verilog and somewhere something gets misoptimized".

Assuming you are doing this work in preparation for an academic publication or similar, you will be able to get better statistics about bugs actually being fixed as the result of your work if you help us by providing testcases that can actually be debugged.

Also as a side note, you can wrap code in two sets of 3 backticks and a language name (e.g. verilog) to make it display better on github

Hello, thank you very much for your reply. I tried to modify the custom optimization sequence again. I found that the final simulation results of custom hierarchy; proc; opt; abc; and direct use of synth were also inconsistent. Even when Replace opt with any pass in opt, such as opt_clean, and the final simulation result will be different from the default synth.

[georgerennie]

That is not what i am getting at, I mean to suggest that "the final simulation result will be different from the default synth" is far too vague to be useful for debugging, you should try to dive into exactly what constructs are causing what issues.

I had a quick further look at this issue and I believe my earlier comment that these are both correct synthesis results is true, one has just been refined more than the other.

Running hierarchy; proc; opt; abc (or anything else that doesn't lower the word level cells) gives the following structure.

When simulated, wire4 takes the value x as it is undriven so the output does too. However, note that the first $le argument is 0. 0 is always less or equal to any other unsigned value so this $le expression can be optimized to a constant 1.

Running just synth gives the following structure, a DFF driven by constant 1, which matches the above optimization.

These are both valid results, they have just had different amounts of lowering. Synthesis passes do not preserve an equivalence relation, but instead a notion of refinement. This blog post talks about the same concept but instead in the context of the llvm compiler.

[LoSyTe]

这不是我要说的，我的意思是说“最终的模拟结果将不同于默认的合成器”太模糊而无法用于调试，您应该尝试深入研究究竟是什么结构导致了哪些问题。

我快速进一步研究了这个问题，我相信我之前的评论，即这些都是正确的综合结果，只是一个比另一个更加完善。

运行hierarchy; proc; opt; abc（或任何其他不会降低字级单元的操作）将产生以下结构。 模拟时，wire4 会获取未驱动的值，因此输出也是如此。但是，请注意第一个参数是 0。0 始终小于或等于任何其他无符号值，因此此表达式可以优化为常数 1。 x``$le``$le

运行只会synth给出以下结构，即由常数 1 驱动的 DFF，与上述优化相匹配。

这些都是有效的结果，只是降低了不同的量。综合过程不保留等价关系，而是保留了细化的概念。这篇博文讨论了相同的概念，但在 llvm 编译器的上下文中。

Thank you very much for your reply. I understand somewhat, but I have questions. In fact, the two processes are equivalent. However, when using Iverilog for functional simulation verification, as I described in the previous picture, there are indeed inconsistencies in the binary code. situation, then the waveform diagram of the functional simulation is different. Is this possibly an error of the Iverilog simulator? Or is it possible that comprehensive files with the same function may have inconsistent simulation results?

[georgerennie]

Or is it possible that comprehensive files with the same function may have inconsistent simulation results?

Yes this is possible when the files are synthesized, as seen here. Consider the following verilog

module top(output logic y);
assign y = 'x;
endmodule

It is perfectly valid for this to be optimized by the synthesis tool to

assign y = '1;

or to

assign y = '0;

as x is a "don't care" value and can't even be represented by real hardware. A fully post synthesis design ready for a hardware target would therefore not have xs in. You can see from this example that the pre-synthesis design will give different simulation results to post-synthesis, and that there are multiple valid ways of synthesising the design that will give different simulation results.

If you want to check correctness of synthesis in this way, you could either avoid ever generating anything with nondeterminism like x, or, instead of comparing two different synthesis sequences you could compare the design before and after synthesis. When doing this, you should only report a mismatch if the pre and post synthesis simulation results differ AND the pre synthesis simulation result is not an x.

Even this may not actually be enough in all cases, but I can't think of any this wouldn't work for off the top of my head.

[widlarizer]

The supposed inconsistency was found by George to be a valid refinement, I'm closing this issue as invalid