SSD Controllers — Two Meanings of the Word Completion

host                                   controller
 write command into a submission queue (in HOST memory)
 ring the doorbell  ─────────────────► queue manager notices
                                       DMA READ the queue entry  ◄── the controller
                                       command is now owned          fetches its own work
                                       DMA READ or WRITE payload
                                       media pipeline
                                       DMA WRITE the completion entry
                                       interrupt
 read the completion entry from HOST memory

host: writes one or more command entries into the submission queue in memory
host: writes the new tail value to that queue's doorbell register
ctrl: notices the queue is non-empty
ctrl: issues a Memory Read to fetch the entry (or entries)
ctrl: the command is owned only when that read's data returns

1  host builds the command                  host owns it
2  host advances the doorbell                announced; still host-visible memory
3  controller fetches the entry              in flight
4  fetch data returns                        CONTROLLER OWNS THE COMMAND
5  payload moves, media completes             controller owns the result
6  CQE written into host memory               result published
7  interrupt raised                           host is told to look
8  host consumes the CQE, advances head       queue slot reusable

package nvme_dbg_pkg;
 
  // The controller's own view of a command's lifetime. This is LOCAL state,
  // not an NVMe-defined status: §7's ownership steps, made observable.
  typedef enum logic [2:0] {
    CS_IDLE      = 3'd0,
    CS_FETCHING  = 3'd1,   // SQE read issued, data not yet returned
    CS_OWNED     = 3'd2,   // fetch returned; the command is ours (step 4)
    CS_MOVING    = 3'd3,   // payload in flight
    CS_MEDIA     = 3'd4,   // media pipeline working
    CS_PUBLISH   = 3'd5,   // CQE write issued
    CS_NOTIFY    = 3'd6    // interrupt pending
  } cmd_state_e;
 
  typedef enum logic [0:0] { DIR_READ = 1'b0, DIR_WRITE = 1'b1 } xfer_dir_e;
 
  function automatic int unsigned gw(input int unsigned n);
    return (n <= 1) ? 1 : $clog2(n);
  endfunction
 
  // A normalized data-movement request. NVMe's actual data-pointer structures
  // (PRP lists, SGLs) are STANDARD-DEFINED and are deliberately not modelled
  // here — see 20.4 for scatter-gather handling and the NVMe specification
  // for the real encodings.
  typedef struct packed {
    logic [15:0] cmd_id;
    logic [15:0] queue_id;
    xfer_dir_e   dir;
    logic [63:0] host_addr;
    logic [31:0] buf_addr;      // controller-local buffer
    logic [31:0] bytes;
  } xfer_desc_t;
 
endpackage

