From b871008d043d6dc8d17e22abc5fe776e7f3c488e Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 18 Apr 2025 06:48:51 -0700
Subject: [PATCH] bugfix for SVA cover

This changes the implicit 'always' used for SVA cover properties from LTL G
to SVA always.  This avoids a mixture of LTL and SVA, which is not supported
by the BMC backend.
---
 regression/verilog/SVA/cover_sequence1.desc | 11 +++++++++++
 regression/verilog/SVA/cover_sequence1.sv   | 15 +++++++++++++++
 src/temporal-logic/normalize_property.cpp   |  2 +-
 src/temporal-logic/normalize_property.h     |  1 +
 4 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 regression/verilog/SVA/cover_sequence1.desc
 create mode 100644 regression/verilog/SVA/cover_sequence1.sv

diff --git a/regression/verilog/SVA/cover_sequence1.desc b/regression/verilog/SVA/cover_sequence1.desc
new file mode 100644
index 000000000..c05639fc9
--- /dev/null
+++ b/regression/verilog/SVA/cover_sequence1.desc
@@ -0,0 +1,11 @@
+CORE
+cover_sequence1.sv
+--bound 10 --numbered-trace
+^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): PROVED$
+^Trace with 5 states:$
+^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): REFUTED up to bound 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/cover_sequence1.sv b/regression/verilog/SVA/cover_sequence1.sv
new file mode 100644
index 000000000..5fcbc9384
--- /dev/null
+++ b/regression/verilog/SVA/cover_sequence1.sv
@@ -0,0 +1,15 @@
+module main(input clk);
+
+  // count up
+  reg [7:0] x = 0;
+
+  always @(posedge clk)
+    x++;
+
+  // expected to pass
+  p0: cover property (x==2 ##1 x==3 ##1 x==4);
+
+  // expected to fail
+  p1: cover property (x==2 ##1 x==3 ##1 x==5);
+
+endmodule
diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp
index 3253d1a81..f259f4a52 100644
--- a/src/temporal-logic/normalize_property.cpp
+++ b/src/temporal-logic/normalize_property.cpp
@@ -119,7 +119,7 @@ exprt normalize_property(exprt expr)
 {
   // top-level only
   if(expr.id() == ID_sva_cover)
-    expr = G_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
+    expr = sva_always_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
 
   expr = trivial_sva(expr);
 
diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h
index bafd7b441..56085d767 100644
--- a/src/temporal-logic/normalize_property.h
+++ b/src/temporal-logic/normalize_property.h
@@ -34,6 +34,7 @@ Author: Daniel Kroening, dkr@amazon.com
 /// weak(φ) --> φ
 /// ¬ sva_s_eventually φ --> sva_always ¬φ
 /// ¬ sva_always φ --> sva_s_eventually ¬φ
+/// cover φ --> sva_always_exprt ¬φ
 ///
 /// ----LTL-----
 /// ¬Xφ --> X¬φ