Merge pull request #764 from diffblue/followed-by3

SVA: add another test for `#-#` and `#=#`

Author: tautschnig

regression/verilog/SVA/followed-by3.desc

@@ -0,0 +1,14 @@
+CORE
+followed-by3.sv
+--bound 20
+^\[.*\] \(main\.x == 0 ##1 main\.x == 1\) #-# \(s_eventually main\.x == 10\): PROVED up to bound 20$
+^\[.*\] \(main\.x == 0 ##1 main\.x == 1\) #=# \(s_eventually main\.x == 10\): PROVED up to bound 20$
+^\[.*\] \(main\.x == 0 ##1 main\.x == 1\) #-# \(s_eventually main\.x == 2\): PROVED up to bound 20$
+^\[.*\] \(main\.x == 0 ##1 main\.x == 1\) #-# \(s_eventually main\.x == 11\): REFUTED$
+^\[.*\] \(main\.x == 0 ##1 main\.x == 1\) #=# \(s_eventually main\.x == 1\): REFUTED$
+^\[.*\] \(main\.x == 0 ##1 main\.x == 2\) #-# 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/followed-by3.sv

@@ -0,0 +1,26 @@
+module main(input clk);
+
+  reg [31:0] x;
+
+  initial x=0;
+
+  // 0, 1, ..., 10
+  always @(posedge clk)
+    if(x!=10)
+      x<=x+1;
+
+  // passes
+  initial p0: assert property (x==0 ##1 x==1 #-# s_eventually x==10);
+  initial p1: assert property (x==0 ##1 x==1 #=# s_eventually x==10);
+  initial p2: assert property (x==0 ##1 x==1 #-# s_eventually x==2);
+
+  // fails, we don't get to 11
+  initial p3: assert property (x==0 ##1 x==1 #-# s_eventually x==11);
+
+  // fails, we don't go back to 1
+  initial p4: assert property (x==0 ##1 x==1 #=# s_eventually x==1);
+
+  // fails owing to left hand side
+  initial p5: assert property (x==0 ##1 x==2 #-# 1);
+
+endmodule