Skip to Main content Skip to Navigation

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.
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Thursday, March 22, 2007 - 11:06:31 AM
Last modification on : Friday, January 21, 2022 - 3:15:47 AM
Long-term archiving on: : Tuesday, September 21, 2010 - 12:30:04 PM


Files produced by the author(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⟩



Record views


Files downloads