Information Technology Reference
In-Depth Information
GCD(a,b) =
if even(a) & even(b)
then 2 * GCD(a/2, b/2)
else if even(a) & !even(b)
then GCD(a/2, b)
else if !even(a) & even(b)
then GCD(a, b/2)
else if a > b
(* a and b are both odd *)
then GCD(a-b,b)
else GCD(a,b-a)
Fig. 9.
Recursive gcd-algorithm
A<>gcd.final
which reads: “for all (
A
) paths, there exists a state (
<>
) where the gcd automaton
is in state final.
Verifying that correct output is produced for any input combination is done
by comparing the result with that of a proven correct implementation (
igcd
)of
the greatest common divisor. This query is specified as follows:
A[]gcd.final imply (igcd(a,b)==c)
where
[]
reads “for all states on a path”.
Two extra variables (
regUpdate
and
cycle
) are added to the specifications to
keep track of the number of changes in register values and the number of clock
cycles. Examples of queries are:
A<>gcd.final && regUpdate <= r
A<>gcd.final && cycle <= x
where
r
and
x
are upper-bound candidates for the number of register changes
and the number of clock cycles needed, respectively.
7.4
Verification of SDES Specification
We have also verified a Gezel specification for the Simplified DES algorithm
(SDES) [11]. The Gezel specification is too elaborate to give here, as the encryp-
tion controller, for example, has 10 states and 9 actions. Encryption takes an
8 bit plaintext and a 10 bit key and produces an 8 bit ciphertext. Decryption
takes the 8 bit ciphertext and the same 10 bit key and produces the original 8
bit plaintext.
Verifying that the hardware design is correct is done in two steps. First, it is
verified that for all input combinations the final state (
final
)ofthe
decryption
automaton is reached:
Search WWH ::
Custom Search