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

sequence s_req_ack( event ev);

1

@(ev) req ##1 ack;

2

endsequence

3

a_matched: assert property (

4

@( posedge dclk)

5

dvalid |->

6

s_req_ack( posedge rclk).matched

7

);

8

Fig. 12.14 Assertion using matched

10 20 30 40 50 60 70 80 90 100

rclk

req

ack

dclk

dvalid

Fig. 12.15 Waveform for assertion a_matched

Note that if s_req_ack( posedge rclk).matched were used in two or more
different clocking event scopes, then there are effectively as many different
.matched end points because their validity ends at different clocking events.

12.2.6 Declarations Within a Clocking Block

Sequences and properties may be declared within a clocking block. No explicit
clocking event control can be written in such a declaration. Instead, all instances of
the named sequence or property are understood to be singly clocked by the clocking
event of the clocking block. If a declaration of a sequence or property within a
clocking block itself instantiates a sequence or property, then that instance must be
singly clocked by a clock that is identical to the clock of the clocking block.
Concurrent assertions cannot be written within a clocking block. Therefore, to
instantiate a named sequence or property that is declared within a clocking block,
the clocking block must be named and the named sequence or property must be
referenced hierarchically.
Here is an example: