Hardware Reference
In-Depth Information
basetime
.Line
3
specifies that when
ev1
occurs, the value of
$time
is stored in
basetime
. According to Line
4
, at the nearest strictly subsequent occurrence of
ev2
,thevalueof
$time
must be at least the sum of
basetime
and
mintime
.
t
Example 12.2.
Write an assertion to check that after an occurrence of event
ev_start
, event
ev_wait
cannot occur any earlier than the time step of the first
occurrence of event
ev_enable
.
Solution:
This solution assumes that in any time step these events will occur before
the Observed region.
sequence
s_ev(
event
ev);
1
@(ev) 1'b1
2
##0 @(ev_enable
or
ev_wait) 1'b1;
3
endsequence
4
a_order:
assert property
(
5
@(ev_start) 1'b1
6
|=> @(ev_enable
or
ev_wait) (
7
s_ev(ev_wait).triggered
8
->
9
s_ev(ev_enable).triggered
10
)
11
);
12
The basic idea of this solution is as follows. If
ev_start
occurs, then advance to
the nearest strictly subsequent occurrence of either
ev_enable
or
ev_wait
. In that
time step, if
ev_wait
has occurred, then
ev_enable
must also have occurred.
In Line
6
, the antecedent of
|=>
matches at an occurrence of
ev_start
. The con-
sequent is clocked by the compound event expression “
ev_enable
or
ev_wait
”,
so it advances to the nearest strictly subsequent occurrence of either
ev_enable
or
ev_wait
. Lines
8
through
10
use the Boolean implication
->
to encode the check
that if
ev_wait
has occurred in the current time step, then
ev_enable
must also
have occurred in the current time step. The job of
s_ev
is to detect whether its event
formal argument
ev
occurs. The detection is accomplished by applying sequence
method
triggered
to instances of
s_ev
in Lines
8
and
10
.
In Line
2
,
s_ev
begins a match at an occurrence of its event formal argument
ev
.Line
3
is counterintuitive. It addresses the following restriction on the use of
triggered
: the ending clock of a sequence instance to which
triggered
is applied
must be identical to the clock governing the context in which the application of
triggered
appears. In Lines
8
and
10
,
triggered
is applied in a context clocked
by
ev_enable
or
ev_wait
,soLine
3
ensures that
s_ev
ends on this clock. Line
3
does not actually cause any time advance for matches of the instances of
s_ev
in
Lines
8
and
10
. The reason is that the actual event arguments in these instances are
ev_wait
and
ev_enable
. If one of these events occurs in a time step, then a fortiori
the compound event “
ev_enable
or
ev_wait
” occurs in that time step.
t
Search WWH ::
Custom Search