module nvme_doorbell_capture #(
  parameter int unsigned NQUEUE = 8
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                  bar_wr_valid,
  input  logic [31:0]                           bar_wr_offset,
  input  logic [31:0]                           bar_wr_data,
  input  logic [nvme_dbg_pkg::gw(NQUEUE)-1:0]   decoded_qid,   // decode owned by 23.2
  input  logic                                  decoded_is_sq,
  output logic                                  db_valid,
  output logic [nvme_dbg_pkg::gw(NQUEUE)-1:0]   db_qid,
  output logic                                  db_is_sq,
  output logic [31:0]                           db_value,
  input  logic                                  db_ready,
  output logic                                  qid_range_error
);
 
  import nvme_dbg_pkg::*;
 
  logic [NQUEUE-1:0] pend_sq, pend_cq;
  logic [31:0]       val_sq [NQUEUE];
  logic [31:0]       val_cq [NQUEUE];
  logic [gw(NQUEUE)-1:0] sel;
  logic sel_is_sq;
 
  // A doorbell naming a queue outside the configured range is REPORTED, not
  // wrapped. Wrapping turns a host software error into execution on an
  // unrelated queue (mutation 6), and the resulting corruption is attributed
  // to whichever queue the index happened to alias onto.
  assign qid_range_error = bar_wr_valid && (decoded_qid >= gw(NQUEUE)'(NQUEUE));
 
  always_comb begin
    sel = '0; sel_is_sq = 1'b1;
    for (int i = NQUEUE-1; i >= 0; i--) if (pend_cq[i]) begin sel = gw(NQUEUE)'(i); sel_is_sq = 1'b0; end
    for (int i = NQUEUE-1; i >= 0; i--) if (pend_sq[i]) begin sel = gw(NQUEUE)'(i); sel_is_sq = 1'b1; end
    db_valid  = (pend_sq != '0) || (pend_cq != '0);
    db_qid    = sel;
    db_is_sq  = sel_is_sq;
    db_value  = sel_is_sq ? val_sq[sel] : val_cq[sel];
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      pend_sq <= '0; pend_cq <= '0;
      for (int i = 0; i < NQUEUE; i++) begin val_sq[i] <= '0; val_cq[i] <= '0; end
    end else begin
      if (bar_wr_valid && !qid_range_error) begin
        if (decoded_is_sq) begin val_sq[decoded_qid] <= bar_wr_data; pend_sq[decoded_qid] <= 1'b1; end
        else               begin val_cq[decoded_qid] <= bar_wr_data; pend_cq[decoded_qid] <= 1'b1; end
      end
      if (db_valid && db_ready) begin
        // Suppress the clear if a newer doorbell for the same queue and
        // direction landed this cycle — otherwise that announcement is lost.
        if (!(bar_wr_valid && !qid_range_error &&
              (decoded_qid == sel) && (decoded_is_sq == sel_is_sq))) begin
          if (sel_is_sq) pend_sq[sel] <= 1'b0;
          else           pend_cq[sel] <= 1'b0;
        end
      end
    end
  end
 
endmodule

module nvme_queue_ctx #(
  parameter int unsigned NQUEUE  = 8,
  parameter int unsigned MAXDEPTH = 1024
)(
  input  logic clk,
  input  logic rst_n,
  // configuration (created and deleted by admin commands; the COMMAND
  // formats are NVMe-defined and are not modelled here)
  input  logic                                cfg_valid,
  input  logic [nvme_dbg_pkg::gw(NQUEUE)-1:0] cfg_qid,
  input  logic                                cfg_enable,
  input  logic [nvme_dbg_pkg::gw(MAXDEPTH+1)-1:0] cfg_depth,
  input  logic [63:0]                         cfg_base,
  // doorbell updates
  input  logic                                db_valid,
  input  logic [nvme_dbg_pkg::gw(NQUEUE)-1:0] db_qid,
  input  logic [31:0]                         db_value,
  output logic                                db_range_error,
  // query
  input  logic [nvme_dbg_pkg::gw(NQUEUE)-1:0] q_sel,
  output logic                                q_enabled,
  output logic                                q_nonempty,
  output logic [nvme_dbg_pkg::gw(MAXDEPTH)-1:0] q_head, q_tail,
  output logic [63:0]                         q_base,
  // head advance when a command is fetched
  input  logic                                head_adv,
  input  logic [nvme_dbg_pkg::gw(NQUEUE)-1:0] head_qid
);
 
  import nvme_dbg_pkg::*;
 
  logic [NQUEUE-1:0] en;
  logic [gw(MAXDEPTH+1)-1:0] depth [NQUEUE];
  logic [gw(MAXDEPTH)-1:0]   head  [NQUEUE], tail [NQUEUE];
  logic [63:0]               base  [NQUEUE];
 
  // A doorbell value at or beyond the queue depth is a host error. It is
  // REPORTED and the tail is not updated — accepting it would make the
  // queue appear to contain entries that do not exist (mutation 7).
  assign db_range_error = db_valid && en[db_qid] && (db_value >= 32'(depth[db_qid]));
 
  assign q_enabled  = en[q_sel];
  assign q_head     = head[q_sel];
  assign q_tail     = tail[q_sel];
  assign q_base     = base[q_sel];
  assign q_nonempty = en[q_sel] && (head[q_sel] != tail[q_sel]);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      en <= '0;
      for (int i = 0; i < NQUEUE; i++) begin
        depth[i] <= '0; head[i] <= '0; tail[i] <= '0; base[i] <= '0;
      end
    end else begin
      if (cfg_valid) begin
        en[cfg_qid]    <= cfg_enable;
        depth[cfg_qid] <= cfg_depth;
        base[cfg_qid]  <= cfg_base;
        // Creating or deleting a queue resets its pointers. A queue that is
        // re-created with stale head/tail executes phantom commands.
        head[cfg_qid]  <= '0;
        tail[cfg_qid]  <= '0;
      end
      if (db_valid && en[db_qid] && !db_range_error)
        tail[db_qid] <= gw(MAXDEPTH)'(db_value);
      if (head_adv && en[head_qid])
        head[head_qid] <= (head[head_qid] == gw(MAXDEPTH)'(depth[head_qid]-1))
                        ? '0 : head[head_qid] + 1'b1;
    end
  end
 
endmodule

module nvme_cmd_fetch #(
  parameter int unsigned NQUEUE = 8,
  parameter int unsigned NSLOT  = 32
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                  q_nonempty,
  input  logic [nvme_dbg_pkg::gw(NQUEUE)-1:0]   q_sel,
  input  logic [63:0]                           q_base,
  input  logic [nvme_dbg_pkg::gw(1024)-1:0]     q_head,
  // outbound Memory Read for the queue entry
  output logic                                  rd_valid,
  output logic [63:0]                           rd_addr,
  output logic [11:0]                           rd_bytes,
  output logic [nvme_dbg_pkg::gw(NSLOT)-1:0]    rd_slot,
  input  logic                                  rd_ready,
  // the read's data returning (a PCIe Completion carrying the entry, §4)
  input  logic                                  fetch_data_valid,
  input  logic [nvme_dbg_pkg::gw(NSLOT)-1:0]    fetch_slot,
  input  logic [15:0]                           fetch_cmd_id,
  // the command becomes OWNED here, and only here
  output logic                                  cmd_owned,
  output logic [nvme_dbg_pkg::gw(NSLOT)-1:0]    cmd_slot,
  output logic [15:0]                           cmd_id,
  output logic                                  head_adv,
  output logic [nvme_dbg_pkg::gw(NQUEUE)-1:0]   head_qid
);
 
  import nvme_dbg_pkg::*;
  localparam int unsigned SQE_BYTES = 64;      // IMPLEMENTATION POLICY
 
  logic [NSLOT-1:0] slot_busy;
  logic [gw(NSLOT)-1:0] alloc;
 
  always_comb begin
    alloc = '0;
    for (int i = NSLOT-1; i >= 0; i--) if (!slot_busy[i]) alloc = gw(NSLOT)'(i);
 
    // A fetch is ISSUED when the queue is non-empty and a slot is free.
    rd_valid = q_nonempty && (slot_busy != '1);
    rd_addr  = q_base + 64'(q_head) * SQE_BYTES;
    rd_bytes = 12'(SQE_BYTES);
    rd_slot  = alloc;
 
    // The head advances when the FETCH IS ISSUED, so the same entry is not
    // fetched twice. The command is not owned yet.
    head_adv = rd_valid && rd_ready;
    head_qid = q_sel;
 
    // OWNERSHIP happens only when the fetch data returns. §7 step 4.
    // A controller that sets cmd_owned from the doorbell is executing on
    // data it has not read (mutation 9) — and §17 measured that the fetch
    // latency usually HIDES this, which is why it survives to silicon.
    cmd_owned = fetch_data_valid;
    cmd_slot  = fetch_slot;
    cmd_id    = fetch_cmd_id;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) slot_busy <= '0;
    else begin
      if (rd_valid && rd_ready)  slot_busy[alloc]      <= 1'b1;
      if (fetch_data_valid)      slot_busy[fetch_slot] <= 1'b0;
    end
  end
 
endmodule

module nvme_xfer_descriptor #(
  parameter int unsigned MAX_CHUNK = 4096      // IMPLEMENTATION POLICY
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                     cmd_valid,
  input  logic [15:0]              cmd_id,
  input  logic [15:0]              queue_id,
  input  nvme_dbg_pkg::xfer_dir_e  dir,
  input  logic [63:0]              host_addr,
  input  logic [31:0]              total_bytes,
  output logic                     cmd_ready,
  output logic                     desc_valid,
  output nvme_dbg_pkg::xfer_desc_t desc,
  input  logic                     desc_ready,
  output logic                     cmd_complete,
  output logic [31:0]              bytes_emitted
);
 
  import nvme_dbg_pkg::*;
 
  logic [31:0] remaining, offset;
  logic        active;
  logic [31:0] this_chunk;
 
  // NVMe's real data pointers (PRP lists, SGLs) are STANDARD-DEFINED and are
  // not modelled. What IS modelled is the conservation obligation: the chunks
  // emitted must sum EXACTLY to the command's byte count, in both directions.
  // 25.6 §4 law 1 measured what a one-sided check misses.
  always_comb begin
    this_chunk = (remaining > MAX_CHUNK) ? MAX_CHUNK : remaining;
    desc_valid = active && (remaining != 0);
    desc       = '{cmd_id:    cmd_id,
                   queue_id:  queue_id,
                   dir:       dir,
                   host_addr: host_addr + 64'(offset),
                   buf_addr:  offset,
                   bytes:     this_chunk};
    cmd_ready    = !active;
    cmd_complete = active && (remaining == 0);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      active <= 1'b0; remaining <= '0; offset <= '0; bytes_emitted <= '0;
    end else begin
      if (cmd_valid && cmd_ready) begin
        active <= 1'b1; remaining <= total_bytes; offset <= '0; bytes_emitted <= '0;
      end else if (desc_valid && desc_ready) begin
        // The final chunk is PARTIAL whenever total_bytes is not a multiple
        // of MAX_CHUNK. Computing a chunk count by truncating division drops
        // it — §16 measured a 25,513,216-byte deficit from exactly that.
        remaining     <= remaining - this_chunk;
        offset        <= offset + this_chunk;
        bytes_emitted <= bytes_emitted + this_chunk;
      end else if (cmd_complete) begin
        active <= 1'b0;
      end
    end
  end
 
