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

@( posedge clk) (pswitch && pmode == normal ##1 !pswitch[ * ]) ##0
ready;
endsequence : begin_mode
initial begin :I1
@begin_mode setup(mode);
$display("Mode started");
end
//...
endmodule

t

In this example, sequence begin_mode is used as event control in initial
procedure I1 . The event control subjects its execution to obtaining a match point
of sequence begin_mode . Accordingly, the initial process gets suspended as it must
wait until the Observed region where the sequence is evaluated. If the match point is
attained there, the simulation control makes its way back to the Active region again
following the normal course via the Reactive region. Now in the Active region, the
initial procedure resumes to execute the $display statement.

Exercises

11.1. Two consecutive requests should be separated with four ack_wait , one
acknowledgement ( ack ), and two idle cycles (in this order).
11.2. What is the difference between the assertion from Example 11.6 and the
assertions below?

a1: assert property (start_ev |=> strong (next[->2:$] ##1 end_ev
));
a2: assert property (start_ev ##1 next[->2:$] |=> end_ev);

11.3. In this exercise, e is a Boolean expression, m and n are integer constants, p is
a property. Implement the following PSL operators as SVA property definitions:

(a) next_event e [n] p

This property holds in the current clock tick iff e does not hold at least n times,
starting at the current clock tick, or p holds at the n th occurrence of e .

(b) next_event! e [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 n th occurrence of e .

(c) next_event_a e [m:n] p

This property holds in the current clock tick iff p holds at the m th through
n th occurrences, inclusive, of e , starting at the current clock tick. If there are
less than n occurrences of e then p holds on all of them, starting from the m th
occurrence.