Skip to content

Commit 615c98b

Browse files
authored
Merge pull request #875 from diffblue/recursive_property1
SVA: KNOWNBUG test for a recursive property
2 parents 150f03a + 89583c8 commit 615c98b

File tree

2 files changed

+23
-0
lines changed

2 files changed

+23
-0
lines changed

Diff for: regression/verilog/SVA/recursive_property1.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
recursive_property1.sv
3+
--bound 10
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
The parameter list fails to parse.

Diff for: regression/verilog/SVA/recursive_property1.sv

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
module main(input clk);
2+
3+
reg [31:0] x = 0;
4+
always_ff @(posedge clk) x = !x;
5+
6+
// 1800-2017 16.12.17
7+
property prop_always(p);
8+
p and (1 |=> prop_always(p))
9+
endproperty
10+
11+
// expected to pass
12+
assert property (prop_always(x <= 1));
13+
14+
endmodule

0 commit comments

Comments
 (0)