Arbiter Mutual Exclusion
Prove that an arbiter never grants more than one requester simultaneously.
Task
Assert $onehot0(grant) on every active cycle and assert grant implies a corresponding request.
Examples
- Implement the required behavior and preserve it under the stated control conditions.
Constraints
- Use synthesizable SystemVerilog unless this stage is verification-only.
Concepts to review
formal, arbiter, onehot
Open HDLForge to solve this problem in the interactive editor.
Related problems
- 4-Request Priority Arbiter — Medium
- One-Hot Grant Assertion — Easy
- Formal Reset Assumptions — Medium
- FIFO Safety Properties — Hard
- FIFO Ordering Property — Hard