Probabilistic Verification for Reliable Network-on-Chip System Design

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

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

Abstract

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
PublisherSpringer
Pages110-126
Number of pages17
ISBN (Electronic)978-3-030-27008-7
ISBN (Print)978-3-030-27007-0
DOIs
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
https://fmics2019.fsa.win.tue.nl/

Publication series

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

Conference

Conference24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019
Abbreviated titleFMICS 2019
CountryNetherlands
CityAmsterdam
Period30/08/1931/08/19
Internet address

Fingerprint

System Design
Systems analysis
Router
Routers
Probabilistic Modeling
Mesh Networks
Conflict Resolution
Random Networks
Model checking
Network Traffic
Probabilistic Model
Model Checking
Scalability
Timing
Pipelines
Scheduling
Voltage
Network on chip
Network-on-chip
Face

Keywords

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

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: 24th International Conference, FMICS 2019, Amsterdam, The Netherlands, August 30–31, 2019, Proceedings (pp. 110-126). (Lecture Notes in Computer Science; Vol. 11687). Cham: Springer. https://doi.org/10.1007/978-3-030-27008-7_7
Lewis, Benjamin ; Hartmanns, Arnd ; Basu, Prabal ; Shridevi, Rajesh Jayashankara ; Chakraborty, Koushik ; Roy, Sanghamitra ; Zhang, Zhen. / Probabilistic Verification for Reliable Network-on-Chip System Design. Formal Methods for Industrial Critical Systems: 24th International Conference, FMICS 2019, Amsterdam, The Netherlands, August 30–31, 2019, Proceedings. editor / Kim Guldstrand Larsen ; Tim Willemse. Cham : Springer, 2019. pp. 110-126 (Lecture Notes in Computer Science).
@inproceedings{5a7da8787880496f9c91865bd92575f1,
title = "Probabilistic Verification for Reliable Network-on-Chip System Design",
abstract = "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.",
keywords = "Network-on-chip, Power supply noise, Probabilistic model checking, Reliability analysis",
author = "Benjamin Lewis and Arnd Hartmanns and Prabal Basu and Shridevi, {Rajesh Jayashankara} and Koushik Chakraborty and Sanghamitra Roy and Zhen Zhang",
year = "2019",
month = "8",
doi = "10.1007/978-3-030-27008-7_7",
language = "English",
isbn = "978-3-030-27007-0",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "110--126",
editor = "Larsen, {Kim Guldstrand} and Tim Willemse",
booktitle = "Formal Methods for Industrial Critical Systems",

}

Lewis, B, Hartmanns, A, Basu, P, Shridevi, RJ, Chakraborty, K, Roy, S & Zhang, Z 2019, Probabilistic Verification for Reliable Network-on-Chip System Design. in KG Larsen & T Willemse (eds), Formal Methods for Industrial Critical Systems: 24th International Conference, FMICS 2019, Amsterdam, The Netherlands, August 30–31, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11687, Springer, Cham, pp. 110-126, 24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019, Amsterdam, Netherlands, 30/08/19. https://doi.org/10.1007/978-3-030-27008-7_7

Probabilistic Verification for Reliable Network-on-Chip System Design. / Lewis, Benjamin; Hartmanns, Arnd; Basu, Prabal; Shridevi, Rajesh Jayashankara; Chakraborty, Koushik; Roy, Sanghamitra; Zhang, Zhen.

Formal Methods for Industrial Critical Systems: 24th International Conference, FMICS 2019, Amsterdam, The Netherlands, August 30–31, 2019, Proceedings. ed. / Kim Guldstrand Larsen; Tim Willemse. Cham : Springer, 2019. p. 110-126 (Lecture Notes in Computer Science; Vol. 11687).

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

TY - GEN

T1 - Probabilistic Verification for Reliable Network-on-Chip System Design

AU - Lewis, Benjamin

AU - Hartmanns, Arnd

AU - Basu, Prabal

AU - Shridevi, Rajesh Jayashankara

AU - Chakraborty, Koushik

AU - Roy, Sanghamitra

AU - Zhang, Zhen

PY - 2019/8

Y1 - 2019/8

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

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

KW - Network-on-chip

KW - Power supply noise

KW - Probabilistic model checking

KW - Reliability analysis

UR - http://www.scopus.com/inward/record.url?scp=85072872821&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-27008-7_7

DO - 10.1007/978-3-030-27008-7_7

M3 - Conference contribution

SN - 978-3-030-27007-0

T3 - Lecture Notes in Computer Science

SP - 110

EP - 126

BT - Formal Methods for Industrial Critical Systems

A2 - Larsen, Kim Guldstrand

A2 - Willemse, Tim

PB - Springer

CY - Cham

ER -

Lewis B, Hartmanns A, Basu P, Shridevi RJ, Chakraborty K, Roy S et al. Probabilistic Verification for Reliable Network-on-Chip System Design. In Larsen KG, Willemse T, editors, Formal Methods for Industrial Critical Systems: 24th International Conference, FMICS 2019, Amsterdam, The Netherlands, August 30–31, 2019, Proceedings. Cham: Springer. 2019. p. 110-126. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-27008-7_7