From 34b5c6d0622f395b569543fa5c166a304253b535 Mon Sep 17 00:00:00 2001 From: phsauter Date: Thu, 13 Jun 2024 22:40:12 +0200 Subject: [PATCH 1/2] peepopt: avoid shift-amount underflow --- passes/pmgen/peepopt_shiftadd.pmg | 5 ++++- tests/opt/bug4413.ys | 15 +++++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 tests/opt/bug4413.ys diff --git a/passes/pmgen/peepopt_shiftadd.pmg b/passes/pmgen/peepopt_shiftadd.pmg index e690ff651..875559790 100644 --- a/passes/pmgen/peepopt_shiftadd.pmg +++ b/passes/pmgen/peepopt_shiftadd.pmg @@ -66,7 +66,8 @@ match add define offset_negative ((port(add, constport).bits().back() == State::S1) ^ (is_sub && varport_A)) // checking some value boundaries as well: - // data[...-c +:W1] is fine for +/-var (pad at LSB, all data still accessible) + // data[...-c +:W1] is fine for any signed var (pad at LSB, all data still accessible) + // unsigned shift may underflow (eg var-3 with var<3) -> cannot be converted // data[...+c +:W1] is only fine for +var(add) and var unsigned // (+c cuts lower C bits, making them inaccessible, a signed var could try to access them) // either its an add or the variable port is A (it must be positive) @@ -74,6 +75,8 @@ match add // -> data[var+c +:W1] (with var signed) is illegal filter !(!offset_negative && varport_signed) + // -> data >> (var-c) (with var unsigned) is illegal + filter !(offset_negative && !varport_signed) // state-variables are assigned at the end only: // shift the log2scale offset in-front of add to get true value: (var+c)< (var<> shift2; +endmodule + +EOT + +equiv_opt -assert peepopt From 74e504330a75afe43117d8ef4ee350f9d6000c74 Mon Sep 17 00:00:00 2001 From: Philippe Sauter Date: Fri, 14 Jun 2024 13:01:18 +0200 Subject: [PATCH 2/2] peepopt: fix sign check in shiftadd --- passes/pmgen/peepopt_shiftadd.pmg | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/passes/pmgen/peepopt_shiftadd.pmg b/passes/pmgen/peepopt_shiftadd.pmg index 875559790..161effe43 100644 --- a/passes/pmgen/peepopt_shiftadd.pmg +++ b/passes/pmgen/peepopt_shiftadd.pmg @@ -63,7 +63,8 @@ match add define constport_signed param(add, !varport_A ? \A_SIGNED : \B_SIGNED).as_bool() define varport_signed param(add, varport_A ? \A_SIGNED : \B_SIGNED).as_bool(); - define offset_negative ((port(add, constport).bits().back() == State::S1) ^ (is_sub && varport_A)) + define const_negative (constport_signed && (port(add, constport).bits().back() == State::S1)) + define offset_negative ((is_sub && varport_A) ^ const_negative) // checking some value boundaries as well: // data[...-c +:W1] is fine for any signed var (pad at LSB, all data still accessible)