Valid/Ready Handshake Assertions

The contract

The valid/ready handshake is the backbone of AXI, AXI-Stream, and most modern on-chip interfaces. The producer asserts valid with payload; the consumer asserts ready when it can accept; the transfer happens on every cycle where both are high at the clock edge. The whole protocol hangs on one discipline: once valid is asserted, the producer has made an offer it cannot retract or alter until ready accepts it. Every rule below enforces a facet of that promise.

Handshake anatomy: transfer = valid && ready at the edge

  tick    :   1    2    3    4    5    6    7
  valid   :   0    1    1    1    0    1    1
  ready   :   1    0    0    1    1    1    1
  data    :   -    D0   D0   D0   -    D1   D2
                   └────────┘                    valid waits, data held
  transfer:   .    .    .    T1   .    T2   T3
                             ^         ^    ^
  T1: D0 accepted after 2 stall cycles
  T2,T3: back-to-back transfers (ready already high) — legal and
         the throughput case your cover points must prove happened

The canonical ruleset

1. Stability: once valid && !ready, valid must remain high next cycle.

2. Payload hold: while valid && !ready, data/strb/last must be stable.

3. X-safety: when valid is high, payload signals contain no X/Z.

4. No retraction: valid may only drop in the cycle after a transfer.

5. Liveness (bounded for simulation): an offered transfer is eventually accepted.

6. Dependency direction: valid must not wait for ready (note: only partially checkable).

Complete assertion module

module vr_checker #(
  parameter int  DW          = 32,
  parameter int  MAX_STALL   = 64   // bounded-liveness window
)(
  input logic           clk,
  input logic           rst_n,
  input logic           valid,
  input logic           ready,
  input logic [DW-1:0]  data,
  input logic           last
);
  // R1+R4: valid holds until accepted (covers retraction too:
  // if valid && !ready this cycle, valid must still be high next)
  a_valid_stable: assert property (@(posedge clk) disable iff (!rst_n)
    (valid && !ready) |-> ##1 valid)
    else $error("valid retracted before ready");

  // R2: payload frozen while the offer is pending
  a_payload_stable: assert property (@(posedge clk) disable iff (!rst_n)
    (valid && !ready) |-> ##1 ($stable(data) && $stable(last)))
    else $error("payload changed during stall");

  // R3: no X on payload while it is being offered
  a_no_x: assert property (@(posedge clk) disable iff (!rst_n)
    valid |-> (!$isunknown(data) && !$isunknown(last)))
    else $error("X on payload while valid");

  // R5: bounded liveness — accepted within MAX_STALL cycles
  a_accepted: assert property (@(posedge clk) disable iff (!rst_n)
    valid |-> ##[0:MAX_STALL] ready)
    else $error("transfer not accepted within %0d cycles", MAX_STALL);

  // Cover the scenarios that prove the checker saw real traffic
  c_b2b:   cover property (@(posedge clk)
    (valid && ready) ##1 (valid && ready));          // back-to-back
  c_stall: cover property (@(posedge clk)
    (valid && !ready) [*3] ##1 (valid && ready));    // 3-cycle stall
endmodule

Rule R1/R2 violation trace

  tick    :   1    2    3    4
  valid   :   0    1    0    1     ← drops at 3 with no transfer at 2
  ready   :   0    0    0    1
  data    :   -    D0   -    D9

  a_valid_stable attempt at tick 2: valid&&!ready → obligation:
  valid at tick 3 == 1. Sampled valid at 3 is 0 → FAIL at tick 3.
  This is RETRACTION — the producer withdrew an un-accepted offer.

  Payload-change variant: valid stays high but data mutates D0→D9
  while stalled → a_payload_stable fails: $stable(data) is false.

The dependency rule — what is actually checkable

AXI's famous deadlock rule says the producer must not wait for ready before asserting valid (the consumer may wait for valid before ready). This is a rule about the internal logic of the producer — a combinational dependency — and a black-box assertion watching only the two wires cannot prove its absence: a producer that waits for ready produces waveforms that are also legal under correct behavior. What you can do: detect the deadlock symptom (both sides waiting forever) with the bounded-liveness rule, and cover the case where valid rises while ready is low — if that cover never hits across a regression, your stimulus never disproved the dependency, which is a coverage hole worth flagging.

// Cannot assert "valid does not depend on ready" from outside.
// CAN cover that valid was observed leading ready:
c_valid_first: cover property (@(posedge clk)
  $rose(valid) && !ready);

// And catch the deadlock symptom with a strict bound:
a_no_deadlock: assert property (@(posedge clk) disable iff (!rst_n)
  $rose(valid) |-> ##[0:1024] ready);

Liveness: unbounded vs bounded

The textbook liveness form is valid |-> s_eventually ready — but in simulation an unbounded eventuality can only fail at end-of-test (reported as an unfinished attempt), which is weak and late. The pragmatic simulation form is the bounded window ##[0:MAX_STALL]: it converts the liveness claim into a safety check that fails loudly at a specific cycle. Keep the unbounded form for formal tools, where it is a genuine liveness obligation. State this distinction in interviews — it is a known senior-signal.

Interview angle

“Write the SVA for an AXI-style valid/ready channel” is arguably the verification interview question. Aim to produce, unprompted: valid-stable-until-ready, payload-stable-while-stalled, no-X-when-valid, bounded acceptance, plus the two covers (back-to-back, stall-then-accept). Then volunteer the two nuances that separate strong candidates: the dependency rule is not black-box checkable (explain why, offer the cover-point compromise), and bounded versus unbounded liveness (simulation wants the bounded safety form). Expect the follow-up “why ##1 $stable(data) and not $stable(data) directly?” — because the obligation is about the next cycle's sample relative to the stalled one; asserting stability in the same cycle as the stall start compares against the pre-offer value and misfires on the first valid cycle.

Key takeaways

• Transfer happens on valid && ready at the edge — every rule guards the integrity of a pending offer.

• Five assertions plus two covers form the complete deployable channel checker.

• Producer-side ready-dependency is unfalsifiable from the pins — cover valid-before-ready instead.

• Use bounded ##[0:N] liveness in simulation; reserve s_eventually for formal.

• Phrase stall rules as (valid && !ready) |-> ##1 ... — the obligation lands on the next sample.

Common pitfalls

• Checking only valid stability and forgetting payload stability — data mutation during stall slips through.

• Unqualified !$isunknown(data) — fires on idle cycles; qualify with valid.

• Unbounded liveness in simulation — failure surfaces only as an end-of-test unfinished attempt.

• Asserting $stable(data) in the same cycle valid rises — compares against pre-offer garbage.

• No cover properties — a checker that was never exercised proves nothing in regression sign-off.