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

where T p is the timed automaton for the single assignment program p presented
in Fig. 8. The local procedure P corresponds to the function p M in Sect. 5.2.
Actually, this automaton is just a special case of the transition shown in Fig. 7,
where the is no guard on the transition and s 1 = s 2 .

7 Examples: Verification of Gezel Specification

In this section we will provide verification examples of high-level hardware de-
signs. The specifications were described as modules and translated into Uppaal
as shown in Sect. 6. We neither give the modules nor the timed automata.
The three examples are specifications of two different greatest common divisor
(gcd) algorithms and a specification of a simplified DES (SDES) algorithm [11].
The aim of the verification is to guarantee certain properties of the underlying
algorithm, e.g. a correct output for every input, an upper bound for the number
of clock cycles needed to compute the output, and an upper bound on the changes
of register values before the algorithm can provide an output — the last being
an indicator of the energy consumption.

7.1 First gcd-Algorithm

This first gcd-algorithm is a simple algorithm based in repeated subtraction as
shown in the following pseudo-code:

while a != b
do { if a < b then b := b-a; else a := a-b };
c:=a;

where a and b are the input ports and c is the output port. A Gezel specification
is found in Fig 3.

7.2 Second gcd-Algorithm

This second gcd-algorithm, in Fig. 9, is a recursive version, see [17], where
even(x) is true iff x is even. A Gezel specification is found in Appendix A.

7.3 Verification of gcd-Specifications

The hardware specifications for the two gcd-algorithms were translated (by hand)
to the Uppaal models, following the principle from Sect. 6. Each timed-automata
model was put in parallel with a timed automaton for the environment, where
the environment automata provides the input for gcd on the first input syn-
chronization. In Uppaal, the input from the environment is chosen by the use
of a select statement, which for verification purposes means that any input is
attempted.
A query for verifying that for all combinations of inputs an output is generated
(i.e. the automaton gcd reaches a final state final )isasfollows: