From 8e853e0b6d987a09360ee2dba4e35553ba160009 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 5 Oct 2025 19:36:30 -0700
Subject: [PATCH] Verilog: packed/unpacked structs

This adds enforcement that only packed structs convert to bit-vector types.
---
 regression/verilog/structs/structs4.sv           |  2 +-
 regression/verilog/structs/unpacked_struct1.desc |  7 +++++++
 regression/verilog/structs/unpacked_struct1.sv   | 11 +++++++++++
 src/verilog/expr2verilog.cpp                     |  5 ++++-
 src/verilog/parser.y                             |  2 ++
 src/verilog/verilog_elaborate_type.cpp           | 10 ++++++++--
 src/verilog/verilog_typecheck_expr.cpp           |  2 +-
 7 files changed, 34 insertions(+), 5 deletions(-)
 create mode 100644 regression/verilog/structs/unpacked_struct1.desc
 create mode 100644 regression/verilog/structs/unpacked_struct1.sv

diff --git a/regression/verilog/structs/structs4.sv b/regression/verilog/structs/structs4.sv
index 0cb9c4441..af4887a73 100644
--- a/regression/verilog/structs/structs4.sv
+++ b/regression/verilog/structs/structs4.sv
@@ -12,7 +12,7 @@ module main;
     s.field3 = 'b1110011;
   end
 
-  // structs can be converted without cast to bit-vectors
+  // packed structs can be converted without cast to bit-vectors
   wire [8:0] w = s;
 
   // Expected to pass.
diff --git a/regression/verilog/structs/unpacked_struct1.desc b/regression/verilog/structs/unpacked_struct1.desc
new file mode 100644
index 000000000..0046665da
--- /dev/null
+++ b/regression/verilog/structs/unpacked_struct1.desc
@@ -0,0 +1,7 @@
+CORE
+unpacked_struct1.sv
+
+^file .* line 9: failed to convert `struct' to `\[8:0\]'$
+^EXIT=2$
+^SIGNAL=0$
+--
diff --git a/regression/verilog/structs/unpacked_struct1.sv b/regression/verilog/structs/unpacked_struct1.sv
new file mode 100644
index 000000000..edc3d3ad8
--- /dev/null
+++ b/regression/verilog/structs/unpacked_struct1.sv
@@ -0,0 +1,11 @@
+module main;
+
+  // an unpacked struct
+  struct {
+    bit field;
+  } s;
+
+  // unpacked structs cannot be converted to bit-vectors
+  wire [8:0] w = s;
+
+endmodule
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index c7160b7ce..832e887a3 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -2149,7 +2149,10 @@ std::string expr2verilogt::convert(const typet &type)
   }
   else if(type.id() == ID_struct)
   {
-    return "struct";
+    if(type.get_bool(ID_packed))
+      return "struct packed";
+    else
+      return "struct";
   }
   else if(type.id() == ID_union)
   {
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index 1c8763280..b667c18a7 100644
--- a/src/verilog/parser.y
+++ b/src/verilog/parser.y
@@ -1552,6 +1552,8 @@ data_type:
 	| struct_union packed_opt signing_opt 
 	  '{' struct_union_member_brace '}' packed_dimension_brace
 	        { $$=$1;
+	          if(stack_expr($2).id() == ID_packed)
+	            stack_type($1).set(ID_packed, true);
 	          addswap($$, ID_declaration_list, $5); }
 	| TOK_ENUM enum_base_type_opt '{' enum_name_declaration_list '}'
 	        { // Like in C, these do _not_ create a scope.
diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp
index 26452e8f5..545e3b2fe 100644
--- a/src/verilog/verilog_elaborate_type.cpp
+++ b/src/verilog/verilog_elaborate_type.cpp
@@ -425,8 +425,14 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
       }
     }
 
-    return struct_union_typet{src.id(), std::move(components)}
-      .with_source_location(src.source_location());
+    auto result =
+      struct_union_typet{src.id(), std::move(components)}.with_source_location(
+        src.source_location());
+
+    if(src.get_bool(ID_packed))
+      result.set(ID_packed, true);
+
+    return result;
   }
   else if(src.id() == ID_verilog_string)
   {
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index 1c9d3f30e..f58ab62c9 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -2481,7 +2481,7 @@ void verilog_typecheck_exprt::struct_decay(exprt &expr) const
   // Verilog packed struct 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_struct)
+  if(type.id() == ID_struct && type.get_bool(ID_packed))
   {
     auto new_type =
       unsignedbv_typet{numeric_cast_v<std::size_t>(get_width(type))};