BAR Logic — Which Aperture Owns This Address?

1. does any aperture of mine contain this address?   (§3, §5)
2. if so, which one -- and only one                  (§5, §6)
3. what local address does it become                 (§8)

offset = addr & (size - 1)                [bytes, within the aperture]

// COMPILE-TIME. Aperture descriptions and the static 64-bit pairing.
// Whether a slot is the low half of a 64-bit BAR, the high half, or an
// independent 32-bit BAR is a property of the DESIGN, not a runtime
// decision that can disagree with itself (§6).
package bar_pkg;
 
  parameter int ADDR_W  = 64;
  parameter int N_SLOT  = 6;                       // physical BAR slots
  parameter int SEL_W   = (N_SLOT <= 1) ? 1 : $clog2(N_SLOT);
 
  typedef enum logic [1:0] {
    SLOT_UNIMPL = 2'd0,
    SLOT_MEM32  = 2'd1,
    SLOT_MEM64_LO = 2'd2,     // this slot plus the next form ONE aperture
    SLOT_MEM64_HI = 2'd3      // never a decode candidate on its own
  } slot_kind_e;
 
  // Design-time slot map. Slot 1 is the high half of slot 0's aperture.
  parameter slot_kind_e SLOT_KIND [N_SLOT] = '{
    SLOT_MEM64_LO, SLOT_MEM64_HI, SLOT_MEM32, SLOT_MEM32,
    SLOT_UNIMPL,   SLOT_UNIMPL };
 
  // Aperture size per slot, in bytes. Powers of two (Chapter 9.4 §5).
  parameter longint unsigned SLOT_SIZE [N_SLOT] = '{
    64'h0000_0100_0000, 64'd0, 64'h0000_0001_0000, 64'h0000_0010_0000,
    64'd0, 64'd0 };
 
  function automatic logic [ADDR_W-1:0] size_mask(input longint unsigned sz);
    // ~(size-1). Guarded so a zero size yields an ALL-ONES mask, which
    // matches nothing useful, rather than an all-zero mask that matches
    // EVERYTHING -- the difference between an unimplemented BAR that is
    // inert and one that swallows the address space.
    if (sz == 0) return {ADDR_W{1'b1}};
    return ~(ADDR_W'(sz) - ADDR_W'(1));
  endfunction
 
  function automatic bit is_decode_candidate(input slot_kind_e k);
    return (k == SLOT_MEM32) || (k == SLOT_MEM64_LO);
  endfunction
 
  // The aperture a candidate slot represents, after pairing.
  function automatic bit is_64bit(input slot_kind_e k);
    return (k == SLOT_MEM64_LO);
  endfunction
 
endpackage

import bar_pkg::*;
 
// SYNTHESIZABLE. One aperture's match. MASK COMPARE, not range compare:
// exact for an aligned power-of-two aperture (§14 Model 8: 0 disagreements
// over 300,000 probes) and free of the adder and carry chain a range
// compare needs on an inbound-critical path (§3).
module aperture_match (
  input  logic [ADDR_W-1:0] addr,
  input  logic [ADDR_W-1:0] base,          // already the FULL 64-bit base (§6)
  input  logic [ADDR_W-1:0] mask,          // ~(size-1)
  input  logic              implemented,
  input  logic              space_enabled,
 
  output logic              match,         // a fact about numbers
  output logic              claim,         // a decision about behaviour (§7)
  output logic              err_misaligned // base not naturally aligned (§4)
);
  // Alignment is a PRECONDITION of the mask form. With a misaligned base
  // the mask and range forms disagree in 33.3% of probes (§14 Model 8),
  // so a misprogrammed base is reported rather than silently obeyed.
  assign err_misaligned = implemented && ((base & ~mask) != '0);
 
  assign match = implemented
              && !err_misaligned
              && ((addr & mask) == (base & mask));
 
  // MATCH IS NOT CLAIM. §14 Model 9: 49.9% of in-aperture probes arrived
  // while the space was disabled; an ungated decoder claims all of them.
  assign claim = match && space_enabled;
endmodule

import bar_pkg::*;
 
// SYNTHESIZABLE. Assembles the FULL 64-bit base from a slot pair (§6).
// A decoder that compares only the lower 32 bits claimed an address 4 GiB
// away in 50.1% of aliased probes -- and an aliased claim is worse than
// silence, because the requester receives wrong data instead of a UR.
module bar_base_assemble #(parameter int SLOT = 0) (
  input  logic [31:0] bar_reg [N_SLOT],
  output logic [ADDR_W-1:0] base,
  output logic              valid_candidate
);
  localparam slot_kind_e KIND = SLOT_KIND[SLOT];
 
  always_comb begin
    valid_candidate = is_decode_candidate(KIND);
    if (!valid_candidate)             base = '0;
    else if (is_64bit(KIND))          base = {bar_reg[SLOT+1], bar_reg[SLOT]};
    else                              base = {32'd0, bar_reg[SLOT]};
  end
endmodule

import bar_pkg::*;
 
// SYNTHESIZABLE. THE FLAGSHIP BLOCK. All apertures, one address, three
// outcomes (§5). §14 Model 5: 0 disagreements against an independent
// range-scan oracle over 400,000 probes, with every overlap flagged.
module bar_decoder (
  input  logic [ADDR_W-1:0] addr,
  input  logic              req_valid,
  input  logic [ADDR_W-1:0] base [N_SLOT],
  input  logic              space_enabled,
 
  output logic [N_SLOT-1:0] match_vec,
  output logic              hit,           // exactly one
  output logic              no_match,      // none of mine (§9)
  output logic              ambiguous,     // two or more -- a CONFIG FAULT
  output logic              disabled_hit,  // matched, but not permitted (§7)
  output logic [SEL_W-1:0]  sel,
  output logic [N_SLOT-1:0] err_misaligned_vec
);
  logic [N_SLOT-1:0] claim_vec;
 
  genvar g;
  generate
    for (g = 0; g < N_SLOT; g++) begin : g_ap
      aperture_match u_m (
        .addr(addr),
        .base(base[g]),
        .mask(size_mask(SLOT_SIZE[g])),
        .implemented(is_decode_candidate(SLOT_KIND[g])),
        .space_enabled(space_enabled),
        .match(match_vec[g]),
        .claim(claim_vec[g]),
        .err_misaligned(err_misaligned_vec[g])
      );
    end
  endgenerate
 
  // ==================================================================
  // THREE OUTCOMES, and the third is REPORTED. A priority encoder here
  // resolves every overlap to the same slot and makes the other aperture
  // permanently unreachable with no error (§5, §14 Model 6: 24.9%).
  // ==================================================================
  assign hit          = req_valid && $onehot(claim_vec);
  assign ambiguous    = req_valid && !$onehot0(match_vec);
  assign disabled_hit = req_valid && !space_enabled && (match_vec != '0);
  assign no_match     = req_valid && (match_vec == '0);
 
  always_comb begin
    sel = '0;
    if (hit)
      for (int i = 0; i < N_SLOT; i++)
        if (claim_vec[i]) sel = SEL_W'(i);
  end
endmodule

import bar_pkg::*;
 
// SYNTHESIZABLE. Target and offset, emitted ATOMICALLY (§8).
// Two halves of one decision. Pipelining them separately can pair one
// packet's target with another's offset -- Chapter 23.1 §3's corruption,
// through a different door.
module bar_translate (
  input  logic clk,
  input  logic rst_n,
  input  logic              hit,
  input  logic [SEL_W-1:0]  sel,
  input  logic [ADDR_W-1:0] addr,
  input  logic              out_ready,
 
  output logic              out_valid,
  output logic [SEL_W-1:0]  out_target,
  output logic [ADDR_W-1:0] out_offset
);
  logic [ADDR_W-1:0] off_c;
 
  // offset = addr & (size-1). Exact, and needs no subtractor: §14 Model 10
  // found 0 disagreements with (addr - base) over 400,000 probes, because
  // the base is aligned (§4).
  always_comb begin
    off_c = '0;
    for (int i = 0; i < N_SLOT; i++)
      if (SEL_W'(i) == sel) off_c = addr & ~size_mask(SLOT_SIZE[i]);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin out_valid <= 1'b0; out_target <= '0; out_offset <= '0; end
    else if (!out_valid || out_ready) begin
      out_valid  <= hit;
      // ONE cycle, BOTH fields -- never a target from one packet and an
      // offset from another.
      out_target <= sel;
      out_offset <= off_c;
    end
    // Under stall (out_valid && !out_ready) nothing changes: the payload
    // is stable, per Chapter 23.1 §3's contract and P14 below.
  end
endmodule

import bar_pkg::*;
 
// SYNTHESIZABLE. Aperture snapshot (§13's audit).
// Software may write a BAR at any time, including while a request is in
// the decode pipeline. The decoder samples the whole table ONCE, at the
// request-accept boundary -- the rule Chapter 19.4 §12 established and
// Chapter 21.1 §13 reused for routing decisions.
module bar_table_snapshot (
  input  logic clk,
  input  logic rst_n,
  input  logic              take,                  // request accepted
  input  logic [ADDR_W-1:0] base_live [N_SLOT],
  input  logic              enable_live,
 
  output logic [ADDR_W-1:0] base_eff [N_SLOT],
  output logic              enable_eff,
  output logic              cfg_changed_in_flight  // sticky, diagnostic
);
  logic [ADDR_W-1:0] b_q [N_SLOT];
  logic              e_q, chg_q;
 
  always_comb begin
    for (int i = 0; i < N_SLOT; i++) base_eff[i] = b_q[i];
    enable_eff = e_q;
  end
  assign cfg_changed_in_flight = chg_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < N_SLOT; i++) b_q[i] <= '0;
      e_q <= 1'b0; chg_q <= 1'b0;
    end else begin
      if (take) begin
        for (int i = 0; i < N_SLOT; i++) b_q[i] <= base_live[i];
        e_q <= enable_live;
      end else begin
        // A change while a decode is in flight is REPORTED, not applied.
        for (int i = 0; i < N_SLOT; i++)
          if (base_live[i] != b_q[i]) chg_q <= 1'b1;
        if (enable_live != e_q) chg_q <= 1'b1;
      end
    end
  end
endmodule

import bar_pkg::*;
 
// VERIFICATION-ONLY. Independent oracle: an explicit RANGE scan, written
// deliberately in the form the RTL does NOT use, so a shared misconception
// cannot make both agree (§15's DV rule).
module bar_decoder_oracle (
  input  logic [ADDR_W-1:0] addr,
  input  logic [ADDR_W-1:0] base [N_SLOT],
  input  logic              space_enabled,
  input  logic [N_SLOT-1:0] rtl_match_vec,
  output logic              err_mismatch,
  output logic [N_SLOT-1:0] ref_match_vec
);
  always_comb begin
    for (int i = 0; i < N_SLOT; i++) begin
      automatic logic [ADDR_W-1:0] lo = base[i];
      automatic logic [ADDR_W-1:0] hi = base[i] + ADDR_W'(SLOT_SIZE[i]);
      ref_match_vec[i] = is_decode_candidate(SLOT_KIND[i])
                      && (SLOT_SIZE[i] != 0)
                      && (addr >= lo) && (addr < hi);
    end
    err_mismatch = (ref_match_vec !== rtl_match_vec);
  end
endmodule

// ==================================================================
// MATCHING (§3, §4) -- the mask form and its precondition.
// ==================================================================
 
// P1: a match means the masked address equals the masked base. This is
// the definition, asserted so a "clever" rewrite cannot drift from it.
property p_match_is_mask_compare;
  @(posedge clk) disable iff (!rst_n)
    match_vec[0] |-> ((addr & size_mask(SLOT_SIZE[0]))
                        == (base[0] & size_mask(SLOT_SIZE[0])));
endproperty
 
// P2: the mask form agrees with an explicit range scan. §14 Model 5:
// 0 disagreements over 400,000 probes.
property p_agrees_with_range_oracle;
  @(posedge clk) disable iff (!rst_n)
    !err_mismatch;
endproperty
 
// P3: an unimplemented slot never matches.
property p_unimplemented_never_matches;
  @(posedge clk) disable iff (!rst_n)
    (SLOT_KIND[4] == SLOT_UNIMPL) |-> !match_vec[4];
endproperty
 
// P4: the HIGH half of a 64-bit pair is never a decode candidate on its
// own -- including it produces phantom matches (§6).
property p_hi_half_never_candidate;
  @(posedge clk) disable iff (!rst_n)
    (SLOT_KIND[1] == SLOT_MEM64_HI) |-> !match_vec[1];
endproperty
 
// P5: a zero-size slot matches nothing. The guarded mask returns all-ones
// so an unimplemented BAR is inert rather than swallowing everything.
property p_zero_size_inert;
  @(posedge clk) disable iff (!rst_n)
    (SLOT_SIZE[5] == 0) |-> !match_vec[5];
endproperty
 
// P6: a misaligned base is REPORTED and does not match. §14 Model 8: the
// mask and range forms disagree in 33.3% of probes when alignment fails.
property p_misaligned_reported_not_obeyed;
  @(posedge clk) disable iff (!rst_n)
    err_misaligned_vec[0] |-> !match_vec[0];
endproperty
 
// ==================================================================
// 64-BIT APERTURES (§6).
// ==================================================================
 
// P7: a 64-bit aperture compares ALL address bits. §14 Model 7: a
// lower-32-only decoder claimed an address 4 GiB away in 50.1% of probes.
property p_64bit_compares_upper_bits;
  @(posedge clk) disable iff (!rst_n)
    (is_64bit(SLOT_KIND[0]) && match_vec[0]) |->
      ((addr[63:32] & size_mask(SLOT_SIZE[0])[63:32])
        == (base[0][63:32] & size_mask(SLOT_SIZE[0])[63:32]));
endproperty
 
// P8: an address differing only in the upper 32 bits does NOT match.
property p_no_4gib_alias;
  @(posedge clk) disable iff (!rst_n)
    (is_64bit(SLOT_KIND[0]) && (addr[31:0] == base[0][31:0])
      && (addr[63:32] != base[0][63:32])) |-> !match_vec[0];
endproperty
 
// ==================================================================
// THREE OUTCOMES (§5, §9).
// ==================================================================
 
// P9: exactly one outcome per accepted request. No silent fourth case.
property p_outcome_total;
  @(posedge clk) disable iff (!rst_n)
    req_valid |-> $onehot({hit, no_match, ambiguous, disabled_hit})
               || (disabled_hit && no_match) === 1'b0;
endproperty
 
// P10: two or more matches are REPORTED, never resolved by priority.
// §14 Model 6: a priority encoder resolves 24.9% of probes silently.
property p_ambiguity_reported;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && !$onehot0(match_vec)) |-> (ambiguous && !hit);
endproperty
 
// P11: ambiguity is computed on MATCH, so a misprogrammed overlap is
// visible even while the space is disabled (§13's audit).
property p_ambiguity_independent_of_enable;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && !$onehot0(match_vec) && !space_enabled) |-> ambiguous;
endproperty
 
// P12: a hit names a slot that actually claimed the address.
property p_hit_names_claiming_slot;
  @(posedge clk) disable iff (!rst_n)
    hit |-> claim_vec[sel];
endproperty
 
// P13: no match means no claim -- the device never answers helpfully (§9).
property p_no_match_no_claim;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && (match_vec == '0)) |-> (no_match && !hit);
endproperty
 
// ==================================================================
// ENABLE (§7) -- availability is not permission.
// ==================================================================
 
// P14: a disabled space never claims. §14 Model 9: 49.9% of in-aperture
// probes arrived disabled; an ungated decoder claims all of them.
property p_disabled_never_claims;
  @(posedge clk) disable iff (!rst_n)
    (!space_enabled) |-> !hit;
endproperty
 
// P15: a match while disabled is reported DISTINCTLY from no match --
// three different non-claims, three different debugging directions (§9).
property p_disabled_hit_distinct;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && !space_enabled && (match_vec != '0)) |-> disabled_hit;
endproperty
 
// ==================================================================
// TRANSLATION (§8) and the STALL CONTRACT (Chapter 23.1 §3).
// ==================================================================
 
// P16: the offset is within the aperture -- it can never address outside
// the resource it was translated into.
property p_offset_within_aperture;
  @(posedge clk) disable iff (!rst_n)
    out_valid |-> (out_offset < ADDR_W'(SLOT_SIZE[out_target]));
endproperty
 
// P17: target and offset are emitted ATOMICALLY, from one decode.
property p_target_offset_atomic;
  @(posedge clk) disable iff (!rst_n)
    ($rose(out_valid)) |-> ((out_target == $past(sel))
                         && (out_offset == $past(off_c)));
endproperty
 
// P18: the result is STABLE under downstream stall.
property p_result_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (out_valid && !out_ready) |=>
      (out_valid && $stable(out_target) && $stable(out_offset));
endproperty
 
// ==================================================================
// SNAPSHOT (§13's audit) and RESET.
// ==================================================================
 
// P19: the effective table changes only at a request-accept boundary --
// a BAR written mid-decode does not change the decision in flight.
property p_table_snapshot_at_boundary;
  @(posedge clk) disable iff (!rst_n)
    (base_eff[0] != $past(base_eff[0])) |-> $past(take);
endproperty
 
// P20: a configuration change while a decode is in flight is REPORTED.
property p_inflight_change_reported;
  @(posedge clk) disable iff (!rst_n)
    (!take && (base_live[0] != base_eff[0])) |=> cfg_changed_in_flight;
endproperty
 
// P21: reset claims nothing and emits nothing.
property p_reset_claims_nothing;
  @(posedge clk)
    (!rst_n) |=> (!hit && !out_valid && (base_eff[0] == '0));
endproperty
 
// P22: the decoder never drives the inbound interface -- it decides, it
// does not backpressure (Chapter 23.1 §4).
property p_decoder_does_not_backpressure;
  @(posedge clk) disable iff (!rst_n)
    $stable(req_valid) or !$stable({hit, no_match, ambiguous});
endproperty