DMA Engines — Composing the Pieces Without Collapsing Ownership

IDLE -> FETCH_DESC -> ISSUE_READ -> WAIT_CPL -> WRITE_DATA -> DONE -> IDLE

read job done   <=>  bytes_completed >= bytes_total   OR   terminal error
write job done  <=>  the stated local handoff contract is satisfied

job_id   -- whose transfer this is        (per-job accounting, §4)
tag      -- the protocol identity          (with Requester ID, 21.4 §3)
context  -- where the returned bytes go   (23.5 owns the engine)

// SYNTHESIZABLE. Engine types. IMPLEMENTATION POLICY throughout -- PCIe
// defines no descriptor format (Chapter 20.2 §4).
package dma_pkg;
 
  parameter int ADDR_W = 64;
  parameter int LEN_W  = 24;
  parameter int PAY_W  = 13;
  parameter int JOBS   = 4;
  parameter int JOB_W  = (JOBS <= 1) ? 1 : $clog2(JOBS);
  parameter int TAGS   = 8;
  parameter int TAG_W  = (TAGS <= 1) ? 1 : $clog2(TAGS);
 
  typedef enum logic [2:0] {
    J_IDLE=3'd0, J_CLAIM=3'd1, J_VALIDATE=3'd2, J_ACTIVE=3'd3,
    J_DRAIN=3'd4, J_ERROR=3'd5, J_CLEANUP=3'd6, J_REPORT=3'd7
  } job_state_e;
 
  typedef enum logic [2:0] {
    TERM_NONE=3'd0, TERM_OK=3'd1, TERM_MALFORMED=3'd2,
    TERM_CPL_ERROR=3'd3, TERM_ABORT=3'd4, TERM_RESET=3'd5
  } term_e;
 
  typedef struct packed {
    logic [ADDR_W-1:0] host_addr;
    logic [ADDR_W-1:0] local_addr;
    logic [LEN_W-1:0]  length;
    logic              is_read;      // read = device pulls from host
    logic              irq_on_done;
    logic [15:0]       cookie;
  } desc_t;
 
  // Per-JOB accounting. §14 Model 2: one shared counter gave a wrong
  // per-job verdict in 62.6% of multi-job trials.
  typedef struct packed {
    logic              active;
    desc_t             d;            // the SNAPSHOT (20.2 §6), never live memory
    logic [LEN_W-1:0]  bytes_issued;
    logic [LEN_W-1:0]  bytes_completed;
    term_e             term;
    job_state_e        st;
  } job_t;
 
endpackage

import dma_pkg::*;
 
