Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System

Riley Roberts; Benjamin Lewis; Arnd Hartmanns; Prabal Basu; Sanghamitra Roy; Koushik Chakraborty; Zhen Zhang

doi:10.1007/978-3-030-85248-1_16

Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System

Riley Roberts, Benjamin Lewis, Arnd Hartmanns, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty, Zhen Zhang

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

3 Citations (Scopus)

49 Downloads (Pure)

Abstract

Modern network-on-chip (NoC) systems face reliability issues due to process and environmental variations. The power supply noise (PSN) in the power delivery network of a NoC plays a key role in determining reliability. PSN leads to voltage droop, which can cause timing errors in the NoC. This paper makes a novel contribution towards formally analyzing PSN in NoC systems. We present a probabilistic model checking approach to analyze key features of PSN at the behavioral level in a 2×2 mesh NoC with a uniform random traffic load. To tackle state explosion, we apply incremental abstraction techniques, including a novel probabilistic choice abstraction, based on observations of NoC behavior. The Modest Toolset is used for probabilistic modeling and verification. Results are obtained for several flit injection patterns to reveal their impacts on PSN. Our analysis finds an optimal flit pattern generation with zero probability of PSN events and suggests spreading flits rather than releasing them in consecutive cycles in order to minimize PSN.

Original language	English
Title of host publication	Formal Methods for Industrial Critical Systems
Subtitle of host publication	26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings
Editors	Alberto Lluch-Lafuente, Anastasia Mavridou
Place of Publication	Cham
Publisher	Springer
Pages	232-248
Number of pages	17
ISBN (Electronic)	978-3-030-85248-1
ISBN (Print)	978-3-030-85247-4
DOIs	https://doi.org/10.1007/978-3-030-85248-1_16
Publication status	Published - 19 Aug 2021
Event	26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021 - Virtual Conference Duration: 24 Aug 2021 → 26 Aug 2021 Conference number: 26

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	12863
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021
Abbreviated title	FMICS 2021
City	Virtual Conference
Period	24/08/21 → 26/08/21

Access to Document

10.1007/978-3-030-85248-1_16

Roberts2021probabilisticFinal published version, 1.02 MBLicence: Taverne

Cite this

Roberts, R., Lewis, B., Hartmanns, A., Basu, P., Roy, S., Chakraborty, K., & Zhang, Z. (2021). Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System. In A. Lluch-Lafuente, & A. Mavridou (Eds.), Formal Methods for Industrial Critical Systems: 26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings (pp. 232-248). (Lecture Notes in Computer Science; Vol. 12863). Springer. https://doi.org/10.1007/978-3-030-85248-1_16

Roberts, Riley ; Lewis, Benjamin ; Hartmanns, Arnd et al. / Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System. Formal Methods for Industrial Critical Systems: 26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings. editor / Alberto Lluch-Lafuente ; Anastasia Mavridou. Cham : Springer, 2021. pp. 232-248 (Lecture Notes in Computer Science).

@inproceedings{59d4dd33c31a425399aa035d6b74f4f3,

title = "Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System",

abstract = "Modern network-on-chip (NoC) systems face reliability issues due to process and environmental variations. The power supply noise (PSN) in the power delivery network of a NoC plays a key role in determining reliability. PSN leads to voltage droop, which can cause timing errors in the NoC. This paper makes a novel contribution towards formally analyzing PSN in NoC systems. We present a probabilistic model checking approach to analyze key features of PSN at the behavioral level in a 2×2 mesh NoC with a uniform random traffic load. To tackle state explosion, we apply incremental abstraction techniques, including a novel probabilistic choice abstraction, based on observations of NoC behavior. The Modest Toolset is used for probabilistic modeling and verification. Results are obtained for several flit injection patterns to reveal their impacts on PSN. Our analysis finds an optimal flit pattern generation with zero probability of PSN events and suggests spreading flits rather than releasing them in consecutive cycles in order to minimize PSN.",

author = "Riley Roberts and Benjamin Lewis and Arnd Hartmanns and Prabal Basu and Sanghamitra Roy and Koushik Chakraborty and Zhen Zhang",

year = "2021",

month = aug,

day = "19",

doi = "10.1007/978-3-030-85248-1_16",

language = "English",

isbn = "978-3-030-85247-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "232--248",

editor = "Alberto Lluch-Lafuente and Anastasia Mavridou",

booktitle = "Formal Methods for Industrial Critical Systems",

address = "Germany",

note = "26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021, FMICS 2021 ; Conference date: 24-08-2021 Through 26-08-2021",

}

