Semantics and verification of a language for modelling hardware architectures In this paper we consider a high-level hardware description language Gezel, from which hardware can be synthesized through a translation to VHDL. The language is equipped with a simulator and supports exploration of hardware designs. The language has no semantics and it is difficult 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 Uppaal 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 for this software

Anything in here will be replaced on browsers that support the canvas element