Expression not recognized as constant

[zputrle]

If I run the following example with ebmc examples/test_constant_expr.v --systemverilog --top test_constant_expr --bound 10

module test_constant_expr #(parameter x = 8'hff) ();

    test_mod #(.p(x[3 : 0])) mod ();

endmodule

module test_mod #(parameter p = 1) ();
    
    initial begin
        $display("p = 0x%0h", p);
    end

endmodule

I get the following output

Parsing examples/test_constant_expr.v
Converting
Type-checking Verilog::test_mod
Type-checking Verilog::test_constant_expr
file examples/test_constant_expr.v line 3: expected constant expression, but got `255[3:0]'
CONVERSION ERROR

It seems that EBMC does not recognize x[3:0], where x is a (constant) parameter, as a constant expression.

[zputrle]

It seems that a similar problem arises if indexed part-select is used instead of part-select.

If I run the following example

module test_constant_expr #(parameter x = 8'hff) ();

    test_mod #(.p(x[3 -: 2])) mod ();

endmodule

module test_mod #(parameter p = 1) ();
    
    initial begin
        $display("p = 0x%0h", p);
    end
endmodule

I get the following output

Parsing examples/test_const_part_select.v
Converting
Type-checking Verilog::test_mod
Type-checking Verilog::test_const_part_select
file examples/test_const_part_select.v line 4: expected constant expression, but got `16'hFFFF[8-4]'
CONVERSION ERROR

I ran the example with latest commits on main branch (fb9a9d4).