SystemVerilog: conversion from/to packed union

regression/verilog/unions/unions1.desc

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

regression/verilog/unions/unions4.desc

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

regression/verilog/unions/unions4.sv

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

src/verilog/verilog_synthesis.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
+#include <util/c_types.h>
 #include <util/ebmc_util.h>
 #include <util/expr_util.h>
 #include <util/identifier.h>
@@ -113,6 +114,21 @@ exprt verilog_synthesist::from_bitvector(
 
     return struct_exprt{std::move(field_values), struct_type};
   }
+  else if(dest.id() == ID_union)
+  {
+    // We use the first field of the union.
+    // All fields of a SystemVerilog packed union must have the same width.
+    const auto &union_type = to_union_type(dest);
+    DATA_INVARIANT(
+      !union_type.components().empty(),
+      "union type must have at least one field");
+    auto &field = union_type.components().front();
+
+    // rec. call
+    auto field_value = from_bitvector(src, offset, field.type());
+
+    return union_exprt{field.get_name(), std::move(field_value), union_type};
+  }
   else
   {
     return extract(src, offset, dest);
@@ -152,6 +168,16 @@ exprt verilog_synthesist::to_bitvector(const exprt &src)
     auto width_int = numeric_cast_v<std::size_t>(get_width(src));
     return concatenation_exprt{std::move(field_values), bv_typet{width_int}};
   }
+  else if(src_type.id() == ID_union)
+  {
+    const auto &union_type = to_union_type(src_type);
+    DATA_INVARIANT(
+      !union_type.components().empty(),
+      "union type must have at least one field");
+    auto &field = union_type.components().front();
+    auto member = member_exprt{src, field};
+    return to_bitvector(member); // rec. call
+  }
   else
   {
     return src;
@@ -302,13 +328,13 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
         auto aval_bval_type = lower_to_aval_bval(dest_type);
         return aval_bval_conversion(typecast_expr.op(), aval_bval_type);
       }
-      else if(dest_type.id() == ID_struct)
+      else if(dest_type.id() == ID_struct || dest_type.id() == ID_union)
       {
         return from_bitvector(typecast_expr.op(), 0, dest_type);
       }
       else
       {
-        if(src_type.id() == ID_struct)
+        if(src_type.id() == ID_struct || src_type.id() == ID_union)
         {
           return extract(to_bitvector(typecast_expr.op()), 0, dest_type);
         }

src/verilog/verilog_typecheck_expr.cpp

@@ -2144,6 +2144,34 @@ typet verilog_typecheck_exprt::enum_decay(const typet &type)
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::union_decay
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void verilog_typecheck_exprt::union_decay(exprt &expr) const
+{
+  // 1800-2017 7.3.1
+  // Verilog union types decay to a vector type [$bits(t)-1:0] when
+  // used in relational or arithmetic expressions.
+  auto &type = expr.type();
+  if(type.id() == ID_union)
+  {
+    auto new_type =
+      unsignedbv_typet{numeric_cast_v<std::size_t>(get_width(type))};
+    // The synthesis stage turns these typecasts into a member
+    // expression.
+    expr = typecast_exprt{expr, new_type};
+  }
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::tc_binary_expr
 
   Inputs:
@@ -2158,6 +2186,9 @@ void verilog_typecheck_exprt::tc_binary_expr(
   const exprt &expr,
   exprt &op0, exprt &op1)
 {
+  union_decay(op0);
+  union_decay(op1);
+
   // follows 1800-2017 11.8.2
   const typet new_type =
     max_type(enum_decay(op0.type()), enum_decay(op1.type()));
@@ -2223,6 +2254,9 @@ void verilog_typecheck_exprt::typecheck_relation(binary_exprt &expr)
   auto &lhs = expr.lhs();
   auto &rhs = expr.rhs();
 
+  union_decay(lhs);
+  union_decay(rhs);
+
   // Relations are special-cased in 1800-2017 11.8.2.
   const typet new_type =
     max_type(enum_decay(lhs.type()), enum_decay(rhs.type()));

src/verilog/verilog_typecheck_expr.h

@@ -136,6 +136,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   }
 
   static typet enum_decay(const typet &);
+  void union_decay(exprt &) const;
   typet max_type(const typet &t1, const typet &t2);
 
   // named blocks