From 0cb00fc4481efddfe4ba7982dadf0ebf107bf36d Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 18 Apr 2025 09:21:36 -0700
Subject: [PATCH] KNOWNBUG test for SVA cover

SVA cover properties pass even when the bound is insufficient to prove them.
---
 regression/verilog/SVA/cover_sequence2.desc | 11 +++++++++++
 regression/verilog/SVA/cover_sequence2.sv   | 15 +++++++++++++++
 2 files changed, 26 insertions(+)
 create mode 100644 regression/verilog/SVA/cover_sequence2.desc
 create mode 100644 regression/verilog/SVA/cover_sequence2.sv

diff --git a/regression/verilog/SVA/cover_sequence2.desc b/regression/verilog/SVA/cover_sequence2.desc
new file mode 100644
index 000000000..8336bbb59
--- /dev/null
+++ b/regression/verilog/SVA/cover_sequence2.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+cover_sequence2.sv
+--bound 2
+^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): PROVED$
+^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): REFUTED up to bound 2$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Cover property p0 cannot ever hold, but is shown proven when using a small bound.
diff --git a/regression/verilog/SVA/cover_sequence2.sv b/regression/verilog/SVA/cover_sequence2.sv
new file mode 100644
index 000000000..af909572a
--- /dev/null
+++ b/regression/verilog/SVA/cover_sequence2.sv
@@ -0,0 +1,15 @@
+module main(input clk);
+
+  // count up
+  reg [7:0] x = 0;
+
+  always @(posedge clk)
+    x++;
+
+  // expected to fail
+  p0: cover property (x==2 ##1 x==3 ##1 x==100);
+
+  // expected to fail until bound reaches 100
+  p1: cover property (x==98 ##1 x==99 ##1 x==100);
+
+endmodule