Optimization Sequence Leads to Functionally Incorrect Synthesis Output in Yosys

[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
hierarchy; flatten; proc -noopt; opt_expr -mux_undef;
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 lines of output is:

Custom optimization sequence，the first lines 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.

I have reduced the design file to the best of my ability as shown below：

module top(y, clk, wire4, wire3, wire2, wire1, wire0);
output wire [(32'h971):(32'h0)] y;
input wire [(1'h0):(1'h0)] clk;
input wire [(5'h12):(1'h0)] wire4;
input wire [(3'h6):(1'h0)] wire3;
input wire signed [(4'ha):(1'h0)] wire2;
input wire [(3'h4):(1'h0)] wire1;
input wire signed [(5'h15):(1'h0)] wire0;
wire signed [(5'h14):(1'h0)] wire5;
reg signed [(5'h14):(1'h0)] forvar9 = (1'h0);
reg [(3'h4):(1'h0)] reg100 = (1'h0);
reg [(4'he):(1'h0)] reg18 = (1'h0);
reg signed [(4'hf):(1'h0)] reg12 = (1'h0);
reg [(5'h15):(1'h0)] reg11 = (1'h0);
reg [(3'h4):(1'h0)] reg10 = (1'h0);
reg [(3'h7):(1'h0)] reg8 = (1'h0);
reg [(3'h4):(1'h0)] reg7 = (1'h0);
assign y = {reg7,reg8,forvar9,reg10,reg11,reg12,reg18,reg100,(1'h0)};
always
@(posedge clk) begin
reg7 <= (wire5[(4'hd):(4'h8)] & (-($unsigned(wire1[(1'h0):(1'h0)]) | ($unsigned(wire2) ? (+wire1) : wire1))));
reg8 <= $unsigned($signed({((wire1 != (8'hbe)) ? $unsigned(wire4) : wire4)}));
for (forvar9 = (1'h0); (forvar9 < (2'h3)); forvar9 = (forvar9 + (1'h1)))
begin
reg10 <= {{((^~wire1[(2'h2):(2'h2)]) ? $signed((reg7 ? reg8 : wire1)) : ($unsigned(reg7) ? forvar9 : ((8'hba) ^ wire0)))}};
reg11 <= (^~wire1[(1'h0):(1'h0)]);
end
if (reg11[(2'h3):(1'h1)])
begin
reg12 <= reg7[(3'h4):(1'h0)];
end
else
begin
reg12 <= $unsigned(((wire2 | wire0[(4'hc):(4'h8)]) ? reg12[(3'h7):(1'h1)] : forvar9));
reg18 <= reg12[(4'he):(3'h4)];
end
reg100 = ($signed(reg10[(2'h3):(2'h3)]) >> $unsigned(((|(8'hbd)) + reg18[(3'h4):(1'h0)])));
end
endmodule

The test script is as follows：
        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 -noopt; opt_expr -mux_undef;
            write_verilog syn_yosys.v"
        iverilog -o wave_2 -y syn_yosys.v yosys_testbench.v
        vvp -n wave_2 -lxt2 >> file2.txt

Thank you.

Expected Behavior

The simulation results are consistent

Actual Behavior

Simulation results are inconsistent

[georgerennie]

With the difference only being that some values are x instead of concrete, this is likely the same deal as #4483 where different refinement has occurred but the results are still consistent.