Credit Updates — A Total, Delivered Twice, Counted Once

TLP arrives
  → occupies the receiver's buffer                  ← credit is "spent"
  → moved into internal processing / storage
  → THE BUFFER IS NOW REUSABLE                      ← the freeing event
  → cumulative freed total advances
  → an UpdateFC eventually carries the new total
  → the transmitter differences it into live credit

transmitter:   returned = new_total − last_total   (modulo)
               available += returned
               last_total = new_total

last_total = 14
new_total  =  2
 
modular difference = (2 − 14) mod 16 = 4

step             1     2     3     4     5     6     7     8
rx_free          1     1     0     1     0     0     1     0
rx_free_count    2     3     -     4     -     -     2     -
rx_total        14     1     1     5     5     5     7     7
dirty            1     1     1     1     1     0     1     1
 
update_valid     0     1     1     1     1     1     0     1
update_ready     0     0     0     1     0     1     0     0
update_total     -    14    14    14     5     5     -     7
 
tx_last          0     0     0     0    14    14    14     5
returned_delta   -     -     -    14     -     7     -     -
tx_available     8     8     8     8     8     8     8     8

// SYNTHESIZABLE. Receiver-side cumulative freed-credit accounting.
// That the receiver reports progress as the RECEIVER EMPTIES ITS BUFFERS,
// via UpdateFC, is NORMATIVE (section 1). That the value is a CUMULATIVE
// TOTAL modulo a fixed field width is at the tier section 1 assigns it --
// hence COUNTER_W is a parameter. The dirty-bit scheduling and the error
// reports are ILLUSTRATIVE IMPLEMENTATION POLICY.
module fc_return_counter #(
  parameter int POOLS     = 6,
  // GUARDED INDEX WIDTH. $clog2(1) is zero and a zero-width port cannot
  // index anything -- the corner Chapter 15.2 was fixed for.
  parameter int POOL_W    = (POOLS <= 1) ? 1 : $clog2(POOLS),
  // The PROTOCOL counter width. Deliberately not hardcoded (section 1).
  parameter int COUNTER_W = 12
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Initialisation, from InitFC (section 1) ---------------------------
  // Normalized: this module does not implement the InitFC1/InitFC2 state
  // machine, it takes the resulting starting total.
  input  logic                  init_valid,
  input  logic [POOL_W-1:0]     init_pool,
  input  logic [COUNTER_W-1:0]  init_total,
 
  // ---- The FREEING EVENT, from the receiver's internal machinery ---------
  // Asserted when buffer capacity becomes REUSABLE -- not when the packet
  // arrived, and not when the transaction completed (section 3).
  input  logic                  free_valid,
  input  logic [POOL_W-1:0]     free_pool,
  input  logic [COUNTER_W-1:0]  free_count,
 
  // ---- To the update scheduler -------------------------------------------
  output logic [COUNTER_W-1:0]  total    [POOLS],
  output logic [POOLS-1:0]      dirty,
  // Asserted by the scheduler when an update for this pool has been taken.
  input  logic                  sent_valid,
  input  logic [POOL_W-1:0]     sent_pool,
  input  logic [COUNTER_W-1:0]  sent_total,
 
  output logic                  free_pool_error
);
 
  generate
    if (POOLS < 1)  $error("POOLS must be at least 1");
    if (POOL_W < 1) $error("POOL_W must be at least 1");
    if ((POOLS > 1) && ((1 << POOL_W) < POOLS))
      $error("POOL_W too narrow to index POOLS");
    if (COUNTER_W < 2) $error("COUNTER_W must be at least 2");
  endgenerate
 
  logic [COUNTER_W-1:0] total_q [POOLS];
  logic [POOLS-1:0]     dirty_q;
  logic                 err_q;
 
  assign total           = total_q;
  assign dirty           = dirty_q;
  assign free_pool_error = err_q;
 
  // RANGE SAFETY. A POOL_W-wide index can express values >= POOLS whenever
  // POOLS is not a power of two. Checked one bit wider, BEFORE any access.
  localparam int CHK = POOL_W + 1;
  wire free_legal = (CHK'(free_pool) < CHK'(POOLS));
  wire init_legal = (CHK'(init_pool) < CHK'(POOLS));
  wire sent_legal = (CHK'(sent_pool) < CHK'(POOLS));
 
  wire do_free = free_valid && free_legal;
  wire do_sent = sent_valid && sent_legal;
 
  // The total AFTER this cycle's free, for the pool being freed. Computed
  // once so the dirty logic and the counter update cannot disagree.
  wire [COUNTER_W-1:0] free_next =
        do_free ? (total_q[free_pool] + free_count) : '0;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < POOLS; i++) total_q[i] <= '0;
      dirty_q <= '0;
      err_q   <= 1'b0;
    end else begin
      if (init_valid && init_legal) begin
        total_q[init_pool] <= init_total;
        dirty_q[init_pool] <= 1'b0;
      end
 
      // MODULAR BY CONSTRUCTION. Fixed-width unsigned addition wraps at
      // 2**COUNTER_W, which IS the protocol modulus. Never widen this.
      if (do_free) begin
        total_q[free_pool] <= free_next;
        dirty_q[free_pool] <= 1'b1;
      end
 
      // ================================================================
      // THE DIRTY-CLEAR RACE (section 9).
      //
      // Clearing dirty[sent_pool] unconditionally on the handshake LOSES
      // any freeing that happened in the SAME cycle: the update carried
      // the OLD total, the counter has already advanced past it, and the
      // pool is now marked clean with unadvertised progress in it.
      //
      // The condition is not "was this pool sent" but "does the total the
      // update carried still match the total we now hold". Written as an
      // explicit comparison so the same-cycle case falls out rather than
      // needing to be special-cased.
      // ================================================================
      if (do_sent) begin
        automatic logic [COUNTER_W-1:0] now =
          (do_free && (free_pool == sent_pool)) ? free_next
                                                : total_q[sent_pool];
        if (sent_total == now) dirty_q[sent_pool] <= 1'b0;
        // else: the pool STAYS dirty -- there is newer progress to advertise
      end
 
      if (free_valid && !free_legal) err_q <= 1'b1;
    end
  end
 
