PCIe in CPUs — The Root Complex as an Ownership Boundary

CPU cores
   ↕   virtual → physical translation happens HERE, in the core's MMU
cache / coherent interconnect
   ↕
SoC / I/O fabric ──────────────► memory controller ──► DRAM
   ↕
IOMMU / address translation      (device-side translation, a different step)
   ↕
PCIe Root Complex
   ↕
Root Ports
   ↕
PCIe hierarchy — Endpoints, Switches

device-visible I/O virtual address (IOVA)
   → translation, using the device's identity
   → permission check
   → host physical address

package rc_pkg;
 
  // §3's total classification. ERROR is a first-class outcome, never a default
  // branch — §13 measured that letting unclaimed addresses fall through to
  // MMIO produced 50,346 spurious PCIe transactions in 200,000 probes.
  typedef enum logic [2:0] {
    ACL_NONE   = 3'd0,
    ACL_DRAM   = 3'd1,
    ACL_MMIO   = 3'd2,
    ACL_CFG    = 3'd3,
    ACL_ERROR  = 3'd4
  } addr_class_e;
 
  // Which host-side boundary rejected or failed first (§17's recorder).
  typedef enum logic [2:0] {
    RCF_NONE      = 3'd0,
    RCF_CLASSIFY  = 3'd1,   // no window owns the address
    RCF_PORT      = 3'd2,   // no Root Port claims an MMIO address
    RCF_XLATE     = 3'd3,   // translation faulted
    RCF_CTX       = 3'd4,   // no free translation context
    RCF_FABRIC    = 3'd5    // downstream fabric refused
  } rc_fault_e;
 
  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 window is [base, limit] INCLUSIVE. Naming the convention once, here,
  // is what keeps 25.5 §6's off-by-one out of every comparator below.
  typedef struct packed {
    logic        valid;
    logic [63:0] base;
    logic [63:0] limit;      // last owned byte
  } window_t;
 
  function automatic logic in_window(input window_t w, input logic [63:0] a);
    return w.valid && (a >= w.base) && (a <= w.limit);
  endfunction
 
endpackage

module host_addr_classify #(
  parameter int unsigned NMMIO = 4        // MMIO windows the platform routes to PCIe
)(
  input  logic                    req_valid,
  input  logic [63:0]             req_addr,
  input  rc_pkg::window_t         dram_win,
  input  rc_pkg::window_t         cfg_win,
  input  rc_pkg::window_t         mmio_win [NMMIO],
  output rc_pkg::addr_class_e     acl,
  output logic [rc_pkg::gw(NMMIO)-1:0] mmio_idx,
  output logic                    ambiguous
);
 
  import rc_pkg::*;
 
  logic hit_dram, hit_cfg;
  logic [NMMIO-1:0] hit_mmio;
  logic [gw(NMMIO+1)-1:0] nhit;
 
  always_comb begin
    // Every window is range-checked at FULL width. §13's third row measured a
    // low-32 comparator misrouting 39,648 MMIO accesses into DRAM — answered
    // by memory, with no error raised anywhere.
    hit_dram = in_window(dram_win, req_addr);
    hit_cfg  = in_window(cfg_win , req_addr);
    for (int i = 0; i < NMMIO; i++) hit_mmio[i] = in_window(mmio_win[i], req_addr);
 
    nhit = gw(NMMIO+1)'(hit_dram) + gw(NMMIO+1)'(hit_cfg);
    for (int i = 0; i < NMMIO; i++) nhit += gw(NMMIO+1)'(hit_mmio[i]);
 
    // More than one owner is a configuration error, reported rather than
    // resolved — the three-outcome decoder of 23.6 §5 and 25.5 §3.
    ambiguous = req_valid && (nhit > 1);
 
    mmio_idx = '0;
    for (int i = NMMIO-1; i >= 0; i--) if (hit_mmio[i]) mmio_idx = gw(NMMIO)'(i);
 
    if      (!req_valid)  acl = ACL_NONE;
    else if (ambiguous)   acl = ACL_ERROR;
    else if (hit_dram)    acl = ACL_DRAM;
    else if (hit_cfg)     acl = ACL_CFG;
    else if (|hit_mmio)   acl = ACL_MMIO;
    // The default is ERROR, not MMIO. This single line is the difference
    // between §13's healthy row and its 50,346 spurious transactions.
    else                  acl = ACL_ERROR;
  end
 
