Scaling Up Livelock Verification for Network-on-Chip Routing Algorithms
summary
Refutation-based simulation scales verification from refutation-based simulation on small meshes to an IVy-checked model up to 15x15, implemented with a C++ simulator and checked with IVy and ABC; two novel livelock patterns appear on 3x3, removed by iteratively modifying routing rules. A zone-based abstraction collapses symmetric nodes so a positional-zone model proves absence of cyclical direction changes of length seven or more on arbitrarily large 2D meshes, yielding a livelock-free fault-tolerant routing algorithm that tolerates zero or one link fault and many two-fault cases.
AI-written summary · about
chapters (18)
- 0:00Intro
- 0:31NetworkonChip
- 1:02Contributions
- 1:33Verification Tools
- 1:55Network on Chip
- 4:37Definitions
- 6:25Example
- 6:49Simulation Approach
- 8:10Simulation Results
- 8:33First Invariant
- 8:50Second Invariant
- 9:10Third Invariant
- 9:24Fourth Invariant
- 10:08Livelock Removal
- 11:45ZoneBased Network
- 13:50Abstract Move
- 19:12Conclusion
- 19:58QA
related talks
21mEvaluating Chiplet-based Large-Scale Interconnection Networks via Cycle-Accurate...
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
25mProperty-agnostic base case extension for scalable verification of distributed systems
54mReduction theorems for effective parameterized verification of round- based distributed algorithms
38mThe Verification of a Distributed System
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
20mAn Automated Scalable RISC-V Cache Coherency Verification Project
28mReasoning about Distributed Reconfigurable Systems