NAK — Retransmission Without a New Transaction

Chapter 14.2 took the path where everything works: packets are transmitted, an acknowledgement advances a frontier, retained storage is released.

This is the other path. Something on the Link did not go well, and the retained storage that 14.2 spent the whole chapter releasing is now the thing that saves the transaction.

When Link-local reception fails, what does NAK/retry information require the transmitter to preserve and resend, and why must retransmission remain invisible as a new Transaction Layer operation?

1. The Verified Behaviour

2. A NAK Is Not a Transaction Error

The word "negative" invites exactly the wrong reading, and Module 13 has just taught four things it is not.

3. What Leads to a NAK

Conceptually, and no further. The receiving component's Link machinery determines that an arriving transmission cannot be accepted as successful, and the reliability mechanism signals that recovery is needed.

The exact detection conditions are not published here. They belong to the receiver-side integrity mechanism and to Chapter 15.4, which owns the NAK and its replay trigger; the identity-based conditions belong to Chapter 14.5.

What this chapter needs is narrower and is enough to build hardware: something on the Link went wrong, and the transmitter is told where the receiver's good history ends.

4. One Event, Two Effects

The NAK's identity is the last packet received correctly. That single fact produces both halves of the response.

Take five retained packets using Chapter 14.2 §3's abstract identities:

retained:   10  11  12  13  14

A NAK naming 11 arrives.

retire:     10  11
replay:                 12  13  14
                         ^
                    replay starts here

5. Why a Range, Not a Packet

The most important structural consequence, and the reason Chapter 14.4 exists.

The intuition is that one packet went wrong, so one packet is resent. The intuition is wrong, and the reason is pipelining.

transmitter sends:   A   B   C   D
                         ^
                    trouble around here

By the time the receiver reports a problem with B, the transmitter has already sent C and D. They were in flight; the transmitter did not wait.

And the receiver's good history ends at A. Whatever it did with C and D — discarded them, could not place them, never saw them — it is not reporting them as received, and the transmitter cannot assume it has them.

So recovery restarts from the boundary and continues forward: B, then C, then D. One event, a suffix of retransmissions.

6. One Logical Packet, Several Attempts

Chapter 14.1 §5 introduced the identity distinction. This chapter is where a design and a testbench must both implement it.

Three quantities, and merging any two produces a distinct bug:

7. The Local Event Contract

PCIe's exact timing rules for these events are Chapter 15.4's and are not published here. But RTL cannot be written without some interface contract, so this chapter states one and asserts it.

The abstract reliability-event interface presents at most one resolved event per cycle. ack_valid and nak_valid are mutually exclusive.

And a second contract, for the same reason: a retry event arriving while a replay walk is already active is flagged as unsupported by this model rather than handled by an invented rule (§11). A production design has defined behaviour; this one reports the case.

8. A Replay Trace

Internal teaching signals, not PCIe wire signals.

step           1    2    3    4    5    6    7    8    9   10   11   12
tl_accept      1    1    1    1    0    0    0    0    0    0    0    0
alloc_seq     10   11   12   13    -    -    -    -    -    -    -    -
 
tx_valid       1    1    1    1    0    0    0    1    1    1    0    0
tx_ready       1    1    1    1    0    0    0    0    1    1    0    0
tx_seq        10   11   12   13    -    -    -   12   12   13    -    -
tx_is_replay   0    0    0    0    -    -    -    1    1    1    -    -
 
event_valid    0    0    0    0    1    0    0    0    0    0    0    0
event_ready    1    1    1    1    1    0    0    1    1    1    1    1
event_seq      -    -    -    -   11    -    -    -    -    -    -    -
 
searching      0    0    0    0    0    1    1    0    0    0    0    0
scan_q         -    -    -    -    -    0    1    -    -    -    -    -
lookup_seq     -    -    -    -    -   10   11    -    -    -    -    -
retire_valid   0    0    0    0    0    0    0    1    0    0    0    0
arm_replay     0    0    0    0    0    0    0    1    0    0    0    0
 
retained  10 10,11 ..12 ..13 ..13 ..13 ..13 12,13 12,13 12,13 12,13 12,13
replay_active  0    0    0    0    0    0    0    1    1    1    0    0

Read step 5. A NAK naming 11 is accepted — event_valid && event_ready. Nothing else happens yet: the controller now has to find 11.

Read steps 6 and 7 — this is what the sequential search looks like. The scan examines one position per cycle. At step 6 it presents position 0 and the store answers 10; no match, so the cursor advances. At step 7 it presents position 1, gets 11, and matches. event_ready is low throughout, so a second event arriving here is held by its producer rather than lost (§11a).

Read step 8. The decision is issued for exactly one cycle: 10 and 11 retire, and the walk is armed over the two survivors. Both halves from one event (§4) — that is P7, and P9 is what keeps it to one cycle.

