Formal Methods for Scheduling of Latency-Insensitive Designs - Archive ouverte HAL Access content directly
Journal Articles EURASIP Journal on Embedded Systems Year : 2007

Formal Methods for Scheduling of Latency-Insensitive Designs

(1) , (1) , (1)
1

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.
Fichier principal
Vignette du fichier
1687-3963-2007-039161.pdf (311.92 Ko) Télécharger le fichier
Vignette du fichier
1687-3963-2007-039161.xml (12.1 Ko) Télécharger le fichier
Origin : Publisher files allowed on an open archive
Format : Other
Loading...

Dates and versions

hal-00784464 , version 1 (04-02-2013)

Identifiers

Cite

Julien Boucaron, Robert de Simone, Jean-Vivien Millo. Formal Methods for Scheduling of Latency-Insensitive Designs. EURASIP Journal on Embedded Systems, 2007, 2007 (1), pp.039161. ⟨10.1155/2007/39161⟩. ⟨hal-00784464⟩
113 View
189 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More