Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Probabilistic Verification for Modular Network-on-Chip Systems (extended version)

Nick Waddoups, Jonah Boe, Arnd Hartmanns, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty, Zhen Zhang

TL;DR

The work tackles reliable NoC design under PSN by delivering a modular, probabilistic verification framework built in the Modest language. It combines functional CTL verification with probabilistic PCTL/SMC analysis to quantify PSN-related risks across NoCs up to $8\times 8$, while preserving scalability via parallel composition and synchronized clocking. Key contributions include a reusable modular NoC model, rigorous correctness proofs for router-level behavior, and PSN characterizations that reveal routing- and topology-driven patterns, plus comparative validation against prior monolithic models. The approach enables early design-stage insights to mitigate PSN effects, guiding traffic patterns and routing choices to improve reliability in modern NoCs.

Abstract

Quantitative verification can provide deep insights into reliable Network-On-Chip (NoC) designs. It is critical to understanding and mitigating operational issues caused by power supply noise (PSN) early in the design process: fluctuations in network traffic in modern NoC designs cause dramatic variations in power delivery across the network, leading to unreliability and errors in data transfers. Further complicating these challenges, NoC designs vary widely in size, usage, and implementation. This case study paper presents a principled, systematic, and modular NoC modeling approach using the Modest language that closely reflects the standard hierarchical design approach in digital systems. Using the Modest Toolset, functional and quantitative correctness was established for several NoC models, all of which were instantiated from a generic modular router model. Specifically, this work verifies the functional correctness of a generic router, inter-router communication, and the entire NoC. Statistical model checking was used to verify PSN-related properties for NoCs of size up to 8x8.

Probabilistic Verification for Modular Network-on-Chip Systems (extended version)

TL;DR

The work tackles reliable NoC design under PSN by delivering a modular, probabilistic verification framework built in the Modest language. It combines functional CTL verification with probabilistic PCTL/SMC analysis to quantify PSN-related risks across NoCs up to , while preserving scalability via parallel composition and synchronized clocking. Key contributions include a reusable modular NoC model, rigorous correctness proofs for router-level behavior, and PSN characterizations that reveal routing- and topology-driven patterns, plus comparative validation against prior monolithic models. The approach enables early design-stage insights to mitigate PSN effects, guiding traffic patterns and routing choices to improve reliability in modern NoCs.

Abstract

Quantitative verification can provide deep insights into reliable Network-On-Chip (NoC) designs. It is critical to understanding and mitigating operational issues caused by power supply noise (PSN) early in the design process: fluctuations in network traffic in modern NoC designs cause dramatic variations in power delivery across the network, leading to unreliability and errors in data transfers. Further complicating these challenges, NoC designs vary widely in size, usage, and implementation. This case study paper presents a principled, systematic, and modular NoC modeling approach using the Modest language that closely reflects the standard hierarchical design approach in digital systems. Using the Modest Toolset, functional and quantitative correctness was established for several NoC models, all of which were instantiated from a generic modular router model. Specifically, this work verifies the functional correctness of a generic router, inter-router communication, and the entire NoC. Statistical model checking was used to verify PSN-related properties for NoCs of size up to 8x8.

Paper Structure

This paper contains 53 sections, 7 equations, 11 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Probabilistic Modeling Checking.
  4. NoC Verification.
  5. Probabilistic NoCs in Modest.
  6. Preliminaries
  7. NoC Architecture
  8. Routing Algorithm
  9. Router Arbitration
  10. Power Supply Noise (PSN)
  11. Statistical Model Checking (SMC)
  12. The Modest Toolset
  13. Rationale for Choosing Modest
  14. Modular Design of the Formal NoC Model
  15. NoC Construction using Parallel Composition
  16. ...and 38 more sections

Figures (11)

  • Figure 1: A ${2}\!\times\!{2}$ NoC architecture and an individual router
  • Figure 2: Adding Actions to Reduce Unnecessary State Space
  • Figure 3: Impact of Synchronizing Actions in a Parallel Composition of $n^2$ Routers
  • Figure 4: PSN for ${2}\!\times\!{2}$ Modular Model
  • Figure 5: Modular and Monolithic ${2}\!\times\!{2}$ NoC Resistive Noise Comparison
  • ...and 6 more figures