From 76d3b1c33e1aa21a9a6d25d143d15a18387b2706 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 17 Jan 2025 07:30:31 -0800
Subject: [PATCH] SVA: error message non-constant SVA cycle delays

Replicates third example in #931.
---
 regression/verilog/SVA/cycle_delay1.desc |  9 +++++++++
 regression/verilog/SVA/cycle_delay1.sv   | 11 +++++++++++
 regression/verilog/SVA/unbounded1.desc   |  2 +-
 src/verilog/verilog_typecheck_sva.cpp    |  8 ++++++++
 4 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 regression/verilog/SVA/cycle_delay1.desc
 create mode 100644 regression/verilog/SVA/cycle_delay1.sv

diff --git a/regression/verilog/SVA/cycle_delay1.desc b/regression/verilog/SVA/cycle_delay1.desc
new file mode 100644
index 000000000..50644d6a8
--- /dev/null
+++ b/regression/verilog/SVA/cycle_delay1.desc
@@ -0,0 +1,9 @@
+CORE
+cycle_delay1.sv
+
+^file cycle_delay1\.sv line \d+: expected constant expression, but got `main.from'$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/cycle_delay1.sv b/regression/verilog/SVA/cycle_delay1.sv
new file mode 100644
index 000000000..5c14cb79b
--- /dev/null
+++ b/regression/verilog/SVA/cycle_delay1.sv
@@ -0,0 +1,11 @@
+module main(input clk, input [31:0] from);
+
+  reg [31:0] x;
+
+  always_ff @(posedge clk)
+    x++;
+
+  // The cycle delay must be elaboration-time constant
+  initial assert property (##[from:2] x!=10);
+
+endmodule
diff --git a/regression/verilog/SVA/unbounded1.desc b/regression/verilog/SVA/unbounded1.desc
index e14d56eb1..879f96491 100644
--- a/regression/verilog/SVA/unbounded1.desc
+++ b/regression/verilog/SVA/unbounded1.desc
@@ -1,7 +1,7 @@
 CORE
 unbounded1.sv
 --module main --bound 1
-^\[main\.assert\.1\] always \(main\.a ##\[0:main\.upper\] main.b\): REFUTED$
+^\[main\.assert\.1\] always \(main\.a ##\[0:\$\] main.b\): REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp
index 635c63aba..9de5a4ff5 100644
--- a/src/verilog/verilog_typecheck_sva.cpp
+++ b/src/verilog/verilog_typecheck_sva.cpp
@@ -193,11 +193,19 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
   if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something
   {
     expr.type() = bool_typet();
+
     convert_expr(expr.op0());
+    expr.op0() = elaborate_constant_expression_check(expr.op0());
+
     if(expr.op1().is_not_nil())
+    {
       convert_expr(expr.op1());
+      expr.op1() = elaborate_constant_expression_check(expr.op1());
+    }
+
     convert_sva(expr.op2());
     make_boolean(expr.op2());
+
     return std::move(expr);
   }
   else if(