SystemVerilog: structs

This adds support for SystemVerilog struct types.

Author: kroening

regression/verilog/structs/structs1.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+structs1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+cast bitvector to struct missing

regression/verilog/structs/structs1.sv

@@ -0,0 +1,18 @@
+module main;
+
+  // The first field is the most-significant bit.
+  struct packed {
+    bit field1, field2;
+    bit [6:0] field3;
+  } s;
+
+  // bit-vectors can be converted without cast to packed structs
+  initial s = 8'b1011111;
+
+  // Expected to pass.
+  p0: assert property ($bits(s) == 9);
+  p1: assert property (s.field1 == 1);
+  p2: assert property (s.field2 == 0);
+  p3: assert property (s.field3 == 'b111111);
+
+endmodule

regression/verilog/structs/structs2.desc

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

regression/verilog/structs/structs2.sv

@@ -0,0 +1,20 @@
+module main;
+
+  // The first field is the most-significant bit.
+  struct packed {
+    bit field1, field2;
+    bit [6:0] field3;
+  } s;
+
+  initial begin
+    s.field1 = 1;
+    s.field2 = 0;
+    s.field3 = 127;
+  end
+
+  // Expected to pass.
+  p1: assert property (s.field1 == 1);
+  p2: assert property (s.field2 == 0);
+  p3: assert property (s.field3 == 'b1111111);
+
+endmodule

regression/verilog/structs/structs3.desc

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

regression/verilog/structs/structs3.sv

@@ -0,0 +1,17 @@
+module main;
+
+  struct packed {
+    // a struct inside a struct
+    struct packed {
+      bit [7:0] field1;
+    } field1;
+  } s;
+
+  initial begin
+    s.field1.field1 = 123;
+  end
+
+  // Expected to pass.
+  p1: assert property (s.field1.field1 == 123);
+
+endmodule

src/verilog/expr2verilog.cpp

@@ -1251,6 +1251,14 @@ std::string expr2verilogt::convert(const typet &type)
   {
     return "enum";
   }
+  else if(type.id() == ID_struct)
+  {
+    return "struct";
+  }
+  else if(type.id() == ID_union)
+  {
+    return "union";
+  }
   else if(type.id() == ID_verilog_type_reference)
   {
     auto &type_reference = to_verilog_type_reference(type);

src/verilog/parser.y

@@ -978,6 +978,11 @@ property_qualifier:
 	| class_item_qualifier
 	;
 
+random_qualifier_opt:
+	  /* Optional */
+	| random_qualifier
+	;
+
 random_qualifier:
 	  TOK_RAND
 	| TOK_RANDC
@@ -1250,8 +1255,9 @@ data_type:
                 }
 	| non_integer_type
 	| struct_union packed_opt signing_opt 
-	  '{' struct_union_member_list '}' packed_dimension_brace
-	        { /* todo */ }
+	  '{' struct_union_member_brace '}' packed_dimension_brace
+	        { $$=$1;
+	          addswap($$, ID_declaration_list, $5); }
 	| TOK_ENUM enum_base_type_opt '{' enum_name_declaration_list '}'
 	        { // Like in C, these do _not_ create a scope.
 	          // The enum names go into the current scope.
@@ -1330,7 +1336,20 @@ integer_atom_type:
 class_type: class_identifier
 	;
 
-struct_union_member_list:
+struct_union_member_brace:
+	  /* Not optional! No empty structs. */
+	  struct_union_member
+		{ init($$); mts($$, $1); }
+	| struct_union_member_brace struct_union_member
+		{ $$=$1; mts($$, $2); }
+	;
+
+struct_union_member:
+	  attribute_instance_brace
+	  random_qualifier_opt
+	  data_type_or_void
+	  list_of_variable_decl_assignments ';'
+		{ $$=$4; stack_expr($$).id(ID_decl); addswap($$, ID_type, $3); }
 	;
 
 enum_base_type_opt:

src/verilog/verilog_expr.h

@@ -402,55 +402,59 @@ inline verilog_set_genvarst &to_verilog_set_genvars(exprt &expr)
   return static_cast<verilog_set_genvarst &>(expr);
 }
 
-class verilog_parameter_declt : public verilog_module_itemt
+// This class is used for all declarators in the parse tree
+class verilog_declaratort : public exprt
 {
 public:
-  inline verilog_parameter_declt() : verilog_module_itemt(ID_parameter_decl)
+  const irep_idt &identifier() const
   {
+    return get(ID_identifier);
   }
 
-  class declaratort : public exprt
+  void identifier(irep_idt _identifier)
   {
-  public:
-    const irep_idt &identifier() const
-    {
-      return get(ID_identifier);
-    }
+    set(ID_identifier, _identifier);
+  }
 
-    void identifier(irep_idt _identifier)
-    {
-      set(ID_identifier, _identifier);
-    }
+  const irep_idt &base_name() const
+  {
+    return get(ID_base_name);
+  }
 
-    const irep_idt &base_name() const
-    {
-      return get(ID_base_name);
-    }
+  const exprt &value() const
+  {
+    return static_cast<const exprt &>(find(ID_value));
+  }
 
-    const exprt &value() const
-    {
-      return static_cast<const exprt &>(find(ID_value));
-    }
+  exprt &value()
+  {
+    return static_cast<exprt &>(add(ID_value));
+  }
 
-    exprt &value()
-    {
-      return static_cast<exprt &>(add(ID_value));
-    }
+  bool has_value() const
+  {
+    return find(ID_value).is_not_nil();
+  }
 
-    bool has_value() const
-    {
-      return find(ID_value).is_not_nil();
-    }
+  // helper to generate a symbol expression
+  symbol_exprt symbol_expr() const
+  {
+    return symbol_exprt(identifier(), type())
+      .with_source_location<symbol_exprt>(*this);
+  }
+};
 
-    // helper to generate a symbol expression
-    symbol_exprt symbol_expr() const
-    {
-      return symbol_exprt(identifier(), type())
-        .with_source_location<symbol_exprt>(*this);
-    }
-  };
+using verilog_declaratorst = std::vector<verilog_declaratort>;
+
+class verilog_parameter_declt : public verilog_module_itemt
+{
+public:
+  inline verilog_parameter_declt() : verilog_module_itemt(ID_parameter_decl)
+  {
+  }
 
-  using declaratorst = std::vector<declaratort>;
+  using declaratort = verilog_declaratort;
+  using declaratorst = verilog_declaratorst;
 
   const declaratorst &declarations() const
   {
@@ -484,8 +488,8 @@ class verilog_local_parameter_declt : public verilog_module_itemt
   {
   }
 
-  using declaratort = verilog_parameter_declt::declaratort;
-  using declaratorst = std::vector<declaratort>;
+  using declaratort = verilog_declaratort;
+  using declaratorst = verilog_declaratorst;
 
   const declaratorst &declarations() const
   {
@@ -516,7 +520,7 @@ class verilog_lett : public verilog_module_itemt
 {
 public:
   // These have a single declarator.
-  using declaratort = verilog_parameter_declt::declaratort;
+  using declaratort = verilog_declaratort;
 
   const declaratort &declarator() const
   {
@@ -700,8 +704,8 @@ class verilog_declt:public verilog_statementt
   }
 
   // When it's not a function or task, there are declarators.
-  using declaratort = verilog_parameter_declt::declaratort;
-  using declaratorst = verilog_parameter_declt::declaratorst;
+  using declaratort = verilog_declaratort;
+  using declaratorst = verilog_declaratorst;
 
   declaratorst &declarators()
   {

src/verilog/verilog_synthesis.cpp

@@ -564,6 +564,31 @@ void verilog_synthesist::assignment_rec(
 
     new_value.swap(last_value);
   }
+  else if(lhs.id() == ID_member)
+  {
+    const auto &member_expr = to_member_expr(lhs);
+    const exprt &lhs_compound = member_expr.struct_op();
+    auto component_name = member_expr.get_component_name();
+
+    if(lhs_compound.type().id() == ID_struct)
+    {
+      // turn
+      //   s.m=e
+      // into
+      //   s'==s WITH [m:=e]
+      auto synth_compound = synth_expr(lhs_compound, symbol_statet::FINAL);
+
+      with_exprt new_rhs{
+        synth_compound, member_designatort{component_name}, rhs};
+
+      // recursive call
+      assignment_rec(lhs_compound, new_rhs, new_value); // recursive call
+    }
+    else
+    {
+      throw errort() << "unexpected member lhs: " << lhs_compound.type().id();
+    }
+  }
   else
   {
     throw errort() << "unexpected lhs: " << lhs.id();
@@ -723,6 +748,10 @@ void verilog_synthesist::assignment_member_rec(
 
     member.pop_back();
   }
+  else if(lhs.id() == ID_member)
+  {
+    add_assignment_member(lhs, member, data);
+  }
   else
   {
     throw errort() << "unexpected lhs: " << lhs.id();
@@ -854,9 +883,14 @@ const symbolt &verilog_synthesist::assignment_symbol(const exprt &lhs)
 
       return it->second;
     }
+    else if(e->id() == ID_member)
+    {
+      e = &to_member_expr(*e).struct_op();
+    }
     else
     {
-      throw errort() << "synthesis: failed to get identifier";
+      throw errort().with_location(e->source_location())
+        << "synthesis: failed to get identifier";
     }
   }
 }

src/verilog/verilog_typecheck.cpp

@@ -805,6 +805,10 @@ void verilog_typecheckt::check_lhs(
       break;
     }
   }
+  else if(lhs.id() == ID_member)
+  {
+    check_lhs(to_member_expr(lhs).struct_op(), vassign);
+  }
   else
   {
     throw errort() << "typechecking: failed to get identifier on LHS "

src/verilog/verilog_typecheck_base.cpp

@@ -182,6 +182,15 @@ std::size_t verilog_typecheck_baset::get_width(const typet &type)
     return (array_size(to_array_type(type)) * element_width).to_ulong();
   }
 
+  if(type.id() == ID_struct)
+  {
+    // add them up
+    mp_integer sum = 0;
+    for(auto &component : to_struct_type(type).components())
+      sum += get_width(component.type());
+    return sum.to_ulong();
+  }
+
   if(type.id() == ID_verilog_shortint)
     return 16;
   else if(type.id() == ID_verilog_int)