word-level BMC: add missing SVA expressions

Author: kroening

src/ebmc/bmc.cpp

@@ -47,14 +47,14 @@ void bmc(
       continue;
 
     // Is it supported by the BMC engine?
-    if(!bmc_supports_property(property.normalized_expr))
+    if(!bmc_supports_property(property.original_expr))
     {
       property.failure("property not supported by BMC engine");
       continue;
     }
 
     ::property(
-      property.normalized_expr,
+      property.original_expr,
       property.timeframe_handles,
       message_handler,
       solver,

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/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,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();
@@ -625,6 +632,43 @@ static obligationst property_obligations_rec(
     }
     return obligationst{t, disjunction(disjuncts)};
   }
+  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 if(property_expr.id() == ID_sva_accept_on || property_expr.id() == ID_sva_sync_accept_on)
+  {
+    auto &sva_abort_expr = to_sva_abort_expr(property_expr);
+    auto lowering = or_exprt{sva_abort_expr.condition(), sva_abort_expr.property()};
+    return property_obligations_rec(
+      lowering, current, no_timeframes);
+  }
+  else if(property_expr.id() == ID_sva_reject_on || property_expr.id() == ID_sva_sync_reject_on)
+  {
+    auto &sva_abort_expr = to_sva_abort_expr(property_expr);
+    auto lowering = and_exprt{
+      not_exprt{sva_abort_expr.condition()}, sva_abort_expr.property()};
+    return property_obligations_rec(
+      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)