use sva_sequence_repetition_exprt for [*] and [+]

The base class sva_sequence_repetition_exprt is now also used for the SVA
consecutive sequence repetition operators [*] and [+].

Author: kroening

regression/verilog/SVA/sequence_repetition2.desc

@@ -1,15 +1,15 @@
 CORE
 sequence_repetition2.sv
 --bound 10
-^\[main\.p0\] main\.x == 0\[\*\]: PROVED up to bound 10$
-^\[main\.p1\] main\.x == 1\[\*\]: PROVED up to bound 10$
-^\[main\.p2\] \(main\.x == 0\[\+\]\) #=# main\.x == 1: PROVED up to bound 10$
-^\[main\.p3\] main\.x == 0\[\+\]: PROVED up to bound 10$
-^\[main\.p4\] main\.half_x == 0\[\*\]: PROVED up to bound 10$
-^\[main\.p5\] 0\[\*\]: PROVED up to bound 10$
-^\[main\.p6\] main\.x == 1\[\+\]: REFUTED$
-^\[main\.p7\] \(main\.x == 0\[\+\]\) #-# main\.x == 1: REFUTED$
-^\[main\.p8\] 0\[\+\]: REFUTED$
+^\[main\.p0\] main\.x == 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p1\] main\.x == 1 \[\*\]: PROVED up to bound 10$
+^\[main\.p2\] \(main\.x == 0 \[\+\]\) #=# main\.x == 1: PROVED up to bound 10$
+^\[main\.p3\] main\.x == 0 \[\+\]: PROVED up to bound 10$
+^\[main\.p4\] main\.half_x == 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p5\] 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p6\] main\.x == 1 \[\+\]: REFUTED$
+^\[main\.p7\] \(main\.x == 0 \[\+\]\) #-# main\.x == 1: REFUTED$
+^\[main\.p8\] 0 \[\+\]: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

src/hw_cbmc_irep_ids.h

@@ -60,7 +60,6 @@ IREP_ID_ONE(sva_cycle_delay_star)
 IREP_ID_ONE(sva_cycle_delay_plus)
 IREP_ID_ONE(sva_disable_iff)
 IREP_ID_ONE(sva_sequence_concatenation)
-IREP_ID_ONE(sva_sequence_consecutive_repetition)
 IREP_ID_ONE(sva_sequence_first_match)
 IREP_ID_ONE(sva_sequence_goto_repetition)
 IREP_ID_ONE(sva_sequence_intersect)

src/temporal-logic/temporal_logic.cpp

@@ -111,7 +111,6 @@ bool is_SVA_sequence_operator(const exprt &expr)
          id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match ||
          id == ID_sva_sequence_throughout || id == ID_sva_sequence_within ||
          id == ID_sva_sequence_goto_repetition ||
-         id == ID_sva_sequence_consecutive_repetition ||
          id == ID_sva_sequence_non_consecutive_repetition ||
          id == ID_sva_sequence_repetition_star ||
          id == ID_sva_sequence_repetition_plus;

src/trans-word-level/sequence.cpp

@@ -307,44 +307,54 @@ sequence_matchest instantiate_sequence(
 
     return result;
   }
