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.
|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|
|Publication status||Published - 2008|