SystemVerilog Unions

regression/verilog/unions/unions1.desc

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

regression/verilog/unions/unions1.sv

@@ -0,0 +1,16 @@
+module main;
+
+  union packed {
+    bit [6:0] field1;
+    bit [6:0] field2;
+  } u;
+
+  // bit-vectors can be converted without cast to packed unions
+  initial u = 7'b1010101;
+
+  // Expected to pass.
+  p0: assert property ($bits(u) == 7);
+  p1: assert property (u.field1 == 7'b1010101);
+  p2: assert property (u.field2 == 7'b1010101);
+
+endmodule

regression/verilog/unions/unions2.desc

@@ -0,0 +1,7 @@
+CORE
+unions2.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/verilog/unions/unions2.sv

@@ -0,0 +1,18 @@
+module main;
+
+  union {
+    bit field1;
+    bit [6:0] field2;
+  } u;
+
+  initial begin
+    u.field2 = 0;
+    u.field1 = 1;
+  end
+
+  // Expected to pass.
+  p1: assert property (u.field1 == 1);
+  p2: assert property (u.field2 == 1);
+  p3: assert property ($bits(u) == 7);
+
+endmodule

regression/verilog/unions/unions3.desc

@@ -0,0 +1,7 @@
+CORE
+unions3.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/verilog/unions/unions3.sv

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

src/hw_cbmc_irep_ids.h

@@ -149,6 +149,7 @@ IREP_ID_ONE(wand)
 IREP_ID_ONE(automatic)
 IREP_ID_TWO(C_verilog_type, #verilog_type)
 IREP_ID_ONE(verilog_enum)
+IREP_ID_ONE(verilog_packed)
 IREP_ID_ONE(verilog_packed_array)
 IREP_ID_ONE(verilog_type_reference)
 IREP_ID_ONE(verilog_unpacked_array)

src/verilog/verilog_synthesis.cpp

@@ -831,7 +831,9 @@ void verilog_synthesist::assignment_rec(
     const exprt &lhs_compound = member_expr.struct_op();
     auto component_name = member_expr.get_component_name();
 
-    if(lhs_compound.type().id() == ID_struct)
+    if(
+      lhs_compound.type().id() == ID_struct ||
+      lhs_compound.type().id() == ID_union)
     {
       // turn
       //   s.m=e

src/verilog/verilog_typecheck_base.cpp

@@ -6,15 +6,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <cassert>
+#include "verilog_typecheck_base.h"
 
 #include <util/ebmc_util.h>
 #include <util/expr_util.h>
 #include <util/prefix.h>
 #include <util/std_types.h>
 
 #include "expr2verilog.h"
-#include "verilog_typecheck_base.h"
+#include "verilog_types.h"
+
+#include <cassert>
 
 /*******************************************************************\
 
@@ -157,7 +159,7 @@ mp_integer verilog_typecheck_baset::array_offset(const array_typet &type)
 
 /*******************************************************************\
 
-Function: verilog_typecheck_baset::get_width
+Function: verilog_typecheck_baset::get_width_opt
 
   Inputs:
 
@@ -167,7 +169,8 @@ Function: verilog_typecheck_baset::get_width
 
 \*******************************************************************/
 
-mp_integer verilog_typecheck_baset::get_width(const typet &type)
+std::optional<mp_integer>
+verilog_typecheck_baset::get_width_opt(const typet &type)
 {
   if(type.id()==ID_bool)
     return 1;
@@ -178,19 +181,36 @@ mp_integer verilog_typecheck_baset::get_width(const typet &type)
 
   if(type.id()==ID_array)
   {
-    mp_integer element_width = get_width(to_array_type(type).element_type());
-    return (array_size(to_array_type(type)) * element_width).to_ulong();
+    auto element_width = get_width_opt(to_array_type(type).element_type());
+    if(element_width.has_value())
+      return array_size(to_array_type(type)) * element_width.value();
+    else
+      return {};
   }
 
   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());
+    {
+      auto component_width = get_width_opt(component.type());
+      if(!component_width.has_value())
+        return {};
+      sum += *component_width;
+    }
     return sum;
   }
 
+  if(type.id() == ID_union)
+  {
+    // find the biggest
+    mp_integer max = 0;
+    for(auto &component : to_verilog_union_type(type).components())
+      max = std::max(max, get_width(component.type()));
+    return max;
+  }
+
   if(type.id() == ID_verilog_shortint)
     return 16;
   else if(type.id() == ID_verilog_int)
@@ -202,8 +222,30 @@ mp_integer verilog_typecheck_baset::get_width(const typet &type)
   else if(type.id() == ID_verilog_time)
     return 64;
 
-  throw errort().with_location(type.source_location())
-    << "type `" << type.id() << "' has unknown width";
+  return {};
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheck_baset::get_width
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+mp_integer verilog_typecheck_baset::get_width(const typet &type)
+{
+  auto width_opt = get_width_opt(type);
+
+  if(width_opt.has_value())
+    return std::move(width_opt.value());
+  else
+    throw errort().with_location(type.source_location())
+      << "type `" << type.id() << "' has unknown width";
 }
 
 /*******************************************************************\

src/verilog/verilog_typecheck_base.h

@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_VERILOG_TYPECHEK_BASE_H
 #define CPROVER_VERILOG_TYPECHEK_BASE_H
 
+#include <util/expr.h>
 #include <util/mp_arith.h>
 #include <util/namespace.h>
 #include <util/typecheck.h>
@@ -44,14 +45,16 @@ class verilog_typecheck_baset:public typecheckt
   const namespacet &ns;
   const irep_idt mode;
 
-  mp_integer get_width(const exprt &expr)
+  static mp_integer get_width(const exprt &expr)
   {
     return get_width(expr.type());
   }
-  mp_integer get_width(const typet &type);
-  mp_integer array_size(const array_typet &);
-  mp_integer array_offset(const array_typet &);
-  typet index_type(const array_typet &);
+
+  static mp_integer get_width(const typet &);
+  static std::optional<mp_integer> get_width_opt(const typet &);
+  static mp_integer array_size(const array_typet &);
+  static mp_integer array_offset(const array_typet &);
+  static typet index_type(const array_typet &);
 };
 
 #endif

src/verilog/verilog_typecheck_expr.cpp

@@ -434,7 +434,7 @@ Function: verilog_typecheck_exprt::bits
 
 exprt verilog_typecheck_exprt::bits(const exprt &expr)
 {
-  auto width_opt = bits_rec(expr.type());
+  auto width_opt = get_width_opt(expr.type());
 
   if(!width_opt.has_value())
   {
@@ -447,57 +447,6 @@ exprt verilog_typecheck_exprt::bits(const exprt &expr)
 
 /*******************************************************************\
 
-Function: verilog_typecheck_exprt::bits_rec
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-std::optional<mp_integer>
-verilog_typecheck_exprt::bits_rec(const typet &type) const
-{
-  if(type.id() == ID_bool)
-    return 1;
-  else if(type.id() == ID_unsignedbv)
-    return to_unsignedbv_type(type).get_width();
-  else if(type.id() == ID_signedbv)
-    return to_signedbv_type(type).get_width();
-  else if(type.id() == ID_integer)
-    return 32;
-  else if(type.id() == ID_array)
-  {
-    auto &array_type = to_array_type(type);
-    auto size_int =
-      numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
-    auto element_bits_opt = bits_rec(array_type.element_type());
-    if(element_bits_opt.has_value())
-      return element_bits_opt.value() * size_int;
-    else
-      return {};
-  }
-  else if(type.id() == ID_struct)
-  {
-    auto &struct_type = to_struct_type(type);
-    mp_integer sum = 0;
-    for(auto &component : struct_type.components())
-    {
-      auto component_bits_opt = bits_rec(component.type());
-      if(!component_bits_opt.has_value())
-        return component_bits_opt.value();
-      sum += component_bits_opt.value();
-    }
-    return sum;
-  }
-  else
-    return {};
-}
-
-/*******************************************************************\
-
 Function: verilog_typecheck_exprt::convert_system_function
 
   Inputs:
@@ -1644,16 +1593,17 @@ void verilog_typecheck_exprt::implicit_typecast(
       expr = typecast_exprt{expr, dest_type};
       return;
     }
-    else if(dest_type.id() == ID_struct)
+    else if(dest_type.id() == ID_struct || dest_type.id() == ID_union)
     {
-      // bit-vectors can be converted to packed structs
+      // bit-vectors can be converted to
+      // packed structs and packed unions
       expr = typecast_exprt{expr, dest_type};
       return;
     }
   }
-  else if(src_type.id() == ID_struct)
+  else if(src_type.id() == ID_struct || src_type.id() == ID_union)
   {
-    // packed structs can be converted to bits
+    // packed structs and packed unions can be converted to bits
     if(
       dest_type.id() == ID_bool || dest_type.id() == ID_unsignedbv ||
       dest_type.id() == ID_signedbv ||

src/verilog/verilog_types.h

@@ -484,4 +484,59 @@ inline verilog_type_referencet &to_verilog_type_reference(typet &type)
   return static_cast<verilog_type_referencet &>(type);
 }
 
+/// The SystemVerilog struct/union type
+class verilog_struct_union_typet : public struct_union_typet
+{
+public:
+  verilog_struct_union_typet(
+    irep_idt __id,
+    bool __is_packed,
+    componentst _components)
+    : struct_union_typet(__id, std::move(_components))
+  {
+    is_packed(__is_packed);
+  }
+
+  bool is_packed() const
+  {
+    return get_bool(ID_verilog_packed);
+  }
+
+  void is_packed(bool __is_packed)
+  {
+    return set(ID_verilog_packed, __is_packed);
+  }
+};
+
+/// The SystemVerilog union type
+class verilog_union_typet : public verilog_struct_union_typet
+{
+public:
+  verilog_union_typet(bool __is_packed, componentst _components)
+    : verilog_struct_union_typet(ID_union, __is_packed, std::move(_components))
+  {
+  }
+};
+
+/// \brief Cast a typet to a \ref verilog_union_typet
+///
+/// This is an unchecked conversion. \a type must be known to be \ref
+/// verilog_union_typet. Will fail with a precondition violation if type
+/// doesn't match.
+///
+/// \param type: Source type.
+/// \return Object of type \ref verilog_union_typet
+inline const verilog_union_typet &to_verilog_union_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_union);
+  return static_cast<const verilog_union_typet &>(type);
+}
+
+/// \copydoc to_union_type(const typet &)
+inline verilog_union_typet &to_verilog_union_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_union);
+  return static_cast<verilog_union_typet &>(type);
+}
+
 #endif