From 6c6f411f81b4ef358db5ce057efe11811f299c06 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 24 Nov 2024 09:34:56 +0000
Subject: [PATCH] Verilog: lowering for types

---
 src/verilog/verilog_lowering.cpp  | 8 ++++++++
 src/verilog/verilog_lowering.h    | 2 ++
 src/verilog/verilog_synthesis.cpp | 4 ++++
 3 files changed, 14 insertions(+)

diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp
index 67f85b71..8d0b8330 100644
--- a/src/verilog/verilog_lowering.cpp
+++ b/src/verilog/verilog_lowering.cpp
@@ -416,3 +416,11 @@ exprt verilog_lowering(exprt expr)
 
   UNREACHABLE;
 }
+
+typet verilog_lowering(typet type)
+{
+  if(type.id() == ID_verilog_signedbv || type.id() == ID_verilog_unsignedbv)
+    return lower_to_aval_bval(type);
+  else
+    return type;
+}
diff --git a/src/verilog/verilog_lowering.h b/src/verilog/verilog_lowering.h
index 4f31d1d6..cdaa7c4b 100644
--- a/src/verilog/verilog_lowering.h
+++ b/src/verilog/verilog_lowering.h
@@ -10,7 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_VERILOG_LOWERING_H
 
 class exprt;
+class typet;
 
 exprt verilog_lowering(exprt);
+typet verilog_lowering(typet);
 
 #endif
diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp
index 6956a1d4..a3f76ec8 100644
--- a/src/verilog/verilog_synthesis.cpp
+++ b/src/verilog/verilog_synthesis.cpp
@@ -3314,6 +3314,10 @@ exprt verilog_synthesist::symbol_expr(
 {
   exprt result=exprt(curr_or_next==NEXT?ID_next_symbol:ID_symbol, symbol.type);
   result.set(ID_identifier, symbol.name);
+
+  // The type may need to be lowered
+  result.type() = verilog_lowering(result.type());
+
   return result;
 }