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

D. Borrione; A. Helmy; L. Pierre; J. Schmaltz

doi:10.1109/NOCS.2007.1

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

D. Borrione, A. Helmy, L. Pierre, J. Schmaltz

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

27 Citations (Scopus)

Abstract

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 NoC?s 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.

Original language	English
Title of host publication	First International Symposium on Networks-on-Chips (NOCS '07, Princeton NJ, USA, May 7-9, 2007. Proceedings)
Publisher	IEEE Computer Society
Pages	127-136
ISBN (Print)	978-0-7695-2773-4
DOIs	https://doi.org/10.1109/NOCS.2007.1
Publication status	Published - 2007

Access to Document

10.1109/NOCS.2007.1

Cite this

@inproceedings{22d7a2a2726e4b01b0560ab7b0bd6ab0,

title = "A generic model for formally verifying NoC communication architectures: A case study",

abstract = "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 NoC?s 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.",

author = "D. Borrione and A. Helmy and L. Pierre and J. Schmaltz",

year = "2007",

doi = "10.1109/NOCS.2007.1",

language = "English",

isbn = "978-0-7695-2773-4",

pages = "127--136",

booktitle = "First International Symposium on Networks-on-Chips (NOCS '07, Princeton NJ, USA, May 7-9, 2007. Proceedings)",

publisher = "IEEE Computer Society",

address = "United States",

}

A generic model for formally verifying NoC communication architectures: A case study. / Borrione, D.; Helmy, A.; Pierre, L. et al.
First International Symposium on Networks-on-Chips (NOCS '07, Princeton NJ, USA, May 7-9, 2007. Proceedings). IEEE Computer Society, 2007. p. 127-136.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Borrione, D.

AU - Helmy, A.

AU - Pierre, L.

AU - Schmaltz, J.

PY - 2007

Y1 - 2007

N2 - 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 NoC?s 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.

AB - 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 NoC?s 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.

UR - http://doi.ieeecomputersociety.org/10.1109/NOCS.2007.1

U2 - 10.1109/NOCS.2007.1

DO - 10.1109/NOCS.2007.1

M3 - Conference contribution

SN - 978-0-7695-2773-4

SP - 127

EP - 136

BT - First International Symposium on Networks-on-Chips (NOCS '07, Princeton NJ, USA, May 7-9, 2007. Proceedings)

PB - IEEE Computer Society

ER -

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

Abstract

Access to Document

Other files and links

Fingerprint

Cite this