endmodule

// SYNTHESIZABLE. Select one dirty pool and offer a normalized FC update
// descriptor.
// That updates are scheduled periodically per non-infinite pool is
// NORMATIVE (section 1: every 32 microseconds, or 120 with Extended
// Synch). The SELECTION POLICY and the immutability contract below are
// ILLUSTRATIVE IMPLEMENTATION POLICY -- section 1's sources state the
// timing, not the arbitration.
module fc_update_scheduler #(
  parameter int POOLS     = 6,
  parameter int POOL_W    = (POOLS <= 1) ? 1 : $clog2(POOLS),
  parameter int COUNTER_W = 12
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic [COUNTER_W-1:0]  total [POOLS],
  input  logic [POOLS-1:0]      dirty,
  // Pools advertised as infinite are never scheduled (section 1).
  input  logic [POOLS-1:0]      pool_infinite,
 
  // ---- Normalized update descriptor out ----------------------------------
  // Chapter 15.1 owns the DLLP encoding; this is the boundary above it.
  output logic                  upd_valid,
  input  logic                  upd_ready,
  output logic [POOL_W-1:0]     upd_pool,
  output logic [COUNTER_W-1:0]  upd_total,
 
  // ---- Back to the return counter ----------------------------------------
  output logic                  sent_valid,
  output logic [POOL_W-1:0]     sent_pool,
  output logic [COUNTER_W-1:0]  sent_total
);
 
  logic                 v_q;
  logic [POOL_W-1:0]    pool_q;
  logic [COUNTER_W-1:0] total_q;
 
  assign upd_valid = v_q;
  assign upd_pool  = pool_q;
  assign upd_total = total_q;
 
  wire fire = v_q && upd_ready;
 
  // The descriptor is reported as SENT on the handshake, carrying the
  // total it actually contained -- which is what lets the return counter
  // decide whether the pool is still dirty (section 7).
  assign sent_valid = fire;
  assign sent_pool  = pool_q;
  assign sent_total = total_q;
 
  wire [POOLS-1:0] eligible = dirty & ~pool_infinite;
 
  // Lowest-index dirty pool. A FIXED PRIORITY, stated as such: section 1's
  // sources give the update TIMING, not the arbitration, so nothing here
  // claims round-robin is mandated. A production scheduler would rotate;
  // the liveness argument in section 13 assumes fairness explicitly.
  logic            any_eligible;
  logic [POOL_W-1:0] sel;
  always_comb begin
    any_eligible = 1'b0;
    sel          = '0;
    for (int p = POOLS-1; p >= 0; p--)
      if (eligible[p]) begin
        any_eligible = 1'b1;
        sel          = POOL_W'(p);
      end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_q <= 1'b0; pool_q <= '0; total_q <= '0;
    end else begin
      // ================================================================
      // IMMUTABILITY CONTRACT: once offered, a descriptor does not change
      // until it is taken.
      //
      // The alternative -- refreshing the offered total as new capacity is
      // freed, the way Chapter 15.3's ACK coalescer refreshes its frontier
      // -- is tempting and is NOT done here. The reason is that the return
      // counter's dirty logic is written against "the total this update
      // carried", and a descriptor that mutates under it would make that
      // comparison meaningless.
      //
      // Nothing is lost: new frees keep the pool DIRTY, so they are
      // advertised by the next update (section 7).
      // ================================================================
      if (!v_q && any_eligible) begin
        v_q     <= 1'b1;
        pool_q  <= sel;
        total_q <= total[sel];
      end else if (fire) begin
        v_q <= 1'b0;
      end
    end
  end
 
