Timing Violations

   ONE CYCLE INSIDE A SCHEDULER, and what each event would record

   cycle 41   queue entries considered : 6   (candidates)
              legality mask passes     : 3
              policy mask selects      : 1   (grant)
              driven on the bus        : 1   (commit)

   a recorder on `candidate` logs 6 commands for cycle 41.
   a recorder on `grant`     logs 1 -- and logs it even if a later
                                  stage squashed it.
   a recorder on `commit`    logs 1, and only if it actually issued.

   only the third is the event a timing rule is about.

   a read is committed at cycle 4181. three rules apply:

     tRCD  from ACT at 4174 to this bank : earliest legal 4180   ok
     tCCD_L from RD at 4177, same group  : earliest legal 4185   VIOLATED by 4
     tCCD_S from RD at 4179, other group : earliest legal 4183   VIOLATED by 2

   earliest legal = max(4180, 4185, 4183) = 4185.

   a checker that reports only tCCD_S understates the violation by 2
   cycles AND names the wrong rule. A checker that reports only the
   FIRST failing rule it evaluates depends on evaluation order.

   the honest report is the binding constraint -- the maximum -- plus
   every rule that failed. §17's snapshot records both.

   commits, most recent last:

     4170  ACT  bank 0  grp 0
     4173  RD   bank 0  grp 0
     4175  ACT  bank 5  grp 1
     4177  RD   bank 2  grp 0
     4179  RD   bank 5  grp 1
     4181  RD   bank 3  grp 0   <-- the violating command

   "the previous command" is the RD at 4179, bank 5, group 1.
   DIFFERENT group -> tCCD_S applies -> separation 2, and if
   tCCD_S is 2 (ILLUSTRATIVE) this looks LEGAL.

   "the previous column command in the SAME bank group" is the RD at
   4177, bank 2, group 0 -> tCCD_L applies -> separation 4, and if
   tCCD_L is 8 (ILLUSTRATIVE) this is a violation by 4 cycles.

   the same command stream is legal or illegal depending on which
   question the recorder answers.

   device specification figure
        |   a time, or a count, or the MAXIMUM of both  -- §12
        v
   firmware / software value
        |   chosen per frequency bin
        v
   unit conversion   time -> command clocks
        |   DIVIDE by the clock period, then ROUND
        v
   rounding direction
        |   a MINIMUM time must round UP
        v
   register encoding
        |   encoded field, often offset from the true count
        v
   controller interpretation
        |   counted in command clocks, or controller clocks?
        v
   applied separation

   clock period   time term in clocks    count term   binding term
   -----------    -------------------    ----------   ------------
   2.50 ns        ceil(7.5 / 2.50) = 3        4        count  (4)
   1.875 ns       ceil(7.5 / 1.875) = 4       4        equal  (4)
   1.25 ns        ceil(7.5 / 1.25)  = 6       4        time   (6)
   0.9375 ns      ceil(7.5/0.9375)  = 8       4        time   (8)

   a controller that implements ONLY the count term applies 4 at
   every frequency. It is correct at the first two rows and
   violates by 2 and by 4 at the last two.

   a controller that implements ONLY the time term applies 3 at the
   first row, where the count term requires 4 -- so it violates by 1
   at LOW frequency and is correct at high frequency.