endmodule

module nvme_buffer_credit #(
  parameter int unsigned NSLOT = 64
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                   pcie_wants_slot,   // inbound write data
  output logic                                   pcie_slot_grant,
  input  logic                                   media_wants_slot,  // outbound read data
  output logic                                   media_slot_grant,
  input  logic                                   pcie_releases,
  input  logic                                   media_releases,
  output logic [nvme_dbg_pkg::gw(NSLOT+1)-1:0]   free_slots,
  output logic                                   would_overflow
);
 
  import nvme_dbg_pkg::*;
 
  logic [gw(NSLOT+1)-1:0] used;
 
  // Explicit free-slot accounting in BOTH directions. The PCIe side and the
  // media side run at unrelated rates, and neither may overrun the buffer
  // when the other stalls (§13). A design that only throttles one direction
  // corrupts the other under the opposite load pattern (mutations 20, 21).
  always_comb begin
    free_slots       = gw(NSLOT+1)'(NSLOT) - used;
    pcie_slot_grant  = pcie_wants_slot  && (free_slots != 0);
    media_slot_grant = media_wants_slot && (free_slots != 0);
    would_overflow   = (pcie_wants_slot || media_wants_slot) && (free_slots == 0);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) used <= '0;
    else begin
      case ({(pcie_slot_grant || media_slot_grant), (pcie_releases || media_releases)})
        2'b10: used <= used + 1'b1;
        2'b01: used <= used - 1'b1;
        default: ;
      endcase
    end
  end
 