endmodule

// WRONG. Two independent updates that are correct in isolation.
if (update_fire)
  dirty_q[sel] <= 1'b0;
 
if (free_fire)
  total_q[free_pool] <= total_q[free_pool] + free_count;

// SYNTHESIZABLE. Convert a received cumulative FC total into newly
// returned credit, exactly once.
// That the value is a cumulative total and the difference is modular is
// the mechanism of section 4, at the tier section 1 assigns it. The
// plausibility bounds and the rejection policy are ILLUSTRATIVE LOCAL
// POLICY (section 5).
module fc_return_integrate #(
  parameter int POOLS     = 6,
  parameter int POOL_W    = (POOLS <= 1) ? 1 : $clog2(POOLS),
  parameter int COUNTER_W = 12,
  parameter int CRED_W    = 12
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- Initialised baseline and capacity, per pool -----------------------
  input  logic                  init_valid,
  input  logic [POOL_W-1:0]     init_pool,
  input  logic [COUNTER_W-1:0]  init_total,
  input  logic [CRED_W-1:0]     init_capacity,
 
  // ---- Decoded update, from Chapter 15.2 ----------------------------------
  input  logic                  upd_valid,
  output logic                  upd_ready,
  input  logic [POOL_W-1:0]     upd_pool,
  input  logic [COUNTER_W-1:0]  upd_total,
 
  // ---- How much is currently outstanding, from Chapter 16.5 --------------
  // Sent but not yet returned. The TIGHTER plausibility bound (section 5).
  input  logic [CRED_W-1:0]     outstanding [POOLS],
 
  // ---- Normalized return event, to Chapter 16.5's accounts ---------------
  output logic                  ret_valid,
  input  logic                  ret_ready,
  output logic [POOL_W-1:0]     ret_pool,
  output logic [CRED_W-1:0]     ret_count,
 
  output logic                  fc_update_error
);
 
  logic [COUNTER_W-1:0] last_q  [POOLS];
  logic [CRED_W-1:0]    cap_q   [POOLS];
  logic [POOLS-1:0]     init_q;
  logic                 err_q;
 
  localparam int CHK = POOL_W + 1;
  wire upd_legal  = (CHK'(upd_pool)  < CHK'(POOLS));
  wire init_legal = (CHK'(init_pool) < CHK'(POOLS));
 
  logic [COUNTER_W-1:0] last_sel;
  logic [CRED_W-1:0]    cap_sel, out_sel;
  logic                 init_sel;
  always_comb begin
    last_sel = '0; cap_sel = '0; out_sel = '0; init_sel = 1'b0;
    if (upd_legal) begin
      last_sel = last_q[upd_pool];
      cap_sel  = cap_q[upd_pool];
      out_sel  = outstanding[upd_pool];
      init_sel = init_q[upd_pool];
    end
  end
 
  // ================================================================
  // THE MODULAR DIFFERENCE.
  //
  // Fixed-width unsigned subtraction IS modular subtraction. There is no
  // modulo operator here and there must not be: a `%` invites a widened
  // intermediate, and a widened intermediate is no longer modular
  // (section 5, and Chapter 14.5 section 6).
  //
  // A DUPLICATE update gives upd_total == last_sel, so returned == 0 and
  // nothing is added. That is the whole de-duplication mechanism.
  // ================================================================
  wire [COUNTER_W-1:0] returned = upd_total - last_sel;
 
  // PLAUSIBILITY, two bounds, both local (section 5).
  //   - a receiver cannot free more than its buffer holds
  //   - a transmitter cannot be owed more than it has outstanding
  // Compared at COUNTER_W so a large modular difference cannot be
  // truncated into a small plausible one.
  wire [COUNTER_W-1:0] cap_x = COUNTER_W'(cap_sel);
  wire [COUNTER_W-1:0] out_x = COUNTER_W'(out_sel);
  wire plausible = init_sel && (returned <= cap_x) && (returned <= out_x);
 
  // ---- Output holding stage ----------------------------------------------
  logic              ret_v_q;
  logic [POOL_W-1:0] ret_p_q;
  logic [CRED_W-1:0] ret_c_q;
 
  wire ret_fire = ret_v_q && ret_ready;
  assign upd_ready = !ret_v_q || ret_ready;
  assign ret_valid = ret_v_q;
  assign ret_pool  = ret_p_q;
  assign ret_count = ret_c_q;
  assign fc_update_error = err_q;
 
  wire accept = upd_valid && upd_ready && upd_legal && plausible;
  // A zero difference is a legitimate no-op -- a duplicate update. It is
  // ACCEPTED (the baseline is already correct) and emits NO event.
  wire emit   = accept && (returned != '0);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < POOLS; i++) begin
        last_q[i] <= '0; cap_q[i] <= '0;
      end
      init_q <= '0; ret_v_q <= 1'b0; ret_p_q <= '0; ret_c_q <= '0;
      err_q  <= 1'b0;
    end else begin
      if (init_valid && init_legal && !init_q[init_pool]) begin
        last_q[init_pool] <= init_total;
        cap_q[init_pool]  <= init_capacity;
        init_q[init_pool] <= 1'b1;
      end
 
      // ============================================================
      // THE BASELINE ADVANCES ONLY ON AN ACCEPTED UPDATE.
      //
      // Advancing it on a REJECTED one would measure the next difference
      // from a total the sender never sent -- silently losing every
      // credit between the rejected value and the next one, permanently.
      // ============================================================
      if (accept) last_q[upd_pool] <= upd_total;
 
      // Emit has priority over drain, so a same-cycle accept-and-consume
      // holds the new event rather than dropping it.
      if (emit) begin
        ret_v_q <= 1'b1;
        ret_p_q <= upd_pool;
        ret_c_q <= CRED_W'(returned);
      end else if (ret_fire) begin
        ret_v_q <= 1'b0;
      end
 
      if (upd_valid && !upd_legal)                        err_q <= 1'b1;
      if (upd_valid &&  upd_legal && !plausible)          err_q <= 1'b1;
    end
  end
 
endmodule

// SVA over fc_return_counter, fc_update_scheduler and
// fc_return_integrate. These assert the LOCAL accounting contract and the
// declared scheduling policy. Liveness appears only with an explicit
// fairness assumption (P17).
 
// ---- ENVIRONMENT ------------------------------------------------------
// A1: free_valid means buffer capacity became REUSABLE (section 3) --
// not that a packet arrived, and not that a transaction completed.
assume property (@(posedge clk) disable iff (!rst_n)
  free_valid |-> (free_count != '0));
// A2: the update descriptor is stable while offered (section 8).
assume property (@(posedge clk) disable iff (!rst_n)
  (upd_valid && !upd_ready) |=> ($stable(upd_pool) && $stable(upd_total)));
 
// ---- RECEIVER SIDE ----------------------------------------------------
 
// P1: a free advances ONLY the selected pool.
generate for (genvar p = 0; p < POOLS; p++) begin : g_iso
  property p_only_selected_pool;
    @(posedge clk) disable iff (!rst_n)
    (do_free && (free_pool != POOL_W'(p))) |=> $stable(total_q[p]);
  endproperty
  a_pool_iso : assert property (p_only_selected_pool);
end endgenerate
 
// P2: RANGE SAFETY -- an out-of-range pool index touches nothing.
property p_no_oob_access;
  @(posedge clk) disable iff (!rst_n)
  (free_valid && !free_legal) |=> (free_pool_error && $stable(total_q));
endproperty
a_oob : assert property (p_no_oob_access);
 
// P3: the cumulative total wraps EXACTLY at the declared modulus. An
// independent restatement, so a widened intermediate fails.
property p_wraps_at_modulus;
  @(posedge clk) disable iff (!rst_n)
  do_free |=> (total_q[$past(free_pool)]
               == COUNTER_W'(($past(total_q[$past(free_pool)])
                            + $past(free_count))));
endproperty
a_wrap : assert property (p_wraps_at_modulus);
 
// P4: dirty is SET whenever unadvertised progress exists.
property p_dirty_when_unadvertised;
  @(posedge clk) disable iff (!rst_n)
  do_free |=> dirty_q[$past(free_pool)];
endproperty
a_dirty_set : assert property (p_dirty_when_unadvertised);
 
// P5: THE RACE PROPERTY (section 9). An update handshake clears dirty ONLY
// if no newer progress remains. Same-cycle free on the same pool must
// leave the pool dirty.
property p_dirty_survives_same_cycle_free;
  @(posedge clk) disable iff (!rst_n)
  (do_sent && do_free && (free_pool == sent_pool))
    |=> dirty_q[$past(sent_pool)];
endproperty
a_race : assert property (p_dirty_survives_same_cycle_free);
 
// P5b: and the general form -- dirty clears only on an exact match.
property p_dirty_clears_only_on_match;
  @(posedge clk) disable iff (!rst_n)
  (do_sent && (sent_total != total_q[sent_pool]))
    |=> dirty_q[$past(sent_pool)];
endproperty
a_dirty_match : assert property (p_dirty_clears_only_on_match);
 
// ---- SCHEDULER --------------------------------------------------------
 
// P6: an offered descriptor is IMMUTABLE until taken (section 8).
property p_descriptor_stable;
  @(posedge clk) disable iff (!rst_n)
  (upd_valid && !upd_ready) |=> (upd_valid && $stable(upd_pool)
                                           && $stable(upd_total));
endproperty
a_stable : assert property (p_descriptor_stable);
 
// P7: an infinite pool is never scheduled (section 1).
property p_infinite_not_scheduled;
  @(posedge clk) disable iff (!rst_n)
  upd_valid |-> !pool_infinite[upd_pool];
endproperty
a_infinite : assert property (p_infinite_not_scheduled);
 
// P8: sent_valid asserts on the HANDSHAKE, not on the offer.
property p_sent_on_fire;
  @(posedge clk) disable iff (!rst_n)
  sent_valid |-> (upd_valid && upd_ready);
endproperty
a_sent : assert property (p_sent_on_fire);
 
// ---- TRANSMITTER SIDE -------------------------------------------------
 
// P9: A DUPLICATE UPDATE DERIVES ZERO NEW CREDIT. The property a design
// that adds the total outright fails on the first repeat.
property p_duplicate_returns_zero;
  @(posedge clk) disable iff (!rst_n)
  (upd_valid && upd_legal && (upd_total == last_sel)) |-> !emit;
endproperty
a_duplicate : assert property (p_duplicate_returns_zero);
 
// P10: the returned amount equals an INDEPENDENT modular reference.
// Restated, so a widened or signed implementation fails rather than
// agreeing with itself.
property p_delta_matches_reference;
  @(posedge clk) disable iff (!rst_n)
  (upd_valid && upd_legal)
    |-> (returned == COUNTER_W'(upd_total - last_sel));
endproperty
a_delta : assert property (p_delta_matches_reference);
 
// P11: AN ACCEPTED UPDATE ADVANCES THE BASELINE EXACTLY ONCE.
property p_baseline_once;
  @(posedge clk) disable iff (!rst_n)
  accept |=> (last_q[$past(upd_pool)] == $past(upd_total));
endproperty
a_baseline : assert property (p_baseline_once);
 
// P12: A REJECTED UPDATE CANNOT CORRUPT THE BASELINE. Advancing it on a
// rejected value loses every credit up to the next one, permanently.
property p_rejected_leaves_baseline;
  @(posedge clk) disable iff (!rst_n)
  (upd_valid && upd_legal && !plausible) |=> $stable(last_q[$past(upd_pool)]);
endproperty
a_reject : assert property (p_rejected_leaves_baseline);
 
// P13: newly returned credit is added EXACTLY ONCE. Ghost counters are
// testbench state -- a VERIFICATION ACCOUNTING IDENTITY, not wire state.
property p_returned_once;
  @(posedge clk) disable iff (!rst_n)
  (ret_valid && ret_ready)
    |=> (g_credit_added == $past(g_credit_added) + $past(ret_count));
endproperty
a_once : assert property (p_returned_once);
 
// P14: NO CREDIT APPEARS WITHOUT A RECEIVER FREE OR AN INITIALISATION.
// Bound across the Link in a two-port testbench: the total credit the
// transmitter has been given never exceeds what the receiver has freed.
property p_no_spontaneous_credit;
  @(posedge clk) disable iff (!rst_n)
  (g_credit_added <= (g_rx_freed + g_initial_advertised));
endproperty
a_no_magic : assert property (p_no_spontaneous_credit);
 
// P15: a decoded return event is not lost under backpressure.
property p_event_not_lost;
  @(posedge clk) disable iff (!rst_n)
  (ret_valid && !ret_ready) |=> (ret_valid && $stable(ret_count)
                                           && $stable(ret_pool));
endproperty
a_no_loss : assert property (p_event_not_lost);
 
// ---- CROSS-MECHANISM NON-INTERFERENCE ---------------------------------
 
// P16: AN ACK CANNOT MOVE THE FC BASELINE. Three feedback loops, three
// mechanisms (section 16).
property p_ack_does_not_touch_fc;
  @(posedge clk) disable iff (!rst_n)
  (dut_retire_window.retire_valid && !upd_valid) |=> $stable(last_q);
endproperty
a_ack : assert property (p_ack_does_not_touch_fc);
 
// P16b: nor does a Completion arrival return FC credit.
property p_completion_returns_no_credit;
  @(posedge clk) disable iff (!rst_n)
  (dut_cpl_arrives && !upd_valid) |=> !ret_valid;
endproperty
a_cpl : assert property (p_completion_returns_no_credit);
 
// P16c: an FC update never alters replay state.
property p_fc_does_not_touch_replay;
  @(posedge clk) disable iff (!rst_n)
  (upd_valid && upd_ready) |=> $stable(dut_replay_buffer.occupancy);
endproperty
a_replay : assert property (p_fc_does_not_touch_replay);
 
// ---- LIVENESS, WITH ITS ASSUMPTION STATED -----------------------------
 
// F1: FAIRNESS ASSUMPTION. The scheduler eventually selects any dirty
// pool, and the transport eventually accepts. This is an ASSUMPTION about
// the environment and the arbiter, not a property of this design.
assume property (@(posedge clk) disable iff (!rst_n)
  s_eventually upd_ready);
 
// P17: given F1, unadvertised progress is eventually advertised. Stated
// only because its assumption is stated.
property p_dirty_eventually_clears;
  @(posedge clk) disable iff (!rst_n)
  dirty_q[0] |-> s_eventually (!dirty_q[0]);
endproperty
a_liveness : assert property (p_dirty_eventually_clears);

// VERIFICATION-ONLY. Independent models for both ends.
// Deliberately different in structure from the RTL: the receiver model
// counts up in a loop and the transmitter model masks explicitly, so a
// shared arithmetic bug cannot hide in both.
class fc_ref;
  int unsigned modulus;                        // 2**COUNTER_W
  int unsigned rx_total[6];                    // receiver cumulative
  int unsigned tx_baseline[6];                 // transmitter baseline
  int unsigned tx_added[6];                    // cumulative credit added
 
  function void rx_free(int pool, int count);
    for (int i = 0; i < count; i++)            // counted, not added
      rx_total[pool] = (rx_total[pool] + 1) % modulus;
  endfunction
 
  function int tx_apply(int pool, int unsigned total);
    int unsigned delta;
    delta = (total + modulus - tx_baseline[pool]) % modulus;  // explicit
    tx_baseline[pool] = total;
    tx_added[pool] += delta;
    return delta;                              // duplicate yields 0
  endfunction
endclass