**@(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 support

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

**
**1. Multiply-clocked sequences

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.

**
**2. Multiply-clocked
properties

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.

**
**3.Clock flow

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.