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.8          References

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