Towards a formally verified network-on-chip

T. Broek, van den, J. Schmaltz

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

6 Citations (Scopus)


Multi-Processor Systems-on-Chip (MPSoC) designs are constructed by assembling pre-designed parameterized components. Communications are crucial to their overall functionality and performance. Formal verification methods have been intensively applied to processing elements, e.g., microprocessors. Very little work has been done with respect to communication modules. We present the formal specification of a packet switched NoC and its proven refinement. At the specification level, routing decisions are computed at once before packets get injected in the network. In the implementation, routing decisions are distributed over each individual node. We prove that the implementation behaves according to its specification for a 2D-mesh NoC. All models and proofs have been checked using the ACL2 theorem proving system. To the best of our knowledge, this work constitutes the first cross-layer verification of on-chip communication networks.
Original languageEnglish
Title of host publicationProceedings of 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD '09, Austin TX, USA, November 15-18, 2009)
Place of PublicationPiscataway
PublisherInstitute of Electrical and Electronics Engineers
ISBN (Print)978-1-4244-4966-8
Publication statusPublished - 2009
Externally publishedYes


Dive into the research topics of 'Towards a formally verified network-on-chip'. Together they form a unique fingerprint.

Cite this