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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

27 Citaten (Scopus)

Samenvatting

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.

Originele taal-2	Engels
Titel	First International Symposium on Networks-on-Chips (NOCS '07, Princeton NJ, USA, May 7-9, 2007. Proceedings)
Uitgeverij	IEEE Computer Society
Pagina's	127-136
ISBN van geprinte versie	978-0-7695-2773-4
DOI's	https://doi.org/10.1109/NOCS.2007.1
Status	Gepubliceerd - 2007

Toegang tot document

10.1109/NOCS.2007.1

Andere bestanden en links

Full text

Citeer dit

@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. blz. 127-136.

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › 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

Samenvatting

Toegang tot document

Andere bestanden en links

Vingerafdruk

Citeer dit