On the Formal Derivation of a FEAL Microprocessor

R. Rukšėnas^{∗}  K. Sere^{†}  Y. Zhao^{∗}

Abstract We present an outline of a method for formal derivation of asynchronous VLSI circuits. The proposed method focuses on transformational style of the design and it uses techniques familiar from the construction of parallel programs. Refinement calculus and action systems are used as a framework for the design process. As a case study we look at the derivation of an asynchronous encryption/decryption microprocessor.

1 Introduction

The paper describes ongoing work on exploring a methodology for formal derivation of asynchronous delay-insensitive VLSI circuits within the refinement calculus and the action system framework. It is aimed to be used in the design of application-specific circuits. The basic idea is to apply techniques familiar from the construction of parallel programs to VLSI design. This approach was originally taken by Martin [9] who has developed a methodology for designing asynchronous VLSI circuits as concurrent programs within the CSP-framework. Using his method he has specified and derived a number of nontrivial circuits. Delay-insensitive, asynchronous chips were then produced from the concurrent programs that can be seen as equivalent to the parallel composition of action systems that we derive here. However, the method of Martin is semiformal and the transformations carried out during the design process are not formally proved to be correct. We want to provide a completely formal basis for Martin’s method.

An action system is a parallel or distributed program where parallel activity is described in terms of events, so called actions. Several actions can be executed in parallel, as long as the actions do not share any variables. A recent extension of the action system framework, adding procedure declarations to action systems [5], gives us a very general mechanism for communication between action systems. The action systems formalism was proposed by Back and Kurki-Suonio [3].

The refinement calculus is a formalization of the stepwise refinement method of program construction. It was originally proposed by Back [1] and it has been later studied and extended by several researchers, see [11, 12] among others.

∗Åbo Akademi University, Department of Computer Science, FIN-20520 Turku, Finland, emails: {rruksena,zyi}@aton.abo.fi

†University of Kuopio, Department of Computer Science and Applied Mathematics, FIN-70211 Kuopio, Finland, email: Kaisa.Sere@uku.fi, fax: +358-71-162595

Originally, the refinement calculus was designed as a framework for systematic derivation of sequential programs only. Back and Sere [4, 13] extended the refinement calculus for the design of action systems and hence, it was possible to handle parallel algorithms within the calculus. Back [2] made yet another extension to the calculus showing how reactive programs could be derived in a stepwise manner within it relying heavily on the work done in data refinement.

Action systems and the refinement calculus approach has already proved to be suitable for VLSI circuit specification and design on logical behaviour level [6]. Now we want to explore its applicability in the design on rather low (signal) level.

The refinement calculus has been also formalised within a mechanical theorem prover by Back and von Wright [7]. This gives us the tool to mechanise the design process and prove correctness of the derived circuit. A somewhat related method and formalism is developed in [14], but the emphasis is put on the verification of and formal models for delay-insensitive circuits.

As a case study we look at the design of an asynchronous FEAL (Fast Encipherment Algorithm) processor [10]. We start from the sequential algorithm which describes logical behaviour of the encryption processor. Our goal is to identify and isolate the basic functional components of the circuit into action systems of their own. The component action systems are joint together in a parallel composition, where they interact with each other using remote procedure calls. Synchronous communication between different componnets of the circuit is achieved through the procedures mechanism [6].

Overview of the paper In section 2, we briefly describe the action systems formalism. In section 3, we describe how action systems are composed into parallel systems. We also briefly mention the refinement calculus. In section 4, we describe the the target processor and give an initial specification for it as a sequential program. In section 5, this specification is stepwise turned into a parallel composition of action systems, where each action system represents one basic functional component of the circuit. In section 6, we introduce real parallelism into our system by creating 3-level pipeline. Finally in section 7, we conclude with some remarks on the proposed method and further steps in the derivation process.

2 Action systems

An action system (with procedures) is a statement of the form

A :: var v; proc w •

|[ var x_{1}, …, x_{h} := x_{1}0, …, x_{h}0; proc p_{1} = P_{1}; …; p_{n} = P_{n};

do A_{1} [] … [] A_{m} od
]|: z

