SVA-to-LTL: [*n], [*n:m]

This adds a conversion for the SVA sequence operators [*n] and [*n:m] to
LTL.

Author: kroening

regression/verilog/SVA/sequence_repetition1.bdd.desc

@@ -0,0 +1,13 @@
+CORE
+sequence_repetition1.sv
+--bdd
+^\[.*\] main\.half_x == 0 \[\*2\]: PROVED$
+^\[.*\] main\.half_x == 0 \[->2\]: FAILURE: property not supported by BDD engine$
+^\[.*\] main\.half_x == 0 \[=2\]: FAILURE: property not supported by BDD engine$
+^\[.*\] main\.x == 0 \[\*2\]: REFUTED$
+^\[.*\] main\.x == 0 \[->2\]: FAILURE: property not supported by BDD engine$
+^\[.*\] main\.x == 0 \[=2\]: FAILURE: property not supported by BDD engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/verilog/SVA/sequence_repetition3.bdd.desc

@@ -0,0 +1,11 @@
+CORE
+sequence_repetition3.sv
+--bdd
+^\[main\.p0\] \(main\.x == 0 \[\*1\]\) #=# \(main\.x == 1 \[\*1\]\): PROVED$
+^\[main\.p1\] \(main\.half_x == 0 \[\*2\]\) #=# \(main\.half_x == 1 \[\*2\]\): PROVED$
+^\[main\.p2\] main\.half_x == 0 \[\*3\]: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sequence_repetition4.bdd.desc

@@ -0,0 +1,10 @@
+CORE
+sequence_repetition4.sv
+--bdd
+^\[main\.p0\] \(main\.x == 0 ##1 main\.x == 1\) \[\*2\]: PROVED$
+^\[main\.p1\] \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 0\) \[\*2\]: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sequence_repetition7.bdd.desc

@@ -0,0 +1,9 @@
+CORE
+sequence_repetition7.sv
+--bdd
+^\[.*\] \(main\.a ##1 main\.b\) \[\*5\]: PROVED$
+^\[.*\] \(\!main\.b ##1 \!main\.a\) \[\*5\]: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

src/temporal-logic/sva_sequence_match.cpp

@@ -29,6 +29,16 @@ sva_sequence_matcht concat(sva_sequence_matcht a, const sva_sequence_matcht &b)
   return a;
 }
 
+// nonoverlapping concatenation
+sva_sequence_matcht repeat(sva_sequence_matcht m, const mp_integer &n)
+{
+  sva_sequence_matcht result;
+  for(mp_integer i = 0; i < n; ++i)
+    result.cond_vector.insert(
+      result.cond_vector.end(), m.cond_vector.begin(), m.cond_vector.end());
+  return result;
+}
+
 // overlapping concatenation
 sva_sequence_matcht
 overlapping_concat(sva_sequence_matcht a, sva_sequence_matcht b)
@@ -71,6 +81,47 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
       }
     return result;
   }
+  else if(sequence.id() == ID_sva_sequence_repetition_star) // [*n], [*n:m]
+  {
+    auto &repetition = to_sva_sequence_repetition_star_expr(sequence);
+    auto matches_op = LTL_sequence_matches(repetition.op());
+
+    if(matches_op.empty())
+      return {};
+
+    std::vector<sva_sequence_matcht> result;
+
+    if(repetition.repetitions_given())
+    {
+      if(repetition.is_range())
+      {
+        if(repetition.is_unbounded()) // [*n:$]
+        {
+          return {}; // no support
+        }
+        else // [*n:m]
+        {
+          auto from = numeric_cast_v<mp_integer>(repetition.from());
+          auto to = numeric_cast_v<mp_integer>(repetition.to());
+
+          for(mp_integer n = from; n < to; ++n)
+            for(auto &match_op : matches_op)
+              result.push_back(repeat(match_op, n));
+        }
+      }
+      else // [*n]
+      {
+        auto n = numeric_cast_v<mp_integer>(repetition.repetitions());
+
+        for(auto &match_op : matches_op)
+          result.push_back(repeat(match_op, n));
+      }
+    }
+    else         // [*]
+      return {}; // no support
+
+    return result;
+  }
   else if(sequence.id() == ID_sva_cycle_delay)
   {
     auto &delay = to_sva_cycle_delay_expr(sequence);

src/temporal-logic/sva_to_ltl.cpp

@@ -34,6 +34,7 @@ static exprt ltl(const sva_sequence_matcht &match)
     if(!c.is_true())
       conjuncts.push_back(n_Xes(i, c));
   }
+
   return conjunction(conjuncts);
 }