From a89e5c737d4d5ae8ff999b0295a66eec72fb040e Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 14 Aug 2025 11:18:05 -0700
Subject: [PATCH] Tests for ##[*] and ##[+] with LHS

This adds a test for SVA's ##[*] and ##[+] with an LHS.
---
 regression/verilog/SVA/cycle_delay_plus4.desc | 12 ++++++++++
 regression/verilog/SVA/cycle_delay_plus4.sv   | 22 ++++++++++++++++++
 regression/verilog/SVA/cycle_delay_star4.desc | 13 +++++++++++
 regression/verilog/SVA/cycle_delay_star4.sv   | 23 +++++++++++++++++++
 4 files changed, 70 insertions(+)
 create mode 100644 regression/verilog/SVA/cycle_delay_plus4.desc
 create mode 100644 regression/verilog/SVA/cycle_delay_plus4.sv
 create mode 100644 regression/verilog/SVA/cycle_delay_star4.desc
 create mode 100644 regression/verilog/SVA/cycle_delay_star4.sv

diff --git a/regression/verilog/SVA/cycle_delay_plus4.desc b/regression/verilog/SVA/cycle_delay_plus4.desc
new file mode 100644
index 000000000..e0ecc4784
--- /dev/null
+++ b/regression/verilog/SVA/cycle_delay_plus4.desc
@@ -0,0 +1,12 @@
+CORE
+cycle_delay_plus4.sv
+--bound 10
+^\[main\.p0\] main\.x == 0 ##\[\+\] main\.x == 1: PROVED up to bound 10$
+^\[main\.p1\] main\.x == 0 ##\[\+\] main\.x == 2: PROVED up to bound 10$
+^\[main\.p2\] main\.x == 1 ##\[\+\] main\.x == 1: REFUTED$
+^\[main\.p3\] main\.x == 0 ##\[\+\] main\.x == 6: PROVED up to bound 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/cycle_delay_plus4.sv b/regression/verilog/SVA/cycle_delay_plus4.sv
new file mode 100644
index 000000000..fd96fd3be
--- /dev/null
+++ b/regression/verilog/SVA/cycle_delay_plus4.sv
@@ -0,0 +1,22 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial x=0;
+
+  always @(posedge clk)
+    if(x < 5)
+      x<=x+1;
+
+  // Should pass
+  initial p0: assert property (x==0 ##[+] x==1);
+  initial p1: assert property (x==0 ##[+] x==2);
+
+  // Should fail
+  initial p2: assert property (x==1 ##[+] x==1);
+
+  // Shoud pass, owing to weak sequence semantics
+  initial p3: assert property (x==0 ##[+] x==6);
+
+endmodule
diff --git a/regression/verilog/SVA/cycle_delay_star4.desc b/regression/verilog/SVA/cycle_delay_star4.desc
new file mode 100644
index 000000000..8a5c3ca7f
--- /dev/null
+++ b/regression/verilog/SVA/cycle_delay_star4.desc
@@ -0,0 +1,13 @@
+CORE
+cycle_delay_star4.sv
+--bound 10
+^\[main\.p0\] main\.x == 0 ##\[\*\] main\.x == 0: PROVED up to bound 10$
+^\[main\.p1\] main\.x == 0 ##\[\*\] main\.x == 1: PROVED up to bound 10$
+^\[main\.p2\] main\.x == 0 ##\[\*\] main\.x == 2: PROVED up to bound 10$
+^\[main\.p3\] main\.x == 1 ##\[\*\] main\.x == 1: REFUTED$
+^\[main\.p4\] main\.x == 0 ##\[\*\] main\.x == 6: PROVED up to bound 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/cycle_delay_star4.sv b/regression/verilog/SVA/cycle_delay_star4.sv
new file mode 100644
index 000000000..1fc451046
--- /dev/null
+++ b/regression/verilog/SVA/cycle_delay_star4.sv
@@ -0,0 +1,23 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial x=0;
+
+  always @(posedge clk)
+    if(x < 5)
+      x<=x+1;
+
+  // Should pass
+  initial p0: assert property (x==0 ##[*] x==0);
+  initial p1: assert property (x==0 ##[*] x==1);
+  initial p2: assert property (x==0 ##[*] x==2);
+
+  // Should fail
+  initial p3: assert property (x==1 ##[*] x==1);
+
+  // Shoud pass, owing to weak sequence semantics
+  initial p4: assert property (x==0 ##[*] x==6);
+
+endmodule