The identifiers x_{1}, …, x_{h} are the variables declared in A and initialized to x_{1}0, …, x_{h}0, p_{1}, …, p_{n} are the procedure headers, and P_{i} is the procedure body of p_{i}, i = 1, …, n. Within the loop, A_{1}, …, A_{m} are the actions of A. Finally, z, v and w are pairwise distinct lists of identifiers. The list z is the import list, indicating which variables and procedures are referenced, but not declared in A. The lists v and w are the export lists, indicating which variables and procedures declared in A are accessible from other action systems. Procedure bodies and actions can be arbitrary statements, and may contain procedure calls.

The guard of a program statement S is the condition gS, defined by

gS = ¬wp(S, false)

where wp is the weakest precondition predicate transformer of Dijkstra [8]. Both procedure bodies and actions will in general be guarded commands, i.e., statements of the form

C = g → S,

where g is a boolean condition and S is a program statement. In this case, the guard of C is g ∧ ¬wp(S, false).

Enabledness of an action Let p = (b → T ) be a procedure and let a → S; p be an action that calls on p. Then the enabledness of this action is determined by the value of the action guard

g(a → S; p) = a ∧ g(S; p)

If a procedure or action contains a call to a procedure that is not declared in the action system, then the behavior of the action system will depend on the way in which the procedures are declared in some other action system, which constitutes the environment of the action system as will be described below.

3 Composing and refining action systems

Consider two action systems,

A :: var v; proc r •

|[ var x := x0; proc p_{1} = P_{1}; …; p_{n} = P_{n};

do A_{1} [] … [] A_{m} od
]|: z

and

B :: var w; proc s •

|[ var y := y0; proc q_{1} = Q_{1}; …; q_{l} = Q_{l};

do B_{1} [] … [] B_{k} od
]|: u

where x ∩ y = ∅, v ∩ w = ∅, and r ∩ s = ∅. Furthermore, the local procedures declared in the two action systems are required to be distinct.

We define the parallel composition A ∥ B of A and B to be the action system C C :: var b; proc c •

|[ var x, y := x0, y0;

proc p_{1} = P_{1}; …; p_{n} = P_{n}; q_{1} = Q_{1}; …; q_{l} = Q_{l};
do A_{1} [] … [] A_{m} [] B_{1} [] … [] B_{k} od
]|: a

where a = z ∪ u − (v ∪ r ∪ w ∪ s), b = v ∪ w, c = r ∪ s.

Thus, parallel composition will combine the state spaces of the two constituent action systems, merging the global variables and global procedures and keeping the local variables distinct. The imported identifiers denote those global variables and/or procedures that are not declared in either A or B. The exported identifiers are the variables and/or procedures declared global in A or B. The procedure declarations and the actions in the parallel composition consists of the procedure declarations and and actions in the original systems.

Enabledness We permit procedure bodies to have guards that are not identically true. Hence, it is possible that an action which is enabled, calls a procedure in another action system, which then turns out not to be enabled in the state in which it is called. This situation is then the same as if the calling action had not been enabled at all, and had therefore never initiated the call. In other words, the enabledness of an action is determined by the enabledness of the whole statement that is invoked when the action is executed, including enabledness of all procedures that might be invoked.

Decomposing action systems Given an action system

C :: var u; proc s • |[ var v := v0;

do C_{1} [] … [] C_{n} od
]|: z

we can decompose it into smaller action systems by parallel composition. This means that we split the variables, actions and procedures of C into disjoint sets so that

C = var u; proc s •

|[ var w := w0; proc r = R;

A ∥ B ]|: z

where

A :: var a_{2}; proc a_{3} •

|[ var x := x0; proc p = P; do A_{1} [] … [] A_{m} od

]|: a_{1}

B :: var b_{2}; proc b_{3} •

|[ var y := y0; proc q = Q; do B_{1} [] … [] B_{k} od

]|: b_{1} The reactive components A and B interact with each other via the global variables and procedures included in the lists a_{2}, a_{3}, b_{2}, b_{3}.

Hiding and revealing Let

