#6130 fixed arith_tree so that a chain link narrower than its consumer
is left out of the tree, and added an equivalence regression for the
exact failing shape. Cover what that test does not: structural checks
that the narrow link survives as its own cell, on both the raw $add
path and the alumacc $alu path, and a mixed case where a wider chain
consuming the truncated link as a leaf still folds and stays
equivalent.
Signed-off-by: Daniel M'BOUYOU <[email protected]>
The JSON backend writes "signed": 1 for any signed wire, including
internal nets. The frontend only parsed the attribute for ports,
so a write-read roundtrip silently cleared is_signed on internal
nets. Signed internal wires became unsigned between the two passes.
Fix: parse 'signed' in the netnames loop, next to the existing
upto/offset handling. Regression test does a full roundtrip and
checks the internal signed wire survives.
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.
Both backends only looked for $assert/$assume/$cover, so a $check cell was
never visited and the resulting formal output carried no proof obligations at
all. write_smv already errors via its catch-all; this follows its message.
Emil J
Daniel M'BOUYOU
John Kearney
Nick Allison
Lofty
Zane Hambly
nella
Lofty
nella
Ethan Sifferman
nick
Mateusz Gancarz
Emil J. Tywoniak
Catherine
Miodrag Milanovic