FPGA Cards — The Half of PCIe You Actually Write

──────────── the IP core typically owns ────────────
  PHY / SerDes, electrical
  LTSSM, link training, equalization        (Module 18)
  Data Link Layer: sequence numbers, ACK/NAK, replay   (Module 14)
  Transaction Layer framing, credit accounting          (Modules 15-16)
────────────── the application interface ──────────────
──────────────── you own everything here ──────────────
  BAR decode and register file                          (23.2, 25.5)
  DMA engine, descriptor management                     (23.3, 25.6)
  Tag allocation, Completion matching                   (23.5, 25.7)
  buffering, clock domain crossing                      (§11, §12)
  reset integration and epochs                          (§13)
  interrupt request generation                          (19.x)
  local memory arbitration                              (§14)
  observability                                         (§15, §16)

package fpga_pcie_pkg;
 
  // The five conceptual channels of §3, named locally. A vendor core's
  // actual field names never appear above the adapter (Block 2).
  typedef enum logic [2:0] {
    REQ_MEM_RD = 3'd0,
    REQ_MEM_WR = 3'd1,
    REQ_CPL    = 3'd2,
    REQ_CPLD   = 3'd3,
    REQ_MSG    = 3'd4
  } req_kind_e;
 
  // §13: an epoch distinguishes work issued before a reset/retrain from work
  // issued after. 25.7 §7's law — an asynchronous response must carry its own
  // identity, including WHICH USE of that identity.
  localparam int unsigned EPOCH_W = 4;
  typedef logic [EPOCH_W-1:0] epoch_t;
 
  function automatic int unsigned gw(input int unsigned n);
    return (n <= 1) ? 1 : $clog2(n);   // §19: $clog2(1) is 0 in some tools
  endfunction
 
  // A DMA job as the engine owns it: a SNAPSHOT. §18 measured a live-read
  // variant losing 143,872 bytes when the host mutated the descriptor.
  typedef struct packed {
    logic [31:0] job_id;
    logic        to_host;         // 1 = device→host (MemWr), 0 = host→device (MemRd)
    logic [63:0] host_addr;
    logic [31:0] local_addr;
    logic [31:0] bytes;
    epoch_t      epoch;
  } dma_job_t;
 
  typedef struct packed {
    req_kind_e   kind;
    logic [63:0] addr;
    logic [11:0] len_bytes;
    logic [7:0]  tag;
    epoch_t      epoch;
  } app_req_t;
 
endpackage

module pcie_core_adapter (
  input  logic clk,
  input  logic rst_n,
  // ---- vendor side: DELIBERATELY generic names (§4). A real design binds
  // these to the core's actual ports in ONE file, and nothing above this
  // module ever sees a vendor-specific identifier.
  input  logic         core_rx_valid,
  output logic         core_rx_ready,
  input  logic [2:0]   core_rx_kind,
  input  logic [63:0]  core_rx_addr,
  input  logic [11:0]  core_rx_len,
  input  logic [7:0]   core_rx_tag,
  output logic         core_tx_valid,
  input  logic         core_tx_ready,
  output logic [2:0]   core_tx_kind,
  output logic [63:0]  core_tx_addr,
  output logic [11:0]  core_tx_len,
  output logic [7:0]   core_tx_tag,
  // status the core reports, and which 25.9 §3 showed is invisible from
  // the link side — captured by Block 12
  input  logic         core_link_up,
  input  logic [5:0]   core_neg_width,
  input  logic [3:0]   core_neg_speed,
  input  logic [4:0]   core_ltssm,
  // ---- application side: project-local types only
  output logic                       app_rx_valid,
  input  logic                       app_rx_ready,
  output fpga_pcie_pkg::app_req_t    app_rx_req,
  input  logic                       app_tx_valid,
  output logic                       app_tx_ready,
  input  fpga_pcie_pkg::app_req_t    app_tx_req,
  output logic                       app_link_up,
  output logic [5:0]                 app_neg_width,
  output logic [4:0]                 app_ltssm
);
 
  import fpga_pcie_pkg::*;
 
  // A pure translation with NO buffering and NO field invention. The ready
  // signals pass straight through, so the adapter cannot become a hidden
  // storage element whose contents diverge from either side (mutation 4).
  always_comb begin
    app_rx_valid      = core_rx_valid;
    core_rx_ready     = app_rx_ready;
    app_rx_req.kind   = req_kind_e'(core_rx_kind);
    app_rx_req.addr   = core_rx_addr;
    app_rx_req.len_bytes = core_rx_len;
    app_rx_req.tag    = core_rx_tag;
    app_rx_req.epoch  = '0;            // epochs are an APPLICATION concept (§13)
 
    core_tx_valid = app_tx_valid;
    app_tx_ready  = core_tx_ready;
    core_tx_kind  = app_tx_req.kind;
    core_tx_addr  = app_tx_req.addr;
    core_tx_len   = app_tx_req.len_bytes;
    core_tx_tag   = app_tx_req.tag;
 
    app_link_up   = core_link_up;
    app_neg_width = core_neg_width;    // NEGOTIATED, not capability (26.2 §4)
    app_ltssm     = core_ltssm;
  end
 
endmodule

