Network Adapters — When a PCIe Limit Becomes Packet Loss

RECEIVE                                TRANSMIT
network ingress                        host writes descriptor + data
  → packet buffer                        → doorbell
  → PCIe DMA WRITE to host memory        → NIC DMA READ of the descriptor
  → status/completion published          → NIC DMA READ of the packet data
  → notification                         → packet buffer
                                         → network egress
                                         → status published → notification

RX ring                                TX ring
software posts EMPTY buffers           software posts FULL buffers
hardware fills them                    hardware drains them
hardware returns them with status      hardware returns them with status
software consumes the data             software frees the memory

package nic_pkg;
 
  typedef enum logic [0:0] { DIR_RX = 1'b0, DIR_TX = 1'b1 } ring_dir_e;
 
  // Why a frame was not delivered. Distinguishing these is the whole of §5:
  // "dropped" is a network statistic, and only the controller knows which of
  // three unrelated causes produced it.
  typedef enum logic [2:0] {
    DROP_NONE      = 3'd0,
    DROP_BUFFER    = 3'd1,   // packet buffer full — the PCIe path is behind
    DROP_NODESC    = 3'd2,   // no free host descriptor — software is behind
    DROP_QDISABLED = 3'd3,   // the queue is not enabled
    DROP_ERROR     = 3'd4    // network-side error; not a PCIe matter
  } drop_reason_e;
 
  function automatic int unsigned gw(input int unsigned n);
    return (n <= 1) ? 1 : $clog2(n);
  endfunction
 
  // A DMA request as the engine owns it: a SNAPSHOT taken when ownership
  // transfers. 25.6 §5 established why this is copied and not referenced.
  typedef struct packed {
    logic [15:0] queue_id;
    logic [15:0] desc_idx;
    ring_dir_e   dir;
    logic [63:0] host_addr;
    logic [15:0] bytes;
  } nic_xfer_t;
 
endpackage

