Hardware Reference
In-Depth Information
dout <= f_ecap(d1);
end
By
V4
, the references to terms
e1
and
e2
in the assertion
a8_2
do not affect
validity, so
posedge
(e1|e2)
is inferred as the leading clock for assertion
a8_1
.
Such a reference can be in the body property or in an action block of the assertion
statement.
t
Terms from an event expression may be used within assertion statements in
the procedural block without affecting validity.
When the event control of a procedure consists of a list of event expressions,
separated either by comma or by operator
or
, then the Rule of Clock Inferencing
requires that there be only one event expression from the list that is inferable and
valid for the procedure. Otherwise, no clock is inferred from the procedure.
Example 14.9.
No clock inferred—two valid inferable event expressions:
always
@(
posedge
e1
or posedge
e2)
begin
d1 <= i1|i2 ;
a9:
assert property
(d1 |=> i3|i4);
dout <= f_ecap(d1);
end
The Rule of Clock Inferencing is violated.
t
A clock is inferred only if a single valid inferable event expression is specified
in the event control.
In the following example, asynchronous reset is specified as an event expression.
Even though the event control has two inferable event expressions, only one is valid.
Example 14.10.
A common use of asynchronous reset event:
always
@(
posedge
e1
or posedge
reset)
begin
if
(reset)
d1 <= 0;
else begin
d1 <= i1|i2;
a10:
assert property
(d1 |=> i3|i4);
dout <= f_ecap(d1);
end
end
Search WWH ::
Custom Search