Module 8 — Liveness and Fairness

Safety says nothing bad happens; liveness says something good eventually does. Express bounded liveness, prove a round-robin arbiter starvation-free, and state the fairness it rests on.

Katas in this module (3)

• Kata 8.1 — The Starved Requester
• Kata 8.2 — The Round-Robin That Doesn't Starve
• Kata 8.3 — Deadlock-Free Under Fairness

Part of Hardware Formal Verification on formal.org.