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