From 90aefcc3e83ae2c95edf871cdc0bbe480e5e2f5d Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 15 Dec 2025 19:51:14 -0800
Subject: [PATCH] Verilog: format struct expressions

This adds a Verilog formatter for struct constructor expressions.
---
 .../verilog/expressions/static_cast4.desc     |  1 +
 src/verilog/expr2verilog.cpp                  | 42 +++++++++++++++++++
 src/verilog/expr2verilog_class.h              |  2 +
 3 files changed, 45 insertions(+)

diff --git a/regression/verilog/expressions/static_cast4.desc b/regression/verilog/expressions/static_cast4.desc
index 8a353d973..db66f2ac3 100644
--- a/regression/verilog/expressions/static_cast4.desc
+++ b/regression/verilog/expressions/static_cast4.desc
@@ -1,6 +1,7 @@
 CORE
 static_cast4.sv
 --module main
+^\[.*\] struct packed'\('\{ a: 1, b: 2 \}\) == main\.some_struct: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index 8674feba9..d723b14f5 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -1540,6 +1540,43 @@ expr2verilogt::resultt expr2verilogt::convert_sequence_property_instance(
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_struct
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt expr2verilogt::convert_struct(const struct_exprt &src)
+{
+  std::string dest = "'{";
+
+  auto &type = to_struct_type(src.type());
+  DATA_INVARIANT(
+    type.components().size() == src.operands().size(),
+    "number of compontents must match");
+
+  for(std::size_t index = 0; index < src.operands().size(); index++)
+  {
+    auto &op = src.operands()[index];
+    if(index != 0)
+      dest += ',';
+    dest += ' ';
+    dest += id2string(type.components()[index].get_name());
+    dest += ": ";
+    dest += convert_rec(op).s;
+  }
+
+  dest += " }";
+
+  return {verilog_precedencet::MAX, dest};
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_value_range
 
   Inputs:
@@ -2081,6 +2118,11 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
       to_sva_sequence_property_instance_expr(src));
   }
 
+  else if(src.id() == ID_struct)
+  {
+    return convert_struct(to_struct_expr(src));
+  }
+
   // no VERILOG language expression for internal representation
   return convert_norep(src);
 }
diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h
index f06989bf6..0b9c79746 100644
--- a/src/verilog/expr2verilog_class.h
+++ b/src/verilog/expr2verilog_class.h
@@ -187,6 +187,8 @@ class expr2verilogt
   resultt convert_sequence_property_instance(
     const class sva_sequence_property_instance_exprt &);
 
+  resultt convert_struct(const struct_exprt &);
+
 protected:
   const namespacet &ns;
 };