From 89583c8f69357233ac5bdd29e94b742febf144df Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 3 Dec 2024 12:49:34 -0800
Subject: [PATCH] SVA: KNOWNBUG test for a recursive property

---
 regression/verilog/SVA/recursive_property1.desc |  9 +++++++++
 regression/verilog/SVA/recursive_property1.sv   | 14 ++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 regression/verilog/SVA/recursive_property1.desc
 create mode 100644 regression/verilog/SVA/recursive_property1.sv

diff --git a/regression/verilog/SVA/recursive_property1.desc b/regression/verilog/SVA/recursive_property1.desc
new file mode 100644
index 000000000..5a7c79e6c
--- /dev/null
+++ b/regression/verilog/SVA/recursive_property1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+recursive_property1.sv
+--bound 10
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The parameter list fails to parse.
diff --git a/regression/verilog/SVA/recursive_property1.sv b/regression/verilog/SVA/recursive_property1.sv
new file mode 100644
index 000000000..55b4160d6
--- /dev/null
+++ b/regression/verilog/SVA/recursive_property1.sv
@@ -0,0 +1,14 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+  always_ff @(posedge clk) x = !x;
+
+  // 1800-2017 16.12.17
+  property prop_always(p);
+    p and (1 |=> prop_always(p))
+  endproperty
+
+  // expected to pass
+  assert property (prop_always(x <= 1));
+
+endmodule