Fix fragment of SVA supported by word-level BMC

1) The simplifier is changed to stay within SVA when simplifying SVA.

2) The logic that recognises supported SVA is adjusted.

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,9 +86,13 @@ 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()))
-    return or_exprt{not_exprt{expr.lhs()}, X_exprt{expr.rhs()}};
+  // Same as a->always[1:1] b if lhs is not a sequence.
+  if(!is_SVA_sequence(expr.lhs()))
+  {
+    auto one = from_integer(1, natural_typet{});
+    return or_exprt{
+      not_exprt{expr.lhs()}, sva_ranged_always_exprt{one, one, expr.rhs()}};
+  }
   else
     return std::move(expr);
 }
@@ -125,13 +129,14 @@ 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(), sva_s_eventually_exprt{expr.op()}};
     }
   }
   else
@@ -171,11 +176,13 @@ exprt normalize_property(exprt expr)
     expr = normalize_pre_sva_or(to_sva_or_expr(expr));
   else if(expr.id() == ID_sva_nexttime)
   {
-    expr = X_exprt{to_sva_nexttime_expr(expr).op()};
+    auto one = from_integer(1, natural_typet{});
+    expr = sva_ranged_always_exprt{one, one, to_sva_nexttime_expr(expr).op()};
   }
   else if(expr.id() == ID_sva_s_nexttime)
   {
-    expr = X_exprt{to_sva_s_nexttime_expr(expr).op()};
+    auto one = from_integer(1, natural_typet{});
+    expr = sva_s_always_exprt{one, one, to_sva_s_nexttime_expr(expr).op()};
   }
   else if(expr.id() == ID_sva_indexed_nexttime)
   {
@@ -190,11 +197,18 @@ exprt normalize_property(exprt expr)
       nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
   }
   else if(expr.id() == ID_sva_cycle_delay)
+  {
     expr = normalize_pre_sva_cycle_delay(to_sva_cycle_delay_expr(expr));
+  }
   else if(expr.id() == ID_sva_cycle_delay_plus)
-    expr = F_exprt{X_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
+  {
+    expr = sva_s_eventually_exprt{
+      sva_s_nexttime_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
+  }
   else if(expr.id() == ID_sva_cycle_delay_star)
-    expr = F_exprt{to_sva_cycle_delay_star_expr(expr).op()};
+  {
+    expr = sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()};
+  }
   else if(expr.id() == ID_sva_if)
   {
     auto &sva_if_expr = to_sva_if_expr(expr);

src/temporal-logic/normalize_property.h

@@ -19,14 +19,16 @@ Author: Daniel Kroening, [email protected]
 /// a sva_iff b --> a <-> b
 /// a sva_implies b --> a -> b
 /// 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φ
+/// 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 is not an SVA sequence
+/// sva_non_overlapped_implication --> ¬a ∨ always[1:1] b  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] φ
+/// ##[*] φ --> F φ
+/// ##[+] φ --> X F φ
 /// sva_if --> ? :
 /// a sva_disable_iff b --> a ∨ b
 /// a sva_accept_on b --> a ∨ b
@@ -39,8 +41,6 @@ Author: Daniel Kroening, [email protected]
 /// ¬¬φ --> φ
 /// ¬Gφ --> F¬φ
 /// ¬Fφ --> G¬φ
-/// ##[*] φ --> F φ
-/// ##[+] φ --> X F φ
 /// strong(φ) --> φ
 /// weak(φ) --> φ
 /// sva_case --> ? :

src/temporal-logic/temporal_logic.h

@@ -45,7 +45,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

@@ -144,33 +144,15 @@ Function: bmc_supports_SVA_property
 
 bool bmc_supports_SVA_property(const exprt &expr)
 {
-  if(!is_temporal_operator(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;
-  }
-  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());
-  else if(expr.id() == ID_sva_always)
-    return true;
-  else if(expr.id() == ID_sva_ranged_always)
-    return true;
-  else
+  // 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;
 }
 
 /*******************************************************************\
@@ -191,8 +173,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
 }
 
 /*******************************************************************\