Skip to content

Commit 40abc2a

Browse files
authored
Merge pull request #433 from diffblue/sequence1
ebmc: KNOWNBUG test for a bounded sequence expression
2 parents 3e4ea73 + 88209ae commit 40abc2a

File tree

2 files changed

+23
-0
lines changed

2 files changed

+23
-0
lines changed

regression/verilog/SVA/sequence1.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
sequence1.sv
3+
--bound 20 --numbered-trace
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
The trace shown only has one state, but 10 are expected.

regression/verilog/SVA/sequence1.sv

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
module main;
2+
3+
reg [31:0] x;
4+
wire clk;
5+
6+
initial x=0;
7+
8+
always @(posedge clk)
9+
x<=x+1;
10+
11+
// fails, and we want to see a trace 0...9
12+
initial p0: assert property (##[0:9] x==100);
13+
14+
endmodule

0 commit comments

Comments
 (0)