Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 71

Assertion a1 states that if a is true then it must be followed by b true at the
next clock tick. Since the assertion is not in any procedure, it will evaluate attempts
starting at every clock tick.
The body of assertion a2 also states that if a is true then it must be followed by b
true at the next clock tick. However, since a2 is in an initial procedure, there will be
only one attempt started at the first clock tick, but then due to the always property
operator it will evaluate a |=> b continuously starting at every clock tick.
Is there a difference between the two assertions? If we are concerned about the
first failure that may occur during a simulation, i.e., a being true at a clock tick
followed by b false at the next clock tick, then there is no difference in reporting
the failure. However, if we wish to detect any subsequent failures or we wish to
know when the failing sequence of a and b started, then assertion a1 provides this
information while a2 may not. This is because a2 runs only one attempt, and if
a |=> b fails somewhere it is a failure of always and thus a failure of only that
attempt. In the case of a1 , the failing evaluation attempt of a |=> b will be reported
with its start and end times. Thereafter, the assertion evaluation continues and may
report other failing attempts. t

4.4.2 Clock

Concurrent assertions must be controlled by a clocking event ,or clock and all
the assertion evaluation attempts are synchronized with this event. Subexpressions
of the property expressions may have their own clocking events. Multiclocked
properties are relatively rare, and we postpone their description until Chap. 12 .For
now, we assume that the subexpressions of the assertion property expression do not
use a different clock.
Since concurrent assertions are clocked, the main assertion clock must be present
in the assertion. This clock either should be explicitly specified or inferred from the
context: from an event control in the surrounding always or initial procedure, or
from default clocking . We discuss in detail clock inference rules in Sects. 12.2.2
and 14.2 .
All signal values participating in the property expression are sampled at the
assertion clock tick only, and their values between the clock ticks are completely
ignored. For example, the assertion

a1: assert property (@( posedge clk) a);
passes for the signal waveforms shown in Fig. 4.7 . Although a is low between time
55 and 65, this is considered to be a glitch and is ignored, because the values of a
are sampled on posedge clk , i.e., at times 10, 20, etc.
The role of a clock in concurrent assertions is to convert the continuous time into
the discrete one. This is important since SVA temporal operators are defined for
discrete time.