Executable formal specification and validation of NoC communication infrastructures
D. Borrione, Amr S. Helmy, Laurence Pierre, Julien Schmaltz · 2008
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.