Skip to content

Commit 9732d42

Browse files
authored
Merge pull request #1211 from diffblue/cycle_delay_star2
KNOWNBUG test for `##[*]`
2 parents b5fc8e4 + 3efeaf6 commit 9732d42

File tree

2 files changed

+24
-0
lines changed

2 files changed

+24
-0
lines changed
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
cycle_delay_star2.sv
3+
--bound 10
4+
^\[main.p0\] ##\[\*\] main\.x == 4: REFUTED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
10+
The BMC engine gives the wrong answer.
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
module main(input clk);
2+
3+
reg [2:0] x;
4+
5+
initial x=0;
6+
7+
// 0, 1, 2, 3, 3, ...
8+
always @(posedge clk)
9+
if(x<=3) x++;
10+
11+
// fails -- 4 is never reached
12+
initial p0: assert property (##[*] x==4);
13+
14+
endmodule

0 commit comments

Comments
 (0)