read_verilog: fix sign extension in array pattern assignments

This commit is contained in:
Emil J. Tywoniak
2026-09-30 12:59:01 +02:00
parent 6f876ae0e2
commit c783ccfdd6
2 changed files with 23 additions and 0 deletions
+12
View File
@@ -1973,6 +1973,18 @@ bool AstNode::simplify(bool const_fold, int stage, int width_hint, bool sign_hin
width_hint_here = -1, sign_hint_here = false;
if (children_are_self_determined)
width_hint_here = -1, sign_hint_here = false;
if (type == AST_ASSIGN_PATTERN) {
// It's unlikely for this simplify to run, but just to be sure
while (!children[i]->basic_prep && children[i]->simplify(false, stage, -1, false))
did_something = true;
// Undo signedness inheritance of the children from the parent AST_ASSIGN_PATTERN
// but widen as needed
int child_width_hint;
bool child_sign_hint;
children[i]->detectSignWidth(child_width_hint, child_sign_hint);
width_hint_here = max(width_hint, child_width_hint);
sign_hint_here = child_sign_hint;
}
did_something_here = children[i]->simplify(const_fold_here, stage, width_hint_here, sign_hint_here);
if (did_something_here)
did_something = true;
@@ -0,0 +1,11 @@
# Signed assignment pattern elements are sign-extended to the element width.
read_verilog -sv <<EOT
module top(output [15:0] o0, o1);
logic [15:0] a [2];
assign a = '{$signed(4'hf), 4'sb1000 >>> 1};
assign o0 = a[0];
assign o1 = a[1];
endmodule
EOT
proc
sat -verify -prove o0 16'hffff -prove o1 16'hfffc