Merge pull request #1236 from diffblue/buechi-cycle_delay_star_plus-fix

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

Author: tautschnig

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