var v_{1}, v_{2}; proc v_{3}, v_{4} • A : z

be an action system of the form above, where z denotes the import list and v_{1}, v_{2}, v_{3}, v_{4} denote the export lists. We can hide some of the exported global variables (v_{2}) and procedure names (v_{4}) by removing them from the export list,

A′ = var v_{1}; proc v_{3} • A : z.

Hiding the variables v_{2} and procedure names v_{4} makes them inaccessible from other actions outside A′ in a parallel composition. Hiding thus has an effect only on the variables and procedures in the export list. The opposite operation, revealing, is also useful.

In connection with the parallel composition below we will follow the following convention. Let var a_{1}; proc a_{2} • A : a_{3} and var b_{1}; proc b_{2} • B : b_{3} be two action systems. Then their parallel composition is the action system

var a_{1} ∪ b_{1}; proc a_{2} ∪ b_{2} • A ∥ B : c

where c = a_{3} ∪ b_{3} − (a_{1} ∪ a_{2} ∪ b_{1} ∪ b_{2}) according to the definition above. Hence, the parallel composition exports all the variables and procedures exported by either A or B. Sometimes there is no need to export all these identifiers, i.e., when they are exclusively accessed by the two component action systems A and B. This effect is achieved with the following construct that turns out to be extremely useful later:

var v; proc p • |[ A ∥ B ]| : c

Here the identifiers v and p are as follows: v ⊆ a_{1} ∪ b_{1} and p ⊆ a_{2} ∪ b_{2}.

Refining action systems Most of the steps we will carry out within the microprocessor derivation are purely syntactic decomposition steps. There are, however, a couple of steps where a higher level action system is refined into an other action system. These steps are formally carried out within the refinement calculus, where we consider action systems as ordinary statements, i.e., as initialized iteration statements.

The refinement calculus is based on the following definition. Let S and S′ be two statements. Then S is correctly refined by S′, denoted S ≤ S′, if for any postcondition Q

wp(S, Q) ⇒ wp(S′, Q).

4 FEAL algorithm and initial specification of the processor

Algorithm As a case study we look at the design of an asynchronous encryption/decryption (FEAL) processor that implements a special case of the so called FEAL-N algorithm [10]. The algorithm takes plaintext (64-bit word) as an input and produces encrypted text of the same length. While encrypting it uses 16-bit keys that are computed from the original one given by the user. We here assume that there are available (when needed) N + 8 keys in the so called key memory.

Encryption of input word T is given by the following set of equations:

L_{0}.R_{−1} = K_{N ..N +3} ⊕ T  (1)
R_{0} = R_{−1} ⊕ L_{0}  (2)
for i ∈ 1..N :
R_{i} = L_{i−1} ⊕ F (R_{i−1}, K_{i−1})  (3)
L_{i} = R_{i−1}  (4)
L_{N +1} = R_{N} ⊕ L_{N}  (5)
C = K_{N +4..N +7} ⊕ R_{N} .L_{N +1}  (6)

Here C stands for the output (encrypted text). A concatenation of two words W_{1} and W_{2} is writen as W_{1}.W_{2}, while exclusive-or (for W_{1}, W_{2} of the equal length) is denoted as W_{1} ⊕ W_{2}. The word under encryption is then represented as a concatenation L.R of the left and right part (both 32-bit long). Furthermore, let K_{m..n} be short for K_{m}.K_{m+1}...K_{n} with K_{j} being j -th key. We assume that function F is available and do not consider its implementation. Decryption algorithm has the same structure only the keys are used in different order.

The parameter N is the number of rounds in the main encryption loop (Equations 3, 4). We consider the case with N = 8. Some extra processing of the word is done before the loop (Equations 1, 2) and after (Equations 5, 6) it. So the algorithm consists of three logical parts.

Structure of the microprocessor We make the design decision to implement each logical part of the algorithm by a separate functional component in the target microprocessor. When processing one word the components are activated one after the other without any possibility for simultaneous activity. However, the processor is supposed to work with a sequence of words. In this case concurrent activity of all its parts is possible. The solution is to have a 3-level pipeline system. To keep input of the second and third components unchanged until the processing of data has been completed and result passed to the next component we introduce two registers (see Figure 1). All components of the circuit communicates through the indicated channels.

