Formal estimation of worst-case communication latency in a Network-on-chip

Network on a Chip (NoC) is an on-chip communication infrastructure implemented using routers similar to a computer network. NoC is used to design complex systems-on-chip (SoCs) for applications that expect quality-of-service (QoS) guarantee, which depends on the application traffic characteristics, timing constraints, NoC router architecture and communication paradigm. There are several QoS metrics such as data-integrity, latency and throughput, however, in this paper we measure latency upper bound (i.e., worst-case communication latency) as it provides insight on QoS guarantee of the system. We present a formal framework for evaluating worst-case end-to-end latency of packets in an on-chip network, which is obtained by systematic abstraction of an earlier formal modeling and verification framework to verify large NoC designs. Worst case communication latencies of the packets are measured for uniform traffic scenarios at different uniform packet injection rates.