Formal methods for networks on chips

Systems on a chip (SoC) are complex embedded systems consisting of many hardware and software blocks. As the complexity of SoCs grows, the focus is less on the computation, and increasingly on communication. This results in a shift from design based on platforms (design templates) to design style that is communication-centric. In this new paradigm, on-chip interconnects must address both the deep-submicron challenges (managing the number of long wires, timing closure, etc.) and complexity (scalability, quality of service, etc.). Networks on chips (NoC) have emerged as a new type of interconnect that can solve these problems. In this paper we introduce the Ethereal NoC as an example to identify when and where formal methods can play a role in this field of research. NoCs use the same basic concepts as computer networks (packets and routers), but the trade-offs that must and can be made are very different. Wires are relatively shorter, NoC resources are relatively expensive compared to the computation resources are interconnected, and the on-chip environment is more stable than off-chip (e.g. for data loss and synchronisation). As a result, many new NoC architectures have been developed.