[figure: K8 11; K12 15; K0 7; T; Li; Li; Lo; Lo; Ri; Ro; Ro; Ri; E; C; O; Y; E; K; M; M; Y; R; REG1; DATAIN; K; CALC; REG2; DATAOUT]

Figure 1: Structure of the microprocessor

We start from the sequential action system that implements above algorithm in the procedure FEAL:

F0:: proc FEAL • |[ var L_{i},R_{i} , R_{o},L_{o} , T ; proc FEAL(t)= (T :=t; |[var R\underline{i},L\underline{o},L[j],R[j] for j=0 ,…,8 ; L_{i}.R\underline{i}:= K8..11 ⊕T ; R_{i}:= L_{i}⊕R\underline{i} ; L[0 ],R[0]:= L_{i},R_{i} ; [ L[j],R[j]:= R[j-1] , L[j − 1 ]⊕F (R[j-1],K0..7[16j-15..16j]) ]

for j=0 ,…,8 ; R_{o},L_{o} :=R[8] , L[8 ] ; L\underline{o}:= R_{o}⊕L_{o} ; C := K12..15 ⊕R_{o}.L\underline{o} ]| )

]|:C , K

In our target program each component of the processor is represented as an action system of its own. Parallel composition of them models the entire system where all elements can be active at the same time. Communication on the channels (synchronization of the action systems) is expressed as a remote procedure calls. We do not consider a derivation of any particular component of the processor here, instead we look more carefully at the task of isolating the basic functional parts and modelling communication through the channels on the low (signal) level.

5 Decomposition into parallel action systems

As described above, the algorithm consists of three parts. We therefore start by making three procedures to represent them:

F1:: proc FEAL • |[ var L_{i},R_{i} , R_{o},L_{o} , T ; proc INXOR(var l_{i},r_{i})=(|[ var R\underline{i} ; l_{i}.R\underline{i}:= K8..11 ⊕T ; r_{i}:= l_{i}⊕R\underline{i} ]|) ; proc CIPHER(l_{i},r_{i},var r_{o},l_{o})=

(|[var L[j],R[j] for j=0 ,…,8 ; L[0 ],R[0]:= l_{i},r_{i} ; [ L[j],R[j]:= R[j-1] , L[j − 1 ]⊕F (R[j-1],K0..7[16j-15..16j]) ]

for j=0 ,…,8 ; r_{o} , l_{o} :=R[8] , L[8 ] ]| ) ;

proc OUTXOR(r_{o} , l_{o})=(|[ var L\underline{o} ; L\underline{o}:= r_{o}⊕l_{o} ; C := K12..15 ⊕r_{o}.L\underline{o} ]|) ; proc FEAL(t)=

(T := t ; INXOR(L_{i},R_{i}); CIPHER(L_{i},R_{i},R_{o},L_{o}); OUTXOR(R_{o},L_{o})) ]|:C , K We have that F0 ≤ F1.

Now the encryption itself is done in procedure CIPHER, while INXOR performs preparatory processing of the word and OUTXOR ends whole process.

Parallelize F There is no parallel activity possible in the above action system. Hence, we proceed by creating a parallel composition of action systems which contains actions that can be executed simultaneously.

First we split the procedure FEAL into three parts by creating new procedures DIN , CALC and DOUT . DIN isolates procedure INXOR from the rest while CALC and DOUT separate procedures CIPHER and OUTXOR. More formally this can be represented as the following sequence of refinements:

