Hardware Reference
In-Depth Information
The computation of
P
using the partitioned form is:
P
.
u
;
v
;ns/ D9
i;cs
Œ˘
j
Œ
u
j
U
j
.i;
v
; cs/:˘
k
Œns
k
T
k
.i;
v
; cs/: .cs/:
Thus, the computation of
P
.
u
;
v
;ns/
can be seen as the computation of the image
of
.cs/
, under the transition relation
U.i;
v
;cs;
u
/:T .i;
v
;cs;ns/
represented in its
partitioned form:
fU
j
.i;
v
;cs/g; fT
k
.i;
v
;cs/g
. In general, we cannot hide variables
in the partitioned representation because, for this, we need to multiply out the
partitions. So, we keep the variables inside the partitions and do not quantify them.
However, by restricting to a specific
.cs/
it becomes affordable to compute the
product of the transitions relations and afterwards to quantify over
i
, therefore when
we come to a specific state subset,
P
, we multiply the partitions, because they are
restricted to the characteristic function of the subset,
.cs/
, and then we quantify
over the inputs
i
. In other words. we say that hiding (quantification) of variables
i
is performed as part of the image computation.
Let
C
j
.i;
v
;cs/
denote the condition that is true when the
j
-th output of
F
conforms to the
j
-th output of
S
:
C
j
.i;
v
;cs/ D ˘
k
ŒO
jk
.i;
v
;cs
F
/ ) O
jk
.i; cs
S
/;
where
cs D .cs
F
;cs
S
/
and the iteration is over all values
k
of the output
O
j
, e.g.,
for binary signals,
k 2f0; 1g
.
Let
C.i;
v
;cs/ D ˘
j
C
j
.i;
v
;cs/
, which is the overall condition when all outputs
of
F
conform to the outputs of
S
:
C.i;
v
;cs/ D ˘
j
˘
k
ŒO
jk
.i;
v
;cs
F
/ ) O
jk
.i; cs
S
/:
Next, we compute
Q
.
u
;
v
/
, the condition on
u
;
v
when the current subset of states
.cs/
leads to the non-conformance of outputs of
F
and
S
:
Q
.
u
;
v
/ D9
i;cs
ŒU.i;
v
;cs
F
;
u
/:C.i;
v
; cs/:.cs/:
Since these combinations of
.
u
;
v
/
can lead to a non-conforming state, we exclude
such transitions and map them all into a single non-accepting state
DCN
with a
universal self-loop. We remove these combinations from consideration by restricting
P
.
u
;
v
;ns/
to those
.
u
;
v
/
that are not contained in
Q
.
u
;
v
/
:
P
0
.
u
;
v
;ns/ D P
.
u
;
v
;ns/:Q
.
u
;
v
/:
Finally, the result is made complete by adding a state
DCA
(which is accepting in
the final answer after complementation), with transitions from
.cs/
into it for all
.
u
;
v
/
that are contained in
Q
.
u
;
v
/
.
Search WWH ::
Custom Search