ACK Packets — Carrying a Frontier Across a Link

ACK DLLP on the wire
   → integrity verdict                    ← lower receive machinery
   → Type classification                  ← Chapter 15.1's dispatcher
   → AckNak_Seq_Num extraction            ← §7's decoder
   → pending cumulative frontier          ← §7's coalescer
   → retirement frontier advance          ← Chapter 14.2's window

AckNak_Seq_Num[11:0]
 
   Byte 2                     Byte 3
   ┌───┬───┬───┬───┬───────┐  ┌───────────────┐
   │ reserved  │ [11:8]    │  │    [7:0]      │
   └───┴───┴───┴───┴───────┘  └───────────────┘
        high nibble               low byte

step             1    2    3    4    5    6    7    8
rx_accept        1    1    1    0    0    1    0    0
rx_seq          10   11   12    -    -   13    -    -
 
pending_valid    1    1    1    1    1    1    1    0
pending_seq     10   11   12   12   12   13   13    -
 
emit_trigger     0    0    0    0    1    0    1    0
ack_valid        0    0    0    0    1    1    1    1
ack_ready        0    0    0    0    0    0    1    1
ack_seq          -    -    -    -   12   12   13   13

// SYNTHESIZABLE. Extract an acknowledgement event from a received DLLP.
// The 12-bit AckNak_Seq_Num and its split position: verified layout
// (section 1). The Type value is a PARAMETER because this chapter does not
// publish the encoding — a design supplies it from the specification.
// The event interface and error outputs: ILLUSTRATIVE.
module ack_dllp_decode #(
  parameter int SEQ_W = 12,
  // Supplied by the integrator from the Base Specification. NOT published
  // here (section 1).
  parameter logic [7:0] ACK_TYPE = 8'h00
) (
  // ---- Received DLLP ----------------------------------------------------
  // The 4-byte DLLP core. Framing and CRC checking happen upstream.
  input  logic              dllp_valid,
  input  logic [7:0]        dllp_byte0,   // Type
  input  logic [7:0]        dllp_byte1,
  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]
  // ABSTRACT integrity verdict from lower receive machinery (section 1).
  input  logic              dllp_integrity_ok,
 
  // ---- Normalized ACK event out, to the coalescer below ----------------
  // NOT a decoupled interface. This block holds nothing; ownership begins
  // one stage later, and two holding stages in series would be one more
  // place for progress to be dropped.
  output logic              ack_hit,
  output logic [SEQ_W-1:0]  ack_seq,
 
  output logic              decode_error       // integrity failed
);
 
  generate
    if (SEQ_W != 12)
      $error("This decoder implements the 12-bit AckNak_Seq_Num of section 1");
  endgenerate
 
  // ---- FIELD REASSEMBLY -------------------------------------------------
  // The field is SPLIT (section 3). Writing the concatenation explicitly,
  // high nibble first, is what makes the layout auditable — a design that
  // sliced {dllp_byte2, dllp_byte3}[11:0] would take byte 2's HIGH nibble
  // into bits [11:8] and be wrong by construction.
  wire [SEQ_W-1:0] seq_field = {dllp_byte2[3:0], dllp_byte3[7:0]};
 
  // INTEGRITY FIRST. A DLLP that failed its check has an unreliable Type
  // and an unreliable sequence field; classifying it would be asking a
  // question about data already known to be bad (Chapter 14.1 section 9).
  wire usable = dllp_valid && dllp_integrity_ok;
 
  assign ack_hit      = usable && (dllp_byte0 == ACK_TYPE);
  assign ack_seq      = seq_field;
  // Reported. Note ack_hit is gated by `usable`, so a failed-integrity DLLP
  // cannot become an acknowledgement by any path.
  assign decode_error = dllp_valid && !dllp_integrity_ok;
 
endmodule

