diff --git a/regression/verilog/expressions/index-constant1.desc b/regression/verilog/expressions/index-constant1.desc new file mode 100644 index 000000000..69a8d73a7 --- /dev/null +++ b/regression/verilog/expressions/index-constant1.desc @@ -0,0 +1,8 @@ +CORE +index-constant1.sv + +^\[.*\] .* PROVED .*$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/expressions/index-constant1.sv b/regression/verilog/expressions/index-constant1.sv new file mode 100644 index 000000000..5e3ba0603 --- /dev/null +++ b/regression/verilog/expressions/index-constant1.sv @@ -0,0 +1,11 @@ +module main; + + // index expressions yield constants + parameter p = 'b1010; + parameter q = p[3]; + parameter r = p[0]; + + assert final (q == 1); + assert final (r == 0); + +endmodule diff --git a/regression/verilog/expressions/index-constant2.desc b/regression/verilog/expressions/index-constant2.desc new file mode 100644 index 000000000..6728da1da --- /dev/null +++ b/regression/verilog/expressions/index-constant2.desc @@ -0,0 +1,8 @@ +CORE +index-constant2.sv + +^\[.*\] .* PROVED .*$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/expressions/index-constant2.sv b/regression/verilog/expressions/index-constant2.sv new file mode 100644 index 000000000..e69eff5c8 --- /dev/null +++ b/regression/verilog/expressions/index-constant2.sv @@ -0,0 +1,9 @@ +module main; + + // index expressions yield constants + parameter p = (1>0); // boolean + parameter q = p[0]; + + assert final (q == 1); + +endmodule diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index a57aaf355..8973881e0 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2738,6 +2738,9 @@ exprt verilog_typecheck_exprt::convert_bit_select_expr(binary_exprt expr) } else { + // extractbit works on bit vectors only + no_bool_ops(expr); + auto width = get_width(op0.type()); auto offset = op0.type().get_int(ID_C_offset);