AXI-Lite Protocol Assertions
Add protocol properties that catch payload instability and missing responses.
Task
Write SVA properties requiring AW payload stability while stalled, W payload stability while stalled, and an eventual B response after an accepted write.
Examples
- AWVALID && !AWREADY keeps AWADDR stable.
- WVALID && !WREADY keeps WDATA/WSTRB stable.
Constraints
- Use `property`/`assert property`.
- Check both address and data stall stability.
- Include a bounded write-response property.
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, AXI4-Lite, protocol checking
Open AXI-Lite 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.