Formally Verifying AXI Interfaces
summary
A compact property set for AXI and AXI-lite is implemented and run with SymbiYosys against many open-source and vendor demo cores, revealing concrete failures: dropped responses, stalled channels that hang until reset, and missing responses for mixed read/write requests. Examples include demonstration cores that give one response then drop the next, a GPIO core that needs six clocks per roundtrip, and a major vendor core with over six protocol violations; some issues are later fixed but several demos remain broken.
AI-written summary · about
chapters (25)
- 0:00Introduction
- 0:38What is AXI
- 1:06AXI E
- 2:20What is Formal Verification
- 3:38Overview
- 4:23Reset
- 4:40Stall
- 5:10Request
- 5:33Basic Properties
- 5:58The Problem
- 7:17Your Design
- 8:05Tiny TPU
- 8:23State Machine
- 8:38Wishbone
- 9:21Bus abort
- 9:50Protocol violations
- 10:13Scan mode toggle
- 11:03Cover traces
- 11:30Blinky
- 12:36AXI Demo
- 12:48AXI Light
- 13:25AXI 8 Example
- 14:01Why did I find so many broken cores
- 15:52Conclusion
- 17:15Adding more formal IP
related talks
46mIntroduction to Formal Verification with Symbiotic EDA Open Source Tools
18mMore than the Core Verifying RISC V SoCs
25mRISC-V System-level Certification from Verification Foundations
21mCombined Dynamic and Formal Verification Approach to Processor Verification
17mDemo: RISC-V AIA Expanding Interrupts: Applications, Implementation and Verification
16mCommercial Adoption of CORE-V Open-Source RISC-V Cores - Lessons Learned
23mCORE-V Verification Test Bench – Commercial Qualit...
12mRISC-V: Hardcore/Softcore Co-Simulation Environment with Cycle-Accurate Rollback