endmodule

module rc_port_route #(
  parameter int unsigned NPORT = 4
)(
  input  logic                  req_valid,
  input  rc_pkg::addr_class_e   acl,
  input  logic [63:0]           req_addr,
  input  rc_pkg::window_t       port_win [NPORT],
  output logic                  route_valid,
  output logic [rc_pkg::gw(NPORT)-1:0] port_idx,
  output logic                  no_port,
  output logic                  multi_port
);
 
  import rc_pkg::*;
  logic [NPORT-1:0] hit;
  logic [gw(NPORT+1)-1:0] n;
 
  always_comb begin
    for (int i = 0; i < NPORT; i++) hit[i] = in_window(port_win[i], req_addr);
    n = '0;
    for (int i = 0; i < NPORT; i++) n += gw(NPORT+1)'(hit[i]);
 
    // Port routing is attempted ONLY for addresses classified as MMIO.
    // A design that routes before classifying cannot distinguish "no port
    // owns this" from "the platform does not own this" (mutation 6).
    no_port     = req_valid && (acl == ACL_MMIO) && (n == 0);
    multi_port  = req_valid && (acl == ACL_MMIO) && (n >  1);
    route_valid = req_valid && (acl == ACL_MMIO) && (n == 1);
 
    port_idx = '0;
    if (route_valid)
      for (int i = NPORT-1; i >= 0; i--) if (hit[i]) port_idx = gw(NPORT)'(i);
  end
 
endmodule

