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

Semantics and Verification of a Language for
Modelling Hardware Architectures

Michael R. Hansen, Jan Madsen, and Aske Wiid Brekling

Informatics and Math. Modelling, Technical University of Denmark
Ricard Petersens Plads, DK-2800 Lyngby
[e-mail], [e-mail], [e-mail]

Abstract. In this paper we consider a high-level hardware description
language Gezel, from which hardware can be synthesized through a trans-
lation to VHDL. The language is equipped with a simulator and supports
exploration of hardware designs. The language has no semantics and it
is dicult to get a deep understanding of many of the constructions.
We therefore give a semantic domain for Gezel. Aiming at automated
verification we relate this domain to the timed-automata model and we
have experimented with verification of Gezel-specifications using the Up-
paal system. In particular, we have proven the correctness of a hardware
specification of the Simplified DES algorithm. We have also used Uppaal
for small experiments of verifying resource usage.
Keywords: Hardware descriptions, semantics, verification, model-
checking.

1 Introduction

As the complexity of chips grows, the methodology to build chips has to evolve.
Today, chips are largely synthesized from high-level architectural descriptions
which hide low-level details such as the physical characteristics of a transis-
tor or how to build a flip-flop. This applies to chips ranging from small scale,
specialized chips to be produced in modest quantities to highly complex ones of
general computers for mass production. Today, the majority of hardware designs
are done using the most common hardware description languages, VHDL [18]
or Verilog [16]. Both languages support high-level architectural descriptions, but
allow hardware designers to incorporate low-level details in order to optimize
for a particular hardware technology. Although this makes it possible to pro-
duce highly optimized chips it also ties the hardware description to a particular
technology or set of technologies.
It is possible to synthesize chips directly from VHDL and Verilog using a
restricted subset of the languages. However, chips may also be synthesized from

This work has been partially funded by The Danish Council for Strategic Research
under project MoDES , the Danish National Advanced Technology Foundation un-
der project DaNES , and ARTIST2 (IST-004527).