Skip to content

Commit

Permalink
Merge pull request #4452 from phsauter/shiftadd-underflow-fix
Browse files Browse the repository at this point in the history
peepopt: avoid shift-amount underflow
  • Loading branch information
widlarizer authored Aug 19, 2024
2 parents 0dfa496 + 74e5043 commit e0d3bbf
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 2 deletions.
8 changes: 6 additions & 2 deletions passes/pmgen/peepopt_shiftadd.pmg
Original file line number Diff line number Diff line change
Expand Up @@ -63,17 +63,21 @@ match add

define <bool> constport_signed param(add, !varport_A ? \A_SIGNED : \B_SIGNED).as_bool()
define <bool> varport_signed param(add, varport_A ? \A_SIGNED : \B_SIGNED).as_bool();
define <bool> offset_negative ((port(add, constport).bits().back() == State::S1) ^ (is_sub && varport_A))
define <bool> const_negative (constport_signed && (port(add, constport).bits().back() == State::S1))
define <bool> offset_negative ((is_sub && varport_A) ^ const_negative)

// 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)
select (add->type.in($add) || varport == \A)

// -> 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)<<N -> (var<<N)+(c<<N)
Expand Down
15 changes: 15 additions & 0 deletions tests/opt/bug4413.ys
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
read_verilog <<EOT
module top(
input wire shift,
input wire [4:0] data,
output wire out
);

wire [1:0] shift2 = shift - 1'b1;

assign out = data >> shift2;
endmodule

EOT

equiv_opt -assert peepopt

0 comments on commit e0d3bbf

Please sign in to comment.