SystemVerilog Unions

This adds basic support for SystemVerilog unions.

Author: kroening

lib/cbmc

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

regression/verilog/unions/unions1.desc

@@ -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/unions1.sv

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

regression/verilog/unions/unions2.desc

@@ -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/unions2.sv

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

regression/verilog/unions/unions3.desc

@@ -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

regression/verilog/unions/unions3.sv

@@ -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/hw_cbmc_irep_ids.h

@@ -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_synthesis.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>
 
 /*******************************************************************\
 
@@ -200,6 +202,15 @@ verilog_typecheck_baset::get_width_opt(const typet &type)
     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)