Read steps 8–10. tx_valid is high with tx_seq = 12 for two cycles, because tx_ready is low at step 8. The walk does not advance on an offer — that is Chapter 14.4 §7's scheduler, whose pointer moves only on the handshake.

And read the whole trace for what is absent. tl_accept is zero from step 5 onward. No new Transaction Layer packet was created by any of this — 12 and 13 were sent twice each, and accepted from above exactly once each (§6).

9. Retry Control, Structurally

This chapter owns which retained entry is offered next. It does not own the storage — Chapter 14.4 does.

Note the split. §11's controller decides what to replay and hands over a length; it does not walk. The walk is the scheduler's, because the walk needs the storage.

10. Replay Priority — an Explicit Policy

While replay_active is set, replay traffic has priority over new traffic, and no new packet is transmitted until the walk completes.

This is illustrative implementation policy used to expose replay ownership — not a universal PCIe scheduler requirement. Production implementations may allow more concurrency, subject to protocol constraints.

Why this policy and not a more concurrent one. The point of §11's RTL is that a replay walk and a normal send stream are two consumers of one transmit interface with different sources of truth — one reads retained storage from a walk pointer, the other takes the next new packet. A strict-priority policy makes the ownership boundary between them completely explicit, and the assertions that check it (§13's P7, P8) are readable.

What a more concurrent policy would need, so the simplification is honest: a defined rule for interleaving replayed and new packets on the wire, an allocation path that does not disturb the walk, and a stop boundary that new allocations cannot cross — which is Chapter 14.4 §7's scheduler, where the storage that makes it possible actually exists.

11. RTL — Retry Controller

