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

CF8 A clock that flows to one of the operators ##n , [ * n] , |-> , |=> , #-# , and
#=# flows across the operator. If the operator is not a synchronizer, then the
clock also governs time advances associated with the operator. Analogous
rules apply to ranged variants of [ * n] .
CF9 A clock that flows to the left operand of one of the infix operators or ,
and , intersect , within , throughout , iff , implies , and until flows to
the operator and distributes to (i.e., flows into) both operands. The clock
also governs time advance for until . Analogous rules apply to the various
variants of these operators.
CF10 A clock that flows to one of the prefix operators not , nexttime , always , and
eventually flows to the operand of the operator. The clock also governs time
advance in nexttime , always , and eventually . Analogous rules apply to
all the variants of these operators.
CF11 A clock that flows to an if - else governs the test condition of the if - else .
The clock also flows into each of the underlying properties of the if - else .
Analogous rules apply to case .
CF12 A clock that flows to a disable iff , accept_on ,or reject_on flows into
the underlying property. The clock does not govern the reset condition.
CF13 A clock that flows to a sync_accept_on or sync_reject_on governs the
abort condition and flows into the underlying property.

The following examples illustrate the clock flow rules.

Example 12.3. Analyze the clock flow in the following property:

@(ev1) a |=> b ##1 @(ev2) c

Solution: By CF3 , ev1 flows to a .By CF7 , ev1 governs a and flows to |=> .By CF8 ,
ev1 flows across |=> to b .By CF7 , ev1 governs b and flows to ##1 .By CF8 , ev1
flows across ##1 to @(ev2) .By CF4 , the scope of ev1 does not flow across @(ev2) .
Therefore, ##1 is a synchronizer between ev1 and ev2 .By CF3 , ev2 flows to c .
By CF7 , ev2 governs c . In summary, the property is equivalent to the following, in
which each of the Booleans is explicitly clocked:

@(ev1) a |=> @(ev1) b ##1 @(ev2) c

t

Example 12.4. Analyze the clock flow in the following property:

@(ev1) a ##1 (b ##1 @(ev2) c) |=> d

Solution: By CF3 , CF7 , and CF8 , ev1 flows to and governs a and flows across
##1 to the parenthesized subsequence (b ##1 @(ev2)c) .By CF6 , ev1 flows into
and across the parenthesized subsequence. Therefore, ev1 flows to and across
|=> ( CF8 ), and so it flows to and governs d ( CF7 ). Within the parenthesized
subsequence, ev1 flows to, governs, and flows across b ( CF7 ), flows across ##1
( CF8 ), and ends at @(ev2) ( CF4 ). Therefore, the ##1 within the parenthesized