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

For example, in the presence of default clocking, the following concurrent assertion
is legal:
c1: cover property (a ##1 b);
When examining the underlying sequence a ##1 b , there is no clock at hand in
the expression. Therefore, the definition of semantic leading clocks uses a device
to indicate that a clock needs to be provided from outside, namely the inherited
semantic leading clock.
The rules of semantic leading clocks propagate these ideas through the various
sequence and property forms. They appear below and define the set LC of semantic
leading clocks for a sequence or property. In the rules, b denotes a Boolean; n
denotes a natural number; r , r 1 , r 2 denote sequences; item denotes a sequence match
item; p, p 1 , p 2 denote properties; x denotes either a sequence or a property; and c
denotes a clocking event.
LC1 If inherited 2 LC.x/, then LC. @( c ) x/ Df c g[ .LC.x/ f inherited g /.
Otherwise, LC. @( c ) x/ D LC.x/.
LC2 LC. ( x ) / D LC.x/.
LC3 : LC.b/ D LC.b [-> n ] / D LC.b [= n ] / Df inherited g . Analogous rules
apply to variants of these operators.
LC4 LC.b throughout r/ Df inherited g[ LC.r/.
LC5 LC.r 1 and r 2 / D LC.r 1 / [ LC.r 2 /. The same rule applies if and is replaced
by any of or , intersect , and within .
LC6 LC.r 1 ## nr 2 / D LC.r 1 /. Analogous rules apply to variants of ## n.
LC7 LC.r [ * n ] / D LC.r/. Analogous rules apply to variants of [ * n ] .
LC8 LC. ( r , item ) ) D LC.r/.
LC9 LC. first_match ( r ) ) D LC.r/. The same rule applies if first_match ()
is replaced by strong () or weak () .
LC10 LC. not p/ D LC.p/.
LC11 : LC.p 1 and p 2 / D LC.p 1 / [ LC.p 2 /. The same rule applies if and is
replaced by any of or , iff , and implies .
LC12 LC.r |-> p/ D LC.r/. The same rule applies if |-> is replaced by any of
|=> , #-# , and #=# .
LC13 LC. nexttime p/ D inherited g . The same rule applies if nexttime
is replaced by always or s_eventually or by variants of any of these
operators.
LC14 LC.p 1 until p 2 / Df inherited g . Analogous rules apply to the variants of
until .
LC15 If p is an if-else or case property, then LC.p/ Df inherited g .
LC16 LC. accept_on ( b ) p/ D LC.p/. The same rule applies if accept_on is
replaced by reject_on or disable iff .
LC17 LC. sync_accept_on ( b ) p/ Df inherited g . The same rule applies when
sync_accept_on is replaced by sync_reject_on .