Fix fragment of SVA supported by word-level BMC

Author: kroening

src/temporal-logic/normalize_property.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "normalize_property.h"
 
 #include <util/arith_tools.h>
+#include <util/mathematical_types.h>
 #include <util/std_expr.h>
 
 #include <verilog/sva_expr.h>
@@ -75,9 +76,8 @@ exprt normalize_pre_implies(implies_exprt expr)
 exprt normalize_pre_sva_overlapped_implication(
   sva_overlapped_implication_exprt expr)
 {
-  // Same as regular implication if lhs and rhs are not
-  // sequences.
-  if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
+  // Same as regular implication if the lhs is not a sequence.
+  if(!is_SVA_sequence(expr.lhs()))
     return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
   else
     return std::move(expr);
@@ -86,8 +86,8 @@ exprt normalize_pre_sva_overlapped_implication(
 exprt normalize_pre_sva_non_overlapped_implication(
   sva_non_overlapped_implication_exprt expr)
 {
-  // Same as a->Xb if lhs and rhs are not sequences.
-  if(!is_SVA_sequence(expr.lhs()) && !is_SVA_sequence(expr.rhs()))
+  // Same as a->Xb if lhs is not a sequence.
+  if(!is_SVA_sequence(expr.lhs()))
     return or_exprt{not_exprt{expr.lhs()}, X_exprt{expr.rhs()}};
   else
     return std::move(expr);
@@ -125,13 +125,13 @@ exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
       expr.from().is_constant() &&
       numeric_cast_v<mp_integer>(to_constant_expr(expr.from())) == 0)
     {
-      // ##[0:$] φ --> F φ
-      return F_exprt{expr.op()};
+      // ##[0:$] φ --> s_eventually φ
+      return sva_s_eventually_exprt{expr.op()};
     }
     else
     {
-      // ##[i:$] φ --> ##i F φ
-      return sva_cycle_delay_exprt{expr.from(), F_exprt{expr.op()}};
+      // ##[i:$] φ --> always[i:i] s_eventually φ
+      return sva_ranged_always_exprt{expr.from(), expr.from(), expr.op()};
     }
   }
   else
@@ -176,7 +176,10 @@ exprt normalize_property(exprt expr)
       expr = sva_ranged_always_exprt{
         nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
     else
-      expr = X_exprt{nexttime_expr.op()};
+    {
+      auto one = from_integer(1, natural_typet{});
+      expr = sva_ranged_always_exprt{one, one, nexttime_expr.op()};
+    }
   }
   else if(expr.id() == ID_sva_s_nexttime)
   {

src/temporal-logic/normalize_property.h

@@ -21,11 +21,11 @@ Author: Daniel Kroening, [email protected]
 /// sva_not a --> ¬a
 /// a sva_and b --> a ∧ b                       if a and b are not SVA sequences
 /// a sva_or b --> a ∨ b                        if a and b are not SVA sequences
-/// sva_overlapped_implication --> ¬a ∨ b       if a and b are not SVA sequences
-/// sva_non_overlapped_implication --> ¬a ∨ Xb  if a and b are not SVA sequences
-/// sva_nexttime φ --> Xφ
+/// sva_overlapped_implication --> ¬a ∨ b       if a is not an SVA sequence
+/// sva_non_overlapped_implication --> ¬a ∨ Xb  if a is not an SVA sequence
+/// sva_nexttime φ --> sva_always[1:1] φ
 /// sva_nexttime[i] φ --> sva_always[i:i] φ
-/// sva_s_nexttime φ --> Xφ
+/// sva_s_nexttime φ --> sva_always[1:1] φ
 /// sva_s_nexttime[i] φ --> sva_s_always[i:i] φ
 /// sva_if --> ? :
 /// a sva_disable_iff b --> a ∨ b

src/temporal-logic/temporal_logic.h

@@ -42,7 +42,7 @@ bool is_SVA_sequence(const exprt &);
 /// Returns true iff the given expression is an SVA temporal operator
 bool is_SVA_operator(const exprt &);
 
-/// Returns true iff the given expression contains an SVA temporal operator
+/// Returns true iff the given expression is an SVA expression
 bool is_SVA(const exprt &);
 
 #endif

src/trans-word-level/property.cpp

@@ -146,31 +146,53 @@ Function: bmc_supports_SVA_property
 
 bool bmc_supports_SVA_property(const exprt &expr)
 {
-  if(!is_temporal_operator(expr))
+  // Define 'SVA unbounded temporal operators' as one of
+  // * always (not: ranged_always)
+  // * s_eventually without range (not: eventually, which is ranged)
+  // * until, s_until, until_with, s_until_with
+
+  // We support
+  // * formulas that contain no unbounded temporal operator
+  // * always φ, where φ is a supported property
+  // * s_eventually φ, where φ contains no unbounded temporal operator
+  // * s_nexttime/nexttime φ, where φ is a supported property
+  // * conjunctions and disjunctions of supported SVA properties
+
+  auto unbounded_operator = [](const exprt &expr)
   {
-    if(!has_temporal_operator(expr))
-      return true; // initial state only
-    else if(
-      expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
-    {
-      for(auto &op : expr.operands())
-        if(!bmc_supports_property(op))
-          return false;
-      return true;
-    }
-    else
-      return false;
+    return expr.id() == ID_sva_always || expr.id() == ID_sva_s_eventually ||
+           expr.id() == ID_sva_until || expr.id() == ID_sva_s_until ||
+           expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with;
+  };
+
+  if(!has_subexpr(expr, unbounded_operator))
+  {
+    return true;
+  }
+  else if(expr.id() == ID_sva_s_eventually)
+  {
+    return !has_subexpr(
+      to_sva_s_eventually_expr(expr).op(), unbounded_operator);
   }
-  else if(expr.id() == ID_sva_cycle_delay)
-    return !has_temporal_operator(to_sva_cycle_delay_expr(expr).op());
-  else if(expr.id() == ID_sva_nexttime)
-    return !has_temporal_operator(to_sva_nexttime_expr(expr).op());
   else if(expr.id() == ID_sva_s_nexttime)
-    return !has_temporal_operator(to_sva_s_nexttime_expr(expr).op());
+  {
+    return bmc_supports_SVA_property(to_sva_s_nexttime_expr(expr).op());
+  }
+  else if(expr.id() == ID_sva_nexttime)
+  {
+    return bmc_supports_SVA_property(to_sva_nexttime_expr(expr).op());
+  }
   else if(expr.id() == ID_sva_always)
+  {
+    return bmc_supports_SVA_property(to_sva_always_expr(expr).op());
+  }
+  else if(expr.id() == ID_and || expr.id() == ID_or)
+  {
+    for(auto &op : expr.operands())
+      if(!bmc_supports_SVA_property(op))
+        return false;
     return true;
-  else if(expr.id() == ID_sva_ranged_always)
-    return true;
+  }
   else
     return false;
 }
@@ -193,8 +215,10 @@ bool bmc_supports_property(const exprt &expr)
     return bmc_supports_LTL_property(expr);
   else if(is_CTL(expr))
     return bmc_supports_CTL_property(expr);
-  else
+  else if(is_SVA(expr))
     return bmc_supports_SVA_property(expr);
+  else
+    return false; // unknown category
 }
 
 /*******************************************************************\

src/verilog/sva_expr.h

@@ -146,6 +146,12 @@ class sva_s_nexttime_exprt : public binary_predicate_exprt
   {
   }
 
+  // indexed variant
+  explicit sva_s_nexttime_exprt(exprt index, exprt op)
+    : binary_predicate_exprt(std::move(index), ID_sva_s_nexttime, std::move(op))
+  {
+  }
+
   bool is_indexed() const
   {
     return index().is_not_nil();