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

software based models in much the same way as compilers produce executable
code. Examples of such languages are Esterel, Lustre and Signal, see e.g. [2].
In this paper, we will use Gezel [12,15] as our choice of language for hard-
ware models. It depends on reasonably few, simple and clean concepts, and it
strikes a balance between software and hardware concerns that we believe suits
the needs for a modern top-down approach to hardware design. Gezel is based
on an execution model which resembles the synchronous model of Esterel, but
unlike Esterel, the language of Gezel contains constructs for hardware design.
Compared to VHDL and Verilog, Gezel may be considered to be at a higher
abstraction level without any explicit timing constructs. This allows Gezel to be
truly independent of any implementation technology.
The advantage of Gezel is that the language has simple parts with a clear
hardware meaning, e.g. registers, controllers, synchronous execution. There are
simulators for Gezel, and, furthermore, the language is designed so that it can
be mapped to a synthesizable subset of VHDL. But the language has no formal
semantics, and it is dicult to get a clear understanding of some of the more
advanced constructs.
In this paper, we will give a semantics domain which can be used for hard-
ware design languages like Gezel. With this semantics, we believe, that a new
Gezel-like language could be defined, where the syntax reflects the semantics in
a direct manner. We also show how the semantics can be used in connection
with verification by relating the semantical domain to timed-automata [1]. We
have experimented with verification of some examples, e.g. the Simplified Data
Encryption Standard Algorithm [11], using the Uppaal system [4].

2 Gezel Specifications

The specification language Gezel [13,14] is used to express models of hardware.
It comes with an interpreter as well as a translator with VHDL as its target
language. The interpreter provides means for simulation and debugging. The
language does not have a formal semantics, and there is no tool for the verifica-
tion of Gezel specifications.
A Gezel specification describes a number of components and their intercon-
nections . A Gezel component consists of a datapath providing a set of named
actions, called signal flow graphs (sfg), and a controller expressed as a finite
state machine which may execute one or more actions in each state transition.
This model is called finite state machine with datapath [8], or FSMD in short.
Fig. 1 shows the elements and structure of an FSMD, while Fig. 2 shows the
pattern for the most essential parts of a Gezel specification.
A Gezel component models a piece of hardware which is always active. Such
components operate in parallel and do not depend on resource allocations. The
expressiveness of the FSMD model allows any type of digital hardware architec-
ture to be modelled, from dedicated hardware devices to full micro processors.
The execution semantics of Gezel is that of complete synchrony, i.e. every FSMD
of a Gezel specification makes exactly one transition in every clock cycle.