xMAS Based Accurate Modeling and Progress Verification of NoCs

Network on Chip (NoC) plays a significant role in improving computation speed in Tiled Chip Multiprocessor (TCMP) by acting as an efficient interconnection network between the tiles. Designing a NoC satisfying all important functional properties with high efficiency is challenging. Some of the crucial properties to be fulfilled for proper functioning of NoC with efficiency are namely progress, mutual exclusion, starvation freedom, deadlock freedom, congestion freedom and livelock freedom. Exhaustive checking of such system properties in NoC can be done by formal verification method. In existing verification works, NoC are modeled in abstract level. Therefore, the properties verified does not guarantee that they work in real hardware. In our work, we have modeled NoC router using Executable Micro Architectural Specification (xMAS) primitives so that our design becomes near to register transfer level (RTL). In this model, we have verified progress property with help of NuSMV model checker. Experimental results show that our model is scalable for progress verification in Mesh and Ring topologies.