PHY Review Checklist

// ILLUSTRATIVE quantities. ROBUST BUILD: provenance is a declared
// property of each quantity, and the launch offset is the sum of a
// calculated term and a measured term -- 19.3 section 2's decomposition,
// made structural so a review can audit it.
module quantity_provenance #(
    parameter int OFF_W        = 8,
    // CALCULATED side: reproducible from programmed state.
    parameter int CWL_CYCLES   = 9,      // 14.10's programmed value
    parameter int SER_CYCLES   = 2,      // 19.2's serialiser depth
    // MEASURED side: MUST arrive as an input. There is no default,
    // because a default is a calculated value wearing a measured name.
    parameter bit ALLOW_CALC_FLIGHT = 1'b0
)(
    input  logic                 clk,
    input  logic                 rst_n,
    // programmed configuration
    input  logic [3:0]           cfg_cwl,
    input  logic [1:0]           cfg_ser_depth,
    // measured, from training
    input  logic [OFF_W-1:0]     trained_flight,
    input  logic                 trained_flight_valid,
    // a quantity the reviewer must classify: does it belong to either side?
    input  logic [OFF_W-1:0]     board_trace_delay,   // never used: see below
    output logic [OFF_W-1:0]     launch_offset,
    output logic                 launch_offset_valid,
    // the census, exposed so a review can read it rather than infer it
    output logic [2:0]           calc_terms,
    output logic [2:0]           meas_terms,
    output logic [2:0]           unclassified_terms
);
  // Provenance enum, structural: 0 = calculated, 1 = measured.
  localparam int NQ = 3;
  localparam bit [NQ-1:0] PROVENANCE = 3'b100;  // {flight, ser, cwl}

  logic [OFF_W-1:0] calc_part, meas_part;

  always_comb begin
    // CALCULATED: from programmed registers, not from parameters. A
    // parameter here would make the term un-reprogrammable, which is
    // 33.2 section 12's finding in a different costume.
    calc_part = OFF_W'(cfg_cwl) + OFF_W'(cfg_ser_depth);

    // MEASURED: from the training input, and ONLY from it.
    meas_part = trained_flight;
  end

  // The census. Counted from PROVENANCE so it cannot drift from the
  // declaration, and unclassified is computed as a residue -- the whole
  // point of section 5's third row.
  always_comb begin
    calc_terms         = 3'(NQ - $countones(PROVENANCE));
    meas_terms         = 3'($countones(PROVENANCE));
    // board_trace_delay contributes to a timing decision and appears on
    // neither side. In the robust build it is REFUSED rather than used.
    unclassified_terms = (board_trace_delay != '0) ? 3'd1 : 3'd0;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      launch_offset       <= '0;
      launch_offset_valid <= 1'b0;
    end else begin
      launch_offset       <= calc_part + meas_part;
      // Refuses while the measured term has no provenance.
      launch_offset_valid <= trained_flight_valid && !ALLOW_CALC_FLIGHT;
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK BUILD: the measured term is computed.
// Set ALLOW_CALC_FLIGHT = 1 and the module derives flight time from the
// clock period and a trace length -- dimensionally correct, reproducible,
// and wrong on every board but the one it was characterised on.
//
//   FLIGHT_NS  = TRACE_MM * PROP_NS_PER_MM      // ILLUSTRATIVE
//   flight_cyc = FLIGHT_NS / CLK_PERIOD_NS
//
// The expression is defensible on a whiteboard. That is the problem:
// it makes `trained_flight` redundant, so nobody notices it is unread.
//
// CONTRACT VIOLATED: 19.3 section 2 -- the measured term is the part that
// is "only knowable by measurement". A formula is not a measurement.
//
// WHY IT SURVIVES: on the characterisation board the two agree to within
// one tap, the census reports three classified terms and zero
// unclassified, and `launch_offset_valid` asserts without training.
// The part boots FASTER than the robust build.
//
// TRACE (ILLUSTRATIVE, PROP_NS_PER_MM = 6.5e-3, CLK_PERIOD_NS = 0.625):
//   board A: TRACE_MM = 48 -> flight_cyc = 0.499 -> 0  trained = 0  SAME
//   board B: TRACE_MM = 48 (assumed) but actual 96
//                          -> flight_cyc = 0       trained = 1  DIFFER
//   -> launch_offset low by 1 cycle on every write on board B.

// ROBUST BUILD: completion is FOUR separate facts, because collapsing
// them is 28.4's finding. The names are chosen to be un-aliasable.
module completion_semantics #(
    parameter int VAL_W    = 8,
    parameter int TIMEOUT  = 64,     // ILLUSTRATIVE
    parameter int STALE_AT = 512     // ILLUSTRATIVE ticks
)(
    input  logic             clk,
    input  logic             rst_n,
    input  logic             start,
    // from the search engine
    input  logic             engine_returned,   // the step finished running
    input  logic             engine_converged,  // it found a point
    input  logic [VAL_W-1:0] engine_value,
    input  logic             engine_in_range,   // the point was inside the sweep
    input  logic             tick,              // ILLUSTRATIVE staleness clock
    input  logic             env_changed,       // e.g. a thermal event
    // four distinct outputs, deliberately not one
    output logic             ran,        // case 1 vs 2: did it even run?
    output logic             converged,  // case 3: did it find a point?
    output logic             in_range,   // case 4: was the point reachable?
    output logic             trusted,    // case 5: is it still true?
    output logic [VAL_W-1:0] value,
    output logic [2:0]       fail_case   // 0 = none; 1..5 = 28.4's cases
);
  logic [$clog2(TIMEOUT+1)-1:0]  busy_cnt;
  logic [$clog2(STALE_AT+1)-1:0] age;
  logic                          running;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      ran <= 1'b0; converged <= 1'b0; in_range <= 1'b0; trusted <= 1'b0;
      value <= '0; fail_case <= 3'd0; busy_cnt <= '0; age <= '0;
      running <= 1'b0;
    end else begin
      if (start) begin
        running   <= 1'b1;
        busy_cnt  <= '0;
        ran       <= 1'b0; converged <= 1'b0;
        in_range  <= 1'b0; trusted   <= 1'b0;
        fail_case <= 3'd0;
      end

      if (running) begin
        busy_cnt <= busy_cnt + 1'b1;

        if (engine_returned) begin
          running   <= 1'b0;
          ran       <= 1'b1;
          converged <= engine_converged;
          in_range  <= engine_in_range;
          value     <= engine_value;
          age       <= '0;
          // trusted requires ALL of the preceding facts, and nothing else
          // may raise it.
          trusted   <= engine_converged && engine_in_range;

          if      (!engine_converged && !engine_in_range) fail_case <= 3'd4;
          else if (!engine_converged)                     fail_case <= 3'd3;
          else                                            fail_case <= 3'd0;
        end else if (busy_cnt == TIMEOUT[$clog2(TIMEOUT+1)-1:0]) begin
          // Case 2: the step never completed. Distinguished from case 1
          // (never started) by `ran` staying low with `busy_cnt` high.
          running   <= 1'b0;
          ran       <= 1'b1;
          fail_case <= 3'd2;
        end
      end

      // Case 5: it converged, it was in range, and it STOPPED being true.
      // 19.5 section 4's continuous side: a value can become invalid without
      // anything failing.
      if (trusted) begin
        if (env_changed) begin
          trusted   <= 1'b0;
          fail_case <= 3'd5;
        end else if (tick) begin
          if (age == STALE_AT[$clog2(STALE_AT+1)-1:0]) begin
            trusted   <= 1'b0;
            fail_case <= 3'd5;
          end else begin
            age <= age + 1'b1;
          end
        end
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK BUILD: one flag, raised on return.
//
//   always_ff @(posedge clk or negedge rst_n)
//     if (!rst_n)              calib_done <= 1'b0;
//     else if (engine_returned) calib_done <= 1'b1;   // <-- the defect
//
// CONTRACT VIOLATED: 28.4 section 2 -- `done` must not mean "returned".
//
// WHY IT SURVIVES: on the bench the engine converges, in range, and
// nothing changes thermally during the test. `calib_done` is high for
// the correct reason, so every consumer behaves correctly. The flag is
// not wrong; it is UNDERDETERMINED.
//
// TRACE, five stimuli (ILLUSTRATIVE):
//   case 1 never started      robust: ran=0            weak: done=0  SAME
//   case 2 hung, timed out    robust: ran=1 fc=2       weak: done=1  DIFFER
//   case 3 returned, no point robust: converged=0 fc=3 weak: done=1  DIFFER
//   case 4 point out of range robust: in_range=0 fc=4  weak: done=1  DIFFER
//   case 5 converged, drifted robust: trusted=0 fc=5   weak: done=1  DIFFER
//
//   distinguishable cases: robust 5 of 5, weak 1 of 5.

