**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 ****Reading**

Visit [EDIS]
to learn about additional modules and their decompositions.

**8.8
****References**

[EDIS] http://edis.win.tue.nl/sys

** **