Verilog: indexed part select expressions with non-constant index

This implements support for indexed part select expressions where the index
is not an elaboration-time constant.

regression/verilog/part-select/index-of-real.desc

@@ -0,0 +1,8 @@
+CORE
+index-of-real.sv
+
+^file .* line 5: bit-select of real is not allowed$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/part-select/index-of-real.sv

@@ -0,0 +1,7 @@
+module main;
+
+  // 1800-2017 6.12.1
+  real some_real;
+  wire x = some_real[0];
+
+endmodule

regression/verilog/indexed-part-select1/test.desc → regression/verilog/part-select/indexed-part-select1.desc

@@ -1,6 +1,6 @@
 CORE broken-smt-backend
-main.sv
---bound 1
+indexed-part-select1.sv
+--bound 0
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/indexed-part-select1/main.sv → regression/verilog/part-select/indexed-part-select1.sv

@@ -9,7 +9,6 @@ module main(in);
     out[16 +: 16]=0;
   end
 
-  always assert property1:
-    { in, { 8 { 1'b0 }} } == out;
+  p1: assert property ({ in, { 8 { 1'b0 }} } == out);
 
 endmodule

regression/verilog/part-select/indexed-part-select2.desc

@@ -0,0 +1,8 @@
+CORE
+indexed-part-select2.sv
+
+^file .* line 4: expected constant expression, but got `main\.width'$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/part-select/indexed-part-select2.sv

@@ -0,0 +1,6 @@
+module main(input [7:0] in, input [2:0] width);
+
+  // The width of an indexed part-select must be a constant
+  wire [7:0] out = in[0 +: width];
+
+endmodule

regression/verilog/part-select/indexed-part-select3.desc

@@ -0,0 +1,8 @@
+CORE
+indexed-part-select3.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/part-select/indexed-part-select3.sv

@@ -0,0 +1,9 @@
+module main(input [7:0] in, input [2:0] where);
+
+  // The base index of an indexed part-select
+  // does not need to be constant.
+  wire out = in[where +: 1];
+
+  p0: assert property (out == in[where]);
+
+endmodule

regression/verilog/part-select/part-select-of-real.desc

@@ -0,0 +1,8 @@
+CORE
+part-select-of-real.sv
+
+^file .* line 5: real not allowed in part select$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/part-select/part-select-of-real.sv

@@ -0,0 +1,7 @@
+module main;
+
+  // 1800-2017 6.12.1
+  real some_real;
+  wire [7:0] x = some_real[7:0];
+
+endmodule

regression/verilog/part-select/real-index.desc

@@ -0,0 +1,8 @@
+CORE
+real-index.sv
+
+^file .* line 5: real number index is not allowed$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/part-select/real-index.sv

@@ -0,0 +1,7 @@
+module main;
+
+  // 1800-2017 6.12.1
+  reg [7:0] vector;
+  wire x = vector[real'(1.5)];
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -32,9 +32,9 @@ IREP_ID_TWO(C_little_endian, #little_endian)
 IREP_ID_ONE(ports)
 IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)
-IREP_ID_ONE(part_select)
-IREP_ID_ONE(indexed_part_select_plus)
-IREP_ID_ONE(indexed_part_select_minus)
+IREP_ID_ONE(verilog_non_indexed_part_select)
+IREP_ID_ONE(verilog_indexed_part_select_plus)
+IREP_ID_ONE(verilog_indexed_part_select_minus)
 IREP_ID_ONE(chandle)
 IREP_ID_ONE(event)
 IREP_ID_ONE(reg)

src/verilog/parser.y

@@ -148,47 +148,6 @@ static void extractbit(YYSTYPE &expr, YYSTYPE &identifier, YYSTYPE &part)
 
 /*******************************************************************\
 
-Function: extractbits
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-static void extractbits(YYSTYPE &expr, YYSTYPE &identifier, YYSTYPE &range)
-{
-  init(expr, ID_extractbits);
-  mto(expr, identifier);
-
-  if(stack_expr(range).id()==ID_part_select)
-  {
-    auto &part_select = to_binary_expr(stack_expr(range));
-    stack_expr(expr).add_to_operands(std::move(part_select.op0()));
-    stack_expr(expr).add_to_operands(std::move(part_select.op1()));
-  }
-  else if(stack_expr(range).id()==ID_indexed_part_select_plus)
-  {
-    auto &part_select = to_binary_expr(stack_expr(range));
-    exprt offset=minus_exprt(part_select.op1(), from_integer(1, integer_typet{}));
-    stack_expr(expr).add_to_operands(part_select.op0());
-    stack_expr(expr).add_to_operands(plus_exprt(part_select.op0(), offset));
-  }
-  else if(stack_expr(range).id()==ID_indexed_part_select_minus)
-  {
-    auto &part_select = to_binary_expr(stack_expr(range));
-    exprt offset=minus_exprt(from_integer(1, integer_typet{}), part_select.op1());
-    stack_expr(expr).add_to_operands(part_select.op0());
-    stack_expr(expr).add_to_operands(plus_exprt(part_select.op0(), offset));
-  }
-  else
-    PRECONDITION(false);
-}
-
-/*******************************************************************\
-
 Function: add_as_subtype
 
   Inputs:
@@ -1145,7 +1104,7 @@ bit_select:
 
 part_select:
 	  '[' const_expression TOK_COLON const_expression ']'
-		{ init($$, ID_part_select); mto($$, $2); mto($$, $4); }
+		{ init($$, ID_verilog_non_indexed_part_select); mto($$, $2); mto($$, $4); }
 	;
 
 // System Verilog standard 1800-2017
@@ -3122,14 +3081,14 @@ inc_or_dec_expression:
 
 constant_range:
 	  const_expression TOK_COLON const_expression
-		{ init($$, ID_part_select); mto($$, $1); mto($$, $3); }
+		{ init($$, ID_verilog_non_indexed_part_select); mto($$, $1); mto($$, $3); }
 	;
 
 indexed_range:
 	  expression TOK_PLUSCOLON constant_expression
-		{ init($$, ID_indexed_part_select_plus); mto($$, $1); mto($$, $3); }
+		{ init($$, ID_verilog_indexed_part_select_plus); mto($$, $1); mto($$, $3); }
 	| expression TOK_MINUSCOLON constant_expression
-		{ init($$, ID_indexed_part_select_minus); mto($$, $1); mto($$, $3); }
+		{ init($$, ID_verilog_indexed_part_select_minus); mto($$, $1); mto($$, $3); }
 	;
 
 part_select_range:
@@ -3161,7 +3120,13 @@ primary_literal:
 hierarchical_identifier_select:
           hierarchical_identifier_bit_select_brace
 	| hierarchical_identifier_bit_select_brace '[' part_select_range ']'
-		{ extractbits($$, $1, $3); }
+		{ // part_select_range has two operands.
+		  // We form a new expression with three operands from it.
+		  auto &part_select = to_binary_expr(stack_expr($3));
+		  stack_expr($3).operands() =
+		    { stack_expr($1), part_select.op0(), part_select.op1() };
+		  $$ = $3;
+		}
 	;
 
 hierarchical_identifier_bit_select_brace: