1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain, for
// any use, without warranty, 2022 by Antmicro Ltd.
// SPDX-License-Identifier: CC0-1.0
module t (/*AUTOARG*/
clk
);
input clk;
int cyc = 0;
logic val = 0;
always @(posedge clk) begin
cyc <= cyc + 1;
val = ~val;
end
property check(int cyc_mod_2, logic expected);
@(posedge clk)
cyc % 2 == cyc_mod_2 |=> val == expected;
endproperty
// Also checks parsing 'var datatype'
property check_if_1(var int cyc_mod_2);
check(cyc_mod_2, 1);
endproperty
// Also checks parsing 'signing range'
property check_if_gt_5(signed [31:0] cyc);
@(posedge clk)
cyc > 5;
endproperty
property pass_assertion(int cyc);
disable iff (cyc <= 10)
cyc > 10;
endproperty
int expected_fails = 0;
assert property(check(0, 1))
else begin
// Assertion should pass
$display("Assert failed, but shouldn't");
$stop;
end
assert property(check(1, 1))
else begin
// Assertion should fail
expected_fails += 1;
end
assert property(check_if_1(1))
else begin
// Assertion should fail
expected_fails += 1;
end
logic out = 1;
property prop_a;
@(posedge clk) disable iff (cyc <= 1) out;
endproperty : prop_a
property prop_b();
@(posedge clk) disable iff (cyc <= 1) out;
endproperty : prop_b
assert property(disable iff (cyc < 5) check_if_gt_5(cyc + 1));
assert property(@(posedge clk) pass_assertion(cyc));
assert property (prop_a) else $error($sformatf("property check failed :assert: (False)"));
assert property (prop_a()) else $error($sformatf("property check failed :assert: (False)"));
assert property (prop_b) else $error($sformatf("property check failed :assert: (False)"));
assert property (prop_b()) else $error($sformatf("property check failed :assert: (False)"));
always @(posedge clk) begin
if (expected_fails == 2) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule
|