endmodule

module nvme_cq_writer #(
  parameter int unsigned NQUEUE   = 8,
  parameter int unsigned MAXDEPTH = 1024
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                     cmd_done,
  input  logic [15:0]                              done_cmd_id,
  input  logic [nvme_dbg_pkg::gw(NQUEUE)-1:0]      done_cq,
  input  logic [15:0]                              done_status,
  // per-CQ state
  input  logic [nvme_dbg_pkg::gw(MAXDEPTH)-1:0]    cq_head,      // host consumed to here
  input  logic [nvme_dbg_pkg::gw(MAXDEPTH)-1:0]    cq_tail,
  input  logic [nvme_dbg_pkg::gw(MAXDEPTH+1)-1:0]  cq_depth,
  input  logic                                     cq_phase,
  // outbound Memory Write carrying the completion entry (Posted, §4)
  output logic                                     cqe_valid,
  output logic [15:0]                              cqe_cmd_id,
  output logic [15:0]                              cqe_status,
  output logic                                     cqe_phase,
  input  logic                                     cqe_ready,
  output logic                                     cq_full_stall,
  output logic                                     tail_adv,
  output logic                                     phase_toggle,
  output logic [31:0]                              full_stall_count
);
 
  import nvme_dbg_pkg::*;
 
  logic [gw(MAXDEPTH)-1:0] next_tail;
 
  always_comb begin
    next_tail = (cq_tail == gw(MAXDEPTH)'(cq_depth-1)) ? '0 : cq_tail + 1'b1;
 
    // The controller must NOT write into a slot the host has not consumed.
    // §17 measured the alternative: removing this check makes the controller
    // report HIGHER completion throughput while destroying completion
    // records the host had not yet read — 25.6 §6's broken ring-full test.
    cq_full_stall = cmd_done && (next_tail == cq_head);
    cqe_valid     = cmd_done && !cq_full_stall;
    cqe_cmd_id    = done_cmd_id;
    cqe_status    = done_status;
 
    // The phase value published with this entry is the CURRENT phase. It is
    // the host's only means of distinguishing a new entry from a stale one
    // left in the ring from the previous lap — a STANDARD-DEFINED mechanism
    // whose encoding lives in the NVMe specification (§1).
    cqe_phase    = cq_phase;
    tail_adv     = cqe_valid && cqe_ready;
    phase_toggle = tail_adv && (next_tail == '0);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) full_stall_count <= '0;
    else if (cq_full_stall && full_stall_count != 32'hFFFF_FFFF)
      full_stall_count <= full_stall_count + 32'd1;
  end
 
endmodule

module nvme_int_gate #(
  parameter int unsigned NQUEUE = 8
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                  cqe_written,     // the CQE write was ACCEPTED
  input  logic [nvme_dbg_pkg::gw(NQUEUE)-1:0]   cqe_cq,
  input  logic                                  int_enabled,
  output logic                                  int_req,
  output logic [nvme_dbg_pkg::gw(NQUEUE)-1:0]   int_cq,
  input  logic                                  int_ack,
  output logic [31:0]                           early_attempts
);
 
  import nvme_dbg_pkg::*;
 
  logic                  pending;
  logic [gw(NQUEUE)-1:0] pend_cq;
 
  // The interrupt is raised ONLY after the completion entry write has been
  // accepted. §16 measured the inverted order at 99,604 early interrupts —
  // every one an opportunity for the host to read a stale ring entry.
  //
  // 19.x owns the interrupt mechanism. What this module owns is the ORDER:
  // publish the durable record, then notify.
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      pending <= 1'b0; pend_cq <= '0; early_attempts <= '0;
    end else begin
      if (cqe_written) begin pending <= 1'b1; pend_cq <= cqe_cq; end
      else if (int_req && int_ack) pending <= 1'b0;
    end
  end
 
  assign int_req = pending && int_enabled;
  assign int_cq  = pend_cq;
 
endmodule

module nvme_counters (
  input  logic clk,
  input  logic rst_n,
  input  logic sqe_fetch, cqe_write, msi_write,
  input  logic data_beat, input logic [15:0] data_bytes,
  input  logic stall_link,     // waiting for credit or Tags
  input  logic stall_media,    // waiting for the flash pipeline
  input  logic stall_buffer,   // waiting for a controller buffer slot
  input  logic stall_cqfull,   // waiting for the host to consume completions
  input  logic clear,
  output logic [31:0] c_sqe, c_cqe, c_msi,
  output logic [63:0] c_data_bytes,
  output logic [31:0] c_link, c_media, c_buffer, c_cqfull
);
 
  // Four separate stall attributions, because §14's whole point is that
  // "the SSD is slow" is not a diagnosis. A media stall and a Link stall
  // demand opposite responses, and a CQ-full stall means the HOST is the
  // limiter — which no amount of controller work will fix.
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_sqe <= '0; c_cqe <= '0; c_msi <= '0; c_data_bytes <= '0;
      c_link <= '0; c_media <= '0; c_buffer <= '0; c_cqfull <= '0;
    end else begin
      if (sqe_fetch    && c_sqe    != '1) c_sqe    <= c_sqe + 1'b1;
      if (cqe_write    && c_cqe    != '1) c_cqe    <= c_cqe + 1'b1;
      if (msi_write    && c_msi    != '1) c_msi    <= c_msi + 1'b1;
      if (stall_link   && c_link   != '1) c_link   <= c_link + 1'b1;
      if (stall_media  && c_media  != '1) c_media  <= c_media + 1'b1;
      if (stall_buffer && c_buffer != '1) c_buffer <= c_buffer + 1'b1;
      if (stall_cqfull && c_cqfull != '1) c_cqfull <= c_cqfull + 1'b1;
      if (data_beat && c_data_bytes != '1) c_data_bytes <= c_data_bytes + 64'(data_bytes);
    end
  end
 
endmodule

// P1 — a doorbell is captured only from an accepted BAR write.
property p1_db_on_accepted_write;
  @(posedge clk) disable iff (!rst_n)
    (bar_wr_valid && !qid_range_error) |=> (pend_sq[$past(decoded_qid)] ||
                                            pend_cq[$past(decoded_qid)]);
endproperty
a_p1: assert property (p1_db_on_accepted_write);
 
// P2 — an out-of-range queue id is reported, never wrapped.
property p2_qid_range;
  @(posedge clk) disable iff (!rst_n)
    (bar_wr_valid && (decoded_qid >= NQUEUE)) |-> qid_range_error;
endproperty
a_p2: assert property (p2_qid_range);
 
// P3 — a newer doorbell for the same queue is not lost to a concurrent accept.
property p3_db_not_lost;
  @(posedge clk) disable iff (!rst_n)
    (db_valid && db_ready && bar_wr_valid && (decoded_qid == db_qid) &&
     (decoded_is_sq == db_is_sq)) |=> (pend_sq[$past(db_qid)] || pend_cq[$past(db_qid)]);
endproperty
a_p3: assert property (p3_db_not_lost);
 
// P4 — a doorbell value beyond the queue depth is rejected, not applied.
property p4_db_value_bounded;
  @(posedge clk) disable iff (!rst_n)
    (db_valid && q_enabled && (db_value >= cfg_depth)) |-> db_range_error;
endproperty
a_p4: assert property (p4_db_value_bounded);
 
// P5 — a disabled queue accepts no work.
property p5_disabled_queue_inert;
  @(posedge clk) disable iff (!rst_n)
    !q_enabled |-> !q_nonempty;
endproperty
a_p5: assert property (p5_disabled_queue_inert);
 
// P6 — creating or deleting a queue clears its pointers.
property p6_cfg_resets_pointers;
  @(posedge clk) disable iff (!rst_n)
    cfg_valid |=> ((head[$past(cfg_qid)] == '0) && (tail[$past(cfg_qid)] == '0));
endproperty
a_p6: assert property (p6_cfg_resets_pointers);
 
// P7 — head and tail stay within the configured depth.
property p7_pointers_bounded;
  @(posedge clk) disable iff (!rst_n)
    q_enabled |-> ((q_head < cfg_depth) && (q_tail < cfg_depth));
endproperty
a_p7: assert property (p7_pointers_bounded);

// P8 — a command is owned only when its fetch data returns, never on the
// doorbell. §17 measured that the fetch latency usually HIDES the violation.
property p8_owned_on_fetch_return;
  @(posedge clk) disable iff (!rst_n)
    cmd_owned |-> fetch_data_valid;
endproperty
a_p8: assert property (p8_owned_on_fetch_return);
 
// P9 — the head advances on fetch ISSUE, so no entry is fetched twice.
property p9_head_on_issue;
  @(posedge clk) disable iff (!rst_n)
    head_adv |-> (rd_valid && rd_ready);
endproperty
a_p9: assert property (p9_head_on_issue);
 
// P10 — a fetch slot is allocated only if free.
property p10_slot_free_on_alloc;
  @(posedge clk) disable iff (!rst_n)
    (rd_valid && rd_ready) |-> !slot_busy[rd_slot];
endproperty
a_p10: assert property (p10_slot_free_on_alloc);
 
// P11 — returning data releases exactly the slot that requested it.
property p11_slot_release_matches;
  @(posedge clk) disable iff (!rst_n)
    fetch_data_valid |-> slot_busy[fetch_slot];
endproperty
a_p11: assert property (p11_slot_release_matches);
 
// P12 — no fetch is issued for an empty queue.
property p12_no_fetch_when_empty;
  @(posedge clk) disable iff (!rst_n)
    rd_valid |-> q_nonempty;
endproperty
a_p12: assert property (p12_no_fetch_when_empty);

// P13 — emitted chunks sum EXACTLY to the command's byte count.
// 25.6 §4 law 1: the check must be two-sided.
property p13_bytes_conserved;
  @(posedge clk) disable iff (!rst_n)
    cmd_complete |-> (bytes_emitted == total_bytes);
endproperty
a_p13: assert property (p13_bytes_conserved);
 
// P14 — the final chunk may be partial and must not be dropped.
// §16 measured a truncating chunk count losing 25,513,216 bytes.
property p14_final_partial_chunk;
  @(posedge clk) disable iff (!rst_n)
    (active && (remaining > 0) && (remaining < MAX_CHUNK))
      |-> (desc_valid && (desc.bytes == remaining));
endproperty
a_p14: assert property (p14_final_partial_chunk);
 
// P15 — a zero-byte command emits no descriptor.
property p15_zero_bytes_no_desc;
  @(posedge clk) disable iff (!rst_n)
    (cmd_valid && cmd_ready && (total_bytes == 32'd0)) |=> !desc_valid;
endproperty
a_p15: assert property (p15_zero_bytes_no_desc);
 
// P16 — a descriptor's byte count never exceeds the chunk limit.
property p16_chunk_bounded;
  @(posedge clk) disable iff (!rst_n)
    desc_valid |-> (desc.bytes <= MAX_CHUNK) && (desc.bytes != 0);
endproperty
a_p16: assert property (p16_chunk_bounded);
 
// P17 — the command id is carried unchanged onto every descriptor.
property p17_cmd_id_propagated;
  @(posedge clk) disable iff (!rst_n)
    desc_valid |-> (desc.cmd_id == cmd_id);
endproperty
a_p17: assert property (p17_cmd_id_propagated);

// P18 — a slot is granted only when one is free, from either direction.
property p18_grant_needs_free;
  @(posedge clk) disable iff (!rst_n)
    (pcie_slot_grant || media_slot_grant) |-> (free_slots != 0);
endproperty
a_p18: assert property (p18_grant_needs_free);
 
// P19 — occupancy never exceeds the buffer size.
property p19_occupancy_bounded;
  @(posedge clk) disable iff (!rst_n)
    (used <= NSLOT);
endproperty
a_p19: assert property (p19_occupancy_bounded);
 
// P20 — an overflow attempt is reported, never silently absorbed.
property p20_overflow_reported;
  @(posedge clk) disable iff (!rst_n)
    ((pcie_wants_slot || media_wants_slot) && (free_slots == 0)) |-> would_overflow;
endproperty
a_p20: assert property (p20_overflow_reported);

// P21 — no completion entry is written into an unconsumed slot.
// §17 measured removing this: 796 clobbered entries at a slow host rate.
property p21_no_cq_overwrite;
  @(posedge clk) disable iff (!rst_n)
    cqe_valid |-> (next_tail != cq_head);
endproperty
a_p21: assert property (p21_no_cq_overwrite);
 
// P22 — a CQ-full condition stalls and is counted, never dropped.
property p22_cq_full_stalls;
  @(posedge clk) disable iff (!rst_n)
    (cmd_done && (next_tail == cq_head)) |-> (cq_full_stall && !cqe_valid);
endproperty
a_p22: assert property (p22_cq_full_stalls);
 
// P23 — the phase toggles exactly at wrap. It is the host's only means of
// distinguishing a new entry from last lap's (§16: 3,111 missed toggles).
property p23_phase_toggles_at_wrap;
  @(posedge clk) disable iff (!rst_n)
    (tail_adv && (next_tail == '0)) |-> phase_toggle;
endproperty
a_p23: assert property (p23_phase_toggles_at_wrap);
 
// P24 — the phase does not toggle anywhere else.
property p24_phase_stable_otherwise;
  @(posedge clk) disable iff (!rst_n)
    (tail_adv && (next_tail != '0)) |-> !phase_toggle;
endproperty
a_p24: assert property (p24_phase_stable_otherwise);
 
// P25 — exactly one completion entry per completed command.
property p25_one_cqe_per_command;
  @(posedge clk) disable iff (!rst_n)
    (cqe_valid && cqe_ready) |=> !(cqe_valid && (cqe_cmd_id == $past(cqe_cmd_id)));
endproperty
a_p25: assert property (p25_one_cqe_per_command);
 
// P26 — the completion entry carries the command id that finished.
// §16 measured 2,909 entries carrying the wrong one.
property p26_cqe_id_correct;
  @(posedge clk) disable iff (!rst_n)
    cqe_valid |-> (cqe_cmd_id == done_cmd_id);
endproperty
a_p26: assert property (p26_cqe_id_correct);
 
// P27 — the interrupt is raised only after the CQE write was ACCEPTED.
// §16 measured the inversion at 99,604 early interrupts.
property p27_int_after_cqe;
  @(posedge clk) disable iff (!rst_n)
    int_req |-> $past(cqe_written, 1) or pending;
endproperty
a_p27: assert property (p27_int_after_cqe);

// P28 — a command reaches exactly one terminal outcome: a completion entry
// is published, or it is still owned. A command that leaves the controller's
// state without publishing is lost silently, and §7's ownership chain has
// no step that would report it.
property p28_command_terminal;
  @(posedge clk) disable iff (!rst_n)
    (cmd_done && !cq_full_stall) |-> cqe_valid;
endproperty
a_p28: assert property (p28_command_terminal);
 
// P28's covers — the load-dependent paths must actually be exercised. §17 measured
// the CQ never filling at all when the host keeps up, which makes P21, P22
// and P23 vacuous against any light-load testbench.
c1_cq_full:     cover property (@(posedge clk) disable iff (!rst_n) cq_full_stall);
c2_cq_wrap:     cover property (@(posedge clk) disable iff (!rst_n) phase_toggle);
c3_db_collide:  cover property (@(posedge clk) disable iff (!rst_n)
                  db_valid && db_ready && bar_wr_valid && (decoded_qid == db_qid));
c4_qid_error:   cover property (@(posedge clk) disable iff (!rst_n) qid_range_error);
c5_partial:     cover property (@(posedge clk) disable iff (!rst_n)
                  desc_valid && (desc.bytes < MAX_CHUNK));
c6_buf_full:    cover property (@(posedge clk) disable iff (!rst_n) would_overflow);
c7_slots_busy:  cover property (@(posedge clk) disable iff (!rst_n) slot_busy == '1);
c8_zero_len:    cover property (@(posedge clk) disable iff (!rst_n)
                  cmd_valid && (total_bytes == 32'd0));

// The controller begins executing as soon as a doorbell advances the tail,
// using whatever the submission-queue slot currently holds.
module ce_a_exec_on_doorbell (
  input  logic clk, rst_n,
  input  logic        db_valid,
  input  logic [15:0] sq_slot_cmd_id,     // reflects host memory, live
  output logic        cmd_owned,
  output logic [15:0] cmd_id
);
  assign cmd_owned = db_valid;            // <-- no fetch, no return
  assign cmd_id    = sq_slot_cmd_id;
endmodule
 
// Failing stimulus: the host advances the doorbell before its submission
// queue entry has become visible in memory.
// Golden: the controller issues a Memory Read for the entry and takes
//         ownership only when that read's data returns (§7 step 4).
// This:   it executes against a slot that may still hold the previous
//         occupant's command, or nothing at all.
// P8 fails.
// §16 measured this producing 0 stale executions at a typical fetch latency
// and 98 once the fetch was shortened to a single step. The fault is present
// in both; only the controller's own read latency hid it.

// A completion entry is written whenever a command finishes, without
// checking whether the host has consumed the slot being overwritten.
module ce_b_no_cq_full_check #(parameter int unsigned CQD = 32)(
  input  logic clk, rst_n,
  input  logic        cmd_done,
  input  logic [15:0] done_cmd_id,
  output logic        cqe_valid,
  output logic [4:0]  cq_tail
);
  assign cqe_valid = cmd_done;            // <-- never consults cq_head
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) cq_tail <= '0;
    else if (cmd_done) cq_tail <= (cq_tail == 5'(CQD-1)) ? '0 : cq_tail + 1'b1;
endmodule
 
// Failing stimulus: a host that consumes completion entries slowly while
// the controller retires commands quickly.
// Golden: the controller stalls, holding the completion until space exists.
// This:   it writes over entries the host has not yet read.
// P21 fails, P22 fails.
// §16 measured 30,118 completions written against a correct design's 4,907,
// with 796 of them clobbering unread entries. The faulty controller reports
// SIX TIMES the completion throughput — achieved by destroying completion
// records. This is 25.6 §6's broken ring-full test in a new place.

// The interrupt is raised in the same cycle the command reaches its terminal
// state, without waiting for the completion-entry write to be accepted.
module ce_c_int_before_cqe (
  input  logic cmd_terminal,
  output logic cqe_valid, int_req
);
  assign cqe_valid = cmd_terminal;
  assign int_req   = cmd_terminal;        // <-- concurrent, not sequenced
endmodule
 
// Failing stimulus: the completion-entry write is back-pressured for several
// cycles while the interrupt message is delivered immediately.
// Golden: the interrupt waits for the CQE write to be accepted (§7 step 7).
// This:   the host is interrupted, reads the completion queue, and finds the
//         PREVIOUS lap's entry — which the phase bit correctly marks as
//         stale, so the host sees no new completion at all and the command
//         appears to hang.
// P27 fails.
// §15 measured 99,604 such interrupts in one run. The failure is
// characteristically intermittent: it appears only when the CQE write path
// is slower than the interrupt path.