Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Custom Yosys Passes Result in Faulty Synthesis and Simulation Errors #4491

Open
PerryLogic opened this issue Jul 15, 2024 · 5 comments
Open
Labels
pending-verification This issue is pending verification and/or reproduction

Comments

@PerryLogic
Copy link

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:
old
Custom optimization sequence,the third and fourth line of output is:
new
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

@PerryLogic PerryLogic added the pending-verification This issue is pending verification and/or reproduction label Jul 15, 2024
@PerryLogic
Copy link
Author

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
Copy link
Contributor

georgerennie commented Jul 19, 2024

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

yosys/passes/opt/opt_expr.cc

Lines 1307 to 1338 in 118b282

if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)) && (keepdc ? assign_map(cell->getPort(ID::B)).is_fully_def() : assign_map(cell->getPort(ID::B)).is_fully_const()))
{
bool sign_ext = cell->type == ID($sshr) && cell->getParam(ID::A_SIGNED).as_bool();
int shift_bits = assign_map(cell->getPort(ID::B)).as_int(cell->type.in(ID($shift), ID($shiftx)) && cell->getParam(ID::B_SIGNED).as_bool());
if (cell->type.in(ID($shl), ID($sshl)))
shift_bits *= -1;
RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID::A));
RTLIL::SigSpec sig_y(cell->type == ID($shiftx) ? RTLIL::State::Sx : RTLIL::State::S0, cell->getParam(ID::Y_WIDTH).as_int());
if (cell->type != ID($shiftx) && GetSize(sig_a) < GetSize(sig_y))
sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
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];
}
cover_list("opt.opt_expr.constshift", "$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx", cell->type.str());
log_debug("Replacing %s cell `%s' (B=%s, SHR=%d) in module `%s' with fixed wiring: %s\n",
log_id(cell->type), log_id(cell), log_signal(assign_map(cell->getPort(ID::B))), shift_bits, log_id(module), log_signal(sig_y));
module->connect(cell->getPort(ID::Y), sig_y);
module->remove(cell);
did_something = true;
goto next_cell;

@georgerennie
Copy link
Contributor

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

@PerryLogic
Copy link
Author

这似乎是 中的一个合法错误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 中的优化造成的。

yosys/passes/opt/opt_expr.cc

Lines 1307 to 1338 in 118b282

if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)) && (keepdc ? assign_map(cell->getPort(ID::B)).is_fully_def() : assign_map(cell->getPort(ID::B)).is_fully_const()))
{
bool sign_ext = cell->type == ID($sshr) && cell->getParam(ID::A_SIGNED).as_bool();
int shift_bits = assign_map(cell->getPort(ID::B)).as_int(cell->type.in(ID($shift), ID($shiftx)) && cell->getParam(ID::B_SIGNED).as_bool());
if (cell->type.in(ID($shl), ID($sshl)))
shift_bits *= -1;
RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID::A));
RTLIL::SigSpec sig_y(cell->type == ID($shiftx) ? RTLIL::State::Sx : RTLIL::State::S0, cell->getParam(ID::Y_WIDTH).as_int());
if (cell->type != ID($shiftx) && GetSize(sig_a) < GetSize(sig_y))
sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
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];
}
cover_list("opt.opt_expr.constshift", "$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx", cell->type.str());
log_debug("Replacing %s cell `%s' (B=%s, SHR=%d) in module `%s' with fixed wiring: %s\n",
log_id(cell->type), log_id(cell), log_signal(assign_map(cell->getPort(ID::B))), shift_bits, log_id(module), log_signal(sig_y));
module->connect(cell->getPort(ID::Y), sig_y);
module->remove(cell);
did_something = true;
goto next_cell;

Thank you very much for your help

@RCoeurjoly
Copy link
Contributor

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");
				}
			}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
pending-verification This issue is pending verification and/or reproduction
Projects
None yet
Development

No branches or pull requests

3 participants