Formal Modeling of Network-on-Chip and its Applications in Starvation and Deadlock Detection and in Developing Deadlock Free Routing Algorithms

Abstract

Due to the uncontrolable heat genearated by a single high speed processor the transition takes place from a single high frequencey processor to Chip Multi Processor (CMP) consists of many processors with moderate clock frequency. The communication between these processors take place with help of a programmable network called Network-on-Chip. Starvation and deadlock are two major issues that degrade the performance of NoC or halt the system. There is no inbuild support to detect such problem in state-of-the-art NoC simulators like Booksim and Gem5. Therefore, our objective is to detect deadlock and starvation using formal model. The first contribution of the thesis ia formal modeling of complete NoC using Finite State Machne (FSM) and detection of starvation freedom. We have used NuSMV model checker to verify the FSM based NoC model. We have also verified progress and transfer of packets in the FSM based NoC model. In our second contribution, we have modelled detailed NoC using Communicating Finite State Machine (CFSM) for detection of application specific deadlock. We have developed a simulation framework with the CFSM based model. The formal simulator checks a given traffic pattern with respect to a given algorithm for detection of confirmed deadlock. We have tested three algorithms using our CFSM based simulator. We have detected deadlock in dynamic XY-routing and detected false positive deadlock warning in the booksim simulator. In our third contribution, we presented deadlock analysis in Torus NoC. Torus NoC is deadlock prone due to the inbuild cyclic paths via wraparound channels, that are useful in reducing hop counts. We have proposed a deadlock avoidance approace for Torus NoC called Arc Model. We have also proposed Directional Dependecny Graph (DDG) for theoretical deadlock detection and avoidance. In our fourth contribution, we have proposed three deadlock free routing algorithms for Torus NoC using Arc Model and DDG. These algorithms do not use any additional resources for deadlock avoidance. We have compared our algorithms with FirstHop and Up*/Down* routing using uniform traffic and PARSEC benchmark suites. Our future direction of work is to develop more effecient algorithms analysing hardware overhead.