Shared Memory Pools

Module 11 ended with a device shared by a small, fixed set of hosts: ownership was a static table, budgets were assigned once, and nothing moved.

This chapter removes the word static.

1. The Engineering Problem — Capacity That Belongs To Nobody Yet

A memory device attached to one host is simple to reason about, because the answer to who owns this byte never changes. 11.3 kept that simplicity by fixing the assignment at configuration time — a handful of hosts, a table written once, a design where nothing has to be decided at runtime.

A pool discards that. Capacity now exists before anyone owns it, and the interesting question is no longer how a host reaches memory but how memory becomes assignable in the first place.

That single change introduces a set of obligations the fixed design never had:

Capacity has to be counted. Not estimated, not inferred from a configuration file — counted, by hardware, in a way that can be reconciled against every other accounting in the system.

Capacity has to be owned. A byte with no recorded owner is not free capacity; it is capacity nobody can prove anything about. A byte with two recorded owners is corruption that has already happened.

Capacity has to be placed. To a host, a pool is one number. To whoever operates it, it is several physical devices, and the difference matters the moment one of them fails.

And capacity has to be returned. Every allocation eventually ends, and the accounting has to survive the return as exactly as it survived the grant.

None of this is exotic. It is inventory management, and it is unforgiving in the same way inventory management always is: the errors are not dramatic failures but slow, quiet divergences between what the system believes it has and what it actually has.

2. The One-Sentence Model

A pool turns memory capacity into inventory. Inventory is counted, owned, placed, allocated, used and returned — and every one of those verbs is a state transition that hardware has to get right, not a fact recorded somewhere.

Call it counted, owned, returned. A byte that exists physically but cannot be assigned safely is not pool capacity. A byte assigned twice is corruption. A byte returned but not accounted for is a leak.

3. What This Chapter Owns

Module 12 has borders on four sides, and the one that matters most is behind it.

Deferred, deliberately:

11.3 built the mechanisms; this chapter asks what they have to become when the assignment is not known in advance. The distinction is concrete. In 11.3 a host's region was decided before the system ran. Here, nothing is decided until a request arrives, and every structure in this chapter exists to make that decision safe.

Connectivity is assumed, not designed. This chapter draws a box labelled allocation manager and does not open it — how such a controller is discovered, reached or made redundant belongs to Module 15, and the switching that carries the traffic belongs to Module 16.

4. Teaching-model boundary

The public CXL material that is freely available describes pooling in terms of what becomes possible — capacity from a device being made available to more than one host — rather than in terms of the manager's internal mechanics. So this chapter does not invent those mechanics.

Nothing below claims to be a CXL structure. There are no pool-management opcodes, no register offsets, no command encodings, no allocation-unit sizes attributed to the specification, no decoder formats and no state encodings. Where a mechanism is needed to teach an invariant, it is built here, labelled as a teaching model, and verified as one.

What is transferable is the set of obligations. A pool manager built by anybody, for any interconnect, has to conserve capacity, record ownership, distinguish free from allocatable, and reconcile its accountings. Those are the subject.

5. RTL 1 — Capacity Must Be Conserved

Start with the smallest possible pool manager: one that does nothing but count.

Capacity exists in exactly three states. It is free and available to grant, allocated to some host, or unavailable because the hardware holding it has failed. Every unit is in exactly one of them, so the three counters must always sum to the pool total.

