Formal Methods for Scheduling of Latency-Insensitive Designs

Julien Boucaron 1, * Robert De Simone 1 Jean-Vivien Millo 1
* Auteur correspondant
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 : Latency-insensitive design (LID) theory was invented to deal with SoC timing closure issues, by allowing arbitrary fixed integer latencies on long global wires. Latencies are coped with using a resynchronization protocol that performs dynamic scheduling of data transportation. Functional behavior is preserved. This dynamic scheduling is implemented using specific synchronous hardware elements: relay-stations (RS) and shell-wrappers (SW). Our first goal is to provide a formal modeling of RS and SW, that can be then formally verified. As turns out, resulting behavior is k-periodic, thus amenable to static scheduling. Our second goal is to provide formal hardware modeling here also. It initially performs throughput equalization, adding integer latencies wherever possible; residual cases require introduction of fractional registers (FRs) at specific locations. Benchmark results are presented, run on our Kpassa tool implementation.
Type de document :
Article dans une revue
EURASIP Journal on Embedded Systems, SpringerOpen, 2007, 2007 (1), pp.039161. 〈10.1155/2007/39161〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger
Contributeur : Ed. Bmc <>
Soumis le : lundi 4 février 2013 - 13:13:17
Dernière modification le : mercredi 14 décembre 2016 - 01:06:45
Document(s) archivé(s) le : lundi 17 juin 2013 - 18:46:42




Julien Boucaron, Robert De Simone, Jean-Vivien Millo. Formal Methods for Scheduling of Latency-Insensitive Designs. EURASIP Journal on Embedded Systems, SpringerOpen, 2007, 2007 (1), pp.039161. 〈10.1155/2007/39161〉. 〈hal-00784464〉



Consultations de
la notice


Téléchargements du document