Completion Timeouts — Which Timer Fired, and Was It the Right One?

the requester observes:   nothing came back
the possible causes:      no Completion was ever sent
                          a Completion was sent and lost on the link
                          a Completion arrived with an identity that did not match
                          Completions arrived but the byte count was never satisfied
                          a Completion arrived and the local retirement path dropped it

1  the hardware Completion Timeout
   owner:  the requester's transaction layer
   scope:  one outstanding non-posted request
   effect: abandons the request and reclaims its Tag
 
2  the local engine watchdog
   owner:  the DMA engine or the function's control logic
   scope:  one job, which may span many requests
   effect: aborts the job; may reset engine state
 
3  the driver/software timeout
   owner:  host software
   scope:  one operation, which may span many jobs
   effect: error recovery, device reset, re-enumeration

package cto_dbg_pkg;
 
  // §4's three timers, kept as distinct types so that a report can never
  // conflate them.  The enum exists to make "which timer fired" a field
  // rather than an inference.
  typedef enum logic [1:0] {
    TMR_NONE     = 2'd0,
    TMR_HARDWARE = 2'd1,   // the requester's Completion Timeout
    TMR_WATCHDOG = 2'd2,   // the local engine's job watchdog
    TMR_DRIVER   = 2'd3    // host software
  } timer_src_e;
 
  // §3's five causes.  The table records which one applied, because the
  // timer itself fires identically for all five.
  typedef enum logic [2:0] {
    CTO_NONE          = 3'd0,
    CTO_NEVER_ANSWERED= 3'd1,  // A — nothing arrived at all
    CTO_LOST          = 3'd2,  // B — indistinguishable from A locally (§3)
    CTO_WRONG_ID      = 3'd3,  // C — arrived, identity mismatched
    CTO_PARTIAL       = 3'd4,  // D — 0 < bytes < requested
    CTO_LOCAL_DROP    = 3'd5   // E — matched, retirement path lost it
  } cto_cause_e;
 
  function automatic int unsigned gw(input int unsigned n);
    return (n <= 1) ? 1 : $clog2(n);
  endfunction
 
  // The epoch is a generation counter per Tag.  Its width bounds how many
  // reissues can occur before a very late Completion could alias onto the
  // same epoch again — see P21 and mutation 24.
  localparam int unsigned EPOCH_W = 4;
  typedef logic [EPOCH_W-1:0] epoch_t;
 
endpackage

