SVA->Buechi: enable fragment of strong sequences

regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc

@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/cover_sequence1.sv
 --buechi --bound 10 --numbered-trace
-^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
-^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
+^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): PROVED$
+^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): REFUTED up to bound 10$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc

@@ -1,10 +1,10 @@
 CORE
 ../../verilog/SVA/cover_sequence2.sv
 --buechi --bound 5
-^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
-^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
-^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
-^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
+^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): REFUTED up to bound 5$
+^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): REFUTED up to bound 5$
+^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): PROVED$
+^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): REFUTED up to bound 5$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/ebmc-spot/sva-buechi/sequence2.bmc.desc

@@ -2,7 +2,7 @@ CORE
 ../../verilog/SVA/sequence2.sv
 --buechi --bound 10
 ^\[main\.p0] weak\(##\[0:\$\] main\.x == 10\): PROVED up to bound 10$
-^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: sva_strong not convertible to Buechi$
+^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: sva_cycle_delay not convertible to Buechi$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/ebmc-spot/sva-buechi/sequence3.bmc.desc

@@ -1,10 +1,10 @@
 CORE
 ../../verilog/SVA/sequence3.sv
 --buechi --bound 20 --numbered-trace
-^\[main\.p0\] strong\(##\[\*\] main\.x == 6\): UNSUPPORTED: sva_strong not convertible to Buechi$
-^\[main\.p1\] strong\(##\[\*\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$
-^\[main\.p2\] strong\(##\[\+\] main\.x == 0\): UNSUPPORTED: sva_strong not convertible to Buechi$
-^\[main\.p3\] strong\(##\[\+\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$
+^\[main\.p0\] strong\(##\[\*\] main\.x == 6\): UNSUPPORTED: sva_cycle_delay_star not convertible to Buechi$
+^\[main\.p1\] strong\(##\[\*\] main\.x == 5\): UNSUPPORTED: sva_cycle_delay_star not convertible to Buechi$
+^\[main\.p2\] strong\(##\[\+\] main\.x == 0\): UNSUPPORTED: sva_cycle_delay_plus not convertible to Buechi$
+^\[main\.p3\] strong\(##\[\+\] main\.x == 5\): UNSUPPORTED: sva_cycle_delay_plus not convertible to Buechi$
 ^EXIT=10$
 ^SIGNAL=0$
 --

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

@@ -1,7 +1,7 @@
 CORE
 ../../verilog/SVA/strong1.sv
 --buechi --bound 4
-^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$
+^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): UNSUPPORTED: sva_cycle_delay not convertible to Buechi$
 ^EXIT=10$
 ^SIGNAL=0$
 --

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

@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/system_verilog_assertion4.sv
 --buechi --module main --bound 10
-^\[main\.p11\] always \(main\.x == 0 \|-> \(\(##1 main\.x == 1\) and \(not \(##2 main\.x == 3\)\)\)\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
-^EXIT=10$
+^\[main\.p11\] always \(main\.x == 0 \|-> \(\(##1 main\.x == 1\) and \(not \(##2 main\.x == 3\)\)\)\): PROVED up to bound 10$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/temporal-logic/ltl_sva_to_string.cpp

@@ -305,42 +305,54 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   {
     PRECONDITION(mode == PROPERTY);
     auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
-    auto op_rec = rec(sequence, SVA_SEQUENCE);
+    auto op_rec = rec(sequence, SVA_SEQUENCE_WEAK);
 
     // weak closure
     return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};
   }
   else if(expr.id() == ID_sva_strong || expr.id() == ID_sva_implicit_strong)
   {
-    throw ltl_sva_to_string_unsupportedt{expr};
+    PRECONDITION(mode == PROPERTY);
+    auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
+    auto op_rec = rec(sequence, SVA_SEQUENCE_STRONG);
+
+    // we use the weak closure, and reject cases where this does not work
+    return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};
   }
   else if(expr.id() == ID_sva_or)
   {
     // can be sequence or property
-    PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE);
+    PRECONDITION(
+      mode == PROPERTY || mode == SVA_SEQUENCE_STRONG ||
+      mode == SVA_SEQUENCE_WEAK);
     return infix("|", expr, mode);
   }
   else if(expr.id() == ID_sva_and)
   {
     // can be sequence or property
-    PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE);
+    PRECONDITION(
+      mode == PROPERTY || mode == SVA_SEQUENCE_STRONG ||
+      mode == SVA_SEQUENCE_WEAK);
     // NLM intersection
     return infix("&", expr, mode);
   }
   else if(expr.id() == ID_sva_sequence_intersect)
   {
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
     return infix("&&", expr, mode);
   }
   else if(expr.id() == ID_sva_boolean)
   {
     // can be sequence or property
-    PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE);
+    PRECONDITION(
+      mode == PROPERTY || mode == SVA_SEQUENCE_STRONG ||
+      mode == SVA_SEQUENCE_WEAK);
     return rec(to_sva_boolean_expr(expr).op(), BOOLEAN);
   }
   else if(expr.id() == ID_sva_cycle_delay)
   {
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
+
     auto &delay = to_sva_cycle_delay_expr(expr);
 
     if(delay.lhs().is_nil())
@@ -349,6 +361,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
 
       if(delay.is_range()) // ##[from:to] rhs
       {
+        if(mode == SVA_SEQUENCE_STRONG)
+          throw ltl_sva_to_string_unsupportedt{expr};
+
         auto from = numeric_cast_v<mp_integer>(delay.from());
 
         if(delay.is_unbounded()) // ##[n:$] rhs
@@ -384,6 +399,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
 
       if(delay.is_range())
       {
+        if(mode == SVA_SEQUENCE_STRONG)
+          throw ltl_sva_to_string_unsupportedt{expr};
+
         auto from = numeric_cast_v<mp_integer>(delay.from());
 
         if(from == 0)
@@ -393,6 +411,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
         }
         else if(delay.is_unbounded()) // f ##[n:$] g
         {
+          if(mode == SVA_SEQUENCE_STRONG)
+            throw ltl_sva_to_string_unsupportedt{expr};
+
           return infix(
             " ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode);
         }
@@ -427,7 +448,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   {
     // ##[*] x ---> 1[*] ; x
     // w ##[*] x ---> w : 1[*] ; x
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
+
+    if(mode == SVA_SEQUENCE_STRONG)
+      throw ltl_sva_to_string_unsupportedt{expr};
+
     auto &cycle_delay_expr = to_sva_cycle_delay_star_expr(expr);
     if(cycle_delay_expr.has_lhs())
     {
@@ -448,7 +473,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   {
     // ##[+] x ---> 1[+] ; x
     // w ##[+] x ---> w : 1[+] ; x
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
+
+    if(mode == SVA_SEQUENCE_STRONG)
+      throw ltl_sva_to_string_unsupportedt{expr};
+
     auto &cycle_delay_expr = to_sva_cycle_delay_plus_expr(expr);
     if(cycle_delay_expr.has_lhs())
     {
@@ -477,11 +506,14 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     expr.id() ==
     ID_sva_sequence_repetition_star) // [*] or [*n] or [*x:y] or [*x:$]
   {
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
     auto &repetition = to_sva_sequence_repetition_star_expr(expr);
     unary_exprt new_expr{ID_sva_sequence_repetition_star, repetition.op()};
     if(!repetition.repetitions_given())
     {
+      if(mode == SVA_SEQUENCE_STRONG)
+        throw ltl_sva_to_string_unsupportedt{expr};
+
       return suffix("[*]", new_expr, mode);
     }
     else if(repetition.is_empty_match())
@@ -504,6 +536,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     }
     else if(repetition.is_unbounded())
     {
+      if(mode == SVA_SEQUENCE_STRONG)
+        throw ltl_sva_to_string_unsupportedt{expr};
+
       auto from = numeric_cast_v<mp_integer>(repetition.from());
       return suffix("[*" + integer2string(from) + "..]", new_expr, mode);
     }
@@ -512,7 +547,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   }
   else if(expr.id() == ID_sva_sequence_repetition_plus) // something[+]
   {
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
+
+    if(mode == SVA_SEQUENCE_STRONG)
+      throw ltl_sva_to_string_unsupportedt{expr};
+
     auto new_expr = unary_exprt{
       ID_sva_sequence_repetition_plus,
       to_sva_sequence_repetition_plus_expr(expr).op()};
@@ -523,7 +562,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     // ltl2tgba produces the wrong anser for [->n] and [=n]
     throw ltl_sva_to_string_unsupportedt{expr};
 
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
     auto &repetition = to_sva_sequence_goto_repetition_expr(expr);
     unary_exprt new_expr{ID_sva_sequence_goto_repetition, repetition.op()};
     if(repetition.is_singleton())
@@ -542,6 +581,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     }
     else if(repetition.is_unbounded())
     {
+      if(mode == SVA_SEQUENCE_STRONG)
+        throw ltl_sva_to_string_unsupportedt{expr};
+
       auto from = numeric_cast_v<mp_integer>(repetition.from());
       return suffix("[->" + integer2string(from) + "..]", new_expr, mode);
     }
@@ -554,7 +596,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     // ltl2tgba produces the wrong anser for [->n] and [=n]
     throw ltl_sva_to_string_unsupportedt{expr};
 
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
     auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr);
     unary_exprt new_expr{
       ID_sva_sequence_non_consecutive_repetition, repetition.op()};
@@ -574,6 +616,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     }
     else if(repetition.is_unbounded())
     {
+      if(mode == SVA_SEQUENCE_STRONG)
+        throw ltl_sva_to_string_unsupportedt{expr};
+
       auto from = numeric_cast_v<mp_integer>(repetition.from());
       return suffix("[=" + integer2string(from) + "..]", new_expr, mode);
     }
@@ -583,9 +628,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   }
   else if(expr.id() == ID_sva_sequence_first_match) // first_match(...)
   {
-    PRECONDITION(mode == SVA_SEQUENCE);
+    PRECONDITION(mode == SVA_SEQUENCE_STRONG || mode == SVA_SEQUENCE_WEAK);
     auto &sequence = to_sva_sequence_first_match_expr(expr).sequence();
-    auto op_rec = rec(sequence, SVA_SEQUENCE);
+    auto op_rec = rec(sequence, mode);
     return resultt{precedencet::ATOM, "first_match(" + op_rec.s + ')'};
   }
   else if(!is_temporal_operator(expr))

src/temporal-logic/ltl_sva_to_string.h

@@ -57,7 +57,12 @@ class ltl_sva_to_stringt
   // Spot may or may not use the same numbering in the AP header.
   numberingt<exprt, irep_hash> atoms;
 
-  using modet = enum { PROPERTY, SVA_SEQUENCE, BOOLEAN };
+  using modet = enum {
+    PROPERTY,
+    SVA_SEQUENCE_STRONG,
+    SVA_SEQUENCE_WEAK,
+    BOOLEAN
+  };
 
   resultt prefix(std::string s, const unary_exprt &, modet);
   resultt suffix(std::string s, const unary_exprt &, modet);