Digital Signal Processing Reference
In-Depth Information
=
{
S1
(
)
→
S2
(
)
|
≤
≤
∧
=
−
}
M
w
r
0
w
N
r
N
w
and we have
T
=
{
S1
(
w
1
)
→
S1
(
w
2
)
|∃
r
1
,
r
2
:
(
S1
(
w
1
)
→
S2
(
r
1
))
,
(
S1
(
w
2
)
→
S2
(
r
2
))
∈
M
∧
w
1
>
w
2
∧
r
1
<
r
2
}
=
{
S1
(
w
1
)
→
S1
(
w
2
)
|
0
≤
w
1
,
w
2
≤
N
∧
w
1
>
w
2
∧
N
−
w
1
<
N
−
w
2
}
=
{
S1
(
w
1
)
→
S1
(
w
2
)
|
0
≤
w
2
<
w
1
≤
N
}.
For
N
0, this relation is clearly non-empty. We conclude that we are dealing with
a reordering channel. See Example
21
for a variation on this example where we find
aFIFO.
In
iscc
, this test can be performed as follows.
>
M := [N] -> { S1[w] -> S2[N - w] : 0 <= w <= N };
T := (M . (ran M << ran M) . Mˆ-1)
*
(dom M >> dom M);
T;
sample T;
That is, we construct a relation that maps reads (
ran M
) to later reads, map both
of these reads to the corresponding writes and intersect the result with a relation
that maps writes to earlier writes. At the end, we perform the
sample
operation to
obtain an element of the set
T
, thereby verifying that it is non-empty. The result is
[N] -> { S1[w] -> S1[w'] : w >= 0 and w <= N and
w' <= -1 + w and w' <= N and w' >= 0 }
[N] -> { S1[1] -> S1[0] : N = 1 }
6.2
Multiplicity
The standard dataflow analysis from Sect.
5.1
may result in communication channels
that are read more often than they are written to when the same value is used in
multiple iterations of the reading process. Such channels require special treatment
and this multiplicity condition should therefore be detected by checking whether
there is any write iteration
w
that is mapped to multiple read iterations through the
mapping
M
. In particular, let
T
be the relation
T
=
{
w
1
→
w
2
|∃
r
1
,
r
2
:
(
w
1
→
r
1
)
,
(
w
2
→
r
2
)
∈
M
∧
w
1
=
w
2
∧
r
1
≺
r
2
}.
This relation contains all pairs of identical write iterations that correspond to a pair
of distinct read iterations. If this relation is non-empty, then multiplicity occurs. As
in the previous section, we can check the emptiness using Operation
2
(Emptiness
Check).
