Accelerating NoC Verification Using a Complete Model and Active Window
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 funct...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2022-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/9858921/ |
| _version_ | 1798036264614625280 |
|---|---|
| author | Surajit Das Chandan Karfa Santosh Biswas |
| author_facet | Surajit Das Chandan Karfa Santosh Biswas |
| author_sort | Surajit Das |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-11T21:10:17Z |
| format | Article |
| id | doaj.art-c10e39aa8dc2480d9438a9fc855e423c |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-04-11T21:10:17Z |
| publishDate | 2022-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-c10e39aa8dc2480d9438a9fc855e423c2022-12-22T04:03:03ZengIEEEIEEE Access2169-35362022-01-0110889858899910.1109/ACCESS.2022.31996719858921Accelerating NoC Verification Using a Complete Model and Active WindowSurajit Das0https://orcid.org/0000-0003-3397-7777Chandan Karfa1https://orcid.org/0000-0002-3835-4184Santosh Biswas2https://orcid.org/0000-0003-3020-4154Department of Computer Science and Engineering, GITAM School of Technology, Bengaluru, Karnataka, IndiaDepartment of Computer Science and Engineering, IIT Guwahati, Guwahati, Assam, IndiaDepartment of Electrical Engineering and Computer Science, IIT Bhilai, Raipur, Chhattisgarh, IndiaThis 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.https://ieeexplore.ieee.org/document/9858921/Network-on-chipformal modelmodel checkingfinite state machinestarvation |
| spellingShingle | Surajit Das Chandan Karfa Santosh Biswas Accelerating NoC Verification Using a Complete Model and Active Window IEEE Access Network-on-chip formal model model checking finite state machine starvation |
| title | Accelerating NoC Verification Using a Complete Model and Active Window |
| title_full | Accelerating NoC Verification Using a Complete Model and Active Window |
| title_fullStr | Accelerating NoC Verification Using a Complete Model and Active Window |
| title_full_unstemmed | Accelerating NoC Verification Using a Complete Model and Active Window |
| title_short | Accelerating NoC Verification Using a Complete Model and Active Window |
| title_sort | accelerating noc verification using a complete model and active window |
| topic | Network-on-chip formal model model checking finite state machine starvation |
| url | https://ieeexplore.ieee.org/document/9858921/ |
| work_keys_str_mv | AT surajitdas acceleratingnocverificationusingacompletemodelandactivewindow AT chandankarfa acceleratingnocverificationusingacompletemodelandactivewindow AT santoshbiswas acceleratingnocverificationusingacompletemodelandactivewindow |