Formal micro-architectural analysis of on-chip ring networks

In the realm of Multi-Processors System-on-Chip (MPSoC’s), the Network-on-Chip (NoC) connecting all system components plays a crucial role in the overall correctness and performance of the system. Recent papers have proposed several ring based NoC solutions. The description and analysis of these micro-architectures are informal in nature. Text is used to argue about, e.g., deadlock freedom. For the first time, this paper proposes an environment for the formal modelling and analysis of such ring architectures with an emphasis on liveness properties. Our contribution includes a language to model ring micro-architectures, invariant generation techniques, deadlock freedom verification, and the application of our approach on a realistic case-study. The analysis reveals a possible deadlock not mentioned in the original paper.