Custom Yosys Passes Result in Faulty Synthesis and Simulation Errors

[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; proc; opt_expr -mux_bool; opt_clean -purge; memory; opt_reduce -full; wreduce; opt_dff -nodffe; fsm; opt_expr -full; abc; 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 third and fourth line of output is: Custom optimization sequence，the third and fourth 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 (test.sh).

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'h1b5):(32'h0)] y; input wire [(1'h0):(1'h0)] clk; input wire [(4'ha):(1'h0)] wire4; input wire signed [(3'h5):(1'h0)] wire3; input wire [(2'h2):(1'h0)] wire2; input wire signed [(5'h18):(1'h0)] wire1; input wire [(5'h14):(1'h0)] wire0; wire signed [(5'h14):(1'h0)] wire38; wire signed [(4'h8):(1'h0)] wire32; wire [(5'h16):(1'h0)] wire6; reg signed [(4'h8):(1'h0)] reg16 = (1'h0); reg [(3'h4):(1'h0)] reg10 = (1'h0); assign y = {wire6,wire32,wire38,(1'h0)}; assign wire6 = (-((8'ha3) || {wire2, (((8'hbc) == wire0) | (8'hb5))})); assign wire32 = ($signed(1'b0) ? reg16[(1'h0):(1'h0)] : 8'ha1); assign wire38 = $signed((($signed(wire0) >>> {wire6, $signed(wire32)}) ? (+reg10) : (8'ha3))); 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; opt_expr -mux_bool; opt_clean -purge; memory; opt_reduce -full;  wreduce; opt_dff -nodffe; fsm; opt_expr -full; abc;
        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

[LoSyTe]

Hello, I checked the custom optimization sequence and found that the issue occurred during the opt_expr -full step after FSM optimization. When I removed opt_expr -full, the sequence changed to 'hierarchy; proc; opt_expr -mux_bool; opt_clean -purge; memory; opt_reduce -full; wreduce; opt_dff -nodffe; fsm; abc;'. With this modified sequence, the simulation results were consistent with the default synth. This indicates that the problem arises during the opt_expr -full optimization step, leading to the inconsistent final simulation results.

[georgerennie]

This does seem to be a legitimate bug in opt_expr. I have found the following minimal reproducer script

# This doesn't prove equivalence
read_verilog <<EOT
module top(output wire y, input wire wire0);
  assign y = $signed(wire0) >>> 32'h80000000;
endmodule
EOT

equiv_opt opt_expr -fine

design -reset

# This successfully proves equivalence
read_verilog <<EOT
module top(output wire y, input wire wire0);
  assign y = $signed(wire0) >>> 32'h7FFFFFFF;
endmodule
EOT

equiv_opt opt_expr -fine

opt_expr tries to optimise the large constant shift to a constant value, but seems to go wrong when the 32nd bit is set. The correct optimization should give y = wire0 as this preserves sign, but when the 32nd bit is set it is instead being optimized to y = 0.

As 32nd bit set is the overflow value for a C++ int on my machine, I suspect this is a case of a constant being cast to an int without appropriate bounds checks, this opt_expr thinks the value is a negative shift amount, however even then I think an $sshr should preserve sign so this is potentially hitting a misoptimization as well as an overflow.

I think this is from this optimization in opt_expr https://github.com/YosysHQ/yosys/blob/118b2829db18b8399ae1eb174e8295717d422544/passes/opt/opt_expr.cc#L1307-L1338

[georgerennie]

This seems very much related to #4164 and #4010. The latter also sees mismatch for opt_expr -fine in particular

[LoSyTe]

这似乎是 中的一个合法错误opt_expr。我找到了以下最小的重现脚本

# This doesn't prove equivalence
read_verilog <<EOT
module top(output wire y, input wire wire0);
  assign y = $signed(wire0) >>> 32'h80000000;
endmodule
EOT

equiv_opt opt_expr -fine

design -reset

# This successfully proves equivalence
read_verilog <<EOT
module top(output wire y, input wire wire0);
  assign y = $signed(wire0) >>> 32'h7FFFFFFF;
endmodule
EOT

equiv_opt opt_expr -fine

opt_expr尝试将较大的常数移位优化为常数值，但当设置第 32 位时似乎出错了。正确的优化应该给出，y = wire0因为这会保留符号，但当设置第 32 位时，它反而被优化为y = 0。

由于第 32 位设置是我的计算机上 C++ 的溢出值int，我怀疑这是一个在没有适当边界检查的情况下将常量转换为 int 的情况，这opt_expr认为该值是一个负移位量，然而即便如此，我认为$sshr应该保留符号，所以这可能会遇到错误优化和溢出。

我认为这是由于 opt_expr 中的优化造成的。

https://github.com/YosysHQ/yosys/blob/118b2829db18b8399ae1eb174e8295717d422544/passes/opt/opt_expr.cc#L1307-L1338

Thank you very much for your help

[RCoeurjoly]

The overflow occurs in https://github.com/YosysHQ/yosys/blob/main/kernel/rtlil.cc#L275 I think it gets triggered because the Verilog shift constant is non signed and the C++ is signed (int32_t ret = 0;), and that value (32'h80000000) does not fit in ret.

After returning a negative value, we go through the else case of this for loop

            for (int i = 0; i < GetSize(sig_y); i++) {
                int idx = i + shift_bits;
                if (0 <= idx && idx < GetSize(sig_a))
                    sig_y[i] = sig_a[idx];
                else if (GetSize(sig_a) <= idx && sign_ext)
                    sig_y[i] = sig_a[GetSize(sig_a)-1];
                else {
                  log_warning("Index out of range");
                }
            }