Application of Formal Methods for System-Level Verification of Network on Chip

Network on chip (NoC) is a system design methodology that uses on-chip routers for integrating the resources on a system on chip (SoC). Applications on the SoC communicate through a layered communication protocol implemented on the NoC´s router-based communication architecture. There is need for a formal system level model of NoC to verify end-to-end protocol correctness in an NoC architecture. In this paper we present a new formal model of the existing Hermes NoC router architecture and its communication scheme using a new formal language called Heterogeneous Protocol Automata (HPA). We model the five bi-directional ports and the bounded buffers at input port of the Hermes Router, including the XY routing algorithm, priority based arbitration logic, wormhole switching and the request-ack handshake protocol of the communication scheme. The automata model is then mapped manually to PROMELA, the specification language of the SPIN model checker for verification, with promising results.