From 3b7c09934ad61150cad715f2eaa04781fcefea4a Mon Sep 17 00:00:00 2001 From: nella Date: Tue, 22 Sep 2026 19:51:39 +0200 Subject: [PATCH] Materialize A sign extension in shiftadd. $shr and $shift sign-extend A to max(A_WIDTH, Y_WIDTH) before shifting. shiftadd resliced A without that extension and left A_SIGNED set, so the narrowed A was sign-extended a second time, from the wrong bit. Bake the extension in before reslicing and clear A_SIGNED. When the constant offset consumed all of A this also left an empty A on a signed $shr, which techmap lowered to x. Fixes #6214, fixes #6041. --- passes/opt/peepopt_shiftadd.pmg | 8 ++++ tests/various/peepopt.ys | 70 +++++++++++++++++++++++++++++++++ 2 files changed, 78 insertions(+) diff --git a/passes/opt/peepopt_shiftadd.pmg b/passes/opt/peepopt_shiftadd.pmg index 622516062..a3eba90f6 100644 --- a/passes/opt/peepopt_shiftadd.pmg +++ b/passes/opt/peepopt_shiftadd.pmg @@ -110,6 +110,12 @@ code reject; } + // $shr and $shift sign-extend A to max(A_WIDTH, Y_WIDTH), so bake that in + // before reslicing A and clear A_SIGNED, or it gets applied twice + bool a_signed = shift->type.in($shr, $shift) && param(shift, \A_SIGNED).as_bool(); + if (a_signed && !old_a.empty()) + old_a.extend_u0(max(GetSize(old_a), GetSize(port(shift, \Y))), true); + did_something = true; log("shiftadd pattern in %s: shift=%s, add/sub=%s, offset: %d\n", \ module, shift, add, offset); @@ -143,6 +149,8 @@ code shift->setPort(\A, new_a); shift->setParam(\A_WIDTH, GetSize(new_a)); + if (a_signed) + shift->setParam(\A_SIGNED, 0); shift->setPort(\B, new_b); shift->setParam(\B_WIDTH, GetSize(new_b)); blacklist(add); diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index e0b9946cf..9e59cef4b 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -245,3 +245,73 @@ design -load postopt clean select -assert-count 1 t:$bmux select -assert-count 0 t:$bmux t:* %D + +#################### + +# shiftadd left an empty A on a signed $shr, which techmap turned into x (#6214) +design -reset +read_verilog <> 2) >> (1 + in[0])); +endmodule +EOT + +synth +sat -verify -prove Y 1'b1 + +#################### + +# signed $shr sign-extends A to Y_WIDTH, the narrowed A must carry that extension +design -reset +read_verilog <> (S + 1); +endmodule +EOT + +prep +# wreduce narrows A below Y_WIDTH +wreduce +equiv_opt -assert peepopt +design -load postopt +clean +select -assert-count 0 t:$add + +#################### + +# A_WIDTH > Y_WIDTH needs no extension, but A_SIGNED must still be cleared +design -reset +read_rtlil <