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

tick of posedge clk2 at time 65, where the sampled value of b is 1'b1 , and so these
attempts succeed. The attempt beginning at time 80 finds the nearest strictly future
tick of posedge clk2 at time 95, where the sampled value of b is again 1'b1 , and
so it succeeds. As before, the fact that posedge clk2 occurs at time 80 is irrelevant
because the operator |=> has been used.
The overlapping suffix implication |-> can also be used as a synchronizer
between different clocks. Suppose that the following assertion is added to the
module in Fig. 12.8 :
a6: assert property (
@( posedge clk1) a |-> @( posedge clk2) b
);
If a match of the antecedent of |-> ends at time t 0 , then the consequent will be
checked at the nearest time greater than or equal to t 0 in which posedge clk2
occurs. Comparing with the waveform in Fig. 12.9 ,theattemptof a6 beginning at
time 20 succeeds because posedge clk2 occurs at time 20 and the sampled value
of b at that time is 1'b1 . The attempts of a6 beginning at times 40 and 60 behave
the same as the corresponding attempts of a5 . Finally, the attempt of a6 beginning
at time 80 fails because there is a tick of posedge clk2 at this time and the sampled
value of b is 1'b0 .
The operators ##1 and ##0 can be used as synchronizers between different clocks
in sequences. The timing associated with ##1 as a synchronizer is the same as that
of |=> . Here is an example:
sequence s1;
@( posedge clk1) a[ * 2] ##1 @( posedge clk2) b;
endsequence
Referring again to Fig. 12.9 , s1 matches over the intervals from times 20 to 65, 40
to 65, and 60 to 95. The following variant replaces ##1 with ##0 :
sequence s2;
@( posedge clk1) a[ * 2] ##0 @( posedge clk2) b;
endsequence
The timing associated with ##0 as a synchronizer is the same as that of |-> .
Therefore, the intervals in Fig. 12.9 over which s2 matches are from times 20 to 65
and 40 to 65. There is no match of s2 beginning at time 60 because the subsequence
a[ * 2] matches ending at time 80 and there is an tick of posedge clk2 at this time
with the sampled value of b equal to 1'b0 .
##1 and ##0 are the only sequence operators that can be used as synchronizers
between different clocks. For all other sequence operators, the operands must be
singly clocked sequences clocked by the same clocking event. Here is an example
of an illegal sequence declaration:
sequence s3_illegal;
@( posedge clk) a[ * 2] within @( negedge clk) b[->1];
endsequence
This sequence is illegal because the operands of within are clocked by different
clocking events.