fix SVA ##[*] and ##[+]

Rewriting SVA the sequences ##[*] and ##[+] to SVA eventually properties
does not match the weak sequence semantics.

This removes the rewrite to a property, and replaces it by a lowering of
the operators ##[*] and ##[+] to ##[:].

Author: kroening

regression/verilog/SVA/sequence2.desc

@@ -1,17 +1,11 @@
-CORE
+KNOWNBUG
 sequence2.sv
 --bound 10 --numbered-trace
-^\[main\.p0] ##\[0:\$\] main\.x == 10: REFUTED$
-^Counterexample with \d+ states:$
-^main\.x@0 = 0$
-^main\.x@1 = 1$
-^main\.x@2 = 2$
-^main\.x@3 = 3$
-^main\.x@4 = 4$
-^main\.x@5 = 5$
-^main\.x@6 = 5$
+^\[main\.p0] ##\[0:\$\] main\.x == 10: PROVED up to bound 10$
+^\[main\.p1] ##\[0:\$\] main\.x == 10: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
+strong(...) is missing.

regression/verilog/SVA/sequence2.sv

@@ -9,7 +9,10 @@ module main;
     if(x != 5)
       x<=x+1;
 
-  // fails once we see the lasso 0, 1, 2, 3, 4, 5, 5
-  initial p0: assert property (##[0:$] x==10);
+  // does not match -- passes
+  initial p0: assert property (weak(##[0:$] x==10));
+
+  // does not match -- fails
+  initial p1: assert property (strong(##[0:$] x==10));
 
 endmodule

regression/verilog/SVA/sequence3.desc

@@ -1,14 +1,13 @@
-CORE
+KNOWNBUG
 sequence3.sv
 --bound 20 --numbered-trace
 ^\[main\.p0\] ##\[\*\] main\.x == 6: REFUTED$
-^Counterexample with 7 states:$
 ^\[main\.p1\] ##\[\*\] main\.x == 5: PROVED up to bound 20$
 ^\[main\.p2\] ##\[\+\] main\.x == 0: REFUTED$
-^Counterexample with 7 states:$
 ^\[main\.p3\] ##\[\+\] main\.x == 5: PROVED up to bound 20$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
+strong(...) is missing

regression/verilog/SVA/sequence3.sv

@@ -10,11 +10,11 @@ module main;
       x<=x+1;
 
   // ##[*] is the same as [0:$]
-  initial p0: assert property (##[*] x==6); // should fail
-  initial p1: assert property (##[*] x==5); // should pass
+  initial p0: assert property (strong(##[*] x==6)); // no match
+  initial p1: assert property (strong(##[*] x==5)); // match
 
   // ##[+] is the same as [1:$]
-  initial p2: assert property (##[+] x==0); // should fail
-  initial p3: assert property (##[+] x==5); // should pass
+  initial p2: assert property (strong(##[+] x==0)); // no match
+  initial p3: assert property (strong(##[+] x==5)); // match
 
 endmodule

src/temporal-logic/normalize_property.cpp

@@ -34,26 +34,6 @@ exprt normalize_pre_sva_non_overlapped_implication(
     return std::move(expr);
 }
 
-exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
-{
-  if(expr.is_unbounded())
-  {
-    if(numeric_cast_v<mp_integer>(expr.from()) == 0)
-    {
-      // ##[0:$] φ --> s_eventually φ
-      return sva_s_eventually_exprt{expr.op()};
-    }
-    else
-    {
-      // ##[i:$] φ --> always[i:i] s_eventually φ
-      return sva_ranged_always_exprt{
-        expr.from(), expr.from(), sva_s_eventually_exprt{expr.op()}};
-    }
-  }
-  else
-    return std::move(expr);
-}
-
 exprt normalize_property_rec(exprt expr)
 {
   // pre-traversal
@@ -84,19 +64,6 @@ exprt normalize_property_rec(exprt expr)
     expr = sva_s_always_exprt{
       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 = sva_s_nexttime_exprt{
-      sva_s_eventually_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
-  }
-  else if(expr.id() == ID_sva_cycle_delay_star)
-  {
-    expr = sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()};
-  }
 
   // normalize the operands
   for(auto &op : expr.operands())

src/temporal-logic/temporal_logic.cpp

@@ -106,6 +106,7 @@ bool is_SVA_sequence_operator(const exprt &expr)
   // are property expressions, not sequence expressions.
   // Note that ID_sva_not does not yield a sequence expression.
   return id == ID_sva_and || id == ID_sva_or || 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 ||

src/trans-word-level/sequence.cpp

@@ -42,30 +42,35 @@ sequence_matchest instantiate_sequence(
         return instantiate_sequence(
           sva_cycle_delay_expr.op(), u, no_timeframes);
     }
-    else
+    else // a range
     {
-      mp_integer to;
+      auto lower = t + from;
+      mp_integer upper;
 
       if(sva_cycle_delay_expr.to().id() == ID_infinity)
       {
         DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-        to = no_timeframes - 1;
+        upper = no_timeframes;
+      }
+      else
+      {
+        mp_integer to;
+        if(to_integer_non_constant(sva_cycle_delay_expr.to(), to))
+          throw "failed to convert sva_cycle_delay offsets";
+        upper = t + to;
       }
-      else if(to_integer_non_constant(sva_cycle_delay_expr.to(), to))
-        throw "failed to convert sva_cycle_delay offsets";
 
-      auto lower = t + from;
-      auto upper = t + to;
+      sequence_matchest matches;
 
-      // Do we exceed the bound? Make it 'true'
+      // Do we exceed the bound? Add an unconditional match.
       if(upper >= no_timeframes)
       {
         DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-        return {{no_timeframes - 1, true_exprt()}};
+        matches.emplace_back(no_timeframes - 1, true_exprt());
+        upper = no_timeframes - 1;
       }
 
-      sequence_matchest matches;
-
+      // Add a potential match for each timeframe in the range
       for(mp_integer u = lower; u <= upper; ++u)
       {
         auto sub_result =
@@ -77,6 +82,16 @@ sequence_matchest instantiate_sequence(
       return matches;
     }
   }
+  else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something
+  {
+    auto &cycle_delay_star = to_sva_cycle_delay_star_expr(expr);
+    return instantiate_sequence(cycle_delay_star.lower(), t, no_timeframes);
+  }
+  else if(expr.id() == ID_sva_cycle_delay_plus) // ##[+] something
+  {
+    auto &cycle_delay_plus = to_sva_cycle_delay_plus_expr(expr);
+    return instantiate_sequence(cycle_delay_plus.lower(), t, no_timeframes);
+  }
   else if(expr.id() == ID_sva_sequence_concatenation)
   {
     auto &implication = to_binary_expr(expr);
@@ -378,8 +393,7 @@ sequence_matchest instantiate_sequence(
   else
   {
     // not a sequence, evaluate as state predicate
-    auto obligations = property_obligations(expr, t, no_timeframes);
-    auto conjunction = obligations.conjunction();
-    return {{conjunction.first, conjunction.second}};
+    auto instantiated = instantiate_property(expr, t, no_timeframes);
+    return {{instantiated.first, instantiated.second}};
   }
 }

src/verilog/sva_expr.cpp

@@ -11,6 +11,24 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/mathematical_types.h>
 
+exprt sva_cycle_delay_plus_exprt::lower() const
+{
+  // same as ##[1:$]
+  return sva_cycle_delay_exprt{
+    from_integer(1, integer_typet{}),
+    exprt{ID_infinity, integer_typet{}},
+    op()};
+}
+
+exprt sva_cycle_delay_star_exprt::lower() const
+{
+  // same as ##[0:$]
+  return sva_cycle_delay_exprt{
+    from_integer(0, integer_typet{}),
+    exprt{ID_infinity, integer_typet{}},
+    op()};
+}
+
 exprt sva_case_exprt::lowering() const
 {
   auto &case_items = this->case_items();

src/verilog/sva_expr.h

@@ -1004,6 +1004,9 @@ class sva_cycle_delay_plus_exprt : public unary_exprt
     : unary_exprt(ID_sva_cycle_delay_plus, std::move(op), bool_typet())
   {
   }
+
+  // ##[1:$] op
+  exprt lower() const;
 };
 
 static inline const sva_cycle_delay_plus_exprt &
@@ -1029,6 +1032,9 @@ class sva_cycle_delay_star_exprt : public unary_exprt
     : unary_exprt(ID_sva_cycle_delay_star, std::move(op), bool_typet())
   {
   }
+
+  // ##[0:$] op
+  exprt lower() const;
 };
 
 static inline const sva_cycle_delay_star_exprt &

src/verilog/verilog_typecheck_sva.cpp

@@ -77,8 +77,7 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr)
 {
   if(
     expr.id() == ID_sva_not || expr.id() == ID_sva_always ||
-    expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay_plus ||
-    expr.id() == ID_sva_cycle_delay_star || expr.id() == ID_sva_nexttime ||
+    expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_nexttime ||
     expr.id() == ID_sva_s_nexttime)
   {
     convert_sva(expr.op());
@@ -87,8 +86,8 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr)
     return std::move(expr);
   }
   else if(
-    expr.id() == ID_sva_cycle_delay_plus ||
-    expr.id() == ID_sva_cycle_delay_star ||
+    expr.id() == ID_sva_cycle_delay_plus ||         // ##[+]
+    expr.id() == ID_sva_cycle_delay_star ||         // ##[*]
     expr.id() == ID_sva_sequence_repetition_plus || // x[+]
     expr.id() == ID_sva_sequence_repetition_star)   // x[*}
   {