Test for SVA ##[*] ...

This adds a test for SVA's ##[*] operator, for BDDs, BMC, Buechi->BMC and
Buechi->BDD.

Author: kroening

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

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

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

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

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

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

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

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

regression/verilog/SVA/cycle_delay_star2.sv

@@ -6,7 +6,7 @@ module main(input clk);
 
   // 0, 1, 2, 3, 3, ...
   always @(posedge clk)
-    if(x<=3) x++;
+    if(x<3) x++;
 
   // fails -- 4 is never reached
   initial p0: assert property (##[*] x==4);

regression/verilog/SVA/cycle_delay_star3.bdd.desc

@@ -0,0 +1,9 @@
+CORE
+cycle_delay_star3.sv
+--bdd
+^\[main.p0\] ##\[\*\] main\.x == 4: FAILURE: property not supported by BDD engine$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/cycle_delay_star3.bmc.desc

@@ -0,0 +1,9 @@
+CORE
+cycle_delay_star3.sv
+--bound 10
+^\[main.p0\] ##\[\*\] main\.x == 4: PROVED up to bound 10$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/cycle_delay_star3.sv

@@ -0,0 +1,14 @@
+module main(input clk);
+
+  reg [2:0] x;
+
+  initial x=0;
+
+  // 0, 1, 2, 3, 4, 4, ...
+  always @(posedge clk)
+    if(x<=3) x++;
+
+  // passes -- 4 is reached
+  initial p0: assert property (##[*] x==4);
+
+endmodule