Probabilistic Verification for Modular Network-on-Chip Systems

on YouTube ↗26m

" summary

A modular NoC model written in Modest produces DTMCs and uses CTL model checking plus statistical model checking to bound power-supply-noise events up to an 8x8 mesh, verifying functional properties like no buffer overflow and single-driver channels. Synchronous labels eliminate interleavings, turning a run that previously exhausted 126 GB into one that completes in about 10 minutes with ~10× less memory; a modular 2x2 now matches the original monolithic results.

AI-written summary · about

" chapters (14)

1. 0:00Probabilistic verification for NoCs
2. 1:02Network-on-chip architectures needed
3. 2:46NoCs mesh topologies and routing
4. 6:15Power supply noise in NoCs
5. 8:01Modeling power supply noise
6. 10:05Modest for probabilistic modeling
7. 13:39Modular NoC model in Modest
8. 16:09Generating packets and behavior
9. 17:32Synchronizing clock cycles
10. 18:34Verifying correctness with CTL
11. 20:21Fixing synchronization issues
12. 21:45Results for 3x3 4x4 8x8 NoCs
13. 22:50Future work on traffic patterns
14. 24:24Q&A