Verilog: fix semantics of cover disable iff

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
 

regression/verilog/SVA/cover_sequence5.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 cover_sequence5.sv
 --bound 10
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This gives the wrong answer.

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);
 

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);

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