LAUSR

This work presents formal modeling of Network-on-Chip (NoC) considering detailed functional units of NoC. The intricate modeling of NoC router components like buffer, switch, and arbiter is accomplished using Finite State Machine (FSM). As in the case of a real NoC, parallel execution of these functional units is carried out by maintaining the synchronization between these functional units within a router and between each of the adjacent routers in the presented formal model. Important properties for the correctness of the proposed model are verified using a model checker. Implementing a detailed and a complete NoC model is a memory extensive operation while verifying with a model checker. We have introduced a concept of active windows to verify each router and its communication with the adjacent routers. The correctness of the model is checked by verifying the synchronization between NoC functional units and NoC routers, verifying progress in functional units, and verifying the successful transfer of packets. Verification of starvation freedom in an NoC router is also performed for round-robin arbiter and fixed-priority arbiter. Parallel threads are used in the experiments to reduce the verification time.