AXI Crossbar Protocol Assertions
Check grant exclusivity and stalled payload stability in the crossbar.
Task
Assert grant is onehot0 and assert AWADDR remains stable while AWVALID is high and AWREADY is low.
Examples
- Implement the required behavior and preserve it under the stated interface/control conditions.
Constraints
- Keep the implementation deterministic and consistent with the interface contract described in the task.
What this problem is testing
SVA questions test temporal reasoning: exactly when signals are sampled, overlapped versus non-overlapped implication, reset disabling, and whether an assertion can pass vacuously.
Interview habit: before coding, state reset behavior, the state that must be stored, and the conditions that update each output.
Verification plan
- Write one passing trace and one deliberately failing trace.
- Check the exact cycle where the antecedent becomes true and where the consequent starts.
- Exercise reset while the property is active.
- Use cover or directed stimulus when useful to prove the antecedent can actually occur.
Common mistakes
- Choosing |-> versus |=> by habit.
- Forgetting disable iff or mishandling reset.
- Allowing vacuous success because the antecedent never occurs.
- Using unbounded eventuality when the protocol has a finite response requirement.
Interview follow-up questions
- Would overlapped or non-overlapped implication be correct here, and why?
- How would you detect or avoid vacuous success?
Concepts to review
SVA, AXI, crossbar
Open AXI Crossbar Protocol Assertions in the HDLForge interactive editor.
Related problems
- Valid Must Eventually Handshake — Medium
- Reset Clears State — Easy
- Payload Stable While Stalled — Medium
- One-Hot Grant Assertion — Easy
- No FIFO Overflow Assertion — Easy
Explore the SystemVerilog Assertions (SVA) Practice hub.