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

clk

en

e

p

Fig. 11.3 Next occurrence

Such language extensions using property definitions can be placed in packages
for reuse. t

Example 11.9. Example 11.8 shows a weak form of the next_occurrence pro-
perty. In the strong version of this property, e[->1] must happen, and property p
should hold when e happens. This means that we must replace the suffix implication
operator used in Example 11.8 with the followed-by (suffix conjunction) operator:

property strong_next_occurrence(e, property p);
e[->1] #-# p;
endproperty

t

Efficiency Tip. Using big factors and ranges in goto repetition is inefficient both
in simulation and in formal verification. In simulation, goto repetition may be
expensive if it causes long or never-ending attempts, and especially for overlapping
attempts, as explained in Sect. 19.3 . For example,

assert property (a ##1 b[->1] |=> c);
is efficient if b happens every few clock ticks; it can be extremely inefficient if a
often happens, and b never happens or if its occurrences are rare. The reason is that
many property evaluation attempts may be simultaneously accumulated.

11.1.3 Nonconsecutive Repetition

Motivation Example.

Example 11.10. Between the occurrences of the transmission start start_t and the
transmission end end_t , exactly four packets must be sent. Each time a packet is
sent, sent is asserted. The value of sent is not to be checked when start_t or
end_t is asserted.