Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System
The work
| Authors | Riley Roberts; Benjamin Lewis; Arnd Hartmanns; Prabal Basu; Sanghamitra Roy; Koushik Chakraborty; Zhen Zhang |
|---|---|
| Editors | |
| Type | misc |
| Year | 2021 |
| Citekey | roberts2021probabilistic |
Where it appeared
| Published in | Formal Methods for Industrial Critical Systems (FMICS 2021) |
|---|---|
| Series | Lecture Notes in Computer Science |
| Pages | 232--248 |
Identifiers
| arXiv | 2108.13148 from its landing_page_url |
|---|---|
| DOI | 10.1007/978-3-030-85248-1_16 |
Access
| Landing page | https://arxiv.org/abs/2108.13148 |
|---|
Related
| Distinct from | lewis2019probabilistic |
|---|---|
| Superseded by | waddoups2025probabilistic |
| Supersedes | lewis2019probabilistic |
From bibtex.
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 observe the PSN in a generic 2x2 mesh NoC with a uniform random traffic load. Key features of PSN are measured at the behavioral level. 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.
A copy is held
pdf, 283.8 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-17 22:07 UTC |
| Approved by | a person 2026-10-05 21:24 UTC |
Filed under
Cite it as
@misc{roberts2021probabilistic,
title = {Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System},
author = {Riley Roberts and Benjamin Lewis and Arnd Hartmanns and Prabal Basu and Sanghamitra Roy and Koushik Chakraborty and Zhen Zhang},
year = {2021},
journal = {Formal Methods for Industrial Critical Systems (FMICS 2021)},
series = {Lecture Notes in Computer Science},
pages = {232--248},
doi = {10.1007/978-3-030-85248-1_16},
}
This record lives at https://refs.drheap.org/roberts2021probabilistic/ and will keep doing so.