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

from above or outside. The second set of rules defines the set of semantic leading
clocks for a sequence or property expression. These rules work from the inside out
and capture the notions that inner clocks take precedence over outer clocks and that
some expressions require an incoming clock.
In the presence of instances of named sequences and properties, both sets of
rules are understood to apply to the assertions, sequence expressions, and property
expressions that result from expanding the instances. 8

12.2.4.1 Clock Flow

The clock flow rules define how scopes of clocks descend from the outside in.
They are intended to be intuitive and to reduce the need for parenthesizing and
repetition of clocking event controls. Reliance on the rules can always be reduced by
adding explicit clocking event controls, although doing so in sequence or property
declarations may reduce their reusability. Here are the clock flow rules:

CF1 A default clock flows to every concurrent assertion in its scope.
CF2 An inferred clock for a procedural context (see Sect. 14.2 ) overrides a default
clock and flows to every concurrent assertion in its scope.
CF3 Clock c flows out of @( c ) .
CF4 A clock c that flows to a clocking event control @( d ) does not flow across
the clocking event control. Instead, the scope of c is halted by @( d ) , and the
scope of d begins after @( d ) . 9
CF5 A clock that flows to an instance of a named property flows into the body of
the corresponding declaration. A clock that flows to an instance of a named
sequence flows into the body of the corresponding declaration, whether or
not a sequence method is applied to the instance. Furthermore, if the instance
is of a sequence, then the clock also flows across the instance, regardless of
whether a sequence method is applied. A clock in the body of a declaration
does not flow out of an instance.
CF6 A clock that flows to a parenthesized subexpression (either a subsequence or a
subproperty) flows into the subexpression. If the subexpression is a sequence,
then the clock also flows across the parenthesized subexpression. A clock
inside the subexpression does not flow out of the enclosing parentheses.
This rule applies to parentheses enclosing a sequence to which one or more
sequence match items are attached. Analogous rules apply to operators with
explicit parentheses: strong () , weak () , first_match () .
CF7 A clock that flows to a maximal Boolean expression b governs b and flows
across b. Analogous rules apply to Boolean repetitions b [->n] , b [=n] ,etc.

8 See the Rewriting Algorithms in Annex F.4 of [ 8 ].
9 Rule CF2 can be thought of as a special case of CF4 if the inferred clock is understood to specify
a clocking event control at the beginning of each of the concurrent assertions in its scope.