LACP

// -----------------------------------------------------------------------
// lacp_pkg -- shared types for 802.1AX Link Aggregation Control.
// -----------------------------------------------------------------------
package lacp_pkg;

  localparam int MAX_MEMBERS = 8;
  localparam int MEMBER_W    = $clog2(MAX_MEMBERS);

  // Slow-protocol destination, distinct from 14.2's control DA.
  localparam logic [47:0] SLOW_DA   = 48'h01_80_C2_00_00_02;
  localparam logic [15:0] SLOW_ET   = 16'h8809;
  localparam logic [7:0]  LACP_SUB  = 8'h01;
  localparam logic [7:0]  LACP_VER  = 8'h01;

  // The eight state bits, carried once for the actor and once for the
  // partner. Bits 2 and 3 are the two roles 15.1 section 3 kept apart.
  typedef struct packed {
    logic expired;         // bit 7
    logic defaulted;       // bit 6 -- using defaults, not heard from
    logic distributing;    // bit 5 -- 15.1's distributing
    logic collecting;      // bit 4 -- 15.1's collecting
    logic synchronised;    // bit 3 -- IN SYNC with the partner
    logic aggregation;     // bit 2 -- willing to aggregate at all
    logic timeout_short;   // bit 1 -- 1 = fast (1 s), 0 = slow (30 s)
    logic activity;        // bit 0 -- 1 = active, will send unprompted
  } lacp_state_t;

  // What identifies an aggregatable entity. Two ports may join the
  // same aggregate only if all four of these match -- section 8.
  typedef struct packed {
    logic [15:0] sys_pri;
    logic [47:0] sys_id;     // the device's own MAC
    logic [15:0] key;        // the aggregation key
    logic [15:0] port_pri;
    logic [15:0] port_id;
  } lacp_id_t;

  typedef enum logic [1:0] {
    MUX_DETACHED, MUX_WAITING, MUX_ATTACHED, MUX_COLLECT_DIST
  } mux_state_e;

endpackage