(T := t ; INXOR(L_{i} ,R_{i}); CIPHER(L_{i},R_{i},R_{o},L_{o}); OUTXOR(R_{o},L_{o})) ≤ proc DIN (l_{i},r_{i})=(INXOR(l_{i},r_{i}) ; CIPHER(L_{i},R_{i},R_{o},L_{o}); OUTXOR(R_{o},L_{o})) ; (T := t ; DIN (L_{i},R_{i})) ≤ proc DIN (l_{i},r_{i})=(INXOR (l_{i},r_{i}) ; CALC (l_{i},r_{i})) ; proc CALC (l_{i},r_{i})=(CIPHER(l_{i},r_{i},R_{o},L_{o}) ; OUTXOR(R_{o},L_{o})) ; (T := t ; DIN (L_{i},R_{i})) ≤ proc DIN (l_{i},r_{i})=(INXOR(l_{i},r_{i}) ; CALC (l_{i},r_{i})) ; proc CALC (l_{i},r_{i})=(CIPHER(l_{i},r_{i},R_{o},L_{o}) ; DOUT (R_{o},L_{o})) ; proc DOUT (r_{o} , l_{o})=(OUTXOR(r_{o} , l_{o})) ; (T := t ; DIN (L_{i},R_{i}))

Now a new action system is as below:

F2:: proc FEAL • |[ var L_{i},R_{i} , R_{o},L_{o} , T ; proc INXOR(var l_{i},r_{i})=(|[ var R\underline{i} ; l_{i}.R\underline{i}:= K8..11 ⊕T ; r_{i}:= l_{i}⊕R\underline{i} ]|) ; proc CIPHER(l_{i},r_{i},var r_{o},l_{o})=

(|[var L[j],R[j] for j=0 ,…,8 ; L[0 ],R[0]:= l_{i},r_{i} ; [ L[j],R[j]:= R[j-1] , L[j − 1 ]⊕F (R[j-1],K0..7[16j-15..16j]) ]

for j=0 ,…,8 ; r_{o} , l_{o} :=R[8] , L[8 ] ]| ) ;

proc OUTXOR(r_{o} , l_{o})=(|[ var L\underline{o} ; L\underline{o}:= r_{o}⊕l_{o} ; C := K12..15 ⊕r_{o}.L\underline{o} ]|) ; proc DIN (l_{i},r_{i})=(INXOR(l_{i},r_{i}) ; CALC (l_{i},r_{i})) ; proc CALC (l_{i},r_{i})=(CIPHER(l_{i},r_{i},R_{o},L_{o}) ; DOUT (R_{o},L_{o})) ; proc DOUT (r_{o} , l_{o})=(OUTXOR(r_{o} , l_{o})); proc FEAL(t)=(T := t ; DIN (L_{i},R_{i})) ]|:C , K

We have also proved the refinement relation F1 ≤ F2.

Next we can relax the atomicity constraints as follows. First we add and initialize two new variables in and ca:

F3:: proc FEAL • |[ var L_{i},R_{i} , R_{o},L_{o} , T ; ic , co ∈ boolean ; proc INXOR(var l_{i},r_{i})=(|[ var R\underline{i} ; l_{i}.R\underline{i}:= K8..11 ⊕T ; r_{i}:= l_{i}⊕R\underline{i} ]|) ; proc CIPHER(l_{i},r_{i},var r_{o},l_{o})=

(|[var L[j],R[j] for j=0 ,…,8 ; L[0 ],R[0]:= l_{i},r_{i} ; [ L[j],R[j]:= R[j-1] , L[j − 1 ]⊕F (R[j-1],K0..7[16j-15..16j]) ]

for j=0 ,…,8 ; r_{o} , l_{o} :=R[8] , L[8 ] ]| ) ;

proc OUTXOR(r_{o} , l_{o})=(|[ var L\underline{o} ; L\underline{o}:= r_{o}⊕l_{o} ; C := K12..15 ⊕r_{o}.L\underline{o} ]|) ; proc DIN (l_{i},r_{i})=( ¬in → INXOR(l_{i},r_{i}) ; in:= true ) ; proc CALC (l_{i},r_{i})=( ¬ca → CIPHER(l_{i},r_{i},R_{o},L_{o}) ; ca:= true ) ; proc DOUT (r_{o} , l_{o})=(OUTXOR(r_{o} , l_{o})) ; proc FEAL(t)=(T := t ; DIN (L_{i},R_{i})) ; in , ca :=false , false ; do

in → CALC (l_{i},r_{i}) ; in:= false [] ca → DOUT (R_{o},L_{o}) ; ca:= false od ]|:K , C

