Skip to content

Commit bc7a3df

Browse files
authored
Merge pull request #932 from diffblue/property1
Verilog: KNOWNBUG test for property ... endproperty
2 parents 095ae90 + b395a5e commit bc7a3df

File tree

6 files changed

+23
-0
lines changed

6 files changed

+23
-0
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
KNOWNBUG
2+
named_property2.sv
3+
--bound 20
4+
^\[main\.assert\.1\] always main\.x_is_eventually_ten: PROVED up to bound 20$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
10+
The type checker only allows expressions, not properties in property ...
11+
endproperty.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
module main(input clk);
2+
3+
reg [31:0] x = 0;
4+
always_ff @(posedge clk) x++;
5+
6+
property x_is_eventually_ten;
7+
s_eventually x == 10
8+
endproperty : x_is_eventually_ten
9+
10+
assert property (x_is_eventually_ten);
11+
12+
endmodule

0 commit comments

Comments
 (0)