SVA->Buechi: fix translation of ##[*] and ##[+]

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

@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/cycle_delay_plus4.sv
+--buechi
+^\[main\.p0\] main\.x == 0 ##\[\+\] main\.x == 1: PROVED \(1-induction\)$
+^\[main\.p1\] main\.x == 0 ##\[\+\] main\.x == 2: PROVED \(1-induction\)$
+^\[main\.p2\] main\.x == 1 ##\[\+\] main\.x == 1: REFUTED$
+^\[main\.p3\] main\.x == 0 ##\[\+\] main\.x == 6: PROVED \(1-induction\)$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star1.sv
 --buechi --bdd
 ^\[main.p0\] ##\[\*\] main\.x == 2 ##1 main\.x == 3: PROVED$
@@ -7,4 +7,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-This gives the wrong answer.

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star1.sv
 --buechi --bound 10
 ^\[main.p0\] ##\[\*\] main\.x == 2 ##1 main\.x == 3: PROVED up to bound 10$
@@ -7,4 +7,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-This gives the wrong answer.

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

@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/cycle_delay_star2.sv
 --buechi --bdd
-^\[main.p0\] ##\[\*\] main\.x == 4: REFUTED$
-^EXIT=10$
+^\[main.p0\] ##\[\*\] main\.x == 4: PROVED$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

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

@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/cycle_delay_star2.sv
 --buechi --bound 10
-^\[main.p0\] ##\[\*\] main\.x == 4: REFUTED$
-^EXIT=10$
+^\[main.p0\] ##\[\*\] main\.x == 4: PROVED up to bound 10$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

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

@@ -1,10 +1,9 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star3.sv
 --buechi --bdd
-^\[main.p0\] ##\[\*\] main\.x == 4: PROVED up to bound 10$
+^\[main.p0\] ##\[\*\] main\.x == 4: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-We get the wrong answer.

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star3.sv
 --buechi --bound 10
 ^\[main.p0\] ##\[\*\] main\.x == 4: PROVED up to bound 10$
@@ -7,4 +7,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-We get the wrong answer.

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

@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/cycle_delay_star4.sv
+--buechi
+^\[main\.p0\] main\.x == 0 ##\[\*\] main\.x == 0: PROVED \(1-induction\)$
+^\[main\.p1\] main\.x == 0 ##\[\*\] main\.x == 1: PROVED \(1-induction\)$
+^\[main\.p2\] main\.x == 0 ##\[\*\] main\.x == 2: PROVED \(1-induction\)$
+^\[main\.p3\] main\.x == 1 ##\[\*\] main\.x == 1: REFUTED$
+^\[main\.p4\] main\.x == 0 ##\[\*\] main\.x == 6: PROVED \(1-induction\)$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/cycle_delay_star2.desc

@@ -1,10 +1,9 @@
-KNOWNBUG
+CORE
 cycle_delay_star2.sv
 --bound 10
-^\[main.p0\] ##\[\*\] main\.x == 4: REFUTED$
-^EXIT=10$
+^\[main.p0\] ##\[\*\] main\.x == 4: PROVED up to bound 10$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The BMC engine gives the wrong answer.

regression/verilog/SVA/cycle_delay_star2.sv

@@ -8,7 +8,8 @@ module main(input clk);
   always @(posedge clk)
     if(x<3) x++;
 
-  // fails -- 4 is never reached
+  // 4 is never reached, but this doesn't fail the property
+  // owing to weak sequence semantics.
   initial p0: assert property (##[*] x==4);
 
 endmodule

src/temporal-logic/ltl_sva_to_string.cpp

@@ -419,17 +419,45 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   }
   else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something
   {
+    // ##[*] x ---> 1[*] ; x
+    // w ##[*] x ---> w : 1[*] ; x
     PRECONDITION(mode == SVA_SEQUENCE);
-    auto new_expr = unary_exprt{
-      ID_sva_cycle_delay_star, to_sva_cycle_delay_star_expr(expr).rhs()};
-    return suffix("[*]", new_expr, mode);
+    auto &cycle_delay_expr = to_sva_cycle_delay_star_expr(expr);
+    if(cycle_delay_expr.has_lhs())
+    {
+      auto new_expr = binary_exprt{
+        cycle_delay_expr.lhs(),
+        ID_sva_cycle_delay_star,
+        cycle_delay_expr.rhs()};
+      return infix(" : 1[*] ; ", new_expr, mode);
+    }
+    else
+    {
+      auto new_expr =
+        unary_exprt{ID_sva_cycle_delay_star, cycle_delay_expr.rhs()};
+      return prefix("1[*] ; ", new_expr, mode);
+    }
   }
   else if(expr.id() == ID_sva_cycle_delay_plus) // ##[+] something
   {
+    // ##[+] x ---> 1[+] ; x
+    // w ##[+] x ---> w : 1[+] ; x
     PRECONDITION(mode == SVA_SEQUENCE);
-    auto new_expr = unary_exprt{
-      ID_sva_cycle_delay_star, to_sva_cycle_delay_plus_expr(expr).rhs()};
-    return suffix("[+]", new_expr, mode);
+    auto &cycle_delay_expr = to_sva_cycle_delay_plus_expr(expr);
+    if(cycle_delay_expr.has_lhs())
+    {
+      auto new_expr = binary_exprt{
+        cycle_delay_expr.lhs(),
+        ID_sva_cycle_delay_plus,
+        cycle_delay_expr.rhs()};
+      return infix(" : 1[+] ; ", new_expr, mode);
+    }
+    else
+    {
+      auto new_expr =
+        unary_exprt{ID_sva_cycle_delay_plus, cycle_delay_expr.rhs()};
+      return prefix("1[+] ; ", new_expr, mode);
+    }
   }
   else if(expr.id() == ID_if)
   {

src/verilog/sva_expr.h

@@ -1203,6 +1203,7 @@ static inline sva_cycle_delay_exprt &to_sva_cycle_delay_expr(exprt &expr)
 class sva_cycle_delay_plus_exprt : public binary_exprt
 {
 public:
+  /// The operands are sequences, the LHS is optional, indicated by nil.
   explicit sva_cycle_delay_plus_exprt(exprt __lhs, exprt __rhs)
     : binary_exprt(
         std::move(__lhs),
@@ -1212,6 +1213,11 @@ class sva_cycle_delay_plus_exprt : public binary_exprt
   {
   }
 
+  bool has_lhs() const
+  {
+    return lhs().is_not_nil();
+  }
+
   // ##[1:$] op
   exprt lower() const;
 };
@@ -1235,6 +1241,7 @@ to_sva_cycle_delay_plus_expr(exprt &expr)
 class sva_cycle_delay_star_exprt : public binary_exprt
 {
 public:
+  /// The operands are a sequences, the LHS is optional, indicated by nil.
   explicit sva_cycle_delay_star_exprt(exprt __lhs, exprt __rhs)
     : binary_exprt(
         std::move(__lhs),
@@ -1244,6 +1251,11 @@ class sva_cycle_delay_star_exprt : public binary_exprt
   {
   }
 
+  bool has_lhs() const
+  {
+    return lhs().is_not_nil();
+  }
+
   // ##[0:$] op
   exprt lower() const;
 };