Basic Properties - SVA: The Power of Assertions in SystemVerilog - page 97

The explicit always operator is rarely used. The vast majority of assertions are
either written outside procedural code or inside always procedures 4 and thus have

the implicit outermost always operator.
As in the case of the explicit double always operators, an always property in the
body of a continuously monitored assertion may result in degradation of simulation
performance.

Efficiency Tip. Do not explicitly specify the outermost always in continuously
monitored assertions.

Example 5.9. Check that signal sig may only have values 0, 1, 2, or 4.

Solution:

a1: assert property (@( posedge clk) sig inside {0, 1, 2, 4});
assuming that a1 is a standalone assertion.
Discussion: Following the efficiency tip, this assertion should not be written as

a2: assert property (@( posedge clk)
always sig inside {0, 1, 2, 4});
Although assertions a1 and a2 are equivalent, simulation performance of a2 may be
worse.

t

5.4 S_eventually Property

Property s_eventually p is true in clock tick i iff p is true in some clock tick
j i . It follows that property s_eventually p is true iff property p is true in some
clock tick, as shown in Fig. 5.4 .
The reader may wonder why the keyword s_eventually has a prefix s_ .As
explained in Chap. 10 , s_eventually is a strong operator, and in SVA names of
strong operators have a prefix s_ .
Similar to always p , property s_eventually p defines a series of evaluations
of p .Butfor s_eventually p to succeed only requires that at least one of those
evaluations succeed.

p

Fig. 5.4 s_eventually
property clock ticks

4 See Chap. 14 for discussion about procedural concurrent assertions.