DDR vs GDDR

   carried bandwidth  =  available_connections  x  per_signal_rate

   31.3 §6 works on the first factor and the SURFACE decides it.
   This chapter works on the second, and the question becomes:

       what limits the rate one connection can carry?

   Let  L    = the memory's completion latency, in cycles
        S    = the spacing between successive returns the channel
               can sustain, in cycles  (the OCCUPANCY, 30.4 §3)
        N    = the number of transactions the requester can keep
               outstanding

   the pipeline is FULL -- and therefore latency is INVISIBLE -- iff

       N  >=  ceil( L / S )

   DERIVED, and read it as a requirement on the REQUESTER:
   the memory states L and S; the consumer must supply N.

   ILLUSTRATIVE L = 60 cycles, S = 4 cycles (a burst's occupancy).

       N* = ceil(60 / 4) = 15 outstanding transactions

   a consumer sustaining 15 or more : latency is invisible, and
       raising L to 80 changes NOTHING observable (N* becomes 20).
   a consumer sustaining 4          : it sees 60 cycles per access,
       serialised, and raising L hurts PROPORTIONALLY.

   recompute at S = 2 (a shorter burst on a faster channel):
       N* = ceil(60 / 2) = 30

   DERIVED, and note the direction: making the CHANNEL faster
   RAISES the concurrency the consumer must supply. A faster
   memory is harder to keep full, not easier.

   A LATENCY-OPTIMISED return path is entitled to assume:

       returns arrive in the order the requests were issued

   so association is FREE -- a FIFO suffices, and the head of the
   FIFO is the request the next return belongs to.

   A THROUGHPUT-OPTIMISED return path gives that up deliberately,
   because reordering is what hidden latency BUYS (§5). So:

       association must be by TAG, not by POSITION

   and the FIFO that was correct becomes a misattribution engine:
   it will pair every return with SOME request, and the pairing
   will be wrong, and nothing will report it.

// ---------------------------------------------------------------------
// read_return_path -- the comparative block of §10.
//
// CLASSIFICATION: synthesisable, ILLUSTRATIVE parameter values, and
// CORRECT as written. The intentionally defective block is §11.
//
// WHAT IT IS: the read return path under either objective. The
// generate boundaries are §5's "affordable to give up" list: the
// latency-critical arm carries a bypass and assumes in-order return;
// the throughput arm carries a deep tagged buffer and assumes
// nothing about order.
//
// WHY IT EXISTS HERE: §5 claims that hidden latency makes a reorder
// buffer affordable, and §8 that it simultaneously invalidates
// position-based association. Both claims are structural, and a
// generate boundary is how a structural claim is made checkable.
//
// HOW TO RUN IT: elaborate both arms and present returns OUT OF
// ORDER.
// EXPECTED RESULT: the throughput arm associates correctly by tag;
// the latency-critical arm REFUSES the stimulus via an assertion,
// because out-of-order return is outside its stated contract rather
// than a case it handles badly.
// EXPECTED TRACE: resp_tag must equal the tag of the request whose
// data is being returned, in both arms, for every return.
//
// SYNTHESIS: the latency-critical arm is a small FIFO plus a bypass
// mux. The throughput arm is a tag-indexed buffer of OUTSTANDING
// entries plus a valid vector.
//
// LIMITATIONS: models ASSOCIATION and BUFFERING. It does not model
// link-level error detection or retry -- §6 lists those as added
// obligations and 22.4 owns the electrical reason, and building a
// retry engine here would rebuild a subject this chapter does not
// own. That omission is STATED and is not the bug.
// ---------------------------------------------------------------------
module read_return_path #(
  // The OBJECTIVE parameter. It changes the CONTRACT (what may be
  // assumed about return order), so 31.1 §12's warning applies at
  // full force: the obligation must be re-derived, not inherited.
  parameter bit LATENCY_CRITICAL = 1'b0,

  parameter int OUTSTANDING      = 64,
  parameter int DATA_W           = 256,

  // COUNT versus INDEX, and both appear here for different things.
  // TAG_W indexes the OUTSTANDING tag space, so $clog2(OUTSTANDING)
  // is correct -- tags run 0 .. OUTSTANDING-1.
  parameter int TAG_W            = $clog2(OUTSTANDING),
  // OCC_W must REPRESENT an occupancy of 0 .. OUTSTANDING inclusive,
  // so it needs $clog2(OUTSTANDING + 1). Using TAG_W here would
  // wrap a full buffer to empty, and §11 is a block that makes a
  // related mistake in a place where it is harder to see.
  parameter int OCC_W            = $clog2(OUTSTANDING + 1)
)(
  input  logic                clk,
  input  logic                rst_n,

  // Issue side.
  input  logic                req_fire,
  input  logic [TAG_W-1:0]    req_tag,

  // Device side. `ret_tag` is meaningful only where the device
  // returns a tag; the latency-critical arm ignores it by contract.
  input  logic                ret_valid,
  input  logic [TAG_W-1:0]    ret_tag,
  input  logic [DATA_W-1:0]   ret_data,

  // Requester side.
  output logic                resp_valid,
  output logic [TAG_W-1:0]    resp_tag,
  output logic [DATA_W-1:0]   resp_data,
  input  logic                resp_ready,

  output logic [OCC_W-1:0]    occupancy,
  output logic                overflow,
  output logic [7:0]          added_obligations
);
  initial begin
    if (OUTSTANDING < 2)
      $fatal(1, "read_return_path: OUTSTANDING must be >= 2");
    if ((OUTSTANDING & (OUTSTANDING - 1)) != 0)
      $fatal(1, "read_return_path: OUTSTANDING must be a power of two for a tag-indexed buffer");
    // §4's condition, surfaced at elaboration as a WARNING rather
    // than a fatal, because it is a property of the CONSUMER and this
    // block cannot know it. What it can do is refuse to pretend: a
    // throughput arm with a shallow buffer cannot hide any latency,
    // and saying so at elaboration is cheaper than measuring it.
    if (!LATENCY_CRITICAL && OUTSTANDING < 8)
      $warning("read_return_path: throughput objective with OUTSTANDING = %0d cannot hide meaningful latency (§4)",
               OUTSTANDING);
  end

  generate
  // ===================================================================
  // THROUGHPUT OBJECTIVE. Latency is hidden (§4), so reordering is
  // AFFORDABLE (§5 row four) -- and association must therefore be by
  // TAG (§8). The buffer is indexed by tag, which is what makes
  // out-of-order return a non-event rather than a special case.
  // ===================================================================
  if (!LATENCY_CRITICAL) begin : g_throughput

    logic [DATA_W-1:0] buf_data [OUTSTANDING];
    logic              buf_full [OUTSTANDING];   // data has arrived
    logic              buf_live [OUTSTANDING];   // tag is outstanding
    logic [OCC_W-1:0]  occ;
    logic [TAG_W-1:0]  drain_ptr;

    always_ff @(posedge clk) begin
      if (!rst_n) begin
        for (int i = 0; i < OUTSTANDING; i++) begin
          buf_full[i] <= 1'b0;
          buf_live[i] <= 1'b0;
        end
        occ       <= '0;
        drain_ptr <= '0;
        overflow  <= 1'b0;
      end else begin
        // Issue: the tag becomes outstanding. A tag reissued while
        // still live is a requester error, and it is flagged rather
        // than silently overwritten -- 7.4's discipline that a
        // confident wrong answer is worse than a reported unknown.
        if (req_fire) begin
          if (buf_live[req_tag]) overflow <= 1'b1;
          buf_live[req_tag] <= 1'b1;
          buf_full[req_tag] <= 1'b0;
          if (occ != {OCC_W{1'b1}}) occ <= occ + 1'b1;
        end

        // Return: land the data at ITS OWN TAG. Order is irrelevant,
        // which is the whole point of this arm.
        if (ret_valid) begin
          buf_data[ret_tag] <= ret_data;
          buf_full[ret_tag] <= 1'b1;
        end

        // Drain: present completed entries to the requester. The
        // pointer sweeps the tag space rather than assuming the next
        // completion is the next tag.
        if (resp_valid && resp_ready) begin
          buf_full[drain_ptr] <= 1'b0;
          buf_live[drain_ptr] <= 1'b0;
          if (occ != '0) occ <= occ - 1'b1;
        end
        if (!(buf_live[drain_ptr] && buf_full[drain_ptr]))
          drain_ptr <= drain_ptr + 1'b1;
      end
    end

    assign resp_valid        = buf_live[drain_ptr] && buf_full[drain_ptr];
    assign resp_tag          = drain_ptr;
    assign resp_data         = buf_data[drain_ptr];
    assign occupancy         = occ;
    assign added_obligations = 8'd7;   // §6's count

  // ===================================================================
  // LATENCY-CRITICAL OBJECTIVE. A bypass so the first beat is not
  // delayed by a buffer, and a shallow in-order FIFO. Position-based
  // association is CORRECT HERE, and §8 states exactly why: the
  // contract includes in-order return, so position carries the
  // association. §12 is what happens when this code is reused where
  // that contract no longer holds.
  // ===================================================================
  end else begin : g_latency

    logic [DATA_W-1:0] fifo_data [OUTSTANDING];
    logic [TAG_W-1:0]  fifo_tag  [OUTSTANDING];
    logic [OCC_W-1:0]  wr_ptr, rd_ptr, occ;
    logic              bypass;

    // The bypass: when nothing is queued and the requester is ready,
    // the return goes straight through. This is what the throughput
    // arm gives up (§5 row three) and it is worth area only when the
    // first beat's arrival time is observable.
    assign bypass = ret_valid && (occ == '0) && resp_ready;

    always_ff @(posedge clk) begin
      if (!rst_n) begin
        wr_ptr <= '0; rd_ptr <= '0; occ <= '0; overflow <= 1'b0;
      end else begin
        if (ret_valid && !bypass) begin
          if (occ == OUTSTANDING[OCC_W-1:0]) overflow <= 1'b1;
          else begin
            fifo_data[wr_ptr[TAG_W-1:0]] <= ret_data;
            fifo_tag[wr_ptr[TAG_W-1:0]]  <= ret_tag;
            wr_ptr <= wr_ptr + 1'b1;
            occ    <= occ + 1'b1;
          end
        end
        if (resp_valid && resp_ready && !bypass) begin
          rd_ptr <= rd_ptr + 1'b1;
          occ    <= occ - 1'b1;
        end
      end
    end

    assign resp_valid = bypass || (occ != '0);
    assign resp_data  = bypass ? ret_data : fifo_data[rd_ptr[TAG_W-1:0]];
    // Even here the TAG is carried rather than reconstructed from
    // position. It costs TAG_W bits per entry and it is what makes
    // §14's association property writable at all -- a path that
    // discards the tag cannot be checked against one.
    assign resp_tag   = bypass ? ret_tag  : fifo_tag[rd_ptr[TAG_W-1:0]];
    assign occupancy  = occ;
    assign added_obligations = 8'd0;

  end
  endgenerate
endmodule

// ---------------------------------------------------------------------
// return_associator -- INTENTIONALLY DEFECTIVE, for review (§11).
//
// CLASSIFICATION: synthesisable, ILLUSTRATIVE, and CONTAINS A BUG.
//
// WHAT IT IS MEANT TO DO: the five-clause contract above -- pair each
// return with its request.
//
// WHY IT EXISTS HERE: §8 establishes that a latency-optimised path is
// ENTITLED to associate by position, and that a throughput path which
// reorders deliberately is not. This block is that entitlement
// carried across a parameter change, and it is the third instance in
// this module of the same bug class -- 31.1 §12 (a contract
// parameter), 31.2 §12 (a duration), 31.3 §12 (a granularity).
//
// It is also a sixth mechanism for 10.5 §9's back-to-back-return
// investigation, whose third listed mechanism is exactly "returns
// are reordered and the in-order assumption does not hold". That
// chapter owns the DEBUG method; this block is the DESIGN that
// produces the symptom.
//
// HOW TO RUN IT: issue tags 0,1,2 and return them 2,0,1.
// EXPECTED RESULT under clause 4: resp_tag follows the DATA.
// EXPECTED TRACE: the return carrying tag 2's data must be presented
// with resp_tag = 2, not with resp_tag = 0.
//
// SYNTHESIS: two pointers and a data FIFO.
// LIMITATIONS: association only. Buffering policy is §10's.
// ---------------------------------------------------------------------
module return_associator #(
  parameter int OUTSTANDING = 64,
  parameter int DATA_W      = 256,
  parameter int TAG_W       = $clog2(OUTSTANDING),
  parameter int OCC_W       = $clog2(OUTSTANDING + 1)
)(
  input  logic                clk,
  input  logic                rst_n,

  input  logic                req_fire,
  input  logic [TAG_W-1:0]    req_tag,

  input  logic                ret_valid,
  input  logic [TAG_W-1:0]    ret_tag,     // on the interface, and...
  input  logic [DATA_W-1:0]   ret_data,

  output logic                resp_valid,
  output logic [TAG_W-1:0]    resp_tag,
  output logic [DATA_W-1:0]   resp_data,
  input  logic                resp_ready,

  output logic [OCC_W-1:0]    occupancy,
  output logic                overflow,
  output logic                assoc_error
);
  // The outstanding-request queue, in ISSUE order.
  logic [TAG_W-1:0]  pend_tag  [OUTSTANDING];
  logic [DATA_W-1:0] ret_buf   [OUTSTANDING];
  logic [OCC_W-1:0]  head, tail, occ;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      head <= '0; tail <= '0; occ <= '0;
      overflow <= 1'b0; assoc_error <= 1'b0;
    end else begin
      // Record the issue order. Correct, and necessary.
      if (req_fire) begin
        if (occ == OUTSTANDING[OCC_W-1:0]) overflow <= 1'b1;
        else begin
          pend_tag[tail[TAG_W-1:0]] <= req_tag;
          tail <= tail + 1'b1;
          occ  <= occ + 1'b1;
        end
      end

      // The return. Data is stored at the HEAD of the issue queue --
      // that is, the return is assumed to belong to the OLDEST
      // outstanding request.
      if (ret_valid) begin
        ret_buf[head[TAG_W-1:0]] <= ret_data;   // <-- THE DEFECT
      end

      if (resp_valid && resp_ready) begin
        head <= head + 1'b1;
        occ  <= occ - 1'b1;
      end
    end
  end

  assign resp_valid = (occ != '0);
  assign resp_tag   = pend_tag[head[TAG_W-1:0]];
  assign resp_data  = ret_buf[head[TAG_W-1:0]];
  assign occupancy  = occ;
endmodule

   ILLUSTRATIVE. Issue tags 0, 1, 2 in that order. The device
   returns them REORDERED as 2, 0, 1 -- which the throughput
   objective explicitly permits (§5 row four).

   issue:   pend_tag[0]=0  pend_tag[1]=1  pend_tag[2]=2   occ=3

   return tag 2 (data D2) :  ret_buf[head=0] <= D2
   return tag 0 (data D0) :  ret_buf[head=0] <= D0   overwritten!
   return tag 1 (data D1) :  ret_buf[head=0] <= D1   overwritten!

   drain: resp_tag = pend_tag[0] = 0,  resp_data = D1

   so request 0 is answered with request 1's data. Then head
   advances and request 1 is answered with whatever landed next.

   TWO failures at once, and the second is worse:
     - MISATTRIBUTION: every response carries the wrong data.
     - LOSS: three returns landed in one slot, so two were
       destroyed. The data is not merely misrouted; it is gone.

      // CORRECTED. Clause 2: file the data at ITS OWN TAG, so return
      // order is irrelevant. This is the same structure as §10's
      // throughput arm, which is the point -- the correct design
      // already existed in the module and this block did not use it.
      if (ret_valid) begin
        if (!pend_live[ret_tag]) begin
          // Clause 3: a return for a tag that is not outstanding is
          // an ERROR and must be REPORTED. Absorbing it is what
          // makes the misattribution undiagnosable in a lab --
          // 30.10 §13's argument that a debug observable is a design
          // deliverable rather than an optional extra.
          assoc_error <= 1'b1;
        end else begin
          ret_buf[ret_tag]  <= ret_data;
          ret_full[ret_tag] <= 1'b1;
        end
      end

      // And the drain must present a COMPLETED entry rather than the
      // oldest issued one, because under reordering the oldest issue
      // is not necessarily the first completion.
      // resp_valid = pend_live[drain_ptr] && ret_full[drain_ptr];
      // resp_tag   = drain_ptr;
      // resp_data  = ret_buf[drain_ptr];

// ---------------------------------------------------------------------
// latency_tolerance_monitor -- verification/telemetry, CORRECT as written.
//
// CLASSIFICATION: synthesisable telemetry. Drives nothing.
//
// WHAT IT DOES: measures the outstanding-transaction count over a
// window against ceil(L / S), reporting whether the pipeline was
// actually full often enough for §4's condition to hold.
//
// WHY IT EXISTS HERE: every trade in §5 is licensed by §4's
// condition, and §4's condition is about the REQUESTER. This is the
// instrument that checks the licence. 30.8 §13 makes the same
// argument for the bandwidth ladder: rung 1 moving does not move
// rung 5, and only a measurement distinguishes them.
//
// HOW TO RUN IT: run the real access pattern and read
// `frac_full_num` / `frac_full_den`.
// EXPECTED RESULT: a deeply pipelined streaming consumer reports a
// high fraction; a dependency-chained one reports near zero, and
// that is the finding -- the technology's premise does not hold for
// that consumer.
//
// SYNTHESIS: two counters, a max tracker, one comparator.
//
// LIMITATIONS: measures CONCURRENCY, not throughput. A consumer can
// satisfy §4's condition and still be limited elsewhere -- 30.8's
// gaps 2-to-3 and 4-to-5 -- so a high fraction here licenses the
// latency trade and proves nothing about achieved bandwidth.
// ---------------------------------------------------------------------
module latency_tolerance_monitor #(
  parameter int WIN         = 65536,
  parameter int OUTSTANDING = 64,
  // L and S from §4. ILLUSTRATIVE, and supplied rather than derived
  // because S depends on the burst and L on the configuration --
  // 30.4 §2's unit discipline means neither can be assumed here.
  parameter int LAT_CYCLES  = 60,
  parameter int RET_SPACING = 4,
  // DERIVED at elaboration: N* = ceil(L / S). Integer ceiling,
  // written so it is obviously a ceiling rather than a truncation --
  // a floor here would UNDERSTATE the requirement and license a
  // trade the consumer cannot support.
  parameter int N_STAR      = (LAT_CYCLES + RET_SPACING - 1) / RET_SPACING,
  // COUNT, not INDEX: occupancy ranges 0 .. OUTSTANDING inclusive.
  parameter int OCC_W       = $clog2(OUTSTANDING + 1),
  parameter int CNT_W       = $clog2(WIN + 1)
)(
  input  logic              clk,
  input  logic              rst_n,

  input  logic              req_fire,
  input  logic              resp_fire,
  input  logic              win_tick,

  output logic [OCC_W-1:0]  r_max_outstanding,
  output logic [CNT_W-1:0]  frac_full_num,   // cycles with occ >= N*
  output logic [CNT_W-1:0]  frac_full_den,   // cycles with occ >  0
  output logic              premise_holds,
  output logic              result_valid,
  output logic              underflow
);
  initial begin
    if (RET_SPACING < 1) $fatal(1, "latency_tolerance_monitor: RET_SPACING >= 1");
    if (LAT_CYCLES  < 1) $fatal(1, "latency_tolerance_monitor: LAT_CYCLES >= 1");
    // The structural warning §4 earns: if the buffer cannot hold N*
    // transactions, the premise CANNOT hold however well the
    // requester behaves, and that is a design error rather than a
    // workload property. Flagged at elaboration because it is a
    // static fact -- 30.9 §3's cheapest-tool rule.
    if (OUTSTANDING < N_STAR)
      $fatal(1, "latency_tolerance_monitor: OUTSTANDING (%0d) < N* (%0d): the pipeline cannot be filled (§4)",
             OUTSTANDING, N_STAR);
  end

  logic [OCC_W-1:0] occ, mx;
  logic [CNT_W-1:0] c_full, c_busy;

  always_ff @(posedge clk) begin
    if (!rst_n) begin
      occ <= '0;  mx <= '0;  c_full <= '0;  c_busy <= '0;
      r_max_outstanding <= '0;
      frac_full_num <= '0;  frac_full_den <= '0;
      premise_holds <= 1'b0;  result_valid <= 1'b0;  underflow <= 1'b0;
    end else if (win_tick) begin
      r_max_outstanding <= mx;
      frac_full_num     <= c_full;
      frac_full_den     <= c_busy;
      // The verdict, cross-multiplied so no divider is needed:
      // the premise holds when the pipeline was full for at least
      // three quarters of the BUSY cycles. The threshold is a POLICY
      // and it is stated here rather than hidden -- 24.2 §5's
      // practice of naming a policy input as a policy input.
      premise_holds     <= (c_full * 4) >= (c_busy * 3);
      result_valid      <= 1'b1;
      mx <= '0;  c_full <= '0;  c_busy <= '0;
    end else begin
      result_valid <= 1'b0;

      // Occupancy tracking. The two events can coincide, so the
      // combined case is handled explicitly rather than by two
      // independent if-statements that would race.
      if (req_fire && !resp_fire) begin
        if (occ != OUTSTANDING[OCC_W-1:0]) occ <= occ + 1'b1;
      end else if (resp_fire && !req_fire) begin
        // A response with nothing outstanding is an ERROR, not a
        // saturating subtract. Absorbing it would make the counter
        // drift silently and every figure below it meaningless --
        // 30.8 §11's rule that an instrument which can report an
        // impossible value has never been checked.
        if (occ == '0) underflow <= 1'b1;
        else           occ <= occ - 1'b1;
      end

      if (occ > mx) mx <= occ;
      if (occ >= N_STAR[OCC_W-1:0] && c_full != {CNT_W{1'b1}})
        c_full <= c_full + 1'b1;
      if (occ != '0 && c_busy != {CNT_W{1'b1}})
        c_busy <= c_busy + 1'b1;
    end
  end
endmodule

  // Offered as "proves every return is associated with a request".
  // Clause 1, and it PASSES on the defective block.
  property p_response_has_a_request;
    @(posedge clk) disable iff (!rst_n)
      resp_valid |-> (occupancy != '0);
  endproperty
  assert property (p_response_has_a_request)
    else $error("a response was presented with nothing outstanding");

  // And the in-order association property, which was CORRECT in the
  // latency-optimised design this code came from.
  property p_response_follows_issue_order;
    @(posedge clk) disable iff (!rst_n)
      (resp_valid && resp_ready) |-> (resp_tag == pend_tag[head]);
  endproperty
  assert property (p_response_follows_issue_order)
    else $error("response tag did not follow issue order");

  // Clause 4, and it is the property that is sound in BOTH arms
  // because it names the DATA's tag rather than a position. The
  // reference function is an independent model of the association --
  // 27.3's independence requirement, and 30.6 §11's rule that a
  // comparative obligation needs a model rather than a property.
  property p_response_tag_matches_its_data;
    @(posedge clk) disable iff (!rst_n)
      (resp_valid && resp_ready) |->
        (resp_data == ref_expected_data(resp_tag));
  endproperty
  assert property (p_response_tag_matches_its_data)
    else $error("response data does not belong to the response tag");

  // Clause 2, guarded by the configuration that licenses it. This is
  // the repair for variety 10: the parameter sits in the ANTECEDENT
  // as a condition on which contract is in force, and the claim
  // inside is unchanged in meaning -- 31.1 §14's test, passed.
  property p_in_order_only_when_licensed;
    @(posedge clk) disable iff (!rst_n)
      (LATENCY_CRITICAL && resp_valid && resp_ready) |->
        (resp_tag == pend_tag[head]);
  endproperty
  assert property (p_in_order_only_when_licensed)
    else $error("in-order association violated in the arm that guarantees it");

  // Clause 3. A return for a tag that is not outstanding must be
  // REPORTED. The defective block leaves assoc_error undriven, so
  // this property is what turns an undriven output into a failure.
  property p_unknown_tag_is_reported;
    @(posedge clk) disable iff (!rst_n)
      (ret_valid && !pend_live[ret_tag]) |-> assoc_error;
  endproperty
  assert property (p_unknown_tag_is_reported)
    else $error("a return for a non-outstanding tag was absorbed silently");

  // Clause 5, both directions. Occupancy is a derived count, so its
  // RANGE is asserted -- 30.8 §11's rule, and the direction matters:
  // an understated occupancy licenses an overflow.
  property p_occupancy_in_range;
    @(posedge clk) disable iff (!rst_n)
      occupancy <= OUTSTANDING;
  endproperty
  assert property (p_occupancy_in_range)
    else $error("occupancy exceeded OUTSTANDING");

  property p_overflow_is_reported;
    @(posedge clk) disable iff (!rst_n)
      (req_fire && occupancy == OUTSTANDING) |-> overflow;
  endproperty
  assert property (p_overflow_is_reported)
    else $error("an issue beyond OUTSTANDING did not set overflow");

  // No data may be OVERWRITTEN before it is delivered. This is the
  // second half of §12's failure -- the loss, which the
  // misattribution properties above do not catch, because a
  // destroyed return produces no wrong value at the interface, only
  // a missing one.
  property p_no_return_overwritten;
    @(posedge clk) disable iff (!rst_n)
      (ret_valid && ret_full[ret_tag]) |-> assoc_error;
  endproperty
  assert property (p_no_return_overwritten)
    else $error("a return overwrote undelivered data for the same tag");

  // §4's premise, asserted where it is a DESIGN fact rather than a
  // workload one: the buffer must be able to hold N*.
  property p_buffer_can_hold_n_star;
    @(posedge clk) disable iff (!rst_n)
      OUTSTANDING >= N_STAR;
  endproperty
  assert property (p_buffer_can_hold_n_star)
    else $error("the return buffer is too shallow to fill the pipeline");

  // ---- Covers. Per configuration, per order, and per depth.
  // The two objectives -- 31.1 §14's configuration rule.
  cover property (@(posedge clk) disable iff (!rst_n)
                  resp_valid && LATENCY_CRITICAL);
  cover property (@(posedge clk) disable iff (!rst_n)
                  resp_valid && !LATENCY_CRITICAL);
  // OUT-OF-ORDER return, which is the antecedent the whole defect
  // lives behind. In-order stimulus makes every property above hold
  // on the defective block, so this cover is the one that matters --
  // and an environment that models the device as in-order will
  // never reach it, however long it runs.
  cover property (@(posedge clk) disable iff (!rst_n)
                  ret_valid && (ret_tag != pend_tag[head]));
  // And the DEPTH regime, because §4 shows the requirement scales:
  // a pipeline that is full is a different test from one that is
  // merely non-empty, and only the first exercises reordering
  // pressure.
  cover property (@(posedge clk) disable iff (!rst_n)
                  occupancy >= N_STAR);
  cover property (@(posedge clk) disable iff (!rst_n)
                  occupancy == OUTSTANDING);

  // ---- The BYPASS, which exists only in the latency arm and is
  //      §5 row three's give-up made concrete. Two obligations, and
  //      they are separate: the bypass must be CORRECT when taken,
  //      and it must not be taken when it would reorder.
  property p_bypass_preserves_association;
    @(posedge clk) disable iff (!rst_n)
      (LATENCY_CRITICAL && bypass) |->
        (resp_tag == ret_tag && resp_data == ret_data);
  endproperty
  assert property (p_bypass_preserves_association)
    else $error("the bypass presented a tag or data that was not the return's");

  // A bypass while the FIFO is non-empty would deliver a NEWER
  // return ahead of an older queued one -- reordering, inside the
  // arm whose whole contract is that it does not reorder. This is
  // the property that makes the bypass safe rather than merely fast.
  property p_no_bypass_when_queued;
    @(posedge clk) disable iff (!rst_n)
      (LATENCY_CRITICAL && bypass) |-> (occupancy == '0);
  endproperty
  assert property (p_no_bypass_when_queued)
    else $error("bypass taken with data queued: the in-order contract is broken");

  // ---- Occupancy must agree with the events that change it. A
  //      derived count, so its RANGE is asserted (30.8 §11) and its
  //      ARITHMETIC is asserted separately -- a counter can be in
  //      range and still have drifted.
  property p_occupancy_tracks_events;
    @(posedge clk) disable iff (!rst_n)
      occupancy == ($past(occupancy)
                    + (($past(req_fire) && !$past(resp_valid && resp_ready)) ? 1 : 0)
                    - ((!$past(req_fire) && $past(resp_valid && resp_ready)) ? 1 : 0));
  endproperty
  assert property (p_occupancy_tracks_events)
    else $error("occupancy drifted from the issue and completion events");

  // ---- The throughput arm's defining property, and the one that is
  //      FALSE in the other arm -- so it is guarded by the
  //      configuration, per §14's repair for variety 10. A tag's
  //      data must be filed at that tag, independent of arrival
  //      order, which is the structural difference §8 names.
  property p_tag_indexed_when_reordering;
    @(posedge clk) disable iff (!rst_n)
      (!LATENCY_CRITICAL && ret_valid) |=> buf_full[$past(ret_tag)];
  endproperty
  assert property (p_tag_indexed_when_reordering)
    else $error("a return did not land at its own tag in the reordering arm");

  // ---- A tag reissued while still outstanding is a REQUESTER error
  //      and must be reported, not absorbed. 7.4's discipline: a
  //      confident wrong answer is worse than a reported unknown,
  //      and silently overwriting a live entry produces exactly the
  //      loss failure §12's second half describes.
  property p_live_tag_reissue_is_reported;
    @(posedge clk) disable iff (!rst_n)
      (!LATENCY_CRITICAL && req_fire && buf_live[req_tag]) |=> overflow;
  endproperty
  assert property (p_live_tag_reissue_is_reported)
    else $error("a live tag was reissued without report");

  // ---- Covers. Per arm, and then per the FEATURE each arm has that
  //      the other does not -- because a cover on the arm alone does
  //      not prove the arm's distinguishing path was exercised.
  // The bypass, taken. Absent from the throughput arm by
  // construction, so this must go DEAD there and be LIVE here --
  // two different instruments, 30.10 §12's distinction.
  cover property (@(posedge clk) disable iff (!rst_n)
                  LATENCY_CRITICAL && bypass);
  // The bypass NOT taken because data was queued: the path that
  // makes p_no_bypass_when_queued non-trivial.
  cover property (@(posedge clk) disable iff (!rst_n)
                  LATENCY_CRITICAL && ret_valid && (occupancy != '0));
  // A return landing at a tag that is NOT the drain pointer, which
  // is the reordering arm's distinguishing event and the antecedent
  // §14's out-of-order cover watches from the other side.
  cover property (@(posedge clk) disable iff (!rst_n)
                  !LATENCY_CRITICAL && ret_valid && (ret_tag != drain_ptr));
  // A full buffer in the reordering arm -- §4's N* condition
  // actually reached, rather than merely permitted by the parameter.
  cover property (@(posedge clk) disable iff (!rst_n)
                  !LATENCY_CRITICAL && (occupancy == OUTSTANDING));