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