Skip to content

Commit 07d9e70

Browse files
committed
test with signed ranking function
1 parent 66a241c commit 07d9e70

File tree

2 files changed

+25
-0
lines changed

2 files changed

+25
-0
lines changed
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
signed1.sv
3+
--ranking-function "(-$signed({1'b0,counter}))"
4+
^\[main\.property\.p0\] always s_eventually main.counter == 0: PROVED$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// count down from 10 to 0
2+
3+
module main(input clk);
4+
5+
reg [7:0] counter;
6+
7+
initial counter = 0;
8+
9+
always @(posedge clk)
10+
if(counter != 100)
11+
counter++;
12+
else
13+
counter = 0;
14+
15+
// expected to pass
16+
p0: assert property (s_eventually counter == 0);
17+
18+
endmodule

0 commit comments

Comments
 (0)