module bar_control_path #(
  parameter int unsigned NREG = 64
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                           req_valid,
  output logic                           req_ready,
  input  logic                           req_is_write,
  input  logic [31:0]                    req_offset,
  input  logic [31:0]                    req_wdata,
  output logic                           rsp_valid,
  input  logic                           rsp_ready,
  output logic [31:0]                    rsp_rdata,
  output logic                           offset_error,
  output logic [31:0]                    reg_file [NREG]
);
 
  import fpga_pcie_pkg::*;
 
  logic [31:0] captured_rdata;
  logic        rsp_pending;
  logic [gw(NREG)-1:0] idx;
 
  // Range-checked, not wrapped. 25.5 §3's law: an unclaimed offset is an
  // error, never a default. Wrapping turns a host bug into a silent write
  // to an unrelated register (mutation 6).
  assign idx          = gw(NREG)'(req_offset >> 2);
  assign offset_error = req_valid && ((req_offset[1:0] != 2'b00) ||
                                      ((req_offset >> 2) >= NREG));
  assign req_ready    = !rsp_pending;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      rsp_pending <= 1'b0; captured_rdata <= '0;
      for (int i = 0; i < NREG; i++) reg_file[i] <= '0;
    end else begin
      if (req_valid && req_ready && !offset_error) begin
        if (req_is_write) reg_file[idx] <= req_wdata;
        else begin
          // The read value is CAPTURED here and held. Re-reading the register
          // file while the response is stalled returns a value the host never
          // requested — a live-configuration read, which is mutation 7 and
          // the same fault 25.5 §10 guards against.
          captured_rdata <= reg_file[idx];
          rsp_pending    <= 1'b1;
        end
      end
      if (rsp_valid && rsp_ready) rsp_pending <= 1'b0;
    end
  end
 
  assign rsp_valid = rsp_pending;
  assign rsp_rdata = captured_rdata;
 
endmodule

module dma_tag_alloc #(
  parameter int unsigned NTAG = 32
)(
  input  logic clk,
  input  logic rst_n,
  input  fpga_pcie_pkg::epoch_t              cur_epoch,
  input  logic                               alloc_req,
  output logic                               alloc_gnt,
  output logic [fpga_pcie_pkg::gw(NTAG)-1:0] alloc_tag,
  output fpga_pcie_pkg::epoch_t              alloc_epoch,
  input  logic                               cpl_valid,
  input  logic [fpga_pcie_pkg::gw(NTAG)-1:0] cpl_tag,
  input  fpga_pcie_pkg::epoch_t              cpl_epoch,
  input  logic                               cpl_last,        // final Cpl of the request
  output logic                               cpl_accept,
  output logic                               cpl_stale,
  output logic [31:0]                        stale_count,
  output logic [fpga_pcie_pkg::gw(NTAG+1)-1:0] free_count
);
 
  import fpga_pcie_pkg::*;
 
  logic [NTAG-1:0] busy;
  epoch_t          tag_epoch [NTAG];
 
  always_comb begin
    alloc_gnt = alloc_req && (busy != '1);
    alloc_tag = '0;
    for (int i = NTAG-1; i >= 0; i--) if (!busy[i]) alloc_tag = gw(NTAG)'(i);
    alloc_epoch = cur_epoch;
 
    // A Completion is accepted only if its Tag is outstanding AND its epoch
    // matches. §18 measured removing this comparison: 62 misdeliveries
    // carrying 70,976 bytes into the wrong job's buffer, across 133 resets.
    cpl_stale  = cpl_valid && (!busy[cpl_tag] || (tag_epoch[cpl_tag] != cpl_epoch));
    cpl_accept = cpl_valid && !cpl_stale;
 
    free_count = '0;
    for (int i = 0; i < NTAG; i++) free_count += gw(NTAG+1)'(!busy[i]);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      busy <= '0; stale_count <= '0;
      for (int i = 0; i < NTAG; i++) tag_epoch[i] <= '0;
    end else begin
      if (alloc_req && alloc_gnt) begin
        busy[alloc_tag]      <= 1'b1;
        tag_epoch[alloc_tag] <= cur_epoch;
      end
      // The Tag is freed on the LAST Completion, not the first. A split
      // series frees early otherwise, and the remaining Completions arrive
      // for a Tag that has been reissued (mutation 12; 25.7 §7).
      if (cpl_accept && cpl_last) busy[cpl_tag] <= 1'b0;
      if (cpl_stale && stale_count != 32'hFFFF_FFFF)
        stale_count <= stale_count + 32'd1;
    end
  end
 
endmodule

module dma_descriptor_engine #(
  parameter int unsigned MAX_CHUNK = 256      // IMPLEMENTATION POLICY (≤ MPS)
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                         desc_valid,
  input  fpga_pcie_pkg::dma_job_t      desc_in,
  output logic                         desc_ready,
  input  fpga_pcie_pkg::epoch_t        cur_epoch,
  output logic                         req_valid,
  output fpga_pcie_pkg::app_req_t      req_out,
  input  logic                         req_ready,
  input  logic                         tag_gnt,
  input  logic [7:0]                   tag_in,
  output logic                         job_done,
  output logic [31:0]                  job_id_done,
  output logic [31:0]                  bytes_issued,
  output logic [31:0]                  bytes_described
);
 
  import fpga_pcie_pkg::*;
 
  dma_job_t    job;
  logic        active;
  logic [31:0] remaining, offset;
  logic [31:0] this_chunk;
 
  always_comb begin
    // The final chunk is PARTIAL whenever bytes is not a multiple of
    // MAX_CHUNK. §18 measured a truncating chunk count dropping it:
    // 4,119 lost tails and a 263,616-byte deficit.
    this_chunk = (remaining > MAX_CHUNK) ? MAX_CHUNK : remaining;
    desc_ready = !active;
    req_valid  = active && (remaining != 0) && tag_gnt;
    req_out    = '{kind:      job.to_host ? REQ_MEM_WR : REQ_MEM_RD,
                   addr:      job.host_addr + 64'(offset),
                   len_bytes: 12'(this_chunk),
                   tag:       tag_in,
                   epoch:     job.epoch};
    job_done    = active && (remaining == 0);
    job_id_done = job.job_id;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      active <= 1'b0; remaining <= '0; offset <= '0;
      bytes_issued <= '0; bytes_described <= '0; job <= '0;
    end else begin
      if (desc_valid && desc_ready) begin
        // SNAPSHOT. The engine never re-reads the descriptor afterwards.
        // §18's live-read variant lost 143,872 bytes when the host mutated
        // a descriptor it had already handed over.
        job             <= desc_in;
        job.epoch       <= cur_epoch;
        active          <= 1'b1;
        remaining       <= desc_in.bytes;
        offset          <= '0;
        bytes_described <= bytes_described + desc_in.bytes;
      end else if (req_valid && req_ready) begin
        remaining    <= remaining - this_chunk;
        offset       <= offset + this_chunk;
        bytes_issued <= bytes_issued + this_chunk;
      end else if (job_done) begin
        active <= 1'b0;
      end
    end
  end
 