// SYNTHESIZABLE. Replay control: convert a reliability event into a
// retirement frontier and, for a NAK, a bounded replay walk.
// The dual effect of a NAK (retire through the named identity, replay from
// the next): NORMATIVE (section 1).
// The SEQUENTIAL SEARCH, the serialized event ownership, the captured stop
// boundary and the strict replay priority: ILLUSTRATIVE IMPLEMENTATION
// POLICY (sections 9, 10, 11a).
//
// The search is ONE LOOKUP PER CYCLE against a single-ported store. It has
// to be: the retained window lives in Chapter 14.4's memory, which answers
// one position at a time. A combinational scan over all entries would need
// DEPTH read ports the store does not have.
module retry_controller #(
  parameter int DEPTH = 8,
  parameter int SEQ_W = 8              // internal identity, NOT PCIe
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Reliability event in, with OWNERSHIP -----------------------------
  // valid/ready, because the search takes multiple cycles and an event that
  // arrived during one must not be lost (section 11a).
  input  logic                       event_valid,
  output logic                       event_ready,
  input  logic                       event_is_nak,     // 0 = ACK, 1 = NAK
  input  logic [SEQ_W-1:0]           event_seq,
 
  // ---- Retained-window lookup (Chapter 14.4's core) ---------------------
  // One position per cycle. The core answers combinationally for the
  // position presented this cycle — the local contract stated in section 11a.
  output logic [$clog2(DEPTH+1)-1:0] lookup_pos,
  input  logic                       lookup_entry_valid,
  input  logic [SEQ_W-1:0]           lookup_seq,
  input  logic [$clog2(DEPTH+1)-1:0] occupancy,
 
  // ---- Retirement request, to the store --------------------------------
  output logic                       retire_valid,
  output logic [$clog2(DEPTH+1)-1:0] retire_count,
 
  // ---- Replay arming, to the scheduler ---------------------------------
  output logic                       arm_replay,
  output logic [$clog2(DEPTH+1)-1:0] arm_survivors,
 
  // ---- Reported conditions ---------------------------------------------
  output logic                       event_unknown,    // identity not retained
  output logic                       searching
);
 
  localparam int CNT_W = $clog2(DEPTH + 1);
 
  generate
    if (DEPTH < 1) $error("DEPTH must be at least 1");
  endgenerate
 
  typedef enum logic [1:0] {
    S_IDLE   = 2'd0,   // no event owned
    S_SEARCH = 2'd1,   // walking the retained window, one position per cycle
    S_COMMIT = 2'd2    // decision computed; issue it for exactly one cycle
  } state_e;
 
  state_e            state_q;
  logic [SEQ_W-1:0]  tgt_seq_q;
  logic              tgt_is_nak_q;
  logic [CNT_W-1:0]  scan_q;        // position currently being examined
  logic [CNT_W-1:0]  snap_occ_q;    // SNAPSHOT of the window depth at capture
  logic [CNT_W-1:0]  covered_q;     // prefix length once matched
  logic              matched_q;
  logic              unk_q;
 
  // SERIALIZED EVENT OWNERSHIP (section 11a). Only one event may be owned at
  // a time, so the window the search walks cannot be renumbered underneath
  // it by a second event's retirement.
  assign event_ready = (state_q == S_IDLE);
  assign searching   = (state_q != S_IDLE);
 
  assign lookup_pos = scan_q;
 
  // The decision is issued for exactly one cycle, in S_COMMIT.
  wire commit = (state_q == S_COMMIT);
 
  assign retire_valid  = commit && matched_q;
  assign retire_count  = (commit && matched_q) ? covered_q : '0;
 
  // After retiring `covered_q` entries the survivors renumber, so the walk
  // starts at 0 and runs for (snapshot - covered) entries.
  wire [CNT_W-1:0] survivors = (snap_occ_q >= covered_q)
                                 ? (snap_occ_q - covered_q) : CNT_W'(0);
 
  assign arm_replay    = commit && matched_q && tgt_is_nak_q
                                && (survivors != CNT_W'(0));
  assign arm_survivors = survivors;
  assign event_unknown = unk_q;
 
  wire accept = event_valid && event_ready;
 
  // Does the position being examined this cycle match the captured target?
  wire scan_hit = (state_q == S_SEARCH)
               && lookup_entry_valid
               && (lookup_seq == tgt_seq_q);
 
  // The scan is examining the LAST legal position. Note it never runs PAST
  // the snapshot: the FSM leaves S_SEARCH when this is true, so scan_q is
  // always < snap_occ_q while searching (section 13's P5). A condition
  // written as (scan_q >= snap_occ_q) would be structurally unreachable.
  wire scan_last = (state_q == S_SEARCH)
                && ((scan_q + CNT_W'(1)) >= snap_occ_q);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q    <= S_IDLE;
      tgt_seq_q  <= '0;  tgt_is_nak_q <= 1'b0;
      scan_q     <= '0;  snap_occ_q   <= '0;
      covered_q  <= '0;  matched_q    <= 1'b0;
      unk_q      <= 1'b0;
    end else begin
      unique case (state_q)
 
        S_IDLE: begin
          if (accept) begin
            // Capture the event AND a snapshot of how far the search may
            // run. The snapshot is what makes the multi-cycle search
            // well-defined (section 11a).
            tgt_seq_q    <= event_seq;
            tgt_is_nak_q <= event_is_nak;
            snap_occ_q   <= occupancy;
            scan_q       <= '0;
            matched_q    <= 1'b0;
            covered_q    <= '0;
            state_q      <= (occupancy == '0) ? S_COMMIT : S_SEARCH;
          end
        end
 
        S_SEARCH: begin
          // Priority: a hit ends the search; otherwise advance; exhausting
          // the snapshot ends it unmatched. Written as one if/else chain so
          // the order is a decision rather than an accident.
          if (scan_hit) begin
            matched_q <= 1'b1;
            covered_q <= scan_q + CNT_W'(1);   // logical position + 1
            state_q   <= S_COMMIT;
          end else if (scan_last) begin
            // LAST LEGAL POSITION, no match. The scan never advances past
            // the snapshot, so there is no out-of-range state to reach.
            state_q <= S_COMMIT;               // matched_q stays 0
          end else begin
            scan_q <= scan_q + CNT_W'(1);
          end
        end
 
        S_COMMIT: begin
          // The decision was issued this cycle. Report an unmatched event and
          // release ownership so the next one may be accepted.
          if (!matched_q) unk_q <= 1'b1;
          state_q <= S_IDLE;
        end
 
        default: state_q <= S_IDLE;
      endcase
    end
  end
 
endmodule

Classification: synthesizable.

Architecture. A three-state machine that owns one reliability event at a time and searches the retained window one position per cycle. It converts the event into a retirement count and, for a NAK, an arming pulse for the walk. It does not own the walk itself — Chapter 14.4 §7's scheduler does — and it addresses entries by logical position, never by a memory index, so range safety belongs to the store.

Why the search is sequential, and this is the correction that matters. The retained window lives in the store's memory, which answers one position at a time. A combinational loop that presented lookup_pos = 0, then 1, then 2 within a single cycle and read a response after each would need DEPTH read ports — it is not a scan, it is DEPTH simultaneous lookups written to look like a scan. One port means one cycle per position, and the FSM is what that costs.

State. The captured target identity and its kind, the scan cursor, the window snapshot, the match result, and a sticky unknown-event flag.

Cycle behaviour.

Same-cycle and ownership contract, stated explicitly:

Contract. The store guarantees logical position 0 is the oldest retained entry, and answers the position presented this cycle in the same cycle (§11a). The event producer holds event_valid and its payload stable until event_ready.

Failure — five, and §13 maps each to a check. A combinational scan over one lookup port is unimplementable — the correction this module exists to make. Using live occupancy instead of the snapshot lets a search run past a window that shrank underneath it. Making event_ready unconditional loses the second of two closely-spaced events. Treating a NAK as purely negative — arming without retiring — resends packets the receiver already has; treating it as purely positive — retiring without arming — loses the suffix permanently (§4). And issuing the decision for more than one cycle retires or arms twice.

Deliberately simplified: no packet storage (Chapter 14.4); a linear search rather than sequence arithmetic (14.5); one event owned at a time (§11a); no replay timer; no bound on replay attempts.

Production implication: a real controller compares Sequence Numbers arithmetically and needs no search at all — the FSM disappears entirely once Chapter 14.5's modular comparison is available. What survives is the event-ownership contract, which a design still needs however the match is computed.

11a. The Search Contract

A multi-cycle search introduces a question a combinational one never had: what may change underneath it?

Three things could, and each would break the scan differently.

And the lookup contract itself, stated because the FSM depends on it: the store answers the position presented this cycle in the same cycle — lookup_entry_valid and lookup_seq are combinational on lookup_pos. That is one port, one position, one cycle, which is exactly what Chapter 14.4 §6's core provides. A registered-output store would need one more cycle per position and an extra FSM state; nothing else about the architecture would change.

12. RTL — New/Replay Transmit Mux

// SYNTHESIZABLE. One transmit interface, two sources: the normal send
// stream and the replay walk.
// The strict replay priority is ILLUSTRATIVE POLICY (section 10). The
// requirement that a replay must not create a Transaction Layer acceptance
// is a NORMATIVE consequence of the identity distinction (section 6).
module tx_replay_mux #(
  parameter int PKT_W = 128,
  parameter int SEQ_W = 8
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Normal send stream (new packets, already retained) --------------
  input  logic              new_valid,
  output logic              new_ready,
  input  logic [PKT_W-1:0]  new_packet,
  input  logic [SEQ_W-1:0]  new_seq,
 
  // ---- Replay stream (retained entry selected by the controller) -------
  input  logic              replay_active,
  input  logic [PKT_W-1:0]  replay_packet,
  input  logic [SEQ_W-1:0]  replay_seq,
  output logic              replay_sent,
 
  // ---- Link transmit ---------------------------------------------------
  output logic              tx_valid,
  input  logic              tx_ready,
  output logic [PKT_W-1:0]  tx_packet,
  output logic [SEQ_W-1:0]  tx_seq,
  // Telemetry: this send is a retransmission. NOT a wire signal — it exists
  // so verification can separate attempts from packets (section 6).
  output logic              tx_is_replay
);
 
  // STRICT PRIORITY while the walk is active (section 10). New traffic is
  // held, not dropped: new_ready simply stays low.
  assign tx_valid     = replay_active ? 1'b1        : new_valid;
  assign tx_packet    = replay_active ? replay_packet : new_packet;
  assign tx_seq       = replay_active ? replay_seq  : new_seq;
  assign tx_is_replay = replay_active;
 
  // A new packet is accepted only when the walk is idle. This is the ONE
  // line that keeps a replay from becoming a new Transaction Layer
  // acceptance: the new stream simply is not consumed during a walk.
  assign new_ready   = !replay_active && tx_ready;
 
  // The handshake is reported back to the controller so the walk pointer
  // advances on the transfer, never on the offer.
  assign replay_sent = replay_active && tx_valid && tx_ready;
 
endmodule

Classification: synthesizable.

Architecture. A two-source mux with a mode-driven select. It is purely combinational — deliberately: it holds no packet, so there is no state in which it could present one source's data with the other's identity.

Contract. Downstream relies on tx_packet and tx_seq being stable while tx_ready is low — which it inherits from its two sources, since it stores nothing. The replay source guarantees replay_packet is stable while replay_active and the pointer are unchanged, which is the retained storage's immutability guarantee (Chapter 14.4).

Failure — three. Selecting the packet from one source and the identity from the other transmits a packet under the wrong sequence identity, which the receiver will place wrongly and which no local check would catch. Asserting new_ready during a walk consumes a new packet that is not transmitted — the packet is lost between the Transaction Layer and the store. And deriving replay_sent from tx_valid alone advances the walk on an offer.

Deliberately simplified: strict priority; no arbitration weights; no per-class separation; no flow-control interaction (Module 16).

13. Assertions

// SVA over retry_controller and tx_replay_mux. These assert the NORMATIVE
// dual effect of a NAK (section 1), the identity distinction (section 6),
// and the LOCAL contracts of sections 7, 10 and 11a — which are labelled as
// policy in the properties that check them. Nothing here asserts NAK DLLP
// format or timing (Chapter 15.4) or sequence arithmetic (Chapter 14.5).
 
// ---- ENVIRONMENT ASSUMPTIONS ----------------------------------------
// A1: THE LOCAL EVENT CONTRACT of section 7 — ACK and NAK are mutually
// exclusive on this interface. A property of the decoder upstream.
assume property (@(posedge clk) disable iff (!rst_n)
  !(ack_valid && nak_valid));
// A2: the store answers the presented position in the SAME cycle
// (section 11a). Without this the FSM would need an extra state.
assume property (@(posedge clk) disable iff (!rst_n)
  (state_q == S_SEARCH) |-> !$isunknown(lookup_entry_valid));
// A3: the event producer holds the offer stable until it is accepted.
assume property (@(posedge clk) disable iff (!rst_n)
  (event_valid && !event_ready)
    |=> (event_valid && $stable({event_is_nak, event_seq})));
 
// ---- EVENT OWNERSHIP -------------------------------------------------
 
// P1: ONE EVENT AT A TIME. No event is accepted while one is owned — the
// serialization that makes the multi-cycle search well-defined (section 11a).
property p_one_event_owned;
  @(posedge clk) disable iff (!rst_n)
  searching |-> !event_ready;
endproperty
a_one_event : assert property (p_one_event_owned);
 
// P2: NO EVENT IS LOST. An offered event that is refused is still offered
// next cycle — the valid/ready contract doing the work a dropped-event
// interface could not.
property p_no_event_lost;
  @(posedge clk) disable iff (!rst_n)
  (event_valid && !event_ready) |=> event_valid;
endproperty
a_no_loss : assert property (p_no_event_lost);
 
// P3: the captured target is stable for the whole search. Catches a second
// event overwriting the identity being looked for.
property p_target_stable_while_searching;
  @(posedge clk) disable iff (!rst_n)
  (state_q == S_SEARCH) |=> ((state_q != S_SEARCH)
                          || $stable({tgt_seq_q, tgt_is_nak_q, snap_occ_q}));
endproperty
a_target_stable : assert property (p_target_stable_while_searching);
 
// ---- SEARCH ----------------------------------------------------------
 
// P4: the scan advances by AT MOST ONE position per cycle. The property that
// a combinational multi-position scan cannot satisfy — and the direct
// statement of the single-port contract.
property p_scan_advances_by_one;
  @(posedge clk) disable iff (!rst_n)
  !$stable(scan_q) |-> ((scan_q == $past(scan_q) + CNT_W'(1))
                     || $past(accept));
endproperty
a_scan_step : assert property (p_scan_advances_by_one);
 
// P5: the scan never examines a position outside the captured snapshot.
property p_scan_within_snapshot;
  @(posedge clk) disable iff (!rst_n)
  (state_q == S_SEARCH) |-> (scan_q < snap_occ_q);
endproperty
a_scan_bound : assert property (p_scan_within_snapshot);
 
// P6: a match records the position it was found at, not some other one.
property p_covered_is_position_plus_one;
  @(posedge clk) disable iff (!rst_n)
  scan_hit |=> (matched_q && (covered_q == $past(scan_q) + CNT_W'(1)));
endproperty
a_covered : assert property (p_covered_is_position_plus_one);
 
// ---- DECISION --------------------------------------------------------
 
// P7: THE NORMATIVE DUAL EFFECT. A matched NAK retires the prefix AND arms
// the walk over the survivors. Both halves from one event (section 4) —
// conjunctive, so a design doing only one fails.
property p_nak_retires_and_arms;
  @(posedge clk) disable iff (!rst_n)
  (commit && matched_q && tgt_is_nak_q)
    |-> (retire_valid && (retire_count == covered_q)
      && (arm_replay == (survivors != CNT_W'(0)))
      && (arm_survivors == survivors));
endproperty
a_dual_effect : assert property (p_nak_retires_and_arms);
 
// P8: a matched ACK retires and does NOT arm. The other half of the
// distinction between the two event kinds.
property p_ack_retires_only;
  @(posedge clk) disable iff (!rst_n)
  (commit && matched_q && !tgt_is_nak_q) |-> (retire_valid && !arm_replay);
endproperty
a_ack_no_arm : assert property (p_ack_retires_only);
 
// P9: the decision is issued for EXACTLY ONE CYCLE. A decision held for two
// retires or arms twice.
property p_decision_pulses_once;
  @(posedge clk) disable iff (!rst_n)
  (retire_valid || arm_replay) |=> (!retire_valid && !arm_replay);
endproperty
a_single_pulse : assert property (p_decision_pulses_once);
 
// P10: an unmatched event changes nothing and is reported.
property p_unmatched_inert;
  @(posedge clk) disable iff (!rst_n)
  (commit && !matched_q)
    |-> ((!retire_valid) && (!arm_replay)) ##1 event_unknown;
endproperty
a_unmatched : assert property (p_unmatched_inert);
 
// P11: the arming never covers more than the snapshot allowed.
property p_survivors_bounded;
  @(posedge clk) disable iff (!rst_n)
  arm_replay |-> (arm_survivors <= snap_occ_q);
endproperty
a_survivors : assert property (p_survivors_bounded);
 
// ---- MUX -------------------------------------------------------------
 
// P12: THE IDENTITY PROPERTY. A replay never creates a Transaction Layer
// acceptance. Section 6's whole argument, in one line.
property p_replay_is_not_acceptance;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && tx_ready && tx_is_replay) |-> !(new_valid && new_ready);
endproperty
a_no_new_acceptance : assert property (p_replay_is_not_acceptance);
 
// P13: POLICY (section 10). No new packet is accepted while a walk is active.
property p_no_new_during_replay;
  @(posedge clk) disable iff (!rst_n)
  replay_active |-> !new_ready;
endproperty
a_policy_priority : assert property (p_no_new_during_replay);
 
// P14: the offered packet and identity always come from the SAME source.
// Catches a mux selecting data and identity independently.
property p_source_consistent;
  @(posedge clk) disable iff (!rst_n)
  tx_valid |-> (replay_active ? ((tx_packet == replay_packet)
                              && (tx_seq    == replay_seq))
                              : ((tx_packet == new_packet)
                              && (tx_seq    == new_seq)));
endproperty
a_source : assert property (p_source_consistent);
 
// P15: reset clears event ownership.
property p_reset_clears;
  @(posedge clk)
  !rst_n |=> (!searching && !retire_valid && !arm_replay);
endproperty
a_reset : assert property (p_reset_clears);
 
// ---- BOUNDED TERMINATION — no fairness assumption required ------------
// The search is a deterministic walk over a finite snapshot with a
// combinational store (A2), so it terminates by construction. Asserting it
// with s_eventually would be weaker AND would need an assumption that is
// not true of anything here — there is no external agent whose fairness the
// scan depends on.
 
// P16: the scan makes progress every cycle it does not commit. Together with
// P5 (scan_q < snap_occ_q) this bounds the walk at snap_occ_q cycles.
property p_scan_progresses_or_commits;
  @(posedge clk) disable iff (!rst_n)
  (state_q == S_SEARCH)
    |=> ((state_q == S_COMMIT)
      || ((state_q == S_SEARCH) && (scan_q == $past(scan_q) + CNT_W'(1))));
endproperty
a_progress : assert property (p_scan_progresses_or_commits);
 
// P17: examining the LAST legal position always commits, matched or not.
// This is the unmatched exit path, and it is the one the removed assumption
// got wrong: the FSM never enters an out-of-range position, so a condition
// phrased as "ran past the snapshot" is unreachable.
property p_last_position_commits;
  @(posedge clk) disable iff (!rst_n)
  scan_last |=> (state_q == S_COMMIT);
endproperty
a_last_commits : assert property (p_last_position_commits);
 
// P18: an empty snapshot commits WITHOUT any array lookup.
property p_empty_snapshot_skips_search;
  @(posedge clk) disable iff (!rst_n)
  (accept && (occupancy == '0)) |=> (state_q == S_COMMIT);
endproperty
a_empty_skips : assert property (p_empty_snapshot_skips_search);
 
// L1: BOUNDED termination. Ownership is released within the snapshot depth
// plus the fixed FSM overhead — a concrete bound, not an eventually.
// (DEPTH + 2 covers the worst case: DEPTH search cycles, one commit, one
// return to IDLE.)
property p_returns_to_idle_bounded;
  @(posedge clk) disable iff (!rst_n)
  accept |-> ##[1:(DEPTH+2)] event_ready;
endproperty
a_bounded_termination : assert property (p_returns_to_idle_bounded);

P7 is the normative property and it is deliberately conjunctive. A matched NAK must produce both effects. A design doing only one passes half the obvious checks — retiring without arming looks like a correct ACK path, and arming without retiring looks like a correct replay path. Only asserting both together catches either, and P8 completes the pair by requiring that an ACK retires without arming, so the two event kinds cannot be conflated in either direction.

P4 is the property that could not exist before this chapter's correction. "The scan advances by at most one position per cycle" is unsatisfiable by a combinational loop that examines every entry in one cycle — so the property is not merely a check on the FSM, it is the statement of the single-port contract. A design that reverts to a parallel scan fails it structurally rather than on some particular stimulus.

P1, P2 and P3 are the ownership triad and they fail on three different mistakes. P1 catches accepting a second event mid-search. P2 catches an interface that drops a refused event rather than holding it — the failure a non-backpressurable event input would have. P3 catches a captured target being overwritten, which is what would happen if event_ready were tied high.

P9 is small and easy to omit. The decision is issued in S_COMMIT for one cycle; a design that lingered there, or that drove retire_valid from matched_q alone, would retire the same prefix twice — and the second retirement would release packets whose delivery is unresolved.

P12 is the identity property and is the chapter in one line. A replay must not coincide with a Transaction Layer acceptance (§6), and it fires the first time a design consumes the new stream during a walk.

P13 is labelled POLICY in its comment deliberately. It checks §10's illustrative scheduling decision, not a protocol rule. A production design with a more concurrent policy would legitimately fail it — and a reader needs to know which properties are protocol and which are this model's, or they will carry the wrong one forward.

A2 describes the store, not this module, and it would change if the store registered its lookup output. Naming it is what makes the FSM's cycle count auditable: with a combinational store the search is one cycle per position; with a registered one it is two, and L1's bound would become 2·DEPTH + 2.

P16, P17, P18 and L1 replace what used to be a fairness assumption, and the replacement is strictly stronger. The search is a deterministic walk over a finite snapshot — there is no external agent whose fairness it depends on, so s_eventually would have been both weaker and unnecessary. L1 states a concrete bound instead: ownership is released within DEPTH + 2 cycles.

And P17 is the property that the removed assumption got wrong. The FSM exits on the last legal position, so it never enters an out-of-range one — a termination condition phrased as "the scan ran past the snapshot" is structurally unreachable, and assuming it would have made the liveness proof vacuous rather than true.

14. Verification

Monitors observe: the Transaction Layer acceptance interface, the transmit interface with tx_is_replay, the reliability events, and the controller's walk state.

The scoreboard tracks logical packets, not sends

Mandatory, and it is §6 made concrete.

// VERIFICATION-ONLY. One entry per LOGICAL packet. Attempts are an
// attribute of the entry, never separate objects.
typedef struct {
  int         packet_id;      // testbench metadata, NOT PCIe state
  bit [127:0] packet;         // as accepted from the Transaction Layer
  int         seq_id;
  int         attempt_count;  // may be ANY value >= 1 — replay is not an error
  bit         retired;
} sb_pkt_t;
 
// On TL acceptance : create ONE entry, attempt_count = 0
// On each send     : find by seq_id; attempt_count++;
//                    ASSERT packet bits unchanged
// On NAK           : construct the EXPECTED replay suffix independently
//                    from the scoreboard's own retained list, and compare
//                    against the observed sequence of replay sends
// On retirement    : assert the retired prefix matches the expected one

The expected replay suffix must be constructed independently. Reading the DUT's covered_q, snap_occ_q or the scheduler's walk bound as the expectation verifies only that the design agrees with itself — and a search that matched the wrong entry keeps all of them mutually consistent.

Retirement and replay

• One retained packet, NAK naming it. Retire 1, no walk — there are no survivors.
• Three retained, NAK naming the oldest. Retire 1, walk over the other two.
• Three retained, NAK naming the middle. Retire 2, walk over one.
• Three retained, NAK naming the newest. Retire 3, no walk.
• Five retained, NAK naming the second. Retire 2, walk over three — verify the order is oldest-first.
• The §8 trace exactly. Verify the retirement, the two-cycle stall on the first replay, and the walk completing at the boundary.

Backpressure and ordering

• tx_ready low for the whole walk, then released. Verify replay_pos never moves while stalled (P6), and the packet and identity are stable (P9).
• tx_ready toggling every cycle during a walk. Verify each entry is sent exactly once.
• A new Transaction Layer packet offered during a walk. Verify new_ready stays low (P7) and the packet is not consumed — it must still be there when the walk ends.
• New traffic immediately after a walk completes. Verify it resumes.

Negative

• A NAK naming an identity not retained. Verify nothing retires, no walk arms, event_unknown sets (P10).
• A NAK on an empty window.
• A second event offered while a search is running. Verify event_ready is low, the offer is held rather than lost (P2), the captured target is unchanged (P3), and the second event is accepted once the first commits.
• A search that scans the whole window without matching. Verify it terminates at the snapshot bound (P5), commits unmatched, and reports event_unknown (P10).
• A search on an empty window. Verify it commits immediately without scanning.
• A search whose match is at the last snapshot position. The boundary between matching and exhausting.
• New allocation during a search. Verify the scan does not follow the growing window — the snapshot bounds it (§11a).
• An ACK during an active walk. Verify it retires correctly and does not disturb the walk boundary.
• Simultaneous ack_valid and nak_valid. Verify the assumption A1 fires — a testbench that can produce this has a bug, and the assumption is what tells you.
• Reset mid-walk. Verify replay_active clears and no partial walk state survives (P13).
• DEPTH = 1, and a non-power-of-two DEPTH.

Which mutation which check kills

15. Debugging

The PHY trace shows a TLP three times; the Transaction Layer monitor shows it once

This may be completely correct (Chapter 14.1 §5). One logical packet, three send attempts, one acceptance from above.

Check tx_is_replay on the second and third sends. Set on both → one packet replayed twice, which is correct. Clear on any of them → the Transaction Layer accepted it more than once, which is a real duplicate and a completely different fault (P5).

And check the receiving side. The receiving Transaction Layer should see it once; more than that is the receive-side duplicate boundary (Chapter 14.1 §9), not this controller.

A remote side effect occurs twice after one NAK event

Investigate the receive-side duplicate boundary first, not the transmitting device's transaction logic.

A replay is expected to put the same packet on the wire again. The receiver is supposed to recognise it and deliver it upward once. If a side effect happened twice, the most likely cause is that the receiver delivered both — Chapter 14.1 §9's acceptance filter.

The distinguishing observation is at the transmitter: how many Transaction Layer acceptances were there for that packet? One → the transmitter is fine and the receiver duplicated it. Two → the transmitter created a second operation, and the replay path is the suspect (P5).

The instinct to resist is starting at the software or the DMA engine. They generated one operation; two happened; the layer in between is where the count changed.

The replay begins at the wrong packet

Three candidates, and one of them is a sign error in reading the NAK.

The identity meaning. A NAK names the last correctly received packet, so the walk starts at the next one (§1). A design that starts at the named entry replays a packet the receiver already has — and worse, it also failed to retire it, so occupancy is wrong too.

The retirement/arm interaction. The walk starts at logical position 0 after the retirement renumbers the survivors. If the arm captures the pointer before the retirement is applied, the walk starts several entries too early.

The match search. If event_unknown is set, no walk armed at all and whatever is being replayed came from somewhere else.

The observation: print the NAK's identity, the retired count, and the first tx_seq of the walk. The first replayed identity must be the one immediately after the NAK's.

New traffic stops forever after a NAK

The walk never completed, and there are three ways.

replay_active never cleared. Check whether the transmit handshake is completing — if tx_ready is permanently low, the walk is correctly waiting and the fault is downstream, which Chapter 14.4 §14's assumption A2 states as an environment condition rather than a defect.

The walk bound is wrong. If the scheduler captured it from live occupancy while allocations continued, the walk chases a tail that keeps moving (Chapter 14.4 §7). A walk position climbing indefinitely is the signature.

A stuck search. Check searching: if it never clears, the scan is not terminating — which under the single-port contract means the cursor is not advancing, and P4 is the property that catches it. A stuck search also blocks every later event, since event_ready stays low.

16. Common Misconceptions

• "A NAK is a Completion error status." Different layer, different scope. Completion status is SC/UR/CRS/CA (Chapter 13.2); a NAK is Link-local (§2).
• "A NAK means software should retry." Software is not involved and is not told. Hardware resends from storage it already holds (§2).
• "A NAK creates a new TLP." It causes an existing retained packet to be transmitted again. No new packet exists (§6).
• "A retried packet gets a new Requester Tag." A Tag is Transaction Layer correlation (Chapter 11.3 §6) and is part of the retained packet — it does not change, because the packet does not change (P4).
• "Only the bad packet needs replaying." By the time the NAK arrives, later packets have already been sent and are unresolved. Replay is a suffix (§5).
• "A replay can regenerate the payload from current upstream signals." The packet is owned state, retained since acceptance. Regenerating it means sending different bits (Chapter 14.1 §8).
• "The retry pointer can advance while the transmit path is stalled." It advances on the handshake, never on the offer (§8, P6).
• "Replay count equals transaction count." One logical packet may have many attempts. A scoreboard counting sends as transactions fails correct hardware (§6).
• "New traffic must always stop globally during a retry." §10's strict priority is this model's policy, chosen to make ownership visible. Production designs may allow more concurrency (§10).
• "A NAK crosses every Switch on the path." It is Link-local. A Switch terminates one reliability relationship and originates another (Chapter 3.2 §2).
• "Replay belongs in the Transaction Layer." It is Data Link machinery, and keeping it there is the entire reason the Transaction Layer can assume a packet handed down arrives (Chapter 14.1 §2).
• "A NAK only replays; it never retires." It names the last correctly received packet, so it does both (§4).

17. Understanding Check

18. What's Next

This chapter turned one event into two effects. A NAK names the boundary of the receiver's good history, so it retires the prefix and replays the suffix — and the replayed packets are the same packet instances, not new operations, which is the property that keeps a Link-layer mechanism from becoming a Transaction Layer bug.

Both Chapter 14.2 and this chapter have been operating on storage they described and did not build. Chapter 14.2 held identities; §11 addressed entries by logical position and explicitly did not own them.

Chapter 14.4 — Replay Buffer builds it: an ordered structure where reading for transmission is not dequeuing, with independent allocation, retirement and replay pointers, a captured replay boundary, correct wrap at any depth, and the simultaneous-event cases all three chapters have been deferring to it.

Chapter 14.5 then replaces the abstract seq_id with PCIe's actual Sequence Number mechanism — including the comparison arithmetic that makes §11's match search unnecessary. Chapter 15.4 owns the NAK DLLP itself: its format and its replay trigger.

The idea to carry forward: a NAK reports where the receiver's good history ends — everything before it is done, everything after it goes again, and none of it is a new transaction.