Easy formal specification and validation of unbounded networks-on-chips architectures

F. Verbeek, J. Schmaltz

Research output: Contribution to journalArticleAcademicpeer-review

9 Citations (Scopus)


This article presents a formal specification and validation environment to prove safety and liveness properties of parametric -- unbounded -- NoCs architectures described at a high-level of abstraction. The environment improves the GeNoC approach with two new theorems, proving evacuation and starvation freedom. The application of the validation methodology is illustrated on a HERMES NoC with adaptive west-first routing and wormhole switching. This case study illustrates the strong compositional aspect of the GeNoC environment. The complete specification of this HERMES instance, together with the proof that the specification is deadlock-free, starvation free, and all messages eventually leave the network at their correct destination, could be achieved in about a week. Approximately 86% of this proof is automatically derived from the GeNoC model.
Original languageEnglish
Pages (from-to)1/1-28
Number of pages28
JournalACM Transactions on Design Automation of Electronic Systems
Issue number1
Publication statusPublished - 2012
Externally publishedYes


Dive into the research topics of 'Easy formal specification and validation of unbounded networks-on-chips architectures'. Together they form a unique fingerprint.

Cite this