Paper Info
Title
Semantics and verification of a language for modelling hardware architectures
Abstract
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.
Year
Venue
Keywords
2007
Formal Methods and Hybrid Real-Time Systems
simplified des algorithm,timed-automata model,modelling hardware architecture,high-level hardware description language,automated verification,hardware design,small experiment,semantic domain,hardware specification,deep understanding,uppaal system,hardware description language,verification,semantics,hardware architecture
Field
DocType
Volume
Functional verification,Programming language,Gezel,Intelligent verification,Computer science,Theoretical computer science,VHDL,Formal methods,High-level verification,Computer hardware,Hardware architecture,Hardware description language
Conference
4700
ISSN
ISBN
Citations 
0302-9743
3-540-75220-X
3
PageRank 
References 
Authors
0.36
11
3
Name
Order
Citations
PageRank
Michael r. Hansen154343.29
Jan Madsen257656.90
Aske Wiid Brekling3191.11