From c69246f4c6d4c2c44cd8538b221cb9e844730fdf Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 7 Aug 2025 12:12:41 -0700
Subject: [PATCH] SVA: test for $stable

---
 regression/verilog/SVA/stable1.desc |  9 +++++++++
 regression/verilog/SVA/stable1.sv   | 17 +++++++++++++++++
 2 files changed, 26 insertions(+)
 create mode 100644 regression/verilog/SVA/stable1.desc
 create mode 100644 regression/verilog/SVA/stable1.sv

diff --git a/regression/verilog/SVA/stable1.desc b/regression/verilog/SVA/stable1.desc
new file mode 100644
index 000000000..4cbf41450
--- /dev/null
+++ b/regression/verilog/SVA/stable1.desc
@@ -0,0 +1,9 @@
+CORE
+stable1.sv
+--bound 20
+^\[main\.p0\] always \(\$stable\(main\.data\) \|=> main\.counter >= 1\): PROVED up to bound 20$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/stable1.sv b/regression/verilog/SVA/stable1.sv
new file mode 100644
index 000000000..6a0d894c8
--- /dev/null
+++ b/regression/verilog/SVA/stable1.sv
@@ -0,0 +1,17 @@
+module main(input clk, input data);
+
+  reg data_old = 0;
+  reg [2:0] counter = 0;
+
+  always_ff @(posedge clk)
+    if(data != data_old)
+      counter = 0;
+    else if(counter < 3)
+      counter++;
+
+  always_ff @(posedge clk)
+    data_old = data;
+
+  p0: assert property ($stable(data) |=> counter >= 1);
+
+endmodule