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

subsequence synchronizes between ev1 and ev2 .By CF3 , ev2 flows to and governs
c ,but ev2 does not flow out of the enclosing parentheses by CF6 . As a result, |=>
is a synchronizer between ev2 and ev1 . In summary, the property is equivalent to
the following, in which each of the Booleans is explicitly clocked:

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

t

Example 12.5. Analyze the clock flow in the following module:

module m1 ( logic a, b, c, d, event ev1, ev2);

1

default clocking EV1 @(ev1); endclocking

2

sequence s4; b ##1 @(ev2) c; endsequence

3

a10: assert property (a ##1 s4 |=> d);

4

endmodule

5

Solution: By CF1 , ev1 flows to a10 , hence flows to and governs a ( CF7 ) and flows
across ##1 to the instance of s4 ( CF8 ). By CF5 , ev1 flows into the body of s4 for
this instance and also across the instance ( CF5 ). Within the body of s4 , ev1 flows
to and governs b ( CF7 ), flows across ##1 ( CF8 ), and stops at @(ev2) ( CF4 ). ev2
governs c ( CF3 , CF7 ), but ev2 does not flow out of the instance of s4 ( CF5 ). ev1
flows across |=> ( CF8 ), and so it flows to and governs d ( CF7 ). In summary, a10
behaves the same as the property in the preceding example.

t

After application of the clock flow rules, each Boolean expression that stands as a
subsequence within a concurrent assertion must be governed by a clock. Otherwise,
the assertion is not legal. The following example illustrates an illegal assertion:

module m2 ( logic a, b, event ev1);

1

a11_illegal: assert property (

2

(@(ev1) a) implies b

3

);

4

endmodule

5

By CF3 and CF7 , ev1 governs a , but by CF6 ev1 does not flow out of the enclosing
parentheses. There is no default clock, so no clock governs b .

12.2.4.2 Semantic Leading Clocks

The rules of semantic leading clocks define how the leading clock or clocks of a
sequence or property are determined from the inside out. One of the basic ideas of
clock flow is that an outer clock is replaced by, rather than flowing through, an inner
clock. This means that @( c )@( d ) p behaves semantically the same as @( d ) p.
Syntactically, the leading clock of @( c )@( d ) p appears to be c, but semantically
it is d .
Another principle of concurrent assertions is that every subsequence, in particular
every Boolean that stands as a subsequence, must be clocked. When examining
semantic leading clocks from the inside out, though, there may be no clock at hand.