Merge pull request #1038 from diffblue/nonconsecutive_rep

SVA: `[->n]` and `[=n]`

Author: kroening

CHANGELOG

@@ -5,6 +5,7 @@
 * SystemVerilog: assignment patterns with keys for structs
 * SystemVerilog: unbased unsigned literals '0, '1, 'x, 'z
 * SystemVerilog: first_match
+* SystemVerilog: [->n] and [=n]
 * SystemVerilog: bugfix for |-> and |=>
 * SystemVerilog: bugfix for SVA sequence and
 * Verilog: 'dx, 'dz

regression/verilog/SVA/sequence_repetition1.desc

@@ -2,11 +2,11 @@ CORE
 sequence_repetition1.sv
 --bound 10
 ^\[.*\] main\.half_x == 0 \[\*2\]: PROVED up to bound 10$
-^\[.*\] main\.half_x == 0 \[->2\]: FAILURE: property not supported by BMC engine$
-^\[.*\] main\.half_x == 0 \[=2\]: FAILURE: property not supported by BMC engine$
+^\[.*\] main\.half_x == 0 \[->2\]: PROVED up to bound 10$
+^\[.*\] main\.half_x == 0 \[=2\]: PROVED up to bound 10$
 ^\[.*\] main\.x == 0 \[\*2\]: REFUTED$
-^\[.*\] main\.x == 0 \[->2\]: FAILURE: property not supported by BMC engine$
-^\[.*\] main\.x == 0 \[=2\]: FAILURE: property not supported by BMC engine$
+^\[.*\] main\.x == 0 \[->2\]: REFUTED$
+^\[.*\] main\.x == 0 \[=2\]: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --

src/trans-word-level/property.cpp

@@ -115,14 +115,6 @@ bool bmc_supports_SVA_property(const exprt &expr)
   if(has_subexpr(expr, ID_sva_sequence_within))
     return false;
 
-  // sva_sequence_non_consecutive_repetition is not supported yet
-  if(has_subexpr(expr, ID_sva_sequence_non_consecutive_repetition))
-    return false;
-
-  // sva_sequence_goto_repetition is not supported yet
-  if(has_subexpr(expr, ID_sva_sequence_goto_repetition))
-    return false;
-
   return true;
 }
 

src/trans-word-level/sequence.cpp

@@ -279,6 +279,72 @@ sequence_matchest instantiate_sequence(
 
     return result;
   }
+  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);
+
+    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());
+    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);
+
+      // 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}});
+    }
+
+    return result;
+  }
+  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);
+
+    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, zero.type());
+    const auto repetitions = from_integer(repetitions_int, zero.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);
+
+      // 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});
+    }
+
+    return result;
+  }
   else
   {
     // not a sequence, evaluate as state predicate

src/verilog/expr2verilog.cpp

@@ -1856,7 +1856,8 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
 
   else if(src.id() == ID_sva_sequence_non_consecutive_repetition)
     return precedence = verilog_precedencet::MIN,
-           convert_sva_binary_repetition("[=", to_binary_expr(src));
+           convert_sva_binary_repetition(
+             "[=", to_sva_sequence_non_consecutive_repetition_expr(src));
   // not sure about precedence
 
   else if(src.id() == ID_sva_sequence_consecutive_repetition)
@@ -1865,7 +1866,8 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
 
   else if(src.id() == ID_sva_sequence_goto_repetition)
     return precedence = verilog_precedencet::MIN,
-           convert_sva_binary_repetition("[->", to_binary_expr(src));
+           convert_sva_binary_repetition(
+             "[->", to_sva_sequence_goto_repetition_expr(src));
   // not sure about precedence
 
   else if(src.id() == ID_sva_ranged_always)

src/verilog/sva_expr.h

@@ -1318,6 +1318,117 @@ to_sva_sequence_consecutive_repetition_expr(exprt &expr)
   return static_cast<sva_sequence_consecutive_repetition_exprt &>(expr);
 }
 
+class sva_sequence_goto_repetition_exprt : public binary_exprt
+{
+public:
+  sva_sequence_goto_repetition_exprt(exprt __op, constant_exprt __repetitions)
+    : binary_exprt{
+        std::move(__op),
+        ID_sva_sequence_goto_repetition,
+        std::move(__repetitions),
+        bool_typet{}}
+  {
+  }
+
+  const exprt &op() const
+  {
+    return op0();
+  }
+
+  exprt &op()
+  {
+    return op0();
+  }
+
+  // The number of repetitions must be a constant after elaboration.
+  const constant_exprt &repetitions() const
+  {
+    return static_cast<const constant_exprt &>(op1());
+  }
+
+  constant_exprt &repetitions()
+  {
+    return static_cast<constant_exprt &>(op1());
+  }
+
+protected:
+  using binary_exprt::op0;
+  using binary_exprt::op1;
+};
+
+inline const sva_sequence_goto_repetition_exprt &
+to_sva_sequence_goto_repetition_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_goto_repetition);
+  sva_sequence_goto_repetition_exprt::check(expr);
+  return static_cast<const sva_sequence_goto_repetition_exprt &>(expr);
+}
+
+inline sva_sequence_goto_repetition_exprt &
+to_sva_sequence_goto_repetition_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_goto_repetition);
+  sva_sequence_goto_repetition_exprt::check(expr);
+  return static_cast<sva_sequence_goto_repetition_exprt &>(expr);
+}
+
+class sva_sequence_non_consecutive_repetition_exprt : public binary_exprt
+{
+public:
+  sva_sequence_non_consecutive_repetition_exprt(
+    exprt __op,
+    constant_exprt __repetitions)
+    : binary_exprt{
+        std::move(__op),
+        ID_sva_sequence_non_consecutive_repetition,
+        std::move(__repetitions),
+        bool_typet{}}
+  {
+  }
+
+  const exprt &op() const
+  {
+    return op0();
+  }
+
+  exprt &op()
+  {
+    return op0();
+  }
+
+  // The number of repetitions must be a constant after elaboration.
+  const constant_exprt &repetitions() const
+  {
+    return static_cast<const constant_exprt &>(op1());
+  }
+
+  constant_exprt &repetitions()
+  {
+    return static_cast<constant_exprt &>(op1());
+  }
+
+protected:
+  using binary_exprt::op0;
+  using binary_exprt::op1;
+};
+
+inline const sva_sequence_non_consecutive_repetition_exprt &
+to_sva_sequence_non_consecutive_repetition_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_non_consecutive_repetition);
+  sva_sequence_non_consecutive_repetition_exprt::check(expr);
+  return static_cast<const sva_sequence_non_consecutive_repetition_exprt &>(
+    expr);
+}
+
+inline sva_sequence_non_consecutive_repetition_exprt &
+to_sva_sequence_non_consecutive_repetition_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_non_consecutive_repetition);
+  sva_sequence_non_consecutive_repetition_exprt::check(expr);
+  return static_cast<sva_sequence_non_consecutive_repetition_exprt &>(expr);
+}
+
 class sva_sequence_intersect_exprt : public binary_exprt
 {
 public: