Lecture
8
Module
Decompositions
8.1
Decompositions of XORk,
k>2
The XOR module
introduced in Chapter 6 may be generalized to similar modules XORk ,
k>2. Cf. [EDIS], where XORk is referred to as
k-merge.
E.g., XOR3
= XOR3[a,b,c,z] = a;z;XOR3 [] b;z;XOR3 [] c;z;XOR3
Any module XORk, k>2, can be “decomposed into” (i.e., implemented by ) XOR modules.
E.g., XOR3.impl
|= XOR3, where
XOR3.impl = (XOR[a,b,y] || XOR[y,c,z])\{y}
To prove the
above statement, we may proceed as follows. Consider the LTSs
given below.
XOR.1
(0,a,1)
(0,b,1)
(1,y,0)
XOR.2
(0,y,1)
(0,c,1)
(1,z,0)
We now wish to
construct action sequences of XOR.1 || XOR.2, which are admitted by XOR3,
viewed as specification. Let ij denote the composite
state of XOR.1||XOR.2, where ‘i’ is the state of XOR.1,
and ‘j’ is the state of XOR.2.
We easily
construct the following sequences. Note that ‘y’ is viewed as an internal
signal.
00[a>10[y>01[z>00
00[b>10[y>01[z>00
00[c>01[z>00
Next, we
compare the above result with XOR3.aut, shown below.
XOR3.aut
des (0,2,4)
(0,a,1)
(0,b,1)
(0,c,1)
(1,z,0)
It follows
that XOR3 is isomorphic to a subsystem of XOR.1||XOR.2. Note however, that XOR.1||XOR.2
also contains sequences not covered by XOR3, e.g.,
00[a>10[y>01[b>11. On the other hand, we evidently have
(XOR.1 || XOR.2)\{y} || XOR3 ==
XOR3
i.e., Req1 is
satisfied.
As to the
verification of Req2 and Req3 see the following exercise.
Exercise
Ex8.1
(a) Convert the
above BLA definition of XOR3.impl into a proper LOTOS-file and then
convert this LOTOS-file into the corresponding aut-file.
Verify Req2 and Req3 by inspection of the resulting aut-file.
(b) Use CADP to
prove that XOR3.impl is indeed a realization (type C) of XOR3.
Follow the method described in Section 7.3.
Any module XORk for k>3 can similarly be decomposed into XORj modules, where j<k. See [EDIS] for details. CADP
may then be applied to verify such decompositions (type-C realizations).
8.2 Decompositions of CELk,
k>2
Recall our
recursive definition of CEL:
CEL = CEL[a,b,z] = *[a;b;z [] b;a;z] =
a;b;z;CEL [] b;a;z;CEL
A 3-input CEL
device is defined similarly:
CEL3 = CEL3[a,b,c,z] =
*[a;b;c;z [] a;c;b;z [] b;a;c;z [] b;c;a;z [] c;a;b;z [] c;b;a;z]
Note that a
more concise description of CEL3 may be obtained by using the sequential
composition operator >> (see Section 8.4). Namely:
CEL3 = (a;$
||| b;$ ||| c;$) >> z;CEL3
CEL3 may be implemented by CEL
modules (C-type realization), similar to the above implementation of XOR3:
CEL3impl[a,b,c,z] = (CEL[a,b,y]
|| CEL[y,c,z])\{y}
Exercise
Ex8.2
Apply CADP to
prove that CEL3impl is indeed a C-type realization of CEL3.
Follow the guidelines of Section 7.3.
8.3 Decompositions of TOGk,
k>2
The TOGGLE
element introduced in Chapter 6 can be generalized to TOGGLEk,
k>2, a device with one input a and k outputs z_1,… z_k. Its behaviour can be specified by
TOGGLEk
= *[a;z_1;a;z_2;…;a;z_k]
We also set TOGGLE
= TOGGLE2.
Methods of
implementing TOGGLEk are discussed in
[EDIS]. In particular, combinations of the following two methods are of
interest.
Method (1). If k=mxn, use one TOGGLEm, and
connect each output to a TOGGLEn.
Method (2) If TOGGLEm is
available, and k=m-1, we can obtain TOGGLEk
by applying the feedback connection shown in [EDIS].
We illustrate
a combination of the above two methods by showing a decomposition of TOGGLE3.impl.
Namely,
consider TOGGLE3[a,w,x,y].
Correspondingly we define:
TOGGLE3.impl [a,w,x,y] =
XOR[a,z,b] || (TOG[b,r,s] || (TOG[r,w,y] ||| TOG[s,x,z])\{r,s,b,z}
Exercise Ex8.3
Use CADP to
prove that TOGGLE3.impl is indeed a C-type realization of TOGGLE3 =
*[a;w;a;x;a;y] .
8.4
Further Decompositions
In this
section we introduce a method of decomposing a given circuit specification into
a composition of both XOR and CEL components.
8.4.1 Circuit Behaviour
Descriptions
Let us
consider circuit behaviour specifications based on
the BLA operators ‘[ ]’ and ‘||’. Let OPj denote
either of the two operators, and consider the following Blot circuit behaviour specification:
cct.spec
= *(((a;$ OP1 b;$) OP2 (c;$ OP3 d;$)) >> z;$)
8.4.2 Realization
We claim that the
above circuit specification may be realized by the following modular circuit (BLA representation):
cct.impl = (MO1[a,b,y1] ||| MO3[c,d,y2]) || MO2[y1,y2,z]\{y1,y2}
Here, MOj = XOR if OPj
= [ ], and MOj = CEL, if OPj = ||.
The prove of this general statement is beyond the scope of this text
and is suggested as an interesting research problem. Here, we apply our
verification method to particular instances of the above general statement.
8.5
The CXC-circuit Example
We now
illustrate the above general statement by the particular example where OP1=OP3=
|| and OP2= [ ]. Below is the corresponding spec-file CXC_spec.lotos.
File CXC_spec.lotos
specification CXC_spec[A,B,C,D,Z]:noexit
behaviour
CXC_spec[A,B,C,D,Z]
where
process CXC_spec[A,B,C,D,Z]:noexit:=
(A;exit ||| B;exit)
[] (C;exit ||| D;exit)
>> Z;exit >>
CXC_spec[A,B,C,D,Z]
endproc
endspec
And here is
the LOTOS file CXC.lotos representing the
corresponding realization.
File CXC.lotos
specification CXC[A,B,C,D,Z]:noexit behaviour
hide Y1,Y2 in
(
(CEL[A,B,Y1] ||| CEL[C,D,Y2])
|[Y1,Y2]|
XOR[Y1,Y2,Z]
)
where
process CEL[A,B,Z]:noexit:=
{copy}
endproc
process XOR[A,B,Z]:noexit:=
{copy}
endproc
endspec
8.6
Verification
Exercise
Ex8.4
Use the method
of Section 7.3 to show that Req1 and Req2 of the claim CXC.lotos
|= CXC_spec.lotos are satisfied.
Verify Req3 by
inspecting the CXC.omin file obtained from CXC.aut by issuing the command:
aldebaran -omin CXC.aut > CXC.omin
8.7
Further
Visit [EDIS]
to learn about additional modules and their decompositions.
8.8
References
[EDIS] http://edis.win.tue.nl/sys