Merge pull request #613 from diffblue/sequence_implication1

Verilog: KNOWNBUG test for sequence implication

Author: tautschnig

regression/verilog/SVA/sequence_implication1.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+sequence_implication1.sv
+--bound 20
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The sequence implication operator does not pick up the end of the chain
+sequence on the left hand side.

regression/verilog/SVA/sequence_implication1.sv

@@ -0,0 +1,15 @@
+module main(input clk);
+
+  reg [31:0] counter = 0;
+
+  // 0 1 2 0 1 2 ...
+  always_ff @(posedge clk)
+    if(counter == 2)
+      counter = 0;
+    else
+      counter++;
+
+  // checks that 1 2 is followed by 0
+  assert property (@(posedge clk) counter == 1 ##1 counter == 2 |-> ##1 counter == 0);
+
+endmodule : main