We have that F2 ≤ F3.

Both DIN and CALC can be viewed as consisting of two parts. The first one execute procedures INXOR and CIPHER correspondingly. Then the control is returned to the caller. Later on the procedures CALC and DOUT are called from separate actions that can be enabled simultaneously. The effect of these refinements is as if we would have introduced an explicit return statement into our language:

F4:: proc FEAL • |[ var L_{i},R_{i} , R_{o},L_{o} , T ; proc INXOR(var l_{i},r_{i})=(|[ var R\underline{i} ; l_{i}.R\underline{i}:= K8..11 ⊕T ; r_{i}:= l_{i}⊕R\underline{i} ]|) ; proc CIPHER(l_{i},r_{i},var r_{o},l_{o})=

(|[var L[j],R[j] for j=0 ,…,8 ; L[0 ],R[0]:= l_{i},r_{i} ; [ L[j],R[j]:= R[j-1] , L[j − 1 ]⊕F (R[j-1],K0..7[16j-15..16j]) ]

for j=0 ,…,8 ; r_{o} , l_{o} :=R[8] , L[8 ] ]| ) ;

proc OUTXOR(r_{o} , l_{o})=(|[ var L\underline{o} ; L\underline{o}:= r_{o}⊕l_{o} ; C := K12..15 ⊕r_{o}.L\underline{o} ]|) ; proc DIN (l_{i},r_{i})=(INXOR(l_{i},r_{i}) ; return ; CALC (l_{i},r_{i})) ; proc CALC (l_{i},r_{i})=(CIPHER(l_{i},r_{i},R_{o},L_{o}) ; return ; DOUT (R_{o},L_{o})) ; proc DOUT (r_{o} , l_{o})=(OUTXOR(r_{o},l_{o})); proc FEAL(t)=(T := t ; DIN (L_{i},R_{i})) ]|:C , K

Hence we have that F3 = F4.

The effect of carrying out F3 is the same as that of F4. The return statement is merely syntactic sugaring.

Separation of DATAIN, CALC and DATAOUT Let us now decompose the action system F4 into a parallel composition of three action systems Datain, Calc and Dataout:

F4 ≤ Datain ∥ Calc ∥ Dataout

where new action systems are defined as below:

Datain:: proc FEAL • |[ var L_{i},R_{i} , T ; proc INXOR=(|[ var R\underline{i}; L_{i}.R\underline{i}:= K8..11 ⊕T ; R_{i}:= L_{i}⊕R\underline{i} ]|) ; proc DIN (l_{i},r_{i})=(L_{i},R_{i}:= l_{i},r_{i} ; INXOR ; return ; CALC (L_{i},R_{i})); proc FEAL(t)=(T := t ; DIN (L_{i},R_{i})) ]|:K , CALC

Calc:: proc CALC • |[ var L_{i},R_{i},R_{o},L_{o} ; proc CIPHER=

(|[var L[j],R[j] for j=0 ,…,8 ; L[0 ],R[0]:= L_{i},R_{i} ; [ L[j],R[j]:= R[j-1] , L[j − 1 ]⊕F (R[j-1],K0..7[16j-15..16j]) ]

for j=0 ,…,8 ; R_{o},L_{o} :=R[8] , L[8 ] ]| ) ;

proc CALC (l_{i},r_{i})=(L_{i},R_{i}:= l_{i},r_{i} ; CIPHER ; return ; DOUT (R_{o} , L_{o})) ]|:K , DOUT

Dataout:: proc DOUT • |[ var R_{o} , L_{o} ; proc OUTXOR=(|[ var L\underline{o} ; L\underline{o}:= R_{o}⊕L_{o} ; C := K12..15 ⊕R_{o}.L\underline{o} ]|) ; proc DOUT (r_{o} , l_{o})=(R_{o} , L_{o}:= r_{o} , l_{o} ; OUTXOR) ]|:C , K

