Question

As in the case of singly-clocked properties, the result of evaluating a multiply-clocked property is either true or false. Multiply-clocked properties can be formed in a number of ways.

Multiply-clocked sequences are themselves multiply-clocked properties. For example,

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

is a multiply-clocked property. If a multiply-clocked sequence is evaluated as a property starting at some point, the evaluation returns true if and only if there is a match of the multiply-clocked sequence beginning at that point.

The boolean property operators (not, and, or) can be used freely to combine singly- and multiply-clocked properties. The meanings of the boolean property operators are the usual ones, just as in the case of singlyclocked properties. For example,

(@(posedge clk0) sig0) and (@(posedge clk1) sig1)

is a multiply-clocked property, but it is not a multiply-clocked sequence. This property evaluates to true at a point if and only if the two sequences

@(posedge clk0) sig0

and

@(posedge clk1) sig1

both have matches beginning at the point.

The non-overlapping implication operator |=> can be used freely to create a multiply-clocked property from an antecedent sequence and a consequent property that are differently- or multiply-clocked. The meaning of multiply-clocked non-overlapping implication is similar to that of singly-clocked non-overlapping implication. For example, if s0, s1 are sequences with no clocking event, then in

@(posedge clk0) s0 |=> @(posedge clk1) s1

|=> synchronizes between posedge clk0 and posedge clk1. Starting at the point at which the implication is being evaluated, for each match of s0 clocked by clk0, time is advanced from the end point of the match to the nearest strictly future occurrence of posedge clk1, and from that point there must exist a match of s1 clocked by clk1.

The non-overlapping implication operator |=> can synchronize between the ending clock event of its antecedent and several leading clock events for subproperties of its consequent. For example, in

@(posedge clk0) s0 |=> (@(posedge clk1) s1) and (@(posedge clk2) s2)

|=> synchronizes between posedge clk0 and both posedge clk1 and posedge clk2.

Since synchronization between distinct clocks always requires strict advance of time, the two property building operators that require special care with multiple clocks are the overlapping implication |-> and if/if...else.

Since |-> overlaps the end of its antecedent with the beginning of its consequent, the clock for the end of the antecedent must be the same as the clock for the beginning of the consequent. For example, if clk0 and clk1 are not identical and s0, s1, s2 are sequences with no clocking events, then

@(posedge clk0) s0 |-> @(posedge clk1) s1 ##1 @(posedge clk2) s2

is illegal, but

@(posedge clk0) s0 |-> @(posedge clk0) s1 ##1 @(posedge clk2) s2

is legal.

The if/if...else operators overlap the test of the boolean condition with the beginning of the if clause property and, if present, the else clause property. Therefore, whenever using if or if...else, the if and else clause properties must begin on the same clock as the test of the boolean condition. For example, if clk0 and clk1 are not identical and s0, s1, s2 are sequences with no clocking events, then

@(posedge clk0) if (b) @(posedge clk0) s1

is legal, but

@(posedge clk0) if (b) @(posedge clk0) s1 else @(posedge clk1) s2

is illegal because the else clause property begins on a different clock than the if condition.