SVA's [->x:y] and [*x:y]

Both the goto repetition operator and the consecutive repetition operator
can either take a singleton number of repetition or a (possibly unbounded)
range.

This adds support for the range case.

Author: kroening

regression/verilog/SVA/cover_sequence4.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 cover_sequence4.sv
 --bound 3
 ^\[main\.p0\] cover \(1 \[=10\]\): REFUTED up to bound 3$
@@ -9,4 +9,3 @@ cover_sequence4.sv
 --
 ^warning: ignoring
 --
-Implementation of [=x:y] is missing.

src/trans-word-level/sequence.cpp

@@ -18,6 +18,63 @@ Author: Daniel Kroening, [email protected]
 #include "obligations.h"
 #include "property.h"
 
+// condition on counters for ocurrences of non-consecutive repetitions
+exprt sequence_count_condition(
+  const sva_sequence_repetition_exprt &expr,
+  const exprt &counter)
+{
+  if(expr.is_range())
+  {
+    // number of repetitions inside a range
+    auto from = numeric_cast_v<mp_integer>(expr.from());
+
+    if(expr.is_unbounded())
+    {
+      return binary_relation_exprt{
+        counter, ID_ge, from_integer(from, counter.type())};
+    }
+    else
+    {
+      auto to = numeric_cast_v<mp_integer>(expr.to());
+
+      return and_exprt{
+        binary_relation_exprt{
+          counter, ID_ge, from_integer(from, counter.type())},
+        binary_relation_exprt{
+          counter, ID_le, from_integer(to, counter.type())}};
+    }
+  }
+  else
+  {
+    // fixed number of repetitions
+    auto repetitions = numeric_cast_v<mp_integer>(expr.repetitions());
+    return equal_exprt{counter, from_integer(repetitions, counter.type())};
+  }
+}
+
+/// determine type for the repetition counter
+typet sequence_count_type(
+  const sva_sequence_repetition_exprt &expr,
+  const mp_integer &no_timeframes)
+{
+  mp_integer max;
+
+  if(expr.is_range())
+  {
+    if(expr.is_unbounded())
+      max = numeric_cast_v<mp_integer>(expr.from());
+    else
+      max = numeric_cast_v<mp_integer>(expr.to());
+  }
+  else
+    max = numeric_cast_v<mp_integer>(expr.repetitions());
+
+  max = std::max(no_timeframes, max);
+
+  auto bits = address_bits(max + 1);
+  return unsignedbv_typet{bits};
+}
+
 sequence_matchest instantiate_sequence(
   exprt expr,
   sva_sequence_semanticst semantics,
@@ -307,7 +364,7 @@ sequence_matchest instantiate_sequence(
 
     return result;
   }
-  else if(expr.id() == ID_sva_sequence_consecutive_repetition)
+  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);
@@ -344,69 +401,59 @@ sequence_matchest instantiate_sequence(
 
     return result;
   }
-  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();
-    auto repetitions_int = numeric_cast_v<mp_integer>(
-      to_sva_sequence_goto_repetition_expr(expr).repetitions());
-    PRECONDITION(repetitions_int >= 1);
+    auto &repetition = to_sva_sequence_goto_repetition_expr(expr);
+    auto &condition = repetition.op();
 
     sequence_matchest result;
 
     // We add up the number of matches of 'op' starting from
     // timeframe u, until the end of our unwinding.
-    const auto bits = address_bits(no_timeframes);
-    const auto zero = from_integer(0, unsignedbv_typet{bits});
-    const auto one = from_integer(1, unsignedbv_typet{bits});
-    const auto repetitions = from_integer(repetitions_int, zero.type());
+    const auto type = sequence_count_type(repetition, no_timeframes);
+    const auto zero = from_integer(0, type);
+    const auto one = from_integer(1, type);
     exprt matches = zero;
 
     for(mp_integer u = t; u < no_timeframes; ++u)
     {
       // match of op in timeframe u?
-      auto rec_op = instantiate(op, u, no_timeframes);
+      auto rec_op = instantiate(condition, u, no_timeframes);
 
       // add up
       matches = plus_exprt{matches, if_exprt{rec_op, one, zero}};
 
       // We have a match for op[->n] if there is a match in timeframe
       // u and matches is n.
-      result.emplace_back(
-        u, and_exprt{rec_op, equal_exprt{matches, repetitions}});
+      result.emplace_back(u, sequence_count_condition(repetition, matches));
     }
 
     return result;
   }
