Question

Multiply-clocked sequences are built by concatenating singly-clocked subsequences using the single-delay concatenation operator ##1. This operator is non-overlapping and synchronizes between the clocks of the two sequences. The single delay indicated by ##1 is understood to be from the endpoint of the first sequence, which occurs at a tick of the first clock, to the nearest strictly subsequent tick of the second clock, where the second sequence begins.

For example, consider

@(posedge clk0) sig0 ##1 @(posedge clk1) sig1

A match of this sequence starts with a match of sig0 at posedge clk0. Then ##1 moves the time to the nearest strictly subsequent posedge clk1, and the match of the sequence ends at that point with a match of sig1. If clk0 and clk1 are not identical, then the clocking event for the sequence changes after ##1. If clk0 and clk1 are identical, then the clocking event does not change after ##1 and the above sequence is equivalent to the singly-clocked sequence

@(posedge clk0) sig0 ##1 sig1

When concatenating differently-clocked sequences, the maximal singly-clocked subsequences are required to admit only non-empty matches. Thus, if s1, s2 are sequence expressions with no clocking events, then the multiply-clocked sequence

@(posedge clk1) s1 ##1 @(posedge clk2) s2

is legal only if neither s1 nor s2 can match the empty word. The clocking event posedge clk1 applies throughout the match of s1, while the clocking event posedge clk2 applies throughout the match of s2. Since the match of s1 is non-empty, there is an end point of this match at posedge clk1. The ##1 synchronizes between this end point and the first occurrence of posedge clk2 strictly after it. That occurrence of posedge clk2 is the start point of the match of s2.

The restriction that maximal singly-clocked subsequences not match the empty word ensures that any multiply-clocked sequence has well-defined starting and ending clocking events and well-defined clock changes. If clk1 and clk2 are not identical, then the following sequence

@(posedge clk0) sig0 ##1 @(posedge clk1) sig1[*0:1]

is illegal because of the possibility of an empty match of sig1[*0:1], which would make ambiguous whether the ending clocking event is posedge clk0 or posedge clk1.

Differently-clocked or multiply-clocked sequence operands cannot be combined with any sequence operators other than ##1. For example, if clk1 and clk2 are not identical, then the following are illegal:

@(posedge clk1) s1 ##0 @(posedge clk2) s2
@(posedge clk1) s1 ##2 @(posedge clk2) s2
@(posedge clk1) s1 intersect @(posedge clk2) s2