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