// SYNTHESIZABLE. ACK CUMULATIVE FRONTIER COALESCER.
// That acknowledgement is cumulative is NORMATIVE (section 1). That a
// cumulative frontier can therefore be COALESCED rather than queued -- and
// must never be silently dropped -- is the design consequence.
// The subsumed report is ILLUSTRATIVE.
module ack_frontier_coalescer #(
  parameter int SEQ_W  = 12,
  parameter int WINDOW = (1 << (SEQ_W - 1))
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- From ack_dllp_decode. NOT backpressurable: it came off the wire. --
  input  logic              in_valid,
  input  logic [SEQ_W-1:0]  in_seq,
 
  // ---- To Chapter 14.2's retirement window ------------------------------
  output logic              out_valid,
  input  logic              out_ready,
  output logic [SEQ_W-1:0]  out_seq,
 
  // An arrival that carried no new progress. Not an error -- it is the one
  // legitimate reason an incoming ACK leaves no trace -- but reported,
  // because a healthy Link should not produce many.
  output logic              subsumed
);
 
  // MODULAR COMPARISON, from Chapter 14.5 section 9. An unsigned test would
  // refuse a legitimate advance from 4095 to 0 and accept a stale value
  // after the wrap.
  //
  // NOTE FOR PRODUCTION: this helper is restated here so the module reads
  // standalone. A real design must share ONE verified sequence-comparison
  // definition across 14.2, 14.3, 14.5 and this block -- two copies of a
  // wrap rule is exactly how they come to disagree at the boundary.
  function automatic bit seq_advances(input logic [SEQ_W-1:0] cand,
                                      input logic [SEQ_W-1:0] cur);
    logic [SEQ_W-1:0] d;
    d = cand - cur;                    // fixed width => modular subtraction
    return (d != '0) && (d < SEQ_W'(WINDOW));
  endfunction
 
  logic             v_q;
  logic [SEQ_W-1:0] seq_q;
  logic             sub_q;
 
  assign out_valid = v_q;
  assign out_seq   = seq_q;
  assign subsumed  = sub_q;
 
  wire fire = v_q && out_ready;
  wire adv  = seq_advances(in_seq, seq_q);
 
  // THE THREE CASES, and they are mutually exclusive by construction.
  //
  // CAPTURE -- nothing pending, or the pending value is being delivered
  // this very cycle AND the arrival advances beyond it. The second half is
  // the consume-and-arrive race: the old frontier leaves on the handshake
  // and the new one takes the slot in the same cycle.
  wire captures = in_valid && (!v_q || (fire && adv));
 
  // REPLACE -- occupied, stalled, and the arrival carries MORE progress.
  // Overwriting is not a loss: a cumulative frontier makes the older value
  // a strict subset of the newer one.
  wire replaces = in_valid && v_q && !fire && adv;
 
  // CLEAR -- delivered, and nothing took the slot.
  wire clears   = fire && !captures;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_q <= 1'b0; seq_q <= '0; sub_q <= 1'b0;
    end else begin
      if (captures) begin
        v_q   <= 1'b1;
        seq_q <= in_seq;
      end else if (replaces) begin
        seq_q <= in_seq;               // v_q stays set
      end else if (clears) begin
        v_q <= 1'b0;
      end
 
      // Anything that neither captured nor replaced was SUBSUMED -- either
      // by the frontier still pending, or by the one just delivered.
      if (in_valid && !captures && !replaces) sub_q <= 1'b1;
    end
  end
 
endmodule

// SYNTHESIZABLE. Receiver-side acknowledgement generation: hold the newest
// accepted progress and offer a descriptor when the scheduling policy fires.
// That the frontier is cumulative — and therefore that newer progress
// OVERWRITES older pending progress — follows from section 1's semantics.
// The emit trigger is an INPUT: the specification's acknowledgement
// scheduling thresholds and timers are NOT modelled here (section 5).
module ack_generator #(
  parameter int SEQ_W  = 12,
  parameter int WINDOW = (1 << (SEQ_W - 1))
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Accepted receive progress (Chapter 14.5's tracker) --------------
  // Pulses when a TLP is accepted IN SEQUENCE and delivered upward. A
  // duplicate or a gap must NOT pulse this — acknowledging progress the
  // receiver has not made is the failure P7 forbids.
  input  logic              rx_accept,
  input  logic [SEQ_W-1:0]  rx_seq,
 
  // ---- Scheduling trigger ----------------------------------------------
  // ABSTRACT. The policy that decides WHEN to acknowledge is not modelled
  // (section 5). Everything else about the pending state is.
  input  logic              emit_trigger,
 
  // ---- Descriptor out, to the DLLP transmit path -----------------------
  output logic              ack_req_valid,
  input  logic              ack_req_ready,
  output logic [SEQ_W-1:0]  ack_req_seq,
 
  output logic              pending_valid,
  output logic [SEQ_W-1:0]  pending_seq
);
 
  logic             pend_v_q;
  logic [SEQ_W-1:0] pend_q;
  logic             req_v_q;
  logic [SEQ_W-1:0] req_q;
 
  assign pending_valid = pend_v_q;
  assign pending_seq   = pend_q;
 
  // MONOTONIC WITHIN THE WINDOW. Progress may only move forward. Compared
  // modularly (Chapter 14.5 section 9) — an unsigned test would refuse a
  // legitimate advance across the wrap and accept a stale value after it.
  wire [SEQ_W-1:0] fwd_delta = rx_seq - pend_q;
  wire advances = !pend_v_q
               || ((fwd_delta != '0) && (fwd_delta < SEQ_W'(WINDOW)));
 
  wire req_fire = req_v_q && ack_req_ready;
 
  assign ack_req_valid = req_v_q;
  assign ack_req_seq   = req_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      pend_v_q <= 1'b0; pend_q <= '0;
      req_v_q  <= 1'b0; req_q  <= '0;
    end else begin
      // ---- Pending progress: OVERWRITE with newer (section 4) -----------
      if (rx_accept && advances) begin
        pend_v_q <= 1'b1;
        pend_q   <= rx_seq;
      end
 
      // ---- Descriptor offer ---------------------------------------------
      // Two things happen here, and the order is the design decision.
      //
      // A pending offer is REFRESHED to the newest progress while it waits.
      // That is safe because the frontier is cumulative — naming MORE
      // progress is strictly better — and it avoids emitting two packets
      // where one suffices (section 6, step 7).
      if (req_v_q && !ack_req_ready && pend_v_q
                  && (req_q != pend_q)) begin
        req_q <= pend_q;
      end
 
      if (emit_trigger && pend_v_q && !req_v_q) begin
        req_v_q <= 1'b1;
        req_q   <= pend_q;
      end else if (req_fire) begin
        req_v_q <= 1'b0;
      end
    end
  end
 
