Hardware Reference
In-Depth Information
Never use antecedents admitting an empty match in suffix implication.
Note also that in case of antecedents admitting an empty match, the transfor-
mation described in Example
6.18
is not valid. For example,
s[
*
0] ##1 1 |-> p
(i.e.,
1 |=> p
)is
p
,but
s[
*
0] |->
nexttime
p
is a tautology.
6.9
Sequence Concatenation and Delay Revisited
In Sect.
6.3
, we introduced sequence concatenation operators with factors
n
0.
The rules of building sequence concatenation may be summarized as follows:
r ##0 s
is a sequence fusion.
r ##1 s
is a sequence concatenation.
r##ns
, where
n
>1is defined in terms of repetition:
r##ns
r ##1 1[
*
n-1] ##1 s
.
We also defined there initial delay operators with factors
n
>0. Now we can
provide a definition for any factor
n
0:
##n s
1[
*
n] ##1 s
.
According to this definition
##0 s
is equivalent to
s
(why? see Sect.
6.5.1.1
), which
is intuitive, as
##0 s
means “wait 0 clock ticks before the sequence beginning”.
In a fashion similar to consecutive repetition ranges (Sect.
6.7.1
), it is possible to
specify
delay ranges
, finite or infinite, between two sequences, as follows:
r ##[0:0] s
r ##0 s
.
r ##[m:n] s
(r ##1 1[
*
m-1:n-1] ##1 s)
, where
n
m
>0.
r ##[0:n] s
(r ##0 s)
or
(r ##[1:n] s)
, where
n
>0.
r ##[m:$] s
(r ##1 1[
*
m-1:$] ##1 s)
, where
m
>0.
r ##[0:$] s
(r ##0 s)
or
(r ##[1:$] s)
, where
n
>0.
Informally speaking
r ##[m:n] s
means that there are
m
to
n
clock ticks from
the tight satisfaction point of
r
to the initial point of
s
.
r ##[m:$] s
means that
there are
m
or more clock ticks from the tight satisfaction point of
r
to the initial
point of
s
. As in the case with consecutive repetition there is a shortcut
r ##[
*
]s
for
r ##[0:$] s
(“zero or more clock ticks”), and
r ##[+] s
for
r ##[1:$] s
(“one or more clock ticks”).
It is also possible to define
initial delay ranges
:
##[m:n] s
1 ##[m:n] s
, where
n
m
0.
##[m:$] s
1 ##[m:$] s
, where
m
0.
Search WWH ::
Custom Search