High-Speed Data Movement — Keeping the Link Busy Without Breaking Anything

available Link bandwidth
  × transaction efficiency        payload / (payload + overhead)      §8
  × ability to keep work in flight   Tags, credits, descriptors       §§6-7
  × ability to absorb what returns   completion buffering, sink rate  §12

bandwidth  ≈  bytes_in_flight / round_trip_latency

required bytes in flight  ≈  target_bandwidth × round_trip_latency
required requests         ≈  ceil(bytes_in_flight / request_size)

ceiling  ≈  tags × request_size / round_trip_latency

can_issue =  tag_available
          && credit_available
          && buffer_space_reserved
          && link_request_ready
          && work_available

reserved_bytes  ≤  capacity        always

required buffering  ≥  arrival_rate × maximum_expected_stall

// SYNTHESIZABLE. Multi-resource admission control (section 9).
// EVERY TERM IS REQUIRED. Section 16 measured an admission check that used
// only tags and work: it issues without credit or buffer in 18.6% of
// resource states -- which is a flow-control violation, not a stall.
//
// THIS BLOCK DOES NOT IMPLEMENT PCIe FLOW CONTROL. It consumes a
// normalized grant from the credit manager (Module 16).
module dma_admission (
  input  logic tag_available,        // section 14's allocator
  input  logic credit_granted,       // NORMALIZED grant, not a raw counter (§10)
  input  logic buffer_reserved,      // section 15
  input  logic tx_request_ready,
  input  logic work_available,
  output logic issue_allowed
);
  // A conjunction, deliberately flat and readable: any future edit that
  // drops a term is visible in review rather than buried in an FSM.
  assign issue_allowed = tag_available
                      && credit_granted
                      && buffer_reserved
                      && tx_request_ready
                      && work_available;
endmodule