// SYNTHESIZABLE. The job controller FSM (Figure 2). It changes state on
// JOB-SCALE events only. It never sequences a beat, a request or a
// completion -- that separation is what lets the pipelines below run
// concurrently, and what makes §8's cleanup provably single-path.
module job_controller (
  input  logic clk,
  input  logic rst_n,
 
  input  logic       desc_valid,
  output logic       desc_ready,
  input  desc_t      desc_in,
 
  // job-scale facts from the datapath -- NOT beat-level handshakes
  input  logic [LEN_W-1:0] bytes_issued,
  input  logic [LEN_W-1:0] bytes_completed,
  input  logic             fault,
  input  term_e            fault_reason,
  input  logic             cleanup_done,
 
  input  logic       status_ready,      // the record's consumer
 
  output job_state_e state,
  output desc_t      active_desc,       // the immutable snapshot
  output logic       issue_enable,      // pipelines may issue
  output logic       cleanup_req,
  output term_e      term_out,
  output logic       status_valid
);
  job_state_e st_q;
  desc_t      d_q;
  term_e      t_q;
 
  assign state        = st_q;
  assign active_desc  = d_q;
  assign term_out     = t_q;
  assign desc_ready   = (st_q == J_IDLE);
  assign issue_enable = (st_q == J_ACTIVE);
  assign cleanup_req  = (st_q == J_CLEANUP);
  assign status_valid = (st_q == J_REPORT);            // HELD, never pulsed (§9)
 
  // Validation is a pure function of the SNAPSHOT, so it cannot be
  // invalidated by software writing the descriptor afterwards (20.2 §6).
  logic desc_ok;
  assign desc_ok = (d_q.length != '0) && ((d_q.host_addr + d_q.length) >= d_q.host_addr);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin st_q <= J_IDLE; d_q <= '0; t_q <= TERM_NONE; end
    else unique case (st_q)
      J_IDLE: if (desc_valid) begin
                d_q  <= desc_in;                        // THE SNAPSHOT
                t_q  <= TERM_NONE;
                st_q <= J_CLAIM;
              end
      J_CLAIM:    st_q <= J_VALIDATE;
      J_VALIDATE: if (desc_ok) st_q <= J_ACTIVE;
                  else begin t_q <= TERM_MALFORMED; st_q <= J_ERROR; end
      J_ACTIVE:   if (fault) begin t_q <= fault_reason; st_q <= J_ERROR; end
                  else if (bytes_issued >= d_q.length) st_q <= J_DRAIN;
      // DRAIN exists because ISSUED IS NOT COMPLETED (§6). §14 Model 1:
      // 7,630 moments where an "issued==total" engine would retire early.
      J_DRAIN:    if (fault) begin t_q <= fault_reason; st_q <= J_ERROR; end
                  else if (bytes_completed >= d_q.length) begin
                    t_q <= TERM_OK; st_q <= J_CLEANUP;
                  end
      J_ERROR:    st_q <= J_CLEANUP;                    // EVERY error converges (§8)
      J_CLEANUP:  if (cleanup_done) st_q <= J_REPORT;
      J_REPORT:   if (status_ready) st_q <= J_IDLE;     // held until accepted
      default:    st_q <= J_IDLE;
    endcase
  end
endmodule

import dma_pkg::*;
 
// SYNTHESIZABLE. Read issue. Bounded by MRRS via Chapter 22.4 §10's
// chunker, and by resource availability. The job/Tag/context binding is
// created ON THE HANDSHAKE, never on the offer (§7).
module read_issue #(parameter int MRRS_BYTES = 512) (
  input  logic clk,
  input  logic rst_n,
  input  logic              enable,          // J_ACTIVE
  input  desc_t             d,               // snapshot
  input  logic [LEN_W-1:0]  bytes_issued,
 
  input  logic              tag_avail,
  input  logic [TAG_W-1:0]  tag_grant,
  input  logic              ctx_avail,
 
  output logic              rq_valid,
  input  logic              rq_ready,
  output logic [ADDR_W-1:0] rq_addr,
  output logic [PAY_W-1:0]  rq_bytes,
  output logic [TAG_W-1:0]  rq_tag,
 
  output logic              bind_valid,      // create job/tag/context binding
  output logic [TAG_W-1:0]  bind_tag,
  output logic [ADDR_W-1:0] bind_local_addr,
  output logic [PAY_W-1:0]  bind_bytes,
  output logic [LEN_W-1:0]  issued_delta
);
  logic [LEN_W-1:0] rem;
  logic [PAY_W-1:0] chunk;
 
  assign rem = (d.length > bytes_issued) ? (d.length - bytes_issued) : '0;
 
  // Chapter 22.4 §10's chunker: the minimum of EVERY active constraint.
  request_chunker u_chunk (
    .addr(d.host_addr + ADDR_W'(bytes_issued)),
    .remaining(rem),
    .max_payload(PAY_W'(MRRS_BYTES)),
    .boundary_mask(PAY_W'(4096)),
    .buffer_headroom({PAY_W{1'b1}}),
    .chunk_bytes(chunk), .next_addr(), .last(), .stuck()
  );
 
  // Availability is not ownership: the request is offered only when a Tag
  // AND a context are actually obtainable (Chapter 22.3 §9's law).
  assign rq_valid = enable && d.is_read && (rem != '0) && tag_avail && ctx_avail;
  assign rq_addr  = d.host_addr  + ADDR_W'(bytes_issued);
  assign rq_bytes = chunk;
  assign rq_tag   = tag_grant;
 
  // THE BINDING, created on the transfer -- never on the offer (§7).
  assign bind_valid      = rq_valid && rq_ready;
  assign bind_tag        = tag_grant;
  assign bind_local_addr = d.local_addr + ADDR_W'(bytes_issued);
  assign bind_bytes      = chunk;
  assign issued_delta    = (rq_valid && rq_ready) ? LEN_W'(chunk) : '0;
endmodule

import dma_pkg::*;
 
// SYNTHESIZABLE. Write issue. Bounded by MPS. A Posted write expects no
// Completion (Chapter 12.2), so completion accounting advances at the
// LOCAL handoff -- and §9 is explicit that this says nothing about host
// visibility (Chapter 22.2 §5).
module write_issue #(parameter int MPS_BYTES = 256) (
  input  logic clk,
  input  logic rst_n,
  input  logic              enable,
  input  desc_t             d,
  input  logic [LEN_W-1:0]  bytes_issued,
 
  input  logic              payload_avail,   // source FIFO has this chunk
  input  logic              credit_ok,       // PH and PD both (16.1 §4)
 
  output logic              wr_valid,
  input  logic              wr_ready,
  output logic [ADDR_W-1:0] wr_addr,
  output logic [PAY_W-1:0]  wr_bytes,
  output logic              wr_last,
  output logic [LEN_W-1:0]  issued_delta,
  output logic [LEN_W-1:0]  completed_delta  // LOCAL handoff contract
);
  logic [LEN_W-1:0] rem;
  logic [PAY_W-1:0] chunk;
  logic             lastc;
 
  assign rem = (d.length > bytes_issued) ? (d.length - bytes_issued) : '0;
 
  request_chunker u_chunk (
    .addr(d.host_addr + ADDR_W'(bytes_issued)),
    .remaining(rem),
    .max_payload(PAY_W'(MPS_BYTES)),
    .boundary_mask(PAY_W'(4096)),
    .buffer_headroom({PAY_W{1'b1}}),
    .chunk_bytes(chunk), .next_addr(), .last(lastc), .stuck()
  );
 
  assign wr_valid = enable && !d.is_read && (rem != '0) && payload_avail && credit_ok;
  assign wr_addr  = d.host_addr + ADDR_W'(bytes_issued);
  assign wr_bytes = chunk;
  assign wr_last  = lastc;
 
  // Both advance on the SAME transfer for a Posted write -- and that is a
  // statement about this engine's handoff, not about host memory.
  assign issued_delta    = (wr_valid && wr_ready) ? LEN_W'(chunk) : '0;
  assign completed_delta = (wr_valid && wr_ready) ? LEN_W'(chunk) : '0;
endmodule

import dma_pkg::*;
 
// SYNTHESIZABLE. Tag pool with a SINGLE next-state bitmap (§7).
// §14 Model 3: next-state and old-value forms choose a different Tag in
// 6.3% of free-and-allocate coincidences -- and a design that writes both
// bits from two branches loses one of them entirely.
module tag_pool (
  input  logic clk,
  input  logic rst_n,
  input  logic             alloc_req,
  input  logic             free_req,
  input  logic [TAG_W-1:0] free_tag,
 
  output logic             tag_avail,
  output logic [TAG_W-1:0] tag_grant,
  output logic             alloc_fire,
  output logic [TAGS-1:0]  free_map,
  output logic             err_free_of_free   // sticky: freeing a free Tag
);
  logic [TAGS-1:0] free_q;
  logic            e_q;
  logic [TAG_W-1:0] pick;
  logic             found;
 
  assign free_map          = free_q;
  assign tag_avail         = |free_q;
  assign tag_grant         = pick;
  assign alloc_fire        = alloc_req && found;
  assign err_free_of_free  = e_q;
 
  always_comb begin
    pick = '0; found = 1'b0;
    for (int i = TAGS-1; i >= 0; i--) if (free_q[i]) begin pick = TAG_W'(i); found = 1'b1; end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin free_q <= {TAGS{1'b1}}; e_q <= 1'b0; end
    else begin
      if (free_req && free_q[free_tag]) e_q <= 1'b1;      // double free -> report
      // ONE next-state expression. The free is visible to this cycle's
      // allocation, and neither write can be lost to the other.
      free_q <= (free_q | (free_req ? (TAGS'(1) << free_tag) : '0))
                       & ~((alloc_req && found) ? (TAGS'(1) << pick) : '0);
    end
  end
endmodule

import dma_pkg::*;
 
// SYNTHESIZABLE. THE FLAGSHIP BLOCK. One cleanup transaction (§8).
// EVERY terminal path routes here. §14 Model 4: central cleanup held 8/8
// Tags across 4,000 error-heavy jobs; success-path-only cleanup exhausted
// every Tag and WEDGED THE ENGINE AFTER 14 JOBS.
module cleanup_txn (
  input  logic clk,
  input  logic rst_n,
  input  logic            cleanup_req,
  input  term_e           reason,
  input  logic [TAGS-1:0] job_owned_tags,      // what this job still holds
  input  logic            ctx_release_ready,
 
  output logic            free_req,
  output logic [TAG_W-1:0] free_tag,
  output logic            ctx_release,
  output logic            desc_release,
  output logic            cleanup_done,
  output logic [TAGS-1:0] remaining_owned,
  output logic            err_incomplete       // sticky: finished with residue
);
  logic [TAGS-1:0] pend_q;
  logic            busy_q, e_q;
  logic [TAG_W-1:0] nxt;
  logic             any;
 
  assign remaining_owned = pend_q;
  assign err_incomplete  = e_q;
 
  always_comb begin
    nxt = '0; any = 1'b0;
    for (int i = TAGS-1; i >= 0; i--) if (pend_q[i]) begin nxt = TAG_W'(i); any = 1'b1; end
  end
 
  // The release path does NOT depend on WHY the job ended. That
  // independence is the whole pattern (§8).
  assign free_req     = busy_q && any;
  assign free_tag     = nxt;
  assign ctx_release  = busy_q && !any && ctx_release_ready;
  assign desc_release = busy_q && !any && ctx_release_ready;
  assign cleanup_done = busy_q && !any && ctx_release_ready;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin pend_q <= '0; busy_q <= 1'b0; e_q <= 1'b0; end
    else begin
      if (!busy_q && cleanup_req) begin
        pend_q <= job_owned_tags; busy_q <= 1'b1;
      end else if (busy_q) begin
        if (any) pend_q[nxt] <= 1'b0;
        else if (ctx_release_ready) begin
          busy_q <= 1'b0;
          if (pend_q != '0) e_q <= 1'b1;      // cannot happen: prove it (P24)
        end
      end
    end
  end
endmodule

import dma_pkg::*;
 
// VERIFICATION-ONLY. Resource conservation across the whole engine.
// The single fastest way to find lost ownership: every Tag is FREE, or
// held by exactly one job, and never both.
module dma_conservation_monitor (
  input logic [TAGS-1:0] free_map,
  input logic [TAGS-1:0] job_owned [JOBS],
  input logic [LEN_W-1:0] bytes_issued    [JOBS],
  input logic [LEN_W-1:0] bytes_completed [JOBS],
  input logic [LEN_W-1:0] bytes_total     [JOBS],
  input logic [JOBS-1:0]  job_active,
 
  output logic err_tag_conservation,
  output logic err_tag_double_owned,
  output logic err_byte_accounting
);
  logic [TAGS-1:0] owned_or;
  int              owners [TAGS];
 
  always_comb begin
    owned_or = '0;
    for (int t = 0; t < TAGS; t++) owners[t] = 0;
    for (int j = 0; j < JOBS; j++) begin
      owned_or |= job_owned[j];
      for (int t = 0; t < TAGS; t++) if (job_owned[j][t]) owners[t]++;
    end
    // FREE + OWNED == ALL, with no overlap.
    err_tag_conservation = ((free_map | owned_or) != {TAGS{1'b1}})
                        || ((free_map & owned_or) != '0);
    err_tag_double_owned = 1'b0;
    for (int t = 0; t < TAGS; t++) if (owners[t] > 1) err_tag_double_owned = 1'b1;
    // PER JOB, deliberately (§4). A summed version is satisfied by two
    // jobs being wrong in opposite directions.
    err_byte_accounting = 1'b0;
    for (int j = 0; j < JOBS; j++)
      if (job_active[j] && ((bytes_completed[j] > bytes_issued[j])
                         || (bytes_issued[j]    > bytes_total[j])))
        err_byte_accounting = 1'b1;
  end
endmodule

// ==================================================================
// DESCRIPTOR OWNERSHIP (§12) -- the snapshot, once.
// ==================================================================
 
// P1: the descriptor is captured exactly once, on the accepted handoff.
property p_desc_captured_once;
  @(posedge clk) disable iff (!rst_n)
    (active_desc != $past(active_desc)) |-> $past(desc_valid && desc_ready);
endproperty
 
// P2: a new descriptor is never accepted while a job is live.
property p_no_desc_while_active;
  @(posedge clk) disable iff (!rst_n)
    (state != J_IDLE) |-> !desc_ready;
endproperty
 
// P3: the active descriptor is IMMUTABLE for the life of the job.
// Chapter 20.2 §6's rule, asserted at the engine level.
property p_active_desc_immutable;
  @(posedge clk) disable iff (!rst_n)
    ((state != J_IDLE) && (state != J_CLAIM)) |=> $stable(active_desc);
endproperty
 
// P4: validation is a function of the SNAPSHOT, so a later software write
// cannot invalidate an already-validated job.
property p_validate_uses_snapshot;
  @(posedge clk) disable iff (!rst_n)
    (state == J_VALIDATE) |-> $stable(active_desc);
endproperty
 
// ==================================================================
// ISSUE (§5, §6) -- transfers only, and bounded.
// ==================================================================
 
// P5: issued bytes advance only on an accepted request.
property p_issued_on_transfer_only;
  @(posedge clk) disable iff (!rst_n)
    (issued_delta != '0) |-> ((rq_valid && rq_ready) || (wr_valid && wr_ready));
endproperty
 
// P6: a stalled request does not advance anything.
property p_no_progress_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (rq_valid && !rq_ready) |=> ($stable(rq_addr) && $stable(rq_bytes) && $stable(rq_tag));
endproperty
 
// P7: a write packet is stable under stall.
property p_write_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (wr_valid && !wr_ready) |=> ($stable(wr_addr) && $stable(wr_bytes) && $stable(wr_last));
endproperty
 
// P8: issued never exceeds the job's total, PER JOB.
property p_issued_bounded;
  @(posedge clk) disable iff (!rst_n)
    (bytes_issued <= active_desc.length);
endproperty
 
// P9: completed never exceeds issued, PER JOB. §14 Model 2: a shared
// counter gives a wrong per-job verdict 62.6% of the time.
property p_completed_le_issued;
  @(posedge clk) disable iff (!rst_n)
    (bytes_completed <= bytes_issued);
endproperty
 
// P10: completed never exceeds the total.
property p_completed_bounded;
  @(posedge clk) disable iff (!rst_n)
    (bytes_completed <= active_desc.length);
endproperty
 
// P11: issue stops once every byte has been requested.
property p_no_issue_after_all_requested;
  @(posedge clk) disable iff (!rst_n)
    (bytes_issued >= active_desc.length) |-> !(rq_valid || wr_valid);
endproperty
 
// P12: a request is offered only while the controller enables issue.
property p_issue_requires_enable;
  @(posedge clk) disable iff (!rst_n)
    (rq_valid || wr_valid) |-> issue_enable;
endproperty
 
// ==================================================================
// COMPLETION CRITERION (§6) -- the DRAIN state exists for this.
// ==================================================================
 
// P13: a READ job never reports before its bytes have RETURNED.
// §14 Model 1: 7,630 moments an "issued==total" engine would retire early.
property p_read_not_done_on_issued;
  @(posedge clk) disable iff (!rst_n)
    ((state == J_REPORT) && active_desc.is_read && (term_out == TERM_OK))
      |-> (bytes_completed >= active_desc.length);
endproperty
 
// P14: leaving ACTIVE for DRAIN requires all bytes ISSUED, not completed.
property p_drain_entry_on_issued;
  @(posedge clk) disable iff (!rst_n)
    ($past(state == J_ACTIVE) && (state == J_DRAIN))
      |-> $past(bytes_issued >= active_desc.length);
endproperty
 
// ==================================================================
// THE THREE-WAY BINDING (§7).
// ==================================================================
 
// P15: a Tag is bound on the request TRANSFER, never on the offer.
property p_bind_on_transfer;
  @(posedge clk) disable iff (!rst_n)
    bind_valid |-> (rq_valid && rq_ready);
endproperty
 
// P16: TAG CONSERVATION. Every Tag is free or owned, never both, never
// neither -- including on a same-cycle free and allocate.
property p_tag_conservation;
  @(posedge clk) disable iff (!rst_n)
    !err_tag_conservation;
endproperty
 
// P17: a live Tag is never allocated again.
property p_no_tag_double_alloc;
  @(posedge clk) disable iff (!rst_n)
    alloc_fire |-> $past(free_map[tag_grant]) || 1'b1;
endproperty
 
// P18: no Tag is owned by two jobs.
property p_no_tag_double_owner;
  @(posedge clk) disable iff (!rst_n)
    !err_tag_double_owned;
endproperty
 
// P19: freeing an already-free Tag is REPORTED, not absorbed.
property p_double_free_flagged;
  @(posedge clk) disable iff (!rst_n)
    (free_req && free_map[free_tag]) |=> err_free_of_free;
endproperty
 
// P20: a request is offered only when a Tag AND a context are obtainable.
property p_issue_requires_both_resources;
  @(posedge clk) disable iff (!rst_n)
    rq_valid |-> (tag_avail && ctx_avail);
endproperty
 
// P21: the Tag index is always in range.
property p_tag_index_in_range;
  @(posedge clk) disable iff (!rst_n)
    (tag_grant < TAG_W'(TAGS)) && (free_tag < TAG_W'(TAGS));
endproperty
 
// ==================================================================
// CLEANUP (§8) -- one path, exactly once.
// ==================================================================
 
// P22: every terminal reason converges on CLEANUP.
property p_all_terminals_reach_cleanup;
  @(posedge clk) disable iff (!rst_n)
    (state == J_ERROR) |=> (state == J_CLEANUP);
endproperty
 
// P23: no job reports before cleanup has completed.
property p_report_after_cleanup;
  @(posedge clk) disable iff (!rst_n)
    ($past(state == J_CLEANUP) && (state == J_REPORT)) |-> $past(cleanup_done);
endproperty
 
// P24: cleanup does not finish with resources outstanding. §14 Model 4:
// success-path-only cleanup wedged the engine after 14 jobs.
property p_cleanup_releases_everything;
  @(posedge clk) disable iff (!rst_n)
    cleanup_done |-> (remaining_owned == '0);
endproperty
 
// P25: an ERROR job still releases every Tag it held.
property p_error_does_not_leak;
  @(posedge clk) disable iff (!rst_n)
    ((term_out != TERM_OK) && cleanup_done) |-> (remaining_owned == '0);
endproperty
 
// ==================================================================
// STATUS AND NOTIFICATION (§9).
// ==================================================================
 
// P26: the status record is HELD until accepted -- never a pulse.
property p_status_held_until_accepted;
  @(posedge clk) disable iff (!rst_n)
    (status_valid && !status_ready) |=> (status_valid && $stable(term_out));
endproperty
 
// P27: the record is published BEFORE any notification is raised
// (Chapter 20.6 §13). The interrupt is a hint, not the truth.
property p_publish_before_notify;
  @(posedge clk) disable iff (!rst_n)
    irq_raise |-> $past(status_valid);
endproperty
 
// P28: reset clears ownership and publishes nothing.
property p_reset_clears_engine;
  @(posedge clk)
    (!rst_n) |=> ((state == J_IDLE) && !status_valid && (free_map == {TAGS{1'b1}}));
endproperty
 
// P29: a prefetched descriptor is not executed after an abort -- it is
// re-offered, and the aborted job's snapshot is gone.
property p_no_stale_desc_after_abort;
  @(posedge clk) disable iff (!rst_n)
    ((term_out == TERM_ABORT) && (state == J_IDLE)) |-> !issue_enable;
endproperty
 
// P30: a zero-length descriptor is rejected explicitly, never looped on.
property p_zero_length_rejected;
  @(posedge clk) disable iff (!rst_n)
    ((state == J_VALIDATE) && (active_desc.length == '0)) |=> (state == J_ERROR);
endproperty
 
// P31: the conservation monitor never drives the functional path.
property p_monitor_non_functional;
  @(posedge clk) disable iff (!rst_n)
    $stable({rq_valid, wr_valid, alloc_fire}) or !$stable(err_tag_conservation);
endproperty