From 8d5a7683b703c0c22fb1ea44caed5e2632330c61 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 22 Sep 2024 10:23:43 -0700
Subject: [PATCH] Verilog: one bit signed/unsigned types

This adds support for specifying 1-bit signed/unsigned types to
SystemVerilog frontend.
---
 regression/verilog/data-types/signed1.desc |  6 ++++++
 regression/verilog/data-types/signed1.sv   | 13 +++++++++++++
 src/verilog/verilog_elaborate_type.cpp     | 10 ++++++++++
 3 files changed, 29 insertions(+)
 create mode 100644 regression/verilog/data-types/signed1.desc
 create mode 100644 regression/verilog/data-types/signed1.sv

diff --git a/regression/verilog/data-types/signed1.desc b/regression/verilog/data-types/signed1.desc
new file mode 100644
index 000000000..893d20965
--- /dev/null
+++ b/regression/verilog/data-types/signed1.desc
@@ -0,0 +1,6 @@
+CORE
+signed1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/verilog/data-types/signed1.sv b/regression/verilog/data-types/signed1.sv
new file mode 100644
index 000000000..08ab50c23
--- /dev/null
+++ b/regression/verilog/data-types/signed1.sv
@@ -0,0 +1,13 @@
+module main;
+
+  wire signed one_bit_signed = -1;
+
+  assert final (one_bit_signed == -1);
+  assert final ($bits(one_bit_signed) == 1);
+
+  wire unsigned one_bit_unsigned = 1;
+
+  assert final (one_bit_unsigned == 1);
+  assert final ($bits(one_bit_unsigned) == 1);
+
+endmodule
diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp
index c9402f428..d1503dad3 100644
--- a/src/verilog/verilog_elaborate_type.cpp
+++ b/src/verilog/verilog_elaborate_type.cpp
@@ -166,6 +166,16 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
     // it's just a bit
     return bool_typet().with_source_location(source_location);
   }
+  else if(src.id() == ID_signed)
+  {
+    // one bit, signed
+    return signedbv_typet{1}.with_source_location(source_location);
+  }
+  else if(src.id() == ID_unsigned)
+  {
+    // one bit, unsigned
+    return unsignedbv_typet{1}.with_source_location(source_location);
+  }
   else if(src.id() == ID_verilog_byte)
   {
     return signedbv_typet{8}.with_source_location(source_location);