Probabilistic Verification for Modular Network-on-Chip Systems (extended version)
By: Nick Waddoups , Jonah Boe , Arnd Hartmanns and more
Potential Business Impact:
Finds errors in computer chips caused by power.
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.
Similar Papers
Rigorous Evaluation of Microarchitectural Side-Channels with Statistical Model Checking
Cryptography and Security
Finds hidden computer flaws with math.
Demystifying FPGA Hard NoC Performance
Hardware Architecture
Makes computer chips faster and use less power.
Self-correcting High-speed Opto-electronic Probabilistic Computer
Quantum Physics
Makes computers solve hard problems much faster.