word-level BMC: add missing SVA expressions

Author: kroening

src/ebmc/k_induction.cpp

@@ -11,7 +11,8 @@ Author: Daniel Kroening, daniel.kroening@inf.ethz.ch
 #include <util/string2int.h>
 
 #include <temporal-logic/temporal_logic.h>
-#include <trans-word-level/instantiate_word_level.h>
+#include <trans-word-level/obligations.h>
+#include <trans-word-level/property.h>
 #include <trans-word-level/trans_trace_word_level.h>
 #include <trans-word-level/unwind.h>
 
@@ -261,7 +262,8 @@ void k_inductiont::induction_step()
         const exprt &p = to_unary_expr(property.normalized_expr).op();
         for(std::size_t c = 0; c < no_timeframes; c++)
         {
-          exprt tmp = instantiate(p, c, no_timeframes);
+          exprt tmp =
+            property_obligations(p, c, no_timeframes).conjunction().second;
           solver.set_to_true(tmp);
         }
       }
@@ -272,13 +274,16 @@ void k_inductiont::induction_step()
     // assumption: time frames 0,...,k-1
     for(std::size_t c = 0; c < no_timeframes - 1; c++)
     {
-      exprt tmp = instantiate(p, c, no_timeframes - 1);
+      exprt tmp =
+        property_obligations(p, c, no_timeframes - 1).conjunction().second;
       solver.set_to_true(tmp);
     }
 
     // property: time frame k
     {
-      exprt tmp = instantiate(p, no_timeframes - 1, no_timeframes);
+      exprt tmp = property_obligations(p, no_timeframes - 1, no_timeframes)
+                    .conjunction()
+                    .second;
       solver.set_to_false(tmp);
     }
 

src/temporal-logic/nnf.cpp

@@ -136,6 +136,10 @@ std::optional<exprt> negate_property_node(const exprt &expr)
     auto not_b = not_exprt{followed_by.property()};
     return sva_non_overlapped_implication_exprt{followed_by.lhs(), not_b};
   }
+  else if(expr.id() == ID_sva_not)
+  {
+    return to_sva_not_expr(expr).op();
+  }
   else
     return {};
 }

src/temporal-logic/normalize_property.cpp

@@ -182,7 +182,7 @@ exprt normalize_property(exprt expr)
   expr = trivial_sva(expr);
 
   // now do recursion
-  expr = normalize_property_rec(expr);
+  //  expr = normalize_property_rec(expr);
 
   return expr;
 }

src/temporal-logic/temporal_logic.cpp

@@ -72,14 +72,16 @@ bool is_SVA_sequence(const exprt &expr)
   return id == ID_sva_and || id == ID_sva_or ||
          id == ID_sva_overlapped_implication ||
          id == ID_sva_non_overlapped_implication || id == ID_sva_cycle_delay ||
+         id == ID_sva_cycle_delay_plus || id == ID_sva_cycle_delay_star ||
          id == ID_sva_sequence_concatenation ||
          id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match ||
          id == ID_sva_sequence_throughout || id == ID_sva_sequence_within ||
          id == ID_sva_sequence_goto_repetition ||
          id == ID_sva_sequence_consecutive_repetition ||
          id == ID_sva_sequence_non_consecutive_repetition ||
          id == ID_sva_sequence_repetition_star ||
-         id == ID_sva_sequence_repetition_plus;
+         id == ID_sva_sequence_repetition_plus || id == ID_sva_strong ||
+         id == ID_sva_weak;
 }
 
 bool is_SVA_operator(const exprt &expr)

src/trans-word-level/property.cpp

@@ -399,6 +399,20 @@ static obligationst property_obligations_rec(
       return obligationst{no_timeframes - 1, true_exprt()}; // works on NNF only
     }
   }
+  else if(property_expr.id() == ID_sva_indexed_nexttime)
+  {
+    auto &nexttime = to_sva_indexed_nexttime_expr(property_expr);
+    auto always = sva_ranged_always_exprt{
+      nexttime.index(), nexttime.index(), nexttime.op()};
+    return property_obligations_rec(always, current, no_timeframes);
+  }
+  else if(property_expr.id() == ID_sva_indexed_s_nexttime)
+  {
+    auto &nexttime = to_sva_indexed_s_nexttime_expr(property_expr);
+    auto s_always = sva_ranged_always_exprt{
+      nexttime.index(), nexttime.index(), nexttime.op()};
+    return property_obligations_rec(s_always, current, no_timeframes);
+  }
   else if(property_expr.id() == ID_sva_s_until || property_expr.id() == ID_U)
   {
     auto &p = to_binary_expr(property_expr).lhs();

src/trans-word-level/sequence.cpp

@@ -176,6 +176,26 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
 
     return result;
   }
+  else if(expr.id() == ID_sva_strong || expr.id() == ID_sva_weak)
+  {
+    // not distinguished
+    auto &op = to_unary_expr(expr).op();
+    return instantiate_sequence(op, t, no_timeframes);
+  }
+  else if(expr.id() == ID_sva_cycle_delay_plus)
+  {
+    auto new_expr = sva_s_eventually_exprt{
+      sva_s_nexttime_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
+    auto obligations = property_obligations(new_expr, t, no_timeframes);
+    return {obligations.conjunction()};
+  }
+  else if(expr.id() == ID_sva_cycle_delay_star)
+  {
+    auto new_expr =
+      sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()};
+    auto obligations = property_obligations(new_expr, t, no_timeframes);
+    return {obligations.conjunction()};
+  }
   else
   {
     // not a sequence, evaluate as state predicate

src/verilog/sva_expr.h

@@ -657,6 +657,11 @@ class sva_not_exprt : public unary_predicate_exprt
     : unary_predicate_exprt(ID_sva_not, std::move(op))
   {
   }
+
+  not_exprt lower() const
+  {
+    return not_exprt{op()};
+  }
 };
 
 static inline const sva_not_exprt &to_sva_not_expr(const exprt &expr)
@@ -731,6 +736,11 @@ class sva_iff_exprt : public binary_predicate_exprt
     : binary_predicate_exprt(std::move(op0), ID_sva_iff, std::move(op1))
   {
   }
+
+  equal_exprt lower() const
+  {
+    return equal_exprt{lhs(), rhs()};
+  }
 };
 
 static inline const sva_iff_exprt &to_sva_iff_expr(const exprt &expr)
@@ -754,6 +764,11 @@ class sva_implies_exprt : public binary_predicate_exprt
     : binary_predicate_exprt(std::move(op0), ID_sva_implies, std::move(op1))
   {
   }
+
+  implies_exprt lower() const
+  {
+    return implies_exprt{lhs(), rhs()};
+  }
 };
 
 static inline const sva_implies_exprt &to_sva_implies_expr(const exprt &expr)