diff --git a/regression/verilog/SVA/cover_sequence2.desc b/regression/verilog/SVA/cover_sequence2.desc new file mode 100644 index 00000000..8336bbb5 --- /dev/null +++ b/regression/verilog/SVA/cover_sequence2.desc @@ -0,0 +1,11 @@ +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 +-- +Cover property p0 cannot ever hold, but is shown proven when using a small bound. diff --git a/regression/verilog/SVA/cover_sequence2.sv b/regression/verilog/SVA/cover_sequence2.sv new file mode 100644 index 00000000..af909572 --- /dev/null +++ b/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