SystemVerilog Unions

kroening · kroening · commit 3cb42a891c22 · 2024-06-19T09:06:57.000-07:00
This adds basic support for SystemVerilog unions.
diff --git a/lib/cbmc b/lib/cbmc
@@ -1 +1 @@
-Subproject commit a8b8f0fd2ad2166d71ccce97dd6925198a018144
+Subproject commit 4f620a2e245e54a81b23566956f0388c03cb7739
diff --git a/regression/verilog/unions/unions1.desc b/regression/verilog/unions/unions1.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+unions1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+cast bitvector to union missing
diff --git a/regression/verilog/unions/unions1.sv b/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
diff --git a/regression/verilog/unions/unions2.desc b/regression/verilog/unions/unions2.desc
@@ -0,0 +1,7 @@
+CORE
+unions2.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/regression/verilog/unions/unions2.sv b/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
diff --git a/regression/verilog/unions/unions3.desc b/regression/verilog/unions/unions3.desc
@@ -0,0 +1,7 @@
+CORE
+unions3.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/regression/verilog/unions/unions3.sv b/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
diff --git a/src/hw_cbmc_irep_ids.h b/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)
diff --git a/src/verilog/verilog_synthesis.cpp b/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
diff --git a/src/verilog/verilog_typecheck_base.cpp b/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>
 
 /*******************************************************************\
 
@@ -191,6 +193,15 @@ mp_integer verilog_typecheck_baset::get_width(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)
diff --git a/src/verilog/verilog_typecheck_base.h b/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>
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
@@ -492,6 +492,19 @@ verilog_typecheck_exprt::bits_rec(const typet &type) const
     }
     return sum;
   }
+  else if(type.id() == ID_union)
+  {
+    auto &union_type = to_verilog_union_type(type);
+    mp_integer max = 0;
+    for(auto &component : union_type.components())
+    {
+      auto component_bits_opt = bits_rec(component.type());
+      if(!component_bits_opt.has_value())
+        return component_bits_opt.value();
+      max = std::max(max, component_bits_opt.value());
+    }
+    return max;
+  }
   else
     return {};
 }
@@ -1644,16 +1657,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 ||
diff --git a/src/verilog/verilog_types.h b/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
