Executable formal specification and validation of NoC communication infrastructures

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

doi:10.1145/1404371.1404421

Executable formal specification and validation of NoC communication infrastructures

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

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

12 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	Proceedings of the 21st Annual Symposium on Integrated Circuits and Systems Design (SBCCI '08, Gramado, Brazil, September 1-4, 2008)
Editors	M. Lubaszewski, M. Renovell, R.K. Gupta
Place of Publication	New York NY
Publisher	Association for Computing Machinery, Inc.
Pages	176-181
ISBN (Print)	978-1-60558-231-3
DOIs	https://doi.org/10.1145/1404371.1404421
Publication status	Published - 2008

Access to Document

10.1145/1404371.1404421

Cite this

Borrione, D., Helmy, A., Pierre, L., & Schmaltz, J. (2008). Executable formal specification and validation of NoC communication infrastructures. In M. Lubaszewski, M. Renovell, & R. K. Gupta (Eds.), Proceedings of the 21st Annual Symposium on Integrated Circuits and Systems Design (SBCCI '08, Gramado, Brazil, September 1-4, 2008) (pp. 176-181). Association for Computing Machinery, Inc.. https://doi.org/10.1145/1404371.1404421

Borrione, D. ; Helmy, A. ; Pierre, L. et al. / Executable formal specification and validation of NoC communication infrastructures. Proceedings of the 21st Annual Symposium on Integrated Circuits and Systems Design (SBCCI '08, Gramado, Brazil, September 1-4, 2008). editor / M. Lubaszewski ; M. Renovell ; R.K. Gupta. New York NY : Association for Computing Machinery, Inc., 2008. pp. 176-181

@inproceedings{5aa51593510b4ec3896aac24227f9c0a,

title = "Executable formal specification and validation of NoC communication infrastructures",

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

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

year = "2008",

doi = "10.1145/1404371.1404421",

language = "English",

isbn = "978-1-60558-231-3",

pages = "176--181",

editor = "M. Lubaszewski and M. Renovell and R.K. Gupta",

booktitle = "Proceedings of the 21st Annual Symposium on Integrated Circuits and Systems Design (SBCCI '08, Gramado, Brazil, September 1-4, 2008)",

publisher = "Association for Computing Machinery, Inc.",

address = "United States",

}

Borrione, D, Helmy, A, Pierre, L & Schmaltz, J 2008, Executable formal specification and validation of NoC communication infrastructures. in M Lubaszewski, M Renovell & RK Gupta (eds), Proceedings of the 21st Annual Symposium on Integrated Circuits and Systems Design (SBCCI '08, Gramado, Brazil, September 1-4, 2008). Association for Computing Machinery, Inc., New York NY, pp. 176-181. https://doi.org/10.1145/1404371.1404421

Executable formal specification and validation of NoC communication infrastructures. / Borrione, D.; Helmy, A.; Pierre, L. et al.
Proceedings of the 21st Annual Symposium on Integrated Circuits and Systems Design (SBCCI '08, Gramado, Brazil, September 1-4, 2008). ed. / M. Lubaszewski; M. Renovell; R.K. Gupta. New York NY: Association for Computing Machinery, Inc., 2008. p. 176-181.

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

TY - GEN

T1 - Executable formal specification and validation of NoC communication infrastructures

AU - Borrione, D.

AU - Helmy, A.

AU - Pierre, L.

AU - Schmaltz, J.

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

UR - http://doi.acm.org/10.1145/1404371.1404421

U2 - 10.1145/1404371.1404421

DO - 10.1145/1404371.1404421

M3 - Conference contribution

SN - 978-1-60558-231-3

SP - 176

EP - 181

BT - Proceedings of the 21st Annual Symposium on Integrated Circuits and Systems Design (SBCCI '08, Gramado, Brazil, September 1-4, 2008)

A2 - Lubaszewski, M.

A2 - Renovell, M.

A2 - Gupta, R.K.

PB - Association for Computing Machinery, Inc.

CY - New York NY

ER -

Borrione D, Helmy A, Pierre L, Schmaltz J. Executable formal specification and validation of NoC communication infrastructures. In Lubaszewski M, Renovell M, Gupta RK, editors, Proceedings of the 21st Annual Symposium on Integrated Circuits and Systems Design (SBCCI '08, Gramado, Brazil, September 1-4, 2008). New York NY: Association for Computing Machinery, Inc. 2008. p. 176-181 doi: 10.1145/1404371.1404421

Executable formal specification and validation of NoC communication infrastructures

Abstract

Access to Document

Other files and links

Fingerprint

Cite this