endmodule

module cdc_control_bit #(
  parameter int unsigned STAGES = 2
)(
  input  logic dst_clk,
  input  logic dst_rst_n,
  input  logic src_level,      // MUST be a stable level, not a pulse
  output logic dst_level
);
 
  // Correct ONLY for a single bit that is a stable LEVEL. A pulse shorter
  // than the destination clock period can be missed entirely (mutation 20),
  // and a MULTI-BIT bus synchronized this way is incoherent even though
  // every individual bit is metastability-safe — counterexample A, and the
  // reason Block 7 exists.
  (* ASYNC_REG = "TRUE" *) logic [STAGES-1:0] sync;
 
  always_ff @(posedge dst_clk or negedge dst_rst_n)
    if (!dst_rst_n) sync <= '0;
    else            sync <= {sync[STAGES-2:0], src_level};
 
  assign dst_level = sync[STAGES-1];
 
endmodule

module cdc_command_handshake #(
  parameter int unsigned WIDTH = 64
)(
  input  logic             src_clk, src_rst_n,
  input  logic             src_valid,
  input  logic [WIDTH-1:0] src_data,
  output logic             src_ready,
  input  logic             dst_clk, dst_rst_n,
  output logic             dst_valid,
  output logic [WIDTH-1:0] dst_data,
  input  logic             dst_ready
);
 
  // The DATA never crosses through a synchronizer. It is held stable in the
  // source domain while a single-bit REQUEST toggle crosses; the destination
  // samples the data only after observing the request, by which time it has
  // been stable for at least two destination clocks.
  //
  // This is the mechanism counterexample A's design should have used.
  logic src_req, dst_req_sync, dst_ack_sync, dst_req;
  logic [WIDTH-1:0] hold;
 
  cdc_control_bit #(.STAGES(2)) u_req (
    .dst_clk(dst_clk), .dst_rst_n(dst_rst_n), .src_level(src_req), .dst_level(dst_req));
  logic src_ack;
  cdc_control_bit #(.STAGES(2)) u_ack (
    .dst_clk(src_clk), .dst_rst_n(src_rst_n), .src_level(dst_ack_sync), .dst_level(src_ack));
 
  always_ff @(posedge src_clk or negedge src_rst_n) begin
    if (!src_rst_n) begin src_req <= 1'b0; hold <= '0; end
    else if (src_valid && src_ready) begin
      hold    <= src_data;          // stable for the whole crossing
      src_req <= ~src_req;
    end
  end
  assign src_ready = (src_req == src_ack);
 
  always_ff @(posedge dst_clk or negedge dst_rst_n) begin
    if (!dst_rst_n) begin dst_req_sync <= 1'b0; dst_ack_sync <= 1'b0; end
    else begin
      dst_req_sync <= dst_req;
      if ((dst_req != dst_req_sync) && dst_ready) dst_ack_sync <= dst_req;
    end
  end
 
  assign dst_valid = (dst_req != dst_ack_sync);
  assign dst_data  = hold;          // sampled only when dst_valid is high
 
endmodule

