word-level BMC: add missing SVA expressions

Author: kroening

src/temporal-logic/normalize_property.cpp

@@ -145,6 +145,7 @@ exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
 
 exprt normalize_property(exprt expr)
 {
+#if 0
   // pre-traversal
   if(expr.id() == ID_not)
     expr = normalize_pre_not(to_not_expr(expr));
@@ -261,6 +262,7 @@ exprt normalize_property(exprt expr)
     op = normalize_property(op);
 
   // post-traversal
+#endif
 
   return expr;
 }

src/temporal-logic/temporal_logic.cpp

@@ -72,9 +72,11 @@ 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_throughout || id == ID_sva_sequence_within ||
+         id == ID_sva_strong || id == ID_sva_weak;
 }
 
 bool is_SVA_operator(const exprt &expr)

src/trans-word-level/property.cpp

@@ -370,6 +370,13 @@ static obligationst property_obligations_rec(
       return obligationst{no_timeframes - 1, true_exprt()}; // works on NNF only
     }
   }
+  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();
@@ -552,6 +559,28 @@ 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_not)
+  {
+    auto &not_expr = to_sva_not_expr(property_expr);
+    return property_obligations_rec(not_expr.lower(), current, no_timeframes);
+  }
+  else if(property_expr.id() == ID_sva_implies)
+  {
+    auto &implies_expr = to_sva_implies_expr(property_expr);
+    return property_obligations_rec(
+      implies_expr.lower(), current, no_timeframes);
+  }
+  else if(property_expr.id() == ID_sva_iff)
+  {
+    auto &iff_expr = to_sva_iff_expr(property_expr);
+    return property_obligations_rec(iff_expr.lower(), current, no_timeframes);
+  }
+  else if(property_expr.id() == ID_sva_case)
+  {
+    auto &case_expr = to_sva_case_expr(property_expr);
+    return property_obligations_rec(
+      case_expr.lowering(), current, no_timeframes);
+  }
   else
   {
     return obligationst{

src/trans-word-level/sequence.cpp

@@ -176,6 +176,18 @@ 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 ||
+    expr.id() == ID_sva_cycle_delay_star)
+  {
+    PRECONDITION(false);
+  }
   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)