Ability Advertisement and Priority Resolution

// SYNTHESIZABLE.
//
// Builds the base link code word this device advertises.
//
// THE FIELDS (clause 28):
//   4:0   selector, 00001 = IEEE 802.3
//   12:5  technology ability A0..A7
//   13    RF   remote fault
//   14    ACK  acknowledge -- set by Section 9, NOT here
//   15    NP   next page follows
//
// THE RULE THIS MODULE ENFORCES: an advertised ability must be one the
// device can actually deliver. A device that advertises 1000BASE-T and
// cannot do it will win the resolution at both ends and then fail to
// establish -- and the failure appears as a link that will not come up
// between two devices that each believe they agreed.
package autoneg_res_pkg;
 
  localparam logic [4:0] SELECTOR_802_3 = 5'b00001;
 
  // Technology ability bit positions WITHIN the word.
  localparam int unsigned A_10T        = 5;
  localparam int unsigned A_10T_FD     = 6;
  localparam int unsigned A_100TX      = 7;
  localparam int unsigned A_100TX_FD   = 8;
  localparam int unsigned A_100T4      = 9;
  localparam int unsigned A_PAUSE      = 10;
  localparam int unsigned A_ASM_DIR    = 11;
  localparam int unsigned A_RESERVED   = 12;
 
  localparam int unsigned B_RF  = 13;
  localparam int unsigned B_ACK = 14;
  localparam int unsigned B_NP  = 15;
 
  // The technologies the resolution ranks. PAUSE and ASM_DIR are NOT
  // here: they are flow control, orthogonal to speed and duplex, and a
  // resolver that ranks them can resolve to "PAUSE", which is not a way
  // to run a link.
  typedef enum logic [3:0] {
    TECH_NONE,
    TECH_10T_HD,
    TECH_10T_FD,
    TECH_100TX_HD,
    TECH_100T4,
    TECH_100TX_FD,
    TECH_1000T_HD,     // advertised by next page
    TECH_1000T_FD      // advertised by next page
  } tech_e;
 
  // THE PRIORITY TABLE, as a RANK rather than as an ordered list.
  // Higher rank wins. Expressing it as a function of the technology
  // makes it checkable: Section 13 asserts that the ranks form a
  // STRICT TOTAL ORDER, which catches a duplicated or missing entry
  // without re-deriving what the order should be.
  function automatic logic [3:0] tech_rank (input tech_e t);
    unique case (t)
      TECH_1000T_FD: tech_rank = 4'd9;
      TECH_1000T_HD: tech_rank = 4'd8;
      TECH_100TX_FD: tech_rank = 4'd7;
      TECH_100T4:    tech_rank = 4'd6;
      TECH_100TX_HD: tech_rank = 4'd5;
      TECH_10T_FD:   tech_rank = 4'd4;
      TECH_10T_HD:   tech_rank = 4'd3;
      default:       tech_rank = 4'd0;
    endcase
  endfunction
 
  // Clause 28's acknowledge rule.
  localparam int unsigned ACK_RX_REQUIRED = 3;   // identical copies received
  localparam int unsigned ACK_TX_MIN      = 6;   // copies sent with ACK
  localparam int unsigned ACK_TX_MAX      = 8;
 
endpackage
 
