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

TL;DR

This paper introduces a modular modeling approach for Network-On-Chip systems using the Modest language, enabling systematic verification of functional correctness and power supply noise effects in various NoC configurations.

Contribution

It presents a novel modular modeling framework with the Modest language, facilitating systematic verification of correctness and reliability in NoC designs of different sizes.

Findings

Verified functional correctness of generic routers and entire NoC models

Applied statistical model checking to assess power supply noise effects

Demonstrated scalability up to 8x8 NoC configurations

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.