Formal Methods for Schedulings of Latency-Insensitive Designs

Julien Boucaron 1 Jean-Vivien Millo 1 Robert De Simone 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, Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : LID ( Latency-Insensitive Design) 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 behaviour 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 then be formally verified. As turns out, resulting behaviour 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.
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger
Contributeur : Rapport de Recherche Inria <>
Soumis le : jeudi 22 mars 2007 - 11:06:31
Dernière modification le : lundi 5 novembre 2018 - 15:36:03
Document(s) archivé(s) le : mardi 21 septembre 2010 - 12:30:04


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00137495, version 2


Julien Boucaron, Jean-Vivien Millo, Robert De Simone. Formal Methods for Schedulings of Latency-Insensitive Designs. [Research Report] RR-6149, INRIA. 2007, pp.25. 〈inria-00137495v2〉



Consultations de la notice


Téléchargements de fichiers