AXI Formal Verification

A 10-module course formally verifying real-world AXI bus components from the open-source wb2axip library. Prove AXI4-Lite, Wishbone bridges, crossbars, and DMA engines correct.

Modules (10)

• Module 1 — Skid Buffer — 3 katas
• Module 2 — AXI-Lite Read — 3 katas
• Module 3 — AXI-Lite Write — 3 katas
• Module 4 — AXI to Wishbone Read — 3 katas
• Module 5 — AXI to Wishbone Write — 3 katas
• Module 6 — Address Decoder — 3 katas
• Module 7 — Compositional Crossbar — 3 katas
• Module 8 — AXI-Lite Firewall — 3 katas
• Module 9 — Master-Mode Verification — 3 katas
• Module 10 — Memcpy DMA Sign-Off — 3 katas

Every kata runs SymbiYosys in the browser: write the properties, run the proof, read the counterexample.