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

module m6 ( logic a, b, event ev1, ev2);
a15: assert property ((@(ev1) a) |=> (@(ev2) b));
a18: assert property (@(ev1) a |=> b);
endmodule
module m7;
logic A,B;
event EV;
...
m6 m6_inst(.a(A), .b(B), .ev1(EV), .ev2(EV));
endmodule
The instance of m6 within m7 connects the same event EV to both of the ports ev1
and ev2 . Therefore, ev1 and ev2 are equivalent in this instance, and so a15 and a18
behave identically.

12.2.5.4 Sequence Methods

SystemVerilog provides two methods for detecting the endpoint of match of an
instance of a named sequence: triggered and matched . triggered is discussed
in detail in Sect. 11.2 . Both of these methods may be used in multiply clocked
sequences and properties, but their behaviors are very different.
Whenever triggered is used in a Boolean expression of a sequence, the clock
governing that Boolean expression must be the same as the ending clock of the
sequence instance to which triggered is applied. This restriction was illustrated in
Example 12.2 from Sect. 12.1.2 .
matched can, and should, be used when the ending clock of the instance to
which it is applied is different than the clock governing the Boolean expression
in which matched appears. matched serves as a synchronizer between these two
clocks. Upon completion of a match of the underlying instance, this fact is stored
until the earliest strictly subsequent time step in which there is a tick of the clock
governing the context in which matched appears. In that time step, the value of the
application of matched to the instance is true.
As an example, suppose that we need to check that if dvalid is true at an
occurrence of posedge dclk , then the sequence req ##1 ack must have already
completed a match clocked at posedge rclk , but the match must not have
completed before the nearest strictly prior occurrence of posedge dclk , if such
an occurrence exists. It does not matter when the match starts. This can be encoded
using matched as shown in Fig. 12.14 . Line 7 illustrates the syntax for applying
method matched to an instance of a sequence.
Figure 12.15 shows a waveform for a_matched . There are two matches of the
instance s_req_ack( posedge rclk) . The first is from times 20 to 40 and causes
Line 7 to be true at time 55. The second is from times 60 to 80 and causes Line 7 to
be true at time 105. As a result, the evaluation of a_matched that starts at time 55
succeeds. However, the evaluation of a_matched that starts at time 80 fails. The
match of s_req_ack( posedge rclk) completing at time 80 is too late because it is
not strictly before time 80. The other evaluations of a_matched succeed vacuously.