| |
|
|
|
|
|
| |
|
|
| |
 |
disable iff
|
|
|
disable iff disables the property if the expression it is checking is active. This is normally used for reset checking and if reset is active, then property is disabled. Also important thing to note is, if property gets activated in last clock it is suppose to run for next 10 clock, but very next clock there is reset, then previous thread, which was spawned is also diabled/killed. |
| |
|
|
|
|
Below example shows some of the usages of disable_iff. |
| |
|
|
| |
 |
Example : disable iff
|
| |
|
|
|
|
1 //+++++++++++++++++++++++++++++++++++++++++++++++++
2 // DUT With assertions
3 //+++++++++++++++++++++++++++++++++++++++++++++++++
4 module disableiff_assertion(
5 input wire clk,req,reset,
6 output reg gnt);
7 //=================================================
8 // Sequence Layer
9 //=================================================
10 sequence req_gnt_seq;
11 // (~req & gnt) and (~req & ~gnt) is Boolean Layer
12 (~req & gnt) ##1 (~req & ~gnt);
13 endsequence
14 //=================================================
15 // Property Specification Layer
16 //=================================================
17 property req_gnt_prop;
18 @ (posedge clk) // At every posedge clk
19 disable iff (reset) // disable if reset is asserted
20 req |=> req_gnt_seq;
21 endproperty
22 //=================================================
23 // Assertion Directive Layer
24 //=================================================
25 req_gnt_assert : assert property (req_gnt_prop);
26 //=================================================
27 // Actual DUT RTL
28 //=================================================
29 always @ (posedge clk)
30 gnt <= req;
31
32 endmodule
33
34 //+++++++++++++++++++++++++++++++++++++++++++++++
35 // Testbench Code
36 //+++++++++++++++++++++++++++++++++++++++++++++++
37 module disableiff_assertion_tb();
38
39 reg clk = 0;
40 reg reset, req = 0;
41 wire gnt;
42
43 always #3 clk ++;
44
45 initial begin
46 reset <= 1;
47 #20 reset <= 0;
48 // Make the assertion pass
49 #100 @ (posedge clk) req <= 1;
50 @ (posedge clk) req <= 0;
51 // Make the assertion fail
52 #100 @ (posedge clk) req <= 1;
53 repeat (5) @ (posedge clk);
54 req <= 0;
55 #10 $finish;
56 end
57
58 disableiff_assertion dut (clk,req,reset,gnt);
59
60 endmodule
You could download file disableiff_assertion.sv here
|
| |
|
|
| |
|
Simulation : disable iff
|
| |
|
|
|
|
"disableiff_assertion.sv", 25: disableiff_assertion_tb.dut.req_gnt_assert:
started at 237s failed at 243s
Offending '((~req) & gnt)'
"disableiff_assertion.sv", 25: disableiff_assertion_tb.dut.req_gnt_assert:
started at 243s failed at 249s
Offending '((~req) & gnt)'
"disableiff_assertion.sv", 25: disableiff_assertion_tb.dut.req_gnt_assert:
started at 249s failed at 255s
Offending '((~req) & gnt)'
"disableiff_assertion.sv", 25: disableiff_assertion_tb.dut.req_gnt_assert:
started at 255s failed at 261s
Offending '((~req) & gnt)'
$finish called from file "disableiff_assertion.sv", line 55.
|
| |
|
|
| |
|
Property Arguments
|
|
|
A property can be declared with optional arguments, When a property is used in as assert or cover or assume, actual arguments can be passed to the property. The property gets expanded with the actual arguments by replacing the formal arguments with the actual arguments. |
| |
|
|
|
|
There are type of arguments declaration. |
| |
|
|
|
|
- No Type : Here input arguments are not typed.
- With Type : Here input arguments are typed.
|
| |
|
|
|
|
One of the big advantage of using property with argument, is it can be reused as shown in below example. |
| |
|
|
|
|
|
| |
|
|
| |
|
Example : Property Arguments
|
| |
|
|
|
|
1 //+++++++++++++++++++++++++++++++++++++++++++++++++
2 // DUT With assertions
3 //+++++++++++++++++++++++++++++++++++++++++++++++++
4 module propargs_assertion();
5 logic clk = 0;
6 logic req,gnt;
7 logic a,b;
8 //=================================================
9 // Sequence Layer with args (NO TYPE)
10 //=================================================
11 sequence notype_seq (X, Y);
12 (~X & Y) ##1 (~X & ~Y);
13 endsequence
14 //=================================================
15 // Sequence Layer with args (NO TYPE)
16 //=================================================
17 sequence withtype_seq (X, Y);
18 (~X & Y) ##1 (~X & ~Y);
19 endsequence
20 //=================================================
21 // Property Specification Layer
22 //=================================================
23 property req_gnt_notype_prop;
24 @ (posedge clk)
25 req |=> notype_seq(req,gnt);
26 endproperty
27
28 property req_gnt_type_prop;
29 @ (posedge clk)
30 req |=> withtype_seq(req,gnt);
31 endproperty
32
33 property a_b_notype_prop;
34 @ (posedge clk)
35 a |=> notype_seq(a,b);
36 endproperty
37
38 property a_b_type_prop;
39 @ (posedge clk)
40 a |=> withtype_seq(a,b);
41 endproperty
42 //=================================================
43 // Assertion Directive Layer
44 //=================================================
45 req_gnt_notype_assert : assert property (req_gnt_notype_prop);
46 req_gnt_type_assert : assert property (req_gnt_type_prop);
47 a_b_notype_assert : assert property (a_b_notype_prop);
48 a_b_type_assert : assert property (a_b_type_prop);
49 //=================================================
50 // Actual DUT RTL
51 //=================================================
52 always @ (posedge clk)
53 gnt <= req;
54
55 always @ (posedge clk)
56 b <= a;
57
58 //+++++++++++++++++++++++++++++++++++++++++++++++++
59 // Assertion testing code
60 //+++++++++++++++++++++++++++++++++++++++++++++++++
61 always #3 clk ++;
62
63 initial begin
64 // Make the assertion pass
65 #100 @ (posedge clk) req <= 1;
66 @ (posedge clk) req <= 0;
67 // Make the assertion fail
68 #100 @ (posedge clk) req <= 1;
69 repeat (2) @ (posedge clk);
70 req <= 0;
71
72 // Make the assertion pass
73 #100 @ (posedge clk) a <= 1;
74 @ (posedge clk) a <= 0;
75 // Make the assertion fail
76 #100 @ (posedge clk) a <= 1;
77 repeat (2) @ (posedge clk);
78 a <= 0;
79 #10 $finish;
80 end
81
82 endmodule
You could download file propargs_assertion.sv here
|
| |
|
|
| |
|
Simulation : Property Arguments
|
| |
|
|
|
|
"propargs_assertion.sv", 45: propargs_assertion.req_gnt_notype_assert:
started at 219s failed at 225s
Offending '((~req) & gnt)'
"propargs_assertion.sv", 46: propargs_assertion.req_gnt_type_assert:
started at 219s failed at 225s
Offending '((~req) & gnt)'
"propargs_assertion.sv", 47: propargs_assertion.a_b_notype_assert:
started at 441s failed at 447s
Offending '((~a) & b)'
"propargs_assertion.sv", 48: propargs_assertion.a_b_type_assert:
started at 441s failed at 447s
Offending '((~a) & b)'
|
| |
|
|
| |
|
Recursive Property
|
|
|
When a named property calls itself, it is called recursive property. Following restiction apply on recursive property. |
| |
|
|
|
|
- The negation operator not cannot be applied to any property expression that instantiates a recursive property. In particular, the negation of a recursive property cannot be asserted or used in defining another property.
- The operator disable iff cannot be used in the declaration of a recursive property.
- Following example shows recursive property.
|
| |
|
|
| |
|
Example : Recursive Property
|
| |
|
|
|
|
1 //+++++++++++++++++++++++++++++++++++++++++++++++++
2 // DUT With assertions
3 //+++++++++++++++++++++++++++++++++++++++++++++++++
4 module recursive_assertion();
5 logic clk = 0;
6 logic req;
7 //=================================================
8 // Property Specification Layer
9 //=================================================
10 property recursive_prop(M);
11 M and (1'b1 |=> recursive_prop(M));
12 endproperty
13 //=================================================
14 // Assertion Directive Layer
15 //=================================================
16 recursive_assert : assert property (recursive_prop(req));
17 //+++++++++++++++++++++++++++++++++++++++++++++++++
18 // Assertion testing code
19 //+++++++++++++++++++++++++++++++++++++++++++++++++
20 always #1 clk ++;
21
22 initial begin
23 // Make the assertion pass
24 #100 @ (posedge clk) req <= 1;
25 repeat (20) @ (posedge clk);
26 req <= 0;
27 #10 $finish;
28 end
29
30 endmodule
You could download file recursive_assertion.sv here
|
| |
|
|
| |
|
Simulation : Recursive Property
|
| |
|
|
|
|
|
| |
|
|
| |
|
|
| |
|
|
|
|
|
| |
|
|
