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 条

[21] Power-Efficient Inter-Layer Communication Architectures for 3D NoC
Rahmani, Amir-Mohammad
Latif, Khalid
Vaddina, Kameswar Rao
Liljeberg, Pasi
Plosila, Juha
Tenhunen, Hannu
[J]. 2011 IEEE COMPUTER SOCIETY ANNUAL SYMPOSIUM ON VLSI (ISVLSI), 2011, : 355 - +
[22] GENERIC MODEL CONTROL - A CASE-STUDY REVISITED
HARRIS, TJ
MCLELLAN, PJ
[J]. CANADIAN JOURNAL OF CHEMICAL ENGINEERING, 1990, 68 (06): : 1066 - 1070
[23] An investigation of latency prediction for NoC-based communication architectures using machine learning techniques
Jefferson Silva
Márcio Kreutz
Monica Pereira
Marjory Da Costa-Abreu
[J]. The Journal of Supercomputing, 2019, 75 : 7573 - 7591
[24] An investigation of latency prediction for NoC-based communication architectures using machine learning techniques
Silva, Jefferson
Kreutz, Marcio
Pereira, Monica
Da Costa-Abreu, Marjory
[J]. JOURNAL OF SUPERCOMPUTING, 2019, 75 (11): : 7573 - 7591
[25] Formally Synthesising a Protocol Converter: A Case Study
Cao, Jing
Nymeyer, Albert
[J]. IMPLEMENTATION AND APPLICATION OF AUTOMATA, PROCEEDINGS, 2009, 5642 : 249 - 252
[26] Case study: verifying a security protocol
不详
[J]. ISABELLE/HOL, 2002, 2283 : 195 - 204
[27] A generic model to simulate the growth of forage legumes with contrasting architectures
Lucas, Faverjon
Gaetan, Louarn
[J]. 2016 IEEE INTERNATIONAL CONFERENCE ON FUNCTIONAL-STRUCTURAL PLANT GROWTH MODELING, SIMULATION, VISUALIZATION AND APPLICATIONS (FSPMA), 2016, : 61 - 67
[28] Performance and communication energy constrained embedded benchmark for fault tolerant core mapping onto NoC architectures
Kumar, Aruru Sai
Rao, T. V. K. Hanumantha
Reddy, B. Naresh Kumar
[J]. INTERNATIONAL JOURNAL OF AD HOC AND UBIQUITOUS COMPUTING, 2022, 41 (02) : 108 - 117
[29] Worst-Case Execution Time Analysis for Many-Core Architectures with NoC
Skalistis, Stefanos
Simalatsar, Alena
[J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, FORMATS 2016, 2016, 9884 : 211 - 227
[30] A new model checking approach for verifying agent communication protocols
Bentahar, Jamal
Moulin, Bernard
Meyer, John-Jules Ch.
[J]. 2006 CANADIAN CONFERENCE ON ELECTRICAL AND COMPUTER ENGINEERING, VOLS 1-5, 2006, : 1877 - +

← 1 2 3 4 5 →