From 3300ecd0d8b21f8633da8a9e1403a9cf954d2a19 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 19 Oct 2025 17:00:11 -0700
Subject: [PATCH] Verilog: fix semantics of cover disable iff

SVA cover items do not pass when disabled.
---
 CHANGELOG                                   |  1 +
 regression/verilog/SVA/cover_sequence5.desc |  3 +-
 src/temporal-logic/normalize_property.cpp   | 43 +++++++++++++++++++++
 src/temporal-logic/trivial_sva.cpp          | 13 -------
 src/temporal-logic/trivial_sva.h            |  1 -
 5 files changed, 45 insertions(+), 16 deletions(-)

diff --git a/CHANGELOG b/CHANGELOG
index 608287b9c..c096edb4f 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -3,6 +3,7 @@
 * Verilog: semantic fix for output register ports
 * SystemVerilog: cover sequence
 * SystemVerilog: semantics fix for explicit casts
+* SystemVerilog: semantics fix for cover disable iff
 
 # EBMC 5.7
 
diff --git a/regression/verilog/SVA/cover_sequence5.desc b/regression/verilog/SVA/cover_sequence5.desc
index 0789e72bf..e5278bfe6 100644
--- a/regression/verilog/SVA/cover_sequence5.desc
+++ b/regression/verilog/SVA/cover_sequence5.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 cover_sequence5.sv
 --bound 10
 ^EXIT=10$
@@ -6,4 +6,3 @@ cover_sequence5.sv
 --
 ^warning: ignoring
 --
-This gives the wrong answer.
diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp
index 0124b6203..27aa98d11 100644
--- a/src/temporal-logic/normalize_property.cpp
+++ b/src/temporal-logic/normalize_property.cpp
@@ -109,11 +109,54 @@ exprt normalize_property_rec(exprt expr)
   return expr;
 }
 
+// Turn "disable iff" into an OR for assertions,
+// and into an AND for cover statements.
+void rewrite_disable_iff(exprt &expr, bool cover)
+{
+  expr.visit_post(
+    [cover](exprt &node)
+    {
+      if(node.id() == ID_sva_disable_iff)
+      {
+        auto &disable_iff = to_sva_disable_iff_expr(node);
+        if(cover)
+        {
+          // a sva_disable_iff b --> ¬a ∧ b
+          node = and_exprt{not_exprt{disable_iff.lhs()}, disable_iff.rhs()};
+        }
+        else // assertion
+        {
+          // a sva_disable_iff b --> a ∨ b
+          node = or_exprt{disable_iff.lhs(), disable_iff.rhs()};
+        }
+      }
+      else if(node.id() == ID_sva_sequence_disable_iff)
+      {
+        // only used in cover sequence (disable iff ...)
+        PRECONDITION(cover);
+        auto &disable_iff = to_sva_sequence_disable_iff_expr(node);
+        // a sva_disable_iff b --> ¬a and b
+        node = sva_and_exprt{
+          sva_boolean_exprt{
+            not_exprt{disable_iff.lhs()}, verilog_sva_sequence_typet{}},
+          disable_iff.rhs(),
+          verilog_sva_sequence_typet{}};
+      }
+    });
+}
+
 exprt normalize_property(exprt expr)
 {
   // top-level only
   if(expr.id() == ID_sva_cover)
+  {
+    rewrite_disable_iff(to_sva_cover_expr(expr).op(), true);
     expr = sva_always_exprt{sva_not_exprt{to_sva_cover_expr(expr).op()}};
+  }
+  else
+  {
+    rewrite_disable_iff(expr, false);
+  }
 
   expr = trivial_sva(expr);
 
diff --git a/src/temporal-logic/trivial_sva.cpp b/src/temporal-logic/trivial_sva.cpp
index be055bc1a..7aa928cee 100644
--- a/src/temporal-logic/trivial_sva.cpp
+++ b/src/temporal-logic/trivial_sva.cpp
@@ -105,19 +105,6 @@ exprt trivial_sva(exprt expr)
                         : sva_if_expr.false_case();
     expr = if_exprt{sva_if_expr.cond(), sva_if_expr.true_case(), false_case};
   }
-  else if(expr.id() == ID_sva_disable_iff)
-  {
-    auto &disable_iff_expr = to_sva_disable_iff_expr(expr);
-    expr = or_exprt{disable_iff_expr.lhs(), disable_iff_expr.rhs()};
-  }
-  else if(expr.id() == ID_sva_sequence_disable_iff)
-  {
-    auto &disable_iff_expr = to_sva_sequence_disable_iff_expr(expr);
-    expr = sva_or_exprt{
-      sva_boolean_exprt{disable_iff_expr.lhs(), verilog_sva_sequence_typet{}},
-      disable_iff_expr.rhs(),
-      verilog_sva_sequence_typet{}};
-  }
   else if(expr.id() == ID_sva_accept_on || expr.id() == ID_sva_sync_accept_on)
   {
     auto &sva_abort_expr = to_sva_abort_expr(expr);
diff --git a/src/temporal-logic/trivial_sva.h b/src/temporal-logic/trivial_sva.h
index 33e2dd9cd..bbe93f51d 100644
--- a/src/temporal-logic/trivial_sva.h
+++ b/src/temporal-logic/trivial_sva.h
@@ -22,7 +22,6 @@ Author: Daniel Kroening, dkr@amazon.com
 /// sva_overlapped_implication --> a -> b     if a and b are not sequences
 /// sva_if --> ? :
 /// sva_case --> ? :
-/// a sva_disable_iff b --> a ∨ b
 /// a sva_accept_on b --> a ∨ b
 /// a sva_reject_on b --> ¬a ∧ b
 /// a sva_sync_accept_on b --> a ∨ b