// -----------------------------------------------------------------------
// lacpdu_builder -- emits one 128-octet LACPDU.
//
// The frame states what WE are (actor) and what we BELIEVE the partner
// to be (partner). The second half is a mirror, and section 19's
// rejected property is about how stale that mirror is.
// -----------------------------------------------------------------------
module lacpdu_builder
  import lacp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        req_valid,
  input  lacp_id_t    actor,
  input  lacp_state_t actor_state,
  input  lacp_id_t    partner,        // what we last heard, or defaults
  input  lacp_state_t partner_state,
  input  logic [15:0] collector_max_delay,
  output logic        req_ready,

  output logic        tx_valid,
  output logic [7:0]  tx_octet,
  output logic        tx_sop,
  output logic        tx_eop,
  output logic [31:0] c_sent
);

  // 6 DA + 6 SA + 2 ET + 110 payload = 124; FCS appended downstream
  // brings the frame to 128. No padding: the payload is well above
  // 5.6's 46-octet minimum.
  localparam int BODY = 124;

  logic [7:0] b [0:BODY-1];
  logic [6:0] idx;
  logic       busy;

  always_comb begin
    int p;
    for (p = 0; p < BODY; p++) b[p] = 8'h00;

    for (p = 0; p < 6; p++) b[p]     = SLOW_DA[47 - 8*p -: 8];
    for (p = 0; p < 6; p++) b[6 + p] = actor.sys_id[47 - 8*p -: 8];
    b[12] = SLOW_ET[15:8];  b[13] = SLOW_ET[7:0];
    b[14] = LACP_SUB;       b[15] = LACP_VER;

    // Actor TLV: type 0x01, length 20.
    b[16] = 8'h01; b[17] = 8'd20;
    b[18] = actor.sys_pri[15:8]; b[19] = actor.sys_pri[7:0];
    for (p = 0; p < 6; p++) b[20 + p] = actor.sys_id[47 - 8*p -: 8];
    b[26] = actor.key[15:8];      b[27] = actor.key[7:0];
    b[28] = actor.port_pri[15:8]; b[29] = actor.port_pri[7:0];
    b[30] = actor.port_id[15:8];  b[31] = actor.port_id[7:0];
    b[32] = actor_state;
    // b[33..35] reserved

    // Partner TLV: type 0x02, length 20. This is our BELIEF about them.
    b[36] = 8'h02; b[37] = 8'd20;
    b[38] = partner.sys_pri[15:8]; b[39] = partner.sys_pri[7:0];
    for (p = 0; p < 6; p++) b[40 + p] = partner.sys_id[47 - 8*p -: 8];
    b[46] = partner.key[15:8];      b[47] = partner.key[7:0];
    b[48] = partner.port_pri[15:8]; b[49] = partner.port_pri[7:0];
    b[50] = partner.port_id[15:8];  b[51] = partner.port_id[7:0];
    b[52] = partner_state;
    // b[53..55] reserved

    // Collector TLV: type 0x03, length 16.
    b[56] = 8'h03; b[57] = 8'd16;
    b[58] = collector_max_delay[15:8]; b[59] = collector_max_delay[7:0];
    // b[60..71] reserved

    // Terminator TLV: type 0x00, length 0, then 50 reserved octets.
    b[72] = 8'h00; b[73] = 8'd0;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      idx <= '0; busy <= 1'b0; c_sent <= '0;
    end else if (!busy) begin
      if (req_valid) begin
        busy   <= 1'b1;
        idx    <= '0;
        c_sent <= c_sent + 1;
      end
    end else begin
      if (idx == BODY-1) begin busy <= 1'b0; idx <= '0; end
      else                     idx  <= idx + 1'b1;
    end
  end

  assign req_ready = !busy;
  assign tx_valid  = busy;
  assign tx_octet  = b[idx];
  assign tx_sop    = busy && (idx == 7'd0);
  assign tx_eop    = busy && (idx == BODY-1);

endmodule

// -----------------------------------------------------------------------
// lacpdu_parser -- validates and extracts an LACPDU.
//
// The partner TLV in a RECEIVED frame is the far end's belief about
// US. Comparing it against what we actually are is how section 7's
// synchronised bit gets set, and it is the only place in the protocol
// where a device learns whether it has been heard correctly.
// -----------------------------------------------------------------------
module lacpdu_parser
  import lacp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        rx_valid,
  input  logic [7:0]  rx_octet,
  input  logic        rx_sop,
  input  logic        rx_eop,
  input  logic        rx_fcs_ok,

  input  lacp_id_t    our_actor,       // what we believe we are

  output logic        pdu_valid,
  output lacp_id_t    rx_actor,        // what THEY say they are
  output lacp_state_t rx_actor_state,
  output lacp_id_t    rx_partner,      // what they think WE are
  output lacp_state_t rx_partner_state,
  output logic        they_see_us,     // their partner TLV matches us

  output logic [31:0] c_received,
  output logic [31:0] c_bad_fcs,
  output logic [31:0] c_wrong_subtype,
  output logic [31:0] c_mismatched_mirror
);

  logic [6:0]  idx;
  logic        in_frame, da_ok, et_ok, sub_ok;
  logic [15:0] et_q;
  lacp_id_t    a_q, p_q;
  lacp_state_t as_q, ps_q;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      idx <= '0; in_frame <= 1'b0; da_ok <= 1'b0;
      et_ok <= 1'b0; sub_ok <= 1'b0; et_q <= '0;
      a_q <= '0; p_q <= '0; as_q <= '0; ps_q <= '0;
      pdu_valid <= 1'b0; they_see_us <= 1'b0;
      c_received <= '0; c_bad_fcs <= '0;
      c_wrong_subtype <= '0; c_mismatched_mirror <= '0;
    end else begin
      pdu_valid <= 1'b0;

      if (rx_valid && rx_sop) begin
        idx <= 7'd1; in_frame <= 1'b1; sub_ok <= 1'b0;
        da_ok <= (rx_octet == SLOW_DA[47:40]);
      end else if (rx_valid && in_frame) begin
        idx <= idx + 1'b1;

        if (idx <= 7'd5)
          if (rx_octet != SLOW_DA[47 - 8*idx -: 8]) da_ok <= 1'b0;

        if (idx == 7'd12) et_q[15:8] <= rx_octet;
        if (idx == 7'd13) et_ok <= ({et_q[15:8], rx_octet} == SLOW_ET);
        if (idx == 7'd14) sub_ok <= (rx_octet == LACP_SUB);

        // Actor TLV.
        if (idx == 7'd18) a_q.sys_pri[15:8] <= rx_octet;
        if (idx == 7'd19) a_q.sys_pri[7:0]  <= rx_octet;
        if (idx >= 7'd20 && idx <= 7'd25)
          a_q.sys_id[47 - 8*(idx-20) -: 8] <= rx_octet;
        if (idx == 7'd26) a_q.key[15:8]      <= rx_octet;
        if (idx == 7'd27) a_q.key[7:0]       <= rx_octet;
        if (idx == 7'd28) a_q.port_pri[15:8] <= rx_octet;
        if (idx == 7'd29) a_q.port_pri[7:0]  <= rx_octet;
        if (idx == 7'd30) a_q.port_id[15:8]  <= rx_octet;
        if (idx == 7'd31) a_q.port_id[7:0]   <= rx_octet;
        if (idx == 7'd32) as_q               <= rx_octet;

        // Partner TLV -- their mirror of us.
        if (idx == 7'd38) p_q.sys_pri[15:8] <= rx_octet;
        if (idx == 7'd39) p_q.sys_pri[7:0]  <= rx_octet;
        if (idx >= 7'd40 && idx <= 7'd45)
          p_q.sys_id[47 - 8*(idx-40) -: 8] <= rx_octet;
        if (idx == 7'd46) p_q.key[15:8]      <= rx_octet;
        if (idx == 7'd47) p_q.key[7:0]       <= rx_octet;
        if (idx == 7'd48) p_q.port_pri[15:8] <= rx_octet;
        if (idx == 7'd49) p_q.port_pri[7:0]  <= rx_octet;
        if (idx == 7'd50) p_q.port_id[15:8]  <= rx_octet;
        if (idx == 7'd51) p_q.port_id[7:0]   <= rx_octet;
        if (idx == 7'd52) ps_q               <= rx_octet;
      end

      if (rx_valid && rx_eop) begin
        in_frame <= 1'b0;
        if (da_ok && et_ok) begin
          if      (!sub_ok)    c_wrong_subtype <= c_wrong_subtype + 1;
          else if (!rx_fcs_ok) c_bad_fcs       <= c_bad_fcs + 1;
          else begin
            c_received       <= c_received + 1;
            pdu_valid        <= 1'b1;
            rx_actor         <= a_q;
            rx_actor_state   <= as_q;
            rx_partner       <= p_q;
            rx_partner_state <= ps_q;

            // Do they have us right? If their mirror does not match
            // what we are, they are talking about somebody else -- or
            // they have not heard our latest state yet.
            they_see_us <= (p_q.sys_id  == our_actor.sys_id) &&
                           (p_q.key     == our_actor.key)    &&
                           (p_q.port_id == our_actor.port_id);
            if (!((p_q.sys_id  == our_actor.sys_id) &&
                  (p_q.key     == our_actor.key)    &&
                  (p_q.port_id == our_actor.port_id)))
              c_mismatched_mirror <= c_mismatched_mirror + 1;
          end
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// lacp_state_machine -- the per-port mux machine.
//
// DETACHED -> WAITING -> ATTACHED -> COLLECTING_DISTRIBUTING
//
// The WAITING state exists so that several ports selecting the same
// aggregate at the same time settle together rather than one at a
// time; without it, a four-member aggregate comes up as a
// one-member aggregate, then two, then three -- and 15.2 section 12's
// rebalance runs at every step.
// -----------------------------------------------------------------------
module lacp_state_machine
  import lacp_pkg::*;
#(
  parameter int AGGREGATION_WAIT = 1000000   // 2 s at 500 MHz
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        pdu_valid,
  input  lacp_id_t    rx_actor,
  input  lacp_state_t rx_actor_state,
  input  logic        they_see_us,
  input  logic        rx_timeout,       // section 12's expiry
  input  logic        port_enabled,     // 15.1 section 6's physical up
  input  logic        selected,         // section 8 chose this port

  output mux_state_e  mux,
  output logic        collecting,
  output logic        distributing,
  output lacp_state_t our_state,
  output logic [31:0] c_attach,
  output logic [31:0] c_detach
);

  logic [31:0] wait_cnt;
  logic        partner_sync;

  // We are synchronised when they have us right AND they say they are
  // synchronised too. Both halves are required: their sync bit alone
  // could be about a different neighbour.
  assign partner_sync = they_see_us && rx_actor_state.synchronised;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      mux <= MUX_DETACHED; wait_cnt <= '0;
      collecting <= 1'b0; distributing <= 1'b0;
      c_attach <= '0; c_detach <= '0;
      our_state <= '0;
    end else begin
      // Any loss of the physical port or of the partner drops us all
      // the way out. There is no partial state.
      if (!port_enabled || rx_timeout || !selected) begin
        if (mux != MUX_DETACHED) c_detach <= c_detach + 1;
        mux          <= MUX_DETACHED;
        collecting   <= 1'b0;
        distributing <= 1'b0;
        wait_cnt     <= '0;
      end else begin
        unique case (mux)
          MUX_DETACHED: begin
            collecting <= 1'b0; distributing <= 1'b0;
            if (selected) begin
              mux      <= MUX_WAITING;
              wait_cnt <= '0;
            end
          end

          MUX_WAITING: begin
            wait_cnt <= wait_cnt + 1;
            if (wait_cnt == AGGREGATION_WAIT-1) mux <= MUX_ATTACHED;
          end

          MUX_ATTACHED: begin
            // 15.1 section 3's order: collect BEFORE distributing, so
            // the far end is never sent frames on a member we are not
            // yet accepting from.
            collecting <= 1'b1;
            if (partner_sync && rx_actor_state.collecting) begin
              mux      <= MUX_COLLECT_DIST;
              c_attach <= c_attach + 1;
            end
          end

          MUX_COLLECT_DIST: begin
            collecting   <= 1'b1;
            distributing <= 1'b1;
          end
        endcase
      end

      our_state.synchronised <= (mux == MUX_ATTACHED) ||
                                (mux == MUX_COLLECT_DIST);
      our_state.collecting   <= collecting;
      our_state.distributing <= distributing;
      our_state.aggregation  <= 1'b1;
      our_state.defaulted    <= rx_timeout;
      our_state.expired      <= rx_timeout;
    end
  end

endmodule

// -----------------------------------------------------------------------
// lacp_key_matcher -- decides whether a port may join an aggregate.
//
// Two ports aggregate together only if BOTH ends agree they should.
// Locally that means the same actor key. Remotely it means the same
// partner system id AND the same partner key. Section 11's mis-cable
// fails the remote half while passing the local one.
// -----------------------------------------------------------------------
module lacp_key_matcher
  import lacp_pkg::*;
(
  input  logic     clk,
  input  logic     rst_n,

  input  logic     pdu_valid [MAX_MEMBERS],
  input  lacp_id_t our_actor  [MAX_MEMBERS],
  input  lacp_id_t rx_actor   [MAX_MEMBERS],   // the partner, per port
  input  logic     partner_valid [MAX_MEMBERS],

  output logic [MAX_MEMBERS-1:0] selected,
  output logic [MAX_MEMBERS-1:0] individual,   // cannot aggregate
  output logic [47:0]            chosen_partner_sys,
  output logic [15:0]            chosen_partner_key,
  output logic [31:0]            c_wrong_partner,
  output logic [31:0]            c_selections
);

  // The reference pairing is the LOWEST-numbered port that has a
  // partner. Every other port must match it or be excluded.
  logic        have_ref;
  logic [47:0] ref_sys;
  logic [15:0] ref_key, ref_akey;

  always_comb begin
    int m;
    have_ref = 1'b0;
    ref_sys  = '0; ref_key = '0; ref_akey = '0;
    for (m = 0; m < MAX_MEMBERS; m++) begin
      if (!have_ref && partner_valid[m]) begin
        have_ref = 1'b1;
        ref_sys  = rx_actor[m].sys_id;
        ref_key  = rx_actor[m].key;
        ref_akey = our_actor[m].key;
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    int m;
    if (!rst_n) begin
      selected <= '0; individual <= '0;
      chosen_partner_sys <= '0; chosen_partner_key <= '0;
      c_wrong_partner <= '0; c_selections <= '0;
    end else begin
      chosen_partner_sys <= ref_sys;
      chosen_partner_key <= ref_key;

      for (m = 0; m < MAX_MEMBERS; m++) begin
        if (!partner_valid[m]) begin
          // Heard nothing. Not selected, and not individual either --
          // we simply do not know yet.
          selected[m]   <= 1'b0;
          individual[m] <= 1'b0;
        end else begin
          // Four conditions, all required.
          automatic logic ok;
          ok = have_ref &&
               (our_actor[m].key    == ref_akey) &&   // local intent
               (rx_actor[m].sys_id  == ref_sys)  &&   // same device
               (rx_actor[m].key     == ref_key);      // same far aggregate

          if (!ok && (rx_actor[m].sys_id != ref_sys)) begin
            // A DIFFERENT DEVICE at the other end of this cable.
            // Section 11: every physical source says this member is
            // healthy, and it must not be aggregated.
            c_wrong_partner <= c_wrong_partner + 1;
            individual[m]   <= 1'b1;
          end else begin
            individual[m] <= 1'b0;
          end

          if (ok && !selected[m]) c_selections <= c_selections + 1;
          selected[m] <= ok;
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// miscable_detector -- names the specific failure static configuration
// cannot see: a member whose far end is a different device.
//
// Every physical source in 15.1 section 6 reports this member healthy.
// The ONLY evidence is the actor system id in its LACPDUs, which no
// local measurement produces.
// -----------------------------------------------------------------------
module miscable_detector
  import lacp_pkg::*;
#(
  parameter int CONFIRM_PDUS = 3      // three consecutive, not one
)(
  input  logic     clk,
  input  logic     rst_n,

  input  logic     pdu_valid  [MAX_MEMBERS],
  input  lacp_id_t rx_actor   [MAX_MEMBERS],
  input  logic [47:0] expected_partner_sys,   // the majority pairing
  input  logic     expected_valid,

  input  logic [MAX_MEMBERS-1:0] port_enabled,   // 15.1's physical up

  output logic [MAX_MEMBERS-1:0] miscabled,
  output logic [47:0]            found_sys [MAX_MEMBERS],
  output logic [31:0]            c_miscables,
  output logic [15:0]            traffic_at_risk_pct
);

  logic [3:0] streak [MAX_MEMBERS];

  always_ff @(posedge clk or negedge rst_n) begin
    int m, n_bad, n_up;
    if (!rst_n) begin
      for (m = 0; m < MAX_MEMBERS; m++) begin
        streak[m] <= '0; found_sys[m] <= '0;
      end
      miscabled <= '0; c_miscables <= '0; traffic_at_risk_pct <= '0;
    end else begin
      for (m = 0; m < MAX_MEMBERS; m++) begin
        if (pdu_valid[m] && expected_valid) begin
          if (rx_actor[m].sys_id != expected_partner_sys) begin
            found_sys[m] <= rx_actor[m].sys_id;
            if (streak[m] != 4'hF) streak[m] <= streak[m] + 1'b1;
            if (streak[m] == CONFIRM_PDUS-1) begin
              miscabled[m] <= 1'b1;
              c_miscables  <= c_miscables + 1;
            end
          end else begin
            streak[m]    <= '0;
            miscabled[m] <= 1'b0;
          end
        end
        // Losing the port clears the finding: an absent cable is a
        // different fault with a different remedy.
        if (!port_enabled[m]) begin
          streak[m]    <= '0;
          miscabled[m] <= 1'b0;
        end
      end

      // What fraction of the aggregate's traffic a STATIC config would
      // be sending to the wrong device. This is the number that makes
      // the finding urgent rather than interesting.
      n_bad = 0; n_up = 0;
      for (m = 0; m < MAX_MEMBERS; m++) begin
        if (port_enabled[m]) n_up = n_up + 1;
        if (miscabled[m])    n_bad = n_bad + 1;
      end
      traffic_at_risk_pct <= (n_up == 0) ? 16'd0
                           : 16'((n_bad * 100) / n_up);
    end
  end

endmodule

// -----------------------------------------------------------------------
// lacp_periodic_timer -- transmit cadence and receive expiry.
//
// The transmit period is chosen by the PARTNER's timeout bit, not by
// ours: a partner that says it wants fast timeouts is telling us to
// transmit every second. This inversion is the most commonly
// implemented backwards thing in the protocol.
// -----------------------------------------------------------------------
module lacp_periodic_timer
  import lacp_pkg::*;
#(
  parameter int CLK_HZ = 500000000
)(
  input  logic       clk,
  input  logic       rst_n,

  input  logic       port_enabled,
  input  logic       our_activity,        // active or passive
  input  logic       partner_activity,
  input  logic       partner_wants_fast,  // partner state bit 1
  input  logic       we_want_fast,        // our own preference, sent out

  input  logic       pdu_received,

  output logic       tx_now,
  output logic       rx_timeout,
  output logic       rx_expired_once,
  output logic [31:0] c_timeouts,
  output logic [31:0] c_tx_periods,
  output logic [31:0] since_last_rx_ms
);

  localparam int FAST_PERIOD = CLK_HZ;          // 1 s
  localparam int SLOW_PERIOD = CLK_HZ * 30;     // 30 s
  localparam int MS_DIV      = CLK_HZ / 1000;

  logic [35:0] tx_cnt, rx_cnt, ms_cnt;
  logic [35:0] tx_period, rx_limit;

  // TRANSMIT at the rate the PARTNER asked for.
  assign tx_period = partner_wants_fast ? 36'(FAST_PERIOD)
                                        : 36'(SLOW_PERIOD);
  // EXPIRE after three of OUR chosen periods -- we asked for this rate,
  // so we are entitled to expect it.
  assign rx_limit  = we_want_fast ? 36'(3 * FAST_PERIOD)
                                  : 36'(3 * SLOW_PERIOD);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tx_cnt <= '0; rx_cnt <= '0; ms_cnt <= '0;
      tx_now <= 1'b0; rx_timeout <= 1'b0; rx_expired_once <= 1'b0;
      c_timeouts <= '0; c_tx_periods <= '0; since_last_rx_ms <= '0;
    end else begin
      tx_now <= 1'b0;

      if (!port_enabled) begin
        tx_cnt <= '0; rx_cnt <= '0; rx_timeout <= 1'b0;
      end else begin
        // A passive port transmits only if its partner is active.
        // Two passive ports never aggregate -- section 13's table.
        if (our_activity || partner_activity) begin
          if (tx_cnt >= tx_period - 1) begin
            tx_cnt       <= '0;
            tx_now       <= 1'b1;
            c_tx_periods <= c_tx_periods + 1;
          end else tx_cnt <= tx_cnt + 1'b1;
        end

        if (pdu_received) begin
          rx_cnt          <= '0;
          rx_timeout      <= 1'b0;
          ms_cnt          <= '0;
          since_last_rx_ms <= '0;
        end else begin
          if (rx_cnt < rx_limit) begin
            rx_cnt <= rx_cnt + 1'b1;
            if (rx_cnt == rx_limit - 1) begin
              rx_timeout      <= 1'b1;
              rx_expired_once <= 1'b1;
              c_timeouts      <= c_timeouts + 1;
            end
          end
          if (ms_cnt == MS_DIV-1) begin
            ms_cnt <= '0;
            since_last_rx_ms <= since_last_rx_ms + 1;
          end else ms_cnt <= ms_cnt + 1'b1;
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// lacp_churn_detector -- reports a port that fails to reach a stable
// synchronised state within a bounded time.
//
// Churn is the protocol-level version of 15.1 section 6's flapping
// member, and it has an additional cause that a flapping cable does
// not: two ends that disagree in a way that oscillates.
// -----------------------------------------------------------------------
module lacp_churn_detector
  import lacp_pkg::*;
#(
  parameter int CHURN_LIMIT   = 2000000000/4,  // ~1 s at 500 MHz
  parameter int WINDOW_CYCLES = 5000000000/10  // ~1 s window
)(
  input  logic       clk,
  input  logic       rst_n,

  input  logic       port_enabled,
  input  logic       actor_sync,
  input  logic       partner_sync,
  input  logic       attach_pulse,
  input  logic       detach_pulse,

  output logic       actor_churn,
  output logic       partner_churn,
  output logic [15:0] attaches_per_window,
  output logic [31:0] c_churn_events,
  output logic [31:0] longest_unsync_ms
);

  logic [31:0] a_unsync, p_unsync, win, ms_div;
  logic [15:0] att_cnt;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      a_unsync <= '0; p_unsync <= '0; win <= '0; ms_div <= '0;
      att_cnt <= '0; attaches_per_window <= '0;
      actor_churn <= 1'b0; partner_churn <= 1'b0;
      c_churn_events <= '0; longest_unsync_ms <= '0;
    end else if (!port_enabled) begin
      a_unsync <= '0; p_unsync <= '0;
      actor_churn <= 1'b0; partner_churn <= 1'b0;
    end else begin
      // Actor churn: WE cannot reach synchronised. Usually our own
      // selection logic oscillating -- section 8's reference moving.
      if (actor_sync) begin
        a_unsync    <= '0;
        actor_churn <= 1'b0;
      end else begin
        a_unsync <= a_unsync + 1;
        if (a_unsync == CHURN_LIMIT-1) begin
          actor_churn    <= 1'b1;
          c_churn_events <= c_churn_events + 1;
        end
        if (a_unsync > longest_unsync_ms * 500000)
          longest_unsync_ms <= a_unsync / 500000;
      end

      // Partner churn: THEY cannot reach synchronised. A different
      // fault entirely and usually theirs, which is why it is a
      // separate bit rather than a shared "not synchronised".
      if (partner_sync) begin
        p_unsync      <= '0;
        partner_churn <= 1'b0;
      end else begin
        p_unsync <= p_unsync + 1;
        if (p_unsync == CHURN_LIMIT-1) begin
          partner_churn  <= 1'b1;
          c_churn_events <= c_churn_events + 1;
        end
      end

      if (attach_pulse) att_cnt <= att_cnt + 1'b1;

      if (win == WINDOW_CYCLES-1) begin
        attaches_per_window <= att_cnt;
        att_cnt <= '0;
        win     <= '0;
      end else win <= win + 1'b1;
    end
  end

endmodule

// -----------------------------------------------------------------------
// lacp_conformance_monitor -- one bit per aggregate.
//
// It distinguishes OUR faults from FINDINGS about the far end. A
// mis-cable is not a defect in this device and must not clear its
// conformance bit -- it is the protocol working.
// -----------------------------------------------------------------------
module lacp_conformance_monitor
  import lacp_pkg::*;
(
  input  logic       clk,
  input  logic       rst_n,

  // Our faults.
  input  logic       tx_period_wrong,     // ignored the partner's rate
  input  logic       sync_without_mirror, // set sync without they_see_us
  input  logic       distributed_early,   // distributing before partner collecting
  input  logic       both_passive,        // configuration: never aggregates
  input  logic       no_active_end,

  // Findings about the far end -- NOT our faults.
  input  logic [MAX_MEMBERS-1:0] miscabled,
  input  logic       partner_churn,
  input  logic       partner_timeout,

  output logic       conformant,
  output logic [7:0] fault_vector,
  output logic [7:0] finding_vector,
  output logic       aggregate_degraded
);

  logic v_period, v_mirror, v_early, v_passive;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_period <= 1'b0; v_mirror <= 1'b0;
      v_early <= 1'b0; v_passive <= 1'b0;
    end else begin
      if (tx_period_wrong)     v_period <= 1'b1;
      if (sync_without_mirror) v_mirror <= 1'b1;
      if (distributed_early)   v_early  <= 1'b1;
      // Standing configuration property: at least one end active.
      v_passive <= both_passive || no_active_end;
    end
  end

  assign conformant = !(v_period || v_mirror || v_early || v_passive);

  assign fault_vector   = {4'b0000, v_passive, v_early, v_mirror, v_period};
  assign finding_vector = {5'b00000, partner_timeout, partner_churn,
                           |miscabled};

  // A separate output: the aggregate is smaller than configured for a
  // reason the protocol UNDERSTOOD. This is the alarm an operator
  // wants, and it is not a conformance failure.
  assign aggregate_degraded = (|miscabled) || partner_churn || partner_timeout;

endmodule

// P1. The LACPDU is addressed to the Slow Protocols multicast and
// carries the Slow Protocols EtherType and the LACP subtype.
property p_frame_identity;
  @(posedge clk) disable iff (!rst_n)
  tx_sop |-> ##12 (tx_octet == SLOW_ET[15:8]) ##1 (tx_octet == SLOW_ET[7:0])
                  ##1 (tx_octet == LACP_SUB);
endproperty

// P2. The frame is exactly 124 body octets -- 128 with the FCS. No
// padding: the payload is well above 5.6's 46-octet minimum.
property p_frame_length;
  @(posedge clk) disable iff (!rst_n)
  tx_sop |-> ##123 tx_eop;
endproperty

// P3. The source address is the DEVICE's identity, not the port's.
// All of a device's ports must claim one identity or the far end
// sees several one-member aggregates.
property p_sa_is_device_id;
  @(posedge clk) disable iff (!rst_n)
  tx_sop |-> ##6 (tx_octet == actor.sys_id[47:40]);
endproperty

// P4. The actor TLV always carries our current state, not a snapshot
// taken when the request was queued.
property p_actor_state_is_current;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && (idx == 7'd32)) |-> (tx_octet == actor_state);
endproperty

// P5. The builder never overlaps frames.
property p_no_overlap;
  @(posedge clk) disable iff (!rst_n)
  tx_sop |-> !tx_sop throughout (tx_eop [->1]);
endproperty

// P6. Nothing is committed on a bad FCS.
property p_no_commit_bad_fcs;
  @(posedge clk) disable iff (!rst_n)
  (rx_eop && !rx_fcs_ok) |-> !pdu_valid;
endproperty

// P7. A non-LACP slow protocol is not an error. Marker frames arrive
// legitimately at a device that does not implement them.
property p_marker_is_not_an_error;
  @(posedge clk) disable iff (!rst_n)
  (rx_eop && da_ok && et_ok && !sub_ok) |-> !$changed(c_bad_fcs);
endproperty

// P8. pdu_valid is one cycle wide -- the mux machine reacts to a pulse.
property p_commit_is_a_pulse;
  @(posedge clk) disable iff (!rst_n)
  pdu_valid |=> !pdu_valid;
endproperty

// P9. they_see_us is exactly the three-field comparison it claims.
property p_mirror_comparison;
  @(posedge clk) disable iff (!rst_n)
  pdu_valid |-> (they_see_us == ((rx_partner.sys_id  == our_actor.sys_id) &&
                                 (rx_partner.key     == our_actor.key)    &&
                                 (rx_partner.port_id == our_actor.port_id)));
endproperty

// P10. Collecting is never enabled after distributing. 15.1 section 3's
// ordering, and the reason no frame is lost bringing a member up.
property p_collect_before_distribute;
  @(posedge clk) disable iff (!rst_n)
  $rose(distributing) |-> collecting;
endproperty

// P11. We never distribute unless the partner says it is collecting.
property p_distribute_needs_partner_collecting;
  @(posedge clk) disable iff (!rst_n)
  distributing |-> rx_actor_state.collecting;
endproperty

// P12. Losing the port, the partner or the selection detaches
// immediately. There is no partial state to linger in.
property p_loss_detaches;
  @(posedge clk) disable iff (!rst_n)
  (!port_enabled || rx_timeout || !selected) |=> (mux == MUX_DETACHED);
endproperty

// P13. Detached means neither role is active.
property p_detached_is_inert;
  @(posedge clk) disable iff (!rst_n)
  (mux == MUX_DETACHED) |-> (!collecting && !distributing);
endproperty

// P14. WAITING lasts exactly AGGREGATION_WAIT, so several ports
// selecting together settle together.
property p_waiting_is_timed;
  @(posedge clk) disable iff (!rst_n)
  $rose(mux == MUX_WAITING) |-> ##AGGREGATION_WAIT (mux == MUX_ATTACHED);
endproperty

// P15. Synchronised requires BOTH they_see_us and their sync bit.
// Checking only the second aggregates a mis-cabled member.
property p_sync_needs_mirror;
  @(posedge clk) disable iff (!rst_n)
  our_state.synchronised |-> they_see_us;
endproperty

// P16. A selected port's partner is the same device as the reference.
property p_selected_same_partner;
  @(posedge clk) disable iff (!rst_n)
  selected[m] |-> (rx_actor[m].sys_id == chosen_partner_sys);
endproperty

// P17. And the same far-end aggregation key.
property p_selected_same_key;
  @(posedge clk) disable iff (!rst_n)
  selected[m] |-> (rx_actor[m].key == chosen_partner_key);
endproperty

// P18. A port whose partner is a DIFFERENT device is individual, never
// selected. The mis-cable, as a property.
property p_wrong_partner_is_individual;
  @(posedge clk) disable iff (!rst_n)
  (partner_valid[m] && (rx_actor[m].sys_id != chosen_partner_sys))
    |=> (individual[m] && !selected[m]);
endproperty

// P19. Not having heard is distinct from having heard the wrong thing.
property p_silence_is_not_individual;
  @(posedge clk) disable iff (!rst_n)
  !partner_valid[m] |-> !individual[m];
endproperty

// P20. A mis-cable finding needs CONFIRM_PDUS consecutive
// disagreements -- one is normal during bring-up.
property p_miscable_needs_confirmation;
  @(posedge clk) disable iff (!rst_n)
  $rose(miscabled[m]) |-> ($past(streak[m]) == CONFIRM_PDUS-1);
endproperty

// P21. Losing the port clears the finding: an absent cable is a
// different fault with a different remedy.
property p_port_down_clears_miscable;
  @(posedge clk) disable iff (!rst_n)
  !port_enabled[m] |=> !miscabled[m];
endproperty

// P22. We transmit at the rate the PARTNER asked for.
property p_tx_rate_follows_partner;
  @(posedge clk) disable iff (!rst_n)
  partner_wants_fast |-> (tx_period == FAST_PERIOD);
endproperty

// P23. We expire after three of OUR chosen periods.
property p_expiry_follows_us;
  @(posedge clk) disable iff (!rst_n)
  we_want_fast |-> (rx_limit == 3*FAST_PERIOD);
endproperty

// P24. Any received PDU resets the receive timer.
property p_rx_resets_timer;
  @(posedge clk) disable iff (!rst_n)
  pdu_received |=> (rx_cnt == '0);
endproperty

// P25. A passive port with a passive partner never transmits. This is
// a legal configuration that never aggregates, and the property makes
// it visible rather than mysterious.
property p_passive_pair_is_silent;
  @(posedge clk) disable iff (!rst_n)
  (!our_activity && !partner_activity) |-> !tx_now;
endproperty

// P26. Churn is raised only after CHURN_LIMIT of continuous unsync.
property p_churn_needs_persistence;
  @(posedge clk) disable iff (!rst_n)
  $rose(actor_churn) |-> ($past(a_unsync) == CHURN_LIMIT-1);
endproperty

// P27. Synchronising clears the churn evidence.
property p_sync_clears_churn;
  @(posedge clk) disable iff (!rst_n)
  actor_sync |=> (a_unsync == '0);
endproperty

// P28. Standing property: at least one end is active.
property p_an_active_end_exists;
  @(posedge clk) disable iff (!rst_n)
  !no_active_end;
endproperty

// P29. A mis-cable is a FINDING, not a fault. It must not clear this
// device's conformance bit -- the protocol worked.
property p_finding_is_not_a_fault;
  @(posedge clk) disable iff (!rst_n)
  (|miscabled && (fault_vector == 8'h00)) |-> conformant;
endproperty

// P30. But it must raise the degraded alarm.
property p_finding_degrades;
  @(posedge clk) disable iff (!rst_n)
  |miscabled |-> aggregate_degraded;
endproperty

// P31. conformant is exactly the conjunction of OUR faults.
property p_conformant_definition;
  @(posedge clk) disable iff (!rst_n)
  conformant <-> (fault_vector == 8'h00);
endproperty