Semantics and Verification of a Language for Modelling Hardware Architectures - Formal Methods and Hybrid Real-Time Systems - page 303

2.1 Extracting FSMD from Programs

An imperative program may be split into basic blocks , i.e. a maximal sequence
of assignments (without any control statement), and its control flow. A program
may then be represented as a graph, with edges mapping into basic blocks and
nodes into control points, typically conditional jumps. Such a graph corresponds
to a finite state machine of Mealy type. This graph is translated to the FSMD
model as follows: each basic block forms an action of the datapath and the finite
state machine becomes the controller of the FSMD, which executes exactly one
basic block in each transition.
Fig. 3 shows the pseudo-code for a greatest common divisor (gcd) algorithm
and its corresponding Gezel specification. Five basic blocks, named bb0 to bb4 ,
are extracted from the gcd-program and the controller consists of 4 states and
6 transitions. Using Gezel all outputs must be given well-defined values in every
transition. This is captured by the action update , which makes sure that the
output c is always given the value of res . Registers, declared as reg ,storevalues

gcd(a,b) =
while a!=b
do if a<b
then b:=b-a;
else a:=a-b;

dp gcd(in a,b: ns(8);
out c: ns(8)) {
reg x, y, res: ns(8);
reg xlessy, xneqy: ns(1);

sfg bb0 { x=a; y=b; xneqy=(a!=b); }
sfg bb1 { xlessy=(x<y); }
sfg bb2 { y=y-x; xneqy=(x!=y-x); }
sfg bb3 { x=x-y; xneqy=(x-y!=y); }
sfg bb4 { res=x; }
sfg update { c=res; }

} ;
c:=a;

}

fsm gcd_ctl(gcd) {
initial s0;
state s1, s2, s3;

@s0 (bb0, update) -> s1;

@s1 if (xneqy)
then (bb1, update) -> s2;
else (bb4, update) -> s3;
@s2 if (xlessy)
then (bb2, update) -> s1;
else (bb3, update) -> s1;
@s3 (bb4, update) -> s3;

}

Fig. 3. An imperative program for gcd and a corresponding Gezel program for a 8-bit
version of the gcd