Negotiation Failures and Duplex Mismatch

// SYNTHESIZABLE.
//
// Observes symptoms and maintains the SET of causes still consistent
// with everything seen so far.
//
// WHY A SET AND NOT A VERDICT. Section 3's matrix is many-to-many:
//   "speed below expectation"      is consistent with 4 causes
//   "duplex below expectation"     with 5
//   "zero errors, low throughput"  with 5
//   "collisions at one end only"   with 2   <- the decisive one
//   "link never establishes"       with 1   <- the only decisive one
//
// So a classifier that emits one cause has encoded a HEURISTIC as a
// FACT. It will be right most of the time, which is exactly what makes
// it dangerous: it reports the common cause confidently, and the
// uncommon one identically.
//
// THIS MODULE instead maintains a bitmask of consistent causes, starts
// with all of them, and clears bits only when an observation is
// INCONSISTENT with a cause. Which means it can also report the one
// thing a verdict cannot: WHAT EVIDENCE IS STILL MISSING.
package diag_pkg;
 
  localparam int unsigned N_CAUSES = 7;
 
  // Cause bit positions.
  localparam int unsigned C_DUPLEX_MISMATCH = 0;
  localparam int unsigned C_LOST_PULSE      = 1;
  localparam int unsigned C_TABLE_DISAGREE  = 2;
  localparam int unsigned C_SLOW_NEGOTIATOR = 3;
  localparam int unsigned C_OVER_ADVERTISE  = 4;
  localparam int unsigned C_STALE_MEASURE   = 5;
  localparam int unsigned C_ONE_END_FORCED  = 6;
 
  // Symptom bit positions.
  localparam int unsigned S_SPEED_LOW       = 0;
  localparam int unsigned S_DUPLEX_LOW      = 1;
  localparam int unsigned S_FCS_UNDER_LOAD  = 2;
  localparam int unsigned S_ONE_SIDED_COLL  = 3;
  localparam int unsigned S_LATE_COLLISION  = 4;
  localparam int unsigned S_NO_ESTABLISH    = 5;
  localparam int unsigned S_RENEG_STORM     = 6;
  localparam int unsigned S_LOW_THROUGHPUT  = 7;
 
  // Section 3's matrix, as a per-symptom mask of CONSISTENT causes.
  // Observing a symptom intersects the live set with its mask.
  function automatic logic [N_CAUSES-1:0] consistent_with (input int sym);
    unique case (sym)
      S_SPEED_LOW:      consistent_with = 7'b1001110;
      S_DUPLEX_LOW:     consistent_with = 7'b1001111;
      S_FCS_UNDER_LOAD: consistent_with = 7'b1100001;
      S_ONE_SIDED_COLL: consistent_with = 7'b1000001;
      S_LATE_COLLISION: consistent_with = 7'b1000001;
      S_NO_ESTABLISH:   consistent_with = 7'b0010000;
      S_RENEG_STORM:    consistent_with = 7'b0010010;
      S_LOW_THROUGHPUT: consistent_with = 7'b1001111;
      default:          consistent_with = 7'b1111111;
    endcase
  endfunction
 
endpackage
 
