SVA: remain within SVA when negating

This uses SVA's until_with and s_until_with when negating SVA's until and
s_until instead of LTL's strong and weak release operators.  This way, the
resulting formula remains an SVA formula, as opposed to becoming a mixture
of SVA and LTL.

Author: kroening

regression/verilog/SVA/sva_iff2.sv

@@ -4,8 +4,10 @@ module main(input a, b);
   p1: assert property ((eventually[0:1] a) iff (eventually[0:1] a));
   p2: assert property ((s_eventually a) iff (s_eventually a));
   p3: assert property ((a until b) iff (a until b));
-  // p4: assert property ((a s_until b) iff (a s_until a));
+  p4: assert property ((a s_until b) iff (a s_until b));
   p5: assert property ((a until_with b) iff (a until_with b));
-  p6: assert property ((a s_until_with b) iff (a s_until_with a));
+  p6: assert property ((a s_until_with b) iff (a s_until_with b));
+  p7: assert property ((a |-> b) iff (a |-> b));
+  p8: assert property ((a #-# b) iff (a #-# b));
 
 endmodule

regression/verilog/SVA/sva_implies2.sv

@@ -5,8 +5,10 @@ module main(input a, b);
   p2: assert property ((eventually[0:1] a) implies (eventually[0:1] a));
   p3: assert property ((s_eventually a) implies (s_eventually a));
   p4: assert property ((a until b) implies (a until b));
-  // p5: assert property ((a s_until b) implies (a s_until a));
+  p5: assert property ((a s_until b) implies (a s_until b));
   p6: assert property ((a until_with b) implies (a until_with b));
-  p7: assert property ((a s_until_with b) implies (a s_until_with a));
+  p7: assert property ((a s_until_with b) implies (a s_until_with b));
+  p8: assert property ((a |-> b) implies (a |-> b));
+  p9: assert property ((a #-# b) implies (a #-# b));
 
 endmodule

src/temporal-logic/nnf.cpp

@@ -94,31 +94,35 @@ std::optional<exprt> negate_property_node(const exprt &expr)
   }
   else if(expr.id() == ID_sva_until)
   {
-    // ¬(φ W ψ) ≡ (¬φ strongR ¬ψ)
-    auto &W = to_sva_until_expr(expr);
-    return strong_R_exprt{not_exprt{W.lhs()}, not_exprt{W.rhs()}};
+    // ¬(φ weakU ψ) ≡ (¬φ strongR ¬ψ) ≡ (¬ψ strongU (¬ψ ∧ ¬φ)) ≡ (¬ψ s_until_with ¬φ)
+    // Note that LHS and RHS are swapped.
+    auto &until = to_sva_until_expr(expr);
+    return sva_s_until_with_exprt{
+      not_exprt{until.rhs()}, not_exprt{until.lhs()}};
   }
   else if(expr.id() == ID_sva_s_until)
   {
-    // ¬(φ U ψ) ≡ (¬φ R ¬ψ)
-    auto &U = to_sva_s_until_expr(expr);
-    return R_exprt{not_exprt{U.lhs()}, not_exprt{U.rhs()}};
+    // ¬(φ strongU ψ) ≡ (¬φ weakR ¬ψ) ≡ (¬ψ weakU (¬ψ ∧ ¬φ)) ≡ (¬ψ until_with ¬φ)
+    // Note that LHS and RHS are swapped.
+    auto &s_until = to_sva_s_until_expr(expr);
+    return sva_until_with_exprt{
+      not_exprt{s_until.rhs()}, not_exprt{s_until.lhs()}};
   }
   else if(expr.id() == ID_sva_until_with)
   {
-    // ¬(φ R ψ) ≡ (¬φ U ¬ψ)
+    // ¬(φ until_with ψ) ≡ ¬(φ until (φ ∧ ψ)) ≡ ¬(ψ weakR φ) ≡ (¬ψ strongU ¬φ)
     // Note LHS and RHS are swapped.
     auto &until_with = to_sva_until_with_expr(expr);
-    auto R = R_exprt{until_with.rhs(), until_with.lhs()};
-    return sva_until_exprt{not_exprt{R.lhs()}, not_exprt{R.rhs()}};
+    return sva_s_until_exprt{
+      not_exprt{until_with.rhs()}, not_exprt{until_with.lhs()}};
   }
   else if(expr.id() == ID_sva_s_until_with)
   {
-    // ¬(φ strongR ψ) ≡ (¬φ W ¬ψ)
+    // ¬(φ s_until_with ψ) ≡ ¬(φ s_until (φ ∧ ψ)) ≡ ¬(ψ strongR φ) ≡ (¬φ weakU ¬ψ)
     // Note LHS and RHS are swapped.
     auto &s_until_with = to_sva_s_until_with_expr(expr);
-    auto strong_R = strong_R_exprt{s_until_with.rhs(), s_until_with.lhs()};
-    return weak_U_exprt{not_exprt{strong_R.lhs()}, not_exprt{strong_R.rhs()}};
+    return sva_until_exprt{
+      not_exprt{s_until_with.rhs()}, not_exprt{s_until_with.lhs()}};
   }
   else if(expr.id() == ID_sva_overlapped_followed_by)
   {

src/verilog/sva_expr.h

@@ -543,6 +543,7 @@ static inline sva_s_until_exprt &to_sva_s_until_expr(exprt &expr)
   return static_cast<sva_s_until_exprt &>(expr);
 }
 
+/// SVA until_with operator -- like LTL (weak) R, but lhs/rhs swapped
 class sva_until_with_exprt : public binary_predicate_exprt
 {
 public:
@@ -567,6 +568,7 @@ static inline sva_until_with_exprt &to_sva_until_with_expr(exprt &expr)
   return static_cast<sva_until_with_exprt &>(expr);
 }
 
+/// SVA s_until_with operator -- like LTL strong R, but lhs/rhs swapped
 class sva_s_until_with_exprt : public binary_predicate_exprt
 {
 public: