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

10 20 30 40 50 60 70 80 90 100

clk1

a

clk2

b

Fig. 12.13 Waveform for assertion a13_v2 of module m3_v2

￿ First proceed to the nearest current or future tick of the governing clock (i.e., first
align with the governing clock).
￿ From that point, advance to the next tick of the governing clock.

Here is an example illustrating such use of nexttime :
module m3_v2 ( logic a, b, clk1, clk2);
a13_v2: assert property (
@( posedge clk1) a |-> @( posedge clk2) nexttime b

);
endmodule
Figure 12.13 shows a waveform with solid arrows representing the temporal actions
of nexttime in the evaluation of a13_v2 . Note that all signals are the same as
in Fig. 12.12 except for clk2 , which no longer has a posedge at time 65. For
the evaluation attempt beginning at time 20, alignment with posedge clk2 does
not advance time. Advancing to the next tick carries the attempt to time 35,
where it fails. For the evaluation attempt beginning at time 60, alignment with
posedge clk2 carries the attempt to time 80. For the attempt beginning at time 80,
alignment with posedge clk2 does not advance time. For both of these attempts,
advancement to the next tick carries the attempt to time 95, where the result is pass.
Because posedge clk1 and posedge clk2 both occur at times 20 and 80, these
evaluation attempts behave the same as a14 .
The operator nexttime [0] specifies only alignment with its governing (i.e.,
incoming) clock. For any property p, nexttime [0] p is equivalent to 1'b1 |-> p.
This operator can be used, e.g., if p may have a leading clock different from the
incoming clock and it is desired to ensure that alignment with the incoming clock
occurs first. Examples of such usage are given in Sect. 17.1 .
Similar considerations apply when other LTL operators are used as synchroni-
zers: time advance specified by the LTL operator is always with respect to the clock
governing (i.e., incoming to) the LTL operator, and evaluation of the LTL operator
first specifies alignment to that clock in case its evaluation is not guaranteed to begin
at such a point. See Exercise 12.4 .