module link_code_word_builder
  import autoneg_res_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
 
  // What this device CAN do -- from straps, fuses or PHY capability
  // registers. Not from software configuration.
  input  logic cap_10t_hd,
  input  logic cap_10t_fd,
  input  logic cap_100tx_hd,
  input  logic cap_100tx_fd,
  input  logic cap_100t4,
  input  logic cap_pause,
  input  logic cap_asm_dir,
  input  logic cap_1000t,            // requires a next page
 
  // What software has been allowed to DISABLE. Software may advertise
  // less than the hardware can do; it may never advertise more.
  input  logic [7:0] admin_mask,
 
  input  logic remote_fault,
  input  logic ack_from_tracker,     // Section 9 owns this bit
 
  output logic [15:0] link_code_word,
  output logic        next_page_required,
 
  // Software asked to advertise something the hardware cannot do.
  // REFUSED and reported -- an advertised ability that cannot be
  // delivered wins the resolution at BOTH ends and then fails.
  output logic             over_advertisement_refused,
  output logic [7:0]       refused_bits,
  output logic [CNT_W-1:0] c_refusals,
  output logic             ever_over_advertised
);
 
  logic [7:0] capability_c;
  logic [7:0] requested_c;
  logic [7:0] advertised_c;
 
  always_comb begin
    // The hardware's true capability, one bit per ability position.
    capability_c = {1'b0,              // A7 reserved, never advertised
                    cap_asm_dir,
                    cap_pause,
                    cap_100t4,
                    cap_100tx_fd,
                    cap_100tx_hd,
                    cap_10t_fd,
                    cap_10t_hd};
 
    // What software asked for.
    requested_c = admin_mask;
 
    // THE INTERSECTION. Software can subtract and never add.
    advertised_c = capability_c & requested_c;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      link_code_word <= 16'd0;
      next_page_required <= 1'b0;
      over_advertisement_refused <= 1'b0;
      refused_bits <= 8'd0; c_refusals <= '0;
      ever_over_advertised <= 1'b0;
    end else begin
      over_advertisement_refused <= 1'b0;
 
      link_code_word <= {
        1'b0,                         // NP, set below
        ack_from_tracker,             // ACK -- owned by Section 9
        remote_fault,                 // RF
        advertised_c,                 // A7..A0
        SELECTOR_802_3                // selector
      };
 
      // Gigabit needs a next page; the base page cannot express it.
      next_page_required     <= cap_1000t && admin_mask[0];
      link_code_word[B_NP]   <= cap_1000t && admin_mask[0];
 
      // REFUSAL. Software asking for an ability the hardware lacks is
      // not an error to be obeyed -- an advertised ability that cannot
      // be delivered wins at both ends and then does not work, and the
      // symptom is a link that will not come up between two devices
      // that each believe they agreed.
      if ((requested_c & ~capability_c) != 8'd0) begin
        over_advertisement_refused <= 1'b1;
        refused_bits               <= requested_c & ~capability_c;
        ever_over_advertised       <= 1'b1;
        if (!(&c_refusals)) c_refusals <= c_refusals + 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Parses a received link code word and validates its fields BEFORE
// anything acts on them.
//
// WHY VALIDATION MATTERS HERE MORE THAN USUAL. Chapter 11.1 §5 showed
// that a pulse accepted beyond data_detect_max shifts every subsequent
// bit, producing a well-formed 16-bit word that is a ROTATION of the
// transmitted one. A rotated word decodes to a plausible and entirely
// wrong set of abilities, with no error indication anywhere.
//
// THREE CHECKS CATCH IT, none of which was designed for it:
//   1. the SELECTOR must be 00001. A rotated word almost never has it.
//   2. the RESERVED bit A7 must be zero.
//   3. an advertisement of NOTHING -- zero technology bits -- is legal
//      to receive and means the partner can do nothing, which is
//      almost always a decode failure rather than a real claim.
module link_code_word_parser
  import autoneg_res_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic [15:0] word_in,
  input  logic        word_valid,
  input  logic        word_fully_bracketed,   // from Chapter 11.1
 
  output logic [4:0]  selector,
  output logic [7:0]  abilities,
  output logic        remote_fault,
  output logic        ack,
  output logic        next_page,
  output logic        parse_valid,
 
  // Validation results, each named because each is a different fault.
  output logic bad_selector,
  output logic reserved_bit_set,
  output logic empty_advertisement,
  output logic not_bracketed,
 
  output logic [CNT_W-1:0] c_words,
  output logic [CNT_W-1:0] c_bad_selector,
  output logic [CNT_W-1:0] c_reserved_set,
  output logic [CNT_W-1:0] c_empty_ads,
  output logic [CNT_W-1:0] c_rejected,
  output logic             ever_bad_selector
);
 
  wire [4:0] sel_c  = word_in[4:0];
  wire [7:0] abil_c = word_in[12:5];
 
  wire bad_sel_c   = (sel_c != SELECTOR_802_3);
  wire reserved_c  = word_in[A_RESERVED];
  // Technology bits only -- PAUSE and ASM_DIR are not technologies, so
  // a word advertising only flow control advertises no way to run.
  wire empty_c     = (abil_c[4:0] == 5'd0);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      selector <= 5'd0; abilities <= 8'd0; remote_fault <= 1'b0;
      ack <= 1'b0; next_page <= 1'b0; parse_valid <= 1'b0;
      bad_selector <= 1'b0; reserved_bit_set <= 1'b0;
      empty_advertisement <= 1'b0; not_bracketed <= 1'b0;
      c_words <= '0; c_bad_selector <= '0; c_reserved_set <= '0;
      c_empty_ads <= '0; c_rejected <= '0; ever_bad_selector <= 1'b0;
    end else if (clear) begin
      c_words <= '0; c_bad_selector <= '0; c_reserved_set <= '0;
      c_empty_ads <= '0; c_rejected <= '0;
      // ever_bad_selector survives: a partner that has ever sent a word
      // with the wrong selector is a partner worth suspecting.
    end else begin
      parse_valid         <= 1'b0;
      bad_selector        <= 1'b0;
      reserved_bit_set    <= 1'b0;
      empty_advertisement <= 1'b0;
      not_bracketed       <= 1'b0;
 
      if (word_valid) begin
        if (!(&c_words)) c_words <= c_words + 1'b1;
 
        selector     <= sel_c;
        abilities    <= abil_c;
        remote_fault <= word_in[B_RF];
        ack          <= word_in[B_ACK];
        next_page    <= word_in[B_NP];
 
        // A word whose bits could not all be vouched for is not parsed.
        // Chapter 11.1's bit_confidence is what makes this checkable,
        // and a design that discards it cannot make this decision.
        if (!word_fully_bracketed) begin
          not_bracketed <= 1'b1;
          if (!(&c_rejected)) c_rejected <= c_rejected + 1'b1;
 
        end else if (bad_sel_c) begin
          // THE SELECTOR CHECK. Designed so one FLP mechanism could
          // serve several standards; useful because a bit-shifted
          // decode almost never lands 00001 in the low five bits.
          bad_selector      <= 1'b1;
          ever_bad_selector <= 1'b1;
          if (!(&c_bad_selector)) c_bad_selector <= c_bad_selector + 1'b1;
          if (!(&c_rejected))     c_rejected     <= c_rejected + 1'b1;
 
        end else if (reserved_c) begin
          // A reserved bit set is not a technology this design does not
          // know. It is a word that should not exist, and treating it
          // as an unknown ability would advertise agreement with it.
          reserved_bit_set <= 1'b1;
          if (!(&c_reserved_set)) c_reserved_set <= c_reserved_set + 1'b1;
          if (!(&c_rejected))     c_rejected     <= c_rejected + 1'b1;
 
        end else if (empty_c) begin
          // A partner claiming no technologies at all. LEGAL to
          // receive, and almost always a decode failure rather than a
          // real advertisement -- so it is reported and not resolved.
          empty_advertisement <= 1'b1;
          if (!(&c_empty_ads)) c_empty_ads <= c_empty_ads + 1'b1;
          if (!(&c_rejected))  c_rejected  <= c_rejected + 1'b1;
 
        end else begin
          parse_valid <= 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Computes the resolution: intersect the two advertisements and select
// the highest-ranked common technology.
//
// THE DESIGN DECISION THAT MATTERS is that the table is expressed as a
// RANK FUNCTION rather than as an ordered if-else chain.
//
//   an if-else chain      -- correct or not, and the only way to check
//        it is to write the same chain again in a property, which
//        checks that two copies of one author's reading agree.
//   a rank function       -- has STRUCTURAL properties that hold for
//        ANY correct table: the ranks are distinct, they are a strict
//        total order, and the resolution is the argmax over the common
//        set. Those are checkable without re-deriving the order.
//
// Section 13's rejected property is the if-else chain written twice.
module priority_resolver
  import autoneg_res_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic [7:0] local_abilities,
  input  logic [7:0] partner_abilities,
  input  logic       local_1000t_hd,
  input  logic       local_1000t_fd,
  input  logic       partner_1000t_hd,
  input  logic       partner_1000t_fd,
  input  logic       resolve,
 
  output tech_e      resolution,
  output logic       resolution_valid,
  output logic [3:0] resolution_rank,
 
  // The common set, exported. A human debugging a wrong resolution
  // needs to see what BOTH ends claimed, and this is the intersection
  // the decision was actually made over.
  output logic [8:0] common_set,
  output logic [3:0] common_count,
 
  // No common technology at all. A distinct outcome from resolving to
  // the lowest one, and the two must never be confused.
  output logic       no_common_technology,
 
  // Flow control is resolved SEPARATELY, because PAUSE and ASM_DIR are
  // not technologies and ranking them yields "PAUSE", which is not a
  // way to run a link.
  output logic       pause_resolved,
  output logic       asm_dir_resolved,
 
  output logic [CNT_W-1:0] c_resolutions,
  output logic [CNT_W-1:0] c_no_common
);
 
  // The common set, one bit per technology, in rank order for clarity.
  //   [0] 10T HD  [1] 10T FD  [2] 100TX HD  [3] 100T4
  //   [4] 100TX FD [5] 1000T HD [6] 1000T FD
  logic [6:0] common_c;
  tech_e      best_c;
  logic [3:0] best_rank_c;
  logic [3:0] count_c;
 
  always_comb begin
    common_c[0] = local_abilities[A_10T      - 5] & partner_abilities[A_10T      - 5];
    common_c[1] = local_abilities[A_10T_FD   - 5] & partner_abilities[A_10T_FD   - 5];
    common_c[2] = local_abilities[A_100TX    - 5] & partner_abilities[A_100TX    - 5];
    common_c[3] = local_abilities[A_100T4    - 5] & partner_abilities[A_100T4    - 5];
    common_c[4] = local_abilities[A_100TX_FD - 5] & partner_abilities[A_100TX_FD - 5];
    common_c[5] = local_1000t_hd & partner_1000t_hd;
    common_c[6] = local_1000t_fd & partner_1000t_fd;
 
    count_c = 4'd0;
    for (int i = 0; i < 7; i = i + 1)
      if (common_c[i]) count_c = count_c + 4'd1;
 
    // ARGMAX OVER THE RANK FUNCTION. Not an ordered if-else chain --
    // a search for the highest rank among the common members. Which
    // means the ORDER lives in one place (tech_rank) and the SELECTION
    // logic is order-independent and separately checkable.
    best_c      = TECH_NONE;
    best_rank_c = 4'd0;
    if (common_c[0] && (tech_rank(TECH_10T_HD)   > best_rank_c)) begin
      best_c = TECH_10T_HD;   best_rank_c = tech_rank(TECH_10T_HD);   end
    if (common_c[1] && (tech_rank(TECH_10T_FD)   > best_rank_c)) begin
      best_c = TECH_10T_FD;   best_rank_c = tech_rank(TECH_10T_FD);   end
    if (common_c[2] && (tech_rank(TECH_100TX_HD) > best_rank_c)) begin
      best_c = TECH_100TX_HD; best_rank_c = tech_rank(TECH_100TX_HD); end
    if (common_c[3] && (tech_rank(TECH_100T4)    > best_rank_c)) begin
      best_c = TECH_100T4;    best_rank_c = tech_rank(TECH_100T4);    end
    if (common_c[4] && (tech_rank(TECH_100TX_FD) > best_rank_c)) begin
      best_c = TECH_100TX_FD; best_rank_c = tech_rank(TECH_100TX_FD); end
    if (common_c[5] && (tech_rank(TECH_1000T_HD) > best_rank_c)) begin
      best_c = TECH_1000T_HD; best_rank_c = tech_rank(TECH_1000T_HD); end
    if (common_c[6] && (tech_rank(TECH_1000T_FD) > best_rank_c)) begin
      best_c = TECH_1000T_FD; best_rank_c = tech_rank(TECH_1000T_FD); end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      resolution <= TECH_NONE; resolution_valid <= 1'b0;
      resolution_rank <= 4'd0; common_set <= 9'd0; common_count <= 4'd0;
      no_common_technology <= 1'b0;
      pause_resolved <= 1'b0; asm_dir_resolved <= 1'b0;
      c_resolutions <= '0; c_no_common <= '0;
    end else begin
      resolution_valid <= 1'b0;
 
      if (resolve) begin
        resolution       <= best_c;
        resolution_rank  <= best_rank_c;
        common_set       <= {2'd0, common_c};
        common_count     <= count_c;
        resolution_valid <= 1'b1;
        if (!(&c_resolutions)) c_resolutions <= c_resolutions + 1'b1;
 
        // NO COMMON TECHNOLOGY is a distinct outcome from resolving to
        // the lowest one. A link with nothing in common must not come
        // up; a link resolving to 10BASE-T half duplex must.
        no_common_technology <= (count_c == 4'd0);
        if (count_c == 4'd0) begin
          if (!(&c_no_common)) c_no_common <= c_no_common + 1'b1;
        end
 
        // FLOW CONTROL, resolved separately and never ranked. PAUSE is
        // not a way to run a link, and a resolver that ranks it can
        // select it.
        pause_resolved   <= local_abilities[A_PAUSE   - 5] &
                            partner_abilities[A_PAUSE - 5];
        asm_dir_resolved <= local_abilities[A_ASM_DIR   - 5] &
                            partner_abilities[A_ASM_DIR - 5];
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Implements clause 28's acknowledge, whose rules are asymmetric and
// whose meaning is narrower than its name suggests.
//
// THE RULES:
//   RECEIVE side -- set ACK only after THREE identical copies of the
//        partner's link code word have arrived. Not three words: three
//        IDENTICAL ones. A partner mid-negotiation emits words that
//        change, and acting on the first is acting on a transient.
//   TRANSMIT side -- once ACK is set, send between SIX and EIGHT
//        copies with it set before considering the exchange complete.
//        The range is a range: fewer than six risks the partner
//        missing them all, more than eight wastes time.
//
// WHAT ACK MEANS: "I received your advertisement."
// WHAT IT DOES NOT MEAN: "I agree", "I applied it", "we resolved the
//        same way", or "we are configured identically".
//
// The gap between those two lists is where Chapter 9.2's duplex
// mismatch lives, and no bit in this protocol closes it.
module acknowledge_tracker
  import autoneg_res_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic restart,
 
  input  logic        word_received,
  input  logic [15:0] received_word,
  input  logic        partner_ack,
 
  output logic        send_ack,
  output logic        exchange_complete,
  output logic [3:0]  identical_count,
  output logic [3:0]  ack_sent_count,
 
  // The exchange completed, and this is EXACTLY what it establishes:
  // both ends received an advertisement. Nothing about conclusions.
  output logic        advertisement_confirmed,
  // The partner's word changed AFTER we set ACK. Legal -- it may be
  // renegotiating -- and worth counting, because a partner whose word
  // keeps changing is not converging.
  output logic        word_changed_after_ack,
 
  output logic [CNT_W-1:0] c_exchanges,
  output logic [CNT_W-1:0] c_restarts,
  output logic [CNT_W-1:0] c_changes_after_ack,
  output logic [3:0]       worst_identical_wait
);
 
  logic [15:0] last_word_q;
  logic [3:0]  same_q;
  logic [3:0]  sent_q;
  logic        acked_q;
 
  // Compare everything EXCEPT the acknowledge bit. The partner sets it
  // when it has heard us, so including it would restart our own count
  // every time the partner's state advances.
  wire [15:0] mask = 16'hFFFF & ~(16'd1 << B_ACK);
 
  assign identical_count = same_q;
  assign ack_sent_count  = sent_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || restart) begin
      last_word_q <= 16'd0; same_q <= 4'd0; sent_q <= 4'd0;
      acked_q <= 1'b0; send_ack <= 1'b0;
      exchange_complete <= 1'b0; advertisement_confirmed <= 1'b0;
      word_changed_after_ack <= 1'b0;
      worst_identical_wait <= 4'd0;
      if (!rst_n) begin
        c_exchanges <= '0; c_restarts <= '0; c_changes_after_ack <= '0;
      end else begin
        if (!(&c_restarts)) c_restarts <= c_restarts + 1'b1;
      end
    end else begin
      exchange_complete      <= 1'b0;
      word_changed_after_ack <= 1'b0;
 
      if (word_received) begin
        if ((received_word & mask) == (last_word_q & mask)) begin
          if (same_q != 4'd15) same_q <= same_q + 4'd1;
 
          // THREE IDENTICAL COPIES. Not three words -- three the same.
          // A partner mid-negotiation emits words that change, and a
          // receiver acting on the first reconfigures on a transient.
          if ((same_q + 4'd1) >= 4'(ACK_RX_REQUIRED) && !acked_q) begin
            acked_q  <= 1'b1;
            send_ack <= 1'b1;
            sent_q   <= 4'd0;
            if ((same_q + 4'd1) > worst_identical_wait)
              worst_identical_wait <= same_q + 4'd1;
          end
 
        end else begin
          if (acked_q) begin
            // The partner's advertisement changed after we acked it.
            // Legal -- it may be renegotiating -- and counted, because
            // a word that keeps changing is a partner not converging.
            word_changed_after_ack <= 1'b1;
            if (!(&c_changes_after_ack))
              c_changes_after_ack <= c_changes_after_ack + 1'b1;
          end
          same_q      <= 4'd1;
          last_word_q <= received_word;
          acked_q     <= 1'b0;
          send_ack    <= 1'b0;
          sent_q      <= 4'd0;
        end
      end
 
      if (acked_q && word_received) begin
        if (sent_q != 4'(ACK_TX_MAX)) sent_q <= sent_q + 4'd1;
 
        // SIX TO EIGHT copies sent with ACK set, AND the partner must
        // have acked us too. Both conditions: our advertisement was
        // heard, and theirs was.
        if ((sent_q + 4'd1 >= 4'(ACK_TX_MIN)) && partner_ack) begin
          exchange_complete       <= 1'b1;
          // AND THIS IS ALL IT ESTABLISHES. Both advertisements were
          // received. Not that both ends resolved the same way.
          advertisement_confirmed <= 1'b1;
          if (!(&c_exchanges)) c_exchanges <= c_exchanges + 1'b1;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// The next-page mechanism, which is how a 16-bit word came to carry
// gigabit abilities that did not exist when it was defined.
//
// THE PROBLEM: the base page has 8 technology bits and they were all
// allocated. 1000BASE-T needs two more, plus a master/slave preference
// (Chapter 9.3 §4), plus a seed for the tie-break.
//
// THE MECHANISM: bit 15 (NP) says "another page follows". Pages are
// exchanged in the same FLP bursts, each acknowledged the same way, and
// the sequence continues until both ends clear NP.
//
// THE RULE THAT MAKES IT WORK: a device that does not understand next
// pages sets NP=0 and the exchange ends after the base page -- so an
// old device negotiates successfully against a new one and simply does
// not learn about the abilities it could not have used anyway.
//
// AND THE ASYMMETRY: if ONE end has more pages to send, the other must
// keep sending NULL pages to keep the exchange alive. A device that
// stops because it has nothing more to say stalls a partner that does.
module next_page_engine
  import autoneg_res_pkg::*;
#(
  parameter int unsigned MAX_PAGES = 8,
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic restart,
 
  input  logic        base_page_done,
  input  logic        partner_np,          // partner has more to send
  input  logic        page_acked,          // this page's exchange done
  input  logic [15:0] partner_page,
 
  // Pages this device wants to send, presented one at a time.
  input  logic        have_page,
  input  logic [15:0] page_to_send,
 
  output logic [15:0] page_out,
  output logic        page_out_valid,
  output logic        np_bit,
  output logic        sending_null_page,
 
  // Extracted gigabit abilities, which is what next pages are mostly
  // used for in practice.
  output logic        partner_1000t_hd,
  output logic        partner_1000t_fd,
  output logic        partner_prefers_master,
 
  output logic        exchange_done,
  output logic [3:0]  pages_exchanged,
  // The page count hit its bound. A partner that keeps setting NP
  // forever is either broken or speaking an extension this design
  // does not know, and either way the exchange must terminate.
  output logic        page_limit_reached,
 
  output logic [CNT_W-1:0] c_pages,
  output logic [CNT_W-1:0] c_null_pages,
  output logic [CNT_W-1:0] c_limit_hits,
  output logic             ever_limit_reached
);
 
  // A null message page: valid, acknowledgeable, and carrying nothing.
  // It exists so a device with nothing left to say can keep a partner's
  // page sequence alive.
  localparam logic [15:0] NULL_MESSAGE_PAGE = 16'h2001;
 
  logic [3:0] count_q;
  logic       active_q;
 
  assign pages_exchanged = count_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || restart) begin
      count_q <= 4'd0; active_q <= 1'b0;
      page_out <= 16'd0; page_out_valid <= 1'b0; np_bit <= 1'b0;
      sending_null_page <= 1'b0;
      partner_1000t_hd <= 1'b0; partner_1000t_fd <= 1'b0;
      partner_prefers_master <= 1'b0;
      exchange_done <= 1'b0; page_limit_reached <= 1'b0;
      if (!rst_n) begin
        c_pages <= '0; c_null_pages <= '0; c_limit_hits <= '0;
        ever_limit_reached <= 1'b0;
      end
    end else begin
      page_out_valid     <= 1'b0;
      page_limit_reached <= 1'b0;
 
      if (base_page_done && !active_q) begin
        active_q      <= 1'b1;
        exchange_done <= 1'b0;
      end
 
      if (active_q) begin
        if (count_q == 4'(MAX_PAGES)) begin
          // BOUNDED. A partner that keeps setting NP forever is broken
          // or speaking an extension we do not know, and either way
          // the exchange must terminate rather than continue.
          page_limit_reached <= 1'b1;
          ever_limit_reached <= 1'b1;
          exchange_done      <= 1'b1;
          active_q           <= 1'b0;
          if (!(&c_limit_hits)) c_limit_hits <= c_limit_hits + 1'b1;
 
        end else if (page_acked) begin
          count_q <= count_q + 4'd1;
          if (!(&c_pages)) c_pages <= c_pages + 1'b1;
 
          // Extract what the partner's page carried. In practice next
          // pages are mostly gigabit abilities plus Chapter 9.3's
          // master/slave preference.
          if (partner_page[0]) begin
            partner_1000t_hd       <= partner_page[9];
            partner_1000t_fd       <= partner_page[10];
            partner_prefers_master <= partner_page[12];
          end
 
          if (have_page) begin
            page_out          <= page_to_send;
            np_bit            <= 1'b1;
            sending_null_page <= 1'b0;
            page_out_valid    <= 1'b1;
 
          end else if (partner_np) begin
            // THE ASYMMETRY. We have nothing more to say and the
            // partner does -- so we must keep the sequence alive with
            // a null page. A device that simply stops here stalls a
            // partner that still has pages to send.
            page_out          <= NULL_MESSAGE_PAGE;
            np_bit            <= 1'b1;
            sending_null_page <= 1'b1;
            page_out_valid    <= 1'b1;
            if (!(&c_null_pages)) c_null_pages <= c_null_pages + 1'b1;
 
          end else begin
            // Neither end has more. The sequence ends here.
            np_bit        <= 1'b0;
            active_q      <= 1'b0;
            exchange_done <= 1'b1;
          end
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Checks the priority table's STRUCTURE rather than its contents.
//
// THE PROBLEM Section 13's rejected property runs into: to verify that
// the resolver picks the right technology, a property must know which
// technology is right -- which means implementing the table again, in
// the property, from the same reading of the standard by the same
// author. A misreading is then duplicated into both, and the assertion
// is green.
//
// WHAT THIS MODULE DOES INSTEAD: it checks properties that hold for
// ANY correct table and fail for specific CLASSES of table error,
// without knowing what the correct order is.
//
//   1. the ranks are DISTINCT -- no two technologies share one, which
//      catches a copy-paste duplicate.
//   2. the ranks are DENSE over their range -- no gaps, which catches
//      an omitted entry.
//   3. every technology has a NON-ZERO rank -- which catches an
//      unhandled enum case falling into the default.
//   4. the ordering is CONSISTENT with two invariants the standard
//      states in prose and which no plausible misreading violates:
//        full duplex outranks half duplex at the same speed, and
//        a higher speed outranks a lower one at the same duplex.
//
// The fourth is the interesting one. It does not encode the table; it
// encodes two RULES the table must satisfy -- and it catches a swapped
// pair without anybody re-deriving the order.
module resolution_consistency_checker
  import autoneg_res_pkg::*;
#(
  parameter int unsigned N_TECH = 7,
  parameter int unsigned CNT_W  = 16
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic check_request,
 
  output logic table_valid,
  output logic ranks_distinct,
  output logic ranks_dense,
  output logic all_ranks_nonzero,
  output logic duplex_ordering_ok,
  output logic speed_ordering_ok,
 
  output logic [3:0] first_bad_rank,
  output logic [CNT_W-1:0] c_checks,
  output logic [CNT_W-1:0] c_failures,
  output logic             ever_table_invalid
);
 
  tech_e ranked [N_TECH];
  logic  distinct_c, dense_c, nonzero_c, duplex_c, speed_c;
  logic [3:0] bad_c;
  logic [15:0] seen_c;
 
  always_comb begin
    ranked[0] = TECH_10T_HD;
    ranked[1] = TECH_10T_FD;
    ranked[2] = TECH_100TX_HD;
    ranked[3] = TECH_100T4;
    ranked[4] = TECH_100TX_FD;
    ranked[5] = TECH_1000T_HD;
    ranked[6] = TECH_1000T_FD;
 
    // 1 and 3: distinct, and none falling through to the default.
    distinct_c = 1'b1;
    nonzero_c  = 1'b1;
    seen_c     = 16'd0;
    bad_c      = 4'd0;
    for (int i = 0; i < N_TECH; i = i + 1) begin
      if (tech_rank(ranked[i]) == 4'd0) begin
        nonzero_c = 1'b0;
        bad_c     = 4'(i);
      end
      if (seen_c[tech_rank(ranked[i])]) begin
        distinct_c = 1'b0;
        bad_c      = tech_rank(ranked[i]);
      end
      seen_c[tech_rank(ranked[i])] = 1'b1;
    end
 
    // 2: dense -- the N ranks occupy N consecutive values, so an
    // omitted entry leaves a gap and is caught.
    dense_c = 1'b1;
    for (int r = 3; r < 3 + N_TECH; r = r + 1)
      if (!seen_c[r]) dense_c = 1'b0;
 
    // 4a: full duplex outranks half duplex at the SAME speed. A rule
    // from the standard's prose that no plausible misreading violates,
    // and it catches a swapped pair without encoding the order.
    duplex_c = (tech_rank(TECH_10T_FD)   > tech_rank(TECH_10T_HD)) &&
               (tech_rank(TECH_100TX_FD) > tech_rank(TECH_100TX_HD)) &&
               (tech_rank(TECH_1000T_FD) > tech_rank(TECH_1000T_HD));
 
    // 4b: a higher speed outranks a lower one at the SAME duplex.
    speed_c = (tech_rank(TECH_100TX_HD) > tech_rank(TECH_10T_HD)) &&
              (tech_rank(TECH_1000T_HD) > tech_rank(TECH_100TX_HD)) &&
              (tech_rank(TECH_100TX_FD) > tech_rank(TECH_10T_FD)) &&
              (tech_rank(TECH_1000T_FD) > tech_rank(TECH_100TX_FD));
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      table_valid <= 1'b0; ranks_distinct <= 1'b0; ranks_dense <= 1'b0;
      all_ranks_nonzero <= 1'b0; duplex_ordering_ok <= 1'b0;
      speed_ordering_ok <= 1'b0; first_bad_rank <= 4'd0;
      c_checks <= '0; c_failures <= '0; ever_table_invalid <= 1'b0;
    end else if (check_request) begin
      ranks_distinct     <= distinct_c;
      ranks_dense        <= dense_c;
      all_ranks_nonzero  <= nonzero_c;
      duplex_ordering_ok <= duplex_c;
      speed_ordering_ok  <= speed_c;
      first_bad_rank     <= bad_c;
 
      table_valid <= distinct_c && dense_c && nonzero_c &&
                     duplex_c && speed_c;
 
      if (!(&c_checks)) c_checks <= c_checks + 1'b1;
      if (!(distinct_c && dense_c && nonzero_c && duplex_c && speed_c)) begin
        ever_table_invalid <= 1'b1;
        if (!(&c_failures)) c_failures <= c_failures + 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Publishes what the negotiation established, what it assumed, and how
// much margin it had -- the same provenance-and-margin discipline
// Chapter 11.1 §12 applies to discovery.
//
// THE CENTRAL OUTPUT: resolution_is_unconfirmed. It is TRUE on every
// successful negotiation, always, because the protocol never confirms
// a resolution. Publishing a constant true might look pointless; it is
// not. It is the design stating, in a register a human can read, that
// the thing everybody assumes was checked was not.
module resolution_telemetry
  import autoneg_res_pkg::*;
#(
  parameter int unsigned CNT_W = 16
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic        resolution_valid,
  input  tech_e       resolution,
  input  logic [8:0]  common_set,
  input  logic [3:0]  common_count,
  input  logic        no_common_technology,
  input  logic        advertisement_confirmed,
  input  logic        table_valid,
  input  logic        parse_valid,
  input  logic        bad_selector,
  input  logic        empty_advertisement,
  input  logic [3:0]  pages_exchanged,
  input  logic [15:0] exchange_ms,
  input  logic        over_advertisement_refused,
 
  // What was established.
  output tech_e resolved_technology,
  output logic  advertisements_were_confirmed,
  // ALWAYS TRUE. The protocol has no mechanism to confirm a
  // resolution, and saying so in a register is the honest output.
  output logic  resolution_is_unconfirmed,
 
  // How much room there was.
  output logic [3:0]  common_count_last,
  output logic        resolved_at_lowest_common,
  output logic [15:0] worst_exchange_ms,
  output logic [3:0]  worst_pages,
 
  output logic [CNT_W-1:0] c_resolutions,
  output logic [CNT_W-1:0] c_no_common,
  output logic [CNT_W-1:0] c_rejected_words,
 
  // Sticky facts a counter clear destroys.
  output logic ever_no_common,
  output logic ever_bad_table,
  output logic ever_over_advertised,
  output logic ever_single_option
);
 
  // The protocol has no confirmation mechanism, so this is a constant.
  assign resolution_is_unconfirmed = 1'b1;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      resolved_technology <= TECH_NONE;
      advertisements_were_confirmed <= 1'b0;
      common_count_last <= 4'd0; resolved_at_lowest_common <= 1'b0;
      worst_exchange_ms <= 16'd0; worst_pages <= 4'd0;
      c_resolutions <= '0; c_no_common <= '0; c_rejected_words <= '0;
      ever_no_common <= 1'b0; ever_bad_table <= 1'b0;
      ever_over_advertised <= 1'b0; ever_single_option <= 1'b0;
    end else begin
      if (clear) begin
        c_resolutions <= '0; c_no_common <= '0; c_rejected_words <= '0;
        worst_exchange_ms <= 16'd0; worst_pages <= 4'd0;
        // The four ever_* flags survive.
      end
 
      if (!table_valid) ever_bad_table <= 1'b1;
      if (over_advertisement_refused) ever_over_advertised <= 1'b1;
      if (bad_selector || empty_advertisement || !parse_valid) begin
        if (!(&c_rejected_words)) c_rejected_words <= c_rejected_words + 1'b1;
      end
 
      if (resolution_valid) begin
        resolved_technology           <= resolution;
        advertisements_were_confirmed <= advertisement_confirmed;
        common_count_last             <= common_count;
 
        // A resolution with exactly ONE common technology has no
        // fallback: any further loss of an advertised ability takes the
        // link down rather than a step down. Not an error, and the only
        // warning available before it happens.
        if (common_count == 4'd1) ever_single_option <= 1'b1;
        resolved_at_lowest_common <= (common_count == 4'd1);
 
        if (exchange_ms > worst_exchange_ms) worst_exchange_ms <= exchange_ms;
        if (pages_exchanged > worst_pages)   worst_pages <= pages_exchanged;
 
        if (!(&c_resolutions)) c_resolutions <= c_resolutions + 1'b1;
        if (no_common_technology) begin
          ever_no_common <= 1'b1;
          if (!(&c_no_common)) c_no_common <= c_no_common + 1'b1;
        end
      end
    end
  end
 
endmodule

// P1. The selector is always the 802.3 value.
property p_selector_is_802_3;
  @(posedge clk) disable iff (!rst_n)
  link_code_word[4:0] == SELECTOR_802_3;
endproperty
a_selector_802_3: assert property (p_selector_is_802_3);
 
// P2. The reserved bit is never advertised.
property p_reserved_never_set;
  @(posedge clk) disable iff (!rst_n)
  !link_code_word[A_RESERVED];
endproperty
a_reserved_never_set: assert property (p_reserved_never_set);
 
// P3. THE SUBSET PROPERTY. Software may subtract abilities and never
// add them -- an advertised ability the hardware cannot deliver wins
// the resolution at BOTH ends and then fails to establish.
property p_advertisement_subset_of_capability;
  @(posedge clk) disable iff (!rst_n)
  (link_code_word[12:5] & ~capability_c) == 8'd0;
endproperty
a_advertisement_subset: assert property (p_advertisement_subset_of_capability);
 
// P4. And an attempt to over-advertise is REPORTED, not silently
// clipped -- the configuration is wrong and somebody needs to know.
property p_over_advertisement_reported;
  @(posedge clk) disable iff (!rst_n)
  ((requested_c & ~capability_c) != 8'd0) |=> over_advertisement_refused;
endproperty
a_over_advertisement_reported: assert property (p_over_advertisement_reported);
 
// P5. Gigabit sets the next-page bit, because the base page cannot
// carry it.
property p_gigabit_requires_next_page;
  @(posedge clk) disable iff (!rst_n)
  next_page_required |-> link_code_word[B_NP];
endproperty
a_gigabit_needs_np: assert property (p_gigabit_requires_next_page);

// P6. A word whose bits could not all be vouched for is never parsed.
// Chapter 11.1's confidence is what makes this decidable.
property p_unbracketed_never_parsed;
  @(posedge clk) disable iff (!rst_n)
  (word_valid && !word_fully_bracketed) |=> !parse_valid;
endproperty
a_unbracketed_not_parsed: assert property (p_unbracketed_never_parsed);
 
// P7. A bad selector rejects the word. Designed for multi-standard
// use; useful because a bit-rotated word almost never has 00001.
property p_bad_selector_rejects;
  @(posedge clk) disable iff (!rst_n)
  (word_valid && word_fully_bracketed && (word_in[4:0] != SELECTOR_802_3))
    |=> (bad_selector && !parse_valid);
endproperty
a_bad_selector_rejects: assert property (p_bad_selector_rejects);
 
// P8. A reserved bit set rejects the word rather than being treated as
// an unknown ability.
property p_reserved_set_rejects;
  @(posedge clk) disable iff (!rst_n)
  (word_valid && word_fully_bracketed && word_in[A_RESERVED])
    |=> (reserved_bit_set && !parse_valid);
endproperty
a_reserved_rejects: assert property (p_reserved_set_rejects);
 
// P9. An empty advertisement is REPORTED rather than resolved to
// nothing -- "the partner claimed nothing" and "we failed to hear the
// claim" are different work orders.
property p_empty_advertisement_reported;
  @(posedge clk) disable iff (!rst_n)
  (word_valid && word_fully_bracketed && (word_in[9:5] == 5'd0))
    |=> empty_advertisement;
endproperty
a_empty_reported: assert property (p_empty_advertisement_reported);

// P10. THE MEMBERSHIP PROPERTY. The resolution is a member of the
// common set. True for ANY correct table, and it catches a resolver
// that selects something neither end advertised.
property p_resolution_is_common;
  @(posedge clk) disable iff (!rst_n)
  (resolution_valid && (resolution != TECH_NONE))
    |-> common_set[resolution_index(resolution)];
endproperty
a_resolution_is_common: assert property (p_resolution_is_common);
 
// P11. THE MAXIMALITY PROPERTY. No common member outranks the
// resolution. Also true for any correct table -- it says the resolver
// implements an argmax, without saying what the ranks should be.
property p_resolution_is_maximal;
  @(posedge clk) disable iff (!rst_n)
  resolution_valid |-> (resolution_rank == max_rank_over(common_set));
endproperty
a_resolution_is_maximal: assert property (p_resolution_is_maximal);
 
// P12. THE MONOTONICITY PROPERTY. Adding an ability to either
// advertisement never LOWERS the resolution. A table with a swapped
// pair violates this for the specific inputs that expose the swap.
property p_resolution_monotone;
  @(posedge clk) disable iff (!rst_n)
  (resolution_valid && $past(resolution_valid) &&
   ((local_abilities & $past(local_abilities)) == $past(local_abilities)) &&
   (partner_abilities == $past(partner_abilities)))
    |-> (resolution_rank >= $past(resolution_rank));
endproperty
a_resolution_monotone: assert property (p_resolution_monotone);
 
// P13. THE DETERMINISM PROPERTY. The same inputs always yield the same
// resolution -- which is what makes two ends with the SAME table agree.
property p_resolution_deterministic;
  @(posedge clk) disable iff (!rst_n)
  (resolution_valid && $past(resolution_valid) &&
   (local_abilities   == $past(local_abilities)) &&
   (partner_abilities == $past(partner_abilities)))
    |-> (resolution == $past(resolution));
endproperty
a_resolution_deterministic: assert property (p_resolution_deterministic);
 
// P14. An empty common set yields TECH_NONE and a distinct flag -- not
// the lowest technology.
property p_no_common_is_distinct;
  @(posedge clk) disable iff (!rst_n)
  (resolution_valid && (common_count == 4'd0))
    |-> (no_common_technology && (resolution == TECH_NONE));
endproperty
a_no_common_distinct: assert property (p_no_common_is_distinct);
 
// P15. Flow control is never a resolution. PAUSE is not a way to run
// a link, and a resolver that ranks it can select it.
property p_flow_control_not_a_technology;
  @(posedge clk) disable iff (!rst_n)
  resolution_valid |-> (resolution inside {TECH_NONE, TECH_10T_HD,
    TECH_10T_FD, TECH_100TX_HD, TECH_100T4, TECH_100TX_FD,
    TECH_1000T_HD, TECH_1000T_FD});
endproperty
a_flow_control_not_tech: assert property (p_flow_control_not_a_technology);

// P16. Ranks are distinct -- catches a copy-paste duplicate.
property p_ranks_distinct;
  @(posedge clk) disable iff (!rst_n)
  check_request |=> ranks_distinct;
endproperty
a_ranks_distinct: assert property (p_ranks_distinct);
 
// P17. Ranks are dense -- catches an omitted entry.
property p_ranks_dense;
  @(posedge clk) disable iff (!rst_n)
  check_request |=> ranks_dense;
endproperty
a_ranks_dense: assert property (p_ranks_dense);
 
// P18. No technology falls into the default case.
property p_no_zero_ranks;
  @(posedge clk) disable iff (!rst_n)
  check_request |=> all_ranks_nonzero;
endproperty
a_no_zero_ranks: assert property (p_no_zero_ranks);
 
// P19. Full duplex outranks half duplex at the same speed. A rule from
// the standard's prose, not a re-derivation of the table.
property p_full_outranks_half;
  @(posedge clk) disable iff (!rst_n)
  check_request |=> duplex_ordering_ok;
endproperty
a_full_outranks_half: assert property (p_full_outranks_half);
 
// P20. And a higher speed outranks a lower one at the same duplex.
property p_faster_outranks_slower;
  @(posedge clk) disable iff (!rst_n)
  check_request |=> speed_ordering_ok;
endproperty
a_faster_outranks_slower: assert property (p_faster_outranks_slower);

// P21. ACK is set only after three IDENTICAL copies -- and the
// comparison masks the ACK bit, or the count never reaches three.
property p_ack_needs_three_identical;
  @(posedge clk) disable iff (!rst_n)
  $rose(send_ack) |-> ($past(same_q) >= 4'(ACK_RX_REQUIRED) - 4'd1);
endproperty
a_ack_needs_three: assert property (p_ack_needs_three_identical);
 
// P22. The exchange completes only after at least ACK_TX_MIN copies
// have been sent AND the partner has acked.
property p_exchange_needs_six_and_partner_ack;
  @(posedge clk) disable iff (!rst_n)
  exchange_complete |-> (($past(sent_q) + 4'd1 >= 4'(ACK_TX_MIN)) &&
                         $past(partner_ack));
endproperty
a_exchange_needs_six: assert property (p_exchange_needs_six_and_partner_ack);
 
// P23. A device with nothing left to send keeps the sequence alive
// with a null page while the partner still has pages.
property p_null_page_when_partner_has_more;
  @(posedge clk) disable iff (!rst_n)
  (page_acked && !have_page && partner_np) |=> sending_null_page;
endproperty
a_null_page_kept_alive: assert property (p_null_page_when_partner_has_more);
 
// P24. The page sequence terminates. A partner setting NP forever must
// not hold the exchange open indefinitely.
property p_page_sequence_bounded;
  @(posedge clk) disable iff (!rst_n)
  $rose(active_q) |-> ##[1:$] (exchange_done || page_limit_reached);
endproperty
a_page_sequence_bounded: assert property (p_page_sequence_bounded);