// ---------------------------------------------------------------------
// timing_violation_snapshot -- CLASSIFICATION: synthesisable, BINDABLE.
//
// WHAT IT DOES: latches the FIRST timing violation with §3's six
// fields, plus the resource identity of BOTH commands, and counts
// subsequent violations without overwriting the first.
//
// WHY FIRST-WINS: Module 28's laws. A timing violation cascades -- one
// early commit puts every later command in a wrong relationship -- so
// the hundredth violation is a consequence and the first is evidence.
//
// WHY BOTH COMMANDS' RESOURCE FIELDS (§2, §6): a misclassification
// produces a correctly recorded violation of the WRONG rule. Storing
// prev_grp alongside cur_grp is what makes "these were the same group
// and the classifier said otherwise" a readable fact rather than an
// inference.
//
// WHY A RULE MASK AND NOT A RULE ID (§4): earliest legal time is a
// maximum, so several rules can fail at once. Recording one id makes
// the report depend on the evaluator's evaluation order.
//
// WHAT IT CANNOT TELL YOU: whether the rule was the right rule.
//
// SYNTHESIS: one set of capture registers, two counters, no arrays.
// ---------------------------------------------------------------------
module timing_violation_snapshot #(
  parameter int BANKS   = 16,
  parameter int GROUPS  = 4,
  parameter int RULES   = 8,    // one bit per named rule
  parameter int CYC_W   = 32
)(
  input  logic                        clk,
  input  logic                        rst_n,

  // ---- commit interface (observed only; §1 -- never candidate/grant)
  input  logic                        commit,
  input  logic [3:0]                  commit_cmd,
  input  logic [$clog2(BANKS)-1:0]    commit_bank,
  input  logic [$clog2(GROUPS)-1:0]   commit_grp,
  input  logic [CYC_W-1:0]            cycle_now,

  // ---- the violation report from the controller's rule evaluator
  input  logic                        viol,
  input  logic [RULES-1:0]            viol_rule_mask,
  input  logic [15:0]                 viol_required,
  input  logic [15:0]                 viol_observed,
  input  logic [3:0]                  prev_cmd,
  input  logic [$clog2(BANKS)-1:0]    prev_bank,
  input  logic [$clog2(GROUPS)-1:0]   prev_grp,
  input  logic [CYC_W-1:0]            prev_cycle,
  input  logic                        clsf_same_bank,
  input  logic                        clsf_same_group,

  input  logic                        clear,

  // ---- published evidence
  output logic                        valid,
  output logic [RULES-1:0]            snap_rule_mask,
  output logic [15:0]                 snap_required,
  output logic [15:0]                 snap_observed,
  output logic [15:0]                 snap_shortfall,
  output logic [3:0]                  snap_cur_cmd,
  output logic [$clog2(BANKS)-1:0]    snap_cur_bank,
  output logic [$clog2(GROUPS)-1:0]   snap_cur_grp,
  output logic [3:0]                  snap_prev_cmd,
  output logic [$clog2(BANKS)-1:0]    snap_prev_bank,
  output logic [$clog2(GROUPS)-1:0]   snap_prev_grp,
  output logic [CYC_W-1:0]            snap_cur_cycle,
  output logic [CYC_W-1:0]            snap_prev_cycle,
  output logic                        snap_clsf_same_bank,
  output logic                        snap_clsf_same_group,
  output logic                        snap_misclassified,
  output logic [15:0]                 viol_count,
  output logic [RULES-1:0]            rules_ever_violated,
  output logic [RULES-1:0]            rules_ever_applied_in
);
  // $clog2(1) is 0, which makes every index vector illegal as [-1:0].
  // A power-of-two test alone accepts 1, so the bound is explicit.
  initial begin
    if (BANKS  < 2) $fatal(1, "timing_violation_snapshot: BANKS must be >= 2 (got %0d)", BANKS);
    if (GROUPS < 2) $fatal(1, "timing_violation_snapshot: GROUPS must be >= 2 (got %0d)", GROUPS);
    if (RULES  < 1) $fatal(1, "timing_violation_snapshot: RULES must be >= 1");
    if (CYC_W  < 8) $fatal(1, "timing_violation_snapshot: CYC_W must be >= 8");
    if ((BANKS % GROUPS) != 0)
      $fatal(1, "timing_violation_snapshot: %0d banks do not divide into %0d groups", BANKS, GROUPS);
  end

  always_ff @(posedge clk) begin
    if (!rst_n || clear) begin
      valid                <= 1'b0;
      snap_rule_mask       <= '0;
      snap_required        <= '0;
      snap_observed        <= '0;
      snap_shortfall       <= '0;
      snap_cur_cmd         <= '0;
      snap_cur_bank        <= '0;
      snap_cur_grp         <= '0;
      snap_prev_cmd        <= '0;
      snap_prev_bank       <= '0;
      snap_prev_grp        <= '0;
      snap_cur_cycle       <= '0;
      snap_prev_cycle      <= '0;
      snap_clsf_same_bank  <= 1'b0;
      snap_clsf_same_group <= 1'b0;
      snap_misclassified   <= 1'b0;
      viol_count           <= '0;
      rules_ever_violated  <= '0;
      rules_ever_applied_in<= '0;
    end else begin
      // §14: count every violation, saturating rather than wrapping. A
      // wrapped count that reads 3 after 65,539 violations would
      // understate a cascade by four orders of magnitude.
      if (viol && viol_count != 16'hFFFF) viol_count <= viol_count + 1'b1;
      if (viol) rules_ever_violated <= rules_ever_violated | viol_rule_mask;

      // §16 row two: a rule the controller never applies to ANY pair is
      // a rule it does not implement. Accumulating the applied mask
      // makes that a one-query check instead of a code review.
      if (commit) rules_ever_applied_in <= rules_ever_applied_in | viol_rule_mask;

      // ---- FIRST violation wins. Nothing but `clear` releases it.
      if (viol && !valid) begin
        valid                <= 1'b1;
        snap_rule_mask       <= viol_rule_mask;
        snap_required        <= viol_required;
        snap_observed        <= viol_observed;
        // §10: the shortfall distribution separates a boundary
        // convention (always 1) from a parameter or classification
        // problem (a spread). Computed here so it is queryable.
        snap_shortfall       <= (viol_required > viol_observed)
                              ? (viol_required - viol_observed) : 16'd0;
        snap_cur_cmd         <= commit_cmd;
        snap_cur_bank        <= commit_bank;
        snap_cur_grp         <= commit_grp;
        snap_prev_cmd        <= prev_cmd;
        snap_prev_bank       <= prev_bank;
        snap_prev_grp        <= prev_grp;
        snap_cur_cycle       <= cycle_now;
        snap_prev_cycle      <= prev_cycle;
        snap_clsf_same_bank  <= clsf_same_bank;
        snap_clsf_same_group <= clsf_same_group;
        // §6's localization, computed rather than left to a reader:
        // the resource fields say same, the classifier says different.
        // This is the ONE derived bit in the block, and it exists
        // because the comparison is what turns six recorded fields
        // into a named defect.
        snap_misclassified   <= ((commit_bank == prev_bank) && !clsf_same_bank)
                             || ((commit_grp  == prev_grp)  && !clsf_same_group);
      end
    end
  end
endmodule

// ---------------------------------------------------------------------
// commit_history -- CLASSIFICATION: synthesisable, BINDABLE.
//
// A BOUNDED recorder. Not a logic analyser: DEPTH records, oldest
// overwritten, and the loss is PUBLISHED rather than silent.
//
// WHY TWO STRUCTURES (§5): "the previous command" and "the previous
// command on the same resource" are different queries. The
// chronological ring answers the first and gives a human context; the
// per-resource table answers the second, which is the one a timing
// rule needs. Neither substitutes for the other.
//
// WHY SATURATING ELAPSED (§13): a narrow cycle counter that wraps
// computes a SMALL gap from a LONG idle, producing a violation whose
// actual separation was enormous. A saturating elapsed value cannot:
// once a resource has been idle past the widest window, it stays
// legal.
//
// WHY `dropped` IS PUBLISHED (§14): 25.2 establishes that sub-channels
// are independent, so two commits in one cycle are legal. A recorder
// with one write port drops one -- and a recorder that loses evidence
// must say so.
//
// SYNTHESIS: one ring buffer, one per-resource register file, two
// counters. No hierarchical references, no DUT handle.
// ---------------------------------------------------------------------
module commit_history #(
  parameter int DEPTH   = 32,
  parameter int BANKS   = 16,
  parameter int GROUPS  = 4,
  parameter int ELAPS_W = 16      // saturating elapsed width
)(
  input  logic                        clk,
  input  logic                        rst_n,

  input  logic                        commit,        // §1: commit ONLY
  input  logic                        commit_2nd,    // a second commit this cycle
  input  logic [3:0]                  commit_cmd,
  input  logic [$clog2(BANKS)-1:0]    commit_bank,
  input  logic [$clog2(GROUPS)-1:0]   commit_grp,
  input  logic                        commit_is_column, // RD or WR
  input  logic                        clear,

  // ---- per-resource query (combinational read)
  input  logic [$clog2(BANKS)-1:0]    q_bank,
  input  logic [$clog2(GROUPS)-1:0]   q_grp,
  output logic [ELAPS_W-1:0]          q_elapsed_bank,
  output logic [ELAPS_W-1:0]          q_elapsed_grp_col,
  output logic                        q_bank_seen,
  output logic                        q_grp_col_seen,

  // ---- published evidence
  output logic [$clog2(DEPTH)-1:0]    wr_ptr,
  output logic [15:0]                 wrapped,
  output logic [15:0]                 dropped,
  output logic [15:0]                 total_commits
);
  initial begin
    if (DEPTH   < 2) $fatal(1, "commit_history: DEPTH must be >= 2 (got %0d)", DEPTH);
    if (BANKS   < 2) $fatal(1, "commit_history: BANKS must be >= 2");
    if (GROUPS  < 2) $fatal(1, "commit_history: GROUPS must be >= 2");
    if (ELAPS_W < 4) $fatal(1, "commit_history: ELAPS_W must be >= 4");
  end

  localparam logic [ELAPS_W-1:0] ELAPS_MAX = {ELAPS_W{1'b1}};

  // ---- chronological ring: context for a human reading the report
  logic [3:0]                      h_cmd  [DEPTH];
  logic [$clog2(BANKS)-1:0]        h_bank [DEPTH];
  logic [$clog2(GROUPS)-1:0]       h_grp  [DEPTH];
  logic                            h_col  [DEPTH];

  // ---- per-resource elapsed: the query a timing rule actually needs
  logic [ELAPS_W-1:0] e_bank    [BANKS];
  logic [ELAPS_W-1:0] e_grp_col [GROUPS];
  logic               s_bank    [BANKS];
  logic               s_grp_col [GROUPS];

  always_ff @(posedge clk) begin
    if (!rst_n || clear) begin
      wr_ptr        <= '0;
      wrapped       <= '0;
      dropped       <= '0;
      total_commits <= '0;
      // §13: clearing the SEEN flags is what prevents a stale
      // timestamp from being compared against the first command after
      // a reset. Clearing the elapsed values alone would leave
      // "elapsed = 0, seen = 1", which reads as a commit last cycle.
      for (int b = 0; b < BANKS;  b++) begin e_bank[b]    <= '0; s_bank[b]    <= 1'b0; end
      for (int g = 0; g < GROUPS; g++) begin e_grp_col[g] <= '0; s_grp_col[g] <= 1'b0; end
    end else begin
      // ---- age every resource by one cycle, saturating. Done FIRST so
      // a commit this cycle overwrites the aged value below rather
      // than being aged itself.
      for (int b = 0; b < BANKS; b++)
        if (s_bank[b] && e_bank[b] != ELAPS_MAX) e_bank[b] <= e_bank[b] + 1'b1;
      for (int g = 0; g < GROUPS; g++)
        if (s_grp_col[g] && e_grp_col[g] != ELAPS_MAX) e_grp_col[g] <= e_grp_col[g] + 1'b1;

      if (commit) begin
        h_cmd [wr_ptr] <= commit_cmd;
        h_bank[wr_ptr] <= commit_bank;
        h_grp [wr_ptr] <= commit_grp;
        h_col [wr_ptr] <= commit_is_column;
        // Oldest-overwritten ring. `wrapped` counts how many whole
        // laps of context have been lost.
        if (wr_ptr == DEPTH - 1) begin
          wr_ptr  <= '0;
          if (wrapped != 16'hFFFF) wrapped <= wrapped + 1'b1;
        end else wr_ptr <= wr_ptr + 1'b1;

        // Elapsed resets to ZERO on the commit cycle, and because this
        // assignment comes after the ageing loop above, it wins. A
        // rule comparing `q_elapsed` next cycle therefore sees 1, not
        // 0 -- which is §9's convention, made explicit in one place.
        e_bank[commit_bank] <= '0;
        s_bank[commit_bank] <= 1'b1;
        if (commit_is_column) begin
          e_grp_col[commit_grp] <= '0;
          s_grp_col[commit_grp] <= 1'b1;
        end

        if (total_commits != 16'hFFFF) total_commits <= total_commits + 1'b1;
      end

      // §14: a second commit in the same cycle is legal and this
      // recorder cannot store it. Silence would corrupt every later
      // reconstruction; the count makes the gap visible.
      if (commit && commit_2nd && dropped != 16'hFFFF)
        dropped <= dropped + 1'b1;
    end
  end

  // Combinational query. `seen` is separate from `elapsed` because
  // "never committed" and "committed a long time ago" are different
  // answers, and zero cannot represent both -- the same three-valued
  // discipline 27.3 §6 and 28.1 §17 arrived at.
  always_comb begin
    q_elapsed_bank    = e_bank[q_bank];
    q_elapsed_grp_col = e_grp_col[q_grp];
    q_bank_seen       = s_bank[q_bank];
    q_grp_col_seen    = s_grp_col[q_grp];
  end
endmodule

// Bound to §15's snapshot and §16's recorder. Every property carries
// `disable iff (!rst_n)`, and every antecedent is published as a cover
// below -- 27.2 measured this curriculum at 78.53% implications, so a
// silent pass is otherwise indistinguishable from an unbound checker.
module timing_debug_sva #(
  parameter int RULES = 8,
  parameter int DEPTH = 32
)(
  input logic clk, rst_n, clear,
  input logic commit, commit_2nd, viol,
  input logic [RULES-1:0] viol_rule_mask, snap_rule_mask, rules_ever_violated,
  input logic [15:0] viol_required, viol_observed,
  input logic [15:0] snap_required, snap_observed, snap_shortfall,
  input logic [15:0] viol_count, wrapped, dropped, total_commits,
  input logic valid, snap_misclassified,
  input logic [$clog2(DEPTH)-1:0] wr_ptr,
  input logic q_bank_seen, q_grp_col_seen,
  input logic [15:0] q_elapsed_bank
);
  // ---- P1. FIRST VIOLATION WINS. Nothing but `clear` changes the
  // snapshot. A timing violation cascades, so the hundredth record is
  // a consequence and the first is the evidence.
  property p_first_violation_sticky;
    @(posedge clk) disable iff (!rst_n)
      (valid && !clear) |=> (snap_rule_mask == $past(snap_rule_mask)
                          && snap_required  == $past(snap_required)
                          && snap_observed  == $past(snap_observed));
  endproperty
  assert property (p_first_violation_sticky)
    else $error("snapshot: a later violation overwrote the first");

  // ---- P2. FORBIDDEN. A later violation must not clear `valid`.
  property p_valid_sticky;
    @(posedge clk) disable iff (!rst_n)
      (valid && !clear) |=> valid;
  endproperty
  assert property (p_valid_sticky)
    else $error("snapshot: valid dropped without a clear");

  // ---- P3. Clear releases. A latch with no release silently stops
  // recording after the first failure of the first boot.
  property p_clear_releases;
    @(posedge clk) disable iff (!rst_n)
      clear |=> (!valid && snap_rule_mask == '0);
  endproperty
  assert property (p_clear_releases)
    else $error("snapshot: clear did not release");

  // ---- P4. The snapshot captures on the FIRST violation, and the
  // captured mask is that violation's mask -- not a later one's.
  property p_capture_is_first;
    @(posedge clk) disable iff (!rst_n)
      (viol && !valid) |=> (snap_rule_mask == $past(viol_rule_mask));
  endproperty
  assert property (p_capture_is_first)
    else $error("snapshot: captured mask is not the first violation's");

  // ---- P5. §10's shortfall is required minus observed, and never
  // negative. A negative shortfall would mean the evaluator reported a
  // violation on a command that met its requirement.
  property p_shortfall_arithmetic;
    @(posedge clk) disable iff (!rst_n)
      valid |-> (snap_shortfall == ((snap_required > snap_observed)
                                    ? (snap_required - snap_observed) : 16'd0));
  endproperty
  assert property (p_shortfall_arithmetic)
    else $error("snapshot: shortfall %0d inconsistent with %0d/%0d",
                snap_shortfall, snap_required, snap_observed);

  // ---- P6. FORBIDDEN. A violation is never reported with observed
  // greater than or equal to required. That combination means the rule
  // evaluator and the snapshot disagree about what failed.
  property p_violation_is_a_shortfall;
    @(posedge clk) disable iff (!rst_n)
      viol |-> (viol_observed < viol_required);
  endproperty
  assert property (p_violation_is_a_shortfall)
    else $error("violation reported with observed %0d >= required %0d",
                viol_observed, viol_required);

  // ---- P7. FORBIDDEN. A violation always names at least one rule. A
  // zero mask is a violation that localises nothing -- §3 field 6.
  property p_violation_names_a_rule;
    @(posedge clk) disable iff (!rst_n)
      viol |-> (viol_rule_mask != '0);
  endproperty
  assert property (p_violation_names_a_rule)
    else $error("violation reported with an empty rule mask");

  // ---- P8. The accumulated mask is monotone: a rule once violated
  // stays recorded. §14 row two depends on the accumulation.
  property p_ever_violated_monotone;
    @(posedge clk) disable iff (!rst_n)
      (!clear) |=> ((rules_ever_violated & $past(rules_ever_violated))
                    == $past(rules_ever_violated));
  endproperty
  assert property (p_ever_violated_monotone)
    else $error("rules_ever_violated lost a bit");

  // ---- P9. INVARIANT. viol_count saturates and never wraps. A
  // wrapped count reading 3 after 65,539 violations would understate a
  // cascade by four orders of magnitude.
  property p_count_saturates;
    @(posedge clk) disable iff (!rst_n)
      (viol_count == 16'hFFFF) |=> (viol_count == 16'hFFFF);
  endproperty
  assert property (p_count_saturates)
    else $error("viol_count wrapped past saturation");

  // ---- P10. FORBIDDEN. The ring pointer never leaves its range.
  property p_wr_ptr_in_range;
    @(posedge clk) disable iff (!rst_n)
      (wr_ptr < DEPTH);
  endproperty
  assert property (p_wr_ptr_in_range)
    else $error("history: wr_ptr %0d outside DEPTH", wr_ptr);

  // ---- P11. FORBIDDEN. A dropped commit is counted, never silent.
  // §14: two commits in one cycle are legal, and a recorder that
  // loses one must say so.
  property p_second_commit_counted;
    @(posedge clk) disable iff (!rst_n)
      (commit && commit_2nd && dropped != 16'hFFFF)
        |=> (dropped == $past(dropped) + 1);
  endproperty
  assert property (p_second_commit_counted)
    else $error("history: a second commit in one cycle was dropped silently");

  // ---- P12. FORBIDDEN. `elapsed` is meaningless while `seen` is
  // false, so nothing may read a zero elapsed as "committed last
  // cycle" on an unseen resource. §13's reset boundary.
  property p_unseen_resource_has_no_elapsed_meaning;
    @(posedge clk) disable iff (!rst_n)
      (!q_bank_seen) |-> (q_elapsed_bank == 16'd0);
  endproperty
  assert property (p_unseen_resource_has_no_elapsed_meaning)
    else $error("history: an unseen resource reported a non-zero elapsed");

  // ---- 27.2 §7: publish every antecedent.
  cover property (@(posedge clk) disable iff (!rst_n) commit);
  cover property (@(posedge clk) disable iff (!rst_n) commit && commit_2nd);
  cover property (@(posedge clk) disable iff (!rst_n) viol);
  cover property (@(posedge clk) disable iff (!rst_n) viol && !valid);
  cover property (@(posedge clk) disable iff (!rst_n) viol &&  valid);
  cover property (@(posedge clk) disable iff (!rst_n) clear);
  cover property (@(posedge clk) disable iff (!rst_n) valid && snap_misclassified);
  cover property (@(posedge clk) disable iff (!rst_n) valid && snap_shortfall == 16'd1);
  cover property (@(posedge clk) disable iff (!rst_n) valid && snap_shortfall >  16'd1);
  cover property (@(posedge clk) disable iff (!rst_n) wrapped != 16'd0);
  cover property (@(posedge clk) disable iff (!rst_n) dropped != 16'd0);
  cover property (@(posedge clk) disable iff (!rst_n) viol_count == 16'hFFFF);
  cover property (@(posedge clk) disable iff (!rst_n) !q_bank_seen);
  cover property (@(posedge clk) disable iff (!rst_n) $countones(viol_rule_mask) > 1);
endmodule

// SIMULATION-ONLY. Independent reference: it stores commits in a
// QUEUE and answers "previous on this resource" by SEARCHING BACKWARD,
// rather than maintaining per-resource registers incrementally. A
// different algorithm, so agreement is evidence -- 27.4 §15's argument.
class history_reference;
  typedef struct {
    int cyc; int cmd; int bank; int grp; bit col;
  } rec_t;
  rec_t log[$];

  function void commit(int cyc, int cmd, int bank, int grp, bit col);
    rec_t r; r.cyc = cyc; r.cmd = cmd; r.bank = bank; r.grp = grp; r.col = col;
    log.push_back(r);
  endfunction

  // §5: the previous COLUMN command in the same bank GROUP -- not the
  // previous command. Returns -1 when none exists, so "never" is a
  // distinct answer from "cycle 0".
  function int prev_col_in_group(int grp, int before_cyc);
    for (int i = log.size() - 1; i >= 0; i--)
      if (log[i].col && log[i].grp == grp && log[i].cyc < before_cyc)
        return log[i].cyc;
    return -1;
  endfunction

  function int prev_in_bank(int bank, int before_cyc);
    for (int i = log.size() - 1; i >= 0; i--)
      if (log[i].bank == bank && log[i].cyc < before_cyc) return log[i].cyc;
    return -1;
  endfunction

  // §4: earliest legal time is a MAXIMUM over applicable rules, and
  // the binding rule is the one that produced it. Returns both, so a
  // test can assert the report named the binding rule and not the
  // first-evaluated one.
  function void earliest_legal(int this_cyc, int bank, int grp,
                               int t_same_bank, int t_ccd_l, int t_ccd_s,
                               output int earliest, output int binding);
    int cands[$]; int rules[$]; int pb, pg;
    earliest = 0; binding = -1;
    pb = prev_in_bank(bank, this_cyc);
    if (pb >= 0) begin cands.push_back(pb + t_same_bank); rules.push_back(0); end
    pg = prev_col_in_group(grp, this_cyc);
    if (pg >= 0) begin cands.push_back(pg + t_ccd_l);     rules.push_back(1); end
    foreach (cands[i])
      if (cands[i] > earliest) begin earliest = cands[i]; binding = rules[i]; end
  endfunction

  // §9's convention, written where a reader can see it: legal when the
  // commit cycle is at or after the earliest legal cycle.
  function bit legal(int this_cyc, int earliest);
    return this_cyc >= earliest;
  endfunction
endclass

  TWO PASSING TIMING-DEBUG REPORTS

  (A) the snapshot was never wired to a running scheduler
        p_first_violation_sticky            PASS
        p_valid_sticky                      PASS
        p_capture_is_first                  PASS
        p_violation_is_a_shortfall          PASS
        p_violation_names_a_rule            PASS
        ... all 12 properties               PASS
        ------------------------------------------------
        cover commit                        0 hits
        cover viol                          0 hits
        cover valid && snap_misclassified   0 hits
        ... all 14 covers                   0 hits

        eight of the twelve properties are implications and never
        armed. The four INVARIANTS -- shortfall arithmetic on an
        invalid snapshot, pointer range, count saturation, unseen
        elapsed -- also pass, correctly, on a block at reset.

        a boot log reading "timing: no violations" is produced by
        this run AND by a clean one.

  (B) the recorder was wired to `candidate` instead of `commit`
        stimulus : full traffic; the history binding uses the
                   scheduler's candidate-valid signal
        all 12 properties                   PASS
        all 14 covers                       HIT
        viol_count                          1,284
        snap_misclassified                  0
        ------------------------------------------------
        snap_prev_cmd / snap_prev_cycle refer to a command that
        never appeared on the bus.

        every property passes and every antecedent armed, so the
        instrument looks healthy. And §1 says a scheduler evaluates
        several candidates per cycle and commits at most one, so the
        recorder holds commands that were considered and rejected.
        Every reconstruction built on it names a wrong previous
        command, which reads as a device timing problem.

    diagnosis : (A) is 27.2's vacuity argument -- the covers are the
      only thing separating a working snapshot from an unbound one.
      (B) is §1, and NO property can catch it: the signal is
      well-formed, the arithmetic is consistent, and only the
      binding is wrong.

    the fix : (A) read the covers. (B) cross-check the recorder's
      total_commits against a bus-level count of commands actually
      driven. A recorder on `candidate` reports several times more
      commits than the bus carried, and that ratio is the detector.