Skip to content

Commit 8f62ffc

Browse files
authored
Merge pull request #1069 from diffblue/cover_sequence2
KNOWNBUG test for SVA cover
2 parents 6dde22a + 0cb00fc commit 8f62ffc

File tree

2 files changed

+26
-0
lines changed

2 files changed

+26
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
KNOWNBUG
2+
cover_sequence2.sv
3+
--bound 2
4+
^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): PROVED$
5+
^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): REFUTED up to bound 2$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--
11+
Cover property p0 cannot ever hold, but is shown proven when using a small bound.
+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
module main(input clk);
2+
3+
// count up
4+
reg [7:0] x = 0;
5+
6+
always @(posedge clk)
7+
x++;
8+
9+
// expected to fail
10+
p0: cover property (x==2 ##1 x==3 ##1 x==100);
11+
12+
// expected to fail until bound reaches 100
13+
p1: cover property (x==98 ##1 x==99 ##1 x==100);
14+
15+
endmodule

0 commit comments

Comments
 (0)