Merge pull request #757 from diffblue/followed-by1-fix

SVA: implement `#-#` and `#=#`

Author: tautschnig

regression/verilog/SVA/sequence_followed_by1.desc renamed to regression/verilog/SVA/followed-by1.desc

@@ -1,9 +1,9 @@
 CORE
-sequence_followed_by1.sv
+followed-by1.sv
 --bound 20 --numbered-trace
-^\[main\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): FAILURE: property not supported by BMC engine$
-^\[main\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): FAILURE: property not supported by BMC engine$
-^EXIT=10$
+^\[main\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): PROVED up to bound 20$
+^\[main\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): PROVED up to bound 20$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/SVA/sequence_followed_by1.sv renamed to regression/verilog/SVA/followed-by1.sv

@@ -1,9 +1,9 @@
 CORE
 followed-by2.sv
 --bound 20
-^\[main\.p0\] always \(\(main\.a #-# main\.b\) iff \(not \(main\.a |-> \(not main\.b\)\)\)\): FAILURE: property not supported by BMC engine$
-^\[main\.p1\] always \(\(main\.a #=# main\.b\) iff \(not \(main\.a |=> \(not main\.b\)\)\)\): FAILURE: property not supported by BMC engine$
-^EXIT=10$
+^\[main\.p0\] always \(\(main\.a #-# main\.b\) iff \(not \(main\.a |-> \(not main\.b\)\)\)\): PROVED up to bound 20$
+^\[main\.p1\] always \(\(main\.a #=# main\.b\) iff \(not \(main\.a |=> \(not main\.b\)\)\)\): PROVED up to bound 20$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/SVA/followed-by2.desc

@@ -73,6 +73,13 @@ std::optional<exprt> negate_property_node(const exprt &expr)
     // not always p --> s_eventually not p
     return sva_s_eventually_exprt{not_exprt{to_sva_always_expr(expr).op()}};
   }
+  else if(expr.id() == ID_sva_ranged_always)
+  {
+    // not always [x:y] p --> s_eventually [x:y] not p
+    auto &always = to_sva_ranged_always_expr(expr);
+    return sva_ranged_s_eventually_exprt{
+      always.lower(), always.upper(), not_exprt{always.op()}};
+  }
   else if(expr.id() == ID_sva_s_eventually)
   {
     // not s_eventually p --> always not p
@@ -113,6 +120,22 @@ std::optional<exprt> negate_property_node(const exprt &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()}};
   }
+  else if(expr.id() == ID_sva_overlapped_followed_by)
+  {
+    // 1800 2017 16.12.9
+    // !(a #-# b)   --->   a |-> !b
+    auto &followed_by = to_sva_followed_by_expr(expr);
+    auto not_b = not_exprt{followed_by.property()};
+    return sva_overlapped_implication_exprt{followed_by.lhs(), not_b};
+  }
+  else if(expr.id() == ID_sva_nonoverlapped_followed_by)
+  {
+    // 1800 2017 16.12.9
+    // !(a #=# b)   --->   a |=> !b
+    auto &followed_by = to_sva_followed_by_expr(expr);
+    auto not_b = not_exprt{followed_by.property()};
+    return sva_non_overlapped_implication_exprt{followed_by.lhs(), not_b};
+  }
   else
     return {};
 }

src/temporal-logic/nnf.cpp

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "instantiate_word_level.h"
 #include "obligations.h"
+#include "sequence.h"
 
 #include <cstdlib>
 
@@ -109,14 +110,6 @@ Function: bmc_supports_SVA_property
 
 bool bmc_supports_SVA_property(const exprt &expr)
 {
-  // sva_nonoverlapped_followed_by is not supported yet
-  if(has_subexpr(expr, ID_sva_nonoverlapped_followed_by))
-    return false;
-
-  // sva_overlapped_followed_by is not supported yet
-  if(has_subexpr(expr, ID_sva_overlapped_followed_by))
-    return false;
-
   return true;
 }
 
@@ -552,6 +545,50 @@ static obligationst property_obligations_rec(
     auto equal_expr = equal_exprt{sva_iff_expr.lhs(), sva_iff_expr.rhs()};
     return property_obligations_rec(equal_expr, current, no_timeframes);
   }
+  else if(
+    property_expr.id() == ID_sva_nonoverlapped_followed_by ||
+    property_expr.id() == ID_sva_overlapped_followed_by)
+  {
+    // The LHS is a sequence, the RHS is a property expression,
+    // the result is a property expression.
+    auto &followed_by = to_sva_followed_by_expr(property_expr);
+
+    // get match points for LHS sequence
+    auto match_points =
+      instantiate_sequence(followed_by.sequence(), current, no_timeframes);
+
+    exprt::operandst disjuncts;
+    mp_integer t = current;
+
+    for(auto &match_point : match_points)
+    {
+      mp_integer property_start = match_point.first;
+
+      // #=# advances the clock by one from the sequence match point
+      if(property_expr.id() == ID_sva_nonoverlapped_followed_by)
+        property_start += 1;
+
+      // at the end?
+      if(property_start >= no_timeframes)
+      {
+        // relies on NNF
+        t = std::max(t, no_timeframes - 1);
+        disjuncts.push_back(match_point.second);
+      }
+      else
+      {
+        auto obligations_rec =
+          property_obligations_rec(
+            followed_by.property(), property_start, no_timeframes)
+            .conjunction();
+
+        disjuncts.push_back(
+          and_exprt{match_point.second, obligations_rec.second});
+        t = std::max(t, obligations_rec.first);
+      }
+    }
+    return obligationst{t, disjunction(disjuncts)};
+  }
   else
   {
     return obligationst{

src/trans-word-level/property.cpp

@@ -349,7 +349,7 @@ class sva_ranged_s_eventually_exprt : public sva_ranged_predicate_exprt
 public:
   explicit sva_ranged_s_eventually_exprt(exprt lower, exprt upper, exprt op)
     : sva_ranged_predicate_exprt(
-        ID_sva_s_eventually,
+        ID_sva_ranged_s_eventually,
         std::move(lower),
         std::move(upper),
         std::move(op))
@@ -793,6 +793,49 @@ static inline sva_or_exprt &to_sva_or_expr(exprt &expr)
   return static_cast<sva_or_exprt &>(expr);
 }
 
+class sva_followed_by_exprt : public binary_predicate_exprt
+{
+public:
+  const exprt &sequence() const
+  {
+    return op0();
+  }
+
+  exprt &sequence()
+  {
+    return op0();
+  }
+
+  const exprt &property() const
+  {
+    return op1();
+  }
+
+  exprt &property()
+  {
+    return op1();
+  }
+};
+
+static inline const sva_followed_by_exprt &
+to_sva_followed_by_expr(const exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_sva_overlapped_followed_by ||
+    expr.id() == ID_sva_nonoverlapped_followed_by);
+  sva_followed_by_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_followed_by_exprt &>(expr);
+}
+
+static inline sva_followed_by_exprt &to_sva_followed_by_expr(exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_sva_overlapped_followed_by ||
+    expr.id() == ID_sva_nonoverlapped_followed_by);
+  sva_followed_by_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_followed_by_exprt &>(expr);
+}
+
 class sva_cycle_delay_exprt : public ternary_exprt
 {
 public: