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

12.2.3 Restrictions in Multiply Clocked Sequences

The only synchronizers allowed in sequences are ##0 and ##1 . Therefore, the
general form of a multiply clocked sequence s is

s D r 0 ##n 1 r 1 ##n 2 ##n k r k

where k 1, each r i , 0 i k, is a singly clocked sequence, and each n i ,
1 i k, is either 0 or 1 . We may assume that in this form r i and r i C 1 are
differently clocked for each 0 i<k, since otherwise they could be combined
into a larger singly clocked subsequence. Then the sequences r i

are the maximal

singly clocked subsequences of s.
SVA requires that the maximal singly clocked subsequences of a multiply
clocked sequence not admit empty match. This guarantees that each r i has unam-
biguous starting and ending clock ticks for any match, thereby ensuring that there
is a well-defined leading clock and that the clock changes for each synchronizer are
well defined.
For example, the following multiply clocked sequence is illegal:

@(ev1) a[ * ] ##1 @(ev2) b
The maximal singly clocked subsequences are @(ev1)a[ * ] and @(ev2)b , and the
former admits empty match. In this situation, we cannot be sure whether the leading
clock is ev1 or ev2 , and this ambiguity is disallowed. Changing the sequence to
@(ev1) a[+] ##1 @(ev2) b
makes it legal. The first maximal singly clocked subsequence is now @(ev1)a[+] ,
which does not admit empty match. Now we can be sure that the leading clock of
the sequence is ev1 and that ##1 synchronizes between a tick of ev1 and a tick
of ev2 .

12.2.4 Scoping of Clocks

In SVA, clocking event controls are declarations with scopes, not operators. As such,
clocks have no strengths. The scoping rules for clocks have been designed to allow
the scopes of clocks to extend intuitively through the structure of the assertions,
sequences, and properties and to reduce the need for parenthesizing and repetition
of clocking event controls.
There are actually two sets of rules that work together to determine how each
part of a concurrent assertion is clocked. The first set of rules, called clock flow
rules, defines how scopes of clocks descend from the outside in, beginning with
the default clock or inferred clock, if it exists. A basic idea in clock flow is that
the scope of a clocking event cannot flow across another clocking event control. In
other words, the inner clock blocks and takes precedence over a clock flowing in