Probabilistic Verification for Modular Network-on-Chip Systems (extended version)
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917086525128704 |
|---|---|
| author | Waddoups, Nick Boe, Jonah Hartmanns, Arnd Basu, Prabal Roy, Sanghamitra Chakraborty, Koushik Zhang, Zhen |
| author_facet | Waddoups, Nick Boe, Jonah Hartmanns, Arnd Basu, Prabal Roy, Sanghamitra Chakraborty, Koushik Zhang, Zhen |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_13890 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Probabilistic Verification for Modular Network-on-Chip Systems (extended version) Waddoups, Nick Boe, Jonah Hartmanns, Arnd Basu, Prabal Roy, Sanghamitra Chakraborty, Koushik Zhang, Zhen Logic in Computer Science 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. |
| title | Probabilistic Verification for Modular Network-on-Chip Systems (extended version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2511.13890 |