Advanced Sequences - SVA: The Power of Assertions in SystemVerilog - page 260

a6: assert property (
write |=> ##[ * ] read ##1 1[+] intersect write[->1]);
a7: assert property (
write |=> ##[+] read ##1 1[ * ] intersect write[->1]);
a8: assert property (
write |=> ##[+] read ##1 1[+] intersect write[->1]);

11.11. Implement the following assertion: if a transaction contains at least two read
requests, there should be at least three clock tick delay between it and the following
transaction. Assume that the transactions cannot overlap.

11.12. Write the following assertions:

(a) After start is asserted, at least one of the following events should happen: two
consecutive read or two consecutive write . When the first such event happens
(e.g., if two consecutive write happen first then in the clock tick of the second
write ), done must be asserted.
(b) When after start is asserted, one of the following events happens for the first
time: two consecutive read or two consecutive write , done must be asserted
(e.g., if two consecutive write happen first then in the clock tick of the second
write ).
(c) After start is asserted either read or write request should arrive, and in the
clock tick when the first of them arrives, done must be asserted.
(d) In the clock tick when one of the read or write requests arrives for the first
time, done must be asserted.
11.13. Show that the following properties are not equivalent (Example 11.25 ):

(a) a |-> b ##1 first_match (c[ * ] ##1 d)##1 e and
a |-> b ##1 c[ * ] ##1 d ##1 e
(b) a ##1 first_match (b[ * ] ##1 c)|-> d and a ##1 b[ * ] ##1 c |-> d
11.14. Read transaction (delimited by start_read and end_read ) may only be
issued if a write transaction (delimited by srart_write and end_write ) finished
beforehand.

11.15. Implement the past temporal operator before for a Boolean argument (see
Sect 11.2.1.1 ).

11.16. Implement the past temporal operator backto for Boolean arguments (see
Sect 11.2.1.1 ).

11.17. Modify the sequence event control example in Sect. 11.3.1 to take the reset
rst into account in the sequence.