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

regression/verilog/SVA/s_eventually4.desc

@@ -0,0 +1,8 @@
+CORE
+s_eventually4.sv
+--module main --bound 11
+^\[main\.p0\] always \(\(s_eventually main\.counter == 1\) or \(s_eventually main.counter == 10\)\): PROVED up to bound 11$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/SVA/s_eventually4.sv

@@ -0,0 +1,17 @@
+module main(input clk);
+
+  reg [7:0] counter;
+
+  initial counter = 0;
+
+  // 0, 1, 2, 3, 4, 0, ...
+  always @(posedge clk)
+    if(counter < 5)
+      counter = counter + 1;
+    else
+      counter = 0;
+
+  // expected to pass, owing to the first disjunct
+  p0: assert property ((s_eventually counter==1) or (s_eventually counter==10));
+
+endmodule

src/temporal-logic/normalize_property.cpp

@@ -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->nexttime b if lhs is not a sequence.
+  // Same as a->always[1:1] b if lhs is not a sequence.
   if(!is_SVA_sequence(expr.lhs()))
-    return or_exprt{not_exprt{expr.lhs()}, sva_nexttime_exprt{expr.rhs()}};
+  {
+    auto one = natural_typet{}.one_expr();
+    return or_exprt{
+      not_exprt{expr.lhs()}, sva_ranged_always_exprt{one, one, expr.rhs()}};
+  }
   else
     return std::move(expr);
 }
@@ -178,7 +182,7 @@ exprt normalize_property(exprt expr)
   else if(expr.id() == ID_sva_s_nexttime)
   {
     auto one = natural_typet{}.one_expr();
-    expr = sva_ranged_always_exprt{one, one, to_sva_s_nexttime_expr(expr).op()};
+    expr = sva_s_always_exprt{one, one, to_sva_s_nexttime_expr(expr).op()};
   }
   else if(expr.id() == ID_sva_indexed_nexttime)
   {
@@ -193,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_sequence_concatenation)
   {
     auto &sequence_concatenation = to_sva_sequence_concatenation_expr(expr);

src/temporal-logic/normalize_property.h

@@ -27,16 +27,16 @@ Author: Daniel Kroening, dkr@amazon.com
 /// 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 ∨ sva_nexttime b  if a is not an SVA sequence
-/// sva_nexttime φ --> Xφ
+/// 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] φ
 /// sva_if --> ? :
 /// ##[0:$] φ --> s_eventually φ
 /// ##[i:$] φ --> s_nexttime[i] s_eventually φ
-/// ##[*] φ --> F φ
-/// ##[+] φ --> X F φ
+/// ##[*] φ --> s_eventually φ
+/// ##[+] φ --> always[1:1] s_eventually φ
 /// 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

@@ -145,35 +145,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 if(expr.id() == ID_sva_s_eventually)
-    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;
 }
 
 /*******************************************************************\
@@ -194,8 +174,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
 }
 
 /*******************************************************************\