SystemVerilog: structs

This adds support for SystemVerilog struct types.

Author: kroening

regression/verilog/structs/structs1.desc

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

regression/verilog/structs/structs1.sv

@@ -0,0 +1,14 @@
+module main;
+
+  // The first field is the most-significant bit.
+  struct packed {
+    bit field1, field2;
+    bit [6:0] field3;
+  } s = 'b1011111;
+
+  // Expected to pass.
+  p1: assert property (s.field1 == 1);
+  p2: assert property (s.field2 == 0);
+  p3: assert property (s.field3 == 'b111111);
+
+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_typecheck_expr.cpp

@@ -954,6 +954,11 @@ exprt verilog_typecheck_exprt::convert_hierarchical_identifier(
         << "identifier `" << rhs_identifier << "' not found in named block";
     }
   }
+  else if(
+    expr.lhs().type().id() == ID_struct || expr.lhs().type().id() == ID_union)
+  {
+    throw errort().with_location(expr.source_location()) << "TBD";
+  }
   else  
   {
     throw errort().with_location(expr.source_location())
@@ -1490,23 +1495,25 @@ void verilog_typecheck_exprt::implicit_typecast(
   if(dest_type.id()==irep_idt())
     return;
 
+  const typet &src_type = expr.type();
+
   auto &verilog_dest_type = dest_type.get(ID_C_verilog_type);
   if(verilog_dest_type == ID_verilog_enum)
   {
     // IEEE 1800-2017 6.19.3: "a variable of type enum cannot be directly
     // assigned a value that lies outside the enumeration set unless an
     // explicit cast is used"
     if(
-      expr.type().get(ID_C_verilog_type) != ID_verilog_enum ||
-      expr.type().get(ID_C_identifier) != dest_type.get(ID_C_identifier))
+      src_type.get(ID_C_verilog_type) != ID_verilog_enum ||
+      src_type.get(ID_C_identifier) != dest_type.get(ID_C_identifier))
     {
       throw errort().with_location(expr.source_location())
         << "assignment to enum requires enum of the same type, but got "
         << to_string(expr.type());
     }
   }
 
-  if(expr.type()==dest_type)
+  if(src_type==dest_type)
     return;
 
   if(dest_type.id() == ID_integer)
@@ -1527,15 +1534,15 @@ void verilog_typecheck_exprt::implicit_typecast(
     }
 
     if(
-      expr.type().id() == ID_bool || expr.type().id() == ID_unsignedbv ||
-      expr.type().id() == ID_signedbv || expr.type().id() == ID_integer)
+      src_type.id() == ID_bool || src_type.id() == ID_unsignedbv ||
+      src_type.id() == ID_signedbv || src_type.id() == ID_integer)
     {
       expr = typecast_exprt{expr, dest_type};
       return;
     }
   }
 
-  if(expr.type().id() == ID_integer)
+  if(src_type.id() == ID_integer)
   {
     // from integer to s.th. else
     if(dest_type.id()==ID_bool)
@@ -1558,19 +1565,20 @@ void verilog_typecheck_exprt::implicit_typecast(
       return;
     }
   }
-  else if(expr.type().id()==ID_bool ||
-          expr.type().id()==ID_unsignedbv ||
-          expr.type().id()==ID_signedbv ||
-          expr.type().id()==ID_verilog_unsignedbv ||
-          expr.type().id()==ID_verilog_signedbv)
+  else if(src_type.id()==ID_bool ||
+          src_type.id()==ID_unsignedbv ||
+          src_type.id()==ID_signedbv ||
+          src_type.id()==ID_verilog_unsignedbv ||
+          src_type.id()==ID_verilog_signedbv)
   {
+    // from bits to s.th. else
     if(dest_type.id()==ID_bool)
     {
       // do not use typecast here
       // we actually only want the lowest bit
 
       if(expr.is_constant() &&
-         expr.type().id()==ID_unsignedbv)
+         src_type.id()==ID_unsignedbv)
       {
         const std::string &value=expr.get_string(ID_value);
         // least significant bit is last
@@ -1614,10 +1622,29 @@ void verilog_typecheck_exprt::implicit_typecast(
       expr = typecast_exprt{expr, dest_type};
       return;
     }
+    else if(dest_type.id() == ID_struct)
+    {
+      // bit-vectors can be converted to packed structs
+      expr = typecast_exprt{expr, dest_type};
+      return;
+    }
+  }
+  else if(src_type.id() == ID_struct)
+  {
+    // packed structs can be converted to bits
+    if(
+      dest_type.id() == ID_bool || dest_type.id() == ID_unsignedbv ||
+      dest_type.id() == ID_signedbv ||
+      dest_type.id() == ID_verilog_unsignedbv ||
+      dest_type.id() == ID_verilog_signedbv)
+    {
+      expr = typecast_exprt{expr, dest_type};
+      return;
+    }
   }
 
   throw errort().with_location(expr.source_location())
-    << "failed to convert `" << to_string(expr.type()) << "' to `"
+    << "failed to convert `" << to_string(src_type) << "' to `"
     << to_string(dest_type) << "'";
 }
 

src/verilog/verilog_typecheck_type.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "verilog_typecheck_expr.h"
 
+#include "verilog_expr.h"
 #include "verilog_types.h"
 
 /*******************************************************************\
@@ -180,6 +181,35 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
     // recursive call
     return convert_type(to_to_be_elaborated_type(src).subtype());
   }
+  else if(src.id() == ID_struct || src.id() == ID_union)
+  {
+    // the declarations of the components
+    auto &declaration_list = src.find(ID_declaration_list).get_sub();
+    struct_union_typet::componentst components;
+
+    for(auto &declaration : declaration_list)
+    {
+      auto &declaration_expr = static_cast<const exprt &>(declaration);
+      DATA_INVARIANT(
+        declaration.id() == ID_decl, "struct type must have declarations");
+      // Convert the type
+      auto type = convert_type(declaration_expr.type());
+      // Convert the declarators
+      for(auto &declarator_expr : declaration_expr.operands())
+      {
+        auto &declarator = static_cast<const verilog_declaratort &>(declarator_expr);
+        struct_union_typet::componentt component;
+        component.add_source_location() = declarator.source_location();
+        component.type() = type;
+        component.set_base_name(declarator.base_name());
+        component.set_name(declarator.base_name());
+        components.push_back(std::move(component));
+      }
+    }
+
+    return struct_union_typet{src.id(), std::move(components)}
+      .with_source_location(src.source_location());
+  }
   else
   {
     throw errort().with_location(source_location)