DMA Concepts — Ownership, Descriptors and the Lifecycle

host_addr      where in host memory        -- device-visible (20.1 §11)
local_addr     where in device memory
length_bytes   how much
dir_read       direction -- decides MemRd vs MemWr (§1's sourced sentence)
irq_on_done    should completion raise an interrupt?
cookie         software's identifier, returned in the completion

descriptor available   published by software, not yet claimed
      ↓
validated              length, direction, local policy checks (§16)
      ↓
active                 hardware owns it; snapshot taken (§6)
      ↓
issued                 requests handed to the transmit path
      ↓
completed              the work actually happened  (§20.1 §7: NOT the same)
      ↓
retired                the completion record has been accepted by software

bytes_completed  <=  bytes_issued  <=  bytes_total

descriptor queue        depth 8, base address programmed
  write pointer         advanced by SOFTWARE  (producer)
  read pointer          advanced by HARDWARE  (consumer)
 
status queue            depth 16, base address programmed
  ...results flow the other way

// SYNTHESIZABLE. Normalized DMA descriptor and status types.
// THIS IS NOT A PCIe FORMAT (section 4). The DIRECTION field's meaning is
// the sourced part: section 1's vendor text states "the direction of
// transfer would determine what kind of TLP is generated (MWr or MRd)".
package dma_desc_pkg;
 
  parameter int ADDR_W  = 64;
  parameter int LADDR_W = 32;
  parameter int LEN_W   = 24;   // illustrative: up to 16 MiB per descriptor
 
  typedef struct packed {
    logic [ADDR_W-1:0]  host_addr;    // DEVICE-VISIBLE address (20.1 §11)
    logic [LADDR_W-1:0] local_addr;
    logic [LEN_W-1:0]   length_bytes;
    logic               dir_read;     // 1 = host->device (MemRd), 0 = device->host (MemWr)
    logic               irq_on_done;  // section 5
    logic [15:0]        cookie;       // returned in the completion record
  } dma_desc_t;
 
  typedef enum logic [2:0] {
    DST_OK          = 3'd0,
    DST_ERR_LEN     = 3'd1,   // zero length -- local contract
    DST_ERR_ALIGN   = 3'd2,   // local alignment policy
    DST_ERR_CTRL    = 3'd3,   // unsupported control bits
    DST_ERR_XFER    = 3'd4,   // transaction-level failure during execution
    DST_ERR_ABORT   = 3'd5
  } dma_status_e;
 
  typedef struct packed {
    logic [15:0]      cookie;         // matches the descriptor that produced it
    dma_status_e      status;
    logic [LEN_W-1:0] bytes_done;
  } dma_result_t;
 
endpackage

import dma_desc_pkg::*;
 
// SYNTHESIZABLE. Own exactly one descriptor, with an immutable snapshot.
// SECTION 6: once accepted, nothing re-reads the input. Section 17
// measured the alternative -- a live re-read mutates the transfer
// mid-flight, and every request it produces is well-formed.
module dma_desc_owner (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Descriptor input stream -------------------------------------------
  input  dma_desc_t desc_in,
  input  logic      desc_valid,
  output logic      desc_ready,
 
  // ---- The owned, immutable working copy ---------------------------------
  output dma_desc_t desc_active,
  output logic      active,
 
  // Execution reports completion of the owned descriptor.
  input  logic      exec_done,
  input  dma_status_e exec_status,
  input  logic [LEN_W-1:0] exec_bytes,
 
  // ---- Completion record, HELD until accepted (section 10) ---------------
  output dma_result_t result,
  output logic        result_valid,
  input  logic        result_ready
);
 
  dma_desc_t   desc_q;
  dma_result_t res_q;
  logic        act_q, res_v_q;
 
  assign desc_active  = desc_q;
  assign active       = act_q;
  assign result       = res_q;
  assign result_valid = res_v_q;
 
  // ==================================================================
  // SINGLE-ENTRY OWNERSHIP.
  //
  // ready falls while a descriptor is owned OR while its completion
  // record is still unclaimed. The second half is section 9's point:
  // a descriptor is not finished with until its RESULT has been taken,
  // because the cookie and status still belong to it.
  //
  // A design that reopened `ready` at exec_done would let the next
  // descriptor overwrite the result of the last (section 17, mutation 6).
  // ==================================================================
  assign desc_ready = !act_q && !res_v_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      desc_q <= '0; res_q <= '0; act_q <= 1'b0; res_v_q <= 1'b0;
    end else begin
      if (desc_valid && desc_ready) begin
        // SNAPSHOT: the whole descriptor, in one assignment (section 6).
        desc_q <= desc_in;
        act_q  <= 1'b1;
      end else if (act_q && exec_done) begin
        act_q   <= 1'b0;
        // The cookie comes from the OWNED descriptor, not from the input --
        // desc_in may already hold the next one (mutation 7).
        res_q   <= '{ cookie: desc_q.cookie,
                      status: exec_status,
                      bytes_done: exec_bytes };
        res_v_q <= 1'b1;
      end
 
      if (res_v_q && result_ready) res_v_q <= 1'b0;
    end
  end
 