-  else if(expr.id() == ID_sva_sequence_consecutive_repetition)
+  else if(expr.id() == ID_sva_sequence_repetition_star)
   {
-    // x[*n] is syntactic sugar for x ##1 ... ##1 x, with n repetitions
-    auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr);
-    return instantiate_sequence(
-      repetition.lower(), semantics, t, no_timeframes);
-  }
-  else if(
-    expr.id() == ID_sva_sequence_repetition_plus ||
-    expr.id() == ID_sva_sequence_repetition_star)
-  {
-    // x[+] and x[*]
-    auto &op = to_unary_expr(expr).op();
+    auto &repetition = to_sva_sequence_repetition_star_expr(expr);
+    if(repetition.is_unbounded() && repetition.repetitions_given())
+    {
+      // [*x:$]
+      auto from = numeric_cast_v<mp_integer>(repetition.from());
+      auto &op = repetition.op();
 
-    // Is x a sequence or a state predicate?
-    if(is_SVA_sequence_operator(op))
-      PRECONDITION(false); // no support
+      // Is op a sequence or a state predicate?
+      if(is_SVA_sequence_operator(op))
+        PRECONDITION(false); // no support
 
-    sequence_matchest result;
+      sequence_matchest result;
 
-    // we incrementally add conjuncts to the condition
-    exprt::operandst conjuncts;
+      // we incrementally add conjuncts to the condition
+      exprt::operandst conjuncts;
 
-    for(mp_integer u = t; u < no_timeframes; ++u)
-    {
-      // does x hold in state u?
-      auto cond_u = instantiate(op, u, no_timeframes);
-      conjuncts.push_back(cond_u);
-      result.push_back({u, conjunction(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);
 
-    // In addition to the above, x[*] allows an empty match.
-    if(expr.id() == ID_sva_sequence_repetition_star)
-      result.push_back({t, true_exprt{}});
+        if(conjuncts.size() >= from)
+          result.push_back({u, conjunction(conjuncts)});
+      }
 
-    return result;
+      // Empty match allowed?
+      if(from == 0)
+        result.push_back({t, true_exprt{}});
+
+      return result;
+    }
+    else
+    {
+      // [*], [*n], [*x:y]
+      return instantiate_sequence(
+        repetition.lower(), semantics, t, no_timeframes);
+    }
+  }
+  else if(expr.id() == ID_sva_sequence_repetition_plus) // [+]
+  {
+    auto &repetition = to_sva_sequence_repetition_plus_expr(expr);
+    return instantiate_sequence(
+      repetition.lower(), semantics, t, no_timeframes);
   }
-  else if(expr.id() == ID_sva_sequence_goto_repetition)
+  else if(expr.id() == ID_sva_sequence_goto_repetition) // [->...]
   {
     // The 'op' is a Boolean condition, not a sequence.
     auto &op = to_sva_sequence_goto_repetition_expr(expr).op();

src/verilog/expr2verilog.cpp

@@ -628,17 +628,20 @@ expr2verilogt::resultt expr2verilogt::convert_sva_sequence_repetition(
 
   std::string dest = op.s + " [" + name;
 
-  if(expr.is_range())
+  if(expr.repetitions_given())
   {
-    dest += convert_rec(expr.from()).s;
+    if(expr.is_range())
+    {
+      dest += convert_rec(expr.from()).s;
 
-    if(expr.is_unbounded())
-      dest += ":$";
+      if(expr.is_unbounded())
+        dest += ":$";
+      else
+        dest += ":" + convert_rec(expr.to()).s;
+    }
     else
-      dest += ":" + convert_rec(expr.to()).s;
+      dest += convert_rec(expr.repetitions()).s;
   }
-  else
-    dest += convert_rec(expr.repetitions()).s;
 
   dest += ']';
 
@@ -1848,23 +1851,17 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return precedence = verilog_precedencet::MIN,
            convert_sva_unary("always", to_sva_always_expr(src));
 
-  else if(src.id() == ID_sva_sequence_repetition_star)
-    return precedence = verilog_precedencet::MIN,
-           convert_sva_unary(to_unary_expr(src), "[*]");
-  // not sure about precedence
-
   else if(src.id() == ID_sva_sequence_repetition_plus)
-    return precedence = verilog_precedencet::MIN,
-           convert_sva_unary(to_unary_expr(src), "[+]");
-  // not sure about precedence
+    return convert_sva_sequence_repetition(
+      "+", to_sva_sequence_repetition_plus_expr(src));
 
   else if(src.id() == ID_sva_sequence_non_consecutive_repetition)
     return convert_sva_sequence_repetition(
       "=", to_sva_sequence_non_consecutive_repetition_expr(src));
 
-  else if(src.id() == ID_sva_sequence_consecutive_repetition)
+  else if(src.id() == ID_sva_sequence_repetition_star)
     return convert_sva_sequence_repetition(
-      "*", to_sva_sequence_consecutive_repetition_expr(src));
+      "*", to_sva_sequence_repetition_star_expr(src));
 
   else if(src.id() == ID_sva_sequence_goto_repetition)
     return convert_sva_sequence_repetition(

src/verilog/parser.y

@@ -2690,7 +2690,7 @@ sequence_abbrev:
 
 consecutive_repetition:
 	  "[*" const_or_range_expression ']'
-		{ init($$, ID_sva_sequence_consecutive_repetition);
+		{ init($$, ID_sva_sequence_repetition_star);
 		  if(stack_expr($2).id() == ID_sva_cycle_delay)
 		    swapop($$, $2);
 		  else
@@ -2700,9 +2700,13 @@ consecutive_repetition:
 		  }
 		}
 	| "[*" ']'
-		{ init($$, ID_sva_sequence_repetition_star); }
+		{ init($$, ID_sva_sequence_repetition_star);
+		  stack_expr($$).add_to_operands(nil_exprt{}, nil_exprt{});
+		}
 	| "[+" ']'
-		{ init($$, ID_sva_sequence_repetition_plus); }
+		{ init($$, ID_sva_sequence_repetition_plus);
+		  stack_expr($$).add_to_operands(nil_exprt{}, nil_exprt{});
+		}
 	;
 
 non_consecutive_repetition:

src/verilog/sva_expr.cpp

@@ -57,12 +57,25 @@ exprt sva_case_exprt::lowering() const
     disjunction(disjuncts), case_items.front().result(), reduced_rec};
 }
 
-exprt sva_sequence_consecutive_repetition_exprt::lower() const
+exprt sva_sequence_repetition_plus_exprt::lower() const
+{
+  // [+] is the same as [*1:$]
+  return sva_sequence_repetition_star_exprt{
+    op(), from_integer(1, integer_typet{}), infinity_exprt{integer_typet{}}};
+}
+
+exprt sva_sequence_repetition_star_exprt::lower() const
 {
   PRECONDITION(
     op().type().id() == ID_bool || op().type().id() == ID_verilog_sva_sequence);
 
-  if(!is_range())
+  if(!repetitions_given())
+  {
+    // op[*] is the same as op[*0:$]
+    return sva_sequence_repetition_star_exprt{
+      op(), from_integer(0, integer_typet{}), infinity_exprt{integer_typet{}}};
+  }
+  else if(!is_range())
   {
     // expand x[*n] into x ##1 x ##1 ...
     auto n = numeric_cast_v<mp_integer>(repetitions());
@@ -94,14 +107,13 @@ exprt sva_sequence_consecutive_repetition_exprt::lower() const
     DATA_INVARIANT(
       to_int >= from_int, "number of repetitions must be interval");
 
-    exprt result = sva_sequence_consecutive_repetition_exprt{op(), from()};
+    exprt result = sva_sequence_repetition_star_exprt{op(), from()};
 
     for(mp_integer n = from_int + 1; n <= to_int; ++n)
     {
       auto n_expr = from_integer(n, integer_typet{});
       result = sva_or_exprt{
-        std::move(result),
-        sva_sequence_consecutive_repetition_exprt{op(), n_expr}};
+        std::move(result), sva_sequence_repetition_star_exprt{op(), n_expr}};
     }
 
     return result;