LPDDR5 Architecture

   17.1 GB/s x 8 bits/byte / 16 pins  =  8.550 Gbps per pin
   data is transferred on both WCK edges
   ->  WCK  =  8550 / 2  =  4275 MHz

// ---------------------------------------------------------------------
// wck_ck_domain_manager -- tracks the configurable integer ratio
// between the data clock and the command clock, and checks that a
// command's reference to a data beat is meaningful.
//
// CLASSIFICATION: educational, synthesisable.
//
// THIS IS THE MACHINERY 4.7 §3 DEFERRED TO MODULE 24.
//
// WHAT IT DOES NOT MODEL:
//   - either clock, any PLL, phase detection or clock generation.
//     19.1 §5 classifies those as outside portable RTL.
//   - jitter, skew, or any electrical property of the crossing
//   - a genuine asynchronous crossing. The block lives in the CK
//     domain with a WCK tick input (§12's header says so), because a
//     real synchroniser discipline would bury the ratio arithmetic
//     this chapter exists to show.
//
// WHY THE RATIO IS AN INPUT AND NOT A PARAMETER: §3. It is
// DEVICE-VERIFIED as selectable (2:1 or 4:1), so a design that fixed
// it at elaboration would have hard-coded a mode-register setting.
// ---------------------------------------------------------------------
module wck_ck_domain_manager #(
  // The largest supported ratio. Sets the counter WIDTH; the MODULUS
  // is a runtime value, which is the whole difficulty of §3.
  parameter int MAX_RATIO = 4,
  parameter int PH_W      = $clog2(MAX_RATIO),        // an INDEX into MAX_RATIO
  parameter int RCNT_W    = $clog2(MAX_RATIO + 1),    // a COUNT up to MAX_RATIO
  parameter int BEAT_W    = 6,
  parameter int CNT_W     = 24
) (
  input  logic                clk,            // CK domain
  input  logic                rst_n,

  // ── Configuration. DEVICE-VERIFIED as selectable, so an input.
  input  logic                cfg_valid,
  input  logic [RCNT_W-1:0]   cfg_ratio,      // 2 or 4

  // ── A WCK edge occurred. In a real design this arrives already
  //    synchronised; here it is simply an input (§12's header).
  input  logic                wck_tick,

  // ── A command that references a data beat.
  input  logic                cmd_valid,
  input  logic [BEAT_W-1:0]   cmd_beat_offset,
  input  logic [BEAT_W-1:0]   cmd_burst_beats,   // 16 or 32 (§6)

  // ── Phase state.
  output logic [PH_W-1:0]     wck_phase,
  output logic                phase_aligned,     // at phase 0
  output logic [RCNT_W-1:0]   ratio_in_force,
  output logic                ratio_valid,

  // ── Crossing verdict.
  output logic                crossing_legal,
  output logic [CNT_W-1:0]    cnt_crossings_ok,
  output logic [CNT_W-1:0]    cnt_crossings_bad,

  // §4's arithmetic, as an output rather than a comment: how many
  // data beats accompany one command slot at the ratio in force.
  output logic [RCNT_W:0]     beats_per_cmd_slot,

  // ── Errors, reported by kind.
  output logic                err_ratio_unsupported,
  output logic                err_cmd_before_config,
  output logic                err_beat_out_of_burst,
  output logic                err_tick_without_ratio,
  output logic                any_error
);

  initial begin
    if (MAX_RATIO != 4)
      $fatal(1, "wck_ck_domain_manager: MAX_RATIO must be 4 (device-verified)");
    if (PH_W < 2)
      $fatal(1, "wck_ck_domain_manager: PH_W too narrow for MAX_RATIO");
  end

  logic [PH_W-1:0]   ph;
  logic [RCNT_W-1:0] ratio;
  logic              have_ratio;
  logic [CNT_W-1:0]  n_ok, n_bad;
  logic              e_rat, e_pre, e_beat, e_tick;

  // A ratio is supported only if it is one of the two verified
  // values. Declared above the assigns that read it.
  logic cfg_ok;
  assign cfg_ok = (cfg_ratio == RCNT_W'(2)) || (cfg_ratio == RCNT_W'(4));

  // §4: at 4:1 a command slot accompanies twice the data of 2:1. CK
  // is DDR for commands (§5), so a CK period holds two slots and the
  // beats per slot is the ratio itself.
  logic [RCNT_W:0] bps;
  assign bps = have_ratio ? (RCNT_W+1)'(ratio) : '0;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      ph <= '0; ratio <= '0; have_ratio <= 1'b0;
      n_ok <= '0; n_bad <= '0;
      e_rat <= 1'b0; e_pre <= 1'b0; e_beat <= 1'b0; e_tick <= 1'b0;
    end else begin
      e_rat <= 1'b0; e_pre <= 1'b0; e_beat <= 1'b0; e_tick <= 1'b0;

      // ── Configuration.
      if (cfg_valid) begin
        if (!cfg_ok) begin
          // An unsupported ratio is REJECTED, not clamped. Clamping
          // would leave the controller believing a ratio is in force
          // that is not, and every crossing after that would be
          // computed against the wrong modulus.
          e_rat <= 1'b1;
        end else begin
          ratio      <= cfg_ratio;
          have_ratio <= 1'b1;
          // The phase resets on a ratio change: the modulus changed,
          // so a phase counted against the old one is meaningless.
          ph         <= '0;
        end
      end

      // ── Phase tracking. The MODULUS is a runtime value, which is
      //    §3's callout in one line of arithmetic.
      if (wck_tick) begin
        if (!have_ratio) begin
          e_tick <= 1'b1;
        end else if (ph == PH_W'(ratio - RCNT_W'(1))) begin
          ph <= '0;
        end else begin
          ph <= ph + PH_W'(1);
        end
      end

      // ── Crossing check.
      if (cmd_valid) begin
        if (!have_ratio) begin
          e_pre <= 1'b1;
          if (n_bad != {CNT_W{1'b1}}) n_bad <= n_bad + CNT_W'(1);
        end else if (cmd_beat_offset >= cmd_burst_beats) begin
          // §3's callout, second item: a beat offset must name a beat
          // that exists within the burst. The burst length is itself
          // configurable (§6), so this bound is a runtime value too.
          e_beat <= 1'b1;
          if (n_bad != {CNT_W{1'b1}}) n_bad <= n_bad + CNT_W'(1);
        end else begin
          if (n_ok != {CNT_W{1'b1}}) n_ok <= n_ok + CNT_W'(1);
        end
      end
    end
  end

  assign wck_phase      = ph;
  assign phase_aligned  = (ph == '0);
  assign ratio_in_force = ratio;
  assign ratio_valid    = have_ratio;
  // Computed combinationally from the CURRENT inputs, not from the
  // registered error flags -- a caller needs the verdict in the same
  // cycle it presents the command.
  assign crossing_legal = cmd_valid && have_ratio &&
                          (cmd_beat_offset < cmd_burst_beats);
  assign cnt_crossings_ok  = n_ok;
  assign cnt_crossings_bad = n_bad;
  assign beats_per_cmd_slot = bps;
  assign err_ratio_unsupported  = e_rat;
  assign err_cmd_before_config  = e_pre;
  assign err_beat_out_of_burst  = e_beat;
  assign err_tick_without_ratio = e_tick;
  assign any_error = e_rat | e_pre | e_beat | e_tick;
endmodule

end else if (ph == PH_W'(ratio - RCNT_W'(1))) begin
  ph <= '0;

// ---------------------------------------------------------------------
// lp5_burst_selector -- runs the same request stream against BOTH
// burst lengths and reports what each would have moved.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHY BOTH AT ONCE: §7's callout. BL32 is set once and applies to
// every access including the small ones, so the decision needs the
// access-size DISTRIBUTION rather than a peak-bandwidth benchmark.
// This block measures both arms against one stream, which is the
// counterfactual form 23.5's policy work uses.
//
// WHAT IT DOES NOT MODEL: energy, bandwidth in bytes per second, or
// command overhead in cycles. So it CANNOT say which is better -- the
// weighting between payload waste and command overhead is not in this
// chapter, and it reports the comparison instead of the verdict.
// ---------------------------------------------------------------------
module lp5_burst_selector #(
  // DEVICE-VERIFIED granules for a x16 channel (§6).
  parameter int GRAN16 = 32,
  parameter int GRAN32 = 64,
  parameter int SH16   = $clog2(GRAN16),
  parameter int SH32   = $clog2(GRAN32),
  parameter int REQ_W  = 16,
  parameter int ACC_W  = 40
) (
  input  logic              clk,
  input  logic              rst_n,

  input  logic              req_valid,
  input  logic [REQ_W-1:0]  req_bytes,

  // ── Both arms, over the same stream.
  output logic [ACC_W-1:0]  requested,
  output logic [ACC_W-1:0]  moved_bl16,
  output logic [ACC_W-1:0]  moved_bl32,
  output logic [ACC_W-1:0]  bursts_bl16,
  output logic [ACC_W-1:0]  bursts_bl32,

  // The difference, both ways, as a PAIR. BL32 always moves at least
  // as much data and always issues no more bursts, so the trade is
  // exactly these two numbers and never a single score.
  output logic [ACC_W-1:0]  extra_bytes_bl32,
  output logic [ACC_W-1:0]  fewer_bursts_bl32,

  // Distribution, which §7's callout says is what should decide.
  output logic [ACC_W-1:0]  cnt_le_32,
  output logic [ACC_W-1:0]  cnt_33_to_64,
  output logic [ACC_W-1:0]  cnt_gt_64,

  output logic              err_zero_length_req,
  output logic              any_saturated
);

  initial begin
    if (GRAN32 != 2 * GRAN16)
      $fatal(1, "lp5_burst_selector: GRAN32 must be twice GRAN16 (device-verified)");
    if (GRAN16 < 2 || (GRAN16 & (GRAN16 - 1)) != 0)
      // The power-of-two test alone ACCEPTS 0 and 1: both give
      // (g & (g-1)) == 0. Either would make $clog2 zero and the
      // round-up shift a no-op, so the lower bound is required and
      // not decorative. 24.3's accountant guards it the same way.
      $fatal(1, "lp5_burst_selector: GRAN16 must be a power of two >= 2");
  end

  logic [ACC_W-1:0] t_req, m16, m32, b16, b32, c_s, c_m, c_l;
  logic             e_zero, sat;

  // Round up by shifting -- no divide. Declared above the assigns.
  logic [REQ_W+1:0] n16, n32;
  assign n16 = (req_bytes == '0) ? '0
             : (REQ_W+2)'(((req_bytes - REQ_W'(1)) >> SH16) + 1);
  assign n32 = (req_bytes == '0) ? '0
             : (REQ_W+2)'(((req_bytes - REQ_W'(1)) >> SH32) + 1);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      t_req <= '0; m16 <= '0; m32 <= '0; b16 <= '0; b32 <= '0;
      c_s <= '0; c_m <= '0; c_l <= '0;
      e_zero <= 1'b0; sat <= 1'b0;
    end else begin
      e_zero <= 1'b0;
      if (req_valid) begin
        if (req_bytes == '0) begin
          e_zero <= 1'b1;
        end else if (m32 > ({ACC_W{1'b1}} - ACC_W'(n32 << SH32))) begin
          sat <= 1'b1;
        end else begin
          t_req <= t_req + ACC_W'(req_bytes);
          m16   <= m16 + ACC_W'(n16 << SH16);
          m32   <= m32 + ACC_W'(n32 << SH32);
          b16   <= b16 + ACC_W'(n16);
          b32   <= b32 + ACC_W'(n32);
          if (req_bytes <= REQ_W'(GRAN16))
            c_s <= c_s + ACC_W'(1);
          else if (req_bytes <= REQ_W'(GRAN32))
            c_m <= c_m + ACC_W'(1);
          else
            c_l <= c_l + ACC_W'(1);
        end
      end
    end
  end

  assign requested   = t_req;
  assign moved_bl16  = m16;
  assign moved_bl32  = m32;
  assign bursts_bl16 = b16;
  assign bursts_bl32 = b32;
  // BL32 never moves less and never issues more bursts, so both
  // differences are non-negative by construction. P8 and P9 assert it.
  assign extra_bytes_bl32  = (m32 >= m16) ? (m32 - m16) : '0;
  assign fewer_bursts_bl32 = (b16 >= b32) ? (b16 - b32) : '0;
  assign cnt_le_32     = c_s;
  assign cnt_33_to_64  = c_m;
  assign cnt_gt_64     = c_l;
  assign err_zero_length_req = e_zero;
  assign any_saturated = sat;
endmodule

// ---------------------------------------------------------------------
// lp5_reconfig_guard -- a configurable architecture needs a protocol
// for changing configuration. This enforces its shape.
//
// CLASSIFICATION: educational, synthesisable.
//
// WHY IT EXISTS: §8. LPDDR5 has THREE configurable architecture
// dimensions, and every one of them changes arithmetic that in-flight
// work depends on -- §11's stack shows the ratio and the burst length
// both feeding the crossing layer. Changing one mid-flight does not
// produce a slightly wrong result; it produces a crossing computed
// against a modulus that no longer applies (§13).
//
// WHAT IT DOES NOT MODEL: any device's real reconfiguration sequence,
// its timing, or its mode-register encodings. It enforces the SHAPE:
// quiesce, change, resume.
// ---------------------------------------------------------------------
module lp5_reconfig_guard #(
  parameter int DIMS  = 3,          // ratio, burst length, bank org (§8)
  parameter int CNT_W = 20
) (
  input  logic              clk,
  input  logic              rst_n,

  // ── A request to change one dimension.
  input  logic              cfg_req,
  input  logic [DIMS-1:0]   cfg_dims,        // which dimensions change

  // ── Activity that must be absent before a change is permitted.
  input  logic              cmds_in_flight,
  input  logic              data_in_flight,
  input  logic              banks_open,

  // ── Verdict.
  output logic              cfg_grant,
  output logic              quiesced,
  output logic [CNT_W-1:0]  cnt_granted,
  output logic [CNT_W-1:0]  cnt_refused,

  // ── Refusals, by reason, so a controller learns WHAT to quiesce.
  output logic              err_cmds_in_flight,
  output logic              err_data_in_flight,
  output logic              err_banks_open,
  output logic              err_no_dim_selected,
  output logic              err_multi_dim_at_once,
  output logic              any_refusal
);

  initial begin
    if (DIMS < 1)
      $fatal(1, "lp5_reconfig_guard: DIMS must be at least 1");
  end

  logic [CNT_W-1:0] n_ok, n_no;
  logic             e_c, e_d, e_b, e_z, e_m, grant;

  // Declared above the assigns that read it.
  logic quiet;
  assign quiet = !cmds_in_flight && !data_in_flight && !banks_open;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_ok <= '0; n_no <= '0; grant <= 1'b0;
      e_c <= 1'b0; e_d <= 1'b0; e_b <= 1'b0; e_z <= 1'b0; e_m <= 1'b0;
    end else begin
      grant <= 1'b0;
      e_c <= 1'b0; e_d <= 1'b0; e_b <= 1'b0; e_z <= 1'b0; e_m <= 1'b0;

      if (cfg_req) begin
        // ── Every reason is reported, not just the first, so a
        //    controller that must quiesce three things learns all
        //    three in one attempt instead of three.
        if (cmds_in_flight) e_c <= 1'b1;
        if (data_in_flight) e_d <= 1'b1;
        if (banks_open)     e_b <= 1'b1;
        if (cfg_dims == '0) e_z <= 1'b1;
        // One dimension at a time. Two simultaneous changes make the
        // intermediate state ambiguous: there is no ordering in which
        // both old values and both new values are consistent.
        if (!$onehot0(cfg_dims)) e_m <= 1'b1;

        if (quiet && (cfg_dims != '0) && $onehot(cfg_dims)) begin
          grant <= 1'b1;
          if (n_ok != {CNT_W{1'b1}}) n_ok <= n_ok + CNT_W'(1);
        end else begin
          if (n_no != {CNT_W{1'b1}}) n_no <= n_no + CNT_W'(1);
        end
      end
    end
  end

  assign cfg_grant   = grant;
  assign quiesced    = quiet;
  assign cnt_granted = n_ok;
  assign cnt_refused = n_no;
  assign err_cmds_in_flight    = e_c;
  assign err_data_in_flight    = e_d;
  assign err_banks_open        = e_b;
  assign err_no_dim_selected   = e_z;
  assign err_multi_dim_at_once = e_m;
  assign any_refusal = e_c | e_d | e_b | e_z | e_m;
endmodule

// Bind unit note: P1-P7 reference wck_ck_domain_manager's internals,
// P8-P11 lp5_burst_selector's, P12-P15 lp5_reconfig_guard's.

// P1 -- the phase is always within the ratio in force. §13's first
// failure mode: a width-modulus counter violates this at 2:1.
property p_phase_within_ratio;
  @(posedge clk) disable iff (!rst_n)
    ratio_valid |-> (wck_phase < PH_W'(ratio_in_force));
endproperty
assert property (p_phase_within_ratio);

// P2 -- the phase advances by exactly one per WCK tick, or wraps to
// zero. Rules out a skipped or doubled phase.
property p_phase_advances_by_one;
  @(posedge clk) disable iff (!rst_n)
    ($past(wck_tick,1) && $past(ratio_valid,1) && !$past(cfg_valid,1))
      |-> ((wck_phase == $past(wck_phase,1) + PH_W'(1)) ||
           (wck_phase == '0));
endproperty
assert property (p_phase_advances_by_one);

// P3 -- §13's second failure mode. A ratio change RESETS the phase,
// because a phase counted against the old modulus is out of range for
// the new one and the wrap comparison would never match again.
property p_ratio_change_resets_phase;
  @(posedge clk) disable iff (!rst_n)
    ($past(cfg_valid,1) && !$past(err_ratio_unsupported,1) && ratio_valid)
      |-> (wck_phase == '0);
endproperty
assert property (p_ratio_change_resets_phase);

// P4 -- §13's third failure mode. An unsupported ratio is REJECTED,
// never clamped into force. Clamping would leave every subsequent
// crossing computed against the wrong modulus.
property p_bad_ratio_never_in_force;
  @(posedge clk) disable iff (!rst_n)
    ratio_valid |-> (ratio_in_force inside {RCNT_W'(2), RCNT_W'(4)});
endproperty
assert property (p_bad_ratio_never_in_force);

// P5 -- no crossing is judged legal before a ratio is configured.
// Without a ratio there is no relationship between the domains, so
// there is nothing to be legal with respect to.
property p_no_crossing_before_config;
  @(posedge clk) disable iff (!rst_n)
    !ratio_valid |-> !crossing_legal;
endproperty
assert property (p_no_crossing_before_config);

// P6 -- a beat offset outside the burst is never legal. §6: the
// burst length is itself configurable, so the bound is a runtime
// value and not a constant.
property p_beat_within_burst;
  @(posedge clk) disable iff (!rst_n)
    crossing_legal |-> (cmd_beat_offset < cmd_burst_beats);
endproperty
assert property (p_beat_within_burst);

// P7 -- §4's arithmetic, as an invariant: the beats accompanying one
// command slot equal the ratio in force.
property p_beats_per_slot_is_ratio;
  @(posedge clk) disable iff (!rst_n)
    ratio_valid |-> (beats_per_cmd_slot == (RCNT_W+1)'(ratio_in_force));
endproperty
assert property (p_beats_per_slot_is_ratio);

// P8 -- BL32 never moves LESS than BL16 over the same stream. The
// invariant that makes §14's subtraction safe.
property p_bl32_moves_at_least_bl16;
  @(posedge clk) disable iff (!rst_n) (moved_bl32 >= moved_bl16);
endproperty
assert property (p_bl32_moves_at_least_bl16);

// P9 -- BL32 never issues MORE bursts than BL16. The other half of
// §7's trade, and the reason the two differences are reported as a
// pair rather than combined into a score.
property p_bl32_issues_no_more_bursts;
  @(posedge clk) disable iff (!rst_n) (bursts_bl32 <= bursts_bl16);
endproperty
assert property (p_bl32_issues_no_more_bursts);

// P10 -- both arms move a whole number of their own granule.
property p_both_arms_whole_granules;
  @(posedge clk) disable iff (!rst_n)
    (((moved_bl16 & ACC_W'(GRAN16 - 1)) == '0) &&
     ((moved_bl32 & ACC_W'(GRAN32 - 1)) == '0));
endproperty
assert property (p_both_arms_whole_granules);

// P11 -- the three size buckets partition every counted request, so
// §7's distribution argument rests on an exhaustive classification.
property p_buckets_partition_requests;
  @(posedge clk) disable iff (!rst_n)
    (req_valid && (req_bytes != '0) && !any_saturated)
      |=> ((cnt_le_32 + cnt_33_to_64 + cnt_gt_64) ==
           ($past(cnt_le_32,1) + $past(cnt_33_to_64,1) +
            $past(cnt_gt_64,1) + ACC_W'(1)));
endproperty
assert property (p_buckets_partition_requests);

// P12 -- FORBIDDEN. Reconfiguration is never granted while anything
// depends on the old value. §15: the change does not produce a
// slightly wrong result, it produces one computed against a modulus
// that no longer applies.
property p_no_reconfig_while_busy;
  @(posedge clk) disable iff (!rst_n)
    (cmds_in_flight || data_in_flight || banks_open) |=> !cfg_grant;
endproperty
assert property (p_no_reconfig_while_busy);

// P13 -- FORBIDDEN. Two dimensions never change together, because no
// ordering makes both old and both new values consistent.
property p_one_dimension_at_a_time;
  @(posedge clk) disable iff (!rst_n)
    (cfg_req && !$onehot0(cfg_dims)) |=> !cfg_grant;
endproperty
assert property (p_one_dimension_at_a_time);

// P14 -- a grant implies the device was quiesced on the request
// cycle. The converse of P12, closing the gap.
property p_grant_implies_was_quiet;
  @(posedge clk) disable iff (!rst_n)
    cfg_grant |-> $past(quiesced, 1);
endproperty
assert property (p_grant_implies_was_quiet);

// P15 -- every refused request is counted, and every request is
// either granted or refused. No request is silently dropped.
property p_every_request_accounted;
  @(posedge clk) disable iff (!rst_n)
    cfg_req |=> ((cnt_granted + cnt_refused) ==
                 ($past(cnt_granted,1) + $past(cnt_refused,1) + CNT_W'(1)));
endproperty
assert property (p_every_request_accounted);

// ── Cover.
// BOTH verified ratios actually in force. A suite testing one has
// tested a fixed-ratio design, which is not what §3 describes.
cover property (@(posedge clk) disable iff (!rst_n)
                  ratio_valid && (ratio_in_force == RCNT_W'(2)));
cover property (@(posedge clk) disable iff (!rst_n)
                  ratio_valid && (ratio_in_force == RCNT_W'(4)));
// A ratio CHANGE, in both directions. §13's second failure mode only
// appears on a change, so a suite that configures once never sees it.
cover property (@(posedge clk) disable iff (!rst_n)
                  (ratio_in_force == RCNT_W'(4)) ##[1:$]
                  (ratio_in_force == RCNT_W'(2)));
cover property (@(posedge clk) disable iff (!rst_n)
                  (ratio_in_force == RCNT_W'(2)) ##[1:$]
                  (ratio_in_force == RCNT_W'(4)));
// The full phase sweep at each ratio.
cover property (@(posedge clk) disable iff (!rst_n)
                  (ratio_in_force == RCNT_W'(4)) && (wck_phase == PH_W'(3)));
cover property (@(posedge clk) disable iff (!rst_n)
                  (ratio_in_force == RCNT_W'(2)) && (wck_phase == PH_W'(1)));
// Each error kind attempted.
cover property (@(posedge clk) disable iff (!rst_n) err_ratio_unsupported);
cover property (@(posedge clk) disable iff (!rst_n) err_cmd_before_config);
cover property (@(posedge clk) disable iff (!rst_n) err_beat_out_of_burst);
// Both burst lengths exercised, and a stream where they differ.
cover property (@(posedge clk) disable iff (!rst_n)
                  cmd_valid && (cmd_burst_beats == BEAT_W'(16)));
cover property (@(posedge clk) disable iff (!rst_n)
                  cmd_valid && (cmd_burst_beats == BEAT_W'(32)));
cover property (@(posedge clk) disable iff (!rst_n)
                  (extra_bytes_bl32 != '0) && (fewer_bursts_bl32 != '0));
// Each refusal reason, and a grant.
cover property (@(posedge clk) disable iff (!rst_n) err_banks_open);
cover property (@(posedge clk) disable iff (!rst_n) err_multi_dim_at_once);
cover property (@(posedge clk) disable iff (!rst_n) cfg_grant);

// Independent ratio reference. Models the phase as an explicit
// modular counter with the ratio passed in each call, rather than as
// registered state, so agreement with the DUT is evidence rather than
// a restatement. SIMULATION-ONLY.
class ratio_ref;
  int ratio;
  int phase;
  bit configured;

  function void reset();
    ratio = 0; phase = 0; configured = 0;
  endfunction

  function bit config_ratio(int r);
    if (r != 2 && r != 4) return 0;      // rejected, NOT clamped
    ratio = r; phase = 0; configured = 1;
    return 1;
  endfunction

  function void tick();
    if (!configured) return;
    phase = (phase + 1) % ratio;         // the modulus is the RATIO
  endfunction

  function bit crossing_ok(int beat, int burst);
    return configured && (beat < burst);
  endfunction

  function int beats_per_slot();
    return configured ? ratio : 0;
  endfunction
endclass

  THE SUITE THAT ONLY EVER RAN AT 4:1
    Phase counter written as ph <= ph + 1 on a 2-bit register,
    wrapping at its WIDTH rather than at the configured ratio.

    at 4:1  : width modulus 4 == ratio 4.
              phase sequence 0 1 2 3 0 1 2 3 ...   CORRECT
              P1 phase_within_ratio                PASS
              every property                       PASS

    at 2:1  : width modulus 4 != ratio 2.
              phase sequence 0 1 2 3 0 1 2 3 ...
              expected       0 1 0 1 0 1 0 1 ...
              P1 phase_within_ratio                FAIL at phase 2

    coverage of the 4:1-only suite:
              ratio_in_force == 4                  HIT
              ratio_in_force == 2                  NEVER HIT
              ratio change, either direction       NEVER HIT

    diagnosis : the bug is in the wrap condition and is invisible at
      the maximum ratio, because at the maximum ratio the width
      modulus and the configured modulus are the same number. It is a
      bug that only exists in the CONFIGURABILITY, so only a suite
      that exercises more than one configuration can see it.

    what makes it dangerous : 4:1 is the ratio that gives more data
      per command slot (§4) and is the likelier default. A design
      verified at its default and shipped configurable carries a bug
      in the non-default mode with a fully green regression.

    the fix : both ratio covers and both change-direction covers of
      §16 are REQUIRED goals. A configurable design verified in one
      configuration has been verified as a fixed design.