Basic Sequences - SVA: The Power of Assertions in SystemVerilog - page 130

b there is a clock tick with a low value of a , i.e., exactly when property a until b
fails. If b never happens and a always happens then any finite fragment of the trace
cannot witness the inability of sequence a[ * ] ##1 b to match, since potentially b
could happen immediately after the end of this fragment. This is, again, consistent
with the definition of until , which requires a always to happen if b never happens.
Exercises
6.1. Write a sequence implementing the scenario “Asserted request is deasserted in
the next clock tick”.
6.2. Show that if r , s , and t are sequences then
(a) (r or s) ##n t is equivalent to (r ##n t) or (s ##n t)
(b) r##n(s or t) is equivalent to (r ##n s) or (r ##n t) .
Is (r ##n s) or t equivalent to (r or t) ##n (s or t) ?
6.3. Modify the transaction definition from Example 6.32 so that the beginning of
the next transaction cannot happen in the same cycle as the end of the previous one.
6.4. During transaction execution the ready flag must be low. The transaction is
delimited by bot and eot signals. What happens if transactions can overlap?
6.5. Modify the assertion from Example 6.24 to account only for the acknowledg-
ment coming strictly after the request.
6.6. Modify the assertion from Example 6.29 to require the signal to be active
during exactly five cycles.