module symptom_classifier
  import diag_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic [7:0] symptom_seen,        // one bit per symptom, level
  input  logic       symptom_valid,
 
  output logic [N_CAUSES-1:0] consistent_causes,
  output logic [3:0]          consistent_count,
  output logic [7:0]          symptoms_observed,
 
  // A single cause remains. Reported as a DIAGNOSIS only here -- never
  // when the set has more than one member.
  output logic                diagnosis_reached,
  output logic [2:0]          diagnosis_cause,
 
  // No cause is consistent with everything observed. Which means the
  // taxonomy is incomplete, or two faults are present at once, or an
  // observation is wrong -- and all three are worth knowing.
  output logic                inconsistent_evidence,
 
  output logic [CNT_W-1:0]    c_narrowings,
  output logic [CNT_W-1:0]    c_diagnoses,
  output logic                ever_inconsistent
);
 
  logic [N_CAUSES-1:0] live_q;
  logic [7:0]          seen_q;
  logic [N_CAUSES-1:0] next_c;
  logic [3:0]          count_c;
 
  assign consistent_causes = live_q;
  assign symptoms_observed = seen_q;
 
  always_comb begin
    next_c = live_q;
    for (int s = 0; s < 8; s = s + 1)
      if (symptom_seen[s]) next_c = next_c & consistent_with(s);
 
    count_c = 4'd0;
    for (int c = 0; c < N_CAUSES; c = c + 1)
      if (next_c[c]) count_c = count_c + 4'd1;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      // START WITH EVERYTHING. A diagnostic that starts from a
      // suspicion has already narrowed on no evidence.
      live_q <= {N_CAUSES{1'b1}};
      seen_q <= 8'd0;
      consistent_count <= 4'(N_CAUSES);
      diagnosis_reached <= 1'b0; diagnosis_cause <= 3'd0;
      inconsistent_evidence <= 1'b0;
      if (!rst_n) begin
        c_narrowings <= '0; c_diagnoses <= '0; ever_inconsistent <= 1'b0;
      end
    end else if (symptom_valid) begin
      seen_q <= seen_q | symptom_seen;
 
      // MONOTONE NARROWING. The set only ever shrinks; an observation
      // never re-admits a cause it previously excluded, because
      // evidence does not un-happen.
      if (next_c != live_q) begin
        live_q <= next_c;
        if (!(&c_narrowings)) c_narrowings <= c_narrowings + 1'b1;
      end
      consistent_count <= count_c;
 
      // A DIAGNOSIS is one cause and only one cause.
      diagnosis_reached <= (count_c == 4'd1);
      if (count_c == 4'd1) begin
        for (int c = 0; c < N_CAUSES; c = c + 1)
          if (next_c[c]) diagnosis_cause <= 3'(c);
        if (!(&c_diagnoses)) c_diagnoses <= c_diagnoses + 1'b1;
      end
 
      // EMPTY SET. Not "no fault" -- the opposite. Either the taxonomy
      // is incomplete, two faults are present, or an observation is
      // wrong, and reporting it as "unknown" would hide all three.
      inconsistent_evidence <= (count_c == 4'd0);
      if (count_c == 4'd0) ever_inconsistent <= 1'b1;
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Correlates evidence from BOTH ends of a link, because three of the
// seven causes cannot be identified from one end at all.
//
// THE THREE:
//   DUPLEX MISMATCH  -- the evidence is ASYMMETRIC. The half-duplex end
//        sees collisions and late collisions; the full-duplex end sees
//        FCS errors and runts. Each alone tells a plausible and wrong
//        physical-layer story: "the segment is congested" and "the
//        cable is bad". The pair is unmistakable, because a genuinely
//        shared segment collides at BOTH ends.
//   TABLE DISAGREEMENT -- neither end reports anything wrong. Both
//        resolved correctly against their own table. The ONLY
//        observation is that the two resolved technologies differ.
//   ONE END FORCED   -- the forced end sends no FLP bursts and reports
//        a clean forced configuration; the other parallel-detects.
//        Each is internally consistent.
//
// This module takes a remote evidence record -- delivered over
// management, LLDP, or an operator typing two register dumps into one
// tool -- and computes the comparisons no single end can.
module two_ended_evidence_correlator
  import diag_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  // Local evidence.
  input  logic [15:0] local_collisions,
  input  logic [15:0] local_late_collisions,
  input  logic [15:0] local_fcs_errors,
  input  logic [15:0] local_runts,
  input  logic [3:0]  local_resolved_tech,
  input  logic        local_full_duplex,
  input  logic        local_forced,
  input  logic        local_duplex_assumed,
 
  // Remote evidence, and a validity bit, because it arrives by a
  // completely different path and may be absent, stale or wrong.
  input  logic        remote_valid,
  input  logic [15:0] remote_collisions,
  input  logic [15:0] remote_late_collisions,
  input  logic [15:0] remote_fcs_errors,
  input  logic [15:0] remote_runts,
  input  logic [3:0]  remote_resolved_tech,
  input  logic        remote_full_duplex,
  input  logic        remote_forced,
 
  // The comparisons.
  output logic asymmetric_collisions,   // one end collides, the other does not
  output logic asymmetric_errors,       // one end FCS-errs, the other does not
  output logic resolution_disagreement, // the two ends chose differently
  output logic duplex_disagreement,
  output logic both_forced_differently,
 
  // The verdicts these comparisons support, as a cause mask.
  output logic [N_CAUSES-1:0] causes_supported,
  output logic [N_CAUSES-1:0] causes_excluded,
 
  // Correlation was attempted without remote evidence. Reported,
  // because "we could not tell" and "there is nothing wrong" are
  // different answers and a design must not conflate them.
  output logic remote_evidence_missing,
  output logic [CNT_W-1:0] c_correlations,
  output logic [CNT_W-1:0] c_missing_remote,
  output logic             ever_disagreed
);
 
  // "One end and not the other" needs a threshold, because zero is
  // rarely exactly zero on a real link.
  localparam logic [15:0] NOISE_FLOOR = 16'd8;
 
  wire local_colls_high  = (local_collisions  > NOISE_FLOOR);
  wire remote_colls_high = (remote_collisions > NOISE_FLOOR);
  wire local_fcs_high    = (local_fcs_errors  > NOISE_FLOOR);
  wire remote_fcs_high   = (remote_fcs_errors > NOISE_FLOOR);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      asymmetric_collisions <= 1'b0; asymmetric_errors <= 1'b0;
      resolution_disagreement <= 1'b0; duplex_disagreement <= 1'b0;
      both_forced_differently <= 1'b0;
      causes_supported <= '0; causes_excluded <= '0;
      remote_evidence_missing <= 1'b0;
      if (!rst_n) begin
        c_correlations <= '0; c_missing_remote <= '0; ever_disagreed <= 1'b0;
      end
    end else begin
      if (!remote_valid) begin
        // NO REMOTE EVIDENCE. Not "no disagreement" -- unknown. Three
        // causes remain unresolvable, and saying so is the honest
        // output.
        remote_evidence_missing <= 1'b1;
        causes_supported        <= '0;
        causes_excluded         <= '0;
        if (!(&c_missing_remote)) c_missing_remote <= c_missing_remote + 1'b1;
 
      end else begin
        remote_evidence_missing <= 1'b0;
        if (!(&c_correlations)) c_correlations <= c_correlations + 1'b1;
 
        // THE DECISIVE COMPARISON. On a genuinely shared segment BOTH
        // ends collide. Collisions at one end and not the other means
        // one end is not arbitrating at all.
        asymmetric_collisions <= (local_colls_high != remote_colls_high);
 
        // And its counterpart: the end that does not collide sees the
        // other's jam as FCS errors and runts.
        asymmetric_errors <= (local_fcs_high != remote_fcs_high);
 
        // NEITHER END REPORTS ANYTHING for this one. The comparison is
        // the entire observation.
        resolution_disagreement <= (local_resolved_tech != remote_resolved_tech);
        duplex_disagreement     <= (local_full_duplex   != remote_full_duplex);
        both_forced_differently <= local_forced && remote_forced &&
                                   (local_full_duplex != remote_full_duplex);
 
        causes_supported <= '0;
        causes_excluded  <= '0;
 
        if ((local_colls_high != remote_colls_high) &&
            (local_fcs_high   != remote_fcs_high)) begin
          // Asymmetric in BOTH directions: the duplex-mismatch
          // signature, and it excludes every cause that is symmetric.
          causes_supported[C_DUPLEX_MISMATCH] <= 1'b1;
          causes_supported[C_ONE_END_FORCED]  <= 1'b1;
          causes_excluded[C_LOST_PULSE]       <= 1'b1;
          causes_excluded[C_SLOW_NEGOTIATOR]  <= 1'b1;
          ever_disagreed <= 1'b1;
        end
 
        if (local_resolved_tech != remote_resolved_tech) begin
          // Two correct resolutions that differ. Chapter 11.2 §6's
          // table disagreement, and nothing else produces it.
          causes_supported[C_TABLE_DISAGREE] <= 1'b1;
          ever_disagreed <= 1'b1;
        end
 
        if (local_colls_high && remote_colls_high) begin
          // BOTH ends collide: a genuinely shared half-duplex segment.
          // Which EXCLUDES a duplex mismatch, and that exclusion is as
          // valuable as any positive finding.
          causes_excluded[C_DUPLEX_MISMATCH] <= 1'b1;
          causes_excluded[C_ONE_END_FORCED]  <= 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Predicts a mismatch BEFORE the symptom, from provenance rather than
// from errors.
//
// THE OBSERVATION THIS RESTS ON. A duplex mismatch needs SIMULTANEOUS
// transmission to produce any symptom at all. At low utilisation that
// almost never happens:
//
//   1% each way  -> P(simultaneous) ~ 0.0001 -> 1 event in 10 000 slots
//   5% each way  -> 0.0025                   -> 1 in 400
//   20% each way -> 0.04                     -> 1 in 25
//   50% each way -> 0.25                     -> 1 in 4
//
// So the link tests clean at commissioning, passes acceptance, and
// degrades in production -- weeks later, under load, with error
// counters that point at the cable.
//
// AND THE PREDICTIVE EVIDENCE WAS AVAILABLE AT BRING-UP. Four of the
// seven causes leave a provenance mark in the milliseconds after link
// up, on a link that is working perfectly:
//   duplex_is_assumed        -- Chapter 11.1 §8
//   ever_parallel_detected   -- Chapter 11.1 §8, sticky
//   common_count == 1        -- Chapter 11.2 §12, no fallback
//   ever_over_advertised     -- Chapter 11.2 §4
//   stale_measurement_used   -- Chapter 11.3 §6
//
// None of them is an error. All of them predict.
module mismatch_predictor
  import diag_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic link_came_up,
 
  // Provenance, carried forward from Chapters 11.1 through 11.3.
  input  logic duplex_is_assumed,
  input  logic ever_parallel_detected,
  input  logic [3:0] common_count,
  input  logic ever_over_advertised,
  input  logic stale_measurement_used,
  input  logic detection_used,
  input  logic near_timeout,
  input  logic [3:0] resolved_tech,
 
  // Utilisation, so the prediction can say WHEN it will surface.
  input  logic [6:0] tx_utilisation_percent,
  input  logic [6:0] rx_utilisation_percent,
 
  // The prediction: which causes this link is EXPOSED to, before any
  // symptom has appeared.
  output logic [N_CAUSES-1:0] exposed_causes,
  output logic [2:0]          exposure_count,
  output logic                link_is_exposed,
 
  // Risk, expressed as the two things that decide it: how weak the
  // provenance is, and how much load will exercise the weakness.
  output logic [1:0]  provenance_strength,   // 3 strong .. 0 assumed
  output logic [13:0] simultaneity_permille, // P(both transmit) x 1000
 
  // The single most useful output: this link works, and here is what
  // it is one load spike away from.
  output logic        predicted_duplex_mismatch,
  output logic        predicted_no_fallback,
 
  output logic [CNT_W-1:0] c_predictions,
  output logic             ever_predicted,
  output logic             ever_exposed_duplex
);
 
  logic [N_CAUSES-1:0] exp_c;
  logic [2:0]          cnt_c;
  logic [13:0]         sim_c;
 
  always_comb begin
    exp_c = '0;
 
    // DUPLEX ASSUMED rather than agreed: exposed to a mismatch and to
    // the forced-partner case, both of which need the far end to
    // confirm and neither of which has produced a symptom yet.
    if (duplex_is_assumed || ever_parallel_detected) begin
      exp_c[C_DUPLEX_MISMATCH] = 1'b1;
      exp_c[C_ONE_END_FORCED]  = 1'b1;
    end
 
    // A COMMON SET OF ONE has no fallback: the next lost pulse takes
    // the link DOWN rather than a step down.
    if (common_count == 4'd1) exp_c[C_LOST_PULSE] = 1'b1;
 
    if (ever_over_advertised)   exp_c[C_OVER_ADVERTISE] = 1'b1;
    if (stale_measurement_used) exp_c[C_STALE_MEASURE]  = 1'b1;
    if (detection_used)         exp_c[C_SLOW_NEGOTIATOR] = 1'b1;
 
    cnt_c = 3'd0;
    for (int c = 0; c < N_CAUSES; c = c + 1)
      if (exp_c[c]) cnt_c = cnt_c + 3'd1;
 
    // P(both ends transmit in the same slot), in per mille. The number
    // that says WHEN a latent mismatch becomes visible: at 1% each way
    // it is 1 in 10 000 slots, at 50% it is 1 in 4.
    sim_c = 14'((tx_utilisation_percent * rx_utilisation_percent) / 7'd10);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      exposed_causes <= '0; exposure_count <= 3'd0;
      link_is_exposed <= 1'b0; provenance_strength <= 2'd3;
      simultaneity_permille <= 14'd0;
      predicted_duplex_mismatch <= 1'b0; predicted_no_fallback <= 1'b0;
      if (!rst_n) begin
        c_predictions <= '0; ever_predicted <= 1'b0;
        ever_exposed_duplex <= 1'b0;
      end
    end else begin
      exposed_causes        <= exp_c;
      exposure_count        <= cnt_c;
      link_is_exposed       <= (cnt_c != 3'd0);
      simultaneity_permille <= sim_c;
 
      // PROVENANCE STRENGTH, from strongest to weakest. Not an error
      // scale -- a confidence scale about how the configuration was
      // arrived at.
      if (stale_measurement_used)        provenance_strength <= 2'd0;
      else if (duplex_is_assumed)        provenance_strength <= 2'd1;
      else if (common_count == 4'd1)     provenance_strength <= 2'd2;
      else                               provenance_strength <= 2'd3;
 
      predicted_duplex_mismatch <= exp_c[C_DUPLEX_MISMATCH];
      predicted_no_fallback     <= (common_count == 4'd1);
 
      if (link_came_up) begin
        if (!(&c_predictions)) c_predictions <= c_predictions + 1'b1;
        if (cnt_c != 3'd0) ever_predicted <= 1'b1;
        if (exp_c[C_DUPLEX_MISMATCH]) ever_exposed_duplex <= 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Detects a link that keeps renegotiating, and -- more usefully --
// measures what fraction of the time it is actually usable.
//
// WHY A DUTY CYCLE AND NOT A COUNT. A renegotiation count says a link
// is unstable. It does not say whether the link is 95% usable or 30%
// usable, and those are completely different findings:
//
//   bring-up 350 ms, renegotiating every 30 s -> 98.8% up
//   bring-up 350 ms, renegotiating every  2 s -> 82.5% up
//   bring-up 1400 ms, renegotiating every 2 s -> 30.0% up
//
// The last one is a link that spends most of its life negotiating, and
// its throughput is a third of nominal with NO errors anywhere --
// which is Section 3's "zero errors, low throughput" symptom arriving
// from a cause nobody suspects.
//
// AND THE BRING-UP TIME MATTERS AS MUCH AS THE INTERVAL. Two links
// renegotiating every 2 s differ by a factor of nearly three in usable
// throughput purely because one takes 350 ms to come up and the other
// 1400 ms -- which is Chapter 11.3's dominant_stage, again.
module renegotiation_storm_detector
  import diag_pkg::*;
#(
  parameter int unsigned CLK_MHZ = 25,
  parameter int unsigned WINDOW_S = 60,
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic link_came_up,
  input  logic link_went_down,
  input  logic [15:0] last_bringup_ms,
 
  output logic [CNT_W-1:0] renegotiations_in_window,
  output logic [15:0]      mean_interval_ms,
  output logic [15:0]      shortest_interval_ms,
 
  // The number that matters: what fraction of the window the link was
  // actually usable.
  output logic [6:0]       duty_percent,
  output logic [15:0]      up_ms_in_window,
  output logic [15:0]      down_ms_in_window,
 
  output logic storm_detected,
  output logic [1:0] storm_severity,      // 0 none .. 3 severe
  output logic window_valid,
 
  output logic [CNT_W-1:0] c_storms,
  output logic             ever_storm
);
 
  localparam int unsigned MS_TICKS  = 1000 * CLK_MHZ;
  localparam int unsigned WINDOW_MS = WINDOW_S * 1000;
  // More than this many renegotiations in the window is a storm.
  localparam int unsigned STORM_COUNT = 8;
 
  logic [31:0] tick_q;
  logic [15:0] window_ms_q;
  logic [15:0] since_up_q;
  logic [CNT_W-1:0] count_q;
  logic [31:0] up_accum_q;
  logic        is_up_q;
 
  assign renegotiations_in_window = count_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      tick_q <= '0; window_ms_q <= 16'd0; since_up_q <= 16'd0;
      count_q <= '0; up_accum_q <= '0; is_up_q <= 1'b0;
      mean_interval_ms <= 16'd0; shortest_interval_ms <= 16'hFFFF;
      duty_percent <= 7'd100; up_ms_in_window <= 16'd0;
      down_ms_in_window <= 16'd0;
      storm_detected <= 1'b0; storm_severity <= 2'd0;
      window_valid <= 1'b0;
      if (!rst_n) begin c_storms <= '0; ever_storm <= 1'b0; end
    end else begin
      if (tick_q == 32'(MS_TICKS - 1)) begin
        tick_q <= '0;
        if (window_ms_q != 16'hFFFF) window_ms_q <= window_ms_q + 16'd1;
        if (since_up_q  != 16'hFFFF) since_up_q  <= since_up_q + 16'd1;
        // Accumulate only the time the link was USABLE, which is the
        // whole point -- a link that is negotiating is not carrying
        // traffic, however healthy its state machine looks.
        if (is_up_q) up_accum_q <= up_accum_q + 1'b1;
      end else begin
        tick_q <= tick_q + 1'b1;
      end
 
      if (link_came_up) begin
        is_up_q <= 1'b1;
        if (since_up_q < shortest_interval_ms)
          shortest_interval_ms <= since_up_q;
        since_up_q <= 16'd0;
        if (!(&count_q)) count_q <= count_q + 1'b1;
      end
 
      if (link_went_down) is_up_q <= 1'b0;
 
      if (window_ms_q >= 16'(WINDOW_MS)) begin
        window_valid    <= 1'b1;
        up_ms_in_window <= 16'(up_accum_q);
        down_ms_in_window <= 16'(WINDOW_MS) - 16'(up_accum_q);
        duty_percent    <= 7'((up_accum_q * 100) / 32'(WINDOW_MS));
        mean_interval_ms <= (count_q == 0) ? 16'hFFFF
                            : 16'(WINDOW_MS / 32'(count_q));
 
        storm_detected <= (count_q > CNT_W'(STORM_COUNT));
        if (count_q > CNT_W'(STORM_COUNT)) begin
          ever_storm <= 1'b1;
          if (!(&c_storms)) c_storms <= c_storms + 1'b1;
        end
 
        // SEVERITY BY DUTY CYCLE, not by count. A link renegotiating
        // often but coming up in 350 ms may still be 98% usable; one
        // renegotiating less often but taking 1400 ms each time may be
        // 30% usable, and the second is far worse.
        if      (7'((up_accum_q * 100) / 32'(WINDOW_MS)) < 7'd50) storm_severity <= 2'd3;
        else if (7'((up_accum_q * 100) / 32'(WINDOW_MS)) < 7'd80) storm_severity <= 2'd2;
        else if (count_q > CNT_W'(STORM_COUNT))                   storm_severity <= 2'd1;
        else                                                      storm_severity <= 2'd0;
 
        window_ms_q <= 16'd0;
        up_accum_q  <= '0;
        count_q     <= '0;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Handles the Remote Fault bit, which is the only mechanism in
// autonegotiation by which one end tells the other that something is
// wrong -- and it is one bit with no reason code.
//
// WHAT RF MEANS: "I have a fault." Nothing about which fault, which
// direction, or whether it is transient.
//
// WHICH MAKES ITS HANDLING A JUDGEMENT. Acting on it aggressively --
// tearing the link down -- turns a far-end transient into a local
// outage. Ignoring it discards the ONLY inbound signal the protocol
// offers. So this module neither acts nor ignores: it RECORDS, with
// enough context that the pattern can be read later.
//
// AND THE PATTERN IS THE INFORMATION. A single RF is noise. RF asserted
// continuously is a partner with a persistent problem. RF that appears
// only after this end renegotiates is a partner reacting to US, which
// points at a loop rather than at a fault.
module remote_fault_handler
  import diag_pkg::*;
#(
  parameter int unsigned CLK_MHZ = 25,
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic remote_fault_bit,
  input  logic word_valid,
  input  logic local_renegotiated,
  input  logic link_up,
 
  output logic rf_asserted,
  output logic rf_persistent,
  output logic rf_follows_our_renegotiation,
 
  output logic [15:0]      rf_duration_ms,
  output logic [15:0]      longest_rf_ms,
  output logic [CNT_W-1:0] c_rf_assertions,
  output logic [CNT_W-1:0] c_rf_after_reneg,
 
  // The judgement, exported rather than acted on: this design does not
  // tear the link down, and it says clearly whether somebody should.
  output logic [1:0] rf_recommendation,   // 0 ignore, 1 watch, 2 investigate
  output logic       ever_rf,
  output logic       ever_rf_persistent
);
 
  localparam int unsigned MS_TICKS = 1000 * CLK_MHZ;
  // RF held this long is persistent rather than transient.
  localparam int unsigned PERSIST_MS = 5000;
  // RF within this window of our own renegotiation is a reaction.
  localparam int unsigned REACTION_MS = 500;
 
  logic [31:0] tick_q;
  logic [15:0] rf_ms_q;
  logic [15:0] since_reneg_q;
  logic        rf_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      tick_q <= '0; rf_ms_q <= 16'd0; since_reneg_q <= 16'hFFFF;
      rf_q <= 1'b0;
      rf_asserted <= 1'b0; rf_persistent <= 1'b0;
      rf_follows_our_renegotiation <= 1'b0;
      rf_duration_ms <= 16'd0; longest_rf_ms <= 16'd0;
      rf_recommendation <= 2'd0;
      if (!rst_n) begin
        c_rf_assertions <= '0; c_rf_after_reneg <= '0;
        ever_rf <= 1'b0; ever_rf_persistent <= 1'b0;
      end
    end else begin
      if (tick_q == 32'(MS_TICKS - 1)) begin
        tick_q <= '0;
        if (rf_q && (rf_ms_q != 16'hFFFF))            rf_ms_q <= rf_ms_q + 16'd1;
        if (since_reneg_q != 16'hFFFF) since_reneg_q <= since_reneg_q + 16'd1;
      end else begin
        tick_q <= tick_q + 1'b1;
      end
 
      if (local_renegotiated) since_reneg_q <= 16'd0;
 
      if (word_valid) begin
        if (remote_fault_bit && !rf_q) begin
          rf_q        <= 1'b1;
          rf_asserted <= 1'b1;
          rf_ms_q     <= 16'd0;
          ever_rf     <= 1'b1;
          if (!(&c_rf_assertions)) c_rf_assertions <= c_rf_assertions + 1'b1;
 
          // RF ARRIVING JUST AFTER WE RENEGOTIATED is the partner
          // reacting to us, not reporting an independent fault -- and
          // it points at a loop rather than at a far-end problem.
          if (since_reneg_q < 16'(REACTION_MS)) begin
            rf_follows_our_renegotiation <= 1'b1;
            if (!(&c_rf_after_reneg)) c_rf_after_reneg <= c_rf_after_reneg + 1'b1;
          end
 
        end else if (!remote_fault_bit && rf_q) begin
          rf_q           <= 1'b0;
          rf_asserted    <= 1'b0;
          rf_persistent  <= 1'b0;
          rf_duration_ms <= rf_ms_q;
          if (rf_ms_q > longest_rf_ms) longest_rf_ms <= rf_ms_q;
        end
      end
 
      if (rf_q && (rf_ms_q > 16'(PERSIST_MS))) begin
        rf_persistent      <= 1'b1;
        ever_rf_persistent <= 1'b1;
      end
 
      // THE RECOMMENDATION, published rather than enacted. Tearing a
      // link down on a far-end transient turns somebody else's problem
      // into an outage here.
      if (rf_persistent)                         rf_recommendation <= 2'd2;
      else if (rf_q && !rf_follows_our_renegotiation) rf_recommendation <= 2'd1;
      else                                        rf_recommendation <= 2'd0;
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Records failure history across link bounces, because the evidence a
// diagnosis needs is destroyed by the recovery that follows the fault.
//
// THE PROBLEM. A link that fails renegotiates and usually succeeds. So
// by the time anybody looks:
//   - every window counter has been reset by the successful attempt
//   - the classifier's consistent set has been re-initialised
//   - the provenance of the CURRENT link is fine, because the current
//     link came up cleanly
//
// And the fault that mattered happened two link-ups ago.
//
// SO THIS MODULE keeps a per-cause history that survives clears and
// link events, plus the full evidence record of the WORST attempt --
// worst by exposure count rather than by recency, because the most
// recent failure is usually the least interesting one.
module failure_history_recorder
  import diag_pkg::*;
#(
  parameter int unsigned CNT_W = 12,
  parameter int unsigned CLK_MHZ = 25
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic link_came_up,
  input  logic link_went_down,
 
  input  logic [N_CAUSES-1:0] consistent_causes,
  input  logic [N_CAUSES-1:0] exposed_causes,
  input  logic [2:0]          exposure_count,
  input  logic [1:0]          provenance_strength,
  input  logic                diagnosis_reached,
  input  logic [2:0]          diagnosis_cause,
  input  logic                remote_evidence_missing,
  input  logic [3:0]          resolved_tech,
 
  // Per-cause history. How many link-ups have been consistent with,
  // or exposed to, each cause -- across every bounce since reset.
  output logic [CNT_W-1:0] consistent_history [N_CAUSES],
  output logic [CNT_W-1:0] exposed_history    [N_CAUSES],
  output logic [CNT_W-1:0] diagnosed_history  [N_CAUSES],
 
  // The WORST link-up seen, held whole. Worst by exposure count, not
  // by recency -- the most recent link-up is usually the successful
  // retry, and the one before it is the interesting one.
  output logic             worst_valid,
  output logic [2:0]       worst_exposure_count,
  output logic [1:0]       worst_provenance,
  output logic [N_CAUSES-1:0] worst_exposed,
  output logic [3:0]       worst_tech,
  output logic             worst_had_no_remote,
 
  output logic [CNT_W-1:0] c_link_ups,
  output logic [CNT_W-1:0] c_link_downs,
  // The dominant cause across history: which one has been consistent
  // with the evidence most often. A distribution, not an event.
  output logic [2:0]       dominant_cause,
  output logic             dominant_valid
);
 
  integer i;
  logic [CNT_W-1:0] best_c;
  logic [2:0]       best_idx_c;
 
  always_comb begin
    best_c     = '0;
    best_idx_c = 3'd0;
    for (int c = 0; c < N_CAUSES; c = c + 1)
      if (consistent_history[c] > best_c) begin
        best_c     = consistent_history[c];
        best_idx_c = 3'(c);
      end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (i = 0; i < N_CAUSES; i = i + 1) begin
        consistent_history[i] <= '0;
        exposed_history[i]    <= '0;
        diagnosed_history[i]  <= '0;
      end
      worst_valid <= 1'b0; worst_exposure_count <= 3'd0;
      worst_provenance <= 2'd3; worst_exposed <= '0;
      worst_tech <= 4'd0; worst_had_no_remote <= 1'b0;
      c_link_ups <= '0; c_link_downs <= '0;
      dominant_cause <= 3'd0; dominant_valid <= 1'b0;
    end else if (clear) begin
      c_link_ups <= '0; c_link_downs <= '0;
      // THE HISTORIES SURVIVE. A clear is what happens immediately
      // before somebody investigates, and clearing the history is
      // exactly what destroys the evidence they came for.
    end else begin
      if (link_went_down) begin
        if (!(&c_link_downs)) c_link_downs <= c_link_downs + 1'b1;
      end
 
      if (link_came_up) begin
        if (!(&c_link_ups)) c_link_ups <= c_link_ups + 1'b1;
 
        for (i = 0; i < N_CAUSES; i = i + 1) begin
          if (consistent_causes[i] && !(&consistent_history[i]))
            consistent_history[i] <= consistent_history[i] + 1'b1;
          if (exposed_causes[i] && !(&exposed_history[i]))
            exposed_history[i] <= exposed_history[i] + 1'b1;
        end
 
        if (diagnosis_reached && !(&diagnosed_history[diagnosis_cause]))
          diagnosed_history[diagnosis_cause] <=
            diagnosed_history[diagnosis_cause] + 1'b1;
 
        // WORST BY EXPOSURE, not by recency. A weaker provenance also
        // wins -- a link that came up on a stale measurement is worse
        // than one exposed to two causes with strong provenance.
        if (!worst_valid ||
            (exposure_count > worst_exposure_count) ||
            (provenance_strength < worst_provenance)) begin
          worst_valid          <= 1'b1;
          worst_exposure_count <= exposure_count;
          worst_provenance     <= provenance_strength;
          worst_exposed        <= exposed_causes;
          worst_tech           <= resolved_tech;
          worst_had_no_remote  <= remote_evidence_missing;
        end
 
        dominant_cause <= best_idx_c;
        dominant_valid <= (best_c != '0);
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Publishes a diagnosis, and refuses to publish one it has not earned.
//
// THREE OUTPUTS, and the third is the one designs omit:
//   1. the CAUSE SET still consistent with the evidence
//   2. the CONFIDENCE, which is high only when one cause remains AND
//      remote evidence was available
//   3. WHAT TO MEASURE NEXT -- the specific observation that would
//      discriminate among the causes that remain
//
// The third turns a diagnostic from a guess into an instruction. A
// reporter that emits "probably a duplex mismatch" and a reporter that
// emits "duplex mismatch or one end forced; read the far end's
// collision counter to separate them" are the same silicon and
// completely different tools.
module diagnosis_reporter
  import diag_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic [N_CAUSES-1:0] consistent_causes,
  input  logic [3:0]          consistent_count,
  input  logic [N_CAUSES-1:0] exposed_causes,
  input  logic                remote_evidence_missing,
  input  logic                inconsistent_evidence,
  input  logic [1:0]          provenance_strength,
  input  logic [7:0]          symptoms_observed,
  input  logic                report_request,
 
  output logic [N_CAUSES-1:0] reported_causes,
  output logic [3:0]          reported_count,
  output logic [1:0]          confidence,     // 0 none .. 3 high
  output logic                report_valid,
 
  // The instruction. Which observation would most reduce the remaining
  // set, expressed as a symptom index to go and measure.
  output logic [2:0]          suggested_observation,
  output logic                suggestion_valid,
  output logic                needs_remote_evidence,
 
  // Refused to report. Distinct from reporting "unknown", because the
  // two mean opposite things: this one says the evidence CONTRADICTS
  // every cause in the taxonomy.
  output logic                report_refused,
  output logic [1:0]          refusal_reason,
 
  output logic [CNT_W-1:0] c_reports,
  output logic [CNT_W-1:0] c_refusals,
  output logic [CNT_W-1:0] c_low_confidence
);
 
  // Which causes need the far end (Section 7's table).
  localparam logic [N_CAUSES-1:0] NEEDS_REMOTE =
    (1 << C_DUPLEX_MISMATCH) | (1 << C_TABLE_DISAGREE) | (1 << C_ONE_END_FORCED);
 
  logic needs_remote_c;
  assign needs_remote_c = |(consistent_causes & NEEDS_REMOTE);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      reported_causes <= '0; reported_count <= 4'd0;
      confidence <= 2'd0; report_valid <= 1'b0;
      suggested_observation <= 3'd0; suggestion_valid <= 1'b0;
      needs_remote_evidence <= 1'b0;
      report_refused <= 1'b0; refusal_reason <= 2'd0;
      c_reports <= '0; c_refusals <= '0; c_low_confidence <= '0;
    end else begin
      report_valid     <= 1'b0;
      report_refused   <= 1'b0;
      suggestion_valid <= 1'b0;
 
      if (report_request) begin
        if (inconsistent_evidence) begin
          // THE EVIDENCE CONTRADICTS EVERY CAUSE. Not "unknown" --
          // the opposite. Two faults at once, an incomplete taxonomy,
          // or a wrong observation, and all three matter.
          report_refused <= 1'b1;
          refusal_reason <= 2'd1;
          if (!(&c_refusals)) c_refusals <= c_refusals + 1'b1;
 
        end else if (consistent_count == 4'(N_CAUSES)) begin
          // Nothing has been narrowed at all. Reporting the whole
          // taxonomy as a diagnosis would be technically true and
          // useless.
          report_refused <= 1'b1;
          refusal_reason <= 2'd2;
          if (!(&c_refusals)) c_refusals <= c_refusals + 1'b1;
 
        end else begin
          reported_causes       <= consistent_causes | exposed_causes;
          reported_count        <= consistent_count;
          report_valid          <= 1'b1;
          needs_remote_evidence <= needs_remote_c && remote_evidence_missing;
          if (!(&c_reports)) c_reports <= c_reports + 1'b1;
 
          // CONFIDENCE. High requires BOTH a single remaining cause and
          // remote evidence when the remaining cause needs it -- which
          // is the combination a naive reporter skips.
          if ((consistent_count == 4'd1) &&
              !(needs_remote_c && remote_evidence_missing)) begin
            confidence <= 2'd3;
          end else if (consistent_count == 4'd1) begin
            // One cause left, but it is one that needs the far end and
            // we never saw the far end. Not high confidence.
            confidence <= 2'd1;
            if (!(&c_low_confidence)) c_low_confidence <= c_low_confidence + 1'b1;
          end else if (consistent_count <= 4'd2) begin
            confidence <= 2'd2;
          end else begin
            confidence <= 2'd1;
            if (!(&c_low_confidence)) c_low_confidence <= c_low_confidence + 1'b1;
          end
 
          // THE INSTRUCTION. Suggest the observation that would most
          // reduce what remains -- ranked by how many causes it splits.
          if (needs_remote_c && remote_evidence_missing) begin
            suggested_observation <= 3'(S_ONE_SIDED_COLL);
            suggestion_valid      <= 1'b1;
          end else if (consistent_causes[C_LOST_PULSE] &&
                       consistent_causes[C_SLOW_NEGOTIATOR]) begin
            // Both are local and provenance separates them.
            suggested_observation <= 3'(S_RENEG_STORM);
            suggestion_valid      <= 1'b1;
          end else if (consistent_count > 4'd1) begin
            suggested_observation <= 3'(S_LATE_COLLISION);
            suggestion_valid      <= 1'b1;
          end
        end
      end
    end
  end
 
endmodule

// P1. THE MONOTONICITY PROPERTY. The consistent set only ever shrinks.
// Evidence does not un-happen, and a set that re-grows will oscillate
// as a load-dependent symptom comes and goes.
property p_set_narrows_monotonically;
  @(posedge clk) disable iff (!rst_n || clear)
  symptom_valid |=> ((consistent_causes & $past(consistent_causes))
                     == consistent_causes);
endproperty
a_set_narrows: assert property (p_set_narrows_monotonically);
 
// P2. Observations accumulate rather than sample -- a duplex mismatch
// produces FCS errors only under load, so the symptom disappears at
// night and a sampling classifier forgets.
property p_symptoms_accumulate;
  @(posedge clk) disable iff (!rst_n || clear)
  symptom_valid |=> ((symptoms_observed & $past(symptoms_observed))
                     == $past(symptoms_observed));
endproperty
a_symptoms_accumulate: assert property (p_symptoms_accumulate);
 
// P3. A cause is eliminated only by an observation INCONSISTENT with
// it -- never by ranking, likelihood or convenience.
property p_elimination_requires_inconsistency;
  @(posedge clk) disable iff (!rst_n || clear)
  (symptom_valid && !consistent_with(S_ONE_SIDED_COLL)[C_LOST_PULSE] &&
   symptom_seen[S_ONE_SIDED_COLL]) |=> !consistent_causes[C_LOST_PULSE];
endproperty
a_elimination_needs_inconsistency: assert property (p_elimination_requires_inconsistency);
 
// P4. A DIAGNOSIS is exactly one cause. Never "the most likely of
// three" reported as an answer.
property p_diagnosis_is_singleton;
  @(posedge clk) disable iff (!rst_n)
  diagnosis_reached |-> (consistent_count == 4'd1);
endproperty
a_diagnosis_singleton: assert property (p_diagnosis_is_singleton);
 
// P5. An EMPTY set is reported distinctly from an unnarrowed one.
// Contradiction and ignorance are opposite findings.
property p_empty_set_distinct;
  @(posedge clk) disable iff (!rst_n)
  (consistent_count == 4'd0) |-> inconsistent_evidence;
endproperty
a_empty_distinct: assert property (p_empty_set_distinct);
 
// P6. The classifier starts with EVERY cause. Starting from a
// suspicion has narrowed on no evidence at all.
property p_starts_unnarrowed;
  @(posedge clk) disable iff (!rst_n)
  $rose(clear) |=> (consistent_causes == {N_CAUSES{1'b1}});
endproperty
a_starts_unnarrowed: assert property (p_starts_unnarrowed);

// P7. Missing remote evidence is REPORTED, never treated as agreement.
// "We could not tell" and "there is nothing wrong" are different
// answers.
property p_missing_remote_reported;
  @(posedge clk) disable iff (!rst_n || clear)
  !remote_valid |=> remote_evidence_missing;
endproperty
a_missing_remote_reported: assert property (p_missing_remote_reported);
 
// P8. And with no remote evidence, NOTHING is supported or excluded.
property p_no_remote_no_conclusions;
  @(posedge clk) disable iff (!rst_n || clear)
  remote_evidence_missing |-> ((causes_supported == '0) &&
                               (causes_excluded  == '0));
endproperty
a_no_remote_no_conclusions: assert property (p_no_remote_no_conclusions);
 
// P9. Asymmetric collisions support a mismatch. The decisive
// comparison, and it requires both ends by construction.
property p_asymmetric_supports_mismatch;
  @(posedge clk) disable iff (!rst_n || clear)
  (remote_valid && (local_colls_high != remote_colls_high) &&
   (local_fcs_high != remote_fcs_high))
    |=> causes_supported[C_DUPLEX_MISMATCH];
endproperty
a_asymmetric_supports: assert property (p_asymmetric_supports_mismatch);
 
// P10. BOTH ends colliding EXCLUDES a mismatch. An exclusion is as
// valuable as a positive finding and is usually the neglected half.
property p_both_colliding_excludes_mismatch;
  @(posedge clk) disable iff (!rst_n || clear)
  (remote_valid && local_colls_high && remote_colls_high)
    |=> causes_excluded[C_DUPLEX_MISMATCH];
endproperty
a_both_colliding_excludes: assert property (p_both_colliding_excludes_mismatch);
 
// P11. Differing resolved technologies support a table disagreement,
// and nothing else produces that observation.
property p_differing_resolution_supports_table;
  @(posedge clk) disable iff (!rst_n || clear)
  (remote_valid && (local_resolved_tech != remote_resolved_tech))
    |=> causes_supported[C_TABLE_DISAGREE];
endproperty
a_differing_resolution: assert property (p_differing_resolution_supports_table);

// P12. THE PREDICTION PROPERTY. An assumed duplex exposes the link to
// a mismatch, on a link that is working perfectly.
property p_assumed_duplex_exposes;
  @(posedge clk) disable iff (!rst_n || clear)
  duplex_is_assumed |=> exposed_causes[C_DUPLEX_MISMATCH];
endproperty
a_assumed_exposes: assert property (p_assumed_duplex_exposes);
 
// P13. A common set of one exposes the link to the next lost pulse
// taking it DOWN rather than a step down.
property p_single_option_exposes;
  @(posedge clk) disable iff (!rst_n || clear)
  (common_count == 4'd1) |=> exposed_causes[C_LOST_PULSE];
endproperty
a_single_option_exposes: assert property (p_single_option_exposes);
 
// P14. Provenance strength is ordered: a stale measurement is weaker
// than an assumption, which is weaker than a single option.
property p_provenance_ordered;
  @(posedge clk) disable iff (!rst_n || clear)
  stale_measurement_used |=> (provenance_strength == 2'd0);
endproperty
a_provenance_ordered: assert property (p_provenance_ordered);
 
// P15. Exposure is computed from PROVENANCE and never from errors --
// so it holds on a link with zero errors.
property p_exposure_independent_of_errors;
  @(posedge clk) disable iff (!rst_n || clear)
  (duplex_is_assumed && link_came_up) |=> ever_exposed_duplex;
endproperty
a_exposure_from_provenance: assert property (p_exposure_independent_of_errors);

// P16. Severity follows the DUTY CYCLE, not the count. A link
// renegotiating often with a fast bring-up may still be 98% usable.
property p_severity_from_duty;
  @(posedge clk) disable iff (!rst_n || clear)
  (window_valid && (duty_percent < 7'd50)) |-> (storm_severity == 2'd3);
endproperty
a_severity_from_duty: assert property (p_severity_from_duty);
 
// P17. Only time the link was USABLE is accumulated. A link that is
// negotiating is not carrying traffic, whatever its state machine says.
property p_duty_counts_up_time_only;
  @(posedge clk) disable iff (!rst_n || clear)
  !is_up_q |=> $stable(up_accum_q);
endproperty
a_duty_up_time_only: assert property (p_duty_counts_up_time_only);
 
// P18. RF arriving just after OUR renegotiation is marked as a
// reaction rather than an independent fault.
property p_rf_reaction_marked;
  @(posedge clk) disable iff (!rst_n || clear)
  (word_valid && remote_fault_bit && !rf_q && (since_reneg_q < 16'(REACTION_MS)))
    |=> rf_follows_our_renegotiation;
endproperty
a_rf_reaction_marked: assert property (p_rf_reaction_marked);
 
// P19. The handler RECOMMENDS and never acts. Tearing a link down on
// a far-end transient converts somebody else's problem into an outage.
property p_rf_never_tears_down;
  @(posedge clk) disable iff (!rst_n)
  rf_asserted |-> (rf_recommendation <= 2'd2);
endproperty
a_rf_never_tears_down: assert property (p_rf_never_tears_down);

// P20. Histories survive a clear -- a clear is what happens
// immediately before somebody investigates.
property p_history_survives_clear;
  @(posedge clk) disable iff (!rst_n)
  (clear && (consistent_history[C_DUPLEX_MISMATCH] != '0))
    |=> (consistent_history[C_DUPLEX_MISMATCH] != '0);
endproperty
a_history_survives: assert property (p_history_survives_clear);
 
// P21. The worst record is selected by EXPOSURE, not by recency -- the
// most recent link-up is usually the successful retry.
property p_worst_by_exposure;
  @(posedge clk) disable iff (!rst_n)
  (link_came_up && (exposure_count > worst_exposure_count))
    |=> (worst_exposure_count == $past(exposure_count));
endproperty
a_worst_by_exposure: assert property (p_worst_by_exposure);
 
// P22. Confidence is high ONLY when one cause remains AND, if that
// cause needs the far end, the far end was observed.
property p_confidence_needs_remote;
  @(posedge clk) disable iff (!rst_n)
  (report_valid && (confidence == 2'd3))
    |-> !(needs_remote_c && remote_evidence_missing);
endproperty
a_confidence_needs_remote: assert property (p_confidence_needs_remote);
 
// P23. A report is refused when the evidence contradicts every cause,
// and the refusal is distinct from reporting "unknown".
property p_contradiction_refuses;
  @(posedge clk) disable iff (!rst_n)
  (report_request && inconsistent_evidence) |=> (report_refused &&
                                                 (refusal_reason == 2'd1));
endproperty
a_contradiction_refuses: assert property (p_contradiction_refuses);
 
// P24. And refused when nothing has been narrowed. Reporting the whole
// taxonomy is technically true and useless.
property p_unnarrowed_refuses;
  @(posedge clk) disable iff (!rst_n)
  (report_request && (consistent_count == 4'(N_CAUSES)))
    |=> (report_refused && (refusal_reason == 2'd2));
endproperty
a_unnarrowed_refuses: assert property (p_unnarrowed_refuses);
 
// P25. Every report with more than one cause carries a suggestion --
// the observation that would discriminate.
property p_multi_cause_report_suggests;
  @(posedge clk) disable iff (!rst_n)
  (report_valid && (reported_count > 4'd1)) |-> suggestion_valid;
endproperty
a_multi_cause_suggests: assert property (p_multi_cause_report_suggests);