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


    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
    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

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

  • Cite this

    Lewis, B., Hartmanns, A., Basu, P., Shridevi, R. J., Chakraborty, K., Roy, S., & Zhang, Z. (2019). Probabilistic Verification for Reliable Network-on-Chip System Design. In K. G. Larsen, & T. Willemse (Eds.), Formal Methods for Industrial Critical Systems (pp. 110-126). (Lecture Notes in Computer Science; Vol. 11687). Cham: Springer.