endmodule

import dma_desc_pkg::*;
 
// SYNTHESIZABLE. Local validity checks -- LOCAL CONTRACT, not PCIe rules.
// A zero-length descriptor is the important one: without an explicit
// policy it produces a transfer that can never make progress and never
// retires (section 17, mutation 3).
module dma_desc_validate #(
  parameter int ALIGN_BYTES = 1     // 1 = no alignment requirement
) (
  input  dma_desc_t  desc,
  output logic       desc_ok,
  output dma_status_e err
);
  wire zero_len   = (desc.length_bytes == '0);
  wire misaligned = (ALIGN_BYTES > 1)
                 && ((desc.host_addr & ADDR_W'(ALIGN_BYTES-1)) != '0);
 
  always_comb begin
    if      (zero_len)   begin desc_ok = 1'b0; err = DST_ERR_LEN;   end
    else if (misaligned) begin desc_ok = 1'b0; err = DST_ERR_ALIGN; end
    else                 begin desc_ok = 1'b1; err = DST_OK;        end
  end
  // NOTE: an invalid descriptor still needs CLEAN RETIREMENT (section 16).
  // Refusing it silently would stall the ring; it must produce a result
  // record with an error status so software learns and the slot frees.
endmodule

import dma_desc_pkg::*;
 
// SYNTHESIZABLE. Three quantities, never conflated (section 9).
// FOR POSTED WRITES "completed" is the DMA engine's declared retirement
// boundary, NOT a PCIe Completion (20.1 §6). For reads it is Completion
// data actually received (20.3).
module dma_progress (
  input  logic clk,
  input  logic rst_n,
  input  logic start,
  input  logic [LEN_W-1:0] total,
 
  input  logic issue_fire,                  // request handshake
  input  logic [LEN_W-1:0] issue_bytes,
  input  logic complete_fire,               // retirement event
  input  logic [LEN_W-1:0] complete_bytes,
 
  output logic [LEN_W-1:0] bytes_total,
  output logic [LEN_W-1:0] bytes_issued,
  output logic [LEN_W-1:0] bytes_completed,
  output logic             all_issued,
  output logic             all_completed
);
  logic [LEN_W-1:0] tot_q, iss_q, cpl_q;
  assign {bytes_total, bytes_issued, bytes_completed} = {tot_q, iss_q, cpl_q};
 
  // ==================================================================
  // all_issued IS NOT all_completed, and only the second may retire a
  // transfer. Chapter 20.1 section 19 measured the conflation for reads:
  // it declares completion early in 99.5% of cases.
  // ==================================================================
  assign all_issued    = (iss_q >= tot_q) && (tot_q != '0);
  assign all_completed = (cpl_q >= tot_q) && (tot_q != '0);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)      begin tot_q<='0; iss_q<='0; cpl_q<='0; end
    else if (start)  begin tot_q<=total; iss_q<='0; cpl_q<='0; end
    else begin
      // ON HANDSHAKES ONLY. Chapter 20.1 measured advancing on `valid`:
      // it exceeds the total in 79.5% of cases.
      if (issue_fire)    iss_q <= iss_q + issue_bytes;
      if (complete_fire) cpl_q <= cpl_q + complete_bytes;
    end
  end
endmodule

// SYNTHESIZABLE. Ring pointer with EXPLICIT wrap and an EXPLICIT count.
// SECTION 13: binary overflow produced an out-of-range pointer in 19.9%
// of increments across non-power-of-two depths (section 17).
// SECTION 12: pointers alone cannot distinguish full from empty --
// 66,032 ambiguous states measured -- so occupancy is a counter.
module dma_ring_ptr #(
  parameter int DEPTH = 8,
  parameter int PTR_W = (DEPTH <= 1) ? 1 : $clog2(DEPTH),
  parameter int CNT_W = (DEPTH <= 1) ? 1 : $clog2(DEPTH + 1)
) (
  input  logic clk,
  input  logic rst_n,
  input  logic push,          // producer advances
  input  logic pop,           // consumer advances
 
  output logic [PTR_W-1:0] wr_ptr,
  output logic [PTR_W-1:0] rd_ptr,
  output logic [CNT_W-1:0] occupancy,
  output logic             full,
  output logic             empty
);
  generate
    if (DEPTH < 1) $error("DEPTH must be at least 1");
    if ((1 << CNT_W) < (DEPTH + 1)) $error("CNT_W too narrow to hold DEPTH");
  endgenerate
 
  logic [PTR_W-1:0] w_q, r_q;
  logic [CNT_W-1:0] c_q;
  assign {wr_ptr, rd_ptr, occupancy} = {w_q, r_q, c_q};
 
  // UNAMBIGUOUS by construction -- no phase bit needed, no slot sacrificed.
  assign full  = (c_q == CNT_W'(DEPTH));
  assign empty = (c_q == '0);
 
  // EXPLICIT WRAP AT DEPTH-1, matching section 1's sourced pseudo-code
  // ("roll over to 0 when pointer == max queue size-1"). NOT binary
  // overflow, which is only correct for power-of-two depths.
  function automatic logic [PTR_W-1:0] nxt(input logic [PTR_W-1:0] p);
    return (p == PTR_W'(DEPTH-1)) ? '0 : (p + PTR_W'(1));
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin w_q <= '0; r_q <= '0; c_q <= '0; end
    else begin
      // PUSH AND POP IN THE SAME CYCLE leave occupancy unchanged -- both
      // pointers advance. A design that handled only one would corrupt the
      // count on simultaneous producer/consumer activity (section 18).
      if (push && !full)  w_q <= nxt(w_q);
      if (pop  && !empty) r_q <= nxt(r_q);
      case ({push && !full, pop && !empty})
        2'b10:   c_q <= c_q + CNT_W'(1);
        2'b01:   c_q <= c_q - CNT_W'(1);
        default: c_q <= c_q;                 // 2'b00 and 2'b11
      endcase
    end
  end
endmodule

// SVA over the descriptor blocks. LOCAL contract only. Nothing asserts
// that software supplies descriptors, consumes results, or that execution
// ever finishes.
 
// ---- ENVIRONMENT ------------------------------------------------------
assume property (@(posedge clk) disable iff (!rst_n)
  (desc_valid && !desc_ready) |=> (desc_valid && $stable(desc_in)));
 
// ---- OWNERSHIP AND THE SNAPSHOT ---------------------------------------
 
// P1: THE WORKING DESCRIPTOR IS IMMUTABLE WHILE ACTIVE. Section 6's law,
// and section 19's counterexample is its violation.
property p_snapshot_immutable;
  @(posedge clk) disable iff (!rst_n)
  (active && !$rose(active)) |-> $stable(desc_active);
endproperty
a_snap : assert property (p_snapshot_immutable);
 
// P2: a descriptor is captured EXACTLY ONCE, on the handshake.
property p_capture_once;
  @(posedge clk) disable iff (!rst_n)
  $rose(active) |-> (desc_active == $past(desc_in))
                 && ($past(desc_valid) && $past(desc_ready));
endproperty
a_cap : assert property (p_capture_once);
 
// P3: NO SECOND DESCRIPTOR while one is owned or its result unclaimed.
property p_single_entry;
  @(posedge clk) disable iff (!rst_n)
  (active || result_valid) |-> !desc_ready;
endproperty
a_single : assert property (p_single_entry);
 
// ---- VALIDATION -------------------------------------------------------
 
// P4: A ZERO-LENGTH DESCRIPTOR NEVER REACHES EXECUTION, and produces an
// error result exactly once (section 15).
property p_zero_len_refused;
  @(posedge clk) disable iff (!rst_n)
  (desc_valid && desc_ready && (desc_in.length_bytes == '0))
    |=> (!active && result_valid && (result.status == DST_ERR_LEN));
endproperty
a_zero : assert property (p_zero_len_refused);
 
// ---- PROGRESS ---------------------------------------------------------
 
// P5: the ordering of the three quantities (section 9).
property p_progress_ordered;
  @(posedge clk) disable iff (!rst_n)
  (bytes_completed <= bytes_issued) && (bytes_issued <= bytes_total);
endproperty
a_order : assert property (p_progress_ordered);
 
// P6: both counters advance ONLY on their handshake.
property p_issued_on_fire;
  @(posedge clk) disable iff (!rst_n)
  (bytes_issued > $past(bytes_issued)) |-> $past(issue_fire);
endproperty
a_iss : assert property (p_issued_on_fire);
 
// P7: RETIREMENT REQUIRES COMPLETED BYTES, never issued bytes.
property p_done_on_completed;
  @(posedge clk) disable iff (!rst_n)
  (exec_done && (exec_status == DST_OK)) |-> all_completed;
endproperty
a_done : assert property (p_done_on_completed);
 
// ---- COMPLETION RECORD ------------------------------------------------
 
// P8: the result is HELD and STABLE until accepted (section 10). Section
// 19's second counterexample is the pulsed version.
property p_result_held;
  @(posedge clk) disable iff (!rst_n)
  (result_valid && !result_ready) |=> (result_valid && $stable(result));
endproperty
a_held : assert property (p_result_held);
 
// P8b: THE COOKIE MATCHES THE DESCRIPTOR THAT PRODUCED IT, not whatever
// is on the input now (mutation 7).
property p_cookie_matches;
  @(posedge clk) disable iff (!rst_n)
  $rose(result_valid) |-> (result.cookie == $past(desc_active.cookie));
endproperty
a_cookie : assert property (p_cookie_matches);
 
// P8c: every accepted descriptor eventually produces exactly one result --
// stated as conservation rather than as liveness (section 20).
property p_conservation;
  @(posedge clk) disable iff (!rst_n)
  accepted_count == (CNT_W'(active) + CNT_W'(result_valid) + retired_count);
endproperty
a_conserve : assert property (p_conservation);
 
// ---- RING -------------------------------------------------------------
 
// P9: THE POINTER IS ALWAYS IN RANGE. Section 17: binary overflow put it
// out of range in 19.9% of increments at non-power-of-two depths.
property p_ptr_range;
  @(posedge clk) disable iff (!rst_n)
  (wr_ptr < PTR_W'(DEPTH)) && (rd_ptr < PTR_W'(DEPTH));
endproperty
a_ptr : assert property (p_ptr_range);
 
// P10: occupancy is bounded and cannot underflow or overflow.
property p_occ_bounded;
  @(posedge clk) disable iff (!rst_n) occupancy <= CNT_W'(DEPTH);
endproperty
a_occ : assert property (p_occ_bounded);
 
// P10b: FULL AND EMPTY ARE UNAMBIGUOUS -- the property that pointer-only
// designs cannot state (section 12).
property p_full_empty_distinct;
  @(posedge clk) disable iff (!rst_n)
  !(full && empty) && (full |-> (occupancy == CNT_W'(DEPTH)))
                   && (empty |-> (occupancy == '0));
endproperty
a_fe : assert property (p_full_empty_distinct);
 
// P11: HARDWARE DOES NOT CONSUME PAST THE PUBLISHED BOUNDARY (section 8's
// hardware half).
property p_no_speculative_consume;
  @(posedge clk) disable iff (!rst_n)
  (pop && !empty) |-> (occupancy != '0);
endproperty
a_pub : assert property (p_no_speculative_consume);
 
// P12: simultaneous push and pop leaves occupancy unchanged.
property p_push_pop;
  @(posedge clk) disable iff (!rst_n)
  (push && !full && pop && !empty) |=> $stable(occupancy);
endproperty
a_pp : assert property (p_push_pop);
 
// P13: reset clears ownership -- no stale descriptor or result survives.
property p_reset;
  @(posedge clk)
  !rst_n |=> (!active && !result_valid && (occupancy == '0));
endproperty
a_reset : assert property (p_reset);