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

Example 12.6. Compute the set of semantic leading clocks in the following asser-
tion and determine any requirements on the context in which the assertion appears:

a12: assert property (
a or @(ev1) b and nexttime @(ev2) c

);

Solution:

LC. b and nexttime @(ev2) c /
= LC. b / [ LC. nexttime @(ev2) c / ( LC11 )

= f inherited g ( LC3 , LC13 )

Therefore by LC1 ,

LC. @(ev1) b and nexttime @(ev2) c / Df ev1 g

By LC3 , LC. a / Df inherited g , and so by LC11 , the set of semantic leading clocks
for the entire assertion is f ev1 ; inherited g . This means that the assertion must be in a
context that guarantees an incoming clock, either by default clocking or by inference
from a procedural context, and the incoming clock must be identical to ev1 .

t

12.2.5 Finer Points of Multiple Clocks

This section covers a few finer points regarding the use of multiple clocks in
sequences and properties.

12.2.5.1 Clocking LTL Operators

When LTL operators nexttime , always , s_eventually , until , and their variants
are used as synchronizers, it is important to remember that the time advance
specified by the LTL operator is determined by the incoming clock, not by the
leading clock or clocks of the operands. Consider the following:

module m3 ( logic a, b, clk1, clk2);
a13: assert property (
@( posedge clk1) a |-> nexttime @( posedge clk2) b

);
a14: assert property (
@( posedge clk1) a |-> ##1 @( posedge clk2) b

);
endmodule
Assertions a13 and a14 look similar, but they behave differently. In both, the
antecedent of |-> matches whenever the sampled value of a is 1'b1 at an occurrence
of posedge clk1 . Suppose that this occurs at time t 0 .In a13 , posedge clk1