A Process Algebraic View of Latency-Insensitive Systems

Latency-insensitive (LI) systems are those which can function correctly in spite of delays along its connecting wires. This delay is assumed to be a multiple of the clock period. The paper presents a single-clock process algebraic model for such systems. It gives the definitions for LI computational blocks and LI connectors. Important properties for these are shown to be satisfied. Composition of such modules can be done by the parallel composition operator of the process algebra. Conditions are given to check for liveness and deadlock freedom of LI systems. Comparison of latency equivalence between streams of events can be done using the model and this leads to a method of proving latency-equivalent modules. The paper is a step toward high-level specification and verification of such systems. The work can be extended to address more complex interconnections by modeling the underlying finite-state machines.