Roberts, R, Lewis, B, Hartmanns, A, Basu, P, Roy, S, Chakraborty, K & Zhang, Z 2021, Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System. in A Lluch-Lafuente & A Mavridou (eds), Formal Methods for Industrial Critical Systems: 26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12863, Springer, Cham, pp. 232-248, 26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021, Virtual Conference, 24/08/21. https://doi.org/10.1007/978-3-030-85248-1_16

Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System. / Roberts, Riley; Lewis, Benjamin; Hartmanns, Arnd et al.
Formal Methods for Industrial Critical Systems: 26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings. ed. / Alberto Lluch-Lafuente; Anastasia Mavridou. Cham: Springer, 2021. p. 232-248 (Lecture Notes in Computer Science; Vol. 12863).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System

AU - Roberts, Riley

AU - Lewis, Benjamin

AU - Hartmanns, Arnd

AU - Basu, Prabal

AU - Roy, Sanghamitra

AU - Chakraborty, Koushik

AU - Zhang, Zhen

N1 - Conference code: 26

PY - 2021/8/19

Y1 - 2021/8/19

N2 - Modern network-on-chip (NoC) systems face reliability issues due to process and environmental variations. The power supply noise (PSN) in the power delivery network of a NoC plays a key role in determining reliability. PSN leads to voltage droop, which can cause timing errors in the NoC. This paper makes a novel contribution towards formally analyzing PSN in NoC systems. We present a probabilistic model checking approach to analyze key features of PSN at the behavioral level in a 2×2 mesh NoC with a uniform random traffic load. To tackle state explosion, we apply incremental abstraction techniques, including a novel probabilistic choice abstraction, based on observations of NoC behavior. The Modest Toolset is used for probabilistic modeling and verification. Results are obtained for several flit injection patterns to reveal their impacts on PSN. Our analysis finds an optimal flit pattern generation with zero probability of PSN events and suggests spreading flits rather than releasing them in consecutive cycles in order to minimize PSN.

AB - Modern network-on-chip (NoC) systems face reliability issues due to process and environmental variations. The power supply noise (PSN) in the power delivery network of a NoC plays a key role in determining reliability. PSN leads to voltage droop, which can cause timing errors in the NoC. This paper makes a novel contribution towards formally analyzing PSN in NoC systems. We present a probabilistic model checking approach to analyze key features of PSN at the behavioral level in a 2×2 mesh NoC with a uniform random traffic load. To tackle state explosion, we apply incremental abstraction techniques, including a novel probabilistic choice abstraction, based on observations of NoC behavior. The Modest Toolset is used for probabilistic modeling and verification. Results are obtained for several flit injection patterns to reveal their impacts on PSN. Our analysis finds an optimal flit pattern generation with zero probability of PSN events and suggests spreading flits rather than releasing them in consecutive cycles in order to minimize PSN.

U2 - 10.1007/978-3-030-85248-1_16

DO - 10.1007/978-3-030-85248-1_16

M3 - Conference contribution

SN - 978-3-030-85247-4

T3 - Lecture Notes in Computer Science

SP - 232

EP - 248

BT - Formal Methods for Industrial Critical Systems

A2 - Lluch-Lafuente, Alberto

A2 - Mavridou, Anastasia

PB - Springer

CY - Cham

T2 - 26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021

Y2 - 24 August 2021 through 26 August 2021

ER -

Roberts R, Lewis B, Hartmanns A, Basu P, Roy S, Chakraborty K et al. Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System. In Lluch-Lafuente A, Mavridou A, editors, Formal Methods for Industrial Critical Systems: 26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings. Cham: Springer. 2021. p. 232-248. (Lecture Notes in Computer Science). doi: 10.1007/978-3-030-85248-1_16

Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this