Clocks - SVA: The Power of Assertions in SystemVerilog - page 279

Rule LC1 captures the fact that an outer clock applied to x is semantically
significant if, and only if, something within x requires an incoming clock, as
evidenced by the presence of inherited in LC.x/.Rule LC3 says that Booleans
require incoming clocks.
Rules LC1 through LC9 account for semantic leading clocks in sequences. They
do not enforce the various restrictions on the clocking of sequences, such as those
from Sect. 12.2.3 . Rather, they allow for partial clocking of sequences that still
requires an incoming clock, as in
(a[ * 2] and @(ev1) b[->1]) ##1 c
LC of this sequence is f inherited ; ev1 g , where inherited records the fact that a[ * 2]
requires an incoming clock. Since and is not a synchronizer for sequences, the
incoming clock must be identical to ev1 for the concurrent assertion in which this
sequence appears to be legal.
Rules LC1 , LC2 , and LC9 through LC17 account for semantic leading clocks in
properties. LC13 and LC14 capture the fact that the incoming clock governs time
advancement in the temporal operators of the nexttime , always , s_eventually ,
and until families. LC15 indicates that the condition of an if-else or case is
governed by the incoming clock, while LC16 indicates that the reset condition of an
asynchronous abort is independent of the incoming clock.
Rule LC17 reflects the definition in the LRM for synchronous aborts, namely,
that the incoming clock governs the abort condition and serves as leading semantic
clock. However, the LRM leaves ambiguous whether and how synchronous abort
operators may be used as synchronizers. 10 Therefore, it is advised to use syn-
chronous aborts only when there is at most one explicit (i.e., non- inherited ) semantic
leading clock of the underlying property and this clock is identical to the incoming
clock.
The top-level property of a concurrent assertion is always required to have a
single semantic leading clock after the resolution of clock scoping. If p is such
a top-level property, then this means that LC.p/ must have one of the following
forms:
￿ f c g . In this case, c is the unique, explicit semantic leading clock of p, and no
incoming clock is required or has any effect.
￿ f inherited g . In this case, p has no explicit semantic leading clock and requires an
incoming clock, either from default clocking or from a procedural context.
￿ f inherited ;c g . In this case, c is an explicit semantic leading clock of p,butp also
requires an incoming clock, which must be identical to c. 11
10 In fact, various rewrite rules in Annex F.5 of the LRM lead to the conclusion that, while the abort
condition of a synchronous abort is governed by the incoming clock, the set of semantic leading
clocks is determined from the underlying property, in contradiction to LC17 .
11 The LRM does not define precisely the criterion “identical”, but through examples it indicates
that syntactically identical events are “identical”, while syntactically distinct, but semantically
equivalent, events are not “identical”.