Sequences specify temporal relationships between signals. However, to describe some complex behaviors, it is also necessary to be able to save values explicitly at some point in a sequence so it can be referenced later in the sequence. Consider a sequence such as �when data goes into a pipeline, it will come out between 3 and 5 clocks later, and will be incremented by one.�

The valid signal marks when data goes into the pipeline, and 3 to 5 clocks later, the output of the pipeline, dout, will be equal to the input data incremented by one. Capturing the sequence-specific data directly in the sequence eliminates the need for the user to write a separate state machine or other auxiliary code to capture the data, and eliminates the need of having to correlate this auxiliary code to each execution attempt of the sequence. It also avoids the problem of having to tell other tools that the auxiliary code is not really part of the design, thus simplifying the tool usage flow as well.

In many cases, sequences by themselves are sufficiently expressive to cover explicit behaviors. However, the property layer allows for more general behaviors to be specified. In particular, properties allow you to invert the sense of a sequence (i.e. the sequence should not happen), disable the sequence evaluation, or specify that a sequence be implied by some other occurrence. The property construct allows these capabilities using the following syntax:

A property definition is identified by the property-endproperty keyword pair, as one would expect, and supports formal arguments and argument passing exactly as sequence definitions do. Consider:

@(posedge clk) init_seq |=> abort_seq;

where |=> is the no overlapping implication operator. This property expression states that each successful completion of the init_seq antecedent sequence implies that an abort_seq consequent sequence will occur on the next clock. For clock cycles in which the antecedent does not occur, the consequent is not evaluated and the property is considered vacuously true.

Multiple clock sequences and properties can be specified using the following syntax.

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.

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

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.

Throughout this subsection, c, d denote clocking event expressions and v, w, x, y, z denote sequences with no clocking events. Clock flow allows the scope of a clocking event to extend in a natural way through various parts of multiplyclocked sequences and properties and reduces the number of places at which the same clocking event must be specified. Intuitively, clock flow provides that in a multiply-clocked sequence or property the scope of a clocking event flows left-to-right across linear operators (e.g., repetition, concatenation, negation, implication) and distributes to the operands of branching operators (e.g., conjunction, disjunction, intersection, if...else) until it is replaced by a new clocking event.

For example,

@(c) x |=> @(c) y ##1 @(d) z

can be written more simply as

@(c) x |=> y ##1 @(d) z

because clock c is understood to flow across |=>.

Clock flow eliminates the need to write clocking events in positions where the clock is not allowed to change. For example,

@(c) x |-> @(c) y ##1 @(d) z

can be written as

@(c) x |-> y ##1 @(d) z

to reinforce the restriction that the clock not change across |->. Similarly,

@(c) if (b) @(c) w ##1 @(d) x else @(c) y ##1 @(d) z

can be written as

@(c) if (b) w ##1 @(d) x else y ##1 @(d) z

to reinforce the restriction that the clock not change from the boolean condition b to the beginnings of the if and else clause properties. Clock flow also makes the adjointness relationships between concatenation and implication clean for multiplyclocked properties:

@(c) x ##1 y |=> @(d) z

is equivalent to

@(c) x |=> y |=> @(d) z

and

@(c) x ##0 y |=> @(d) z

is equivalent to

@(c) x |-> y |=> @(d) z

The scope of a clocking event flows into parenthesized subexpressions and, if the subexpression is a sequence, also flows left-to-right across the parenthesized subexpression. However, the scope of a clocking event does not flow out of enclosing parentheses.