Now the systems communicate through the global procedures CALC and DOUT . We have also removed the parameters (l_{i},r_{i}) and (r_{o},l_{o}) from procedures INXOR, CIPHER and OUTXOR and added some extra assignments into procedures DIN , CALC and DOUT to play the role of the now unnecessary parameters.

6 Registers

From three action systems above only Datain and Dataout can be executed in parallel. To make all components executable simultaneously, we add two registers between the action systems. New procedures REG1 and REG2 are created to keep intermediate results of the computation unchanged while they are used by the next component.

First we refine Datain to Datain′:

(L_{i},R_{i}:= l_{i},r_{i} ; INXOR ; return ; CALC (L_{i},R_{i})) ≤ proc REG1 (l_{i},r_{i})=(|[ var L\underline{i},R\underline{i} ; L\underline{i},R\underline{i}:= l_{i},r_{i} ; return ; CALC (L\underline{i},R\underline{i}) ]|) ; (L_{i},R_{i}:= l_{i},r_{i} ; INXOR ; return ; REG1 (L_{i},R_{i}))

Datain′:: proc FEAL • |[ var L_{i},R_{i} , T ; proc INXOR=(|[ var R\underline{i}; L_{i}.R\underline{i}:= K8..11 ⊕T ; R_{i}:= L_{i}⊕R\underline{i} ]|) ; proc FEAL(t)=(T := t ; DIN (L_{i},R_{i})) ; proc DIN (l_{i},r_{i})=(L_{i},R_{i}:= l_{i},r_{i} ; INXOR ; return ; REG1 (L_{i},R_{i})) ; proc REG1 (l_{i},r_{i})=

(|[ var L\underline{i},R\underline{i} ; L\underline{i},R\underline{i}:= l_{i},r_{i} ; return ; CALC (L\underline{i},R\underline{i}) ]|); proc FEAL(t)=(T := t ; DIN (L_{i},R_{i})) ]|:K , CALC

Then Calc is refined by Calc′:

(L_{i},R_{i}:= l_{i},r_{i} ; CIPHER ; return ; DOUT (R_{o} , L_{o})) ≤ proc REG2 (r_{o},l_{o})=(|[ var R\underline{o},L\underline{o} ; R\underline{o},L\underline{o}:= R_{o},L_{o} ; return ; DOUT (R\underline{o},L\underline{o}) ]|) ; (L_{i},R_{i}:= l_{i},r_{i} ; CIPHER ; return ; REG2 (R_{o} , L_{o}))

Calc′:: proc CALC • |[ var L_{i},R_{i} , R_{o},L_{o} ; proc CIPHER=

(|[var L[j],R[j] for j=0 ,…,8 ; L[0 ],R[0]:= L_{i},R_{i} ; [ L[j],R[j]:= R[j-1] , L[j − 1 ]⊕F (R[j-1],K0..7[16j-15..16j]) ]

for j=0 ,…,8 ; R_{o},L_{o} :=R[8] , L[8 ] ]| ) ;

proc CALC (l_{i},r_{i})=(L_{i},R_{i}:= l_{i},r_{i} ; CIPHER ; return ; REG2 (R_{o} , L_{o})) ; proc REG2 (r_{o},l_{o})=

(|[ var R\underline{o},L\underline{o} ; R\underline{o},L\underline{o}:= R_{o},L_{o} ; return ; DOUT (R\underline{o},L\underline{o}) ]|) ]|:K , DOUT

Finally, we split Datain′ into two components Datain′′ and Reg1 as follows:

Datain′′:: proc FEAL • |[ var L_{i},R_{i} , T ; proc INXOR=(|[ var R\underline{i}; L_{i}.R\underline{i}:= K8..11 ⊕T ; R_{i}:= L_{i}⊕R\underline{i} ]|) ; proc DIN (l_{i},r_{i})=(L_{i},R_{i}:= l_{i},r_{i} ; INXOR ; return ; REG1 (L_{i},R_{i})); proc FEAL(t)=(T := t ; DIN (L_{i},R_{i})) ]|:K , REG1 Reg1:: proc REG1 •

