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
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Bouyer, Patricia; Fahrenberg, Uli; Larsen, Kim Guldstrand; Markey, Nicolas; Ouaknine, Joël; Worrell, James: Model checking real-time systems (2018)
- Fahrenberg, Uli; Larsen, Kim G.; Legay, Axel: Model-based verification, optimization, synthesis and performance evaluation of real-time systems (2013)
- Fahrenberg, Uli; Larsen, Kim G.; Thrane, Claus R.: Verification, performance analysis and controller synthesis for real-time systems (2010)
- Hansen, Michael R.; Madsen, Jan; Brekling, Aske Wiid: Semantics and verification of a language for modelling hardware architectures (2007)
- Sakiyama, K.; Batina, L.; Preneel, B.; Verbauwhede, I.: HW/SW co-design for public-key cryptosystems on the 8051 micro-controller (2007)
- Schaumont, Patrick; Verbauwhede, Ingrid: Domain specific tools and methods for application in Security processor design (2002)
Further publications can be found at: http://rijndael.ece.vt.edu/gezel2/publications.html