Merge pull request #1033 from diffblue/followed-by4

SVA: add a test for followed-by

Author: tautschnig

regression/verilog/SVA/followed-by4.desc

@@ -0,0 +1,11 @@
+CORE
+followed-by4.sv
+--bound 3
+^\[main\.p1\] always \(main\.x == 0 #-# 1\): REFUTED$
+^\[main\.p2\] \(1 or \(##2 1\)\) #-# main\.x == 2: PROVED up to bound 3$
+^\[main\.p3\] \(1 or \(##2 1\)\) #-# main\.x == 0: PROVED up to bound 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/followed-by4.sv

@@ -0,0 +1,19 @@
+module main(input clk);
+
+  reg [31:0] x;
+
+  initial x=0;
+
+  // 0, 1, ...
+  always @(posedge clk)
+    x<=x+1;
+
+  // fails in the 2nd timeframe since the LHS doesn't match
+  p1: assert property (x==0 #-# 1);
+
+  // the RHS only needs to hold from _any one_ of the LHS matches,
+  // not all
+  initial p2: assert property ((1 or ##2 1) #-# x==2);
+  initial p3: assert property ((1 or ##2 1) #-# x==0);
+
+endmodule