module cto_outstanding_table #(
  parameter int unsigned NTAG      = 32,
  parameter int unsigned CTO_LIMIT = 32'd2000    // MODEL PARAMETER — see §6
)(
  input  logic clk,
  input  logic rst_n,
  // allocation
  input  logic                                   alloc,
  input  logic [cto_dbg_pkg::gw(NTAG)-1:0]       alloc_tag,
  input  logic [31:0]                            alloc_bytes,
  input  cto_dbg_pkg::epoch_t                    alloc_epoch,
  // completion arrival, already identity-qualified upstream
  input  logic                                   cpl_ok,
  input  logic [cto_dbg_pkg::gw(NTAG)-1:0]       cpl_tag,
  input  logic [15:0]                            cpl_bytes,
  // outputs
  output logic                                   timeout_fire,
  output logic [cto_dbg_pkg::gw(NTAG)-1:0]       timeout_tag,
  output cto_dbg_pkg::cto_cause_e                timeout_cause,
  output logic [31:0]                            timeout_bytes_got,
  output logic [31:0]                            timeout_bytes_want
);
 
  import cto_dbg_pkg::*;
 
  typedef struct packed {
    logic        live;
    logic [31:0] age;
    logic [31:0] want;      // bytes requested
    logic [31:0] got;       // bytes received so far — §5's requirement
    logic        saw_any;   // did ANY completion match this request?
    epoch_t      ep;
  } ent_t;
 
  ent_t tbl [NTAG];
  logic [gw(NTAG)-1:0] sweep;
 
  // Per-entry age, and the NEXT-value comparison of §6.  `age == LIMIT`
  // is 25.4 §7's measured failure: it never fires when the counter can
  // step by more than one.
  logic [31:0] age_next;
  assign age_next = tbl[sweep].age + 32'd1;
 
  always_comb begin
    timeout_fire       = tbl[sweep].live && (age_next >= CTO_LIMIT);
    timeout_tag        = sweep;
    timeout_bytes_got  = tbl[sweep].got;
    timeout_bytes_want = tbl[sweep].want;
 
    // §3's classification, decided from the evidence the table kept.
    // A timer alone cannot produce this; only the recorded fields can.
    if      (!timeout_fire)                          timeout_cause = CTO_NONE;
    else if (tbl[sweep].got == 0 && !tbl[sweep].saw_any)
                                                     timeout_cause = CTO_NEVER_ANSWERED;
    else if (tbl[sweep].got == 0 &&  tbl[sweep].saw_any)
                                                     timeout_cause = CTO_WRONG_ID;
    else if (tbl[sweep].got < tbl[sweep].want)        timeout_cause = CTO_PARTIAL;
    else                                             timeout_cause = CTO_LOCAL_DROP;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < NTAG; i++) tbl[i] <= '0;
      sweep <= '0;
    end else begin
      // Age every live entry.  Note this is NOT gated on link activity —
      // a timer that stops when the link stops cannot detect a dead link
      // (P11, mutation 13).
      for (int i = 0; i < NTAG; i++)
        if (tbl[i].live && tbl[i].age != 32'hFFFF_FFFF)
          tbl[i].age <= tbl[i].age + 32'd1;
 
      if (alloc) begin
        tbl[alloc_tag].live    <= 1'b1;
        tbl[alloc_tag].age     <= '0;
        tbl[alloc_tag].want    <= alloc_bytes;
        tbl[alloc_tag].got     <= '0;
        tbl[alloc_tag].saw_any <= 1'b0;
        tbl[alloc_tag].ep      <= alloc_epoch;
      end
 
      if (cpl_ok) begin
        tbl[cpl_tag].saw_any <= 1'b1;
        tbl[cpl_tag].got     <= tbl[cpl_tag].got + 32'(cpl_bytes);
        // Retire on BYTE COUNT, never on "a completion arrived" (§5).
        if ((tbl[cpl_tag].got + 32'(cpl_bytes)) >= tbl[cpl_tag].want)
          tbl[cpl_tag].live <= 1'b0;
      end
 
      if (timeout_fire) tbl[sweep].live <= 1'b0;
      sweep <= (sweep == gw(NTAG)'(NTAG-1)) ? '0 : sweep + 1'b1;
    end
  end
 
endmodule

module cto_tag_alloc #(
  parameter int unsigned NTAG = 32
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                request,
  output logic                                grant,
  output logic [cto_dbg_pkg::gw(NTAG)-1:0]    grant_tag,
  output cto_dbg_pkg::epoch_t                 grant_epoch,
  input  logic                                retire,      // normal completion
  input  logic [cto_dbg_pkg::gw(NTAG)-1:0]    retire_tag,
  input  logic                                abandon,     // timeout
  input  logic [cto_dbg_pkg::gw(NTAG)-1:0]    abandon_tag,
  output cto_dbg_pkg::epoch_t                 cur_epoch [NTAG],
  output logic [cto_dbg_pkg::gw(NTAG+1)-1:0]  free_count
);
 
  import cto_dbg_pkg::*;
 
  logic [NTAG-1:0] free_mask;
  epoch_t          ep [NTAG];
 
  assign cur_epoch = ep;
 
  always_comb begin
    grant     = request && (free_mask != '0);
    grant_tag = '0;
    for (int i = NTAG-1; i >= 0; i--) if (free_mask[i]) grant_tag = gw(NTAG)'(i);
    grant_epoch = ep[grant_tag];
    free_count  = '0;
    for (int i = 0; i < NTAG; i++) free_count += gw(NTAG+1)'(free_mask[i]);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      free_mask <= '1;
      for (int i = 0; i < NTAG; i++) ep[i] <= '0;
    end else begin
      if (grant)  free_mask[grant_tag]  <= 1'b0;
      if (retire) begin
        free_mask[retire_tag] <= 1'b1;
        ep[retire_tag]        <= ep[retire_tag] + 1'b1;
      end
      if (abandon) begin
        free_mask[abandon_tag] <= 1'b1;
        // The bump happens HERE, at abandonment — not at the next reissue.
        // Deferring it leaves a window in which a late Completion matches
        // the current epoch (mutation 22), and §13's third row measured
        // what removing the bump entirely costs: 39,574 misdeliveries that
        // the epoch-based diagnostic reports as ZERO late Completions.
        ep[abandon_tag] <= ep[abandon_tag] + 1'b1;
      end
    end
  end
 
endmodule

module cto_cpl_qualify #(
  parameter int unsigned NTAG = 32
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                                 cpl_valid,
  input  logic [15:0]                          cpl_rid,
  input  logic [cto_dbg_pkg::gw(NTAG)-1:0]     cpl_tag,
  input  cto_dbg_pkg::epoch_t                  cpl_epoch,
  input  logic [15:0]                          my_rid,
  input  cto_dbg_pkg::epoch_t                  cur_epoch [NTAG],
  input  logic [NTAG-1:0]                      tag_live,
  output logic                                 cpl_accept,
  output logic                                 cpl_late,      // stale epoch
  output logic                                 cpl_foreign,   // wrong RID
  output logic                                 cpl_orphan,    // tag not live
  output logic [31:0]                          late_count,
  output logic [31:0]                          foreign_count,
  output logic [31:0]                          orphan_count
);
 
  import cto_dbg_pkg::*;
 
  // Three distinct rejection reasons, never merged.  Merging them is
  // mutation 27, and it destroys exactly the distinction §3 classes C and
  // the late-completion path depend on.
  always_comb begin
    cpl_foreign = cpl_valid && (cpl_rid != my_rid);
    cpl_orphan  = cpl_valid && !cpl_foreign && !tag_live[cpl_tag];
    cpl_late    = cpl_valid && !cpl_foreign &&  tag_live[cpl_tag] &&
                  (cpl_epoch != cur_epoch[cpl_tag]);
    cpl_accept  = cpl_valid && !cpl_foreign && !cpl_orphan && !cpl_late;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      late_count <= '0; foreign_count <= '0; orphan_count <= '0;
    end else begin
      if (cpl_late    && late_count    != 32'hFFFF_FFFF) late_count    <= late_count + 32'd1;
      if (cpl_foreign && foreign_count != 32'hFFFF_FFFF) foreign_count <= foreign_count + 32'd1;
      if (cpl_orphan  && orphan_count  != 32'hFFFF_FFFF) orphan_count  <= orphan_count + 32'd1;
    end
  end
 
endmodule

module cto_bytecount_check (
  input  logic        clk,
  input  logic        rst_n,
  input  logic        cpl_accept,
  input  logic [11:0] cpl_byte_count,   // remaining INCLUDING this Cpl (13.3 §2)
  input  logic [15:0] cpl_payload_bytes,
  input  logic [31:0] req_want,
  input  logic [31:0] req_got,
  output logic        bc_consistent,
  output logic        bc_violation,
  output logic        would_overrun,
  output logic [31:0] bc_violation_count
);
 
  logic [31:0] expect_remaining;
 
  always_comb begin
    // What the requester believes remains, before crediting this Cpl.
    expect_remaining = req_want - req_got;
    // The completer's own statement of what remains, from the header.
    // Comparing the two catches a lost or duplicated split Completion at
    // the moment it happens, several timer periods before the timeout.
    bc_consistent = cpl_accept && (32'(cpl_byte_count) == expect_remaining);
    bc_violation  = cpl_accept && !bc_consistent;
    // A Cpl carrying more payload than the request has outstanding is a
    // buffer overrun, and it is the same two-sided reasoning as 25.6 §4.
    would_overrun = cpl_accept && (32'(cpl_payload_bytes) > expect_remaining);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) bc_violation_count <= '0;
    else if (bc_violation && bc_violation_count != 32'hFFFF_FFFF)
      bc_violation_count <= bc_violation_count + 32'd1;
  end
 
endmodule

module cto_timer_order #(
  parameter int unsigned HW_LIMIT   = 32'd2_000,    // MODEL PARAMETERS (§6)
  parameter int unsigned WDOG_LIMIT = 32'd20_000,
  parameter int unsigned DRV_LIMIT  = 32'd200_000
)(
  input  logic clk,
  input  logic rst_n,
  input  logic [31:0] req_age,
  input  logic [31:0] job_age,
  input  logic [31:0] op_age,
  output cto_dbg_pkg::timer_src_e fired,
  output logic        ordering_ok,
  output logic        ordering_ambiguous
);
 
  import cto_dbg_pkg::*;
 
  // The ordering is checked, not assumed.  §14 measured that inverting it
  // changes the reported cause of an unchanged fault population from
  // "hardware Completion Timeout, 9,984" to "driver timeout, 9,984".
  assign ordering_ok        = (HW_LIMIT < WDOG_LIMIT) && (WDOG_LIMIT < DRV_LIMIT);
  assign ordering_ambiguous = (HW_LIMIT == WDOG_LIMIT) || (WDOG_LIMIT == DRV_LIMIT) ||
                              (HW_LIMIT == DRV_LIMIT);
 
  // Innermost first.  This priority is only MEANINGFUL when ordering_ok
  // holds; when it does not, the reported cause is a property of this
  // priority list rather than of the fault (§4's third row).
  always_comb begin
    if      (req_age >= HW_LIMIT)   fired = TMR_HARDWARE;
    else if (job_age >= WDOG_LIMIT) fired = TMR_WATCHDOG;
    else if (op_age  >= DRV_LIMIT)  fired = TMR_DRIVER;
    else                            fired = TMR_NONE;
  end
 
endmodule

module cto_first_record #(
  parameter int unsigned NTAG = 32
)(
  input  logic clk,
  input  logic rst_n,
  input  logic                              timeout_fire,
  input  logic [cto_dbg_pkg::gw(NTAG)-1:0]  timeout_tag,
  input  cto_dbg_pkg::cto_cause_e           timeout_cause,
  input  cto_dbg_pkg::timer_src_e           timeout_timer,
  input  logic [31:0]                       bytes_got,
  input  logic [31:0]                       bytes_want,
  input  logic                              clear,
  output logic                              captured,
  output cto_dbg_pkg::cto_cause_e           first_cause,
  output cto_dbg_pkg::timer_src_e           first_timer,
  output logic [31:0]                       first_got,
  output logic [31:0]                       first_want,
  output logic [31:0]                       timeout_count
);
 
  import cto_dbg_pkg::*;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      captured <= 1'b0; first_cause <= CTO_NONE; first_timer <= TMR_NONE;
      first_got <= '0; first_want <= '0; timeout_count <= '0;
    end else if (timeout_fire) begin
      // Sticky FIRST, per 25.1 §6: later timeouts are usually consequences
      // of the first (a stalled requester times out everything it holds),
      // and overwriting destroys the only informative sample.
      if (!captured) begin
        captured    <= 1'b1;
        first_cause <= timeout_cause;
        first_timer <= timeout_timer;
        first_got   <= bytes_got;
        first_want  <= bytes_want;
      end
      if (timeout_count != 32'hFFFF_FFFF) timeout_count <= timeout_count + 32'd1;
    end
  end
 
endmodule

// verilog_lint: waive-start module-filename
module cto_misdeliver_oracle #(
  parameter int unsigned NTAG   = 32,
  parameter int unsigned SER_W  = 32
)(
  input  logic clk,
  input  logic rst_n,
  // A ground-truth serial stamped on every request and carried, in the
  // TESTBENCH only, alongside each Completion.  No RTL mechanism reads it.
  input  logic                              alloc,
  input  logic [cto_dbg_pkg::gw(NTAG)-1:0]  alloc_tag,
  input  logic [SER_W-1:0]                  alloc_serial,
  input  logic                              cpl_credited,
  input  logic [cto_dbg_pkg::gw(NTAG)-1:0]  cpl_tag,
  input  logic [SER_W-1:0]                  cpl_serial,
  input  logic [15:0]                       cpl_bytes,
  output logic                              misdeliver,
  output logic [31:0]                       misdeliver_count,
  output logic [63:0]                       misdeliver_bytes
);
 
  logic [SER_W-1:0] owner_serial [NTAG];
 
  // The check is independent of the epoch mechanism ENTIRELY.  §13's third
  // row is why: with the epoch bump removed, an epoch-based detector
  // reports 0 late Completions while 39,574 payloads land in wrong
  // buffers.  A diagnostic derived from the mechanism it checks is blind
  // exactly where that mechanism fails.
  assign misdeliver = cpl_credited && (cpl_serial != owner_serial[cpl_tag]);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      misdeliver_count <= '0; misdeliver_bytes <= '0;
      for (int i = 0; i < NTAG; i++) owner_serial[i] <= '0;
    end else begin
      if (alloc) owner_serial[alloc_tag] <= alloc_serial;
      if (misdeliver) begin
        misdeliver_count <= misdeliver_count + 32'd1;
        misdeliver_bytes <= misdeliver_bytes + 64'(cpl_bytes);
      end
    end
  end
 
endmodule
// verilog_lint: waive-stop module-filename

// P1 — a tag is live in the table iff the allocator has it outstanding.
property p1_table_alloc_agree;
  @(posedge clk) disable iff (!rst_n)
    tbl_live[tag] |-> !free_mask[tag];
endproperty
a_p1: assert property (p1_table_alloc_agree);
 
// P2 — allocation initialises the entry completely.  A partially reset
// entry inherits the previous request's byte counts (mutation 4).
property p2_alloc_clears;
  @(posedge clk) disable iff (!rst_n)
    alloc |=> ((tbl[$past(alloc_tag)].age == 0) &&
               (tbl[$past(alloc_tag)].got == 0) &&
               (tbl[$past(alloc_tag)].saw_any == 1'b0));
endproperty
a_p2: assert property (p2_alloc_clears);
 
// P3 — an entry leaves the table exactly once per occupancy.
property p3_single_exit;
  @(posedge clk) disable iff (!rst_n)
    (retire && (retire_tag == abandon_tag)) |-> !abandon;
endproperty
a_p3: assert property (p3_single_exit);
 
// P4 — no allocation of a tag that is already live.
property p4_no_double_alloc;
  @(posedge clk) disable iff (!rst_n)
    alloc |-> !tbl_live[alloc_tag];
endproperty
a_p4: assert property (p4_no_double_alloc);
 
// P5 — the free count never exceeds NTAG.
property p5_free_bounded;
  @(posedge clk) disable iff (!rst_n)
    (free_count <= NTAG);
endproperty
a_p5: assert property (p5_free_bounded);

// P6 — retirement happens on byte count, never on completion arrival.
property p6_retire_on_bytes;
  @(posedge clk) disable iff (!rst_n)
    retire |-> (tbl[retire_tag].got >= tbl[retire_tag].want);
endproperty
a_p6: assert property (p6_retire_on_bytes);
 
// P7 — a request is never retired with bytes still owed.  The direct
// statement of "a split completion series is not one completion".
property p7_no_early_retire;
  @(posedge clk) disable iff (!rst_n)
    (cpl_accept && (tbl[cpl_tag].got + cpl_bytes < tbl[cpl_tag].want))
      |=> tbl_live[$past(cpl_tag)];
endproperty
a_p7: assert property (p7_no_early_retire);
 
// P8 — received bytes never exceed requested bytes.  25.6 §4's two-sided
// reasoning, applied to the completion path.
property p8_no_byte_overrun;
  @(posedge clk) disable iff (!rst_n)
    cpl_accept |-> !would_overrun;
endproperty
a_p8: assert property (p8_no_byte_overrun);

// P9 — the expiry comparison is on the NEXT value and is >=, not ==.
// 25.4 §15 measured `== LIMIT` missing 20.0% of the time at a 1-3 step.
property p9_next_value_compare;
  @(posedge clk) disable iff (!rst_n)
    (tbl_live[sweep] && ((tbl[sweep].age + 1) >= CTO_LIMIT)) |-> timeout_fire;
endproperty
a_p9: assert property (p9_next_value_compare);
 
// P10 — age is per request, cleared at allocation, never shared.
property p10_age_per_request;
  @(posedge clk) disable iff (!rst_n)
    alloc |=> (tbl[$past(alloc_tag)].age == 32'd0);
endproperty
a_p10: assert property (p10_age_per_request);
 
// P11 — the age advances regardless of link activity.  A timer gated on
// link-active stops counting exactly when the fault occurs (mutation 13).
property p11_age_not_link_gated;
  @(posedge clk) disable iff (!rst_n)
    (tbl_live[tag] && !link_active && (tbl[tag].age != 32'hFFFF_FFFF))
      |=> (tbl[tag].age > $past(tbl[tag].age));
endproperty
a_p11: assert property (p11_age_not_link_gated);
 
// P12 — no timeout fires before the limit.
property p12_no_early_timeout;
  @(posedge clk) disable iff (!rst_n)
    timeout_fire |-> ((tbl[timeout_tag].age + 1) >= CTO_LIMIT);
endproperty
a_p12: assert property (p12_no_early_timeout);
 
// P13 — the age saturates rather than wrapping.  A wrapped age restarts
// the wait silently and the request never times out at all.
property p13_age_saturates;
  @(posedge clk) disable iff (!rst_n)
    (tbl[tag].age == 32'hFFFF_FFFF) |=> (tbl[tag].age == 32'hFFFF_FFFF);
endproperty
a_p13: assert property (p13_age_saturates);

// P14 — the completer's stated remaining count agrees with the requester's.
// This catches a lost split Completion AT the completion, not at the
// timeout several timer periods later.
property p14_bytecount_agrees;
  @(posedge clk) disable iff (!rst_n)
    cpl_accept |-> bc_consistent;
endproperty
a_p14: assert property (p14_bytecount_agrees);
 
// P15 — a byte count disagreement is reported, never silently tolerated.
property p15_bc_violation_reported;
  @(posedge clk) disable iff (!rst_n)
    (cpl_accept && !bc_consistent) |-> bc_violation;
endproperty
a_p15: assert property (p15_bc_violation_reported);
 
// P16 — the final Completion of a series states a remaining count equal to
// its own payload.
property p16_final_cpl_bytecount;
  @(posedge clk) disable iff (!rst_n)
    (cpl_accept && ((tbl[cpl_tag].got + cpl_bytes) == tbl[cpl_tag].want))
      |-> (cpl_byte_count == cpl_payload_bytes);
endproperty
a_p16: assert property (p16_final_cpl_bytecount);

// P17 — a Completion with a foreign Requester ID is never accepted.
property p17_reject_foreign_rid;
  @(posedge clk) disable iff (!rst_n)
    (cpl_valid && (cpl_rid != my_rid)) |-> !cpl_accept;
endproperty
a_p17: assert property (p17_reject_foreign_rid);
 
// P18 — a Completion whose epoch does not match the tag's current epoch is
// never accepted.  This is the CHECK; §13's second row removed it and
// measured 39,574 misdeliveries carrying 1,907,096 bytes.
property p18_reject_stale_epoch;
  @(posedge clk) disable iff (!rst_n)
    (cpl_valid && tag_live[cpl_tag] && (cpl_epoch != cur_epoch[cpl_tag]))
      |-> !cpl_accept;
endproperty
a_p18: assert property (p18_reject_stale_epoch);
 
// P19 — the epoch is bumped AT abandonment.  This is the BUMP; §13's third
// row removed it and measured identical corruption while the epoch-based
// diagnostic reported ZERO late Completions.  P18 and P19 are a pair and
// neither alone is sufficient.
property p19_epoch_bumped_on_abandon;
  @(posedge clk) disable iff (!rst_n)
    abandon |=> (cur_epoch[$past(abandon_tag)] != $past(cur_epoch[$past(abandon_tag)]));
endproperty
a_p19: assert property (p19_epoch_bumped_on_abandon);
 
// P20 — the epoch is also bumped on normal retirement, so a very late
// Completion from a retired request cannot match either.
property p20_epoch_bumped_on_retire;
  @(posedge clk) disable iff (!rst_n)
    retire |=> (cur_epoch[$past(retire_tag)] != $past(cur_epoch[$past(retire_tag)]));
endproperty
a_p20: assert property (p20_epoch_bumped_on_retire);
 
// P21 — a tag is not reissued until its epoch has advanced.  Without this
// the bump and the reissue can race (mutation 22).
property p21_no_reissue_before_bump;
  @(posedge clk) disable iff (!rst_n)
    (abandon && grant && (grant_tag == abandon_tag)) |-> 1'b0;
endproperty
a_p21: assert property (p21_no_reissue_before_bump);
 
// P22 — the INDEPENDENT oracle sees no misdelivery.  Deliberately not
// derived from the epoch, because §13 showed an epoch-derived check is
// blind exactly where the epoch mechanism fails.
property p22_no_misdelivery;
  @(posedge clk) disable iff (!rst_n)
    !misdeliver;
endproperty
a_p22: assert property (p22_no_misdelivery);

// P23 — every timeout reclaims its tag.  Omitting this starves the
// requester: §13 measured 366 requests issued against a healthy 31,195.
property p23_timeout_reclaims;
  @(posedge clk) disable iff (!rst_n)
    timeout_fire |=> free_mask[$past(timeout_tag)];
endproperty
a_p23: assert property (p23_timeout_reclaims);
 
// P24 — a live request eventually leaves the table, by retirement or
// timeout.  The chapter's only liveness property.
property p24_eventual_exit;
  @(posedge clk) disable iff (!rst_n)
    alloc |-> s_eventually (!tbl_live[$past(alloc_tag)]);
endproperty
a_p24: assert property (p24_eventual_exit);
 
// P25 — free tags are eventually available again under any fault.
property p25_no_permanent_starvation;
  @(posedge clk) disable iff (!rst_n)
    (free_count == 0) |-> s_eventually (free_count > 0);
endproperty
a_p25: assert property (p25_no_permanent_starvation);

// P26 — the three limits are strictly ordered innermost-to-outermost.
// §14 measured that violating this changes the REPORTED CAUSE of an
// unchanged fault population.
property p26_timer_ordering;
  @(posedge clk) disable iff (!rst_n)
    ordering_ok;
endproperty
a_p26: assert property (p26_timer_ordering);
 
// P27 — no two limits are equal.  Equal limits make the reported cause a
// property of the sweep order rather than of the fault.
property p27_no_ambiguous_order;
  @(posedge clk) disable iff (!rst_n)
    !ordering_ambiguous;
endproperty
a_p27: assert property (p27_no_ambiguous_order);
 
// P28 — when the hardware timer has expired, no outer timer reports.
property p28_innermost_reports;
  @(posedge clk) disable iff (!rst_n)
    (req_age >= HW_LIMIT) |-> (fired == cto_dbg_pkg::TMR_HARDWARE);
endproperty
a_p28: assert property (p28_innermost_reports);

// P29 — the first timeout's record is sticky.
property p29_first_sticky;
  @(posedge clk) disable iff (!rst_n)
    (captured && !clear) |=> (captured && $stable(first_cause) && $stable(first_timer));
endproperty
a_p29: assert property (p29_first_sticky);
 
// P30 — the recorded cause is consistent with the recorded byte counts.
// An instrument whose fields contradict each other is worse than none.
property p30_cause_consistent;
  @(posedge clk) disable iff (!rst_n)
    (captured && (first_cause == cto_dbg_pkg::CTO_PARTIAL))
      |-> ((first_got > 0) && (first_got < first_want));
endproperty
a_p30: assert property (p30_cause_consistent);
 
// P31 — every rejection reason is counted separately (mutation 27).
property p31_reasons_distinct;
  @(posedge clk) disable iff (!rst_n)
    cpl_valid |-> $onehot0({cpl_late, cpl_foreign, cpl_orphan});
endproperty
a_p31: assert property (p31_reasons_distinct);

// P32 — a request leaves the outstanding table by exactly one route, and
// that route is recorded.  A request that exits without a recorded cause
// makes §3's five-way classification unavailable for that request forever.
property p32_exit_route_recorded;
  @(posedge clk) disable iff (!rst_n)
    (tbl_live[tag] && !$past(tbl_live[tag])) or
    ($fell(tbl_live[tag]) |-> (retire || timeout_fire));
endproperty
a_p32: assert property (p32_exit_route_recorded);
 
// P32's covers — the rare events must occur, or P14 through P22 never evaluate.
// §13's model required an explicit "very late" traffic class to produce
// any late Completions at all; c3 is the cover that proves the testbench
// has one.
c1_partial_timeout: cover property (@(posedge clk) disable iff (!rst_n)
                      timeout_fire && (timeout_bytes_got > 0) &&
                      (timeout_bytes_got < timeout_bytes_want));
c2_zero_byte_to:    cover property (@(posedge clk) disable iff (!rst_n)
                      timeout_fire && (timeout_bytes_got == 0));
c3_late_cpl:        cover property (@(posedge clk) disable iff (!rst_n) cpl_late);
c4_foreign_rid:     cover property (@(posedge clk) disable iff (!rst_n) cpl_foreign);
c5_orphan_cpl:      cover property (@(posedge clk) disable iff (!rst_n) cpl_orphan);
c6_tag_exhaust:     cover property (@(posedge clk) disable iff (!rst_n) free_count == 0);
c7_bc_violation:    cover property (@(posedge clk) disable iff (!rst_n) bc_violation);
c8_split_series:    cover property (@(posedge clk) disable iff (!rst_n)
                      cpl_accept ##[1:$] cpl_accept ##[1:$] retire);

module ce_a_retire_on_arrival #(parameter int unsigned NTAG = 32)(
  input  logic clk, rst_n,
  input  logic cpl_accept, input logic [4:0] cpl_tag,
  output logic [NTAG-1:0] live
);
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) live <= '0;
    else if (cpl_accept) live[cpl_tag] <= 1'b0;     // <-- any Cpl retires it
endmodule
 
// Failing stimulus: a 256-byte read split at RCB=64 into four Completions.
// Golden: live until the 4th Cpl satisfies the byte count.
// This:   retires on the 1st.  The tag is freed with 192 bytes still in
//         flight, and the remaining three Completions become orphans.
// P6 fails (got < want at retirement).  P7 fails.
// Observable consequence: the requester reports success having received a
// quarter of its data, and 3 orphan Completions arrive for a freed tag.

module ce_b_no_epoch_check (
  input  logic cpl_valid, input logic [15:0] cpl_rid, input logic [15:0] my_rid,
  input  logic tag_is_live, output logic cpl_accept
);
  assign cpl_accept = cpl_valid && (cpl_rid == my_rid) && tag_is_live;
endmodule                                            // <-- no epoch compare
 
// Failing stimulus: request S1 on tag 7 times out; tag 7 is reissued to S2;
// S1's Completion arrives carrying epoch 0 while tag 7's epoch is now 1.
// Golden: cpl_late, discarded and counted.
// This:   accepted, credited to S2.
// P18 fails.  P22 fails (the independent oracle sees serial S1 credited to
// an entry owning serial S2).
// §13 measured this configuration at 39,574 misdeliveries and 1,907,096
// bytes written into wrong buffers.

module ce_c_no_epoch_bump #(parameter int unsigned NTAG = 32)(
  input  logic clk, rst_n, input logic abandon, input logic [4:0] abandon_tag,
  output cto_dbg_pkg::epoch_t ep [NTAG]
);
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) for (int i = 0; i < NTAG; i++) ep[i] <= '0;
    // the abandon path is present, and does NOT touch the epoch
endmodule
 
// Failing stimulus: identical to counterexample B.
// Golden: cpl_late asserts, the Completion is discarded.
// This:   every epoch is permanently 0, so cpl_epoch == cur_epoch ALWAYS.
//         The epoch comparison is present and passes.  The Completion is
//         accepted and credited to S2.
// P19 fails.  P22 fails.  P18 is VACUOUSLY SATISFIED — its antecedent
// (cpl_epoch != cur_epoch) is never true.
// This is the chapter's sharpest result: §13 measured 39,574 misdeliveries
// and 1,907,096 bytes — byte-identical to counterexample B — while the
// late-Completion counter read ZERO.  A diagnostic derived from the
// mechanism it checks is blind exactly where that mechanism fails.

module ce_d_link_gated_age (
  input  logic clk, rst_n, input logic link_active, input logic live,
  output logic [31:0] age
);
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) age <= '0;
    else if (live && link_active) age <= age + 32'd1;   // <-- gated
endmodule
 
// Failing stimulus: the link drops while a request is outstanding.
// Golden: the age continues, the request times out, recovery begins.
// This:   age freezes.  The request NEVER times out.  The requester waits
//         forever for a Completion that cannot arrive, holding its tag.
// P11 fails.  P24 fails (no eventual exit).
// Observable consequence: the exact fault the timer exists to detect is
// the one condition under which the timer stops running.

module ce_e_global_timer (
  input  logic clk, rst_n, input logic any_live, input logic alloc,
  output logic [31:0] age, output logic expire
);
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) age <= '0;
    else if (alloc) age <= '0;              // <-- reset by ANY allocation
    else if (any_live) age <= age + 32'd1;
  assign expire = (age >= 32'd2000);
endmodule
 
// Failing stimulus: a steady stream of short requests alongside one long
// outstanding request.
// Golden: the long request ages independently and times out.
// This:   every new allocation resets the shared age, so the old request
//         never expires while traffic continues.  Under load it never
//         times out at all; when traffic stops, everything times out
//         simultaneously.
// P10 fails (age is not per-request).  P12 fails.
// Observable consequence: timeouts arrive in bursts at idle, attributed to
// whatever was outstanding then — never to the request that actually hung.

module ce_f_merged_reject (
  input  logic clk, rst_n, input logic cpl_valid,
  input  logic rid_bad, epoch_bad, tag_dead,
  output logic [31:0] reject_count
);
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) reject_count <= '0;
    else if (cpl_valid && (rid_bad || epoch_bad || tag_dead))
      reject_count <= reject_count + 32'd1;      // <-- one counter for three
endmodule
 
// Failing stimulus: a run containing foreign-RID Completions, late
// Completions, and Completions for freed tags.
// Golden: three counters — foreign, late, orphan — separately readable.
// This:   one number.  A reading of 8,371 is consistent with a healthy
//         requester discarding late Completions (§13's correct row) AND
//         with a misrouted fabric delivering foreign traffic.
// P31 fails.
// Observable consequence: §3's classes C and the late-Completion path
// become indistinguishable, and §15 case 4's primary evidence is gone.