endmodule

// SVA over ack_dllp_decode and ack_generator. These assert the verified
// field layout of section 1 and the LOCAL generation/decode contracts. They
// assert nothing about acknowledgement scheduling timing (not modelled,
// section 5), nothing about the retirement algorithm (Chapter 14.2), and
// nothing about credit flow (Chapter 15.2).
 
// ---- ENVIRONMENT -----------------------------------------------------
// A1: rx_accept pulses only for in-sequence accepted progress — never on a
// duplicate or a gap (Chapter 14.5 section 10). The caller's obligation.
assume property (@(posedge clk) disable iff (!rst_n)
  rx_accept |-> !$isunknown(rx_seq));
// A2: the DLLP core bytes are stable while dllp_valid is asserted.
assume property (@(posedge clk) disable iff (!rst_n)
  dllp_valid |-> !$isunknown({dllp_byte0, dllp_byte2, dllp_byte3}));
 
// ---- DECODE ----------------------------------------------------------
 
// P1: only an ACK-Type DLLP produces an acknowledgement event.
property p_only_ack_type_decodes;
  @(posedge clk) disable iff (!rst_n)
  (dllp_valid && (dllp_byte0 != ACK_TYPE)) |-> !ack_hit;
endproperty
a_type : assert property (p_only_ack_type_decodes);
 
// P2: THE FIELD PROPERTY. The extracted identity equals an INDEPENDENT
// reassembly of the split field. Catches every slicing mistake in section 3.
property p_field_extraction_exact;
  @(posedge clk) disable iff (!rst_n)
  ack_hit |-> (ack_seq == {dllp_byte2[3:0], dllp_byte3});
endproperty
a_field : assert property (p_field_extraction_exact);
 
// P3: a DLLP that failed its integrity check NEVER becomes an event.
property p_corrupt_not_decoded;
  @(posedge clk) disable iff (!rst_n)
  (dllp_valid && !dllp_integrity_ok) |-> !ack_hit;
endproperty
a_corrupt : assert property (p_corrupt_not_decoded);
 
// ---- COALESCER: THE OWNERSHIP CONTRACT -------------------------------
 
// P4: THE CENTRAL PROPERTY. Every integrity-valid arrival is RETAINED or
// SUBSUMED -- never silently lost. "Retained" means it became the pending
// frontier; "subsumed" means an equal-or-newer frontier is pending or was
// delivered this cycle. A one-entry register with can_take FAILS this.
property p_retained_or_subsumed;
  @(posedge clk) disable iff (!rst_n)
  in_valid |-> (captures || replaces || subsumed_now);
endproperty
a_no_loss : assert property (p_retained_or_subsumed);
 