// SYNTHESIZABLE. Multi-Tag allocator with an optional rotating search.
// DEEPENS Chapter 20.3 section 15's allocator: same lease semantics, plus
// same-cycle free-and-allocate and a fairness option.
//
// Section 16: 600,000 random operations across TAGS in {1,2,3,8,32},
// including simultaneous free+alloc -- 0 disagreements with an
// independent set model.
module tag_pool #(
  parameter int TAGS       = 32,
  parameter bit ROTATE     = 1,           // 1 = round-robin search (§ fairness)
  parameter int TW = (TAGS <= 1) ? 1 : $clog2(TAGS)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic          alloc_req,
  output logic          alloc_valid,
  output logic [TW-1:0] alloc_tag,
 
  input  logic          free_req,
  input  logic [TW-1:0] free_tag,
 
  output logic [TAGS-1:0] busy_map,
  output logic [TW:0]     free_count,     // one bit wider: 0..TAGS
  output logic            err_bad_free
);
  generate if (TAGS < 1) $error("TAGS must be at least 1"); endgenerate
 
  logic [TAGS-1:0] busy_q;
  logic [TW-1:0]   rr_q;
  logic            bad_q;
  assign busy_map     = busy_q;
  assign err_bad_free = bad_q;
 
  // Free count is a real count, not a popcount recomputed downstream --
  // section 15's reservation logic needs it every cycle.
  always_comb begin
    free_count = '0;
    for (int i = 0; i < TAGS; i++) if (!busy_q[i]) free_count = free_count + 1;
  end
 
  // ==================================================================
  // SEARCH ORDER IS A FAIRNESS POLICY, NOT A CORRECTNESS ONE (§ below).
  // A fixed low-index-first search is functionally correct and repeatedly
  // favours low Tag IDs -- which is harmless protocol-wise and can skew
  // lab observation and latency distribution. ROTATE makes it round-robin.
  // PCIe REQUIRES NO TAG FAIRNESS; this is implementation policy.
  // ==================================================================
  logic [TW-1:0] pick;
  logic          found;
  always_comb begin
    pick = '0; found = 1'b0;
    for (int k = TAGS-1; k >= 0; k--) begin
      int idx = ROTATE ? ((int'(rr_q) + k) % TAGS) : k;
      if (!busy_q[idx]) begin pick = TW'(idx); found = 1'b1; end
    end
  end
  assign alloc_valid = alloc_req && found;
  assign alloc_tag   = pick;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin busy_q <= '0; rr_q <= '0; bad_q <= 1'b0; end
    else begin
      // ==============================================================
      // SAME-CYCLE FREE AND ALLOCATE IS THE STEADY STATE of a busy
      // engine: a context retiring while a new request issues. Free is
      // applied first so the released Tag is immediately re-allocatable.
      // ==============================================================
      if (free_req) begin
        if (free_tag < TW'(TAGS) && busy_q[free_tag]) busy_q[free_tag] <= 1'b0;
        else bad_q <= 1'b1;                       // double or out-of-range free
      end
      if (alloc_valid) begin
        busy_q[alloc_tag] <= 1'b1;
        rr_q <= (alloc_tag == TW'(TAGS-1)) ? '0 : (alloc_tag + TW'(1));
      end
    end
  end
endmodule

// SYNTHESIZABLE. Reserve sink capacity BEFORE issuing (section 12).
// RESERVE-THEN-ISSUE, RELEASE-ON-COMMIT. Reserving after the request is
// issued is too late: the Completion is already coming.
module completion_reservation #(
  parameter int CAPACITY_BYTES = 16384,
  parameter int CW = $clog2(CAPACITY_BYTES + 1)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic [CW-1:0] req_bytes,
  input  logic          reserve_req,
  output logic          reserve_ok,
 
  input  logic          release_valid,
  input  logic [CW-1:0] release_bytes,
 
  output logic [CW-1:0] reserved_bytes,
  output logic [CW-1:0] free_bytes,
  output logic          almost_full,
  output logic          err_over_release
);
  logic [CW-1:0] res_q;
  logic          over_q;
  assign reserved_bytes  = res_q;
  assign free_bytes      = CW'(CAPACITY_BYTES) - res_q;
  assign almost_full     = (free_bytes < CW'(CAPACITY_BYTES/8));
  assign err_over_release = over_q;
 
  // ADMISSION USES FREE CAPACITY, not a full bit -- a request needs a
  // specific number of bytes, and "not full" does not mean "enough".
  assign reserve_ok = reserve_req && (req_bytes <= free_bytes);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin res_q <= '0; over_q <= 1'b0; end
    else begin
      unique case ({reserve_ok, release_valid})
        2'b10: res_q <= res_q + req_bytes;
        2'b01: if (release_bytes <= res_q) res_q <= res_q - release_bytes;
               else over_q <= 1'b1;                   // released more than held
        2'b11: begin
                 // Same cycle: net the two so the invariant never breaks
                 // transiently (section 20's audit).
                 if (release_bytes <= res_q) res_q <= res_q - release_bytes + req_bytes;
                 else over_q <= 1'b1;
               end
        default: ;
      endcase
    end
  end
  // INVARIANT: reserved_bytes <= CAPACITY_BYTES, always (P8).
endmodule

// SYNTHESIZABLE. Job epoch -- the stale-prefetch defence (section 11).
// IMPLEMENTATION POLICY, and the epoch is LOCAL: it is never transmitted
// over PCIe and has no protocol meaning.
//
// Section 16: without this, 161,182 stale descriptors executed across
// 40,000 randomized abort sequences. With it, 0.
module job_epoch #(parameter int EW = 4) (
  input  logic clk,
  input  logic rst_n,
  input  logic job_start,
  input  logic job_abort,
 
  input  logic [EW-1:0] item_epoch,     // carried with each prefetched item
  input  logic          item_valid,
  output logic          item_is_stale,
 
  output logic [EW-1:0] current_epoch
);
  logic [EW-1:0] ep_q;
  assign current_epoch = ep_q;
  // Wrap is harmless: a stale item would need exactly 2^EW epoch changes
  // to alias, and the FIFO is far shallower than that.
  assign item_is_stale = item_valid && (item_epoch != ep_q);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)                    ep_q <= '0;
    else if (job_abort || job_start) ep_q <= ep_q + EW'(1);
  end
endmodule

// SYNTHESIZABLE. Assemble small source beats into efficient payloads (§8).
// BOUNDED THREE WAYS so it never waits forever: the target size, the end
// of a descriptor, and an explicit flush. Waiting only for the target
// would stall a transfer whose final bytes never reach it.
//
// Section 16: 60,000 random (beat, target, ready) cases -- byte
// conservation `accepted == emitted + buffered` held in every one.
module payload_packer #(
  parameter int TARGET_BYTES = 256,
  parameter int BUF_BYTES    = 1024,
  parameter int BW = $clog2(BUF_BYTES + 1)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic          in_valid,
  output logic          in_ready,
  input  logic [7:0]    in_bytes,        // beat size, normalized
  input  logic          in_last,         // end of descriptor -> flush
 
  output logic          pkt_valid,
  input  logic          pkt_ready,
  output logic [BW-1:0] pkt_bytes,
  output logic          pkt_last,
 
  output logic [BW-1:0] buffered_bytes
);
  logic [BW-1:0] buf_q;
  logic          last_q;
  assign buffered_bytes = buf_q;
 
  // Accept while there is room for a maximum beat -- never overflow.
  assign in_ready = (buf_q + BW'(255) <= BW'(BUF_BYTES));
 
  wire have_target = (buf_q >= BW'(TARGET_BYTES));
  // EMIT ON TARGET **OR** ON FLUSH. The second condition is what makes a
  // final short payload emit at all (section 20, mutation 11).
  assign pkt_valid = have_target || (last_q && (buf_q != '0));
  assign pkt_bytes = have_target ? BW'(TARGET_BYTES) : buf_q;
  assign pkt_last  = last_q && !have_target;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin buf_q <= '0; last_q <= 1'b0; end
    else begin
      // Both directions on their own handshake. Same-cycle in and out is
      // the normal case at speed, and the arithmetic must net correctly.
      unique case ({in_valid && in_ready, pkt_valid && pkt_ready})
        2'b10: buf_q <= buf_q + BW'(in_bytes);
        2'b01: buf_q <= buf_q - pkt_bytes;
        2'b11: buf_q <= buf_q + BW'(in_bytes) - pkt_bytes;
        default: ;
      endcase
      if (in_valid && in_ready && in_last) last_q <= 1'b1;
      if (pkt_valid && pkt_ready && pkt_last) last_q <= 1'b0;
    end
  end
endmodule

// SYNTHESIZABLE. One shared PCIe transmit opportunity, several producers.
// GRANT IS HELD UNTIL THE TRANSFER COMPLETES (section 20's counterexample).
// A combinational priority encoder re-evaluated every cycle changes the
// selected producer while `valid && !ready`, so the request that finally
// transfers is not the one that was offered.
module tx_arbiter #(
  parameter int N = 4,
  parameter int IW = (N <= 1) ? 1 : $clog2(N)
) (
  input  logic clk,
  input  logic rst_n,
  input  logic [N-1:0] req,
  input  logic         down_ready,
  output logic [N-1:0] grant,
  output logic         grant_valid,
  output logic [IW-1:0] grant_idx
);
  logic [IW-1:0] owner_q, rr_q;
  logic          held_q;
 
  assign grant_valid = held_q;
  assign grant_idx   = owner_q;
  always_comb begin
    grant = '0;
    if (held_q) grant[owner_q] = 1'b1;
  end
 
  // Round-robin from the last owner: no producer is starved while it keeps
  // requesting. FAIRNESS IS IMPLEMENTATION POLICY, not a PCIe requirement.
  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 (req[idx]) begin pick = IW'(idx); found = 1'b1; end
    end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin held_q <= 1'b0; owner_q <= '0; rr_q <= '0; end
    else begin
      if (!held_q) begin
        if (found) begin owner_q <= pick; held_q <= 1'b1; end
      end else if (down_ready) begin
        // ==========================================================
        // OWNERSHIP RELEASED ONLY ON AN ACTUAL TRANSFER. Not when the
        // requester deasserts, not on a timer. Section 16 verified
        // conservation across 60,000 runs: transfers never exceeded
        // offers.
        // ==========================================================
        held_q <= 1'b0;
        rr_q   <= (owner_q == IW'(N-1)) ? '0 : (owner_q + IW'(1));
      end
    end
  end
endmodule

// SYNTHESIZABLE. Bottleneck attribution -- the chapter's debugging tool.
// EVERY COUNTER IS DIAGNOSTIC ONLY and drives no functional signal (P12).
// Priority is DECLARED so simultaneous causes are attributed consistently
// rather than double-counted.
module dma_bottleneck #(parameter int CW = 32) (
  input  logic clk,
  input  logic rst_n,
  input  logic tx_valid, tx_ready,
  input  logic work_available, tag_available, credit_granted, buffer_reserved,
  input  logic clear,
 
  output logic [CW-1:0] tx_busy_cycles,
  output logic [CW-1:0] tx_stall_cycles,
  output logic [CW-1:0] no_work_cycles,
  output logic [CW-1:0] no_tag_cycles,
  output logic [CW-1:0] no_credit_cycles,
  output logic [CW-1:0] no_buffer_cycles
);
  logic [CW-1:0] busy_q, stall_q, work_q, tag_q, cred_q, buf_q;
  assign {tx_busy_cycles, tx_stall_cycles} = {busy_q, stall_q};
  assign {no_work_cycles, no_tag_cycles}   = {work_q, tag_q};
  assign {no_credit_cycles, no_buffer_cycles} = {cred_q, buf_q};
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      busy_q<='0; stall_q<='0; work_q<='0; tag_q<='0; cred_q<='0; buf_q<='0;
    end else begin
      // ==============================================================
      // DECLARED PRIORITY (section 19's ladder reads these in this order):
      //   a transfer happened          -> busy
      //   offered but not accepted     -> downstream stall
      //   otherwise, the FIRST missing resource, in a fixed order
      //
      // Without a declared order, a cycle missing two resources is
      // counted twice and the percentages stop summing.
      // ==============================================================
      if (tx_valid && tx_ready)        begin if(!(&busy_q))  busy_q  <= busy_q  + CW'(1); end
      else if (tx_valid && !tx_ready)  begin if(!(&stall_q)) stall_q <= stall_q + CW'(1); end
      else if (!work_available)        begin if(!(&work_q))  work_q  <= work_q  + CW'(1); end
      else if (!tag_available)         begin if(!(&tag_q))   tag_q   <= tag_q   + CW'(1); end
      else if (!credit_granted)        begin if(!(&cred_q))  cred_q  <= cred_q  + CW'(1); end
      else if (!buffer_reserved)       begin if(!(&buf_q))   buf_q   <= buf_q   + CW'(1); end
    end
  end
endmodule

// SVA over the high-speed blocks. LOCAL contract only. Nothing asserts
// that downstream becomes ready, that credits are returned, that
// Completions arrive, or that any bandwidth is achieved.
 
// ---- ADMISSION --------------------------------------------------------
 
// P1: ISSUE REQUIRES EVERY RESOURCE. Section 16 measured a two-term check:
// it issues without credit or buffer in 18.6% of resource states.
property p_admission_complete;
  @(posedge clk) disable iff (!rst_n)
  issue_allowed |-> (tag_available && credit_granted && buffer_reserved
                                   && tx_request_ready && work_available);
endproperty
a_adm : assert property (p_admission_complete);
 
// ---- TAG POOL ---------------------------------------------------------
 
// P2: AN ALLOCATED TAG WAS PREVIOUSLY FREE -- no double allocation.
property p_alloc_was_free;
  @(posedge clk) disable iff (!rst_n)
  alloc_valid |-> !busy_map[alloc_tag];
endproperty
a_alloc : assert property (p_alloc_was_free);
 
// P3: A TAG STAYS BUSY UNTIL EXPLICITLY FREED -- the lease from 20.3 §9.
property p_tag_lease;
  @(posedge clk) disable iff (!rst_n)
  (busy_map[t] && !(free_req && (free_tag == TW'(t)))) |=> busy_map[t];
endproperty
a_lease : assert property (p_tag_lease);
 
// P3b: freeing a non-busy or out-of-range Tag is REPORTED.
property p_bad_free;
  @(posedge clk) disable iff (!rst_n)
  (free_req && ((free_tag >= TW'(TAGS)) || !busy_map[free_tag])) |=> err_bad_free;
endproperty
a_badfree : assert property (p_bad_free);
 
// P4: THE OUTSTANDING COUNT EQUALS THE LIVE CONTEXT POPULATION. A drift
// here is a leak that stays invisible until Tags exhaust (mutation 18).
property p_outstanding_matches;
  @(posedge clk) disable iff (!rst_n)
  ($countones(busy_map) + free_count) == (TW+1)'(TAGS);
endproperty
a_pop : assert property (p_outstanding_matches);
 
// ---- SHARED RESOURCES -------------------------------------------------
 
// P5: A GRANT IS CONSUMED BY AT MOST ONE PRODUCER. The property section
// 16's first counterexample violates -- two engines spending one credit.
property p_single_consumer;
  @(posedge clk) disable iff (!rst_n)
  $onehot0(grant);
endproperty
a_one : assert property (p_single_consumer);
 
// ---- COMPLETION RESERVATION -------------------------------------------
 
// P8: RESERVED BYTES NEVER EXCEED CAPACITY. The core sink invariant.
property p_reservation_bounded;
  @(posedge clk) disable iff (!rst_n)
  reserved_bytes <= CW'(CAPACITY_BYTES);
endproperty
a_res : assert property (p_reservation_bounded);
 
// P8b: reservation happens BEFORE issue, never after (section 12).
property p_reserve_before_issue;
  @(posedge clk) disable iff (!rst_n)
  issue_allowed |-> buffer_reserved;
endproperty
a_pre : assert property (p_reserve_before_issue);
 
// P9: RELEASE IS BOUNDED AND EXACTLY ONCE -- releasing more than is held
// is reported, not silently wrapped (mutation 19).
property p_release_bounded;
  @(posedge clk) disable iff (!rst_n)
  (release_valid && (release_bytes > reserved_bytes)) |=> err_over_release;
endproperty
a_rel : assert property (p_release_bounded);
 
// ---- PAYLOAD PACKER ---------------------------------------------------
 
// P10: BYTE CONSERVATION. Section 16 verified this across 60,000 random
// (beat, target, ready) cases with zero violations.
property p_packer_conserves;
  @(posedge clk) disable iff (!rst_n)
  (buffered_bytes <= BW'(BUF_BYTES))
  && ((pkt_valid && pkt_ready) |-> (pkt_bytes <= buffered_bytes));
endproperty
a_pack : assert property (p_packer_conserves);
 
// P10b: THE FINAL PARTIAL PAYLOAD IS EMITTED. Without the flush condition
// a descriptor's tail is stranded forever (mutation 11).
property p_final_flush;
  @(posedge clk) disable iff (!rst_n)
  (last_q && (buffered_bytes != '0)) |-> pkt_valid;
endproperty
a_flush : assert property (p_final_flush);
 
// P11: THROUGHPUT ACCOUNTING COUNTS TRANSFERS, NOT OFFERS. The rule from
// 18.9 §15, 19.5 §15, 20.1 §19 -- fourth module, same law.
property p_count_on_fire;
  @(posedge clk) disable iff (!rst_n)
  (tx_busy_cycles > $past(tx_busy_cycles)) |-> ($past(tx_valid) && $past(tx_ready));
endproperty
a_cnt : assert property (p_count_on_fire);
 
// P12: DIAGNOSTICS DO NOT AFFECT FUNCTION. A counter that gates behaviour
// is a functional block wearing a diagnostic label (section 15).
property p_counters_inert;
  @(posedge clk) disable iff (!rst_n)
  clear |-> ($stable(issue_allowed) || $past(tx_ready) || $past(work_available));
endproperty
a_inert : assert property (p_counters_inert);
 
// ---- ARBITER ----------------------------------------------------------
 
// P13: THE GRANT IS STABLE UNDER STALL. Section 16's second counterexample
// is the combinational encoder that moves it mid-transaction.
property p_grant_held;
  @(posedge clk) disable iff (!rst_n)
  (grant_valid && !down_ready) |=> (grant_valid && $stable(grant_idx));
endproperty
a_hold : assert property (p_grant_held);
 
// P13b: and it is released ONLY on an actual transfer, not when the
// requester deasserts.
property p_release_on_transfer;
  @(posedge clk) disable iff (!rst_n)
  ($fell(grant_valid)) |-> $past(down_ready);
endproperty
a_reltx : assert property (p_release_on_transfer);
 
// ---- PREFETCH ---------------------------------------------------------
 
// P14: THE PREFETCH FIFO NEVER OVERFLOWS OR UNDERFLOWS.
property p_fifo_bounded;
  @(posedge clk) disable iff (!rst_n)
  (prefetch_count <= PF_W'(PREFETCH_DEPTH));
endproperty
a_fifo : assert property (p_fifo_bounded);
 
// P15: A STALE-EPOCH ITEM CANNOT EXECUTE. Section 16: 161,182 stale
// descriptors executed without this check, 0 with it.
property p_no_stale_execute;
  @(posedge clk) disable iff (!rst_n)
  item_is_stale |-> !descriptor_executes;
endproperty
a_stale : assert property (p_no_stale_execute);
 
// P15b: an abort or a new job changes the epoch, so everything already in
// the FIFO becomes stale by construction.
property p_epoch_advances;
  @(posedge clk) disable iff (!rst_n)
  (job_abort || job_start) |=> (current_epoch != $past(current_epoch));
endproperty
a_epoch : assert property (p_epoch_advances);
 
// P16: reset clears every ownership -- no Tag, reservation or grant
// survives.
property p_reset;
  @(posedge clk)
  !rst_n |=> ((busy_map == '0) && (reserved_bytes == '0) && !grant_valid);
endproperty
a_reset : assert property (p_reset);

                    PHASE A          PHASE B           PHASE C
                 1 outstanding   32 outstanding   32 outstanding
cycle           1   2   3   4  |  5   6   7   8  |  9  10  11  12
desc_ready      1   1   1   1  |  1   1   1   1  |  1   1   1   1
request_valid   1   0   0   0  |  1   1   1   1  |  1   1   0   0
request_ready   1   0   0   0  |  1   1   1   1  |  1   1   0   0
outstanding     1   1   1   1  | 12  20  28  32  | 32  32  32  32
tag_free_count 31  31  31  31  | 20  12   4   0  |  4   2   0   0
np_credit_ok    1   1   1   1  |  1   1   1   1  |  1   1   0   0
cpl_buf_free   16k 16k 16k 16k | 12k  8k  4k  2k |  1k  0   0   0
cpl_valid       0   0   0   1  |  0   1   1   1  |  1   1   1   1
tx_utilized     1   0   0   0  |  1   1   1   1  |  1   1   0   0
stall_reason    -  RTT RTT RTT |  -   -   -   -  |  -   -  CRD BUF