SystemVerilog Assertions

SVA Handshake Assertions Guide

Handshake assertions convert informal timing rules into executable properties. For ready/valid-style interfaces, the highest-value properties usually describe what must persist during backpressure, when transfers are allowed to occur and how reset disables or constrains the protocol.

Core design rules

• Sample protocol properties on the interface clock and make reset semantics explicit with disable iff or implication as appropriate.
• When VALID is high and READY is low, assert that VALID remains high until the transfer and that payload remains stable.
• Distinguish same-cycle implication (|->) from next-cycle implication (|=>); choosing the wrong one shifts the intended requirement.
• Prefer several small properties with clear failure messages over one giant property that is difficult to debug.

Implementation path

• Write a transfer definition and a stall definition before writing properties.
• Add a VALID-hold property, then a payload-stability property.
• Add response persistence or one-hot/ordering properties specific to the protocol.
• Run both passing and intentionally failing stimulus so you know the assertion can actually fire.

Verification checklist

• Hold READY low for multiple cycles while changing stimulus around the source.
• Deassert VALID illegally during a stall and confirm the property fails.
• Change payload illegally while stalled and confirm $stable catches it.
• Exercise reset near a pending transfer to confirm the property is neither over- nor under-disabled.

Useful RTL / verification pattern

property valid_holds_until_ready;
  @(posedge clk) disable iff (reset)
    valid && !ready |=> valid;
endproperty

property payload_stable_while_stalled;
  @(posedge clk) disable iff (reset)
    valid && !ready |=> $stable(data);
endproperty

Practice with executable problems

Turn it into a project