Hardware Reference
In-Depth Information
module m_illegal_disable_nesting( logic reset, a, b, clk);
1
default clocking PCLK @( posedge clk); endclocking
2
property p_disable;
3
disable iff (reset) a |=> b;
4
endproperty
5
a_disable: assert property (
6
disable iff (reset)
7
p_disable
8
) else $error("FAIL");
9
endmodule
10
Fig. 13.3
Illegal nesting of disable conditions
argument value of a property declaration. This is especially useful when creating
reusable properties for a library. For example,
1 property p_inferred_disable(x, y,
2 event ck = $inferred_clock,
3 logic rst = $inferred_disable);
4 disable iff (rst) @ck x |=> y;
5 endproperty
6 module m_inferred_disable( logic reset, a, b, clk);
7
default disable iff reset;
default clocking @( posedge clk); endclocking
8
a_inferred_disable:
9
assert property (p_inferred_disable(a, b))
10
else $error("FAIL");
11
endmodule
12
The property declaration p_inferred_disable uses the inferred value functions
to specify that in the absence of the actual argument for ck or for rst ,thevalueof
the argument should be inferred from the instantiation context. In the case of rst ,
it can only be inferred from the default disable declaration. If there is none then
the inferred value is 1'b0 . The assertion a_inferred_disable does not specify
these arguments; therefore, the clocking event is inferred from the default clocking
declaration as posedge clk , and the disabling condition is inferred from default
disable declaration as reset .
13.1.2
Aborts
The term abort refers to resets specified by the following property operators:
accept_on , reject_on , sync_accept_on , and sync_reject_on . The first two of
these are asynchronous aborts, while the last two are synchronous aborts. Each of
these property operators has two operands. The first is the abort condition , which is
enclosed in parentheses, and the second is the underlying property governed by the
abort operator. Here is an example of the syntax:
Search WWH ::




Custom Search