NAK Packets — Delivering a Recovery Request Safely

receiver's good history ends at 11
packet 12 arrives with a bad LCRC
 
Nak carries:  11         ← the last GOOD one
NOT:          12         ← the one that failed

Nak decoded          →  retry controller
                          S_SEARCH: up to DEPTH cycles
                          S_COMMIT: 1 cycle
                        then a replay walk: up to DEPTH more

step             1    2    3    4    5    6    7    8    9   10
dllp_valid       1    0    1    0    0    0    0    0    0    0
dllp_type      NAK    -  ACK    -    -    -    -    -    -    -
dllp_seq        11    -   13    -    -    -    -    -    -    -
 
q_count          0    1    1    2    2    1    1    1    0    0
evt_valid        0    1    1    1    1    1    1    1    0    0
evt_ready        0    1    0    0    0    1    0    0    0    0
evt_kind         -  NAK  NAK  NAK  NAK  ACK  ACK  ACK    -    -
 
searching        0    0    1    1    1    0    1    1    0    0
scan_q           -    -    0    1    2    -    0    -    -    -
retire_valid     0    0    0    0    0    1    0    0    1    0
arm_replay       0    0    0    0    0    1    0    0    0    0

// SYNTHESIZABLE. Extract a recovery event from a received DLLP.
// The 12-bit split AckNak_Seq_Num: verified layout (section 1). The Type
// value is a PARAMETER — this chapter does not publish the encoding.
// The event interface: ILLUSTRATIVE.
//
// The sequence field is emitted UNMODIFIED. It names the last correctly
// received packet (section 3); applying the "+1 for replay start" semantics
// is Chapter 14.3's, and doing it here would put one rule in two places.
module nak_dllp_decode #(
  parameter int SEQ_W = 12,
  parameter logic [7:0] NAK_TYPE = 8'h10   // supplied by the integrator
) (
  input  logic              dllp_valid,
  input  logic [7:0]        dllp_byte0,
  input  logic [7:0]        dllp_byte2,   // [3:0] = AckNak_Seq_Num[11:8]
  input  logic [7:0]        dllp_byte3,   // [7:0] = AckNak_Seq_Num[7:0]
  input  logic              dllp_integrity_ok,
 
  output logic              nak_hit,      // this DLLP is a Nak
  output logic [SEQ_W-1:0]  nak_seq,
  output logic              nak_bad_integrity
);
 
  generate
    if (SEQ_W != 12)
      $error("This decoder implements the 12-bit AckNak_Seq_Num of section 1");
  endgenerate
 
  // SPLIT FIELD reassembly, written as an explicit concatenation for the
  // reason Chapter 15.3 section 3 gives: a {byte2, byte3}[11:0] slice takes
  // byte 2's HIGH nibble and is wrong by construction.
  assign nak_seq = {dllp_byte2[3:0], dllp_byte3[7:0]};
 
  // INTEGRITY FIRST. A corrupted DLLP's Type and sequence field are both
  // untrustworthy, and a corrupted value fed to the retry controller would
  // arm a replay from an arbitrary point.
  wire usable = dllp_valid && dllp_integrity_ok;
 
  assign nak_hit           = usable && (dllp_byte0 == NAK_TYPE);
  assign nak_bad_integrity = dllp_valid && !dllp_integrity_ok;
 
endmodule

// SYNTHESIZABLE. Hold decoded reliability events until Chapter 14.3's
// controller can take them.
// That a decoded Nak must not be lost is a consequence of section 4's
// asymmetry. The DEPTH-2 choice, the merge policy and the overflow report:
// ILLUSTRATIVE IMPLEMENTATION POLICY.
package rel_evt_pkg;
 
  typedef enum logic {
    REL_ACK = 1'b0,
    REL_NAK = 1'b1
  } rel_kind_e;
 
  // NORMALIZED INTERNAL EVENT. Once decoded, kind and identity stay attached
  // — nothing downstream re-reads the parser (Chapter 11.6 section 7).
  typedef struct packed {
    rel_kind_e   kind;
    logic [11:0] seq;
  } rel_evt_t;
 
endpackage

import rel_evt_pkg::*;
 
