Question

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.

For example, in

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

w, x, z are clocked at c and y is clocked at d. Clock c flows across ##1, across the parenthesized subsequence (x ##1 @(d) y), and across |=>. Clock c also flows into the parenthesized subsequence, but it does not flow through @(d). Clock d does not flow out of its enclosing parentheses.

As another example, in

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

v, w, y, z are clocked at c and x is clocked at d. Clock c flows across |=>, distributes to both operands of the and (which is a property conjunction due to the multiple clocking), and flows into each of the parenthesized subexpressions. Within (w ##1 @(d) x), c flows across ##1 but does not flow through @(d). Clock d does not flow out of its enclosing parentheses. Within (y ##1 z), c flows across ##1.

Similarly, the scope of a clocking event flows into an instance of a named sequence or property, and, if the instance is a sequence, also flows left-to-right across the instance. However, a clocking event in the declaration of a sequence or property does not flow out of an instance of that sequence or property.

Note that juxtaposing two clocking events nullifies the first of them:

@(d) @(c) x

is equivalent to

@(c) x

because the flow of clock d is immediately overridden by clock c.