SVA-to-Buechi: s_always

This adds conversion for SVA s_always to the SVA-to-Buechi translation.

Author: kroening

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

@@ -0,0 +1,11 @@
+KNOWNBUG
+../../verilog/SVA/s_always1.sv
+--buechi --bound 20
+^\[main\.p0\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
+^\[main\.p1\] not \(s_always \[0:9\] main\.x < 10\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+main.p1 is not refuted.

src/temporal-logic/ltl_sva_to_string.cpp

@@ -177,7 +177,19 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   }
   else if(expr.id() == ID_sva_s_always)
   {
-    throw ebmc_errort{} << "cannot convert " << expr.id() << " to Buechi";
+    auto &always = to_sva_s_always_expr(expr);
+    auto new_expr = unary_exprt{ID_sva_s_always, always.op()};
+    auto from = numeric_cast_v<mp_integer>(always.from());
+    if(!always.is_range())
+      return prefix("G[" + integer2string(from) + "]", new_expr, mode);
+    else
+    {
+      auto to = numeric_cast_v<mp_integer>(always.to());
+      return prefix(
+        "G[" + integer2string(from) + ":" + integer2string(to) + "]",
+        new_expr,
+        mode);
+    }
   }
   else if(expr.id() == ID_sva_s_eventually)
   {