// An async FIFO is a solved problem with subtle correctness requirements
// (Gray-coded pointers, correctly synchronized in both directions, depth a
// power of two). This chapter does NOT reimplement one — a homemade async
// FIFO in a PCIe datapath is a liability, and vendor libraries and the
// repository's existing CDC primitives should be used instead.
//
// What IS this chapter's business is the CONTRACT the FIFO must satisfy,
// stated here so §16's assertions can check it and §18 can measure it.
module cdc_async_fifo_if #(
  parameter int unsigned WIDTH = 512,
  parameter int unsigned DEPTH = 32          // MUST be a power of two
)(
  input  logic             wr_clk, wr_rst_n,
  input  logic             wr_en,
  input  logic [WIDTH-1:0] wr_data,
  output logic             wr_full,
  output logic             wr_overflow,      // an attempted write while full
  input  logic             rd_clk, rd_rst_n,
  input  logic             rd_en,
  output logic [WIDTH-1:0] rd_data,
  output logic             rd_empty,
  output logic             rd_underflow      // an attempted read while empty
);
 
  // The contract, and the three things §18 measured breaking:
  //   1. wr_en must never be asserted while wr_full.       (105,801 overflows)
  //   2. rd_en must never be asserted while rd_empty.      (1,653 underflows)
  //   3. DEPTH must be a power of two, or Gray pointers are invalid.
  // Overflow and underflow are REPORTED here rather than being silent,
  // because 25.1 §6's rule applies: a condition detected and discarded is
  // indistinguishable from one never detected.
  initial begin
    if (DEPTH & (DEPTH-1))
      $fatal(1, "cdc_async_fifo_if: DEPTH must be a power of two");
  end
 
endmodule

module reset_epoch (
  input  logic clk,
  input  logic rst_n,
  input  logic link_down,           // the core reports the link left L0
  input  logic app_reset_req,       // a software-initiated application reset
  output fpga_pcie_pkg::epoch_t cur_epoch,
  output logic                  epoch_changed,
  output logic [31:0]           epoch_count
);
 
  import fpga_pcie_pkg::*;
 
  logic link_down_d;
 
  // The epoch advances on any event that can invalidate in-flight work.
  // PCIe's own reset semantics are SPEC-DEFINED and are not restated here;
  // this local epoch is IMPLEMENTATION POLICY, and its job is narrow:
  // make a response issued before the event distinguishable from one issued
  // after. §18 measured 133 such events producing 165 stale responses, all
  // correctly discarded — and 62 misdeliveries when the check was removed.
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cur_epoch <= '0; link_down_d <= 1'b0; epoch_count <= '0;
    end else begin
      link_down_d <= link_down;
      if ((link_down && !link_down_d) || app_reset_req) begin
        cur_epoch   <= cur_epoch + 1'b1;
        epoch_count <= epoch_count + 32'd1;
      end
    end
  end
 
  assign epoch_changed = (link_down && !link_down_d) || app_reset_req;
 
endmodule

module app_stream_bridge #(
  parameter int unsigned DATA_BYTES = 64
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                        in_valid,
  input  logic [DATA_BYTES*8-1:0]     in_data,
  input  logic [DATA_BYTES-1:0]       in_keep,      // partial final beat
  input  logic                        in_last,
  output logic                        in_ready,
  output logic                        out_valid,
  output logic [DATA_BYTES*8-1:0]     out_data,
  output logic [DATA_BYTES-1:0]       out_keep,
  output logic                        out_last,
  input  logic                        out_ready,
  output logic [63:0]                 bytes_passed
);
 
  // A GENERIC ready/valid stream. AXI is a vendor-ecosystem convention and
  // is NOT required by PCIe (§10); this interface is deliberately protocol-
  // neutral so the ownership properties can be stated without importing a
  // bus specification.
  //
  // `keep` exists because the final beat of a transfer is usually partial.
  // A bridge that ignores it silently rounds every transfer up to a beat
  // boundary — 25.6 §4's dropped tail, in a new place (mutation 17).
  assign out_valid = in_valid;
  assign in_ready  = out_ready;
  assign out_data  = in_data;
  assign out_keep  = in_keep;
  assign out_last  = in_last;
 
  function automatic int unsigned popcount(input logic [DATA_BYTES-1:0] k);
    popcount = 0;
    for (int i = 0; i < DATA_BYTES; i++) popcount += k[i];
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) bytes_passed <= '0;
    else if (out_valid && out_ready)
      bytes_passed <= bytes_passed + 64'(popcount(out_keep));
  end
 
endmodule

