SVA [*] for sequence operands

This implements the SVA operator op[*x:y] for the case when op is a
sequence.

Author: kroening

regression/verilog/SVA/sequence_repetition7.desc

@@ -0,0 +1,10 @@
+CORE
+sequence_repetition7.sv
+--bound 20
+^\[.*\] \(main\.a ##1 main\.b\) \[\*5\]: PROVED up to bound 20$
+^\[.*\] \(\!main\.b ##1 \!main\.a\) \[\*5\]: PROVED up to bound 20$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sequence_repetition7.sv

@@ -0,0 +1,16 @@
+module main(input clk);
+
+  bit a = 1, b = 0;
+
+  always_ff @(posedge clk) begin
+    a = !a;
+    b = !b;
+  end
+
+  // a b a b ...
+  initial assert property ((a ##1 b)[*5]);
+
+  // !b !a !b !a ...
+  initial assert property ((!b ##1 !a)[*5]);
+
+endmodule

src/trans-word-level/sequence.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "sequence.h"
 
 #include <util/arith_tools.h>
+#include <util/mathematical_types.h>
 
 #include <ebmc/ebmc_error.h>
 #include <temporal-logic/temporal_logic.h>
@@ -367,36 +368,21 @@ sequence_matchest instantiate_sequence(
   else if(expr.id() == ID_sva_sequence_repetition_star) // [*...]
   {
     auto &repetition = to_sva_sequence_repetition_star_expr(expr);
-    if(repetition.is_unbounded() && repetition.repetitions_given())
+    if(repetition.is_empty_match())
     {
-      // [*x:$]
-      auto from = numeric_cast_v<mp_integer>(repetition.from());
-      auto &op = repetition.op();
-
-      // Is op a sequence or a state predicate?
-      if(is_SVA_sequence_operator(op))
-        PRECONDITION(false); // no support
-
-      sequence_matchest result;
-
-      // we incrementally add conjuncts to the condition
-      exprt::operandst conjuncts;
-
-      for(mp_integer u = t; u < no_timeframes; ++u)
-      {
-        // does op hold in timeframe u?
-        auto cond_u = instantiate(op, u, no_timeframes);
-        conjuncts.push_back(cond_u);
-
-        if(conjuncts.size() >= from)
-          result.push_back({u, conjunction(conjuncts)});
-      }
-
-      // Empty match allowed?
-      if(from == 0)
-        result.push_back({t, true_exprt{}});
+      // [*0] denotes the empty match
+      return {{t, true_exprt{}}};
+    }
+    else if(repetition.is_unbounded() && repetition.repetitions_given())
+    {
+      // [*from:$] -> op[*from:to]
+      // with to = no_timeframes - t
+      auto to = from_integer(no_timeframes - t, integer_typet{});
+      auto new_repetition = sva_sequence_repetition_star_exprt{
+        repetition.op(), repetition.from(), to};
 
-      return result;
+      return instantiate_sequence(
+        new_repetition.lower(), semantics, t, no_timeframes);
     }
     else
     {

src/verilog/sva_expr.cpp

@@ -79,7 +79,7 @@ exprt sva_sequence_repetition_star_exprt::lower() const
   {
     // expand x[*n] into x ##1 x ##1 ...
     auto n = numeric_cast_v<mp_integer>(repetitions());
-    DATA_INVARIANT(n >= 1, "number of repetitions must be at least one");
+    PRECONDITION(n >= 1); // [*0] is a special case, denoting the empty match
 
     exprt result = op();
 
@@ -103,7 +103,7 @@ exprt sva_sequence_repetition_star_exprt::lower() const
     auto from_int = numeric_cast_v<mp_integer>(from());
     auto to_int = numeric_cast_v<mp_integer>(to());
 
-    DATA_INVARIANT(from_int >= 1, "number of repetitions must be at least one");
+    DATA_INVARIANT(from_int >= 0, "number of repetitions must not be negative");
     DATA_INVARIANT(
       to_int >= from_int, "number of repetitions must be interval");
 

src/verilog/sva_expr.h

@@ -1401,6 +1401,12 @@ class sva_sequence_repetition_exprt : public ternary_exprt
     return op1().is_not_nil();
   }
 
+  /// op[*0] is a special case, denoting the empty match
+  bool is_empty_match() const
+  {
+    return !is_range() && repetitions_given() && op0().is_zero();
+  }
+
   // The number of repetitions must be a constant after elaboration.
   const constant_exprt &repetitions() const
   {