Probabilistic Verification for Reliable Network-on-Chip System Design

Benjamin Lewis*, Arnd Hartmanns, Prabal Basu, Rajesh Jayashankara Shridevi, Koushik Chakraborty, Sanghamitra Roy, Zhen Zhang

*Corresponding author for this work

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

1 Citation (Scopus)
10 Downloads (Pure)


The design of modern network-on-chip (NoC) systems faces reliability challenges due to process and environmental variations. Peak power supply noise (PSN) in the power delivery network of a NoC device plays a critical role in determining reliable operations: PSN typically leads to voltage droop, which can cause timing errors in the NoC router pipelines. Existing simulation-based approaches cannot provide rigorous, worst-case reliability guarantees on the probabilistic behaviors of PSN. To address this problem, this paper takes a significant step in formally analyzing PSN in modern NoCs. Specifically, we present a probabilistic model checking approach for the rigorous characterization of PSN for a generic central router of a large mesh-NoC system, under the Round Robin scheduling mechanism with a uniform random network traffic load. Defining features for PSN are extracted at the behavioral level to facilitate property formulation. Several abstract models have been derived for the central router’s concrete model based on the observations of its arbiter’s conflict resolution behavior. Probabilistic modeling and verification are performed using the Modest Toolset. Results show significant scalability of our abstract models, and reveal key PSN characteristics that are indicative of NoC design and optimization.

Original languageEnglish
Title of host publicationFormal Methods for Industrial Critical Systems
Subtitle of host publication24th International Conference, FMICS 2019, Amsterdam, The Netherlands, August 30–31, 2019, Proceedings
EditorsKim Guldstrand Larsen, Tim Willemse
Place of PublicationCham
Number of pages17
ISBN (Electronic)978-3-030-27008-7
ISBN (Print)978-3-030-27007-0
Publication statusPublished - Aug 2019
Event24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019 - Amsterdam Science Park, Amsterdam, Netherlands
Duration: 30 Aug 201931 Aug 2019
Conference number: 24

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019
Abbreviated titleFMICS 2019
Internet address


  • Network-on-chip
  • Power supply noise
  • Probabilistic model checking
  • Reliability analysis


Dive into the research topics of 'Probabilistic Verification for Reliable Network-on-Chip System Design'. Together they form a unique fingerprint.

Cite this