// ROBUST BUILD: refusal is the reset state, and the gate is closed by
// a value that cannot be produced by a stuck-at-zero fault on the
// validity input.
module untrained_refusal #(
    parameter int OFF_W = 8
)(
    input  logic             clk,
    input  logic             rst_n,
    input  logic [OFF_W-1:0] trained_offset,
    input  logic             trained_valid,
    input  logic             op_request,
    output logic             op_grant,
    output logic [OFF_W-1:0] offset_in_use,
    output logic             gate_open,
    // telemetry: 19.5's lifecycle, made countable
    output logic [15:0]      untrained_attempts,
    output logic [15:0]      granted_ops
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      // The whole item is these three lines.
      gate_open          <= 1'b0;
      offset_in_use      <= '0;
      untrained_attempts <= '0;
      granted_ops        <= '0;
      op_grant           <= 1'b0;
    end else begin
      // The gate tracks validity in BOTH directions -- 28.4's case 5
      // means a trained value can stop being trusted, so the gate must
      // be able to reclose.
      gate_open <= trained_valid;

      if (trained_valid) offset_in_use <= trained_offset;

      op_grant <= op_request && gate_open;

      if (op_request && !gate_open) untrained_attempts <= untrained_attempts + 1'b1;
      if (op_request &&  gate_open) granted_ops        <= granted_ops + 1'b1;
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK BUILD: the gate opens at reset and
// closes on invalidity.
//
//   if (!rst_n)  gate_open <= 1'b1;            // <-- the defect
//   else         gate_open <= trained_valid;
//
// CONTRACT VIOLATED: 19.5 section 2 -- a PHY is not usable at reset release.
//
// WHY IT SURVIVES: `gate_open` is corrected on the first clock after
// reset, so the window is ONE CYCLE WIDE, and the boot ROM does not
// issue a transaction in it. The defect is invisible unless something
// changes the boot sequence -- a faster ROM, a warm reset that does not
// re-run the ROM, or a debug flow that drives traffic early.
//
// TRACE (ILLUSTRATIVE, 4 requests at t = 0, 1, 40, 41; training at t = 20):
//   robust: untrained_attempts = 2  granted_ops = 2  -> refused both early
//   weak:   untrained_attempts = 1  granted_ops = 3  -> ONE early op granted
//                                                       with offset_in_use = 0
//   gap: one operation, executed with a reset-value delay, no error raised.

// ROBUST BUILD: trained state lives in the POR domain, and the POR
// domain is the one that triggers retraining. The two facts are tied
// together by construction, not by a comment.
module reset_domain_map #(
    parameter int OFF_W = 8
)(
    input  logic             clk,
    input  logic             rst_por_n,    // cold: clears trained state
    input  logic             rst_func_n,   // warm: does not
    input  logic [OFF_W-1:0] trained_offset_in,
    input  logic             training_done,
    input  logic             op_request,
    output logic             retrain_req,
    output logic [OFF_W-1:0] trained_offset,
    output logic             trained_valid,
    output logic             op_grant,
    output logic [7:0]       training_runs,
    output logic [7:0]       ops_with_stale_offset
);
  // TRAINED STATE: POR domain only. A warm reset does not appear in
  // this sensitivity list, which is the entire mechanism.
  always_ff @(posedge clk or negedge rst_por_n) begin
    if (!rst_por_n) begin
      trained_offset <= '0;
      trained_valid  <= 1'b0;
      training_runs  <= '0;
    end else begin
      if (training_done) begin
        trained_offset <= trained_offset_in;
        trained_valid  <= 1'b1;
        training_runs  <= training_runs + 1'b1;
      end
    end
  end

  // RETRAIN TRIGGER: also POR domain. Same reset, so the clear and the
  // replacement cannot get out of step.
  always_ff @(posedge clk or negedge rst_por_n) begin
    if (!rst_por_n)          retrain_req <= 1'b1;   // cleared -> retrain
    else if (training_done)  retrain_req <= 1'b0;
  end

  // FUNCTIONAL STATE: warm domain. Traffic is re-gated on the warm
  // reset, but the trained value it uses is untouched.
  always_ff @(posedge clk or negedge rst_func_n) begin
    if (!rst_func_n) begin
      op_grant              <= 1'b0;
      ops_with_stale_offset <= '0;
    end else begin
      op_grant <= op_request && trained_valid;
      // Telemetry the reviewer asked for: an operation granted while the
      // offset is the reset value is the escape, counted.
      if (op_request && trained_valid && (trained_offset == '0))
        ops_with_stale_offset <= ops_with_stale_offset + 1'b1;
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK BUILD: trained state moves into the
// functional domain, and the retrain trigger does not follow it.
//
//   always_ff @(posedge clk or negedge rst_func_n) begin   // <-- moved
//     if (!rst_func_n) begin
//       trained_offset <= '0;
//       trained_valid  <= 1'b0;          // cleared by a WARM reset
//     end ...
//   always_ff @(posedge clk or negedge rst_por_n)
//     if (!rst_por_n) retrain_req <= 1'b1;                 // <-- not moved
//
// CONTRACT VIOLATED: 19.5 section 2's cold-boot / warm-reset divergence.
//
// WHY IT SURVIVES: cold boot asserts BOTH resets, so `trained_valid`
// clears and `retrain_req` rises together. Every cold boot is perfect.
// Bring-up tests cold-boot. So does the regression.
//
// TRACE (ILLUSTRATIVE):
//   cold boot:  trained_valid 0 -> retrain_req 1 -> train -> valid 1
//               robust and weak IDENTICAL.
//   warm reset after training:
//     robust: trained_valid stays 1, trained_offset preserved,
//             training_runs = 1, ops_with_stale_offset = 0
//     weak:   trained_valid -> 0, trained_offset -> 0, retrain_req
//             stays 0 (POR did not fire), and `trained_valid` re-raises
//             only if `training_done` ever pulses again -- it does not.
//             -> the gate stays CLOSED and the interface is dead,
//                OR, if the gate defaults open (item 3's weak build),
//                every subsequent operation uses offset 0.
//
//   gap: cold boots to failure = 0; warm resets to failure = 1.

// ROBUST BUILD: the interval timer REQUESTS; the preconditions GRANT.
// Separating them is the whole item.
module recal_preconditions #(
    parameter int INTERVAL   = 256,   // ILLUSTRATIVE ticks
    parameter int QUIET_FOR  = 8,     // ILLUSTRATIVE idle cycles required
    parameter int VAL_W      = 8
)(
    input  logic             clk,
    input  logic             rst_n,
    input  logic             tick,
    input  logic             bus_busy,
    input  logic             thermal_settling,   // a second precondition
    input  logic [VAL_W-1:0] measured_value,
    input  logic             measurement_done,
    output logic             recal_start,
    output logic [VAL_W-1:0] committed_value,
    output logic [15:0]      recals_started,
    output logic [15:0]      recals_deferred,
    output logic [15:0]      commits_under_traffic
);
  logic [$clog2(INTERVAL+1)-1:0]  ivl;
  logic [$clog2(QUIET_FOR+1)-1:0] quiet;
  logic                           pending, running;

  // Preconditions, named once and used once. A reviewer can point at
  // this expression and at the list it came from.
  wire preconditions_met = (quiet == QUIET_FOR[$clog2(QUIET_FOR+1)-1:0])
                        && !bus_busy
                        && !thermal_settling;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      ivl <= '0; quiet <= '0; pending <= 1'b0; running <= 1'b0;
      recal_start <= 1'b0; committed_value <= '0;
      recals_started <= '0; recals_deferred <= '0;
      commits_under_traffic <= '0;
    end else begin
      recal_start <= 1'b0;

      // Quiet-window tracker.
      if (bus_busy) quiet <= '0;
      else if (quiet != QUIET_FOR[$clog2(QUIET_FOR+1)-1:0]) quiet <= quiet + 1'b1;

      // The timer only ever sets `pending`. It never starts anything.
      if (tick) begin
        if (ivl == INTERVAL[$clog2(INTERVAL+1)-1:0]) begin
          ivl     <= '0;
          pending <= 1'b1;
        end else begin
          ivl <= ivl + 1'b1;
        end
      end

      // Deferral is counted, because an unbounded deferral is its own
      // defect and a reviewer must be able to see it.
      if (pending && !running) begin
        if (preconditions_met) begin
          pending        <= 1'b0;
          running        <= 1'b1;
          recal_start    <= 1'b1;
          recals_started <= recals_started + 1'b1;
        end else if (tick) begin
          recals_deferred <= recals_deferred + 1'b1;
        end
      end

      if (running && measurement_done) begin
        running <= 1'b0;
        // Commit only if the preconditions held for the WHOLE measurement.
        if (preconditions_met) committed_value <= measured_value;
        else commits_under_traffic <= commits_under_traffic + 1'b1;
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK BUILD: the timer starts the measurement.
//
//   if (tick && (ivl == INTERVAL)) begin
//     ivl <= '0; recal_start <= 1'b1; running <= 1'b1;   // <-- the defect
//   end
//   if (running && measurement_done) committed_value <= measured_value;
//
// CONTRACT VIOLATED: the measurement's own validity conditions. Not a
// timing rule, not a protocol rule -- a MEASUREMENT rule, which is why
// no protocol checker catches it.
//
// WHY IT SURVIVES: it is more robust-looking than the robust build. It
// never defers, never stalls, never reports a deferral, and always
// commits on schedule. `recals_started` matches the expected count
// exactly, which is what a reviewer checks.
//
// TRACE (ILLUSTRATIVE, 8 intervals, bus busy during 3 of them):
//   robust: recals_started = 5  recals_deferred = 3
//           commits_under_traffic = 0   committed_value: always valid
//   weak:   recals_started = 8  recals_deferred = 0
//           commits_under_traffic = 3   committed_value: 3 of 8 measured
//                                       under traffic and committed anyway
//
//   gap: 3 of 8 commits (37.5%) are measurements of the wrong thing.

// ROBUST BUILD: one sweep, five distinguishable outcomes.
module search_range_adequacy #(
    parameter int TAPS      = 32,    // ILLUSTRATIVE sweep width
    parameter int TAP_W     = 5,
    parameter int HW_TAPS   = 64     // ILLUSTRATIVE hardware range
)(
    input  logic             clk,
    input  logic             rst_n,
    input  logic             start,
    input  logic             prereq_done,     // 21.5's dependency structure
    input  logic             probe_valid,
    input  logic             probe_pass,
    input  logic             classifier_alive, // did the observable ever move?
    output logic [TAP_W-1:0] tap,
    output logic             probe_req,
    output logic             done,
    output logic             found,
    output logic [TAP_W-1:0] best_tap,
    // the five outcomes, as separate bits
    output logic             err_prereq,       // cause: unfinished prerequisite
    output logic             err_classifier,   // cause: stuck observable
    output logic             range_exhausted,  // cause: mis-programmed range
    output logic             edge_at_low,      // pass region touched tap 0
    output logic             edge_at_high,     // pass region touched TAPS-1
    output logic [TAP_W:0]   pass_count
);
  logic sweeping;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tap <= '0; probe_req <= 1'b0; sweeping <= 1'b0;
      done <= 1'b0; found <= 1'b0; best_tap <= '0;
      err_prereq <= 1'b0; err_classifier <= 1'b0;
      range_exhausted <= 1'b0; edge_at_low <= 1'b0; edge_at_high <= 1'b0;
      pass_count <= '0;
    end else begin
      probe_req <= 1'b0;

      if (start) begin
        done <= 1'b0; found <= 1'b0; pass_count <= '0;
        err_prereq <= 1'b0; err_classifier <= 1'b0;
        range_exhausted <= 1'b0; edge_at_low <= 1'b0; edge_at_high <= 1'b0;
        // The prerequisite check is BEFORE the sweep, so a prerequisite
        // failure cannot masquerade as a margin failure.
        if (!prereq_done) begin
          err_prereq <= 1'b1;
          done       <= 1'b1;
        end else begin
          tap      <= '0;
          sweeping <= 1'b1;
        end
      end

      if (sweeping && !probe_valid) probe_req <= 1'b1;

      if (sweeping && probe_valid) begin
        if (probe_pass) begin
          pass_count <= pass_count + 1'b1;
          if (!found) begin found <= 1'b1; best_tap <= tap; end
          if (tap == '0)                                  edge_at_low  <= 1'b1;
          if (tap == TAP_W'(TAPS-1))                      edge_at_high <= 1'b1;
        end

        if (tap == TAP_W'(TAPS-1)) begin
          sweeping <= 1'b0;
          done     <= 1'b1;
          // Stuck observable: not one probe ever differed from another.
          if (!classifier_alive) err_classifier <= 1'b1;
          // Range exhausted: nothing passed AND the hardware has range
          // this sweep did not use. That second clause is the item --
          // "nothing passed" alone does not distinguish the causes.
          else if (!found && (TAPS < HW_TAPS)) range_exhausted <= 1'b1;
        end else begin
          tap <= tap + 1'b1;
        end
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK BUILD: one failure bit.
//
//   if (tap == TAPS-1) begin
//     done <= 1'b1;
//     failed <= !found;            // <-- the defect: one code, five causes
//   end
//
// and the prerequisite is checked NOWHERE, so an unfinished prerequisite
// runs the sweep and reports a margin failure.
//
// CONTRACT VIOLATED: 28.1 section 4's failure-domain split -- a search
// defect, an observation defect, a configuration defect, a stale-state
// defect, an ordering defect and a margin problem are six domains, and
// `failed` is one bit.
//
// WHY IT SURVIVES: `failed` is CORRECT. Nothing passed, so the search
// failed. The defect is not a wrong value; it is a report with less
// information than the design had. And on the bench, where the range is
// right and the prerequisites run in order, `failed` never asserts.
//
// TRACE (ILLUSTRATIVE, five stimuli):
//   prereq not done      robust: err_prereq=1        weak: failed=1
//   classifier stuck     robust: err_classifier=1    weak: failed=1
//   range 32 of 64 taps  robust: range_exhausted=1   weak: failed=1
//   genuine no-margin    robust: all clear, found=0  weak: failed=1
//   pass region at edge  robust: found=1 edge_at_high=1  weak: found=1
//
//   distinguishable causes: robust 4 of 4 failures; weak 1 of 4.
//   And row 5: the weak build reports SUCCESS with the answer against
//   the end of the sweep -- a pass region that is probably wider than
//   the range, i.e. an unmeasured margin reported as a measured one.

// ROBUST BUILD: the selection rule is a parameter of the SEARCH, and
// each search declares its region shape.
module selection_rule_shape #(
    parameter int TAPS   = 32,
    parameter int TAP_W  = 5,
    // 0 = two-sided (centre it); 1 = one-sided (offset from the edge)
    parameter bit ONE_SIDED = 1'b0,
    parameter int LEAD_TAPS = 3      // ILLUSTRATIVE, 19.4's LEAD_CYCLES analogue
)(
    input  logic               clk,
    input  logic               rst_n,
    input  logic [TAPS-1:0]    pass_map,
    input  logic               map_valid,
    output logic [TAP_W-1:0]   chosen_tap,
    output logic               chosen_valid,
    output logic [TAP_W-1:0]   region_low,
    output logic [TAP_W-1:0]   region_high,
    output logic               chosen_in_region,
    output logic [TAP_W:0]     margin_to_fail
);
  logic [TAP_W-1:0] lo, hi;
  logic             any;

  always_comb begin
    lo  = '0; hi = '0; any = 1'b0;
    for (int i = 0; i < TAPS; i++) begin
      if (pass_map[i]) begin
        if (!any) begin lo = TAP_W'(i); any = 1'b1; end
        hi = TAP_W'(i);
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      chosen_tap <= '0; chosen_valid <= 1'b0;
      region_low <= '0; region_high <= '0;
      chosen_in_region <= 1'b0; margin_to_fail <= '0;
    end else if (map_valid) begin
      region_low   <= lo;
      region_high  <= hi;
      chosen_valid <= any;

      if (any) begin
        if (ONE_SIDED) begin
          // The region has ONE real edge. The other end is not a
          // boundary -- it is where the sweep stopped. So offset a
          // documented lead from the real edge, and do not average.
          chosen_tap     <= lo + TAP_W'(LEAD_TAPS);
          margin_to_fail <= (TAP_W+1)'(LEAD_TAPS);
        end else begin
          // Two real edges: the midpoint maximises the distance to both.
          chosen_tap     <= TAP_W'((lo + hi) >> 1);
          margin_to_fail <= (TAP_W+1)'((hi - lo) >> 1);
        end
      end
    end
  end

  // Traceability: the choice must land inside the region it came from.
  always_comb chosen_in_region = chosen_valid
                              && (chosen_tap >= region_low)
                              && (chosen_tap <= region_high);
endmodule

// INTENTIONALLY DEFECTIVE. WEAK BUILD: one rule, both searches.
//
//   chosen_tap <= (lo + hi) >> 1;      // <-- always centre
//
// with ONE_SIDED removed from the parameter list entirely, so no
// instantiation can express the distinction.
//
// CONTRACT VIOLATED: 21.3 section 2 -- the gate's pass region is one-sided
// and therefore not centred.
//
// WHY IT SURVIVES: on a two-sided region it is IDENTICAL to the robust
// build. The eye-centring instance is correct. Only the gate instance is
// wrong, and only when the region's high end is the sweep's end rather
// than a real edge.
//
// TRACE (ILLUSTRATIVE, TAPS = 32, LEAD_TAPS = 3):
//   two-sided map, pass on taps 9..23:
//     robust (ONE_SIDED=0): chosen 16  margin 7    -- centred
//     weak:                 chosen 16  margin 7    IDENTICAL
//   one-sided map, pass on taps 6..31 (31 is the sweep end):
//     robust (ONE_SIDED=1): chosen 9   margin_to_fail 3   in_region 1
//     weak:                 chosen 18  margin_to_fail 12  in_region 1
//
//   gap: 9 taps. And the weak build's reported margin, 12, is LARGER --
//   it is measuring distance to tap 31, which is not a failing tap.
//   It is the end of the sweep.

// ROBUST BUILD: the margin is computed from the measured width, and the
// design checks that the arithmetic is satisfiable before committing.
module margin_provenance #(
    parameter int TAP_W       = 6,
    // The drift budget is a DECLARED fraction of the measured window,
    // not an absolute tap count. Provenance: 19.5 section 4's continuous
    // side -- the window narrows with temperature, and the budget is the
    // allowance for that narrowing.
    parameter int DRIFT_NUM   = 1,
    parameter int DRIFT_DEN   = 4,     // ILLUSTRATIVE: 25% of the window
    parameter int MIN_USABLE  = 4      // ILLUSTRATIVE taps
)(
    input  logic             clk,
    input  logic             rst_n,
    input  logic [TAP_W-1:0] window_low,     // measured
    input  logic [TAP_W-1:0] window_high,    // measured
    input  logic             window_valid,
    output logic [TAP_W-1:0] chosen_tap,
    output logic             chosen_valid,
    output logic [TAP_W:0]   margin_required,
    output logic [TAP_W:0]   margin_available,
    output logic             margin_satisfiable,
    output logic [7:0]       margin_refusals
);
  logic [TAP_W:0] width;

  always_comb begin
    width            = (TAP_W+1)'(window_high) - (TAP_W+1)'(window_low) + 1'b1;
    // The margin is a FUNCTION of the measurement. It cannot exceed the
    // window, because it is a fraction of it.
    margin_required  = (TAP_W+1)'((width * DRIFT_NUM) / DRIFT_DEN);
    margin_available = (width >> 1);
    // The satisfiability test is the item. A margin that does not fit is
    // refused, not truncated.
    margin_satisfiable = window_valid
                      && (width >= (TAP_W+1)'(MIN_USABLE))
                      && (margin_required <= margin_available);
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      chosen_tap <= '0; chosen_valid <= 1'b0; margin_refusals <= '0;
    end else if (window_valid) begin
      if (margin_satisfiable) begin
        chosen_tap   <= TAP_W'((window_low + window_high) >> 1);
        chosen_valid <= 1'b1;
      end else begin
        // 21.4's rule, enforced: a grid with no usable cell must FAIL.
        chosen_valid    <= 1'b0;
        margin_refusals <= margin_refusals + 1'b1;
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK BUILD: the margin is a constant.
//
//   parameter int GUARD_TAPS = 6;      // "measured on the bench"
//   ...
//   chosen_tap   <= window_low + GUARD_TAPS;
//   chosen_valid <= window_valid;      // <-- no satisfiability test
//
// CONTRACT VIOLATED: 21.4 section 2 -- training does not create margin,
// and a constant margin asserts an amount of margin the window may not
// contain.
//
// WHY IT SURVIVES: GUARD_TAPS = 6 was measured. On the characterisation
// part the window was 24 taps wide, 6 is 25% of it, and the arithmetic
// is exactly what the robust build computes. The constant is not a
// guess -- it is a correct answer, frozen.
//
// TRACE (ILLUSTRATIVE, DRIFT 1/4):
//   wide part,   window 8..31 (width 24):
//     robust: required 6  available 12  satisfiable 1  chosen 19
//     weak:                                            chosen 14
//     -- both inside the window; different points, both usable.
//   narrow part, window 14..21 (width 8):
//     robust: required 2  available 4   satisfiable 1  chosen 17
//     weak:   chosen = 14 + 6 = 20      chosen_valid 1
//     -- inside, but 1 tap from the failing edge instead of 4.
//   very narrow, window 16..19 (width 4):
//     robust: required 1  available 2   satisfiable 1  chosen 17
//     weak:   chosen = 16 + 6 = 22      chosen_valid 1
//     -- OUTSIDE the window. The part is configured to fail, and
//        `chosen_valid` says it is fine.
//
//   gap: on the narrowest part, the chosen tap is 3 taps outside the
//   measured window and the design reports success. margin_refusals:
//   robust 0 (all three satisfiable), weak has no such counter.

// ROBUST BUILD: direction and side are part of each value's identity,
// and the write path cannot lose them.
module direction_side_map #(
    parameter int VAL_W = 8
)(
    input  logic             clk,
    input  logic             rst_n,
    input  logic             wr_en,
    input  logic [VAL_W-1:0] wr_value,
    input  logic             wr_is_write_dir,  // 1 = write direction
    input  logic             wr_is_device,     // 1 = device side
    // the four cells, held separately because they are four quantities
    output logic [VAL_W-1:0] vref_rd_host,     // read dir, host samples
    output logic [VAL_W-1:0] vref_wr_device,   // write dir, device samples
    output logic [VAL_W-1:0] dly_rd_host,
    output logic [VAL_W-1:0] dly_wr_device,
    // the two cells that must stay EMPTY: 21.4's direction asymmetry
    output logic [1:0]       illegal_cell_writes,
    output logic [3:0]       cells_populated
);
  // The legality rule, stated once. A reference level belongs to the
  // side that SAMPLES, and the sampling side is decided by direction:
  // reads are sampled by the host, writes by the device.
  function automatic bit legal_cell(bit is_write_dir, bit is_device);
    return (is_write_dir == is_device);
  endfunction

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      vref_rd_host <= '0; vref_wr_device <= '0;
      dly_rd_host  <= '0; dly_wr_device  <= '0;
      illegal_cell_writes <= '0; cells_populated <= '0;
    end else if (wr_en) begin
      if (!legal_cell(wr_is_write_dir, wr_is_device)) begin
        // A write naming an impossible {direction, side} pair is REFUSED.
        // This is the whole item: the pair is checked, not assumed.
        illegal_cell_writes <= illegal_cell_writes + 1'b1;
      end else if (!wr_is_write_dir) begin
        vref_rd_host       <= wr_value;
        dly_rd_host        <= wr_value;
        cells_populated[0] <= 1'b1;
        cells_populated[2] <= 1'b1;
      end else begin
        vref_wr_device     <= wr_value;
        dly_wr_device      <= wr_value;
        cells_populated[1] <= 1'b1;
        cells_populated[3] <= 1'b1;
      end
    end
  end
endmodule

// INTENTIONALLY DEFECTIVE. WEAK BUILD: one reference level, both sides.
//
//   input  logic [VAL_W-1:0] wr_value;
//   ...
//   always_ff ... if (wr_en) vref_all <= wr_value;   // <-- one register
//
// with `wr_is_device` declared and never read -- 33.2 section 8's tell,
// appearing for the ninth time in this track's documented defects.
//
// CONTRACT VIOLATED: 21.4 section 2's direction asymmetry, and 28.4's
// side-asymmetry error class.
//
// WHY IT SURVIVES: on a symmetric link the two sides' correct values are
// close, so one register holding either is within tolerance. The training
// search finds a passing point. The part works. The defect appears when
// the sides stop being similar -- a different device vendor, a different
// rank population, a different termination setting.
//
// TRACE (ILLUSTRATIVE, correct host Vref 0x48, correct device Vref 0x5C):
//   symmetric part  (host 0x4A, device 0x4C):
//     robust: vref_rd_host=0x4A  vref_wr_device=0x4C  illegal=0
//     weak:   vref_all=0x4C (last write wins)
//     -- read direction runs 2 codes off centre; inside the eye. WORKS.
//   asymmetric part (host 0x48, device 0x5C):
//     robust: vref_rd_host=0x48  vref_wr_device=0x5C  illegal=0
//     weak:   vref_all=0x5C
//     -- read direction runs 20 codes off centre. Reads fail; writes pass.
//
//   gap: 20 codes, and the failure is DIRECTIONAL -- one direction
//   corrupts and the other does not, which is 28.4's side-asymmetry
//   signature exactly.
//
//   And the illegal-pair check: the robust build counts a write naming
//   {read direction, device side} as illegal; the weak build cannot,
//   because it does not read `wr_is_device` at all.

  // ---- Section 6: provenance. The measured term must be READ, which is
  // the property a formula-based build cannot satisfy.
  property p_offset_uses_trained_term;
    @(posedge clk) disable iff (!rst_n)
      launch_offset_valid |-> (launch_offset == (calc_part + trained_flight));
  endproperty
  assert property (p_offset_uses_trained_term)
    else $error("the launch offset did not include the trained flight term");

  property p_no_unclassified_quantity;
    @(posedge clk) disable iff (!rst_n) unclassified_terms == '0;
  endproperty
  assert property (p_no_unclassified_quantity)
    else $error("a quantity feeding a timing decision has no declared provenance");

  property p_refuses_without_provenance;
    @(posedge clk) disable iff (!rst_n)
      (!trained_flight_valid) |-> !launch_offset_valid;
  endproperty
  assert property (p_refuses_without_provenance)
    else $error("the launch offset was declared valid with no measured term");

  // ---- Section 7: flag semantics. `trusted` is a CONJUNCTION, and the
  // property names all three facts -- 28.4's five-into-one collapse.
  property p_trusted_implies_all_facts;
    @(posedge clk) disable iff (!rst_n)
      trusted |-> (ran && converged && in_range);
  endproperty
  assert property (p_trusted_implies_all_facts)
    else $error("trusted asserted without all of its constituent facts");

  property p_trust_is_not_monotonic;
    @(posedge clk) disable iff (!rst_n)
      (trusted && env_changed) |=> !trusted;
  endproperty
  assert property (p_trust_is_not_monotonic)
    else $error("trust survived an environment change: the flag cannot fall");

  // ---- Section 8: untrained refusal. Reset value AND the reclose path.
  property p_no_grant_while_gate_closed;
    @(posedge clk) disable iff (!rst_n) op_grant |-> $past(gate_open);
  endproperty
  assert property (p_no_grant_while_gate_closed)
    else $error("an operation was granted with the trained-value gate closed");

  property p_gate_closed_without_validity;
    @(posedge clk) disable iff (!rst_n) (!trained_valid) |=> !gate_open;
  endproperty
  assert property (p_gate_closed_without_validity)
    else $error("the gate stayed open with no valid trained value");

  // ---- Section 9: reset domains. The ONLY property in this chapter whose
  // antecedent is a reset, and it must be written outside the
  // `disable iff` that every other property uses.
  property p_clear_implies_retrain;
    @(posedge clk)
      $fell(trained_valid) |-> ##[0:2] (retrain_req || trained_valid);
  endproperty
  assert property (p_clear_implies_retrain)
    else $error("a trained value was cleared and no retraining was requested");

  property p_no_ops_on_reset_value;
    @(posedge clk) disable iff (!rst_por_n) ops_with_stale_offset == '0;
  endproperty
  assert property (p_no_ops_on_reset_value)
    else $error("an operation used the reset-value offset");

  // ---- Section 10: recalibration preconditions.
  property p_start_only_when_permitted;
    @(posedge clk) disable iff (!rst_n) recal_start |-> preconditions_met;
  endproperty
  assert property (p_start_only_when_permitted)
    else $error("recalibration started with its preconditions unmet");

  property p_commit_only_under_preconditions;
    @(posedge clk) disable iff (!rst_n) commits_under_traffic == '0;
  endproperty
  assert property (p_commit_only_under_preconditions)
    else $error("a measurement taken under traffic was committed");

  // ---- Section 11: range adequacy. Two-sided, because "failed" being
  // correct is exactly why one bit is not enough.
  property p_failure_has_a_cause;
    @(posedge clk) disable iff (!rst_n)
      (done && !found) |-> (err_prereq || err_classifier || range_exhausted
                            || (pass_count == '0));
  endproperty
  assert property (p_failure_has_a_cause)
    else $error("a search failed and reported no distinguishing cause");

  property p_prereq_checked_before_sweep;
    @(posedge clk) disable iff (!rst_n)
      (start && !prereq_done) |=> (err_prereq && done);
  endproperty
  assert property (p_prereq_checked_before_sweep)
    else $error("the sweep ran with an unfinished prerequisite");

  // ---- Section 12: selection rule. The shared cheap detector.
  property p_choice_inside_its_region;
    @(posedge clk) disable iff (!rst_n) chosen_valid |-> chosen_in_region;
  endproperty
  assert property (p_choice_inside_its_region)
    else $error("the chosen tap lies outside the region it was selected from");

  property p_one_sided_is_not_centred;
    @(posedge clk) disable iff (!rst_n)
      (chosen_valid && ONE_SIDED) |-> (chosen_tap == region_low + TAP_W'(LEAD_TAPS));
  endproperty
  assert property (p_one_sided_is_not_centred)
    else $error("a one-sided region was centred");

  // ---- Section 13: margin provenance. The satisfiability test, asserted.
  property p_margin_fits_the_window;
    @(posedge clk) disable iff (!rst_n)
      chosen_valid |-> (margin_required <= margin_available);
  endproperty
  assert property (p_margin_fits_the_window)
    else $error("a point was committed whose margin exceeds the measured window");

  property p_unsatisfiable_margin_refuses;
    @(posedge clk) disable iff (!rst_n)
      (window_valid && !margin_satisfiable) |=> !chosen_valid;
  endproperty
  assert property (p_unsatisfiable_margin_refuses)
    else $error("an unsatisfiable margin produced a valid choice");

  // ---- Section 14: direction and side.
  property p_illegal_pair_refused;
    @(posedge clk) disable iff (!rst_n)
      (wr_en && (wr_is_write_dir != wr_is_device)) |=> $stable(vref_rd_host)
                                                    && $stable(vref_wr_device);
  endproperty
  assert property (p_illegal_pair_refused)
    else $error("a write naming an impossible direction/side pair changed a cell");

  property p_sides_are_separate;
    @(posedge clk) disable iff (!rst_n)
      (wr_en && !wr_is_write_dir && !wr_is_device) |=> $stable(vref_wr_device);
  endproperty
  assert property (p_sides_are_separate)
    else $error("a read-direction host write disturbed the device-side value");

  // ---- COVERS. Each on the dimension its defect scales with.
  // Section 6: the trained term DIFFERING from any formula's answer.
  cover property (@(posedge clk) disable iff (!rst_n)
                  trained_flight_valid && (trained_flight != '0));
  // Section 7: each of the five cases reached. The antecedent of
  // p_trusted_implies_all_facts is unreachable for four of them.
  cover property (@(posedge clk) disable iff (!rst_n) fail_case == 3'd2);
  cover property (@(posedge clk) disable iff (!rst_n) fail_case == 3'd3);
  cover property (@(posedge clk) disable iff (!rst_n) fail_case == 3'd4);
  cover property (@(posedge clk) disable iff (!rst_n) fail_case == 3'd5);
  // Section 8: a request INSIDE the untrained window -- not a legal boot
  // sequence, which is why no stimulus reaches it by accident.
  cover property (@(posedge clk) disable iff (!rst_n) op_request && !gate_open);
  // Section 9: a WARM reset after successful training. The dimension is
  // the reset TYPE, and cold-booting more times never reaches it.
  cover property (@(posedge clk) trained_valid ##1 $fell(rst_func_n));
  // Section 10: the interval expiring while the bus is BUSY.
  cover property (@(posedge clk) disable iff (!rst_n)
                  (ivl == INTERVAL[$clog2(INTERVAL+1)-1:0]) && bus_busy);
  // Section 11: a pass region touching the sweep's end -- the false
  // success of row 5, which is not a failure and must still be covered.
  cover property (@(posedge clk) disable iff (!rst_n) done && found && edge_at_high);
  // Section 12: a ONE-SIDED region, which a random pass map rarely gives.
  cover property (@(posedge clk) disable iff (!rst_n)
                  map_valid && pass_map[TAPS-1] && !pass_map[0]);
  // Section 13: a window NARROW enough that the constant margin fails.
  cover property (@(posedge clk) disable iff (!rst_n)
                  window_valid && (width < (TAP_W+1)'(2*MIN_USABLE)));
  // Section 14: an ASYMMETRIC pair. Symmetric sides hide the defect.
  cover property (@(posedge clk) disable iff (!rst_n)
                  wr_en && (vref_rd_host != '0)
                        && (wr_value > vref_rd_host + 8'd16));