Accelerating NoC Verification Using a Complete Model and Active Window

Surajit Das

doi:10.1109/ACCESS.2022.3199671

Accelerating NoC Verification Using a Complete Model and Active Window

2022-01-01

1

OA

AI

DOI：10.1109/ACCESS.2022.3199671

Original

Original request for help

Save

Abstract

En 中文

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.

Keywords:

Synchronization

Switches

Automata

Computational modeling

Ports (computers)

Computer science

Network-on-chip

XML

Network-on-chip

formal model

model checking

finite state machine

starvation

Accelerating NoC Verification Using a Complete Model and Active Window

Abstract

Journal

Organization

Cited Papers