module nic_queue_ctx #(
  parameter int unsigned NQUEUE = 8,
  parameter int unsigned MAXRING = 4096
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                 cfg_valid,
  input  logic [nic_pkg::gw(NQUEUE)-1:0]       cfg_qid,
  input  logic                                 cfg_enable,
  input  logic [nic_pkg::gw(MAXRING+1)-1:0]    cfg_depth,
  input  logic                                 db_valid,
  input  logic [nic_pkg::gw(NQUEUE)-1:0]       db_qid,
  input  logic [31:0]                          db_tail,
  input  logic                                 head_adv,
  input  logic [nic_pkg::gw(NQUEUE)-1:0]       head_qid,
  input  logic [nic_pkg::gw(NQUEUE)-1:0]       q_sel,
  output logic                                 q_enabled,
  output logic                                 q_has_work,
  output logic [nic_pkg::gw(MAXRING)-1:0]      q_head, q_tail,
  output logic                                 qid_error
);
 
  import nic_pkg::*;
 
  logic [NQUEUE-1:0] en;
  logic [gw(MAXRING+1)-1:0] depth [NQUEUE];
  logic [gw(MAXRING)-1:0]   head  [NQUEUE], tail [NQUEUE];
 
  // Every piece of per-queue state is INDEXED, never shared. A single global
  // head/tail pair across queues is mutation 11, and its symptom is that one
  // stalled queue stops every other — the cross-talk §16's identity oracle
  // measures.
  assign qid_error = (db_valid && (db_qid >= gw(NQUEUE)'(NQUEUE))) ||
                     (cfg_valid && (cfg_qid >= gw(NQUEUE)'(NQUEUE)));
 
  assign q_enabled  = en[q_sel];
  assign q_head     = head[q_sel];
  assign q_tail     = tail[q_sel];
  assign q_has_work = 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;
      end
    end else begin
      if (cfg_valid && !qid_error) begin
        en[cfg_qid]    <= cfg_enable;
        depth[cfg_qid] <= cfg_depth;
        head[cfg_qid]  <= '0;
        tail[cfg_qid]  <= '0;
      end
      if (db_valid && !qid_error && en[db_qid] && (db_tail < 32'(depth[db_qid])))
        tail[db_qid] <= gw(MAXRING)'(db_tail);
      if (head_adv && en[head_qid])
        head[head_qid] <= (head[head_qid] == gw(MAXRING)'(depth[head_qid]-1))
                        ? '0 : head[head_qid] + 1'b1;
    end
  end
 
endmodule

module nic_buffer_account #(
  parameter int unsigned BUFCAP = 256
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                   pkt_arrive,
  input  logic                                   q_enabled,
  input  logic                                   desc_available,
  input  logic                                   drain_done,      // a frame left for host memory
  output logic                                   accept,
  output nic_pkg::drop_reason_e                  drop_reason,
  output logic [nic_pkg::gw(BUFCAP+1)-1:0]       occupancy,
  output logic [31:0]                            c_drop_buffer, c_drop_nodesc, c_drop_qdis
);
 
  import nic_pkg::*;
 
  // Acceptance depends on BUFFER SPACE only. Descriptor availability is a
  // separate question answered later, because a frame with buffer space but
  // no descriptor can WAIT — dropping it is throwing away a frame the
  // adapter had room for (§8 audit A, mutation 14).
  always_comb begin
    accept      = pkt_arrive && q_enabled && (occupancy < gw(BUFCAP+1)'(BUFCAP));
    drop_reason = DROP_NONE;
    if (pkt_arrive && !q_enabled)                                   drop_reason = DROP_QDISABLED;
    else if (pkt_arrive && (occupancy >= gw(BUFCAP+1)'(BUFCAP)))    drop_reason = DROP_BUFFER;
  end
 
  // The three drop counters are SEPARATE. §5's whole point is that "receive
  // drops" is one network statistic covering three unrelated causes: the
  // PCIe path is behind (DROP_BUFFER), software is behind (DROP_NODESC), or
  // the queue is down. Merging them makes §18 case 2 unanswerable.
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      occupancy <= '0; c_drop_buffer <= '0; c_drop_nodesc <= '0; c_drop_qdis <= '0;
    end else begin
      case ({accept, drain_done})
        2'b10: occupancy <= occupancy + 1'b1;
        2'b01: occupancy <= occupancy - 1'b1;
        default: ;
      endcase
      if (drop_reason == DROP_BUFFER    && c_drop_buffer != '1) c_drop_buffer <= c_drop_buffer + 1'b1;
      if (drop_reason == DROP_QDISABLED && c_drop_qdis   != '1) c_drop_qdis   <= c_drop_qdis + 1'b1;
      if (pkt_arrive && q_enabled && !desc_available && c_drop_nodesc != '1)
        c_drop_nodesc <= c_drop_nodesc + 1'b1;
    end
  end
 
endmodule

module nic_rx_alloc #(
  parameter int unsigned NQUEUE  = 8,
  parameter int unsigned NINFLT  = 32
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                 frame_ready,     // a buffered frame needs a home
  input  logic [nic_pkg::gw(NQUEUE)-1:0]       frame_qid,
  input  logic [15:0]                          frame_bytes,
  input  logic                                 desc_avail,
  input  logic [15:0]                          desc_idx,
  input  logic [63:0]                          desc_host_addr,
  output logic                                 alloc_valid,
  output nic_pkg::nic_xfer_t                   alloc_xfer,
  input  logic                                 alloc_ready,
  input  logic                                 status_accepted, // the completion was published
  input  logic [nic_pkg::gw(NINFLT)-1:0]       status_slot,
  output logic                                 recycle_valid,
  output logic [15:0]                          recycle_idx,
  output logic [nic_pkg::gw(NINFLT+1)-1:0]     inflight
);
 
  import nic_pkg::*;
 
  logic [NINFLT-1:0] busy;
  logic [15:0]       held_idx [NINFLT];
  logic [gw(NINFLT)-1:0] alloc_slot;
 
  always_comb begin
    alloc_slot = '0;
    for (int i = NINFLT-1; i >= 0; i--) if (!busy[i]) alloc_slot = gw(NINFLT)'(i);
 
    alloc_valid = frame_ready && desc_avail && (busy != '1);
    alloc_xfer  = '{queue_id:  16'(frame_qid),
                    desc_idx:  desc_idx,
                    dir:       DIR_RX,
                    host_addr: desc_host_addr,
                    bytes:     frame_bytes};
 
    // The descriptor returns to software ONLY when its status has been
    // ACCEPTED — not when the last data beat moved. Recycling on the beat is
    // counterexample A: software sees a buffer marked ready while the write
    // to it may still be in flight (§8 audit B).
    recycle_valid = status_accepted && busy[status_slot];
    recycle_idx   = held_idx[status_slot];
 
    inflight = '0;
    for (int i = 0; i < NINFLT; i++) inflight += gw(NINFLT+1)'(busy[i]);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      busy <= '0;
      for (int i = 0; i < NINFLT; i++) held_idx[i] <= '0;
    end else begin
      if (alloc_valid && alloc_ready) begin
        busy[alloc_slot]     <= 1'b1;
        held_idx[alloc_slot] <= desc_idx;
      end
      if (recycle_valid) busy[status_slot] <= 1'b0;
    end
  end
 
endmodule

module nic_tx_fetch #(
  parameter int unsigned NQUEUE = 8
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                 q_has_work,
  input  logic [nic_pkg::gw(NQUEUE)-1:0]       q_sel,
  input  logic [63:0]                          ring_base,
  input  logic [15:0]                          ring_head,
  // stage 1: fetch the DESCRIPTOR
  output logic                                 dfetch_valid,
  output logic [63:0]                          dfetch_addr,
  input  logic                                 dfetch_ready,
  input  logic                                 dfetch_data_valid,
  input  logic [63:0]                          dfetch_pkt_addr,
  input  logic [15:0]                          dfetch_pkt_bytes,
  // stage 2: fetch the PACKET DATA, only after the descriptor returned
  output logic                                 pfetch_valid,
  output nic_pkg::nic_xfer_t                   pfetch_xfer,
  input  logic                                 pfetch_ready,
  output logic                                 head_adv
);
 
  import nic_pkg::*;
  localparam int unsigned DESC_BYTES = 16;      // IMPLEMENTATION POLICY
 
  typedef enum logic [1:0] {T_IDLE, T_DFETCH, T_PFETCH} st_e;
  st_e st;
  logic [63:0] pkt_addr;
  logic [15:0] pkt_bytes, cur_qid;
 
  // Two DISTINCT fetches. The descriptor tells the adapter where the packet
  // is; the packet fetch cannot be issued until that answer returns. Merging
  // them is mutation 17 — it issues a read against an address the adapter
  // has not yet been told.
  always_comb begin
    dfetch_valid = (st == T_DFETCH);
    dfetch_addr  = ring_base + 64'(ring_head) * DESC_BYTES;
    pfetch_valid = (st == T_PFETCH);
    pfetch_xfer  = '{queue_id: cur_qid, desc_idx: ring_head, dir: DIR_TX,
                     host_addr: pkt_addr, bytes: pkt_bytes};
    head_adv     = dfetch_valid && dfetch_ready;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st <= T_IDLE; pkt_addr <= '0; pkt_bytes <= '0; cur_qid <= '0;
    end else begin
      unique case (st)
        T_IDLE:   if (q_has_work) begin st <= T_DFETCH; cur_qid <= 16'(q_sel); end
        T_DFETCH: if (dfetch_data_valid) begin
                    pkt_addr  <= dfetch_pkt_addr;
                    pkt_bytes <= dfetch_pkt_bytes;
                    st        <= T_PFETCH;
                  end
        T_PFETCH: if (pfetch_valid && pfetch_ready) st <= T_IDLE;
        default:  st <= T_IDLE;
      endcase
    end
  end
 
endmodule

module nic_queue_arbiter #(
  parameter int unsigned NQUEUE = 8
)(
  input  logic clk,
  input  logic rst_n,
  input  logic [NQUEUE-1:0]              q_request,
  input  logic [NQUEUE-1:0]              q_blocked,   // this queue cannot proceed
  output logic [NQUEUE-1:0]              q_grant,
  output logic                           any_grant,
  output logic [nic_pkg::gw(NQUEUE)-1:0] grant_qid
);
 
  import nic_pkg::*;
  logic [gw(NQUEUE)-1:0] rr;
  logic [NQUEUE-1:0]     eligible;
  logic                  found;
  logic [gw(NQUEUE)-1:0] sel;
 
  always_comb begin
    // A BLOCKED queue is skipped rather than held at the head of the
    // arbiter. This is the isolation property: one queue that cannot make
    // progress must not prevent every other queue from being served
    // (mutation 20), which is 25.8 §15's per-class lesson applied to queues.
    eligible = q_request & ~q_blocked;
    sel = rr; found = 1'b0;
    for (int k = 0; k < NQUEUE; k++) begin
      automatic logic [gw(NQUEUE)-1:0] i = gw(NQUEUE)'((rr + k) % NQUEUE);
      if (!found && eligible[i]) begin sel = i; found = 1'b1; end
    end
    any_grant = found;
    grant_qid = sel;
    q_grant   = '0;
    if (found) q_grant[sel] = 1'b1;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) rr <= '0;
    else if (any_grant) rr <= (sel == gw(NQUEUE)'(NQUEUE-1)) ? '0 : sel + 1'b1;
  end
 
endmodule

module nic_rx_complete #(
  parameter int unsigned NINFLT = 32
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                dma_last_beat,
  input  logic [nic_pkg::gw(NINFLT)-1:0]      dma_slot,
  input  logic [15:0]                         dma_bytes,
  output logic                                status_valid,
  output logic [nic_pkg::gw(NINFLT)-1:0]      status_slot,
  output logic [15:0]                         status_bytes,
  input  logic                                status_ready,
  input  logic                                status_accepted,
  output logic                                evt_valid,
  output logic [nic_pkg::gw(NINFLT)-1:0]      evt_slot,
  input  logic                                evt_ready
);
 
  import nic_pkg::*;
 
  typedef enum logic [1:0] {C_IDLE, C_STATUS, C_EVENT} st_e;
  st_e st;
  logic [gw(NINFLT)-1:0] slot;
  logic [15:0]           bytes;
 
  // The order is: durable status record first, notification second. An
  // interrupt is not the authoritative completion state (19.x), and this
  // module enforces the sequence rather than assuming it.
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st <= C_IDLE; slot <= '0; bytes <= '0;
    end else begin
      unique case (st)
        C_IDLE:   if (dma_last_beat) begin slot <= dma_slot; bytes <= dma_bytes; st <= C_STATUS; end
        C_STATUS: if (status_valid && status_ready && status_accepted) st <= C_EVENT;
        C_EVENT:  if (evt_valid && evt_ready) st <= C_IDLE;
        default:  st <= C_IDLE;
      endcase
    end
  end
 
  assign status_valid = (st == C_STATUS);
  assign status_slot  = slot;
  assign status_bytes = bytes;
  assign evt_valid    = (st == C_EVENT);
  assign evt_slot     = slot;
 
endmodule

module nic_vector_snapshot #(
  parameter int unsigned NQUEUE = 8,
  parameter int unsigned NVEC   = 16
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                 evt_valid,
  input  logic [nic_pkg::gw(NQUEUE)-1:0]       evt_qid,
  input  logic [nic_pkg::gw(NVEC)-1:0]         vec_table [NQUEUE],  // host-writable, LIVE
  output logic                                 int_req,
  output logic [nic_pkg::gw(NVEC)-1:0]         int_vector,
  output logic [nic_pkg::gw(NQUEUE)-1:0]       int_qid,
  input  logic                                 int_ack
);
 
  import nic_pkg::*;
 
  logic                    pending;
  logic [gw(NVEC)-1:0]     snap_vec;
  logic [gw(NQUEUE)-1:0]   snap_qid;
 
  // The mapping is SNAPSHOTTED when the event takes ownership, and the
  // pending request is driven from the snapshot. Reading vec_table live
  // while the request is stalled sends the notification to a vector the
  // host has since reprogrammed (mutation 24, §8 audit C).
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      pending <= 1'b0; snap_vec <= '0; snap_qid <= '0;
    end else begin
      if (evt_valid && !pending) begin
        pending  <= 1'b1;
        snap_vec <= vec_table[evt_qid];
        snap_qid <= evt_qid;
      end else if (int_req && int_ack) begin
        pending <= 1'b0;
      end
    end
  end
 
  assign int_req    = pending;
  assign int_vector = snap_vec;
  assign int_qid    = snap_qid;
 
endmodule

module nic_coalesce #(
  parameter int unsigned PKT_THRESH = 16,      // IMPLEMENTATION POLICY
  parameter int unsigned TIMER_LIMIT = 200     // IMPLEMENTATION POLICY
)(
  input  logic clk,
  input  logic rst_n,
  input  logic        completion_event,
  input  logic        int_taken,
  output logic        int_request,
  output logic [15:0] batch_count,
  output logic [31:0] c_interrupts, c_events
);
 
  // PCIe specifies NOTHING about interrupt batching. This is a device policy
  // that trades latency for interrupt rate, and §17 measured its effect:
  // one interrupt per packet gave 71,991 interrupts for 71,991 packets;
  // a threshold of 16 gave 4,499; a threshold of 64 gave 1,124.
  logic [15:0] cnt;
  logic [31:0] timer;
  logic        thresh_hit, timer_hit;
 
  // Both terms use the NEXT value. `cnt == PKT_THRESH` on the old value is
  // one packet late, and `>` instead of `>=` waits for the 17th packet —
  // §17 measured that off-by-one firing 4,234 times instead of 4,499.
  assign thresh_hit  = ((cnt + 16'd1) >= 16'(PKT_THRESH)) && completion_event;
  assign timer_hit   = ((timer + 32'd1) >= 32'(TIMER_LIMIT)) && (cnt != 0);
  assign int_request = thresh_hit || timer_hit;
  assign batch_count = cnt;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cnt <= '0; timer <= '0; c_interrupts <= '0; c_events <= '0;
    end else begin
      if (completion_event && c_events != '1) c_events <= c_events + 1'b1;
      // Both conditions true in one cycle close the batch ONCE (§8 audit D).
      if (int_request && int_taken) begin
        cnt <= '0; timer <= '0;
        if (c_interrupts != '1) c_interrupts <= c_interrupts + 1'b1;
      end else begin
        if (completion_event) cnt <= cnt + 16'd1;
        if (cnt != 0) timer <= timer + 32'd1;
      end
    end
  end
 
endmodule

module nic_counters (
  input  logic clk,
  input  logic rst_n,
  input  logic rx_beat, input logic [15:0] rx_bytes,
  input  logic tx_beat, input logic [15:0] tx_bytes,
  input  logic stall_link,       // credit or Tag exhaustion
  input  logic stall_hostmem,    // the write is accepted slowly upstream
  input  logic stall_nodesc,     // no free host descriptor
  input  logic clear,
  output logic [63:0] c_rx_bytes, c_tx_bytes,
  output logic [31:0] c_link, c_hostmem, c_nodesc
);
 
  // §5's three candidates, counted separately. "RX drops" is one network
  // statistic; these three counters are what turn it into a diagnosis, and
  // the third — no free descriptor — is a SOFTWARE limit that looks exactly
  // like a PCIe one from the network side.
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_rx_bytes <= '0; c_tx_bytes <= '0;
      c_link <= '0; c_hostmem <= '0; c_nodesc <= '0;
    end else begin
      if (rx_beat && c_rx_bytes != '1) c_rx_bytes <= c_rx_bytes + 64'(rx_bytes);
      if (tx_beat && c_tx_bytes != '1) c_tx_bytes <= c_tx_bytes + 64'(tx_bytes);
      if (stall_link    && c_link    != '1) c_link    <= c_link + 1'b1;
      if (stall_hostmem && c_hostmem != '1) c_hostmem <= c_hostmem + 1'b1;
      if (stall_nodesc  && c_nodesc  != '1) c_nodesc  <= c_nodesc + 1'b1;
    end
  end
 
endmodule

// P1 — every queue's state is independent: configuring one leaves others alone.
property p1_queue_isolation;
  @(posedge clk) disable iff (!rst_n)
    (cfg_valid && (cfg_qid != q_sel)) |=> ($stable(head[q_sel]) && $stable(tail[q_sel]));
endproperty
a_p1: assert property (p1_queue_isolation);
 
// P2 — an out-of-range queue id is reported, never wrapped.
property p2_qid_range;
  @(posedge clk) disable iff (!rst_n)
    ((db_valid && (db_qid >= NQUEUE)) || (cfg_valid && (cfg_qid >= NQUEUE))) |-> qid_error;
endproperty
a_p2: assert property (p2_qid_range);
 
// P3 — a disabled queue accepts no work.
property p3_disabled_inert;
  @(posedge clk) disable iff (!rst_n)
    !q_enabled |-> !q_has_work;
endproperty
a_p3: assert property (p3_disabled_inert);
 
// P4 — pointers stay within the configured depth.
property p4_pointers_bounded;
  @(posedge clk) disable iff (!rst_n)
    q_enabled |-> ((q_head < cfg_depth) && (q_tail < cfg_depth));
endproperty
a_p4: assert property (p4_pointers_bounded);
 
// P5 — configuring a queue resets its pointers.
property p5_cfg_resets;
  @(posedge clk) disable iff (!rst_n)
    (cfg_valid && !qid_error) |=> ((head[$past(cfg_qid)] == '0) && (tail[$past(cfg_qid)] == '0));
endproperty
a_p5: assert property (p5_cfg_resets);

// P6 — occupancy never exceeds capacity.
property p6_occupancy_bounded;
  @(posedge clk) disable iff (!rst_n)
    (occupancy <= BUFCAP);
endproperty
a_p6: assert property (p6_occupancy_bounded);
 
// P7 — occupancy never underflows.
property p7_no_underflow;
  @(posedge clk) disable iff (!rst_n)
    (occupancy == 0) |-> !drain_done;
endproperty
a_p7: assert property (p7_no_underflow);
 
// P8 — a frame is accepted only if there is room for it.
property p8_accept_needs_room;
  @(posedge clk) disable iff (!rst_n)
    accept |-> (occupancy < BUFCAP);
endproperty
a_p8: assert property (p8_accept_needs_room);
 
// P9 — a dropped frame always has exactly one recorded reason. §5's whole
// argument: "RX drops" covers three unrelated causes.
property p9_drop_reason_unique;
  @(posedge clk) disable iff (!rst_n)
    (pkt_arrive && !accept) |-> (drop_reason != DROP_NONE);
endproperty
a_p9: assert property (p9_drop_reason_unique);
 
// P10 — a frame is never dropped for lack of a descriptor while buffer space
// exists. It waits instead (§8 audit A).
property p10_nodesc_does_not_drop;
  @(posedge clk) disable iff (!rst_n)
    (pkt_arrive && q_enabled && (occupancy < BUFCAP) && !desc_available)
      |-> (accept && (drop_reason == DROP_NONE));
endproperty
a_p10: assert property (p10_nodesc_does_not_drop);

// P11 — a descriptor is allocated only when free.
property p11_alloc_when_free;
  @(posedge clk) disable iff (!rst_n)
    (alloc_valid && alloc_ready) |-> !busy[alloc_slot];
endproperty
a_p11: assert property (p11_alloc_when_free);
 
// P12 — a descriptor is recycled only after its STATUS was accepted, never
// on the last data beat. Counterexample A; §16 measured 479,609 violations.
property p12_recycle_after_status;
  @(posedge clk) disable iff (!rst_n)
    recycle_valid |-> status_accepted;
endproperty
a_p12: assert property (p12_recycle_after_status);
 
// P13 — a host buffer is not reused while hardware owns it.
property p13_no_reuse_while_owned;
  @(posedge clk) disable iff (!rst_n)
    (busy[s] && !recycle_valid) |=> busy[s];
endproperty
a_p13: assert property (p13_no_reuse_while_owned);
 
// P14 — the in-flight count agrees with the busy vector at all times. This
// is the CONSERVATION oracle of §16, and it is blind to cross-talk.
property p14_inflight_consistent;
  @(posedge clk) disable iff (!rst_n)
    (inflight == $countones(busy));
endproperty
a_p14: assert property (p14_inflight_consistent);
 
// P15 — a completion returns to the queue that issued it. This is the
// IDENTITY oracle of §16, and it is blind to premature recycling. Both are
// required; neither is sufficient.
property p15_completion_queue_identity;
  @(posedge clk) disable iff (!rst_n)
    recycle_valid |-> (alloc_xfer_qid_of[status_slot] == status_qid);
endproperty
a_p15: assert property (p15_completion_queue_identity);
 
// P16 — the transfer request is immutable while it waits.
property p16_xfer_stable;
  @(posedge clk) disable iff (!rst_n)
    (alloc_valid && !alloc_ready) |=> (alloc_valid && $stable(alloc_xfer));
endproperty
a_p16: assert property (p16_xfer_stable);

// P17 — the packet fetch follows the descriptor fetch, never precedes it.
property p17_packet_after_descriptor;
  @(posedge clk) disable iff (!rst_n)
    pfetch_valid |-> $past(dfetch_data_valid, 1) or (st == T_PFETCH);
endproperty
a_p17: assert property (p17_packet_after_descriptor);
 
// P18 — the packet address comes from the fetched descriptor.
property p18_packet_addr_from_desc;
  @(posedge clk) disable iff (!rst_n)
    (dfetch_data_valid) |=> (pkt_addr == $past(dfetch_pkt_addr));
endproperty
a_p18: assert property (p18_packet_addr_from_desc);
 
// P19 — the head advances once per descriptor fetched.
property p19_head_once;
  @(posedge clk) disable iff (!rst_n)
    head_adv |-> (dfetch_valid && dfetch_ready);
endproperty
a_p19: assert property (p19_head_once);

// P20 — at most one queue granted per cycle.
property p20_grant_onehot0;
  @(posedge clk) disable iff (!rst_n)
    $onehot0(q_grant);
endproperty
a_p20: assert property (p20_grant_onehot0);
 
// P21 — a blocked queue is never granted, and never blocks the others.
property p21_blocked_skipped;
  @(posedge clk) disable iff (!rst_n)
    q_blocked[i] |-> !q_grant[i];
endproperty
a_p21: assert property (p21_blocked_skipped);
 
// P22 — an eligible queue is eventually granted (no starvation).
property p22_no_starvation;
  @(posedge clk) disable iff (!rst_n)
    (q_request[i] && !q_blocked[i]) |-> s_eventually q_grant[i];
endproperty
a_p22: assert property (p22_no_starvation);
 
// P23 — a queue that is blocked does not prevent another from being served.
// 25.8 §15's per-class lesson, applied to queues.
property p23_isolation_under_block;
  @(posedge clk) disable iff (!rst_n)
    ((q_request & ~q_blocked) != '0) |-> any_grant;
endproperty
a_p23: assert property (p23_isolation_under_block);

// P24 — the event never precedes the status publication.
property p24_event_after_status;
  @(posedge clk) disable iff (!rst_n)
    evt_valid |-> $past(status_accepted);
endproperty
a_p24: assert property (p24_event_after_status);
 
// P25 — the vector is snapshotted at event ownership and held.
property p25_vector_snapshot_stable;
  @(posedge clk) disable iff (!rst_n)
    (int_req && !int_ack) |=> (int_req && $stable(int_vector) && $stable(int_qid));
endproperty
a_p25: assert property (p25_vector_snapshot_stable);
 
// P26 — a batch closes exactly once even when both triggers fire together.
property p26_batch_closes_once;
  @(posedge clk) disable iff (!rst_n)
    (int_request && int_taken) |=> (batch_count == 16'd0);
endproperty
a_p26: assert property (p26_batch_closes_once);
 
// P27 — the coalescing count is exact: the threshold fires ON the Nth event.
// §17 measured `>` instead of `>=` firing 4,234 times instead of 4,499.
property p27_threshold_exact;
  @(posedge clk) disable iff (!rst_n)
    (completion_event && ((batch_count + 1) == PKT_THRESH)) |-> int_request;
endproperty
a_p27: assert property (p27_threshold_exact);

// P28 — a frame reaches exactly one outcome: accepted into the buffer, or
// dropped with a recorded reason. A frame that produces neither has been
// lost with no counter naming it, which makes §5's three-way attribution
// unavailable for that frame forever.
property p28_frame_outcome_total;
  @(posedge clk) disable iff (!rst_n)
    pkt_arrive |-> (accept ^ (drop_reason != DROP_NONE));
endproperty
a_p28: assert property (p28_frame_outcome_total);
 
// P28's covers — the load-dependent states must occur. §15 measured ZERO drops at two
// of four drain rates, which makes P8, P9 and P10 vacuous against a test
// whose host keeps up.
c1_buffer_full: cover property (@(posedge clk) disable iff (!rst_n) occupancy == BUFCAP);
c2_drop_buffer: cover property (@(posedge clk) disable iff (!rst_n) drop_reason == DROP_BUFFER);
c3_no_desc:     cover property (@(posedge clk) disable iff (!rst_n)
                  pkt_arrive && q_enabled && !desc_available);
c4_queue_block: cover property (@(posedge clk) disable iff (!rst_n) q_blocked != '0);
c5_vec_rewrite: cover property (@(posedge clk) disable iff (!rst_n)
                  int_req && !int_ack && vec_write);
c6_both_trig:   cover property (@(posedge clk) disable iff (!rst_n) thresh_hit && timer_hit);
c7_all_inflt:   cover property (@(posedge clk) disable iff (!rst_n) busy == '1);
c8_ring_wrap:   cover property (@(posedge clk) disable iff (!rst_n)
                  head_adv && (q_head == cfg_depth - 1));

// The RX descriptor is returned to software when the final data beat moves,
// rather than when the status write has been accepted.
module ce_a_recycle_on_beat (
  input  logic clk, rst_n,
  input  logic        dma_last_beat,
  input  logic [4:0]  dma_slot,
  output logic        recycle_valid,
  output logic [4:0]  recycle_slot
);
  assign recycle_valid = dma_last_beat;      // <-- not status_accepted
  assign recycle_slot  = dma_slot;
endmodule
 
// Failing stimulus: the last beat is issued, and the status write is
// back-pressured for several cycles.
// Golden: the descriptor stays owned until status_accepted.
// This:   software sees the descriptor returned and reads the buffer while
//         the final write may still be in flight.
// P12 fails. P14's conservation oracle reports 479,609 violations (§16).
// Observable consequence: intermittent short or corrupted frames delivered
// to the network stack, at a rate that rises with host-memory latency.

// The completion path derives the queue from the current arbiter selection
// rather than from the record made when the transfer was issued.
module ce_b_cross_queue_completion (
  input  logic [2:0] arbiter_qid_now,     // whatever the arbiter is serving
  input  logic       completion_valid,
  output logic [2:0] credit_qid
);
  assign credit_qid = arbiter_qid_now;    // <-- not the issuing queue
endmodule
 
// Failing stimulus: two queues with transfers in flight; a completion for
// queue 1 returns while the arbiter is serving queue 2.
// Golden: queue 1 is credited.
// This:   queue 2 is credited. Queue 1 leaks an owned descriptor and queue 2
//         gains one it never issued.
// P15 fails. P14's CONSERVATION oracle reports ZERO — the wrong ring's
// decrement and increment cancel, so every ring's sum stays correct (§16).
// §16 measured 3,284 such events. Observable consequence: one queue slowly
// runs out of descriptors while another accumulates phantom free entries.

// All discarded frames increment one counter.
module ce_c_merged_drops (
  input  logic clk, rst_n,
  input  logic pkt_arrive, accept,
  output logic [31:0] rx_drops
);
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) rx_drops <= '0;
    else if (pkt_arrive && !accept) rx_drops <= rx_drops + 1'b1;
endmodule
 
// Failing stimulus: a run mixing buffer-full drops, no-descriptor stalls and
// frames arriving on a disabled queue.
// Golden: three separate counters naming three unrelated causes.
// This:   one number. A reading of 23,495 is consistent with a PCIe/host
//         bandwidth shortfall (§15 row 3), with software failing to post
//         descriptors, and with a queue that was never enabled.
// P9 fails.
// Observable consequence: §21 case 2 is unanswerable. The three causes have
// three different owners — the platform, the driver, and configuration —
// and no further analysis of a merged counter can separate them.