SVA-to-Buechi: sequence repetition operators

regression/ebmc-spot/sva-buechi/sequence_repetition4.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence_repetition4.sv
+--buechi --bound 10
+^\[main\.p0\] \(main\.x == 0 ##1 main\.x == 1\) \[\*2\]: PROVED up to bound \d+$
+^\[main\.p1\] \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 0\) \[\*2\]: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_repetition5.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence_repetition5.sv
+--buechi --bound 20
+^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:9\] ##1 main.pulse: PROVED up to bound 20$
+^\[.*\] main\.pulse ##1 \!main\.pulse \[\*1:8\] ##1 main.pulse: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/sva-buechi/sequence_repetition7.desc

@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence_repetition7.sv
+--buechi --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
+--

src/temporal-logic/ltl_sva_to_string.cpp

@@ -433,6 +433,105 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     auto a2 = and_exprt{not_exprt{if_expr.cond()}, if_expr.false_case()};
     return rec(or_exprt{a1, a2}, mode);
   }
+  else if(
+    expr.id() ==
+    ID_sva_sequence_repetition_star) // [*] or [*n] or [*x:y] or [*x:$]
+  {
+    PRECONDITION(mode == SVA_SEQUENCE);
+    auto &repetition = to_sva_sequence_repetition_star_expr(expr);
+    unary_exprt new_expr{ID_sva_sequence_repetition_star, repetition.op()};
+    if(!repetition.repetitions_given())
+    {
+      return suffix("[*]", new_expr, mode);
+    }
+    else if(repetition.is_empty_match())
+    {
+      throw ebmc_errort{} << "cannot convert [*0] to Buechi";
+    }
+    else if(repetition.is_singleton())
+    {
+      auto n = numeric_cast_v<mp_integer>(repetition.repetitions());
+      return suffix("[*" + integer2string(n) + "]", new_expr, mode);
+    }
+    else if(repetition.is_bounded_range())
+    {
+      auto from = numeric_cast_v<mp_integer>(repetition.from());
+      auto to = numeric_cast_v<mp_integer>(repetition.to());
+      return suffix(
+        "[*" + integer2string(from) + ".." + integer2string(to) + "]",
+        new_expr,
+        mode);
+    }
+    else if(repetition.is_unbounded())
+    {
+      auto from = numeric_cast_v<mp_integer>(repetition.from());
+      return suffix("[*" + integer2string(from) + "..]", new_expr, mode);
+    }
+    else
+      DATA_INVARIANT(false, "unexpected sva_sequence_repetition_star");
+  }
+  else if(expr.id() == ID_sva_sequence_repetition_plus) // something[+]
+  {
+    PRECONDITION(mode == SVA_SEQUENCE);
+    return suffix("[+]", expr, mode);
+  }
+  else if(expr.id() == ID_sva_sequence_goto_repetition) // something[->n]
+  {
+    PRECONDITION(mode == SVA_SEQUENCE);
+    auto &repetition = to_sva_sequence_goto_repetition_expr(expr);
+    unary_exprt new_expr{ID_sva_sequence_goto_repetition, repetition.op()};
+    if(repetition.is_singleton())
+    {
+      auto n = numeric_cast_v<mp_integer>(repetition.repetitions());
+      return suffix("[->" + integer2string(n) + "]", new_expr, mode);
+    }
+    else if(repetition.is_bounded_range())
+    {
+      auto from = numeric_cast_v<mp_integer>(repetition.from());
+      auto to = numeric_cast_v<mp_integer>(repetition.to());
+      return suffix(
+        "[->" + integer2string(from) + ".." + integer2string(to) + "]",
+        new_expr,
+        mode);
+    }
+    else if(repetition.is_unbounded())
+    {
+      auto from = numeric_cast_v<mp_integer>(repetition.from());
+      return suffix("[->" + integer2string(from) + "..]", new_expr, mode);
+    }
+    else
+      DATA_INVARIANT(false, "unexpected sva_sequence_goto_repetition");
+  }
+  else if(
+    expr.id() == ID_sva_sequence_non_consecutive_repetition) // something[=n]
+  {
+    PRECONDITION(mode == SVA_SEQUENCE);
+    auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr);
+    unary_exprt new_expr{
+      ID_sva_sequence_non_consecutive_repetition, repetition.op()};
+    if(repetition.is_singleton())
+    {
+      auto n = numeric_cast_v<mp_integer>(repetition.repetitions());
+      return suffix("[=" + integer2string(n) + "]", new_expr, mode);
+    }
+    else if(repetition.is_bounded_range())
+    {
+      auto from = numeric_cast_v<mp_integer>(repetition.from());
+      auto to = numeric_cast_v<mp_integer>(repetition.to());
+      return suffix(
+        "[=" + integer2string(from) + ".." + integer2string(to) + "]",
+        new_expr,
+        mode);
+    }
+    else if(repetition.is_unbounded())
+    {
+      auto from = numeric_cast_v<mp_integer>(repetition.from());
+      return suffix("[=" + integer2string(from) + "..]", new_expr, mode);
+    }
+    else
+      DATA_INVARIANT(
+        false, "unexpected sva_sequence_non_consecutive_repetition");
+  }
   else if(!is_temporal_operator(expr))
   {
     auto number = atoms.number(expr);

src/verilog/sva_expr.h

@@ -1456,19 +1456,19 @@ class sva_sequence_repetition_exprt : public ternary_exprt
   /// op[*0] is a special case, denoting the empty match
   bool is_empty_match() const
   {
-    return !is_range() && repetitions_given() && op1().is_zero();
+    return is_singleton() && op1().is_zero();
   }
 
   // The number of repetitions must be a constant after elaboration.
   const constant_exprt &repetitions() const
   {
-    PRECONDITION(repetitions_given() && !is_range());
+    PRECONDITION(is_singleton());
     return static_cast<const constant_exprt &>(op1());
   }
 
   constant_exprt &repetitions()
   {
-    PRECONDITION(repetitions_given() && !is_range());
+    PRECONDITION(is_singleton());
     return static_cast<constant_exprt &>(op1());
   }
 
@@ -1477,6 +1477,16 @@ class sva_sequence_repetition_exprt : public ternary_exprt
     return op2().is_not_nil();
   }
 
+  bool is_bounded_range() const
+  {
+    return op2().is_not_nil() && op2().id() != ID_infinity;
+  }
+
+  bool is_singleton() const
+  {
+    return op1().is_not_nil() && op2().is_nil();
+  }
+
   bool is_unbounded() const
   {
     return op2().id() == ID_infinity;
@@ -1496,13 +1506,13 @@ class sva_sequence_repetition_exprt : public ternary_exprt
 
   const constant_exprt &to() const
   {
-    PRECONDITION(is_range() && !is_unbounded());
+    PRECONDITION(is_bounded_range());
     return static_cast<const constant_exprt &>(op2());
   }
 
   constant_exprt &to()
   {
-    PRECONDITION(is_range() && !is_unbounded());
+    PRECONDITION(is_bounded_range());
     return static_cast<constant_exprt &>(op2());
   }