Packet Forwarding — Moving a TLP Across a Switch

Endpoint A → Switch      A's TLP acknowledged by the SWITCH's ingress DLL
Switch    → Endpoint B   a DIFFERENT transmission, with its own sequence
                         number, its own credits, and its own ACK from B

ingress accepts a COMPLETE TLP
      ↓
an internal packet record owns it        header + payload handle + route (§5)
      ↓
the egress arbiter grants it             §9
      ↓
the egress transfer completes            all beats accepted
      ↓
the internal owner retires               and only now is the buffer freed

// SYNTHESIZABLE. Normalized internal switch packet.
// NOT A TLP WIRE FORMAT. The routing decision is already made
// (Chapter 21.1) and travels WITH the packet from here on.
package switch_fwd_pkg;
 
  parameter int N_PORT = 4;
  parameter int PORT_W = (N_PORT <= 1) ? 1 : $clog2(N_PORT);
  parameter int SLOTS  = 8;
  parameter int SLOT_W = (SLOTS  <= 1) ? 1 : $clog2(SLOTS);
  parameter int LEN_W  = 12;
 
  // Section 1: the ingress credit handler has separate thresholds for
  // Posted, Non-Posted and Completion. The class travels with the packet
  // because egress credit is per-class too.
  typedef enum logic [1:0] { FC_P = 2'd0, FC_NP = 2'd1, FC_CPL = 2'd2 } fc_class_e;
 
  typedef struct packed {
    logic                valid;
    logic [PORT_W-1:0]   ingress_port;
    logic [PORT_W-1:0]   egress_port;    // THE SNAPSHOTTED ROUTE (§5)
    logic                to_upstream;    // 21.1's default direction
    fc_class_e           fc_class;
    logic [2:0]          tc;
    logic [LEN_W-1:0]    payload_bytes;
    logic [SLOT_W-1:0]   payload_handle; // NOT the payload itself
  } switch_pkt_t;
 
endpackage

import switch_fwd_pkg::*;
 
// SYNTHESIZABLE. Own the payload buffer slots.
// FREED AT RETIREMENT ONLY (§6). Section 14 measured freeing at grant:
// 100.0% of stalled sequences had the payload overwritten underneath a
// packet that was still in flight.
module pkt_slot_alloc #(
  parameter int N = SLOTS,
  parameter int W = (N <= 1) ? 1 : $clog2(N)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic         alloc_req,
  output logic         alloc_valid,
  output logic [W-1:0] alloc_slot,
 
  // Asserted ONLY when the egress transfer has fully completed.
  input  logic         retire_req,
  input  logic [W-1:0] retire_slot,
 
  output logic [N-1:0] busy_map,
  output logic         no_slots,
  output logic         err_bad_free
);
  generate if (N < 1) $error("SLOTS must be at least 1"); endgenerate
 
  logic [N-1:0] busy_q; logic bad_q;
  assign busy_map     = busy_q;
  assign no_slots     = (&busy_q);
  assign err_bad_free = bad_q;
 
  logic [W-1:0] pick; logic found;
  always_comb begin
    pick='0; found=1'b0;
    for (int i = N-1; i >= 0; i--) if (!busy_q[i]) begin pick=W'(i); found=1'b1; end
  end
  assign alloc_valid = alloc_req && found;
  assign alloc_slot  = pick;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin busy_q <= '0; bad_q <= 1'b0; end
    else begin
      // Retire first, so a slot freed this cycle is immediately reusable --
      // the steady state of a busy switch.
      if (retire_req) begin
        if (retire_slot < W'(N) && busy_q[retire_slot]) busy_q[retire_slot] <= 1'b0;
        else bad_q <= 1'b1;                  // double or out-of-range free
      end
      if (alloc_valid) busy_q[alloc_slot] <= 1'b1;
    end
  end
endmodule

import switch_fwd_pkg::*;
 
// SYNTHESIZABLE. Accept a complete TLP at ingress and take ownership.
// THE ROUTE IS CAPTURED WITH THE PACKET (§5). Section 14 measured
// re-reading the routing table while buffered: the egress port changed
// under stall in 56.7% of cases.
module ingress_owner (
  input  logic clk,
  input  logic rst_n,
 
  input  logic              in_valid,
  output logic              in_ready,
  input  logic [PORT_W-1:0] in_ingress_port,
  input  fc_class_e         in_class,
  input  logic [LEN_W-1:0]  in_bytes,
 
  // From Chapter 21.1's decoder -- consulted ONCE, at acceptance.
  input  logic              route_valid,
  input  logic [PORT_W-1:0] route_port,
  input  logic              route_upstream,
  input  logic              route_ambiguous,
 
  input  logic              slot_valid,
  input  logic [SLOT_W-1:0] slot_id,
  output logic              slot_req,
 
  output switch_pkt_t       pkt,
  input  logic              pkt_taken,        // egress retired it
 
  output logic              err_no_route
);
  switch_pkt_t p_q; logic err_q;
  assign pkt          = p_q;
  assign err_no_route = err_q;
 
  // ==================================================================
  // NO ACCEPTANCE WITHOUT A ROUTE AND A SLOT.
  //
  // Accepting a packet with nowhere to put it, or with no decided
  // destination, means either dropping it later or holding it in a
  // register that the next packet overwrites (§13, mutation 11).
  // ==================================================================
  wire route_ok = (route_valid || route_upstream) && !route_ambiguous;
  assign slot_req = in_valid && !p_q.valid && route_ok;
  assign in_ready = !p_q.valid && route_ok && slot_valid;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin p_q <= '0; err_q <= 1'b0; end
    else begin
      if (in_valid && in_ready) begin
        // SNAPSHOT: header metadata, class, and THE ROUTE, in one
        // assignment. Nothing re-reads the routing table afterwards.
        p_q.valid          <= 1'b1;
        p_q.ingress_port   <= in_ingress_port;
        p_q.egress_port    <= route_port;
        p_q.to_upstream    <= route_upstream;
        p_q.fc_class       <= in_class;
        p_q.payload_bytes  <= in_bytes;
        p_q.payload_handle <= slot_id;
      end else if (p_q.valid && pkt_taken) begin
        p_q.valid <= 1'b0;
      end
      if (in_valid && route_ambiguous) err_q <= 1'b1;   // 21.1 §8
    end
  end
endmodule

forward_allowed = packet_available
               && egress_link_operational        Module 18
               && egress_fc_grant                Module 16, per class

Ingress 0 ─┐
Ingress 1 ─┼──►  Egress 3     only one may transfer at a time
Ingress 2 ─┘

import switch_fwd_pkg::*;
 
// SYNTHESIZABLE. Which ingress wants which egress.
// A MATRIX, NOT ONE GLOBAL ARBITER: independent egress ports can transfer
// concurrently, and a single arbiter would serialize a switch that has no
// reason to be serial.
module egress_request_matrix (
  input  switch_pkt_t [N_PORT-1:0] ingress_pkt,
  output logic [N_PORT-1:0][N_PORT-1:0] request   // [egress][ingress]
);
  always_comb begin
    request = '0;
    for (int i = 0; i < N_PORT; i++)
      if (ingress_pkt[i].valid)
        request[ingress_pkt[i].egress_port][i] = 1'b1;
  end
endmodule

import switch_fwd_pkg::*;
 
// SYNTHESIZABLE. THE FLAGSHIP BLOCK. One egress port, several ingress
// requesters, multi-beat packets.
//
// TWO OWNERSHIP RULES, both measured in section 14:
//   grant held until the transfer completes  -- else the request mutates
//   packet locked SOP through EOP            -- else beats interleave (67.0%)
module egress_arbiter #(
  parameter int N = N_PORT,
  parameter int IW = (N <= 1) ? 1 : $clog2(N)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic [N-1:0] request,        // one bit per ingress wanting THIS egress
  input  logic [N-1:0] beat_valid,
  input  logic [N-1:0] beat_sop,
  input  logic [N-1:0] beat_eop,
 
  // Egress legality (section 8) -- a normalized grant, not a credit counter.
  input  logic         link_operational,
  input  logic         fc_grant,
 
  input  logic         out_ready,
  output logic         out_valid,
  output logic [IW-1:0] owner,
  output logic          owner_valid,
  output logic          retire_pulse    // last beat accepted -> free the slot
);
  typedef enum logic { S_IDLE, S_LOCKED } st_e;
  st_e            st_q;
  logic [IW-1:0]  own_q, rr_q;
 
  assign owner       = own_q;
  assign owner_valid = (st_q == S_LOCKED);
 
  // ==================================================================
  // A PACKET IS ONLY OFFERED WHEN IT IS LEGAL TO SEND (section 8).
  // Routing decided WHERE; credit and link state decide WHETHER.
  // ==================================================================
  assign out_valid = (st_q == S_LOCKED) && beat_valid[own_q]
                                        && link_operational && fc_grant;
 
  assign retire_pulse = out_valid && out_ready && beat_eop[own_q];
 
  // Round-robin from the last owner. Fairness is implementation policy;
  // PCIe mandates no particular arbitration here.
  logic [IW-1:0] pick; logic found;
  always_comb begin
    pick='0; found=1'b0;
    for (int k = N-1; k >= 0; k--) begin
      int idx = (int'(rr_q) + k) % N;
      if (request[idx] && beat_sop[idx]) begin pick = IW'(idx); found = 1'b1; end
    end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin st_q <= S_IDLE; own_q <= '0; rr_q <= '0; end
    else begin
      unique case (st_q)
        S_IDLE :
          // ==========================================================
          // SELECTION HAPPENS ONLY AT A START-OF-PACKET.
          //
          // Choosing mid-packet is how beats from two TLPs end up
          // interleaved into one malformed packet -- section 14 measured
          // 67.0% of two-stream runs.
          // ==========================================================
          if (found) begin own_q <= pick; st_q <= S_LOCKED; end
 
        S_LOCKED :
          // ==========================================================
          // LOCKED UNTIL THE LAST BEAT IS ACCEPTED. Not until the
          // requester deasserts, not on a timer, and NOT re-evaluated
          // when another ingress becomes higher priority.
          // ==========================================================
          if (out_valid && out_ready && beat_eop[own_q]) begin
            st_q <= S_IDLE;
            rr_q <= (own_q == IW'(N-1)) ? '0 : (own_q + IW'(1));
          end
 
        default : st_q <= S_IDLE;
      endcase
    end
  end
endmodule

// SVA over the forwarding blocks. LOCAL contract only. Nothing asserts
// that an egress becomes ready, that credit is granted, or that any packet
// is ever delivered.
 
// ---- SLOT OWNERSHIP ---------------------------------------------------
 
// P1: a slot is allocated only if it was free -- no double allocation.
property p_alloc_was_free;
  @(posedge clk) disable iff (!rst_n) alloc_valid |-> !busy_map[alloc_slot];
endproperty
a_alloc : assert property (p_alloc_was_free);
 
// P2: an invalid or out-of-range free is REPORTED, not applied.
property p_bad_free;
  @(posedge clk) disable iff (!rst_n)
  (retire_req && ((retire_slot >= W'(N)) || !busy_map[retire_slot])) |=> err_bad_free;
endproperty
a_free : assert property (p_bad_free);
 
// P3: OUTSTANDING PACKETS EQUAL LIVE SLOTS -- a drift here is a leak that
// stays invisible until the switch stops accepting.
property p_slot_population;
  @(posedge clk) disable iff (!rst_n)
  $countones(busy_map) == live_packet_count;
endproperty
a_pop : assert property (p_slot_population);
 
// ---- PACKET METADATA --------------------------------------------------
 
// P4: THE ROUTE IS STABLE WHILE THE PACKET IS OWNED. Section 14 measured
// re-reading the routing table: 56.7% changed destination under stall.
property p_route_stable;
  @(posedge clk) disable iff (!rst_n)
  (pkt.valid && !pkt_taken) |=> (pkt.valid && $stable(pkt.egress_port)
                                           && $stable(pkt.to_upstream));
endproperty
a_route : assert property (p_route_stable);
 
// P4b: and so is the payload handle -- metadata and payload must not drift
// apart (mutation 22).
property p_handle_stable;
  @(posedge clk) disable iff (!rst_n)
  (pkt.valid && !pkt_taken) |=> $stable(pkt.payload_handle);
endproperty
a_handle : assert property (p_handle_stable);
 
// P5: a packet is accepted only with a decided route and an owned slot.
property p_accept_needs_route_and_slot;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && in_ready) |-> ((route_valid || route_upstream)
                              && !route_ambiguous && slot_valid);
endproperty
a_accept : assert property (p_accept_needs_route_and_slot);
 
// ---- ARBITRATION ------------------------------------------------------
 
// P6: THE SLOT IS FREED ONLY AT RETIREMENT. Section 14: freeing at grant
// corrupted the payload in 100.0% of stalled sequences.
property p_free_on_retire;
  @(posedge clk) disable iff (!rst_n)
  retire_req |-> (out_valid && out_ready && beat_eop[owner]);
endproperty
a_retire : assert property (p_free_on_retire);
 
// P7: AT MOST ONE INGRESS OWNS AN EGRESS at a time.
property p_single_owner;
  @(posedge clk) disable iff (!rst_n) $onehot0(grant_vec);
endproperty
a_one : assert property (p_single_owner);
 
// P7b: and one packet is never granted to two egresses.
property p_one_destination;
  @(posedge clk) disable iff (!rst_n)
  $onehot0({egress_owns[0][i], egress_owns[1][i],
            egress_owns[2][i], egress_owns[3][i]});
endproperty
a_dest : assert property (p_one_destination);
 
// P8: THE GRANT IS STABLE UNDER STALL.
property p_grant_held;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && !out_ready) |=> (owner_valid && $stable(owner));
endproperty
a_hold : assert property (p_grant_held);
 
// P9: THE PACKET OWNER IS STABLE FROM SOP TO EOP -- no mid-packet source
// switch. Section 14: 67.0% malformed without this.
property p_packet_locked;
  @(posedge clk) disable iff (!rst_n)
  (owner_valid && !(out_valid && out_ready && beat_eop[owner]))
    |=> (owner_valid && $stable(owner));
endproperty
a_lock : assert property (p_packet_locked);
 
// P9b: selection happens only at a start-of-packet.
property p_select_at_sop;
  @(posedge clk) disable iff (!rst_n)
  $rose(owner_valid) |-> $past(beat_sop[pick]);
endproperty
a_sop : assert property (p_select_at_sop);
 
// ---- LEGALITY ---------------------------------------------------------
 
// P10: NO TRANSFER WITHOUT AN OPERATIONAL EGRESS LINK.
property p_link_required;
  @(posedge clk) disable iff (!rst_n) out_valid |-> link_operational;
endproperty
a_link : assert property (p_link_required);
 
// P11: NO TRANSFER WITHOUT THE EGRESS FLOW-CONTROL GRANT. Routing never
// overrides credit (section 8).
property p_credit_required;
  @(posedge clk) disable iff (!rst_n) out_valid |-> fc_grant;
endproperty
a_credit : assert property (p_credit_required);
 
// P12: a packet is never transmitted twice.
property p_no_duplicate;
  @(posedge clk) disable iff (!rst_n)
  retire_pulse |=> !(out_valid && (owner == $past(owner))
                                && (pkt_id == $past(pkt_id)));
endproperty
a_dup : assert property (p_no_duplicate);
 
// P13: a packet is not retired before its final transfer.
property p_no_early_retire;
  @(posedge clk) disable iff (!rst_n)
  pkt_taken |-> $past(retire_pulse);
endproperty
a_early : assert property (p_no_early_retire);
 
// P14: beat data is stable while the egress stalls.
property p_beat_stable;
  @(posedge clk) disable iff (!rst_n)
  (out_valid && !out_ready) |=> $stable(out_beat);
endproperty
a_beat : assert property (p_beat_stable);
 
// ---- CROSS-LINK INDEPENDENCE ------------------------------------------
 
// P15: NO DLLP IS FORWARDED. Section 1: DLLPs are handled within the DLL
// logic of the port that received them (§4).
property p_no_dllp_forward;
  @(posedge clk) disable iff (!rst_n)
  dut_ingress.dllp_received |-> !dut_egress.tlp_offered_this_cycle;
endproperty
a_dllp : assert property (p_no_dllp_forward);
 
// P16: an ingress ACK does not depend on the egress transfer (§3).
property p_ack_independent;
  @(posedge clk) disable iff (!rst_n)
  dut_ingress.ack_sent |-> !$past(egress_transfer_required);
endproperty
a_ack : assert property (p_ack_independent);
 
// P17: reset clears ownership -- no live slot, no locked owner.
property p_reset;
  @(posedge clk)
  !rst_n |=> ((busy_map == '0) && !owner_valid && !pkt.valid);
endproperty
a_reset : assert property (p_reset);