// P4b: and "subsumed" is a CLAIM, not a label. Whenever an arrival leaves
// no trace, the frontier it was measured against really was equal-or-newer.
// Written as an independent modular test, so a broken seq_advances cannot
// satisfy it by agreeing with itself.
property p_subsumed_is_justified;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && !captures && !replaces)
    |-> (v_q && !(((in_seq - seq_q) != '0)
               && ((in_seq - seq_q) < SEQ_W'(WINDOW))));
endproperty
a_subsumed : assert property (p_subsumed_is_justified);
 
// P4c: THE PENDING FRONTIER NEVER MOVES BACKWARD. A stale arrival cannot
// replace a newer pending value.
property p_frontier_monotonic;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && $past(out_valid) && !$past(fire) && !$stable(out_seq))
    |-> (((out_seq - $past(out_seq)) != '0)
      && ((out_seq - $past(out_seq)) < SEQ_W'(WINDOW)));
endproperty
a_monotonic_frontier : assert property (p_frontier_monotonic);
 
// P4d: a pending frontier is STABLE while stalled unless REPLACED by a
// verified newer arrival. Catches spontaneous mutation.
property p_pending_stable_unless_replaced;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && !out_ready && !replaces) |=> (out_valid && $stable(out_seq));
endproperty
a_stable : assert property (p_pending_stable_unless_replaced);
 
// P4e: THE RACE. Consume and arrive in the same cycle, with the arrival
// advancing: the old frontier is delivered AND the new one is captured.
property p_consume_and_capture;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && out_ready && in_valid && adv)
    |=> (out_valid && (out_seq == $past(in_seq)));
endproperty
a_race : assert property (p_consume_and_capture);
 
// P4f: NOT A QUEUE. Three advancing arrivals while stalled produce ONE
// delivered event naming the newest -- not three.
property p_coalesces_not_queues;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && out_ready) |-> (out_seq == newest_arrived_seq);
endproperty
a_coalesce : assert property (p_coalesces_not_queues);
 
// P5: THE LAYER PROPERTY. A decoded acknowledgement never produces a
// Transaction Layer event (Chapter 15.1 section 6).
property p_not_a_completion;
  @(posedge clk) disable iff (!rst_n)
  (ack_hit || out_valid) |-> !(tl_cpl_valid || tl_mem_valid);
endproperty
a_layer : assert property (p_not_a_completion);
 
// ---- GENERATION ------------------------------------------------------
 
// P6: PENDING PROGRESS IS MONOTONIC in the sequence window. It never names
// less progress than the receiver has made. Modular, not unsigned.
property p_pending_monotonic;
  @(posedge clk) disable iff (!rst_n)
  (pending_valid && !$stable(pending_seq))
    |-> (((pending_seq - $past(pending_seq)) != '0)
      && ((pending_seq - $past(pending_seq)) < SEQ_W'(WINDOW)));
endproperty
a_monotonic : assert property (p_pending_monotonic);
 
// P7: pending progress reflects ACCEPTED progress only. Bound against the
// receive tracker so an acknowledgement can never name a gap.
property p_pending_tracks_accepted;
  @(posedge clk) disable iff (!rst_n)
  (pending_valid && !$stable(pending_seq)) |-> $past(rx_accept);
endproperty
a_accepted_only : assert property (p_pending_tracks_accepted);
 
// P8: ONE PENDING VALUE, NOT A QUEUE (section 4). Three accepts before an
// emit produce ONE descriptor. (req_count is a testbench counter.)
property p_one_descriptor_per_trigger;
  @(posedge clk) disable iff (!rst_n)
  (ack_req_valid && ack_req_ready) |-> (req_count + 1 <= trigger_count);
endproperty
a_one_desc : assert property (p_one_descriptor_per_trigger);
 
// P9: an offered descriptor never names LESS progress than when offered.
// The refresh may only increase it (section 8).
property p_offer_never_regresses;
  @(posedge clk) disable iff (!rst_n)
  (ack_req_valid && !ack_req_ready && !$stable(ack_req_seq))
    |-> (((ack_req_seq - $past(ack_req_seq)) != '0)
      && ((ack_req_seq - $past(ack_req_seq)) < SEQ_W'(WINDOW)));
endproperty
a_offer_forward : assert property (p_offer_never_regresses);
 
// P10: an emitted descriptor never names progress beyond what is pending.
property p_offer_within_pending;
  @(posedge clk) disable iff (!rst_n)
  (ack_req_valid && pending_valid)
    |-> ((pending_seq - ack_req_seq) < SEQ_W'(WINDOW));
endproperty
a_within_pending : assert property (p_offer_within_pending);
 
// P11: reset clears every stage that owns progress.
property p_reset_clears;
  @(posedge clk)
  !rst_n |=> (!out_valid && !ack_req_valid && !pending_valid && !subsumed);
endproperty
a_reset : assert property (p_reset_clears);