module reliability_event_queue (
  input  logic clk,
  input  logic rst_n,
 
  // ---- ACK side: COALESCED and BACKPRESSURABLE --------------------------
  // Chapter 15.3's ack_frontier_coalescer sits between the ACK decoder and
  // this queue. So the ACK arriving here is a cumulative frontier that the
  // coalescer will KEEP ADVANCING if this queue is not ready -- which means
  // refusing it costs nothing, and a handshake is safe.
  input  logic        ack_evt_valid,
  output logic        ack_evt_ready,
  input  logic [11:0] ack_evt_seq,
 
  // ---- NAK side: UNBACKPRESSURABLE ---------------------------------------
  // A Nak is not cumulative and cannot be re-derived (section 4). Nothing
  // upstream can hold it, so this queue must.
  input  logic        nak_hit,
  input  logic [11:0] nak_seq,
 
  // ---- To Chapter 14.3's retry controller ------------------------------
  output logic      evt_valid,
  input  logic      evt_ready,
  output rel_evt_t  evt,
 
  output logic [1:0] q_count,
  output logic       evt_overflow      // an event could not be held
);
 
  // DEPTH IS FIXED AT TWO (see the callout). Two entries, explicit — no
  // pointer arithmetic to get wrong at a depth this small.
  rel_evt_t e0_q, e1_q;
  logic [1:0] cnt_q;
  logic       ovf_q;
 
  assign q_count     = cnt_q;
  assign evt_valid   = (cnt_q != 2'd0);
  assign evt         = e0_q;              // head
  assign evt_overflow = ovf_q;
 
  wire pop = evt_valid && evt_ready;
 
  // EFFECTIVE capacity: a slot vacated this cycle is usable this cycle.
  wire can_take = (cnt_q != 2'd2) || pop;
 
  // ADMISSION PRIORITY: NAK FIRST, ALWAYS.
  //
  // The two sources can now present in the same cycle -- the coalescer holds
  // its frontier until taken, so it may still be offering when a Nak
  // arrives. The tie-break is not arbitrary and it is not fairness:
  //
  //   a refused NAK is LOST and unrecoverable (section 4);
  //   a refused ACK is HELD by the coalescer, which keeps advancing it.
  //
  // So the unrecoverable event wins, and the coalescable one waits at
  // zero cost. Round-robin here would be strictly worse.
  wire take_nak = nak_hit && can_take;
  wire take_ack = ack_evt_valid && !nak_hit && can_take;
 
  // The ACK side is refused, not dropped. Nothing is lost by refusing it.
  assign ack_evt_ready = take_ack;
 
  wire        push      = take_nak || take_ack;
  rel_evt_t   push_evt;
  assign push_evt.kind = take_nak ? REL_NAK : REL_ACK;
  assign push_evt.seq  = take_nak ? nak_seq : ack_evt_seq;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      e0_q <= '0; e1_q <= '0; cnt_q <= 2'd0; ovf_q <= 1'b0;
    end else begin
      // Four explicit arms. Shifting is written out because at depth two it
      // is clearer than pointers and cannot alias.
      unique case ({push, pop})
        2'b10: begin                          // push only
          if (cnt_q == 2'd0) e0_q <= push_evt;
          else               e1_q <= push_evt;
          cnt_q <= cnt_q + 2'd1;
        end
        2'b01: begin                          // pop only
          e0_q  <= e1_q;                      // shift down
          cnt_q <= cnt_q - 2'd1;
        end
        2'b11: begin                          // push AND pop
          // The head leaves and the new event lands behind whatever
          // remains. Occupancy is unchanged.
          if (cnt_q == 2'd1) e0_q <= push_evt;
          else begin e0_q <= e1_q; e1_q <= push_evt; end
        end
        default: ;                            // idle
      endcase
 
      // OVERFLOW IS A NAK-ONLY CONDITION NOW. A refused ACK is not an
      // overflow -- the coalescer still owns it. A refused NAK is a lost
      // recovery request, which must never be silent (section 4).
      if (nak_hit && !can_take) ovf_q <= 1'b1;
    end
  end
 
endmodule

// SVA over nak_dllp_decode and reliability_event_queue, bound against
// Chapter 14.3's controller. These assert the verified field layout of
// section 1 and the LOCAL delivery contract. Nothing here asserts Nak
// generation timing (not modelled, section 1), the replay algorithm
// (Chapters 14.3-14.4), or sequence arithmetic (14.5).
 
// ---- ENVIRONMENT -----------------------------------------------------
// A1: one received DLLP is an Ack or a Nak, never both. (The DECODERS are
// still mutually exclusive; the QUEUE INPUTS are not, because the coalesced
// ACK may still be offering when a Nak arrives -- which is exactly what the
// admission priority exists for.)
assume property (@(posedge clk) disable iff (!rst_n)
  !(ack_hit && nak_hit));
// A1b: the ACK side obeys valid/ready -- the coalescer holds its frontier
// stable while refused (Chapter 15.3 P4d).
assume property (@(posedge clk) disable iff (!rst_n)
  (ack_evt_valid && !ack_evt_ready) |=> ack_evt_valid);
// A2: the DLLP core bytes are stable while dllp_valid.
assume property (@(posedge clk) disable iff (!rst_n)
  dllp_valid |-> !$isunknown({dllp_byte0, dllp_byte2, dllp_byte3}));
 
// ---- DECODE ----------------------------------------------------------
 
// P1: the split field is reassembled exactly. Independent restatement, so a
// wrong slice cannot pass by agreeing with itself.
property p_field_exact;
  @(posedge clk) disable iff (!rst_n)
  nak_hit |-> (nak_seq == {dllp_byte2[3:0], dllp_byte3});
endproperty
a_field : assert property (p_field_exact);
 
// P2: a corrupted DLLP never becomes a recovery event. Worse here than for
// an Ack: a corrupted value would arm a replay from an arbitrary point.
property p_corrupt_never_naks;
  @(posedge clk) disable iff (!rst_n)
  (dllp_valid && !dllp_integrity_ok) |-> !nak_hit;
endproperty
a_corrupt : assert property (p_corrupt_never_naks);
 
// P3: only a Nak-Type DLLP decodes as a Nak.
property p_type_exact;
  @(posedge clk) disable iff (!rst_n)
  (dllp_valid && (dllp_byte0 != NAK_TYPE)) |-> !nak_hit;
endproperty
a_type : assert property (p_type_exact);
 
// P4: THE OFFSET IS APPLIED EXACTLY ONCE, and downstream. Bound across the
// boundary against Chapter 14.3's controller: the first packet the replay
// walk re-sends is the named sequence PLUS ONE (section 3). A decoder that
// "helpfully" pre-added one, or a controller that added a second one, both
// fail this -- and neither could be caught inside a single module.
property p_offset_applied_once;
  @(posedge clk) disable iff (!rst_n)
  dut_retry_controller.arm_replay
    |-> (dut_replay_buffer.first_resend_seq
           == (dut_retry_controller.event_seq + 12'd1));
endproperty
a_offset_once : assert property (p_offset_applied_once);
 
// ---- QUEUE -----------------------------------------------------------
 
// P5: NO NAK IS EVER LOST. The chapter's central property, and the one a
// one-entry structure fails. A Nak is admitted or reported -- never
// silently absent.
property p_no_nak_lost;
  @(posedge clk) disable iff (!rst_n)
  nak_hit |-> (take_nak || evt_overflow_next);
endproperty
a_no_loss : assert property (p_no_nak_lost);
 
// P5b: NAK ADMISSION PRIORITY. Whenever both sources present and there is
// room, the NAK is the one admitted -- because refusing it is unrecoverable
// and refusing the ACK is free.
property p_nak_wins;
  @(posedge clk) disable iff (!rst_n)
  (nak_hit && ack_evt_valid && can_take) |-> (take_nak && !ack_evt_ready);
endproperty
a_nak_priority : assert property (p_nak_wins);
 
// P5c: NO ACK IS LOST EITHER -- it is REFUSED, not dropped. Bound against
// Chapter 15.3's coalescer: a refused frontier is still owned upstream.
property p_ack_refused_not_dropped;
  @(posedge clk) disable iff (!rst_n)
  (ack_evt_valid && !ack_evt_ready)
    |=> (dut_ack_coalescer.out_valid);
endproperty
a_ack_held : assert property (p_ack_refused_not_dropped);
 
// P6: a NAK that could not be held is REPORTED, never silent. A refused
// ACK is NOT an overflow -- asserting otherwise would train an integrator
// to ignore a flag that does mean something.
property p_overflow_reported;
  @(posedge clk) disable iff (!rst_n)
  (nak_hit && !can_take) |=> evt_overflow;
endproperty
a_overflow : assert property (p_overflow_reported);
 
// P6b: an ACK refused for room, or deferred behind a NAK, NEVER sets it.
property p_ack_refusal_is_not_overflow;
  @(posedge clk) disable iff (!rst_n)
  (ack_evt_valid && !ack_evt_ready && !nak_hit && !$past(nak_hit))
    |=> $stable(evt_overflow);
endproperty
a_ack_not_overflow : assert property (p_ack_refusal_is_not_overflow);
 
// P6c: NAKS ARE NEVER COALESCED. Two Naks are two events. Only the ACK
// side is cumulative (Chapter 15.3 section 4); applying that optimisation
// to recovery requests would discard one.
property p_naks_not_coalesced;
  @(posedge clk) disable iff (!rst_n)
  (take_nak && $past(take_nak)) |-> (nak_admit_count == $past(nak_admit_count) + 1);
endproperty
a_no_nak_coalesce : assert property (p_naks_not_coalesced);
 
// P7: IMMUTABILITY. A queued event's kind and identity do not change while
// it waits. Catches a design re-reading the parser at pop time.
property p_queued_event_immutable;
  @(posedge clk) disable iff (!rst_n)
  (evt_valid && !evt_ready) |=> (evt_valid && $stable(evt));
endproperty
a_immutable : assert property (p_queued_event_immutable);
 
// P8: SAME-CYCLE push and pop both apply — occupancy unchanged, and the
// arriving event is retained.
property p_simul_push_pop;
  @(posedge clk) disable iff (!rst_n)
  (push && pop) |=> (q_count == $past(q_count));
endproperty
a_simul : assert property (p_simul_push_pop);
 
// P9: STRICT ARRIVAL ORDER. Events reach the controller in the order they
// were decoded — reordering would change which prefix retires first.
// (exp_order is a testbench queue.)
property p_order_preserved;
  @(posedge clk) disable iff (!rst_n)
  (evt_valid && evt_ready) |-> (evt == exp_order[0]);
endproperty
a_order : assert property (p_order_preserved);
 
// P10: occupancy is bounded and never underflows.
property p_count_sane;
  @(posedge clk) disable iff (!rst_n)
  (q_count <= 2'd2) && !(pop && (q_count == 2'd0));
endproperty
a_count : assert property (p_count_sane);
 
// ---- INTEGRATION with Chapter 14.3 -----------------------------------
 
// P11: a decoded Nak reaching the controller arms a replay OR is reported
// unknown — it is never silently absorbed.
property p_nak_reaches_a_decision;
  @(posedge clk) disable iff (!rst_n)
  (evt_valid && evt_ready && (evt.kind == REL_NAK))
    |-> ##[1:(DEPTH+2)] (arm_replay || event_unknown);
endproperty
a_nak_decided : assert property (p_nak_reaches_a_decision);
 
// P12: THE IDENTITY PROPERTY. A decoded Nak never creates a Transaction
// Layer acceptance — the replay it triggers resends existing packets
// (Chapter 14.3 section 6).
property p_nak_creates_no_tl_packet;
  @(posedge clk) disable iff (!rst_n)
  (evt_valid && evt_ready && (evt.kind == REL_NAK)) |-> !tl_accept;
endproperty
a_no_tl : assert property (p_nak_creates_no_tl_packet);
 
// P13: a decoded Nak is never a Completion-status event (Chapter 13.2).
property p_nak_not_completion_status;
  @(posedge clk) disable iff (!rst_n)
  nak_hit |-> !(tl_cpl_valid);
endproperty
a_not_cpl : assert property (p_nak_not_completion_status);
 
// P14: reset clears queue ownership.
property p_reset_clears;
  @(posedge clk)
  !rst_n |=> ((q_count == 2'd0) && !evt_valid);
endproperty
a_reset : assert property (p_reset_clears);

received control packets   ← what the wire carried
decoded events             ← what the parser produced
controller decisions       ← retire counts and arm pulses
Link send attempts         ← how many times each packet was transmitted
Transaction Layer packets  ← how many operations exist  (Chapter 14.3 §6)