module rp_request_queue #(
  parameter int unsigned DEPTH = 8
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                  enq_valid,
  output logic                  enq_ready,
  input  logic [2:0]            enq_type,
  input  logic [63:0]           enq_addr,
  input  logic [11:0]           enq_len,
  input  logic [15:0]           enq_rid,       // requester context
  output logic                  deq_valid,
  input  logic                  deq_ready,
  output logic [2:0]            deq_type,
  output logic [63:0]           deq_addr,
  output logic [11:0]           deq_len,
  output logic [15:0]           deq_rid,
  output logic [rc_pkg::gw(DEPTH+1)-1:0] level
);
 
  import rc_pkg::*;
 
  typedef struct packed {
    logic [2:0]  rtype;
    logic [63:0] addr;
    logic [11:0] len;
    logic [15:0] rid;
  } req_t;
 
  req_t mem [DEPTH];
  logic [gw(DEPTH)-1:0] wr, rd;
 
  assign enq_ready = (level != gw(DEPTH+1)'(DEPTH));
  assign deq_valid = (level != '0);
  // The output is driven from STORED state, never from the input port.
  // Re-deriving it from live fabric signals is mutation 9, and its symptom
  // is a request whose address changes while it waits for a busy Root Port.
  assign deq_type  = mem[rd].rtype;
  assign deq_addr  = mem[rd].addr;
  assign deq_len   = mem[rd].len;
  assign deq_rid   = mem[rd].rid;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wr <= '0; rd <= '0; level <= '0;
    end else begin
      // Transfer is valid && ready. Counting `valid` cycles as transfers is
      // the forbidden reading of the transfer contract, and mutation 10.
      if (enq_valid && enq_ready) begin
        mem[wr] <= '{rtype: enq_type, addr: enq_addr, len: enq_len, rid: enq_rid};
        wr      <= (wr == gw(DEPTH)'(DEPTH-1)) ? '0 : wr + 1'b1;
      end
      if (deq_valid && deq_ready)
        rd <= (rd == gw(DEPTH)'(DEPTH-1)) ? '0 : rd + 1'b1;
 
      case ({enq_valid && enq_ready, deq_valid && deq_ready})
        2'b10: level <= level + 1'b1;
        2'b01: level <= level - 1'b1;
        default: ;                       // both or neither: level unchanged
      endcase
    end
  end
 
endmodule

module xlate_req_if #(
  parameter int unsigned NCTX = 16
)(
  input  logic clk,
  input  logic rst_n,
  // request side
  input  logic                        req_valid,
  output logic                        req_ready,
  input  logic [15:0]                 req_devid,      // requester identity
  input  logic [63:0]                 req_iova,
  input  logic                        req_is_write,
  input  logic [11:0]                 req_len,
  input  logic [rc_pkg::gw(NCTX)-1:0] req_ctx,
  // response side
  output logic                        rsp_valid,
  input  logic                        rsp_ready,
  output logic [rc_pkg::gw(NCTX)-1:0] rsp_ctx,
  output logic [63:0]                 rsp_paddr,
  output logic                        rsp_permit,
  output logic                        rsp_fault
);
 
  // This module deliberately implements NO page walk. It exists to make four
  // properties explicit and assertable: translation has latency, it applies
  // backpressure, it can fault, and its response carries a context (§5).
  //
  // A faulting translation must NOT produce a memory transaction. §14
  // measured a design that forwarded anyway: 2,103 accesses proceeded on a
  // translation that had been denied.
  assign req_ready = 1'b1;   // placeholder for the agent's own flow control
 
endmodule

module xlate_ctx_table #(
  parameter int unsigned NCTX = 16,
  parameter int unsigned CANCEL_LIMIT = 32'd4096   // IMPLEMENTATION POLICY
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                          alloc_req,
  output logic                          alloc_gnt,
  output logic [rc_pkg::gw(NCTX)-1:0]   alloc_ctx,
  output logic [15:0]                   alloc_gen,     // generation, §14
  input  logic [63:0]                   alloc_iova,
  input  logic                          rsp_valid,
  input  logic [rc_pkg::gw(NCTX)-1:0]   rsp_ctx,
  input  logic [15:0]                   rsp_gen,
  input  logic                          rsp_fault,
  output logic                          rsp_accept,
  output logic                          rsp_stale,
  output logic [31:0]                   stale_count,
  output logic [rc_pkg::gw(NCTX+1)-1:0] free_count
);
 
  import rc_pkg::*;
 
  logic [NCTX-1:0]  busy;
  logic [15:0]      gen  [NCTX];
  logic [31:0]      age  [NCTX];
 
  always_comb begin
    alloc_gnt = alloc_req && (busy != '1);
    alloc_ctx = '0;
    for (int i = NCTX-1; i >= 0; i--) if (!busy[i]) alloc_ctx = gw(NCTX)'(i);
    alloc_gen = gen[alloc_ctx];
 
    free_count = '0;
    for (int i = 0; i < NCTX; i++) free_count += gw(NCTX+1)'(!busy[i]);
 
    // A response is accepted only if the context is busy AND the generation
    // matches. Pairing a response with whatever occupies the slot NOW is
    // mutation 15, and §14 measured it misrouting 11,857 responses.
    rsp_stale  = rsp_valid && (!busy[rsp_ctx] || (gen[rsp_ctx] != rsp_gen));
    rsp_accept = rsp_valid && !rsp_stale;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      busy <= '0; stale_count <= '0;
      for (int i = 0; i < NCTX; i++) begin gen[i] <= '0; age[i] <= '0; end
    end else begin
      if (alloc_req && alloc_gnt) begin
        busy[alloc_ctx] <= 1'b1;
        age [alloc_ctx] <= '0;
      end
      for (int i = 0; i < NCTX; i++) if (busy[i]) age[i] <= age[i] + 32'd1;
 
      if (rsp_accept) begin
        busy[rsp_ctx] <= 1'b0;
        // The generation advances at RELEASE, so a late response for this
        // context can never match the next occupant (25.7 §7's law).
        gen [rsp_ctx] <= gen[rsp_ctx] + 16'd1;
      end
      if (rsp_stale && stale_count != 32'hFFFF_FFFF)
        stale_count <= stale_count + 32'd1;
 
      // Cancellation: a context that has waited too long is reclaimed, and
      // its generation advances for the same reason.
      for (int i = 0; i < NCTX; i++)
        if (busy[i] && age[i] >= CANCEL_LIMIT) begin
          busy[i] <= 1'b0; gen[i] <= gen[i] + 16'd1;
        end
    end
  end
 
endmodule

module dma_return_router (
  input  logic                  in_valid,
  output logic                  in_ready,
  input  logic [2:0]            in_type,
  input  logic [63:0]           in_addr,       // already translated, if applicable
  input  logic                  in_translated,
  input  rc_pkg::addr_class_e   in_acl,
  input  logic                  in_xlate_fault,
  output logic                  to_mem_valid,
  input  logic                  to_mem_ready,
  output logic                  to_ctrl_valid,
  input  logic                  to_ctrl_ready,
  output logic                  to_msg_valid,
  input  logic                  to_msg_ready,
  output logic                  dropped_fault
);
 
  import rc_pkg::*;
 
  localparam logic [2:0] T_MSG = 3'd4;
 
  always_comb begin
    // A faulting translation is dropped and REPORTED. Forwarding it anyway
    // is mutation 17 — the permission decision is made and then ignored.
    dropped_fault = in_valid && in_xlate_fault;
 
    to_mem_valid  = in_valid && !in_xlate_fault && (in_acl == ACL_DRAM) && (in_type != T_MSG);
    to_ctrl_valid = in_valid && !in_xlate_fault && (in_acl == ACL_CFG ) && (in_type != T_MSG);
    to_msg_valid  = in_valid && !in_xlate_fault && (in_type == T_MSG);
 
    // Exactly one destination, or none. Never two (P7).
    in_ready = (to_mem_valid  && to_mem_ready ) ||
               (to_ctrl_valid && to_ctrl_ready) ||
               (to_msg_valid  && to_msg_ready ) ||
               dropped_fault;
  end
 
endmodule

module rc_perf_counters (
  input  logic clk,
  input  logic rst_n,
  input  logic mmio_rd, mmio_wr,
  input  logic dma_in_beat,
  input  logic [15:0] dma_in_bytes,
  input  logic xlate_stall,        // request held because translation is busy
  input  logic fabric_stall,       // request held because the fabric is busy
  input  logic credit_stall,       // request held for lack of PCIe credit
  input  logic cpl_wait,           // an MMIO read is outstanding
  input  logic clear,
  output logic [31:0] c_mmio_rd, c_mmio_wr,
  output logic [63:0] c_dma_bytes,
  output logic [31:0] c_xlate_stall, c_fabric_stall, c_credit_stall, c_cpl_wait
);
 
  // Diagnostic ONLY: nothing here feeds a functional path. A counter that
  // gates behaviour stops being an instrument and becomes a design
  // dependency, which is mutation 27 (and P24 asserts it does not happen).
  //
  // The three stall counters are separate on purpose. 22.1's point is that
  // "PCIe is slow" is never a diagnosis: the stall has to be attributed to
  // translation, fabric or credit before any change is worth making.
  `define SATCNT(c, en) if (en && (c != '1)) c <= c + 1'b1
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_mmio_rd <= '0; c_mmio_wr <= '0; c_dma_bytes <= '0;
      c_xlate_stall <= '0; c_fabric_stall <= '0; c_credit_stall <= '0; c_cpl_wait <= '0;
    end else begin
      `SATCNT(c_mmio_rd, mmio_rd);
      `SATCNT(c_mmio_wr, mmio_wr);
      `SATCNT(c_xlate_stall, xlate_stall);
      `SATCNT(c_fabric_stall, fabric_stall);
      `SATCNT(c_credit_stall, credit_stall);
      `SATCNT(c_cpl_wait, cpl_wait);
      if (dma_in_beat && (c_dma_bytes != '1)) c_dma_bytes <= c_dma_bytes + 64'(dma_in_bytes);
    end
  end
  `undef SATCNT
 
endmodule

module rc_first_fault (
  input  logic clk,
  input  logic rst_n,
  input  logic        req_valid,
  input  logic [63:0] req_addr,
  input  logic        f_classify, f_port, f_xlate, f_ctx, f_fabric,
  input  logic        clear,
  output rc_pkg::rc_fault_e first_fault,
  output logic [63:0] first_addr,
  output logic        captured,
  output logic [31:0] fault_count
);
 
  import rc_pkg::*;
  rc_fault_e this_f;
 
  // Priority is the ORDER OF THE PIPELINE, so the recorded fault is the most
  // upstream one. A later failure is very often a consequence of an earlier
  // one, and reporting the wrong end of the chain sends the investigation
  // to the wrong block entirely (25.5 §15 case 7).
  always_comb begin
    if      (f_classify) this_f = RCF_CLASSIFY;
    else if (f_port    ) this_f = RCF_PORT;
    else if (f_ctx     ) this_f = RCF_CTX;
    else if (f_xlate   ) this_f = RCF_XLATE;
    else if (f_fabric  ) this_f = RCF_FABRIC;
    else                 this_f = RCF_NONE;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      captured <= 1'b0; first_fault <= RCF_NONE; first_addr <= '0; fault_count <= '0;
    end else if (req_valid && (this_f != RCF_NONE)) begin
      if (!captured) begin
        captured <= 1'b1; first_fault <= this_f; first_addr <= req_addr;
      end
      if (fault_count != 32'hFFFF_FFFF) fault_count <= fault_count + 32'd1;
    end
  end
 
endmodule

// P1 — the classification is total: some class is always produced.
property p1_class_total;
  @(posedge clk) disable iff (!rst_n)
    req_valid |-> (acl inside {ACL_DRAM, ACL_MMIO, ACL_CFG, ACL_ERROR});
endproperty
a_p1: assert property (p1_class_total);
 
// P2 — an address in no window classifies as ERROR, never as MMIO.
// §13 measured the alternative at 50,346 spurious PCIe transactions.
property p2_unclaimed_is_error;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && !hit_dram && !hit_cfg && (hit_mmio == '0)) |-> (acl == ACL_ERROR);
endproperty
a_p2: assert property (p2_unclaimed_is_error);
 
// P3 — at most one window claims an address; more is reported.
property p3_no_silent_ambiguity;
  @(posedge clk) disable iff (!rst_n)
    ambiguous |-> (acl == ACL_ERROR);
endproperty
a_p3: assert property (p3_no_silent_ambiguity);
 
// P4 — window membership is decided at full width.
property p4_full_width_compare;
  @(posedge clk) disable iff (!rst_n)
    (acl == ACL_MMIO) |-> ((req_addr >= mmio_win[mmio_idx].base) &&
                           (req_addr <= mmio_win[mmio_idx].limit));
endproperty
a_p4: assert property (p4_full_width_compare);
 
// P5 — the last byte of a window is inside it, and the next byte is not.
// 25.5 §6's pair, restated at platform scale.
property p5_window_edges;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && (req_addr == dram_win.limit)) |-> (acl == ACL_DRAM);
endproperty
a_p5: assert property (p5_window_edges);
 
property p6_window_edge_exclusive;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && (req_addr == dram_win.limit + 64'd1) && !hit_cfg && (hit_mmio == '0))
      |-> (acl == ACL_ERROR);
endproperty
a_p6: assert property (p6_window_edge_exclusive);

// P7 — routing is attempted only for MMIO-classified addresses.
property p7_route_needs_mmio;
  @(posedge clk) disable iff (!rst_n)
    route_valid |-> (acl == ACL_MMIO);
endproperty
a_p7: assert property (p7_route_needs_mmio);
 
// P8 — exactly one port, or an explicit no-port/multi-port report.
property p8_route_onehot;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && (acl == ACL_MMIO)) |-> $onehot({route_valid, no_port, multi_port});
endproperty
a_p8: assert property (p8_route_onehot);
 
// P9 — an unrouted MMIO address is reported, never silently dropped.
property p9_no_port_reported;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && (acl == ACL_MMIO) && (port_hit_count == 0)) |-> no_port;
endproperty
a_p9: assert property (p9_no_port_reported);

// P10 — a captured request is immutable while it waits.
property p10_request_stable;
  @(posedge clk) disable iff (!rst_n)
    (deq_valid && !deq_ready) |=> (deq_valid && $stable(deq_addr) &&
                                   $stable(deq_len) && $stable(deq_rid));
endproperty
a_p10: assert property (p10_request_stable);
 
// P11 — valid does not depend on ready.
property p11_valid_independent;
  @(posedge clk) disable iff (!rst_n)
    (deq_valid && !deq_ready) |=> deq_valid;
endproperty
a_p11: assert property (p11_valid_independent);
 
// P12 — level tracks transfers, not valid cycles.
property p12_level_accounting;
  @(posedge clk) disable iff (!rst_n)
    (enq_valid && enq_ready && !(deq_valid && deq_ready)) |=> (level == $past(level) + 1);
endproperty
a_p12: assert property (p12_level_accounting);
 
// P13 — the queue never overflows or underflows.
property p13_level_bounded;
  @(posedge clk) disable iff (!rst_n)
    (level <= DEPTH);
endproperty
a_p13: assert property (p13_level_bounded);
 
// P14 — no enqueue when full, no dequeue when empty.
property p14_no_overrun;
  @(posedge clk) disable iff (!rst_n)
    ((enq_valid && enq_ready) |-> (level < DEPTH)) and
    ((deq_valid && deq_ready) |-> (level > 0));
endproperty
a_p14: assert property (p14_no_overrun);

// P15 — a context is allocated only when free.
property p15_alloc_when_free;
  @(posedge clk) disable iff (!rst_n)
    (alloc_req && alloc_gnt) |-> !busy[alloc_ctx];
endproperty
a_p15: assert property (p15_alloc_when_free);
 
// P16 — a context is never allocated twice concurrently.
property p16_ctx_unique;
  @(posedge clk) disable iff (!rst_n)
    (alloc_req && alloc_gnt) |=> busy[$past(alloc_ctx)];
endproperty
a_p16: assert property (p16_ctx_unique);
 
// P17 — a response is accepted only for a busy context with a matching
// generation. §14 measured pairing-with-current at 11,857 misroutes.
property p17_response_identity;
  @(posedge clk) disable iff (!rst_n)
    rsp_accept |-> (busy[rsp_ctx] && (gen[rsp_ctx] == rsp_gen));
endproperty
a_p17: assert property (p17_response_identity);
 
// P18 — a stale response is discarded AND counted.
property p18_stale_counted;
  @(posedge clk) disable iff (!rst_n)
    rsp_stale |=> (stale_count > $past(stale_count));
endproperty
a_p18: assert property (p18_stale_counted);
 
// P19 — the generation advances whenever a context is released, so a late
// response can never match the next occupant.
property p19_gen_advances_on_release;
  @(posedge clk) disable iff (!rst_n)
    rsp_accept |=> (gen[$past(rsp_ctx)] != $past(gen[$past(rsp_ctx)]));
endproperty
a_p19: assert property (p19_gen_advances_on_release);
 
// P20 — no double free.
property p20_no_double_free;
  @(posedge clk) disable iff (!rst_n)
    (rsp_accept && !busy[rsp_ctx]) |-> 1'b0;
endproperty
a_p20: assert property (p20_no_double_free);
 
// P21 — reset invalidates every context.
property p21_reset_clears_ctx;
  @(posedge clk)
    !rst_n |=> (busy == '0);
endproperty
a_p21: assert property (p21_reset_clears_ctx);
 
// P22 — the free count agrees with the busy vector.
property p22_free_count_consistent;
  @(posedge clk) disable iff (!rst_n)
    (free_count == NCTX - $countones(busy));
endproperty
a_p22: assert property (p22_free_count_consistent);

// P23 — a faulting translation never produces a memory transaction.
// §14 measured a design that forwarded anyway: 2,103 accesses.
property p23_fault_blocks_memory;
  @(posedge clk) disable iff (!rst_n)
    in_xlate_fault |-> (!to_mem_valid && !to_ctrl_valid);
endproperty
a_p23: assert property (p23_fault_blocks_memory);
 
// P24 — exactly one destination, or none.
property p24_router_onehot0;
  @(posedge clk) disable iff (!rst_n)
    $onehot0({to_mem_valid, to_ctrl_valid, to_msg_valid});
endproperty
a_p24: assert property (p24_router_onehot0);
 
// P25 — diagnostic counters are non-functional: nothing depends on them.
property p25_counters_nonfunctional;
  @(posedge clk) disable iff (!rst_n)
    $stable(c_dma_bytes) or (route_valid == $past(route_valid_expected));
endproperty
a_p25: assert property (p25_counters_nonfunctional);

// P26 — a request produces exactly one outcome: it is classified, routed
// and forwarded, or it is recorded as a fault. A request that produces
// neither has vanished inside the host boundary, and no downstream
// instrument can tell that it did.
property p26_every_request_resolved;
  @(posedge clk) disable iff (!rst_n)
    req_valid |-> (route_valid || win_reject || (acl == ACL_ERROR) ||
                   (acl inside {ACL_DRAM, ACL_CFG}));
endproperty
a_p26: assert property (p26_every_request_resolved);
 
// P26's covers — the exceptional states must actually occur, or P2, P3, P9, P17 and
// P23 are all satisfied without ever evaluating a consequent.
c1_error_class:  cover property (@(posedge clk) disable iff (!rst_n) acl == ACL_ERROR);
c2_ambiguous:    cover property (@(posedge clk) disable iff (!rst_n) ambiguous);
c3_no_port:      cover property (@(posedge clk) disable iff (!rst_n) no_port);
c4_stale_rsp:    cover property (@(posedge clk) disable iff (!rst_n) rsp_stale);
c5_xlate_fault:  cover property (@(posedge clk) disable iff (!rst_n) in_xlate_fault);
c6_ctx_exhaust:  cover property (@(posedge clk) disable iff (!rst_n) free_count == 0);
c7_queue_full:   cover property (@(posedge clk) disable iff (!rst_n) !enq_ready);
c8_window_edge:  cover property (@(posedge clk) disable iff (!rst_n)
                   req_valid && (req_addr == dram_win.limit));

// The classifier tests the ranges it knows and sends everything else to PCIe.
module ce_a_fallthrough_classify (
  input  logic [63:0] a,
  input  rc_pkg::window_t dram, cfg,
  output rc_pkg::addr_class_e acl
);
  import rc_pkg::*;
  always_comb begin
    if      (in_window(dram, a)) acl = ACL_DRAM;
    else if (in_window(cfg , a)) acl = ACL_CFG;
    else                         acl = ACL_MMIO;   // <-- the default
  end
endmodule
 
// Failing stimulus: an address above every configured window.
// Golden: ACL_ERROR — the platform does not own it.
// This:   ACL_MMIO. A real TLP is generated toward a Root Port for an address
//         no window claims.
// P2 fails.
// §13 measured 50,346 such addresses in 200,000 probes. The observable
// consequence is an Unsupported Request the software never asked for, and a
// fault reported against the DEVICE for an error made by the host.

// The MMIO window comparison uses only the low 32 bits of the address.
module ce_b_low32_classify (
  input  logic [63:0] a,
  input  rc_pkg::window_t dram,
  output rc_pkg::addr_class_e acl
);
  import rc_pkg::*;
  always_comb
    acl = (a[31:0] <= dram.limit[31:0]) ? ACL_DRAM : ACL_ERROR;   // <-- truncated
endmodule
 
// Failing stimulus: an MMIO address whose low 32 bits fall inside the DRAM
// window — e.g. DRAM [0, 0xFFFF_FFFF] and MMIO at 0x1_0000_0000.
// Golden: ACL_MMIO, routed to a Root Port.
// This:   ACL_DRAM. The access is answered by the memory controller.
// P4 fails.
// §13 measured 39,648 MMIO accesses misrouted into DRAM. The device is never
// reached, the read SUCCEEDS, and it returns whatever DRAM held. No error is
// raised at any layer — 25.5 §4's Direction B, at platform scale.