Hardware Reference
In-Depth Information
(d) next_event_a! e [m:n] p
This property holds in the current clock tick iff e holds at least n times, starting
at the current clock tick, and p holds at the m th through n th occurrences,
inclusive, of e .
(e) next_event_e e [m:n] p
This property holds in the current clock tick iff p holds at some occurrence of
e among its m th through n th occurrences, inclusive, starting at the current clock
tick, or there are less than n occurrences of e .
(f) next_event_e! e [m:n] p
This property holds in the current clock tick iff p holds at some occurrence of
e among its m th through n th occurrences, inclusive, starting at the current clock
tick, or there are less than n occurrences of e .
11.4.
Write the following assertions:
(a) For each request, an acknowledgment should be sent from 2 to 5 times
(b) For each request, an acknowledgment should be sent 2 or 5 times
11.5. Implement the following assertion: In the transaction delimited by the
start_t and end_t , there should be an even number of actions ( act ).
11.6. What is the meaning of the following assertions?
a1: assert property (a[=1]);
a2: assert property ( strong (a[=1]));
a3: assert property (a[=1] |-> b);
Discuss their efficiency in simulation and in FV.
11.7. Implement the assertion from Example 11.14 without using operators from
the intersect family.
11.8. Implement the assertion from Example 11.15 to ignore read and write
requests happening simultaneously with the end of the transaction end_t .
11.9. During a memory transaction (delimited by start_t and end_t ), the snoop
request ( snoop_req ), and the credit update message ( credit_update ) must be sent
in any order. The transaction must terminate in the clock tick when the later of these
two events happen.
11.10. Which of the following assertions is equivalent to the assertion from
Example 11.19 ?
a1: assert property (
write |=> read[=1] intersect write[->1]);
a2: assert property (
write |=> read[=1] ##1 1 intersect write[->1]);
a3: assert property (
write |=> read[=1:$] intersect write[->1]);
a4: assert property (
write |=> read[=1:$] ##1 1 intersect write[->1]);
a5: assert property (
write |=> ##[ * ] read ##1 1[ * ] intersect write[->1]);
Search WWH ::




Custom Search