From aa53cdd637685435806e3bea1095e81a9bf0da5f Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 17 Jan 2025 09:26:01 -0800
Subject: [PATCH] Verilog: error on real operand for edge control

1800-2017 6.12.1 prohibits real operands given to edge control operators.
This adds an error message for this case.
---
 regression/verilog/synthesis/posedge_real.desc |  9 +++++++++
 regression/verilog/synthesis/posedge_real.v    |  7 +++++++
 src/verilog/verilog_typecheck_expr.cpp         | 11 +++++++++++
 3 files changed, 27 insertions(+)
 create mode 100644 regression/verilog/synthesis/posedge_real.desc
 create mode 100644 regression/verilog/synthesis/posedge_real.v

diff --git a/regression/verilog/synthesis/posedge_real.desc b/regression/verilog/synthesis/posedge_real.desc
new file mode 100644
index 00000000..bc67a01c
--- /dev/null
+++ b/regression/verilog/synthesis/posedge_real.desc
@@ -0,0 +1,9 @@
+CORE
+posedge_real.v
+--module main
+^file posedge_real.v line \d+: edge event controls do not take real operands$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/synthesis/posedge_real.v b/regression/verilog/synthesis/posedge_real.v
new file mode 100644
index 00000000..0f7b1aea
--- /dev/null
+++ b/regression/verilog/synthesis/posedge_real.v
@@ -0,0 +1,7 @@
+module main;
+
+  real data;
+
+  always @(posedge data);
+
+endmodule
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index ff15ec32..cac23447 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -2568,6 +2568,17 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
   else if(expr.id() == ID_posedge || expr.id() == ID_negedge)
   {
     convert_expr(expr.op());
+
+    // 1800-2017 6.12.1
+    // Edge event controls must not be given real operands.
+    if(
+      expr.op().type().id() == ID_verilog_shortreal ||
+      expr.op().type().id() == ID_verilog_real)
+    {
+      throw errort().with_location(expr.source_location())
+        << "edge event controls do not take real operands";
+    }
+
     expr.type() = bool_typet{};
   }
   else if(expr.id() == ID_verilog_smv_eventually)