Formal verification of circuit-switched Network on chip (NoC) architectures using SPIN

Simulation techniques cannot cope with the distributive and reactive nature of Network on chip (NoC) architectures very well and thus compromise on the accuracy of the analysis results. Formal verification has been used to overcome these challenges but, to the best of our knowledge, has been mainly used for the verification of packet-switched NoC's. The main focus of this paper is on the formal verification of circuit-switched NoC's, which provide a dedicated channel for all communications with full bandwidth and thus are found to be more efficient than packet-switched NoCs in many contexts. In particular, the paper presents a generic methodology for the formal verification of circuit-switched NoC using the SPIN model checker. The proposed methodology provides generic modelling guidelines and identifies some properties, including deadlock freedom, starvation freedom, mutual exclusion and liveness, that are quite useful in the context of circuit-switched NoC. For illustration purposes, we use our methodology to verify the programmable NoC (PNoC) architecture, which is one of the most widely used circuit-switched NoC.