Skip to Content

Search

Formal Verification of Design Properties of Hardware Architectures

Fri, 10/26/2012 - 16:43 — Andreas Vörg, eda...
0
Your rating: None
(unregistered) Author(s): 
Aske Brekling
Jan Madsen
Michael R. Hansen
Download URL: 
http://www.imm.dtu.dk/English.aspx

We present a formal language for hardware models based on the Gezel hardware description language developed and maintained by Virginia Tech, USA. The language depends on reasonably few, simple and clean concepts, and it strikes a balance between software and hardware concerns that suits the needs for a modern top-down approach to hardware design. We show how the language can be used in connection with verification by relating the semantical domain to timed-automata using the UPPAAL system. Besides presenting the language and the semantic domain as a timed-automata model, we will demonstarte a formal verification of design properties of a few simple example circuits including the Simplified Data Encryption Standard (SDES) Algorithm and different algorithmic implementations of the Greatest Coomon Divisor. Verification guarantees properties of the underlying algorithm, e.g. correct output for any given input, as well as other properties such as upper limits on the number of clock cycles for the algorithm to stabilize with a given input and upper limits on the number of register updates, to serve as an indicator of energy consumption.

Contact:
Jan Madsen (Jan@imm.dtu.dk)

Project Information
Project Acronym: 
MoDES
Project Homepage: 
http://www.cs.aau.dk/modes/
Project Description: 
Model Driven Development of Intelligent Embedded Systems: Embedded systems are a modern technology that is rapidly changing our society. Intelligence, in the form of software and hardware, is introduced into all kinds of products and artifacts with the objective of enhancing their functionality. In order for the industries to meet this demand in an efficient and predictable manner, their design engineers must master a complex set of constraints related to hardware, software, and reconcile them with the specific needs of the application in the overall product. The sheer complexity of future embedded devices is seriously challenging current development and maintenance practices, and new, integrating and scalable methods are urgently needed. The MoDES project will research, develop, evaluate and disseminate concepts, methods and tools that can be used to design dependable embedded systems that meet their requirements in a controlled and resource-efficient way using model-driven approaches. This means that design decisions, analysis, simulation, testing, code generation, on-line monitoring etc. are always based upon models that reflect the relevant aspects of the design. This requires tools and techniques to maintain, manipulate, combine, transform and analyze models in a coherent and meaningful way.


Theme by Dr. Radut.