KNOWNBUG test for SVA cover

SVA cover properties pass even when the bound is insufficient to prove them.

Author: kroening

regression/verilog/SVA/cover_sequence2.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+cover_sequence2.sv
+--bound 2
+^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): PROVED$
+^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): REFUTED up to bound 2$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/cover_sequence2.sv

@@ -0,0 +1,15 @@
+module main(input clk);
+
+  // count up
+  reg [7:0] x = 0;
+
+  always @(posedge clk)
+    x++;
+
+  // expected to fail
+  p0: cover property (x==2 ##1 x==3 ##1 x==100);
+
+  // expected to fail until bound reaches 100
+  p1: cover property (x==98 ##1 x==99 ##1 x==100);
+
+endmodule