arith_tree: do not flatten a chain link narrower than its consumer

sole_chainable_consumer folded a cell into its consumer without ever
comparing widths. A link truncates its result at its own Y width, and that
truncation is invisible only when the consumer truncates at least as hard,
since (x % 2**link) % 2**parent == x % 2**parent holds only when
parent <= link. When the consumer is wider, the carry the link discards
becomes observable, and flattening the chain silently recovers it.

For

  module top(input [7:0] a, b, c, output [8:0] o);
    wire [7:0] t = a + b;
    assign o = t + c;
  endmodule

synth -arith_tree computes a + b + c where the design specifies
((a + b) % 256) + c. The two differ by 256 whenever a + b overflows,
for example at a=169 b=135 c=7.

alumacc already guards the structurally identical $macc merge using
macc_may_overflow(); arith_tree carried no equivalent check.

Add two cases to tests/arith_tree/arith_tree_equiv.ys: equiv_double_neg
widened to a 5 bit result, and a dedicated equiv_narrow_intermediate.
This commit is contained in:
Daniel M Bouyou 2026-08-18 12:06:48 +02:00
parent 621d943ac8
commit e5c56c6400
2 changed files with 25 additions and 4 deletions

View File

@ -134,6 +134,13 @@ struct ArithTreeWorker {
else if (consumer != c)
return nullptr;
}
// A link truncates its own result at its own Y width. That truncation
// is invisible only if the consumer truncates at least as hard, since
// (x % 2**link) % 2**parent == x % 2**parent only when parent <= link.
// A link narrower than its consumer discards a carry that the wider
// consumer would otherwise see, so it must not be flattened away.
if (consumer != nullptr && GetSize(sig) < GetSize(consumer->getPort(ID::Y)))
return nullptr;
return consumer;
}

View File

@ -163,7 +163,7 @@ design -reset
read_verilog <<EOT
module equiv_double_neg(
input [3:0] a, b, c,
output [3:0] y
output [4:0] y
);
wire [3:0] ab = a - b;
assign y = c - ab;
@ -172,7 +172,21 @@ EOT
hierarchy -auto-top
proc
equiv_opt -assert arith_tree
design -load postopt
select -assert-count 2 t:$fa
select -assert-count 1 t:$add
design -reset
# A chain link that is narrower than the cell consuming it truncates its own
# result, and that truncation is observable in the wider consumer. Flattening
# the chain must not recover the carry the narrower link discarded.
read_verilog <<EOT
module equiv_narrow_intermediate(
input [7:0] a, b, c,
output [8:0] y
);
wire [7:0] t = a + b;
assign y = t + c;
endmodule
EOT
hierarchy -auto-top
proc
equiv_opt -assert arith_tree
design -reset