|[ proc REG1 (l_{i},r_{i})=

(|[ var L\underline{i},R\underline{i} ; L\underline{i},R\underline{i}:= l_{i},r_{i} ; return ; CALC (L\underline{i},R\underline{i}) ]|) ]|:K , CALC

Similarly, Calc′ is divided into Calc′′ and Reg2:

Calc′′:: proc CALC • |[ var L_{i},R_{i} , R_{o},L_{o} ; proc CIPHER=

(|[var L[j],R[j] for j=0 ,…,8 ; L[0 ],R[0]:= L_{i},R_{i} ; [ L[j],R[j]:= R[j-1] , L[j − 1 ]⊕F (R[j-1],K0..7[16j-15..16j]) ]

for j=0 ,…,8 ; R_{o},L_{o} :=R[8] , L[8 ] ]| ) ;

proc CALC (l_{i},r_{i})=(L_{i},R_{i}:= l_{i},r_{i} ; CIPHER ; return ; REG2 (R_{o} , L_{o})) ]|:K , REG2

Reg2:: proc REG2 •

|[ proc REG2 (r_{o},l_{o})=

(|[ var R\underline{o},L\underline{o} ; R\underline{o},L\underline{o}:= R_{o},L_{o} ; return ; DOUT (R\underline{o},L\underline{o}) ]|) ]|:K , DOUT

As a result, we have derived the action system that models the processor in Figure 1:

F5:: proc FEAL • |[Datain′′ ∥ Reg1 ∥ Calc′′∥ Reg2 ∥ Dataout]|: C , K

We have also established the refinement relation between initial and final programs:

F0 ≤ F5

7 Concluding remarks

The final parallel composition of action systems is a refinement of the initial sequential program. We isolated so far the basic functional components of the processor and introduced two registers thus creating 3-level pipeline system. All manipulations with the program were completely formal and based on the refinement calculus. To achieve this result we mostly used the method of parallel decomposition of an action system. Communication through the channels was modelled by remote procedure calls. Some steps involved a refinement of the atomicity of the system so they were true refinements and required proofs.

Next step in the derivation would be a refinement of the communication between action systems (components of the processor). We intend to implement it by so called handshaking protocol. Then an isolation of control and data parts of the circuit could follow.

References

[1] R. J. R. Back. On the Correctness of Refinement Steps in Program Development. PhD thesis, Department of Computer Science, University of Helsinki, Helsinki, Finland, 1978. Report A–1978–4.

[2] R. J. R. Back. Refinement calculus, part II: Parallel and reactive programs. In J. W. de Bakker, W.–P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Proceedings. 1989, volume 430 of Lecture Notes in Computer Science. Springer–Verlag, 1990.

[3] R. J. R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. In Proc. of the 2nd ACM SIGACT–SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983.

[4] R. J. R. Back and K. Sere. Stepwise refinement of parallel algorithms. Science of Computer Programming 13, pages 133–180, 1989.

[5] R. J. R. Back and K. Sere. Action systems with synchronous communication. In E.-R. Olderog, editor, Programming Concepts, Methods and Calculi. Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference, pages 107–126, 1994.

[6] R. J. R. Back and K. Sere. Specification of a Microprocessor. Reports on computer science and mathematics 148, Åbo Akademi, 1994.

[7] R. J. R. Back and J. von Wright. Refinement concepts formalised in higherorder logic. Formal Aspects of Computing 2, pages 247–272, 1990.

[8] E. W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.

[9] A. J. Martin. Synthesis of Asynchronous VLSI Circuits. CalTech, Technical Report, 1993.

[10] S. Miyaguchi and A. Shimizu. Fast Data Encipherment Algorithm. EU-ROCRYPT ’87, pages 267–278, 1987.

[11] C. C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3):403–419, July 1988.

[12] J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287–306, 1987.

[13] K. Sere Stepwise Refinement of Parallel Algorithms. PhD thesis, Department of Computer Science, Åbo Akademi University, Turku, Finland, 1990.

[14] J. Staunstrup and M. R. Greenstreet. Synchronized Transitions. IFIP WG 10.5, Summer school on Formal Methods for VLSI Design, Lecture Notes 1990.