Merge pull request #1237 from diffblue/cycle_delay_star4

Tests for `##[*]` and `##[+]` with LHS

Author: tautschnig

regression/verilog/SVA/cycle_delay_plus4.desc

@@ -0,0 +1,12 @@
+CORE
+cycle_delay_plus4.sv
+--bound 10
+^\[main\.p0\] main\.x == 0 ##\[\+\] main\.x == 1: PROVED up to bound 10$
+^\[main\.p1\] main\.x == 0 ##\[\+\] main\.x == 2: PROVED up to bound 10$
+^\[main\.p2\] main\.x == 1 ##\[\+\] main\.x == 1: REFUTED$
+^\[main\.p3\] main\.x == 0 ##\[\+\] main\.x == 6: PROVED up to bound 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/cycle_delay_plus4.sv

@@ -0,0 +1,22 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial x=0;
+
+  always @(posedge clk)
+    if(x < 5)
+      x<=x+1;
+
+  // Should pass
+  initial p0: assert property (x==0 ##[+] x==1);
+  initial p1: assert property (x==0 ##[+] x==2);
+
+  // Should fail
+  initial p2: assert property (x==1 ##[+] x==1);
+
+  // Shoud pass, owing to weak sequence semantics
+  initial p3: assert property (x==0 ##[+] x==6);
+
+endmodule

regression/verilog/SVA/cycle_delay_star4.desc

@@ -0,0 +1,13 @@
+CORE
+cycle_delay_star4.sv
+--bound 10
+^\[main\.p0\] main\.x == 0 ##\[\*\] main\.x == 0: PROVED up to bound 10$
+^\[main\.p1\] main\.x == 0 ##\[\*\] main\.x == 1: PROVED up to bound 10$
+^\[main\.p2\] main\.x == 0 ##\[\*\] main\.x == 2: PROVED up to bound 10$
+^\[main\.p3\] main\.x == 1 ##\[\*\] main\.x == 1: REFUTED$
+^\[main\.p4\] main\.x == 0 ##\[\*\] main\.x == 6: PROVED up to bound 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/cycle_delay_star4.sv

@@ -0,0 +1,23 @@
+module main;
+
+  reg [31:0] x;
+  wire clk;
+
+  initial x=0;
+
+  always @(posedge clk)
+    if(x < 5)
+      x<=x+1;
+
+  // Should pass
+  initial p0: assert property (x==0 ##[*] x==0);
+  initial p1: assert property (x==0 ##[*] x==1);
+  initial p2: assert property (x==0 ##[*] x==2);
+
+  // Should fail
+  initial p3: assert property (x==1 ##[*] x==1);
+
+  // Shoud pass, owing to weak sequence semantics
+  initial p4: assert property (x==0 ##[*] x==6);
+
+endmodule