VHDL Observers for Clock Constraint Checking

Charles André 1 Frédéric Mallet 1 Julien Deantoni 1
1 AOSTE - Models and methods of analysis and optimization for systems with real-time and embedding constraints
CRISAM - Inria Sophia Antipolis - Méditerranée , Inria Paris-Rocquencourt, COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : Abstract--Logical time has proved very useful to model heterogeneous and concurrent systems at various abstraction levels. The Clock Constraint Specification Language (CCSL) uses logical clocks as first-class citizens and supports a set of (logical) time patterns to specify the time behavior of systems. We promote here the use of CCSL to express and verify safety properties of VHDL designs. Our proposal relies on an automatic transformation of a CCSL specification into VHDL code that checks the expected properties. Being written in VHDL this code can be integrated in a classical VHDL design and verification flow. Our proposed structural transformation assembles instances of pre-built VHDL components while preserving the polychronous semantics of CCSL. This is not trivial due to major differences between the discrete-time delta cycle based semantics of VHDL and the fixed point semantics of CCSL. This paper describes these differences and proposes solutions to deal with them so as to build VHDL observers for the kernel CCSL constraints. We illustrate the approach by verifying an open-source implementation of the AMBA AHB-to-ABP bridge.
Type de document :
Communication dans un congrès
Symposium on Industrial Embedded Systems, Jul 2010, trento, Italy. IEEE computer society, 2010, <http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5551372VHDL Observers for Clock Constraint Checking>. <10.1109/SIES.2010.5551372>
Liste complète des métadonnées

https://hal.inria.fr/inria-00587107
Contributeur : Team Aoste <>
Soumis le : mardi 19 avril 2011 - 14:27:11
Dernière modification le : lundi 5 octobre 2015 - 16:58:44

Identifiants

Collections

Citation

Charles André, Frédéric Mallet, Julien Deantoni. VHDL Observers for Clock Constraint Checking. Symposium on Industrial Embedded Systems, Jul 2010, trento, Italy. IEEE computer society, 2010, <http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5551372VHDL Observers for Clock Constraint Checking>. <10.1109/SIES.2010.5551372>. <inria-00587107>

Partager

Métriques

Consultations de la notice

146