Executable Formal Specification and Validation of NoC Communication Infrastructures

被引：0

作者：

Borrione, Dominique ^{[1
]}

Helmy, Amr ^{[1
]}

Pierre, Laurence ^{[1
]}

Schmaltz, Julien

机构：

[1] CNRS GrenobleINP UJF, TIMA Lab, Grenoble, France

来源：

SBCCI 2008: 21ST SYMPOSIUM ON INTEGRATED CIRCUITS AND SYSTEMS DESIGN, PROCEEDINGS | 2008年

关键词：

Verification; Theorem proving; Simulation;

D O I：

暂无

中图分类号：

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

学科分类号：

0812 ;

摘要：

We describe an enhanced generic model for Networks-on-Chip (NoCs), implemented in the executable logic of the ACL2 theorem prover. The model is meant for serving as a formal reference for the specification, validation, and simulation at the initial design phase. Instantiated on a specific NoC, the model may be used for formal proofs and for simulation. The methodology is illustrated on HERMES.

引用

页码：176 / 181

页数：6

共 13 条

[1] BORRIONE D, 2007, P IEEE INT C NOCS 07
[2] GEBREMICHAEL B, 2005, P CHARME 05 OCT
[3] GENKO N, 2005, P PARCO 2005
[4] Modeling layered distributed communication systems
Herzberg, D
Broy, M
[J]. FORMAL ASPECTS OF COMPUTING, 2005, 17 (01) : 1 - 18
[5] KARIM F, 2002, IEEE MICRO, V22
[6] KAUFMANN M, 2002, COMPUTER AIDED REASO
[7] Moore J. S., 1994, Formal Aspects of Computing, V6, P60, DOI 10.1007/BF01211081
[8] MORAES F, 2004, VLSI J, V38
[9] RAMAS JP, 2005, P PARCO 2005 MIN NOC
[10] Roychoudhury A, 2003, DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, PROCEEDINGS, P828

← 1 2 →