-  else if(expr.id() == ID_sva_sequence_non_consecutive_repetition)
+  else if(expr.id() == ID_sva_sequence_non_consecutive_repetition) // [=...]
   {
-    // The 'op' is a Boolean condition, not a sequence.
-    auto &op = to_sva_sequence_non_consecutive_repetition_expr(expr).op();
-    auto repetitions_int = numeric_cast_v<mp_integer>(
-      to_sva_sequence_non_consecutive_repetition_expr(expr).repetitions());
-    PRECONDITION(repetitions_int >= 1);
+    auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr);
+    auto &condition = repetition.op();
 
     sequence_matchest result;
 
     // We add up the number of matches of 'op' starting from
     // timeframe u, until the end of our unwinding.
-    const auto bits =
-      address_bits(std::max(no_timeframes, repetitions_int + 1));
-    const auto zero = from_integer(0, unsignedbv_typet{bits});
-    const auto one = from_integer(1, zero.type());
-    const auto repetitions = from_integer(repetitions_int, zero.type());
+    const auto type = sequence_count_type(repetition, no_timeframes);
+    const auto zero = from_integer(0, type);
+    const auto one = from_integer(1, type);
     exprt matches = zero;
 
     for(mp_integer u = t; u < no_timeframes; ++u)
     {
       // match of op in timeframe u?
-      auto rec_op = instantiate(op, u, no_timeframes);
+      auto rec_op = instantiate(condition, u, no_timeframes);
 
       // add up
       matches = plus_exprt{matches, if_exprt{rec_op, one, zero}};
 
       // We have a match for op[=n] if matches is n.
-      result.emplace_back(u, equal_exprt{matches, repetitions});
+      result.emplace_back(u, sequence_count_condition(repetition, matches));
     }
 
     return result;

src/verilog/expr2verilog.cpp

@@ -608,7 +608,7 @@ expr2verilogt::resultt expr2verilogt::convert_sva_binary(
 
 /*******************************************************************\
 
-Function: expr2verilogt::convert_sva_sequence_consecutive_repetition
+Function: expr2verilogt::convert_sva_sequence_repetition
 
   Inputs:
 
@@ -622,20 +622,22 @@ expr2verilogt::resultt expr2verilogt::convert_sva_sequence_repetition(
   const std::string &name,
   const sva_sequence_repetition_exprt &expr)
 {
-  auto op = convert_rec(expr.op());
-  if(op.p == verilog_precedencet::MIN)
-    op.s = "(" + op.s + ")";
+  auto op_rec = convert_rec(expr.op());
+
+  if(op_rec.p == verilog_precedencet::MIN)
+    op_rec.s = "(" + op_rec.s + ")";
 
-  std::string dest = op.s + " [" + name;
+  std::string dest = op_rec.s + " [" + name;
 
   if(expr.is_range())
   {
     dest += convert_rec(expr.from()).s;
+    dest += ':';
 
     if(expr.is_unbounded())
-      dest += ":$";
+      dest += '$';
     else
-      dest += ":" + convert_rec(expr.to()).s;
+      dest += convert_rec(expr.to()).s;
   }
   else
     dest += convert_rec(expr.repetitions()).s;

src/verilog/expr2verilog_class.h

@@ -16,8 +16,8 @@ class sva_abort_exprt;
 class sva_case_exprt;
 class sva_if_exprt;
 class sva_ranged_predicate_exprt;
-class sva_sequence_repetition_exprt;
 class sva_sequence_first_match_exprt;
+class sva_sequence_repetition_exprt;
 
 // Precedences (higher means binds more strongly).
 // Follows Table 11-2 in IEEE 1800-2017.

src/verilog/verilog_typecheck_sva.cpp

@@ -352,6 +352,9 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
 
     expr.op1() = from_integer(n, integer_typet{});
 
+    if(expr.op2().is_not_nil())
+      convert_expr(expr.op2());
+
     expr.type() = verilog_sva_sequence_typet{};
 
     return std::move(expr);