Hardware Reference
In-Depth Information
a19:
assert property
(
1
@(
posedge
clk)
2
sync_accept_on
(reset || $past(reset, , , @(
posedge
clk)))
3
dOut == $past(dIn)
4
);
5
Fig. 13.11
Abort with a compound abort condition
a_abort_subproperties:
assert property
(
1
@(
posedge
clk)
2
a |=>
3
(
accept_on
(retry) b[
*
2])
4
and
5
(
reject_on
(bad) c |=> !c)
6
);
7
Fig. 13.12
Assertion with multiple abort subproperties
in which
posedge
clk
occurs. If we need to check that
dOut
is equal to last cycle's
value of
dIn
, but only if no reset occurred in either cycle, this can be accomplished
by the code in Fig.
13.11
(see also Exercise
13.3
).
13.2.2
Aborts as Subproperties
Since an abort is a property, it participates in the determination of the result of
evaluation of an enveloping property in the same way as other subproperties,
regardless of whether the disposition of the abort is due to occurrence of the abort
condition.
In the assertion of Fig.
13.12
, the consequent of
|=>
in Line
3
is the conjunction
of two abort subproperties.
Consider the waveform of Fig.
13.13
.Theattemptof
a_abort_subproperties
beginning at time 20 starts subevaluations of Lines
4
and
6
at time 40. The
occurrence of
retry
in the time step after time 45 causes the evaluation of Line
4
to
pass. The evaluation of Line
6
continues, and the occurrence of
bad
in the time step
after time 55 causes the evaluation of Line
6
to fail. The overall assertion therefore
fails. The attempt of
a_abort_subproperties
beginning at time 60 passes because
Line
4
results in success at time 100 and Line
6
results in vacuous success at time 80.
Search WWH ::
Custom Search