GPUs

   1  WHICH CONSTRAINT
        a BIMODAL requester mix -- two populations whose answers to
        31.4 §4's latency condition are at opposite extremes (§3)

   2  WHAT DECISION
        SEPARATE the populations rather than averaging them, because
        no single tuning serves both and they are COUPLED (§5, §6)

   3  WHAT GRADE
        almost entirely D. The mechanisms are generic and the
        platform figures are not published (§8)

   latency is INVISIBLE to a requester iff   N >= ceil( L / S )

     L  the memory's completion latency, in cycles
     S  the spacing between successive returns the channel sustains
     N  the transactions the requester keeps outstanding

   and 31.4 §4's result: HALVING S DOUBLES the required N. A faster
   channel raises the bar.

   GRADE D.  L = 200 cycles,  S = 4 cycles.
   DERIVED:  N* = ceil(200 / 4) = 50 outstanding transactions.

     population T :  N_T = 4096
         DERIVED  N_T / N*  =  81.9x
         -> latency is invisible. Raising L changes NOTHING
            observable for T until L exceeds 4096 * 4 = 16,384.

     population L :  N_L = 2   (a two-deep dependency chain)
         DERIVED  N_L / N*  =  0.04
         -> every cycle of L is SERIALISED. L pays 200 cycles per
            access, and doubling L doubles its cost exactly.

   TUNING 1 -- for THROUGHPUT.
     deep reorder window, long direction batches, coarse access
     granularity, aggressive row-hit preference (23.4)

     effect on S : improves. say S: 4 -> 3.4  (+18% throughput)
     effect on L : worsens.  say L: 200 -> 400 (deeper queues,
                   longer batches ahead of any given request)

     population T :  N* becomes ceil(400/3.4) = 118
                     N_T/N* = 4096/118 = 34.7x   -- still clear
                     gain: +18% throughput.  COST: none.
     population L :  cost 200 -> 400 cycles.  DOUBLED.

   TUNING 2 -- for LATENCY.
     shallow queues, no batching, near-FCFS service

     effect on L : improves. say L: 200 -> 120
     effect on S : worsens.  say S: 4 -> 5.2  (-23% throughput)

     population T :  loses 23% of its throughput -- its VISIBLE
                     output.
     population L :  cost 200 -> 120.  -40%.

   mean latency under tuning 1:
       0.97 * (T's latency, which it does not feel) + 0.03 * 400

   the first term is the problem: T's requests DO have a latency
   and T DOES NOT CARE. Including them in a mean produces a number
   dominated by requests nobody is waiting for.

   23.1 §9 owns this exactly -- the average is the wrong statistic --
   and here it is worse than wrong: the 97% that dominates the mean
   is precisely the part with no deadline.

   DERIVED from a stated model. GRADE D.

     launch interval        I = 2,000 cycles  (a new batch of T work
                                is dispatched this often)
     L's latency per launch = the chain's cost, serialised

   under TUNING 1 (§4): L's cost rises 200 -> 400 cycles.

     extra stall per launch      = 200 cycles
     as a fraction of the period = 200 / 2000 = 10.0%

   so T's UTILISATION falls by 10% -- it spends 10% more of each
   period waiting to be told what to do.

   and the throughput gain from tuning 1 was +18% (§4).

     net effect = 1.18 x (1 - 0.10) = 1.062
       -> +6.2%, not +18%. Two thirds of the gain is consumed by
          the coupling.

   recompute at I = 800 cycles (a finer-grained workload):
     stall fraction = 200 / 800 = 25.0%
     net = 1.18 x 0.75 = 0.885   ->  -11.5%. NET NEGATIVE.

   tuning for throughput is net positive iff

       (1 + g)  x  (1 - dL / I)  >  1

     g   the throughput gain
     dL  the increase in L's serialised cost
     I   the launch interval

   so the break-even launch interval is

       I*  =  dL x (1 + g) / g

   DERIVED with g = 0.18, dL = 200:
       I* = 200 x 1.18 / 0.18 = 1,311 cycles

   workloads with a launch interval SHORTER than ~1,300 cycles lose
   from this tuning. Longer ones gain.

   what must be partitioned, and why sharing fails for each

     ADMISSION CREDITS   T can hold every credit. L then waits at
                         admission, and its wait is a function of
                         T's occupancy -- unbounded in L's terms.
                         §13's defect.

     QUEUE ENTRIES       L's entries sit behind T's thousands.
                         Head-of-line blocking across populations.

     REORDER WINDOW      a window deep enough to serve T's
                         throughput is deeper than L's whole chain.

   what must NOT be partitioned

     LEGALITY            the thirteen obligations are properties of
                         the DRAM and know nothing about who asked
                         (31.1 §5, 32.1 §8). Partitioning legality
                         would be 17.4 §3's "inverse error, which is
                         worse".

   DERIVED, grade D. Same L = 200, two attaches.

     attach 1 (perimeter, higher per-pin rate):  S = 4
         N* = 50
         T : 4096/50  = 81.9x clear
         L : 2/50     = cannot clear

     attach 2 (on-package, many narrow channels): S = 1.5
         N* = ceil(200/1.5) = 134
         T : 4096/134 = 30.6x clear
         L : 2/134    = cannot clear, and the RATIO is worse

   DERIVED: the faster attach helps T (more throughput) and moves L
   FURTHER from the condition it already could not meet.

// ---------------------------------------------------------------------
// population_admission -- the platform-profile block of §10.
//
// CLASSIFICATION: synthesisable, grade-D parameter values, CORRECT as
// written. The intentionally defective block is §13.
//
// WHAT IT IS: §6's part 2 as hardware -- a STRUCTURAL partition of
// admission credits, not a preference over a shared pool. With
// outstanding counts of 4096 against 2 (§3), any shared resource
// served by preference gives population L an unmeasurable share, and
// 17.4 §9 owns why: a preference layer with no bounded override
// starves.
//
// WHY IT EXISTS HERE: §5 derives that starving L can reduce T's
// delivered throughput, and §4 that no single tuning serves both. So
// the response is separation, and separation of a shared credit pool
// is the part that must be structural rather than policy.
//
// HOW TO RUN IT: backlog population T to its full credit allocation
// and then present a single population-L request.
// EXPECTED RESULT: L is admitted within its own allocation,
// independent of T's occupancy.
// EXPECTED TRACE: l_admit must rise while t_credits_used is at its
// maximum. §14's block cannot do this.
//
// SYNTHESIS: one credit counter per population plus a small compare.
//
// LIMITATIONS: partitions ADMISSION. It does not partition queues or
// reorder windows -- §6 lists those as also requiring partition, and
// 17.2 owns the entry pool. Nor does it partition LEGALITY, which
// §6 and 17.4 §3 both say must never be partitioned. Those
// boundaries are STATED and are not the bug.
// ---------------------------------------------------------------------
module population_admission #(
  // The platform property. A single-population platform needs no
  // partition, so the mechanism is ABSENT rather than disabled.
  parameter int NUM_POP    = 2,

  // Grade D allocations. On a real platform these are CONFIGURATION
  // inputs, for 32.1 §13's reason: an allocation is a platform
  // property and a platform property in a parameter is grade D
  // consumed as grade A. They are parameters here only to keep the
  // block readable, and the elaboration guard below is what a
  // runtime version would check instead.
  parameter int CREDITS_T  = 512,
  parameter int CREDITS_L  = 8,

  // COUNT, not INDEX: each counter must REPRESENT its allocation
  // inclusive, so it needs $clog2(allocation + 1) bits. Sized
  // $clog2(allocation) a full pool wraps to empty and admission
  // becomes unbounded -- the counter failing inside the exhaustion
  // case it exists to detect.
  parameter int CT_W       = $clog2(CREDITS_T + 1),
  parameter int CL_W       = $clog2(CREDITS_L + 1)
)(
  input  logic              clk,
  input  logic              rst_n,

  // Population T.
  input  logic              t_req,
  input  logic              t_done,
  output logic              t_admit,

  // Population L.
  input  logic              l_req,
  input  logic              l_done,
  output logic              l_admit,

  output logic [CT_W-1:0]   t_credits_used,
  output logic [CL_W-1:0]   l_credits_used,
  output logic              t_exhausted,
  output logic              l_exhausted,
  output logic              credit_underflow
);
  initial begin
    if (NUM_POP < 1) $fatal(1, "population_admission: NUM_POP >= 1");
    if (CREDITS_T < 1 || CREDITS_L < 1)
      $fatal(1, "population_admission: each allocation must be >= 1");
    // §6 part 2: L's allocation must at least cover its chain depth,
    // or the partition is present and useless. A chain of depth N_L
    // that cannot hold N_L credits serialises on admission as well as
    // on latency -- 31.2 §7's "present in the source, absent in the
    // silicon", applied to an allocation.
    if (NUM_POP > 1 && CREDITS_L < 2)
      $fatal(1, "population_admission: CREDITS_L < 2 cannot cover a dependency chain (§6)");
  end

  generate
  if (NUM_POP > 1) begin : g_partitioned

    logic [CT_W-1:0] ct;
    logic [CL_W-1:0] cl;

    // Two INDEPENDENT counters. This is the whole mechanism, and its
    // simplicity is the argument: a partition needs no arbitration,
    // no weights and no fairness bound, because neither population
    // can reach the other's resource at all.
    assign t_exhausted = (ct >= CREDITS_T[CT_W-1:0]);
    assign l_exhausted = (cl >= CREDITS_L[CL_W-1:0]);

    assign t_admit = t_req && !t_exhausted;
    assign l_admit = l_req && !l_exhausted;

    always_ff @(posedge clk) begin
      if (!rst_n) begin
        ct <= '0;  cl <= '0;  credit_underflow <= 1'b0;
      end else begin
        // Each population's counter moves only on its own events.
        // §6's part 1 is what makes this possible: without a
        // population identifier on the request, the controller
        // cannot separate what it was not told, and a population
        // CANNOT be inferred from the request's fields.
        unique case ({t_admit, t_done})
          2'b10 : ct <= ct + 1'b1;
          2'b01 : begin
                    if (ct == '0) credit_underflow <= 1'b1;
                    else          ct <= ct - 1'b1;
                  end
          default : ;   // both or neither: net zero
        endcase
        unique case ({l_admit, l_done})
          2'b10 : cl <= cl + 1'b1;
          2'b01 : begin
                    // A completion with no outstanding request is an
                    // ERROR, not a saturating subtract. Absorbing it
                    // lets the counter drift and every figure below
                    // it becomes meaningless -- 30.8 §11's rule.
                    if (cl == '0) credit_underflow <= 1'b1;
                    else          cl <= cl - 1'b1;
                  end
          default : ;
        endcase
      end
    end

    assign t_credits_used = ct;
    assign l_credits_used = cl;

  end else begin : g_single

    // One population: no partition exists, and the single pool is
    // correct rather than a compromise.
    logic [CT_W-1:0] ct;
    assign t_exhausted    = (ct >= CREDITS_T[CT_W-1:0]);
    assign l_exhausted    = 1'b0;
    assign t_admit        = t_req && !t_exhausted;
    assign l_admit        = 1'b0;
    assign l_credits_used = '0;
    always_ff @(posedge clk) begin
      if (!rst_n) begin ct <= '0; credit_underflow <= 1'b0; end
      else begin
        unique case ({t_admit, t_done})
          2'b10 : ct <= ct + 1'b1;
          2'b01 : begin
                    if (ct == '0) credit_underflow <= 1'b1;
                    else          ct <= ct - 1'b1;
                  end
          default : ;
        endcase
      end
    end
    assign t_credits_used = ct;

  end
  endgenerate
endmodule

// ---------------------------------------------------------------------
// population_queues -- CORRECT as written. Grade-D depths.
//
// CLASSIFICATION: synthesisable. Consumes 17.2's entry discipline and
// does not reimplement it.
//
// WHAT IT IS: §6 part 2's second partition -- separate entry pools
// with separate reorder windows, so a population-L entry never sits
// behind a population-T backlog.
//
// WHY IT EXISTS HERE: §10 partitions ADMISSION. A request admitted
// into a shared queue has merely moved its wait from the credit stage
// to the queue stage, and §5's coupling does not care which stage the
// stall happened in. So the partition must cover both, and §6 says so.
//
// HOW TO RUN IT: fill population T's pool and present a
// population-L request.
// EXPECTED RESULT: L's entry is allocated and becomes a candidate
// without waiting for any T entry to retire.
// EXPECTED TRACE: l_cand must rise while t_pool_full is high.
//
// SYNTHESIS: two free-lists and two window counters. The entries
// themselves are 17.2's pool and are not duplicated here.
//
// LIMITATIONS: partitions ENTRIES and the REORDER WINDOW. It does not
// partition legality -- §6 and 17.4 §3 both forbid that -- and it
// does not choose among candidates, which is 17.4's layered mask.
// One entry per population per cycle, so 17.2 §13's simultaneous
// allocation-and-free case is out of scope and STATED.
// ---------------------------------------------------------------------
module population_queues #(
  parameter int DEPTH_T   = 64,     // grade D
  parameter int DEPTH_L   = 4,      // grade D: covers the chain (§6)
  // The reorder window per population. §4's tuning argument in
  // hardware: T wants a window deep enough to find row hits, and a
  // window deeper than L's whole chain can only delay L.
  parameter int WIN_T     = 32,
  parameter int WIN_L     = 1,      // near-FCFS, per §4's tuning 2
  // COUNT, not INDEX: each occupancy must represent its depth
  // inclusive, so $clog2(depth + 1). Sized $clog2(depth) a full pool
  // reads as empty and allocation becomes unbounded.
  parameter int OT_W      = $clog2(DEPTH_T + 1),
  parameter int OL_W      = $clog2(DEPTH_L + 1)
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             t_alloc, t_retire,
  input  logic             l_alloc, l_retire,

  output logic             t_pool_full, l_pool_full,
  output logic             t_cand, l_cand,
  output logic [OT_W-1:0]  t_occ,
  output logic [OL_W-1:0]  l_occ,
  output logic             hol_blocked,
  output logic             pool_underflow
);
  initial begin
    if (DEPTH_T < 1 || DEPTH_L < 1)
      $fatal(1, "population_queues: each depth must be >= 1");
    // §6 part 2 and §16's two-sided bound: a window deeper than the
    // population's own pool can never fill, so it is a parameter that
    // does nothing -- 31.2 §7's "present in the source, absent in
    // the silicon" applied to a reorder window.
    if (WIN_T > DEPTH_T) $fatal(1, "population_queues: WIN_T exceeds DEPTH_T");
    if (WIN_L > DEPTH_L) $fatal(1, "population_queues: WIN_L exceeds DEPTH_L");
    // §4's tuning asymmetry, enforced: L's window must not be tuned
    // like T's, or the partition reproduces the shared behaviour it
    // exists to prevent.
    if (WIN_L > 4)
      $warning("population_queues: WIN_L = %0d reorders L's dependency chain (§4)", WIN_L);
  end

  logic [OT_W-1:0] ot;
  logic [OL_W-1:0] ol;

  assign t_pool_full = (ot >= DEPTH_T[OT_W-1:0]);
  assign l_pool_full = (ol >= DEPTH_L[OL_W-1:0]);

  // Candidacy is per population and independent BY CONSTRUCTION.
  // This is the whole mechanism: neither expression mentions the
  // other population's state, so §16's isolation property is
  // trivially true here and false in any shared design.
  assign t_cand = (ot != '0);
  assign l_cand = (ol != '0);

  // The observable §6 needs and §18 measures: an L entry exists and
  // cannot proceed while T's pool is full. In THIS block that is
  // impossible, so the signal is identically low -- and 30.5 §11's
  // lesson applies: a guard another structure always shadows is
  // UNTESTED, so the cover below watches it rather than assuming it.
  assign hol_blocked = l_alloc && !l_cand && t_pool_full;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      ot <= '0;  ol <= '0;  pool_underflow <= 1'b0;
    end else begin
      unique case ({t_alloc && !t_pool_full, t_retire})
        2'b10 : ot <= ot + 1'b1;
        2'b01 : begin
                  if (ot == '0) pool_underflow <= 1'b1;
                  else          ot <= ot - 1'b1;
                end
        default : ;
      endcase
      unique case ({l_alloc && !l_pool_full, l_retire})
        2'b10 : ol <= ol + 1'b1;
        2'b01 : begin
                  // A retire with nothing allocated is an ERROR, not
                  // a saturating subtract -- 30.8 §11: an instrument
                  // that can report an impossible value has never
                  // been checked.
                  if (ol == '0) pool_underflow <= 1'b1;
                  else          ol <= ol - 1'b1;
                end
        default : ;
      endcase
    end
  end

  assign t_occ = ot;
  assign l_occ = ol;
endmodule

  // ---- The queue partition's own contract.
  // Isolation, the same class 31.3 §15 named for replicated channels
  // and §16 names for credits. Vacuously true in a shared pool, so a
  // design grown from one has never had it checked.
  property p_t_alloc_does_not_move_l_occ;
    @(posedge clk) disable iff (!rst_n)
      (t_alloc && !l_alloc && !l_retire) |=> $stable(l_occ);
  endproperty
  assert property (p_t_alloc_does_not_move_l_occ)
    else $error("a T allocation changed L's queue occupancy");

  // L's candidacy must not depend on T's pool at all -- clause 2 of
  // §13's contract, restated for the queue stage.
  property p_l_candidacy_independent;
    @(posedge clk) disable iff (!rst_n)
      (l_occ != '0) |-> l_cand;
  endproperty
  assert property (p_l_candidacy_independent)
    else $error("L had entries and was not a candidate");

  // Head-of-line blocking across populations must be IMPOSSIBLE in a
  // partitioned design. An invariant, because there is no cycle on
  // which it is acceptable.
  property p_no_cross_population_hol;
    @(posedge clk) disable iff (!rst_n) !hol_blocked;
  endproperty
  assert property (p_no_cross_population_hol)
    else $error("cross-population head-of-line blocking occurred");

  // ---- Covers.
  // The case the partition exists for: T's pool full while L runs.
  cover property (@(posedge clk) disable iff (!rst_n)
                  t_pool_full && l_cand);
  // L's own pool full -- the legitimate limit, distinguishable from
  // the starvation case above.
  cover property (@(posedge clk) disable iff (!rst_n) l_pool_full);
  // Both pools occupied, so the bimodality was exercised rather than
  // assumed -- the per-dimension rule of 31.3 §15.
  cover property (@(posedge clk) disable iff (!rst_n)
                  (t_occ > 0) && (l_occ > 0));
  // T's reorder window actually full, so §4's tuning-1 behaviour is
  // known to have been reached.
  cover property (@(posedge clk) disable iff (!rst_n) t_occ >= WIN_T);

// ---------------------------------------------------------------------
// population_monitor -- verification/telemetry, CORRECT as written.
//
// CLASSIFICATION: synthesisable telemetry. Drives nothing. Grade D.
//
// WHAT IT DOES: keeps per-population latency extremes and outstanding
// extremes SEPARATE, and measures the launch interval and L's
// serialised cost so §5's net-effect condition can be evaluated.
//
// WHY IT EXISTS HERE: §4 proves a combined mean is dominated by the
// 97% with no deadline, and §5 proves the deciding quantity is a
// workload property (the launch interval) that no datasheet supplies.
// Both consequences are measurements, and §8 establishes that they
// are the ONLY grade above D available on this platform class.
//
// HOW TO RUN IT: run the real workload and evaluate §5's inequality
// from launch_interval and l_lat_max.
// EXPECTED RESULT: net_positive high when (1+g)(1 - dL/I) > 1.
//
// SYNTHESIS: four extreme trackers, two counters. NO divider -- §5's
// condition is evaluated by cross-multiplication.
//
// LIMITATIONS: reports extremes and a launch interval, NOT
// distributions. 23.1 §12 owns the distribution tracker and this
// block does not duplicate it; extremes are what §5's inequality
// needs. And it cannot measure the throughput gain g -- that is a
// comparison against another configuration, which 23.5's
// counterfactual owns.
// ---------------------------------------------------------------------
module population_monitor #(
  parameter int WIN       = 1048576,
  parameter int LAT_W     = 20,
  parameter int OCC_W     = 13,
  // Grade D. The throughput gain of the tuning under evaluation,
  // expressed in percent. It is an INPUT on a real platform because
  // 23.5's counterfactual measurement is the only way to obtain it.
  parameter int GAIN_PCT  = 18,
  parameter int CNT_W     = $clog2(WIN + 1)
)(
  input  logic              clk,
  input  logic              rst_n,

  input  logic              t_start, t_end,
  input  logic              l_start, l_end,
  input  logic [LAT_W-1:0]  t_lat_sample,
  input  logic [LAT_W-1:0]  l_lat_sample,
  input  logic [OCC_W-1:0]  t_outstanding,
  input  logic [OCC_W-1:0]  l_outstanding,
  input  logic              work_launch,
  input  logic              win_tick,

  output logic [LAT_W-1:0]  t_lat_max, t_lat_min,
  output logic [LAT_W-1:0]  l_lat_max, l_lat_min,
  output logic [OCC_W-1:0]  t_occ_max, l_occ_max,
  output logic [CNT_W-1:0]  launch_interval,
  output logic              net_positive,
  output logic              interval_unmeasured,
  output logic              result_valid
);
  logic [LAT_W-1:0] tmx, tmn, lmx, lmn;
  logic [OCC_W-1:0] tox, lox;
  logic [CNT_W-1:0] since_launch, sum_int, n_int;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      // AND-accumulator discipline: minimum trackers start at
      // all-ones or the first sample never wins and every reported
      // minimum stays zero, which would make every span look
      // enormous and hide the bimodality entirely.
      tmx <= '0;  tmn <= '1;  lmx <= '0;  lmn <= '1;
      tox <= '0;  lox <= '0;
      since_launch <= '0;  sum_int <= '0;  n_int <= '0;
      t_lat_max <= '0;  t_lat_min <= '0;
      l_lat_max <= '0;  l_lat_min <= '0;
      t_occ_max <= '0;  l_occ_max <= '0;
      launch_interval <= '0;
      net_positive <= 1'b0;  interval_unmeasured <= 1'b1;
      result_valid <= 1'b0;
    end else if (win_tick) begin
      // Published SEPARATELY. There is deliberately no combined
      // figure anywhere in this block's interface -- §4's whole
      // result is that a combined mean improves when the wrong
      // thing gets better, so the block does not offer one.
      t_lat_max <= tmx;  t_lat_min <= tmn;
      l_lat_max <= lmx;  l_lat_min <= lmn;
      t_occ_max <= tox;  l_occ_max <= lox;

      // The launch interval, as a mean over observed launches.
      // Reported as UNMEASURED rather than as zero when too few
      // launches occurred -- an instrument that can report a
      // meaningless value has not been checked (30.8 §11).
      interval_unmeasured <= (n_int < 2);
      launch_interval     <= (n_int >= 2) ? (sum_int / n_int) : '0;

      // §5's condition, cross-multiplied so no divider is needed:
      //     (1 + g)(1 - dL/I) > 1
      //  => (100 + GAIN_PCT) * (I - dL) > 100 * I
      // with dL taken as L's observed worst serialised cost.
      net_positive <= (n_int >= 2) &&
        (((100 + GAIN_PCT) * ((sum_int / n_int) - lmx)) > (100 * (sum_int / n_int)));

      result_valid <= 1'b1;
      tmx <= '0;  tmn <= '1;  lmx <= '0;  lmn <= '1;
      tox <= '0;  lox <= '0;  sum_int <= '0;  n_int <= '0;
    end else begin
      result_valid <= 1'b0;
      if (t_end) begin
        if (t_lat_sample > tmx) tmx <= t_lat_sample;
        if (t_lat_sample < tmn) tmn <= t_lat_sample;
      end
      if (l_end) begin
        if (l_lat_sample > lmx) lmx <= l_lat_sample;
        if (l_lat_sample < lmn) lmn <= l_lat_sample;
      end
      if (t_outstanding > tox) tox <= t_outstanding;
      if (l_outstanding > lox) lox <= l_outstanding;

      // The launch interval. §8's finding: this is a WORKLOAD
      // property and no datasheet supplies it, so it must be
      // observed on the software that will actually run.
      if (work_launch) begin
        if (n_int != {CNT_W{1'b1}}) begin
          sum_int <= sum_int + since_launch;
          n_int   <= n_int + 1'b1;
        end
        since_launch <= '0;
      end else if (since_launch != {CNT_W{1'b1}}) begin
        since_launch <= since_launch + 1'b1;
      end
    end
  end
endmodule

// ---------------------------------------------------------------------
// shared_credit_pool -- INTENTIONALLY DEFECTIVE, for review (§13).
//
// CLASSIFICATION: synthesisable, grade-D values, and CONTAINS A BUG.
//
// WHAT IT IS MEANT TO DO: the five-clause contract above -- admit
// requests against a per-population credit allocation.
//
// WHY IT EXISTS HERE: §6 part 2 argues the partition must be
// STRUCTURAL rather than policy, because with outstanding counts of
// 4096 against 2 (§3) any shared resource gives population L an
// unmeasurable share. This block is the shared version, and it is
// the natural design: one pool is simpler, uses the credits more
// efficiently, and measures better (§14).
//
// HOW TO RUN IT: backlog population T so it presents a request every
// cycle, then present a single population-L request.
// EXPECTED RESULT under clause 2: L is admitted promptly,
// independent of T's occupancy.
// EXPECTED TRACE: l_admit must rise within L's own allocation. It
// instead waits for T's backlog to drain.
//
// SYNTHESIS: one counter, one comparator.
//
// LIMITATIONS: admission only, as §10's block. That is STATED and is
// not the bug.
// ---------------------------------------------------------------------
module shared_credit_pool #(
  parameter int CREDITS_TOTAL = 520,     // grade D: 512 + 8
  parameter int C_W           = $clog2(CREDITS_TOTAL + 1)
)(
  input  logic             clk,
  input  logic             rst_n,

  // The population identifier IS on the interface. Clause 1 and 3
  // both depend on it.
  input  logic             req,
  input  logic             pop_id,        // 0 = T, 1 = L
  input  logic             done,
  input  logic             done_pop_id,

  output logic             admit,
  output logic [C_W-1:0]   credits_used,
  output logic             exhausted,
  output logic             credit_underflow
);
  logic [C_W-1:0] c;

  initial begin
    if (CREDITS_TOTAL < 2) $fatal(1, "shared_credit_pool: CREDITS_TOTAL >= 2");
  end

  // Clauses 3's accounting and 5's exhaustion report are both
  // present and both CORRECT for the pool as a whole. A reviewer
  // checking "are credits conserved?" and "is exhaustion reported?"
  // finds that they are, and that is what conceals the defect.
  assign exhausted = (c >= CREDITS_TOTAL[C_W-1:0]);
  assign admit     = req && !exhausted;   // <-- THE DEFECT

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      c <= '0;  credit_underflow <= 1'b0;
    end else begin
      unique case ({admit, done})
        2'b10 : c <= c + 1'b1;
        2'b01 : begin
                  if (c == '0) credit_underflow <= 1'b1;
                  else         c <= c - 1'b1;
                end
        default : ;
      endcase
    end
  end

  assign credits_used = c;
endmodule

   GRADE D.  CREDITS_TOTAL = 520.  S = 4 cycles per completion.
   Population T is backlogged: 4096 requests pending, presenting
   one every cycle. Population L presents ONE request.

   steady state with the shared pool:
       T holds all 520 credits.
       a credit returns every S = 4 cycles.
       T presents a request EVERY cycle, so it takes each
       returned credit first.

   L's wait = until T's backlog stops presenting.
       T's backlog drains at 1 request per S cycles:
       DERIVED  4096 x 4 = 16,384 cycles.

   so L's observed latency:
       contract (partitioned, §10) :   200 cycles
       this block                  : 16,384 + 200 = 16,584 cycles
       DERIVED ratio               : 82.9x

   DERIVED, using §5's model. Launch interval I = 2,000 cycles.

     dL = 16,584 - 200 = 16,384 cycles of extra serialised stall
     dL / I = 16,384 / 2,000 = 8.19

   the stall EXCEEDS the launch interval by a factor of eight, so
   population T cannot be re-launched on schedule at all. Its
   utilisation is set by L's admission wait, not by its own
   throughput.

   §5's condition: (1 + g)(1 - dL/I) > 1 requires dL/I < g/(1+g).
     with g = 0.18 :  dL/I must be < 0.153
     observed      :  8.19
   DERIVED: net effect is catastrophically negative.

   a throughput benchmark runs population T almost exclusively.
   under the SHARED pool, T can hold all 520 credits.
   under the PARTITIONED pool (§10), T can hold only 512.

   DERIVED: T's available concurrency is 520 vs 512, +1.6%.
   And §3 showed T clears its condition 81.9x over, so the extra
   credits translate directly into a marginally deeper pipeline
   and a marginally better sustained rate.

   so the defective block WINS the benchmark, by a small honest
   margin, and the partitioned block LOSES it.

  // CORRECTED. Clauses 1 and 2: per-population counters, so neither
  // population can reach the other's allocation at all.
  //
  // Note what is NOT added: no arbiter, no weight, no fairness
  // bound, no age threshold. 17.4 §9's machinery exists to make a
  // SHARED resource fair, and with a 2048:1 capability ratio (§3) no
  // weighting can achieve what removing the sharing achieves. A
  // partition is both cheaper and provable.
  assign t_exhausted = (ct >= CREDITS_T);
  assign l_exhausted = (cl >= CREDITS_L);
  assign admit = req && (pop_id ? !l_exhausted : !t_exhausted);
  // ... and ct / cl each move only on their own population's
  //     admit and done, keyed by pop_id and done_pop_id.

  // Offered as "proves the credit pool is correct". All PASS on the
  // defective block.
  property p_credits_never_exceed_pool;
    @(posedge clk) disable iff (!rst_n)
      credits_used <= CREDITS_TOTAL;
  endproperty
  assert property (p_credits_never_exceed_pool)
    else $error("credits used exceeded the pool");

  property p_no_admit_when_exhausted;
    @(posedge clk) disable iff (!rst_n)
      exhausted |-> !admit;
  endproperty
  assert property (p_no_admit_when_exhausted)
    else $error("a request was admitted with no credit available");

  property p_credits_conserved;
    @(posedge clk) disable iff (!rst_n)
      (admit && !done) |=> (credits_used == $past(credits_used) + 1);
  endproperty
  assert property (p_credits_conserved)
    else $error("credit accounting drifted");

  // Clause 1. Names pop_id, so it cannot pass while pop_id is
  // ignored. Variety 2's repair.
  property p_population_uses_own_allocation;
    @(posedge clk) disable iff (!rst_n)
      (admit && pop_id == 1'b1) |-> (l_credits_used < CREDITS_L);
  endproperty
  assert property (p_population_uses_own_allocation)
    else $error("population L was admitted outside its own allocation");

  // Clause 2, and it must be a BOUNDED LIVENESS property because the
  // defect is a starvation -- variety 8's repair. The bound is
  // JUSTIFIED from L's own allocation and completion rate, never
  // chosen: with CREDITS_L credits and a completion every S cycles,
  // a request waits at most CREDITS_L * S cycles for one of its
  // OWN credits. 30.9 §5 Q2 owns that a bound must be derived.
  property p_l_admission_is_bounded;
    @(posedge clk) disable iff (!rst_n)
      (l_req && !l_admit) |-> ##[1:(CREDITS_L*S_CYCLES)] l_admit;
  endproperty
  assert property (p_l_admission_is_bounded)
    else $error("population L's admission was not bounded by its own allocation");

  // And the INDEPENDENCE property, which is clause 2 stated
  // structurally rather than temporally: L's admission must not be a
  // function of T's occupancy at all. This is the property a
  // partition makes trivially true and a shared pool cannot satisfy.
  property p_l_admit_independent_of_t;
    @(posedge clk) disable iff (!rst_n)
      (l_req && !l_exhausted) |-> l_admit;
  endproperty
  assert property (p_l_admit_independent_of_t)
    else $error("L's admission depended on T's occupancy");

  // Clause 5: per-population exhaustion. One flag cannot express
  // which population is starved, so the property names both.
  property p_exhaustion_is_per_population;
    @(posedge clk) disable iff (!rst_n)
      (l_req && !l_admit) |-> l_exhausted;
  endproperty
  assert property (p_exhaustion_is_per_population)
    else $error("L was refused without its own exhaustion being reported");

  // ---- Covers. The dimension this defect scales with is the
  //      POPULATION RATIO, and 31.3 §15's rule says the cover must be
  //      on that dimension.
  // The case that matters: T saturated AND L requesting. A throughput
  // benchmark never produces it, because its purpose is to keep T
  // saturated with no L traffic at all (§14).
  cover property (@(posedge clk) disable iff (!rst_n)
                  t_exhausted && l_req);
  // L admitted while T is saturated -- the positive outcome, and the
  // one §13's block cannot produce.
  cover property (@(posedge clk) disable iff (!rst_n)
                  t_exhausted && l_admit);
  // Both populations active at all, so the bimodality is known to
  // have been exercised rather than assumed.
  cover property (@(posedge clk) disable iff (!rst_n)
                  (t_outstanding > 0) && (l_outstanding > 0));
  // L's own allocation exhausted -- the legitimate refusal, which
  // must be distinguishable from the starvation case above.
  cover property (@(posedge clk) disable iff (!rst_n) l_exhausted);
  // And the single-population arm, per 31.1 §14's configuration rule.
  cover property (@(posedge clk) disable iff (!rst_n)
                  (NUM_POP == 1) && t_admit);

  // The structural independence of the two counters. In §10's block
  // this is true by construction; in §13's it is false. A property
  // that distinguishes two designs at a glance is worth more than a
  // property that constrains one of them tightly.
  property p_t_events_do_not_move_l;
    @(posedge clk) disable iff (!rst_n)
      (t_admit && !l_admit && !l_done) |=> $stable(l_credits_used);
  endproperty
  assert property (p_t_events_do_not_move_l)
    else $error("a population-T event changed population L's credit count");

  property p_l_events_do_not_move_t;
    @(posedge clk) disable iff (!rst_n)
      (l_admit && !t_admit && !t_done) |=> $stable(t_credits_used);
  endproperty
  assert property (p_l_events_do_not_move_t)
    else $error("a population-L event changed population T's credit count");

  // Each allocation is respected in RANGE -- a derived count, so
  // 30.8 §11's rule applies and the direction matters: an
  // understated count licenses over-admission.
  property p_allocations_in_range;
    @(posedge clk) disable iff (!rst_n)
      (t_credits_used <= CREDITS_T) && (l_credits_used <= CREDITS_L);
  endproperty
  assert property (p_allocations_in_range)
    else $error("a population exceeded its allocation");

  // Underflow must be REPORTED, not absorbed. A drifting credit
  // counter invalidates every figure that depends on it, and
  // 30.8 §11 owns that an instrument which can report an impossible
  // value has never been checked.
  property p_underflow_is_reported;
    @(posedge clk) disable iff (!rst_n)
      ((t_done && t_credits_used == '0) || (l_done && l_credits_used == '0))
        |=> credit_underflow;
  endproperty
  assert property (p_underflow_is_reported)
    else $error("a completion with no outstanding credit was absorbed silently");

  // The PLATFORM invariant, with the parameter in the ANTECEDENT and
  // not inside the claim -- 31.1 §14's test. It may be shared across
  // both configurations.
  property p_single_population_never_admits_l;
    @(posedge clk) disable iff (!rst_n)
      (NUM_POP == 1) -> !l_admit;
  endproperty
  assert property (p_single_population_never_admits_l)
    else $error("a single-population platform admitted a second population");

  // And the two-sided bound: a partition must not be so small that L
  // serialises on admission as well as on latency. §6 part 2's
  // "present in the source, absent in the silicon" -- a partition
  // that cannot hold the chain depth is a partition in name only.
  property p_l_allocation_covers_chain;
    @(posedge clk) disable iff (!rst_n)
      (l_outstanding > 0) |-> (CREDITS_L >= l_outstanding);
  endproperty
  assert property (p_l_allocation_covers_chain)
    else $error("L's allocation is smaller than its observed chain depth");

  // ---- Covers for the partitioned admission block. Every other
  //      assertion set in this module has them, and without them
  //      these properties are statements about whichever arm ran.
  // T saturated while L is admitted: the outcome §13's block cannot
  // produce, and the single most valuable cover in the chapter.
  cover property (@(posedge clk) disable iff (!rst_n)
                  t_exhausted && l_admit);
  // The single-population arm, per 31.1 §14's configuration rule.
  cover property (@(posedge clk) disable iff (!rst_n)
                  (NUM_POP == 1) && t_admit);
  // Both allocations simultaneously at their limits -- the only
  // state in which the partition's sizing is fully exercised.
  cover property (@(posedge clk) disable iff (!rst_n)
                  t_exhausted && l_exhausted);

   the condition (31.4 §4):     N_L  >=  ceil( L / S )

   the MEMORY team's lever:  reduce L
       bounded below by the DRAM itself -- the thirteen obligations
       of 31.1 §5 do not go away, and 23.1 §7 owns which latency
       components are IRREDUCIBLE.

   the UPSTREAM team's lever:  raise N_L
       bounded by the dependency chain's structure, which is a
       software and dispatch-architecture property.

   tuning 2 (§4) took L from 200 to 120 cycles -- a 40% reduction,
   and it cost population T 23% of its throughput.

   the effect on the condition:
       N* before = ceil(200/4) = 50
       N* after  = ceil(120/4) = 30

   and L's position:
       N_L = 2.   2/50 = 0.04   ->   2/30 = 0.067

   DERIVED: the memory team's most aggressive available tuning moves
   L from 4% of the requirement to 6.7% of it. L still cannot hide
   any latency at all, and T paid 23% of its throughput for that.