module pool_ledger #(parameter int TOTAL = 64, parameter int FAULT_INJECT = 0) (
  input  logic       clk, rst_n,
  input  logic       alloc_en, input logic [7:0] alloc_n,
  input  logic       free_en,  input logic [7:0] free_n,
  input  logic       fail_en,  input logic [7:0] fail_n,   // free -> unavailable
  input  logic       rest_en,  input logic [7:0] rest_n,   // unavailable -> free
  output logic [7:0] free_q, used_q, unav_q,
  output logic       overdraw_err, conserve_err, accepted
);
  // ONE combined next-state decision. Independent conditional assignments to
  // the same counter lose the simultaneous case.
  logic signed [10:0] dF, dU, dV, nF, nU, nV;
  logic any_ev, feasible;
 
  always_comb begin
    dF = 11'sd0; dU = 11'sd0; dV = 11'sd0;
    if (alloc_en) begin dF = dF - $signed({3'b0, alloc_n}); dU = dU + $signed({3'b0, alloc_n}); end
    if (free_en)  begin dF = dF + $signed({3'b0, free_n});  dU = dU - $signed({3'b0, free_n});  end
    if (fail_en)  begin dF = dF - $signed({3'b0, fail_n});
                        if (FAULT_INJECT == 0) dV = dV + $signed({3'b0, fail_n}); end
    if (rest_en)  begin dF = dF + $signed({3'b0, rest_n});  dV = dV - $signed({3'b0, rest_n});  end
    nF = $signed({3'b0, free_q}) + dF;
    nU = $signed({3'b0, used_q}) + dU;
    nV = $signed({3'b0, unav_q}) + dV;
    any_ev   = alloc_en | free_en | fail_en | rest_en;
    feasible = (nF >= 0) && (nU >= 0) && (nV >= 0);
  end
 
  assign accepted = any_ev & feasible;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      free_q <= TOTAL[7:0]; used_q <= 8'd0; unav_q <= 8'd0;
      overdraw_err <= 1'b0; conserve_err <= 1'b0;
    end else begin
      if (any_ev) begin
        if (feasible) begin
          free_q <= nF[7:0]; used_q <= nU[7:0]; unav_q <= nV[7:0];
        end else begin
          overdraw_err <= 1'b1;            // phantom capacity attempt; state unchanged
        end
      end
      if ((free_q + used_q + unav_q) != TOTAL[7:0]) conserve_err <= 1'b1;
    end
  end
endmodule

Two decisions in that module are worth more than the arithmetic.

The deltas are combined before anything is committed. An allocation and a return can land in the same cycle, and a design that writes the counter twice keeps only one of them. This defect has now appeared in twelve separate models across this curriculum, always with the same shape, and the only reliable defence is to compute one next-state value from all the events at once. The measured case: from 58 free and 6 used, allocating 5 while returning 3 gives free=56 used=8 — not 53, and not 61.

Infeasible cycles are rejected whole. If any of the three pools would go negative the entire cycle is refused and overdraw_err is raised. Granting part of a request is worse than refusing it, because the requester believes it received capacity that the pool never had.

The boundary between those two behaviours is exact and is tested from both sides. Taking every remaining free unit is legal — the run reaches free=0 used=64 with overdraw=0. Asking for one unit beyond that is not — the state is unchanged at free=0 used=64 and overdraw=1.

6. RTL 2 — One Bit Per Unit, And Two Ways To Get It Wrong

The ledger counts capacity but cannot say which capacity. That is the bitmap's job: one bit per allocation unit, set when the unit is handed out and cleared when it comes back.

module alloc_bitmap #(parameter int UNITS = 16) (
  input  logic clk, rst_n,
  input  logic set_en, input logic [3:0] set_idx,
  input  logic clr_en, input logic [3:0] clr_idx,
  output logic [UNITS-1:0] map_q,
  output logic [4:0] used_cnt,
  output logic double_alloc_err, unknown_free_err, set_clr_race_err
);
  logic same_unit;
  assign same_unit = set_en & clr_en & (set_idx == clr_idx);
 
  logic [UNITS-1:0] nxt;
  always_comb begin
    nxt = map_q;
    if (set_en) nxt[set_idx] = 1'b1;
    if (clr_en) nxt[clr_idx] = 1'b0;   // same-unit set+clear: the return wins
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      map_q <= {UNITS{1'b0}}; double_alloc_err <= 1'b0;
      unknown_free_err <= 1'b0; set_clr_race_err <= 1'b0;
    end else begin
      map_q <= nxt;
      if (set_en &&  map_q[set_idx] && !same_unit) double_alloc_err <= 1'b1;
      if (clr_en && !map_q[clr_idx] && !same_unit) unknown_free_err <= 1'b1;
      if (same_unit)                               set_clr_race_err <= 1'b1;
    end
  end
endmodule

The same_unit term is there because of something the baseline run found, and it is not a detail.

The first version of this model raised double_alloc_err whenever a set landed on an already-set bit. That looks correct, and it is wrong for one specific case: a grant and a release colliding on the same unit in the same cycle. The unit ends up free, so the grant did not take effect — but the alarm says two owners, and an engineer reading it goes looking for a second owner that does not exist.

Those are different failures with different fixes, so they get different counters. The measured run confirms the separation: a same-unit set and clear leaves used=3 with race_err=1 and dbl_err=0, while a set on a unit genuinely owned by somebody else raises dbl_err=1.

Two counters, two operational meanings. A double allocation means the allocator handed out capacity it had already handed out. A set/clear race means the allocator and the reclaim path disagreed about ordering. Merging them saves a flip-flop and costs a debug session.

The third alarm, unknown_free_err, fires when a return arrives for a unit that was not allocated — measured at 1 in the run. It matters more than it looks: an unknown return is the signature of a stale event, and Module 12.3 is largely about where those come from.

7. RTL 3 — Inventory Without An Owner Is Not Allocated

A set bit says a unit is taken. It does not say by whom, and without that the pool cannot answer any of the questions that actually get asked in production: how much does host 2 hold, is this return legitimate, who is affected if this device dies.

module owner_table #(parameter int UNITS = 16) (
  input  logic clk, rst_n,
  input  logic asg_en, input logic [3:0] asg_unit, input logic [1:0] asg_host,
  input  logic rel_en, input logic [3:0] rel_unit, input logic [1:0] rel_host,
  input  logic [3:0] q_unit,
  output logic q_valid, output logic [1:0] q_owner,
  output logic [4:0] h_cnt0, h_cnt1, h_cnt2, h_cnt3,
  output logic asg_grant, rel_grant,
  output logic double_owner_err, wrong_owner_err, unknown_rel_err
);
  logic       valid_q [0:UNITS-1];
  logic [1:0] owner_q [0:UNITS-1];
 
  logic asg_ok, rel_ok;
  assign asg_ok = asg_en && !valid_q[asg_unit];
  assign rel_ok = rel_en &&  valid_q[rel_unit] && (owner_q[rel_unit] == rel_host);
  assign asg_grant = asg_ok;
  assign rel_grant = rel_ok;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (i = 0; i < UNITS; i = i + 1) begin valid_q[i] <= 1'b0; owner_q[i] <= 2'd0; end
      double_owner_err <= 1'b0; wrong_owner_err <= 1'b0; unknown_rel_err <= 1'b0;
    end else begin
      if (rel_ok) valid_q[rel_unit] <= 1'b0;
      if (asg_ok) begin valid_q[asg_unit] <= 1'b1; owner_q[asg_unit] <= asg_host; end
      if (asg_en && valid_q[asg_unit])                                double_owner_err <= 1'b1;
      if (rel_en && valid_q[rel_unit] && owner_q[rel_unit]!=rel_host) wrong_owner_err  <= 1'b1;
      if (rel_en && !valid_q[rel_unit])                               unknown_rel_err  <= 1'b1;
    end
  end
endmodule

Three properties, each verified, each with an operational consequence.

Per-host occupancy is derived, never separately incremented. The counts come from scanning the table. A second counter that is incremented alongside the table is a counter that can drift from it, and once they disagree neither can be trusted. The measured baseline reads h0=3, h1=2, h2=1 and those numbers are recomputed from the table on every cycle.

A release must come from the recorded owner. Releasing a unit you do not own raises wrong_owner_err — measured at 1 — and changes nothing. Releasing a unit nobody owns raises unknown_rel_err, also measured at 1. Both leave the table exactly as it was.

And a second host cannot take an owned unit. The attempt raises double_owner_err=1, and the query port confirms the original owner is untouched.

The asg_grant and rel_grant outputs exist because of a second finding, discussed in section 13. They are not decoration: every accounting downstream of this table must be driven by these grants and never by the request that produced them.

8. Waveform — Allocate, Return, And The Cycle That Does Both

The trace below is not drawn. It is the printed output of a run that instantiates the ledger, the bitmap and the ownership table on one 16-unit pool, drives a request sequence through all three, and asserts on every cycle that the three accountings agree.

Two cycles carry the whole chapter.

Cycle 5 allocates unit 12 to host 2 while host 1 returns unit 5. The free count stays at 14 — one unit out, one unit in — and both per-host counts move in opposite directions in the same edge. This is the case a two-assignment counter destroys.

Cycle 6 is host 1 asking for unit 9, which host 2 owns. grant stays low, dbl_err rises, and not one counter moves: free stays at 14, both host counts hold. That is the correct outcome, and section 13 explains why an early version of this integration got it wrong.

9. RTL 4 — One Number To A Host, Several Devices To An Operator

A pool presents itself as a single quantity of capacity. Physically it is several devices, and the two views diverge the instant anything fails.

module device_map #(parameter int UNITS = 16) (
  input  logic clk, rst_n,
  input  logic alloc_en, input logic [3:0] alloc_unit,
  input  logic free_en,  input logic [3:0] free_unit,
  input  logic [1:0] q_dev,
  output logic [2:0] d_used0, d_used1, d_used2, d_used3,
  output logic [2:0] q_used, q_free,
  output logic [2:0] imbalance,
  output logic       place_err
);
  localparam int PER_DEV = UNITS / 4;
  logic [UNITS-1:0] used_q;
  logic [3:0] u0, u1, u2, u3, mx, mn;
 
  always_comb begin
    u0 = 4'd0; u1 = 4'd0; u2 = 4'd0; u3 = 4'd0;
    for (i = 0; i < PER_DEV; i = i + 1) begin
      u0 = u0 + {3'b0, used_q[i]};
      u1 = u1 + {3'b0, used_q[PER_DEV   + i]};
      u2 = u2 + {3'b0, used_q[2*PER_DEV + i]};
      u3 = u3 + {3'b0, used_q[3*PER_DEV + i]};
    end
    mx = u0; if (u1>mx) mx=u1; if (u2>mx) mx=u2; if (u3>mx) mx=u3;
    mn = u0; if (u1<mn) mn=u1; if (u2<mn) mn=u2; if (u3<mn) mn=u3;
  end
  assign imbalance = mx[2:0] - mn[2:0];
endmodule

The measurement that makes the point uses the same four allocations twice.

Identical capacity consumed. Identical free total. Completely different exposure: with the packed placement, losing device 0 costs four allocations, and with the spread placement it costs one.

Neither is correct in general. Packing leaves whole devices empty, which is what you want if you intend to power one down or reserve it. Spreading limits the damage from any single failure. This is a policy choice, it belongs to whoever operates the pool, and the only thing hardware owes it is the number: imbalance, measured at 4 packed and 0 spread on identical occupancy.

The important structural claim is that placement is state. If the allocator does not record which device holds each unit, then when a device fails the only honest answer to which hosts are affected is all of them — and a pool that cannot narrow that down cannot be operated. 12.4 builds on this directly.

10. RTL 5 — Free Is Not Allocatable

This is the model the chapter exists for.

A pool reporting free capacity is reporting a sum. An allocation needs a run. Those are different properties of the same bitmap, and they can be arbitrarily far apart.

module extent_scan #(parameter int UNITS = 16) (
  input  logic clk, rst_n,
  input  logic [UNITS-1:0] map_in,          // 1 = allocated
  output logic [4:0] free_total, largest, frags
);
  logic [4:0] ft, lg, fr, run;
  always_comb begin
    ft = 5'd0; lg = 5'd0; fr = 5'd0; run = 5'd0;
    for (i = 0; i < UNITS; i = i + 1) begin
      if (!map_in[i]) begin
        run = run + 5'd1;
        ft  = ft  + 5'd1;
        if (run == 5'd1) fr = fr + 5'd1;    // a run just started: new fragment
        if (run > lg)    lg = run;
      end else begin
        run = 5'd0;
      end
    end
  end
endmodule

Two bitmaps, measured:

Both pools are half free. One can satisfy a request for eight contiguous units. The other cannot satisfy a request for two.

A capacity counter reports 8 for both and is, in the narrow sense, telling the truth. It is also useless, because the only question anyone is actually asking is whether the next request can be served — and free_total cannot answer it. That takes largest, and diagnosing why a pool got into that state takes frags.

The fragment count is the operational signal. Free capacity falling means the pool is filling and somebody should buy more. Fragment count rising at constant free capacity means the pool is filling with holes, which is an allocation-policy problem and is not fixed by adding capacity. 12.2 attacks it directly.

11. RTL 6 — Two Failures That Must Not Share A Counter

An allocation request can fail for two reasons that look identical to the requester and are opposites to the operator.

module admit_gate (
  input  logic clk, rst_n,
  input  logic       req_valid,
  input  logic [4:0] req_size,
  input  logic [4:0] free_total,     // from the ledger
  input  logic [4:0] largest,        // from the extent scan
  output logic       grant, fail_cap, fail_frag,
  output logic [7:0] n_req, n_grant, n_cap, n_frag
);
  logic cap_short, frag_short;
  assign cap_short  = req_valid && (req_size > free_total);
  assign frag_short = req_valid && !cap_short && (req_size > largest);
 
  assign fail_cap  = cap_short;
  assign fail_frag = frag_short;
  assign grant     = req_valid && !cap_short && !frag_short;
endmodule

The ordering is deliberate. Capacity is tested first, because reporting a fragmentation failure on a pool that is simply empty sends an operator to defragment nothing.

Run against the two bitmaps from section 10, asking for two units each time:

Same request, same free capacity, opposite results — and the counters say which. Over the full run: 8 requests, 4 granted, 2 capacity failures, 2 fragmentation failures, with every request accounted for exactly once.

Merging those two counters is a real and common design error. The remedies are opposite. A capacity failure means the pool needs more memory. A fragmentation failure means the pool has the memory and the allocation policy has broken it into unusable pieces — and buying more capacity postpones the problem by exactly one fill cycle.

12. RTL 7 — The Byte You Paid For And Cannot Use

Pools hand out whole units. A request is therefore rounded up, and the difference is capacity the host is charged for and cannot address.

module unit_gran #(parameter int UNIT_BYTES = 256, parameter int FAULT_INJECT = 0) (
  input  logic clk, rst_n,
  input  logic        req_valid,
  input  logic [15:0] req_bytes,
  output logic [7:0]  units,
  output logic [15:0] res_bytes, waste,
  output logic [31:0] tot_req, tot_res, tot_waste,
  output logic [15:0] n_req,
  output logic        waste_err
);
  localparam int SHIFT = $clog2(UNIT_BYTES);
  logic [16:0] rounded;
  assign rounded   = {1'b0, req_bytes} + UNIT_BYTES[16:0]
                   - ((FAULT_INJECT == 0) ? 17'd1 : 17'd0);
  assign units     = rounded[16:SHIFT];
  assign res_bytes = {units, {SHIFT{1'b0}}};
  assign waste     = res_bytes - req_bytes;
endmodule

With a teaching unit size of 256 bytes — this figure is chosen to make the effect legible and is not a CXL quantity:

One byte past a unit boundary costs an entire additional unit, of which 255 bytes are unusable. Across the seven-request run the pool reserved 19200 bytes to satisfy 18561, wasting 639 — an allocation efficiency of 96%.

The tradeoff runs in both directions and neither end is free:

waste_err guards the rounding itself: per-request waste can never reach a whole unit, because if it does the pool is reserving capacity nobody asked for. Like the conservation monitor, it cannot fire while the arithmetic is right — so the same fault-injection hook proves it works. With the hook armed the same seven requests reserve 19968 bytes instead of 19200 and the alarm fires.

13. RTL 8 — Three Accountings That Must Agree

The pool now has three independent records of the same fact: the ledger's used_q, the bitmap's popcount, and the sum of the ownership table's per-host counts. In a correct system all three are equal at all times.

module pool_reconcile (
  input  logic clk, rst_n,
  input  logic       sample_en,
  input  logic [7:0] ledger_used, bitmap_used, owner_used, pool_total,
  output logic [7:0] high_water,      // telemetry
  output logic [7:0] free_now,        // policy input
  output logic       accounting_err,  // hard alarm
  output logic [15:0] n_samples, n_mismatch
);
  logic agree;
  assign agree    = (ledger_used == bitmap_used) && (ledger_used == owner_used);
  assign free_now = pool_total - ledger_used;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      high_water <= 8'd0; accounting_err <= 1'b0;
      n_samples <= 16'd0; n_mismatch <= 16'd0;
    end else if (sample_en) begin
      n_samples <= n_samples + 16'd1;
      if (ledger_used > high_water) high_water <= ledger_used;
      if (!agree) begin
        accounting_err <= 1'b1;
        n_mismatch <= n_mismatch + 16'd1;
      end
    end
  end
endmodule

Note that the three outputs are not the same kind of signal, and the module's comments say so:

Telemetry describes what happened. A policy input feeds a decision. A hard alarm means the system's model of itself is wrong and no decision built on it is safe. Mixing the three is how a genuine corruption ends up on the same dashboard panel as a utilisation graph.

High water is sampled on the edge that presents the value, which is a repeated lesson from earlier modules: a peak observed only after it has passed was never recorded. The run drives occupancy to 31, drains it to 4, and the mark still reads 31; a single-sample peak of 52 is captured and survives everything after it.

14. Quantitative Reasoning

Four numbers describe a pool, and they answer different questions.

Utilisation. The fraction of usable capacity currently allocated:

U = allocated / (total - unavailable)

The denominator matters. After the measured failure event the pool holds 64 units of which 12 are unavailable, so 20 allocated units is 20/52 = 38% utilised, not 20/64 = 31%. Reporting against physical capacity flatters the system and hides the failure.

Allocation efficiency. Requested bytes over reserved bytes:

E = tot_req / tot_res = 18561 / 19200 = 96%

The missing 4% is internal fragmentation — real capacity, paid for, unaddressable. It scales with the number of requests, not their size, so a pool serving many small requests loses far more than one serving few large ones.

External fragmentation has no single number, and pretending otherwise is the mistake. It takes two:

free_total = 8      largest = 1     -> 2 units unallocatable
free_total = 8      largest = 8     -> 8 units allocatable

Both pools report the same free capacity. The pair is the metric.

Pool balance. Maximum device occupancy minus minimum, measured at 4 for the packed placement and 0 for the spread one at identical total occupancy. It is a policy dial, not a correctness measure — a fully packed pool is not broken, it is exposed.

15. Assertions

Every property below is written as SystemVerilog for the reader and executed as procedural checker logic in the run, because the available simulator does not execute concurrent assertions — see section 17.

Capacity is conserved.

property p_conserve;
  @(posedge clk) disable iff (!rst_n)
    (free_q + used_q + unav_q) == TOTAL;
endproperty

A grant never exceeds what the pool holds.

property p_no_phantom;
  @(posedge clk) disable iff (!rst_n)
    accepted |-> (nF >= 0) && (nU >= 0) && (nV >= 0);
endproperty

A unit is never handed to a second owner.

property p_unique_owner;
  @(posedge clk) disable iff (!rst_n)
    (asg_en && valid_q[asg_unit]) |-> !asg_grant;
endproperty

A release must come from the recorded owner.

property p_owner_release;
  @(posedge clk) disable iff (!rst_n)
    rel_grant |-> (owner_q[rel_unit] == rel_host);
endproperty

Every request produces exactly one outcome.

property p_one_outcome;
  @(posedge clk) disable iff (!rst_n)
    req_valid |-> ($countones({grant, fail_cap, fail_frag}) == 1);
endproperty

A fragmentation failure implies the capacity was present.

property p_frag_implies_capacity;
  @(posedge clk) disable iff (!rst_n)
    fail_frag |-> (req_size <= free_total);
endproperty

Reserved capacity is never below requested.

property p_reserve_covers;
  @(posedge clk) disable iff (!rst_n)
    req_valid |-> (res_bytes >= req_bytes) && (waste < UNIT_BYTES);
endproperty

The three accountings agree.

property p_reconcile;
  @(posedge clk) disable iff (!rst_n)
    sample_en |-> (ledger_used == bitmap_used) && (ledger_used == owner_used);
endproperty

The suite contains 135 assertion sites — 128 across the eight models and 7 more in the integration run, which re-checks the three accountings on every cycle. All pass.

16. Mutation Testing

Assertions that never fail prove nothing. Each mutation below is a single deliberate change to the RTL; a mutation that leaves the testbench passing is a hole in the testbench.

53 mutations injected, 53 killed, 0 surviving.

Representative kills, each naming a real defect:

Three mutations did not die on the first run, and none of them meant a missing checker.

The first was a mistake in the mutation, not the design, and moving the injection point killed it. The other two are the same category, and they are the reason both models carry a FAULT_INJECT hook: a monitor guarding an invariant that the module maintains by construction cannot be reached by any input sequence. Arming the hook on a second instance of the same source makes the monitor fire, and — because the checker line is shared — deleting it now dies.

This taxonomy has now held for five consecutive batches. Escapes are stimulus gaps, unreachable checkers, or late sampling. Not one has ever been a checker that was simply missing.

17. Verification Strategy

Tool reality first. The simulator available here is Icarus Verilog 13.0, which does not execute concurrent SVA: property blocks are read by humans and the equivalent logic is checked procedurally. Every property in section 15 has an executable counterpart, and the numbers reported in this chapter come from those. Where a chapter claims a property holds, it means a procedural check ran and passed — not that an assertion was written.

The oracle is structurally different from the design in every model. This is not a style preference; a testbench that recomputes the design's own algorithm can only prove the design agrees with itself.

The extent scan is the clearest case. The design walks the bitmap once carrying a run length. The oracle tries every start position and extends from it, and counts fragments from run boundaries rather than run starts. Two algorithms, same answer, and a bug in either one shows up as a disagreement.

Coverage. The points that matter for a pool are occupancy level, request size class, outcome, fragmentation level, and the concurrency shape of the cycle. The crosses worth driving are request size against fragmentation level, and outcome against occupancy — the second is what proves the admission gate classifies correctly across the whole range rather than at one convenient point.

A scoreboard for a pool holds one entry per allocation with unit, owner, and state. It is checked against the design's tables at every sample, and the check is a set comparison, not a count comparison — two tables can hold the same number of entries and disagree about every one of them.

18. Synthesis and Implementation Reality

Pool management is cheap to describe and can be expensive to build.

The bitmap is the easy part. One bit per allocation unit:

bits = capacity / allocation_unit

A large pool at a fine granularity is a lot of flops, and the granularity choice from section 12 is therefore also an area choice — halving the unit size doubles the bitmap and doubles the search.

The ownership table dominates. Each entry carries an owner field and a valid bit, and the width of the owner field grows with the log of the host count. Unlike the bitmap it is not one bit per unit but several, and it is read associatively.

The derived counters are the trap. The per-host occupancy in section 7 is computed by scanning the whole table combinationally. That is correct and it is honest teaching RTL, and at 16 units it is trivial. At a realistic unit count it is a wide adder tree that will not close timing in one cycle.

The fix is not to abandon derivation for incremented counters — that reintroduces exactly the drift the derivation prevents. It is to pipeline the scan and accept that occupancy is reported with a known latency, or to maintain incremented counters and periodically reconcile them against a scan, which is what pool_reconcile is for.

The extent scan has the same shape and is worse, because it is inherently sequential: each unit's run length depends on the one before it. A flat combinational implementation is a long carry chain. Realistic implementations pipeline it, or compute it hierarchically over blocks and merge at the boundaries, or maintain it incrementally as the bitmap changes.

No gate counts are offered here. The structural claims — bitmap scales with capacity over granularity, table scales with unit count times owner width, scan depth grows with the number of units — hold regardless of process, and the numbers do not.

19. Silicon Observability

A pool fails slowly, and it fails in the accounting before it fails in a way anybody notices. The counters below are what makes the difference between a diagnosis and a guess.

Individually they are ordinary. In combination they isolate specific failures, which is the point.

The most valuable of these is the third. accounting_err on its own means the pool's model of itself is wrong while nothing has yet been misallocated — the one window in which the problem is still cheap to fix. Without a reconciliation check, that window does not exist, and the first symptom is a host reading somebody else's data.

20. Debug Lab

  0xAAAA striped : free=8 largest=1 frags=8
  8 free, largest 1, request 2 : fail_frag=1 (capacity was there)

assign cap_short  = req_valid && (req_size > free_total);
assign frag_short = req_valid && !cap_short && (req_size > largest);

  second host takes unit 5: double_owner_err=1

assign asg_ok = asg_en && !valid_q[asg_unit];
if (asg_en && valid_q[asg_unit]) double_owner_err <= 1'b1;

if ((free_q + used_q + unav_q) != TOTAL[7:0]) conserve_err <= 1'b1;

  c6 | req=1 u= 9 h=1 | ret=0 u= 0 | free=14 used=2 | h1=0 h2=2 | dbl=1

assign asg_grant = asg_ok;          // the table publishes its decision
// ... and every downstream accounting is enabled from asg_grant, never asg_en

  packed  4 units : d0=4 d1=0 d2=0 d3=0 imbalance=4
  spread  4 units : d0=1 d1=1 d2=1 d3=1 imbalance=0

assign imbalance = mx[2:0] - mn[2:0];   // publish it, then decide about it

  totals: requested=18561 reserved=19200 waste=639 efficiency=96%

assign waste = res_bytes - req_bytes;
if (waste >= UNIT_BYTES[15:0]) waste_err <= 1'b1;   // rounding itself is wrong

  peak occupancy    : high_water=31 (telemetry)
  after draining    : high_water=31 (does not fall back)

if (ledger_used > high_water) high_water <= ledger_used;

  bitmap drift      : accounting_err=1 (hard alarm)
  samples=9 mismatches=2

assign agree = (ledger_used == bitmap_used) && (ledger_used == owner_used);
if (!agree) begin accounting_err <= 1'b1; n_mismatch <= n_mismatch + 16'd1; end

21. Design Review

Assembled, the eight models are one manager with a strict direction of flow.

What a reviewer should attack first.

The grant boundary. Every enable feeding an accounting structure must originate at the ownership table's decision. This is the single defect that reached the integrated baseline in this chapter, it is invisible until the first refused request, and refusals are routine. Ask to see the enable, not the diagram.

The derived counters. Per-host occupancy is recomputed from the table on every cycle. That is correct and it will not close timing at scale. A reviewer should ask what the plan is — pipelined scan, or incremented counters with periodic reconciliation — and reject "we will optimise it later", because the two answers have different verification consequences.

The two failure counters. If n_cap and n_frag are one counter, the design has decided that operators will never need to distinguish buying capacity from fixing policy. That decision should be made explicitly or not at all.

The unreachable monitors. conserve_err and waste_err cannot fire through the ports. Ask how they were tested. If the answer is inspection, they are decoration.

What is deliberately not here. No allocator: section 11 tests whether a request can be served, and 12.2 decides where. No host lifecycle, no generations, no reassignment — 12.3. No rack, no enclosure, no reachability — 12.4. No fabric manager and no switch — Modules 15 and 16.

22. How This Appears in Real Engineering

In architecture review, the argument is almost never about whether pooling works. It is about granularity. A fine unit gives better utilisation and costs bitmap area, table entries, search depth and fragment-management work; a coarse unit gives the opposite. The measured 96% allocation efficiency in section 12 is the shape of that argument made concrete, and it moves with unit size and with the request-size distribution, so neither side can win it without the workload.

In RTL design, the recurring mistake is the one section 13 documents: an accounting structure enabled by a request. It survives review because the block diagram is right — the arrow does point from the allocator to the ledger — and only the enable term is wrong.

In verification, the hard part is that the interesting behaviour is concurrent. An allocation and a return in the same cycle, two requests for the last extent, a return arriving while a device fails: none of these appear in directed tests written from a specification, and all of them appear in production within hours.

In bring-up, pools fail quietly. A leak of a fraction of a percent per hour is invisible on a dashboard and fatal over a month. The reconciliation check is what turns that into an event with a timestamp.

In operations, the single most requested number is the one section 10 supplies: not how much is free, but how much can be allocated. Every pool that ships without it generates the same support ticket repeatedly.

23. Common Misconceptions

"A pool is several hosts sharing memory." Sharing is what it looks like from outside. Inside, it is inventory management with correctness obligations, and every one of this chapter's eight models exists to satisfy one of them.

"If the pool reports free capacity, an allocation will succeed." Measured false: 8 units free, largest extent 1, a two-unit request refused.

"Free capacity is the pool's utilisation denominator." Only if nothing has failed. With 12 units unavailable, 20 allocated units is 38% of usable capacity and 31% of physical capacity, and the second number describes a pool that does not exist any more.

"A bitmap is enough." A bitmap says a unit is taken. It cannot validate a return, cannot answer who is affected by a device failure, and cannot bound a blast radius.

"Reassignment is a table write." The ownership table refuses a same-cycle release and assign of one unit, and it is right to: the new owner would be enabled before the old one had retired. Measured, the unit ends free and the handover completes a cycle later.

"Redundant accountings are safer." Only with a comparison. Three structures counting the same thing without a reconciler is three chances to be wrong and no way to find out.

"A monitor in the RTL means the invariant is checked." Not if no stimulus can reach it. Two monitors in this chapter needed a fault-injection hook before they could be shown to work at all.

"Fragmentation is fixed by adding capacity." It is postponed by exactly one fill cycle. n_frag rising while n_cap stays flat is a policy problem wearing a capacity problem's clothes.

24. Interview Reasoning

25. Exercises

1. Calculation. A 1 TiB pool uses 256 MiB allocation units. Compute the bitmap width in bits, and the ownership table size in bits for 64 hosts with a valid bit per unit. Then repeat both for a 64 MiB unit and state which structure grows fastest and why.

2. Analysis. A pool reports 40% utilisation and refuses a request for 16 contiguous units. Give the two measurements that distinguish a fragmentation refusal from a capacity refusal, state the values you would expect in each case, and explain why utilisation alone cannot separate them.

3. RTL task. Extend pool_ledger with a fourth state, reserved, for capacity promised to a request that has not yet been activated. State the new conservation law, and identify the one transition that must not be allowed to skip the reserved state.

4. Assertion task. Write the property proving that a fragmentation failure implies the capacity was present. Then explain why this property is stronger than asserting that the two failure counters are never both set, and which real defect only the first one catches.

5. Design task. Redesign extent_scan to compute the largest free extent hierarchically over four-unit blocks. Specify exactly what each block must publish for the merge to work, and prove the merged result is correct when a run spans a block boundary.

6. Testbench design. Design the stimulus that distinguishes an accounting driven by grants from one driven by requests. Explain why a test in which every request succeeds cannot distinguish them, and state the minimum sequence that can.

7. Debug task. A pool leaks roughly 0.1% of capacity per hour. Give your investigation order, name the single check that converts this from a trend into an event with a timestamp, and explain why that check is unreachable in verification without a fault-injection hook.

8. Design review. A colleague argues that internal fragmentation is negligible because allocations are large, and proposes doubling the allocation unit to halve the bitmap. Give the strongest version of that argument, then state the request-size distribution that makes it fail and the counter that would prove it in production.

26. Summary

A pool turns memory capacity into inventory — counted, owned, placed, allocated and returned, with every verb a state transition that hardware has to get right.

• Capacity must be conserved. Free plus allocated plus unavailable equals the total, checked continuously. The fault-injected instance holds 48 units of 64 and says so.
• Simultaneous events need one next-state decision. Allocating 5 while returning 3 gives free=56, used=8 — the twelfth appearance of a defect that has never once survived construction-by-combination.
• The exact ceiling is legal and one unit past it is not. Measured free=0, used=64, overdraw=0 against an unchanged state with overdraw=1.
• Free is not allocatable. 0xFF00 and 0xAAAA both hold 8 free units; largest extents of 8 and 1, fragments of 1 and 8, and a two-unit request that succeeds against one and fails against the other.
• Capacity failures and fragmentation failures are different problems. Measured 8 requests: 4 granted, 2 capacity, 2 fragmentation, every request accounted for exactly once.
• A pool is one number to a host and several devices to an operator. The same four allocations give an imbalance of 4 packed and 0 spread, and a device failure costs four allocations or one.
• Granularity is paid for in bytes nobody can address. 18561 bytes requested reserved 19200 — 96% allocation efficiency — and one byte past a boundary costs a whole unit.
• Three accountings must be compared, not merely maintained. Two injected drifts produced 2 mismatches over 9 samples, each naming its own structure.
• Accounting must be driven by outcomes. The integration defect — a refused request that still moved the free counter — was found by the baseline, not by mutation testing, and fixed by making the ownership table publish its grant.
• Verification: 135 assertion sites, 53 of 53 mutations killed, zero surviving. Three first-run escapes were one defective mutation and two monitors unreachable through the ports.

Next: 12.2 Resource Allocation, which takes the admission gate's yes and asks the question this chapter never does — where. Choosing among candidate extents, splitting and merging them, and running the lifecycle that turns a grant into an owner.