A generic model for formally verifying NoC communication architectures: A case study

被引：0

作者：

Borrione, Dominique ^{[1
]}

Helmy, Amr ^{[1
]}

Pierre, Laurence ^{[1
]}

Schmaltz, Julien ^{[2
]}

机构：

[1] INPG, TIMA Lab, 46 Av Felix Viallet, F-38031 Grenoble, France

[2] Univ Saarland, D-66041 Saarbrucken, Germany

来源：

NOCS 2007: FIRST INTERNATIONAL SYMPOSIUM ON NETWORKS-ON-CHIP, PROCEEDINGS | 2007年

关键词：

D O I：

暂无

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Networks on Chip are emerging as a promising solution for the design of complex Systems on a Chip, to interconnect manufactured IP cores, and the need to formally guarantee their correctness is crucial. In a NoC centered design, the individual IP's are considered already validated. This paper addresses the validation of the communication infrastructure. A generic formal model for NoCs has been developed and implemented in the ACL2 theorem prover. As an application, the HERMES network has been formalized in this model, and we show that both formal proofs and simulation experiments can be performed in ACL2.

引用

页码：127 / +

页数：2

共 50 条

[1] New generic GALS NoC architectures with multiple QoS
Zid, Mounir
Zitouni, Abdelkrim
Baganne, Adel
Tourki, Rached
[J]. IEEE DTIS: 2006 INTERNATIONAL CONFERENCE ON DESIGN & TEST OF INTEGRATED SYSTEMS IN NANOSCALE TECHNOLOGY, PROCEEDINGS, 2006, : 345 - 349
[2] A Case Study for NoC-Based Homogeneous MPSoC Architectures
Tota, Sergio V.
Casu, Mario R.
Roch, Massimo Ruo
Macchiarulo, Luca
Zamboni, Maurizio
[J]. IEEE TRANSACTIONS ON VERY LARGE SCALE INTEGRATION (VLSI) SYSTEMS, 2009, 17 (03) : 384 - 388
[3] A Case Study on Formally Verifying an Open-source Deep Learning Accelerator Design
Jain, Anshul
Kumar, Binod
[J]. 2023 IEEE 32ND ASIAN TEST SYMPOSIUM, ATS, 2023, : 165 - 170
[4] An analytical model for reliability evaluation of NoC architectures
Dalirsani, Atefe
Hosseinabady, Mohammad
Navabi, Zainalabedin
[J]. 13TH IEEE INTERNATIONAL ON-LINE TESTING SYMPOSIUM PROCEEDINGS, 2007, : 49 - 54
[5] Customized NoC Topologies Construction for High Performance Communication Architectures
Ezhumalai, P.
Chilambuchelvan, A.
[J]. ADVANCES IN POWER ELECTRONICS AND INSTRUMENTATION ENGINEERING, 2011, 148 : 88 - +
[6] A generic model for software architectures
Rossak, W
Kirova, V
Jololian, L
Lawson, H
Zemel, T
[J]. IEEE SOFTWARE, 1997, 14 (04) : 84 - 92
[7] An Efficient Channel Model for Evaluating Wireless NoC Architectures
Agyeman, Michael Opoku
Vien, Quoc-Tuan
Hill, Gary
Turner, Scott
Mak, Terrence
[J]. 2016 28TH IEEE INTERNATIONAL SYMPOSIUM ON COMPUTER ARCHITECTURE AND HIGH PERFORMANCE COMPUTING WORKSHOPS (SBAC-PADW), 2016, : 85 - 90
[8] A Performance Model of Communication in the Quarc NoC
Moadeli, M.
Vanderbauwhede, W.
Shahrabi, A.
[J]. PROCEEDINGS OF THE 2008 14TH IEEE INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED SYSTEMS, 2008, : 908 - +
[9] Improving Energy Consumption of NoC based Architectures through Approximate Communication
Ascia, Giuseppe
Catania, Vincenzo
Monteleone, Salvatore
Palesi, Maurizio
Patti, Davide
Jose, John
[J]. 2018 7TH MEDITERRANEAN CONFERENCE ON EMBEDDED COMPUTING (MECO), 2018, : 33 - 36
[10] Formally specifying and verifying mobile agents - Model checking mobility: The MobiOZ approach
Information Systems Architecture Research Division, Grace Center National Institute of Informatics, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101 8430, Japan
不详
[J]. International Journal of Agent-Oriented Software Engineering, 2008, 2 (04) : 449 - 474

← 1 2 3 4 5 →