Verilog: assignment pattern expressions

This adds support for struct and array literals to the SystemVerilog
frontend by implementing the assignment_pattern_expression production rules.

Author: kroening

regression/verilog/arrays/array_literal1.desc

@@ -0,0 +1,6 @@
+CORE
+array_literal1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--

regression/verilog/arrays/array_literal1.sv

@@ -0,0 +1,8 @@
+module main;
+
+  reg [7:0] my_array[10] = '{1, 2, 3, 4, 5, 6, 7, 8, 9, 10};
+
+  initial p0: assert property (my_array[0] == 1);
+  initial p1: assert property (my_array[9] == 10);
+
+endmodule

regression/verilog/arrays/array_literal2.desc

@@ -0,0 +1,8 @@
+CORE
+array_literal2.sv
+
+^file array_literal2\.sv line 3: number of expressions does not match number of array elements$
+^CONVERSION ERROR$
+^EXIT=2$
+^SIGNAL=0$
+--

regression/verilog/arrays/array_literal2.sv

@@ -0,0 +1,5 @@
+module main;
+
+  reg [7:0] my_array[10] = '{1, 2, 3, 4}; // too short
+
+endmodule

regression/verilog/structs/structs5.desc

@@ -0,0 +1,9 @@
+CORE
+structs5.sv
+--bound 0
+^\[main\.p1\] always main\.s\.field1 == 1: PROVED up to bound 0$
+^\[main\.p2\] always main\.s\.field2 == 0: PROVED up to bound 0$
+^\[main\.p3\] always main\.s\.field3 == 115: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/verilog/structs/structs5.sv

@@ -0,0 +1,13 @@
+module main;
+
+  struct packed {
+    bit field1, field2;
+    bit [6:0] field3;
+  } s = '{ 1, 0, 'b1110011 };
+
+  // Expected to pass.
+  p1: assert property (s.field1 == 1);
+  p2: assert property (s.field2 == 0);
+  p3: assert property (s.field3 == 'b1110011);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -50,6 +50,7 @@ IREP_ID_TWO(C_little_endian, #little_endian)
 IREP_ID_ONE(ports)
 IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)
+IREP_ID_ONE(verilog_assignment_pattern)
 IREP_ID_ONE(verilog_explicit_cast)
 IREP_ID_ONE(verilog_size_cast)
 IREP_ID_ONE(verilog_implicit_typecast)

src/verilog/parser.y

@@ -3009,6 +3009,18 @@ case_item:
                   mto($$, $2); }
 	;
 
+// System Verilog standard 1800-2017
+// A.6.7.1 Patterns
+
+assignment_pattern:
+	'\'' '{' expression_brace '}'
+		{ init($$, ID_verilog_assignment_pattern); swapop($$, $3); }
+	;
+
+assignment_pattern_expression:
+	  assignment_pattern
+	;
+
 // System Verilog standard 1800-2017
 // A.6.8 Looping statements
 
@@ -3331,6 +3343,7 @@ primary:  primary_literal
 	| '(' mintypmax_expression ')'
 		{ $$ = $2; }
 	| cast
+	| assignment_pattern_expression
         | TOK_NULL { init($$, ID_NULL); }
 	;
 

src/verilog/verilog_typecheck_expr.cpp

@@ -318,6 +318,20 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr)
   {
     return convert_expr_function_call(to_function_call_expr(expr));
   }
+  else if(expr.id() == ID_verilog_assignment_pattern)
+  {
+    // multi-ary -- may become a struct or array, depending
+    // on context.
+    for(auto &op : expr.operands())
+      convert_expr(op);
+
+    // Typechecking can only be completed once we know the type
+    // from the usage context. We record "verilog_assignment_pattern"
+    // to signal that.
+    expr.type() = typet(ID_verilog_assignment_pattern);
+
+    return expr;
+  }
   else
   {
     std::size_t no_op;
@@ -1614,6 +1628,64 @@ void verilog_typecheck_exprt::implicit_typecast(
       return;
     }
   }
+  else if(src_type.id() == ID_verilog_assignment_pattern)
+  {
+    DATA_INVARIANT(
+      expr.id() == ID_verilog_assignment_pattern,
+      "verilog_assignment_pattern expression expected");
+    if(dest_type.id() == ID_struct)
+    {
+      auto &struct_type = to_struct_type(dest_type);
+      auto &components = struct_type.components();
+
+      if(expr.operands().size() != components.size())
+      {
+        throw errort().with_location(expr.source_location())
+          << "number of expressions does not match number of struct members";
+      }
+
+      for(std::size_t i = 0; i < components.size(); i++)
+      {
+        // rec. call
+        implicit_typecast(expr.operands()[i], components[i].type());
+      }
+
+      // turn into struct expression
+      expr.id(ID_struct);
+      expr.type() = dest_type;
+      return;
+    }
+    else if(dest_type.id() == ID_array)
+    {
+      auto &array_type = to_array_type(dest_type);
+      auto &element_type = array_type.element_type();
+      auto array_size =
+        numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
+
+      if(array_size != expr.operands().size())
+      {
+        throw errort().with_location(expr.source_location())
+          << "number of expressions does not match number of array elements";
+      }
+
+      for(std::size_t i = 0; i < array_size; i++)
+      {
+        // rec. call
+        implicit_typecast(expr.operands()[i], element_type);
+      }
+
+      // turn into array expression
+      expr.id(ID_array);
+      expr.type() = dest_type;
+      return;
+    }
+    else
+    {
+      throw errort().with_location(expr.source_location())
+        << "cannot convert assignment pattern to '" << to_string(dest_type)
+        << '\'';
+    }
+  }
 
   throw errort().with_location(expr.source_location())
     << "failed to convert `" << to_string(src_type) << "' to `"