Merge pull request #1131 from diffblue/buechi-sva-s_always

SVA-to-Buechi: `s_always`

Author: kroening

regression/ebmc-spot/sva-buechi/nexttime1.bdd.desc

@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/nexttime1.sv
+--buechi --bdd
+^\[main\.p1\] s_nexttime\[0\] main\.counter == 0: PROVED$
+^\[main\.p2\] s_nexttime\[1\] main\.counter == 1: PROVED$
+^\[main\.p3\] nexttime\[8\] main\.counter == 8: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/nexttime1.sv
+--buechi --module main --bound 10
+^\[main\.p1\] s_nexttime\[0\] main\.counter == 0: PROVED up to bound 10$
+^\[main\.p2\] s_nexttime\[1\] main\.counter == 1: PROVED up to bound 10$
+^\[main\.p3\] nexttime\[8\] main\.counter == 8: PROVED up to bound 10$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Backend support missing.

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.

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

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/sva_iff2.sv
+--buechi --bound 10
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/sva_implies2.sv
+--buechi --bound 2
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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)
   {