module local_mem_arbiter #(
  parameter int unsigned NREQ = 2      // DMA and accelerator
)(
  input  logic clk,
  input  logic rst_n,
  input  logic [NREQ-1:0]                    req_valid,
  input  logic [NREQ-1:0]                    req_is_write,
  input  logic [31:0]                        req_addr [NREQ],
  output logic [NREQ-1:0]                    req_grant,
  output logic                               mem_valid,
  output logic [31:0]                        mem_addr,
  output logic                               mem_is_write,
  input  logic                               mem_ready,
  // responses must return to the RECORDED owner, not the current requester
  input  logic                               rsp_valid,
  input  logic [fpga_pcie_pkg::gw(NREQ)-1:0] rsp_id,
  output logic [NREQ-1:0]                    rsp_route,
  output logic                               rsp_misroute
);
 
  import fpga_pcie_pkg::*;
 
  logic [gw(NREQ)-1:0] rr, sel;
  logic found;
  logic [NREQ-1:0] outstanding;
 
  always_comb begin
    sel = rr; found = 1'b0;
    for (int k = 0; k < NREQ; k++) begin
      automatic logic [gw(NREQ)-1:0] i = gw(NREQ)'((rr + k) % NREQ);
      if (!found && req_valid[i]) begin sel = i; found = 1'b1; end
    end
    mem_valid    = found;
    mem_addr     = req_addr[sel];
    mem_is_write = req_is_write[sel];
    req_grant    = '0;
    if (found && mem_ready) req_grant[sel] = 1'b1;
 
    // The response is routed by the RECORDED requester id carried with the
    // transaction — never by whoever is being served now. Counterexample E
    // is the alternative, and it is the same fault 26.4 §16's identity
    // oracle exists to catch.
    rsp_route    = '0;
    if (rsp_valid) rsp_route[rsp_id] = 1'b1;
    rsp_misroute = rsp_valid && !outstanding[rsp_id];
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      rr <= '0; outstanding <= '0;
    end else begin
      if (found && mem_ready) begin
        rr <= (sel == gw(NREQ)'(NREQ-1)) ? '0 : sel + 1'b1;
        outstanding[sel] <= 1'b1;
      end
      if (rsp_valid) outstanding[rsp_id] <= 1'b0;
    end
  end
 
endmodule

module perf_and_capture #(
  parameter int unsigned NTAG = 32
)(
  input  logic clk,
  input  logic rst_n,
  // per-stage activity, so §17's limiting stage can be identified in silicon
  input  logic        pcie_beat,  input logic [15:0] pcie_bytes,
  input  logic        app_beat,   input logic [15:0] app_bytes,
  input  logic        stall_credit, stall_tag, stall_fifo_full,
  input  logic        stall_fifo_empty, stall_localmem,
  // first-failure inputs
  input  logic        fifo_overflow, fifo_underflow, cpl_stale,
  input  logic        byte_mismatch, rsp_misroute,
  input  logic [4:0]  ltssm,
  input  logic [7:0]  tag_snapshot,
  input  logic [31:0] job_snapshot,
  input  logic [15:0] fifo_level,
  input  logic        clear,
  output logic [63:0] c_pcie_bytes, c_app_bytes,
  output logic [31:0] c_credit, c_tag, c_full, c_empty, c_localmem,
  output logic        captured,
  output logic [3:0]  first_cause,
  output logic [4:0]  cap_ltssm,
  output logic [7:0]  cap_tag,
  output logic [31:0] cap_job,
  output logic [15:0] cap_fifo_level,
  output logic [31:0] cap_cycle
);
 
  logic [31:0] cycle;
  logic [3:0]  this_cause;
 
  // §16: in hardware, ONE well-chosen snapshot at the first failure is worth
  // more than hours of trace capture — 25.9 §3 measured that the link-side
  // view cannot see any of these signals at all.
  always_comb begin
    if      (fifo_overflow)  this_cause = 4'd1;
    else if (fifo_underflow) this_cause = 4'd2;
    else if (byte_mismatch)  this_cause = 4'd3;
    else if (rsp_misroute)   this_cause = 4'd4;
    else if (cpl_stale)      this_cause = 4'd5;
    else                     this_cause = 4'd0;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_pcie_bytes <= '0; c_app_bytes <= '0;
      c_credit <= '0; c_tag <= '0; c_full <= '0; c_empty <= '0; c_localmem <= '0;
      captured <= 1'b0; first_cause <= '0; cycle <= '0;
      cap_ltssm <= '0; cap_tag <= '0; cap_job <= '0; cap_fifo_level <= '0; cap_cycle <= '0;
    end else begin
      cycle <= cycle + 32'd1;
      if (pcie_beat && c_pcie_bytes != '1) c_pcie_bytes <= c_pcie_bytes + 64'(pcie_bytes);
      if (app_beat  && c_app_bytes  != '1) c_app_bytes  <= c_app_bytes  + 64'(app_bytes);
      // Counting BEATS ACCEPTED, never `valid` cycles. A counter incremented
      // on valid alone overstates throughput whenever the sink stalls, which
      // is mutation 33 and makes every §17 measurement wrong.
      if (stall_credit     && c_credit  != '1) c_credit  <= c_credit + 1'b1;
      if (stall_tag        && c_tag     != '1) c_tag     <= c_tag + 1'b1;
      if (stall_fifo_full  && c_full    != '1) c_full    <= c_full + 1'b1;
      if (stall_fifo_empty && c_empty   != '1) c_empty   <= c_empty + 1'b1;
      if (stall_localmem   && c_localmem!= '1) c_localmem<= c_localmem + 1'b1;
 
      if (!captured && (this_cause != 4'd0)) begin
        captured       <= 1'b1;
        first_cause    <= this_cause;
        cap_ltssm      <= ltssm;
        cap_tag        <= tag_snapshot;
        cap_job        <= job_snapshot;
        cap_fifo_level <= fifo_level;
        cap_cycle      <= cycle;
      end
    end
  end
 
endmodule

internal throughput = bytes_per_beat × accepted_beats_per_cycle × clock_frequency

// P1 — the adapter buffers nothing: ready passes straight through.
property p1_adapter_transparent;
  @(posedge clk) disable iff (!rst_n)
    (core_rx_ready == app_rx_ready) && (app_tx_ready == core_tx_ready);
endproperty
a_p1: assert property (p1_adapter_transparent);
 
// P2 — a transfer offered and not accepted stays stable and stays offered.
property p2_stream_stable;
  @(posedge clk) disable iff (!rst_n)
    (out_valid && !out_ready) |=> (out_valid && $stable(out_data) &&
                                   $stable(out_keep) && $stable(out_last));
endproperty
a_p2: assert property (p2_stream_stable);
 
// P3 — valid does not depend on ready.
property p3_valid_independent;
  @(posedge clk) disable iff (!rst_n)
    (out_valid && !out_ready) |=> out_valid;
endproperty
a_p3: assert property (p3_valid_independent);
 
// P4 — a non-final beat is full; only the last beat may be partial.
property p4_keep_only_last;
  @(posedge clk) disable iff (!rst_n)
    (out_valid && out_ready && !out_last) |-> (out_keep == '1);
endproperty
a_p4: assert property (p4_keep_only_last);
 
// P5 — negotiated width is reported, never capability (26.2 §4).
property p5_negotiated_reported;
  @(posedge clk) disable iff (!rst_n)
    app_link_up |-> (app_neg_width == core_neg_width);
endproperty
a_p5: assert property (p5_negotiated_reported);

// P6 — an out-of-range or misaligned offset is reported, never wrapped.
property p6_offset_checked;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && (((req_offset >> 2) >= NREG) || (req_offset[1:0] != 2'b00)))
      |-> offset_error;
endproperty
a_p6: assert property (p6_offset_checked);
 
// P7 — a captured read response is held stable under backpressure and is
// NOT re-read from the live register file.
property p7_read_response_stable;
  @(posedge clk) disable iff (!rst_n)
    (rsp_valid && !rsp_ready) |=> (rsp_valid && $stable(rsp_rdata));
endproperty
a_p7: assert property (p7_read_response_stable);
 
// P8 — no new request is accepted while a response is pending.
property p8_one_outstanding;
  @(posedge clk) disable iff (!rst_n)
    rsp_pending |-> !req_ready;
endproperty
a_p8: assert property (p8_one_outstanding);

// P9 — a Tag is allocated only when free.
property p9_tag_free_on_alloc;
  @(posedge clk) disable iff (!rst_n)
    (alloc_req && alloc_gnt) |-> !busy[alloc_tag];
endproperty
a_p9: assert property (p9_tag_free_on_alloc);
 
// P10 — a Tag is freed on the LAST Completion, not the first.
property p10_free_on_last;
  @(posedge clk) disable iff (!rst_n)
    (cpl_accept && !cpl_last) |=> busy[$past(cpl_tag)];
endproperty
a_p10: assert property (p10_free_on_last);
 
// P11 — no Tag leaks: an allocated Tag is eventually freed.
property p11_no_tag_leak;
  @(posedge clk) disable iff (!rst_n)
    (alloc_req && alloc_gnt) |-> s_eventually !busy[$past(alloc_tag)];
endproperty
a_p11: assert property (p11_no_tag_leak);
 
// P12 — a Completion whose epoch does not match its Tag's epoch is rejected.
// §17 measured removing this: 62 misdeliveries, 70,976 bytes.
property p12_stale_epoch_rejected;
  @(posedge clk) disable iff (!rst_n)
    (cpl_valid && busy[cpl_tag] && (tag_epoch[cpl_tag] != cpl_epoch)) |-> !cpl_accept;
endproperty
a_p12: assert property (p12_stale_epoch_rejected);
 
// P13 — a Completion for a Tag that is not outstanding is rejected.
property p13_orphan_cpl_rejected;
  @(posedge clk) disable iff (!rst_n)
    (cpl_valid && !busy[cpl_tag]) |-> !cpl_accept;
endproperty
a_p13: assert property (p13_orphan_cpl_rejected);
 
// P14 — a stale Completion is COUNTED, never silently dropped.
property p14_stale_counted;
  @(posedge clk) disable iff (!rst_n)
    cpl_stale |=> (stale_count > $past(stale_count));
endproperty
a_p14: assert property (p14_stale_counted);
 
// P15 — the epoch advances on a reset or link-down event.
property p15_epoch_advances;
  @(posedge clk) disable iff (!rst_n)
    epoch_changed |=> (cur_epoch != $past(cur_epoch));
endproperty
a_p15: assert property (p15_epoch_advances);
 
// P16 — the epoch does not change otherwise.
property p16_epoch_stable;
  @(posedge clk) disable iff (!rst_n)
    !epoch_changed |=> $stable(cur_epoch);
endproperty
a_p16: assert property (p16_epoch_stable);

// P17 — the descriptor is snapshotted; the job record never changes.
// §17 measured a live read losing 143,872 bytes.
property p17_descriptor_immutable;
  @(posedge clk) disable iff (!rst_n)
    (active && !job_done) |=> (active && $stable(job));
endproperty
a_p17: assert property (p17_descriptor_immutable);
 
// P18 — bytes issued equal bytes described, at job completion.
property p18_bytes_conserved;
  @(posedge clk) disable iff (!rst_n)
    job_done |-> (bytes_issued == bytes_described);
endproperty
a_p18: assert property (p18_bytes_conserved);
 
// P19 — the engine never issues MORE than described. Two-sided, per
// 25.6 §4 law 1: a one-sided check reports an overrun as success.
property p19_no_overrun;
  @(posedge clk) disable iff (!rst_n)
    (bytes_issued <= bytes_described);
endproperty
a_p19: assert property (p19_no_overrun);
 
// P20 — the final chunk may be partial and must not be dropped.
// §17 measured 4,119 lost tails and a 263,616-byte deficit.
property p20_final_chunk;
  @(posedge clk) disable iff (!rst_n)
    (active && (remaining > 0) && (remaining < MAX_CHUNK))
      |-> (req_out.len_bytes == 12'(remaining));
endproperty
a_p20: assert property (p20_final_chunk);
 
// P21 — a zero-byte job issues no request.
property p21_zero_bytes;
  @(posedge clk) disable iff (!rst_n)
    (desc_valid && desc_ready && (desc_in.bytes == 0)) |=> !req_valid;
endproperty
a_p21: assert property (p21_zero_bytes);
 
// P22 — nothing is issued without a Tag.
property p22_tag_before_issue;
  @(posedge clk) disable iff (!rst_n)
    req_valid |-> tag_gnt;
endproperty
a_p22: assert property (p22_tag_before_issue);

// P23 — never write a full FIFO. §17 measured 105,801 overflows.
property p23_no_overflow;
  @(posedge clk) disable iff (!rst_n)
    wr_en |-> !wr_full;
endproperty
a_p23: assert property (p23_no_overflow);
 
// P24 — never read an empty FIFO. §17 measured 1,653 underflows.
property p24_no_underflow;
  @(posedge clk) disable iff (!rst_n)
    rd_en |-> !rd_empty;
endproperty
a_p24: assert property (p24_no_underflow);
 
// P25 — full and empty are never simultaneously true.
property p25_full_empty_exclusive;
  @(posedge clk) disable iff (!rst_n)
    !(wr_full && rd_empty && (DEPTH > 0));
endproperty
a_p25: assert property (p25_full_empty_exclusive);
 
// P26 — the handshake holds its data stable for the whole crossing.
// Counterexample A is what happens without this.
property p26_cdc_data_stable;
  @(posedge src_clk) disable iff (!src_rst_n)
    (src_req != src_ack) |=> $stable(hold);
endproperty
a_p26: assert property (p26_cdc_data_stable);
 
// P27 — the destination samples data only when dst_valid is asserted.
property p27_cdc_sample_qualified;
  @(posedge dst_clk) disable iff (!dst_rst_n)
    dst_valid |-> (dst_req != dst_ack_sync);
endproperty
a_p27: assert property (p27_cdc_sample_qualified);

// P28 — a memory response routes to the RECORDED owner.
property p28_response_to_owner;
  @(posedge clk) disable iff (!rst_n)
    rsp_valid |-> (rsp_route == (1 << rsp_id));
endproperty
a_p28: assert property (p28_response_to_owner);
 
// P29 — a response for a requester with nothing outstanding is reported.
property p29_misroute_reported;
  @(posedge clk) disable iff (!rst_n)
    (rsp_valid && !outstanding[rsp_id]) |-> rsp_misroute;
endproperty
a_p29: assert property (p29_misroute_reported);
 
// P30 — at most one grant per cycle, and only to a requester.
property p30_grant_onehot0;
  @(posedge clk) disable iff (!rst_n)
    $onehot0(req_grant) and ((req_grant & ~req_valid) == '0);
endproperty
a_p30: assert property (p30_grant_onehot0);
 
// P31 — the interrupt follows the status record, never precedes it.
// §17 measured 5,178 events raised ahead of their record.
property p31_int_after_status;
  @(posedge clk) disable iff (!rst_n)
    evt_valid |-> $past(status_accepted);
endproperty
a_p31: assert property (p31_int_after_status);

// P32 — every DMA job reaches a terminal state: it completes, or it is
// invalidated by an epoch change. A job that reaches neither holds its Tag
// forever, and §21 case 6's leak is exactly this failure accumulating.
property p32_job_terminal;
  @(posedge clk) disable iff (!rst_n)
    (desc_valid && desc_ready) |-> s_eventually (job_done || epoch_changed);
endproperty
a_p32: assert property (p32_job_terminal);
 
// P32's covers — the rare states must occur. §17's model needed randomly injected
// resets to produce any stale Completions at all; without them P12, P14,
// P15 and P16 are all vacuously satisfied.
c1_epoch_change: cover property (@(posedge clk) disable iff (!rst_n) epoch_changed);
c2_stale_cpl:    cover property (@(posedge clk) disable iff (!rst_n) cpl_stale);
c3_fifo_full:    cover property (@(posedge clk) disable iff (!rst_n) wr_full);
c4_fifo_empty:   cover property (@(posedge clk) disable iff (!rst_n) rd_empty);
c5_partial_beat: cover property (@(posedge clk) disable iff (!rst_n)
                   out_valid && out_last && (out_keep != '1));
c6_tag_exhaust:  cover property (@(posedge clk) disable iff (!rst_n) free_count == 0);
c7_mem_conflict: cover property (@(posedge clk) disable iff (!rst_n) req_valid == '1);
c8_offset_err:   cover property (@(posedge clk) disable iff (!rst_n) offset_error);
c9_status_stall: cover property (@(posedge clk) disable iff (!rst_n)
                   status_valid && !status_ready);

// Every bit of a 64-bit descriptor address crosses through its own
// two-flop synchronizer.
module ce_a_multibit_two_flop (
  input  logic dst_clk, dst_rst_n,
  input  logic [63:0] src_addr,
  output logic [63:0] dst_addr
);
  (* ASYNC_REG = "TRUE" *) logic [63:0] s1, s2;
  always_ff @(posedge dst_clk or negedge dst_rst_n)
    if (!dst_rst_n) begin s1 <= '0; s2 <= '0; end
    else begin s1 <= src_addr; s2 <= s1; end
  assign dst_addr = s2;              // <-- 64 independent crossings
endmodule
 
// Failing stimulus: src_addr changes from 64'h0000_0000_FFFF_FFFF to
// 64'h0000_0001_0000_0000 — 33 bits change at once.
// Golden: the destination sees one value or the other.
// This:   bits resolve on different edges, so the destination can sample
//         64'h0000_0001_FFFF_FFFF — a value that NEVER EXISTED in the
//         source domain.
// P26 fails.
// Observable consequence: a DMA write to an address neither the host nor
// the FPGA ever computed. Every bit is metastability-safe and the word is
// incoherent. §22 case 4 is what this looks like in hardware, and it is
// invisible in simulation without CDC-aware modelling.

// Completions are matched on Tag alone, with no epoch comparison.
module ce_b_no_epoch (
  input  logic       cpl_valid,
  input  logic [4:0] cpl_tag,
  input  logic [31:0] busy,
  output logic       cpl_accept
);
  assign cpl_accept = cpl_valid && busy[cpl_tag];    // <-- no epoch
endmodule
 
// Failing stimulus: job A issues a read on Tag 9; the link drops and
// recovers, reclaiming outstanding Tags; job B is issued on Tag 9; job A's
// Completion arrives.
// Golden: rejected as stale, counted, discarded.
// This:   accepted and credited to job B.
// P12 fails.
// §17 measured 62 misdeliveries carrying 70,976 bytes into wrong buffers
// across 133 reset events. The correct design saw 165 stale responses and
// misdelivered none — late responses are NORMAL, and discarding them is
// the design's job.

// The full flag is registered, so the write enable is qualified by a
// value that is one cycle old.
module ce_c_late_full_check (
  input  logic clk, rst_n,
  input  logic [15:0] level, input logic DEPTH_i,
  input  logic wr_req,
  output logic wr_en
);
  logic full_r;
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) full_r <= 1'b0;
    else        full_r <= (level >= 16'd32);      // <-- registered
  assign wr_en = wr_req && !full_r;
endmodule
 
// Failing stimulus: the FIFO reaches depth in cycle N with a write also
// requested in cycle N+1.
// Golden: wr_en is low in N+1.
// This:   full_r still reflects cycle N-1, so wr_en is high and a write
//         lands in a full FIFO.
// P23 fails.
// §17 measured 105,801 overflows. Observable consequence: silently
// corrupted payload, with byte conservation still balancing because the
// bytes were counted as written.

// A read answered by several split Completions frees its Tag on the first.
module ce_d_free_on_first (
  input  logic clk, rst_n,
  input  logic cpl_accept, input logic [4:0] cpl_tag,
  output logic [31:0] busy
);
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) busy <= '0;
    else if (cpl_accept) busy[cpl_tag] <= 1'b0;   // <-- ignores cpl_last
endmodule
 
// Failing stimulus: a 256-byte read split into four Completions at RCB.
// Golden: the Tag is freed on the fourth.
// This:   freed on the first. The Tag is reissued while three Completions
//         for the old request are still in flight, and they are credited
//         to the new one.
// P10 fails, and P12 cannot save it — the epoch is unchanged, so the stale
// Completions match. This is 25.7 §7's misdelivery window reproduced by a
// design error rather than by a timeout.

// The local memory response is delivered to whichever requester the
// arbiter is serving at the moment the response returns.
module ce_e_route_by_current (
  input  logic       rsp_valid,
  input  logic [0:0] arbiter_sel_now,
  output logic [1:0] rsp_route
);
  always_comb begin
    rsp_route = '0;
    if (rsp_valid) rsp_route[arbiter_sel_now] = 1'b1;   // <-- not the owner
  end
endmodule
 
// Failing stimulus: the accelerator issues a read; the arbiter then grants
// the DMA engine; the accelerator's read data returns.
// Golden: routed to the accelerator, which recorded the request.
// This:   routed to the DMA engine.
// P28 fails, P29 fails.
// Observable consequence: the DMA engine writes the accelerator's data to
// host memory and the accelerator waits forever. This is 26.4 §16's
// identity fault in a new place, and a conservation check on outstanding
// counts does not see it.

software writes control / builds work in memory
   → doorbell or configuration write               (a small BAR access)
      → device takes OWNERSHIP of the work         (by snapshot, not reference)
         → device generates PCIe requests          (Tags, credits, chunking)
            → data is placed                       (host memory or device memory)
               → local execution                   (media, compute, network)
                  → durable STATUS record          (a Posted write)
                     → NOTIFICATION                (MSI/MSI-X, strictly after)