Basic Sequences - SVA: The Power of Assertions in SystemVerilog - page 124

property passes. Sequential property a ##1 b is false in clock tick 1 (recall that the
truth value of a sequential property relates to the initial point of its sequence), while
c is true the first time in clock tick 2. Therefore, property a ##1 b until c fails.
t

Example 6.35. When the first operand of until_with is an integral expression,
and the second one is a sequence, a until_with s may be implemented with
sequential property a[ * ] ##0 s .

t

Efficiency Tip. Infinite repetition ranges may be inefficient in simulation. Their
efficiency is explained in detail in Sect. 19.3 . Infinite repetition ranges are efficient
in FV if their lower bound is small.
Previous examples show that sequence and property operators are in some cases
interchangeable in assertions. In such cases, it is a matter of style or of simulator
efficiency, which solution to choose. The sequence operators are often more concise,
but in many cases property operators are more readable. Sequence operators are
more flexible as they can appear in both sequences and properties, whereas property
operators may appear only within another property or assertion. On the other hand,
property operators are more generic, as they can have both sequences and properties
as their operands, while sequences may only have sequence (or Boolean) arguments.
This fact makes property-based implementation more suitable for assertion libraries.
We will end this section with an example illustrating some semantic subtlety of
the use of infinite repetition range in the antecedent.

Example 6.36. What does the following assertion mean?
a1: assert property (@( posedge clk) a[+] |-> p);

Solution: For each evaluation attempt a1 checks that when there is a continuous
series of a , property p holds. For example, if there is a series aa at the beginning of
some attempt, p should hold in the first two clock ticks of this attempt. But checking
p in the second clock tick of this attempt is redundant: it will be checked in the first
clock tick of the next attempt. Therefore, the original assertion is equivalent to

a2: assert property (@( posedge clk) a |-> p);

Discussion: There should be no difference between the efficiency of a1 and a2 in
FV, but a2 is extremely inefficient in simulation. t

Efficiency Tip. Never implement the property s |-> p as s[+] |-> p .

6.8 Sequences Admitting Empty Match

Sequences admitting an empty match introduce many subtle points that should be
well understood. Unlike other sequences, sequences that admit an empty match
cannot be promoted to properties according to the definition of sequential property
(Sect. 6.2 ). One such sequence is an empty sequence described in Sect. 6.5.1 .The