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

@@ -66,7 +66,6 @@ IREP_ID_ONE(sva_sequence_goto_repetition)
 IREP_ID_ONE(sva_sequence_intersect)
 IREP_ID_ONE(sva_sequence_non_consecutive_repetition)
 IREP_ID_ONE(sva_sequence_property)
-IREP_ID_ONE(sva_sequence_repetition_star)
 IREP_ID_ONE(sva_sequence_repetition_plus)
 IREP_ID_ONE(sva_sequence_throughout)
 IREP_ID_ONE(sva_sequence_within)

src/temporal-logic/temporal_logic.cpp

@@ -113,7 +113,6 @@ bool is_SVA_sequence_operator(const exprt &expr)
          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

@@ -309,42 +309,52 @@ sequence_matchest instantiate_sequence(
   }
   else if(expr.id() == ID_sva_sequence_consecutive_repetition)
   {
-    // 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();
+    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) // x[+]
+  {
+    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,15 +1851,9 @@ 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(

src/verilog/parser.y

@@ -2700,9 +2700,13 @@ consecutive_repetition:
 		  }
 		}
 	| "[*" ']'
-		{ init($$, ID_sva_sequence_repetition_star); }
+		{ init($$, ID_sva_sequence_consecutive_repetition);
+		  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_repetition_plus_exprt::lower() const
+{
+  // [+] is the same as [*1:$]
+  return sva_sequence_consecutive_repetition_exprt{
+    op(), from_integer(1, integer_typet{}), infinity_exprt{integer_typet{}}};
+}
+
 exprt sva_sequence_consecutive_repetition_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_consecutive_repetition_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());

src/verilog/sva_expr.h

@@ -1325,10 +1325,22 @@ inline sva_case_exprt &to_sva_case_expr(exprt &expr)
 }
 
 /// Base class for [->...], [*...], [=...]
-/// The ... constraint may be x, x:y, x:$
+/// The ... constraint may be blank, x, x:y, x:$
 class sva_sequence_repetition_exprt : public ternary_exprt
 {
 public:
+  /// number of repetitions not given, e.g., [*] or [+]
+  sva_sequence_repetition_exprt(exprt __op, irep_idt __id)
+    : ternary_exprt{
+        __id,
+        std::move(__op),
+        nil_exprt{},
+        nil_exprt{},
+        verilog_sva_sequence_typet{}}
+  {
+  }
+
+  /// fixed number of repetitions
   sva_sequence_repetition_exprt(
     exprt __op,
     irep_idt __id,
@@ -1342,6 +1354,7 @@ class sva_sequence_repetition_exprt : public ternary_exprt
   {
   }
 
+  /// bounded range for the number of repetitions
   sva_sequence_repetition_exprt(
     exprt __op,
     irep_idt __id,
@@ -1356,6 +1369,21 @@ class sva_sequence_repetition_exprt : public ternary_exprt
   {
   }
 
+  /// unbounded range for the number of repetitions
+  sva_sequence_repetition_exprt(
+    exprt __op,
+    irep_idt __id,
+    constant_exprt __from,
+    infinity_exprt __to)
+    : ternary_exprt{
+        __id,
+        std::move(__op),
+        std::move(__from),
+        std::move(__to),
+        verilog_sva_sequence_typet{}}
+  {
+  }
+
   // May be a sequence for [*...], Boolean otherwise
   const exprt &op() const
   {
@@ -1367,16 +1395,22 @@ class sva_sequence_repetition_exprt : public ternary_exprt
     return op0();
   }
 
+  /// true if number of repetitions is given
+  bool repetitions_given() const
+  {
+    return op1().is_not_nil();
+  }
+
   // The number of repetitions must be a constant after elaboration.
   const constant_exprt &repetitions() const
   {
-    PRECONDITION(!is_range());
+    PRECONDITION(repetitions_given() && !is_range());
     return static_cast<const constant_exprt &>(op1());
   }
 
   constant_exprt &repetitions()
   {
-    PRECONDITION(!is_range());
+    PRECONDITION(repetitions_given() && !is_range());
     return static_cast<constant_exprt &>(op1());
   }
 
@@ -1434,10 +1468,52 @@ to_sva_sequence_repetition_expr(exprt &expr)
   return static_cast<sva_sequence_repetition_exprt &>(expr);
 }
 
+/// op[+]
+class sva_sequence_repetition_plus_exprt : public sva_sequence_repetition_exprt
+{
+public:
+  /// The operand is a sequence
+  explicit sva_sequence_repetition_plus_exprt(exprt op)
+    : sva_sequence_repetition_exprt{
+        std::move(op),
+        ID_sva_sequence_repetition_plus}
+  {
+  }
+
+  // op[*1:$]
+  exprt lower() const;
+};
+
+static inline const sva_sequence_repetition_plus_exprt &
+to_sva_sequence_repetition_plus_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_repetition_plus);
+  sva_sequence_repetition_plus_exprt::check(expr);
+  return static_cast<const sva_sequence_repetition_plus_exprt &>(expr);
+}
+
+static inline sva_sequence_repetition_plus_exprt &
+to_sva_sequence_repetition_plus_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_repetition_plus);
+  sva_sequence_repetition_plus_exprt::check(expr);
+  return static_cast<sva_sequence_repetition_plus_exprt &>(expr);
+}
+
+/// [*] or [*n] or [*x:y] or [*x:$]
 class sva_sequence_consecutive_repetition_exprt
   : public sva_sequence_repetition_exprt
 {
 public:
+  /// op[*]
+  explicit sva_sequence_consecutive_repetition_exprt(exprt __op)
+    : sva_sequence_repetition_exprt{
+        std::move(__op),
+        ID_sva_sequence_consecutive_repetition}
+  {
+  }
+
+  /// op[*n]
   sva_sequence_consecutive_repetition_exprt(
     exprt __op,
     constant_exprt __repetitions)
@@ -1448,6 +1524,7 @@ class sva_sequence_consecutive_repetition_exprt
   {
   }
 
+  /// op[*x:y]
   sva_sequence_consecutive_repetition_exprt(
     exprt __op,
     constant_exprt __from,
@@ -1460,6 +1537,22 @@ class sva_sequence_consecutive_repetition_exprt
   {
   }
 
+  /// op[*x:$]
+  sva_sequence_consecutive_repetition_exprt(
+    exprt __op,
+    constant_exprt __from,
+    infinity_exprt __to)
+    : sva_sequence_repetition_exprt{
+        std::move(__op),
+        ID_sva_sequence_consecutive_repetition,
+        std::move(__from),
+        std::move(__to)}
+  {
+  }
+
+  /// [*] --> [0:$]
+  /// [*n] --> op ##1 op ##1 op ...
+  /// [*x:y] --> op[*x] or op[*x+1] or ... or op[*y]
   exprt lower() const;
 };