Store-and-Forward against Cut-Through

// -----------------------------------------------------------------------
// cutthru_pkg -- shared types for forwarding-discipline selection.
// -----------------------------------------------------------------------
package cutthru_pkg;

  typedef enum logic [1:0] {
    FM_STORE_FORWARD = 2'd0,  // commit at the last octet
    FM_CUT_THROUGH   = 2'd1,  // commit at octet 14
    FM_FRAGMENT_FREE = 2'd2,  // commit at octet 64 -- runts excluded
    FM_ADAPTIVE      = 2'd3   // per-frame, Section 12
  } fwd_mode_e;

  // Why a frame could not be cut through. Each has a different remedy and
  // only one of them is a defect.
  typedef enum logic [2:0] {
    CR_OK             = 3'd0,
    CR_EGRESS_FASTER  = 3'd1,  // Section 7's rate rule -- would underrun
    CR_EGRESS_BUSY    = 3'd2,  // queued, so it has been stored anyway
    CR_MODE_FORCED    = 3'd3,  // configured store-and-forward
    CR_ERROR_RATE     = 3'd4,  // Section 12 fell back after errors
    CR_UNKNOWN_LENGTH = 3'd5   // Chapter 5.5's length/type ambiguity
  } cutthru_refusal_e;

  // What happened to a frame already in flight when it turned out bad.
  typedef enum logic [1:0] {
    LF_NONE     = 2'd0,
    LF_STOMPED  = 2'd1,  // FCS deliberately corrupted -- Section 11
    LF_TRUNCATED= 2'd2,  // transmission aborted mid-frame
    LF_PASSED   = 2'd3   // emitted intact -- the failure this chapter warns of
  } late_fault_e;

  localparam int COMMIT_CUT      = 14;    // through EtherType
  localparam int COMMIT_FRAGFREE = 64;    // Chapter 5.6's minimum
  localparam int FCS_OCTETS      = 4;

endpackage

// -----------------------------------------------------------------------
// commit_point_tracker -- says, for each octet of an arriving frame, what
// is known and whether the switch has committed.
//
// The value of making this explicit is that "committed" becomes a signal
// other modules can be checked against, rather than something implied by
// where a valid happens to assert in a pipeline.
// -----------------------------------------------------------------------
module commit_point_tracker
  import cutthru_pkg::*;
#(
  parameter int LEN_W = 14,
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             frame_start,
  input  logic             octet_valid,
  input  logic             frame_end,
  input  fwd_mode_e        mode,

  output logic [LEN_W-1:0] octets_received,
  output logic             have_destination,   // >= 6
  output logic             have_source,        // >= 12
  output logic             have_ethertype,     // >= 14
  output logic             have_min_frame,     // >= 64
  output logic             have_fcs,           // frame_end

  output logic             committed,
  output logic [LEN_W-1:0] commit_octet,
  output logic [LEN_W-1:0] octets_after_commit,
  output logic [CNT_W-1:0] c_commits,
  output logic [CNT_W-1:0] c_octets_uninspected
);

  logic [LEN_W-1:0] cnt_q;
  logic             committed_q;

  assign octets_received  = cnt_q;
  assign have_destination = (cnt_q >= LEN_W'(6));
  assign have_source      = (cnt_q >= LEN_W'(12));
  assign have_ethertype   = (cnt_q >= LEN_W'(COMMIT_CUT));
  assign have_min_frame   = (cnt_q >= LEN_W'(COMMIT_FRAGFREE));
  assign have_fcs         = frame_end;

  always_comb begin
    unique case (mode)
      FM_CUT_THROUGH:   commit_octet = LEN_W'(COMMIT_CUT);
      FM_FRAGMENT_FREE: commit_octet = LEN_W'(COMMIT_FRAGFREE);
      default:          commit_octet = '1;   // the last octet
    endcase
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cnt_q                <= '0;
      committed_q          <= 1'b0;
      c_commits            <= '0;
      c_octets_uninspected <= '0;
      octets_after_commit  <= '0;
    end else begin
      if (frame_start) begin
        cnt_q               <= '0;
        committed_q         <= 1'b0;
        octets_after_commit <= '0;
      end else if (octet_valid) begin
        cnt_q <= cnt_q + 1'b1;

        // THE COMMIT. After this edge the frame is leaving and no later
        // information can prevent it -- only Section 11's stomping can
        // mark it.
        if (!committed_q && (cnt_q + 1'b1 >= commit_octet) &&
            (mode != FM_STORE_FORWARD)) begin
          committed_q <= 1'b1;
          if (!(&c_commits)) c_commits <= c_commits + 1'b1;
        end

        // Every octet arriving after the commit is an octet the switch
        // forwarded without inspecting. On a maximum frame under cut-
        // through that is 1504 octets -- 12032 bits.
        if (committed_q) begin
          octets_after_commit  <= octets_after_commit + 1'b1;
          c_octets_uninspected <= c_octets_uninspected + 1'b1;
        end
      end

      if (frame_end && (mode == FM_STORE_FORWARD)) begin
        committed_q <= 1'b1;
        if (!(&c_commits)) c_commits <= c_commits + 1'b1;
      end
    end
  end

  assign committed = committed_q;

endmodule

// -----------------------------------------------------------------------
// gate_schedule_checker -- for each of Chapter 12.3's six gates, is its
// input available before the commit point?
//
// This module computes nothing the datapath needs. It exists so that the
// answer is a signal rather than a claim in a design document, and so
// that a design which quietly runs a gate on unavailable data is caught.
// -----------------------------------------------------------------------
module gate_schedule_checker
  import cutthru_pkg::*;
#(
  parameter int LEN_W = 14,
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             frame_active,
  input  logic [LEN_W-1:0] octets_received,
  input  logic             committed,
  input  fwd_mode_e        mode,

  // The six gates asserting that they have evaluated.
  input  logic             g1_eligibility_done,   // needs the FCS
  input  logic             g2_ingress_state_done,
  input  logic             g3_lookup_done,
  input  logic             g4_filter_done,
  input  logic             g5_egress_state_done,
  input  logic             g6_admission_done,

  output logic [5:0]       gates_available,       // input has arrived
  output logic [5:0]       gates_evaluated,
  output logic             g1_impossible,         // the chapter's thesis
  output logic [CNT_W-1:0] v_gate_ran_early,      // evaluated without input
  output logic [CNT_W-1:0] c_frames_uninspected
);

  // GATE 1 needs the frame check sequence, which is the LAST four octets.
  // Under cut-through the commit is at octet 14 and the FCS arrives at
  // octet N-4 for N up to 1518. The input is not late; it is absent.
  logic g1_input_available;
  assign g1_input_available = 1'b0;   // never, before a cut-through commit

  // GATES 2 and 5 read a port-state register. Available at octet 0.
  // GATE 3 needs the destination address -- octet 6 -- plus Chapter
  // 12.5's four-cycle lookup, which at 500 MHz is 8 ns, comfortably
  // inside the 48 ns the next 6 octets take at 1 Gb/s.
  // GATE 4 compares the lookup's answer against the ingress port.
  // GATE 6 reads queue occupancy, available at octet 0 -- but see the
  // note below on why its answer can be invalidated.
  always_comb begin
    gates_available[0] = (mode == FM_STORE_FORWARD);          // g1
    gates_available[1] = 1'b1;                                // g2
    gates_available[2] = (octets_received >= LEN_W'(6));      // g3
    gates_available[3] = (octets_received >= LEN_W'(6));      // g4
    gates_available[4] = 1'b1;                                // g5
    gates_available[5] = 1'b1;                                // g6
  end

  assign gates_evaluated = {g6_admission_done, g5_egress_state_done,
                            g4_filter_done,    g3_lookup_done,
                            g2_ingress_state_done, g1_eligibility_done};

  // THE THESIS, AS A SIGNAL. Under any early-commit mode, gate 1 cannot
  // be evaluated before the commit, because its input arrives up to
  // 12032 bits afterwards.
  assign g1_impossible = frame_active && (mode != FM_STORE_FORWARD);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_gate_ran_early     <= '0;
      c_frames_uninspected <= '0;
    end else begin
      // A gate that claims to have evaluated before its input arrived is
      // evaluating on reset values, on the previous frame's data, or on
      // an X. All three produce a decision that looks valid.
      for (int g = 0; g < 6; g++)
        if (gates_evaluated[g] && !gates_available[g])
          if (!(&v_gate_ran_early)) v_gate_ran_early <= v_gate_ran_early + 1'b1;

      if (committed && g1_impossible && !$past(committed))
        if (!(&c_frames_uninspected))
          c_frames_uninspected <= c_frames_uninspected + 1'b1;
    end
  end

endmodule

// -----------------------------------------------------------------------
// cutthrough_forwarder -- runs the five available gates and commits at
// octet 14.
//
// Note what is NOT in this module: any evaluation of frame validity. It
// is absent because it is impossible, and the absence is marked with an
// explicit output rather than left as a gap somebody later fills with a
// tied-off constant.
// -----------------------------------------------------------------------
module cutthrough_forwarder
  import cutthru_pkg::*;
#(
  parameter int N_PORTS   = 24,
  parameter int PORT_BITS = 5,
  parameter int LEN_W     = 14,
  parameter int CNT_W     = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 frame_start,
  input  logic [LEN_W-1:0]     octets_received,
  input  fwd_mode_e            mode,

  // The five gates whose inputs exist by octet 14.
  input  logic                 ingress_forwarding,   // gate 2
  input  logic                 lookup_valid,         // gate 3
  input  logic                 lookup_hit,
  input  logic [PORT_BITS-1:0] lookup_port,
  input  logic [PORT_BITS-1:0] ingress_port,         // gate 4
  input  logic [N_PORTS-1:0]   forwarding_mask,      // gate 5
  input  logic                 egress_has_room,      // gate 6

  output logic                 commit,
  output logic [N_PORTS-1:0]   egress_mask,
  output logic                 eligibility_unknown,  // ALWAYS high here
  output logic [CNT_W-1:0]     c_committed_unchecked,
  output logic [2:0]           deciding_gate
);

  logic committed_q;
  logic [N_PORTS-1:0] all_but_ingress;

  assign all_but_ingress = ~(N_PORTS'(1) << ingress_port);

  // THE ADMISSION. Chapter 12.3's composer, minus gate 1, at octet 14.
  always_comb begin
    egress_mask   = '0;
    deciding_gate = 3'd0;

    if (!ingress_forwarding) begin
      deciding_gate = 3'd2;
    end else if (!lookup_valid) begin
      // The lookup has not answered by the commit point. Chapter 12.3
      // Section 4's deadline applies here too, and it is much tighter:
      // the answer must exist by octet 14, not by 28 ns.
      deciding_gate = 3'd3;
      egress_mask   = forwarding_mask & all_but_ingress;
    end else if (lookup_hit && (lookup_port == ingress_port)) begin
      deciding_gate = 3'd4;                       // filter -- emit nothing
    end else if (lookup_hit && !forwarding_mask[lookup_port]) begin
      deciding_gate = 3'd5;
    end else if (lookup_hit && !egress_has_room) begin
      // Gate 6 at the commit point. NOTE: this answer can be invalidated
      // by the queue filling while the remaining 1504 octets arrive --
      // Section 13.
      deciding_gate = 3'd6;
    end else if (lookup_hit) begin
      egress_mask   = (N_PORTS'(1) << lookup_port);
    end else begin
      egress_mask   = forwarding_mask & all_but_ingress;
    end
  end

  // GATE 1 IS NOT HERE AND CANNOT BE. This output states that in the
  // interface rather than leaving a hole for somebody to tie off.
  assign eligibility_unknown = (mode != FM_STORE_FORWARD);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      committed_q           <= 1'b0;
      commit                <= 1'b0;
      c_committed_unchecked <= '0;
    end else begin
      commit <= 1'b0;
      if (frame_start) committed_q <= 1'b0;

      if (!committed_q && (mode != FM_STORE_FORWARD) &&
          (octets_received >= LEN_W'(COMMIT_CUT))) begin
        committed_q <= 1'b1;
        commit      <= 1'b1;
        // Every commit under an early-commit mode is a frame forwarded
        // without its validity established. The count is not an error --
        // it is the discipline's operating volume, and it belongs on a
        // report next to the error counters it can explain.
        if (!(&c_committed_unchecked))
          c_committed_unchecked <= c_committed_unchecked + 1'b1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// rate_compatibility_gate -- decides whether cut-through is even available
// for this ingress/egress pair.
//
// The arithmetic: with a head start of H bits, an egress at rate Re and
// an ingress at rate Ri, the egress has sent more than has been received
// after t = H / (Re - Ri). For a 1 Gb/s ingress feeding a 10 Gb/s egress
// with a 14-octet head start, t = 12.4 ns -- the transmitter runs dry
// having emitted 15.6 octets.
// -----------------------------------------------------------------------
module rate_compatibility_gate
  import cutthru_pkg::*;
#(
  parameter int N_PORTS   = 24,
  parameter int PORT_BITS = 5,
  parameter int CNT_W     = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  // Rates in units of 100 Mb/s, so 1 G is 10 and 10 G is 100.
  input  logic [11:0]          port_rate [N_PORTS],

  input  logic                 req_valid,
  input  logic [PORT_BITS-1:0] ingress_port,
  input  logic [PORT_BITS-1:0] egress_port,
  input  fwd_mode_e            requested_mode,
  input  logic [7:0]           head_start_octets,

  output logic                 cutthru_available,
  output fwd_mode_e            granted_mode,
  output cutthru_refusal_e     refusal,
  output logic [15:0]          underrun_ns,        // 0 when compatible
  output logic [CNT_W-1:0]     c_refused_rate,
  output logic [CNT_W-1:0]     c_granted
);

  logic [11:0] ri, re;
  assign ri = port_rate[ingress_port];
  assign re = port_rate[egress_port];

  // THE RULE. Egress must be no faster than ingress. Equal is fine --
  // the transmitter consumes exactly as fast as the receiver supplies,
  // and the head start is never spent. SLOWER egress is also fine: the
  // buffer grows, which is what a queue is for.
  logic rate_ok;
  assign rate_ok = (re <= ri);

  // How long the frame survives if the rule is violated, in nanoseconds.
  // t = H_bits / (Re - Ri), with rates in 100 Mb/s units:
  //   bits/ns at 100 Mb/s = 0.1, so (re - ri) * 0.1 bits per ns.
  always_comb begin
    if (rate_ok || (re == ri)) underrun_ns = 16'd0;
    else                       underrun_ns =
      16'((16'(head_start_octets) * 16'd8 * 16'd10) / 16'(re - ri));
  end

  always_comb begin
    cutthru_available = 1'b0;
    granted_mode      = FM_STORE_FORWARD;
    refusal           = CR_OK;

    if (req_valid) begin
      if (requested_mode == FM_STORE_FORWARD) begin
        granted_mode = FM_STORE_FORWARD;
      end else if (!rate_ok) begin
        // A speed step UPWARD -- access to aggregation, the direction of
        // almost every real network -- forces store-and-forward. This is
        // not a policy choice; the alternative emits a truncated frame.
        refusal      = CR_EGRESS_FASTER;
        granted_mode = FM_STORE_FORWARD;
      end else begin
        cutthru_available = 1'b1;
        granted_mode      = requested_mode;
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_refused_rate <= '0;
      c_granted      <= '0;
    end else if (req_valid) begin
      if (cutthru_available) begin
        if (!(&c_granted)) c_granted <= c_granted + 1'b1;
      end else if (refusal == CR_EGRESS_FASTER) begin
        if (!(&c_refused_rate)) c_refused_rate <= c_refused_rate + 1'b1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// underrun_detector -- catches a transmitter that has run out of frame.
//
// The rate gate in Section 7 prevents the configured case. This detector
// exists for the cases it cannot see: an ingress link that slows
// mid-frame (Chapter 11.4's renegotiation), a receive FIFO that stalls,
// or a rate table that disagrees with the link's actual negotiated speed.
// -----------------------------------------------------------------------
module underrun_detector
  import cutthru_pkg::*;
#(
  parameter int PORT_BITS = 5,
  parameter int LEN_W     = 14,
  parameter int CNT_W     = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 tx_active,          // mid-frame on egress
  input  logic                 tx_octet_ready,     // egress wants an octet
  input  logic                 rx_octet_available, // ingress has supplied one
  input  logic                 frame_complete,     // whole frame received
  input  logic [PORT_BITS-1:0] egress_port,
  input  logic [LEN_W-1:0]     octets_sent,

  output logic                 underrun,
  output logic                 abort_transmission,
  output late_fault_e          fault,
  output logic [CNT_W-1:0]     c_underruns,
  output logic [LEN_W-1:0]     shortest_underrun_at,
  output logic [PORT_BITS-1:0] last_underrun_port
);

  // THE CONDITION. The egress wants an octet, the ingress has not
  // supplied one, and the frame is not finished. There is no way to
  // pause: Ethernet's transmitter must emit a continuous stream from the
  // start delimiter to the FCS.
  assign underrun = tx_active && tx_octet_ready &&
                    !rx_octet_available && !frame_complete;

  // Abort rather than emit filler. Emitting idle or padding produces a
  // frame that is the WRONG LENGTH with a VALID-looking body, which a
  // receiver may accept. Aborting produces something a receiver will
  // certainly reject.
  assign abort_transmission = underrun;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      fault                <= LF_NONE;
      c_underruns          <= '0;
      shortest_underrun_at <= '1;
      last_underrun_port   <= '0;
    end else begin
      fault <= LF_NONE;
      if (underrun) begin
        fault <= LF_TRUNCATED;
        if (!(&c_underruns)) c_underruns <= c_underruns + 1'b1;
        // How far in the frame died. Section 7 predicts 15.6 octets for
        // a 1 G to 10 G step with a 14-octet head start; a measurement
        // far from the prediction means the rate table is wrong.
        if (octets_sent < shortest_underrun_at)
          shortest_underrun_at <= octets_sent;
        last_underrun_port <= egress_port;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// fcs_stomper -- deliberately corrupts the outgoing check sequence when
// the incoming one turns out to be bad.
//
// THE CONSTRUCTIVE ANSWER TO SECTION 4. Gate 1 cannot run before the
// commit. What CAN be done is to ensure the frame that was committed is
// unambiguously marked as bad by the time it finishes leaving -- so that
// every downstream device discards it, and so that no downstream
// cut-through switch relays it further.
// -----------------------------------------------------------------------
module fcs_stomper
  import cutthru_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             tx_active,
  input  logic             tx_in_fcs,          // emitting the last 4 octets
  input  logic             rx_fcs_bad,         // ingress check failed
  input  logic             rx_frame_end,
  input  logic             committed,

  input  logic [31:0]      computed_fcs,       // over what was forwarded

  output logic [31:0]      tx_fcs,
  output logic             stomped,
  output late_fault_e      fault,
  output logic [CNT_W-1:0] c_stomped,
  output logic [CNT_W-1:0] c_bad_after_commit,
  output logic [CNT_W-1:0] c_bad_before_commit
);

  logic stomp_q;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      stomp_q             <= 1'b0;
      stomped             <= 1'b0;
      fault               <= LF_NONE;
      c_stomped           <= '0;
      c_bad_after_commit  <= '0;
      c_bad_before_commit <= '0;
    end else begin
      stomped <= 1'b0;
      fault   <= LF_NONE;

      if (rx_frame_end && rx_fcs_bad) begin
        if (committed) begin
          // THE CASE THIS MODULE EXISTS FOR. The frame is already
          // leaving. Nothing can stop it; the outgoing FCS can be made
          // wrong on purpose.
          stomp_q <= 1'b1;
          if (!(&c_bad_after_commit))
            c_bad_after_commit <= c_bad_after_commit + 1'b1;
        end else begin
          // Not committed yet -- a store-and-forward path, or a frame
          // shorter than the commit point. Ordinary gate 1 rejection.
          if (!(&c_bad_before_commit))
            c_bad_before_commit <= c_bad_before_commit + 1'b1;
        end
      end

      if (stomp_q && tx_in_fcs) begin
        stomped   <= 1'b1;
        fault     <= LF_STOMPED;
        stomp_q   <= 1'b0;
        if (!(&c_stomped)) c_stomped <= c_stomped + 1'b1;
      end
    end
  end

  // INVERT the computed value rather than emitting a constant. A constant
  // could, on some frame, coincidentally BE the correct FCS -- and then
  // the corrupt frame is forwarded with a valid check sequence, which is
  // strictly the worst outcome available.
  assign tx_fcs = stomp_q ? ~computed_fcs : computed_fcs;

endmodule

// -----------------------------------------------------------------------
// latency_mode_selector -- picks store-and-forward, fragment-free or
// cut-through for THIS frame.
//
// Every input is available by octet 14, which is what makes a per-frame
// choice possible rather than a per-port configuration. The selector is
// also where an error-rate fallback lives: a port that has recently
// delivered corrupt frames should not have its frames relayed onward.
// -----------------------------------------------------------------------
module latency_mode_selector
  import cutthru_pkg::*;
#(
  parameter int N_PORTS      = 24,
  parameter int PORT_BITS    = 5,
  parameter int ERR_WINDOW   = 1_000_000,
  parameter int ERR_THRESH   = 10,          // bad frames per window
  parameter int CNT_W        = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 sel_valid,
  input  logic [PORT_BITS-1:0] ingress_port,
  input  logic                 rate_ok,          // Section 7's gate
  input  logic                 egress_idle,      // Section 10
  input  fwd_mode_e            configured_mode,
  input  logic                 length_ambiguous, // Chapter 5.5

  input  logic                 rx_frame_done,
  input  logic                 rx_frame_bad,

  output fwd_mode_e            selected_mode,
  output cutthru_refusal_e     refusal,
  output logic                 fallback_active [N_PORTS],
  output logic [CNT_W-1:0]     c_sf,
  output logic [CNT_W-1:0]     c_ff,
  output logic [CNT_W-1:0]     c_ct,
  output logic [PORT_BITS-1:0] worst_error_port
);

  logic [CNT_W-1:0] err_win [N_PORTS];
  logic [CNT_W-1:0] frames_win [N_PORTS];

  always_comb begin
    selected_mode = FM_STORE_FORWARD;
    refusal       = CR_OK;

    if (sel_valid) begin
      if (configured_mode == FM_STORE_FORWARD) begin
        refusal = CR_MODE_FORCED;
      end else if (!rate_ok) begin
        // Section 7. Not a policy -- the alternative truncates the frame.
        refusal = CR_EGRESS_FASTER;
      end else if (fallback_active[ingress_port]) begin
        // This port has recently delivered corrupt frames. Relaying them
        // spends Section 9's bandwidth on every downstream hop, so the
        // switch contains them at the cost of this port's latency.
        refusal = CR_ERROR_RATE;
      end else if (length_ambiguous) begin
        // Chapter 5.5's length/type ambiguity: a value at octets 12-13
        // below 1536 is a LENGTH, and a frame whose length is not yet
        // decidable cannot have its end predicted.
        refusal = CR_UNKNOWN_LENGTH;
      end else if (!egress_idle) begin
        // Section 10. The frame will be queued, so it has been stored
        // anyway -- and saying so keeps the counters honest about how
        // often the mechanism actually engages.
        refusal       = CR_EGRESS_BUSY;
        selected_mode = FM_STORE_FORWARD;
      end else begin
        selected_mode = configured_mode;
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int p = 0; p < N_PORTS; p++) begin
        err_win[p] <= '0; frames_win[p] <= '0; fallback_active[p] <= 1'b0;
      end
      c_sf <= '0; c_ff <= '0; c_ct <= '0;
      worst_error_port <= '0;
    end else begin
      if (sel_valid) begin
        unique case (selected_mode)
          FM_STORE_FORWARD: c_sf <= c_sf + 1'b1;
          FM_FRAGMENT_FREE: c_ff <= c_ff + 1'b1;
          FM_CUT_THROUGH:   c_ct <= c_ct + 1'b1;
          default: ;
        endcase
      end

      if (rx_frame_done) begin
        frames_win[ingress_port] <= frames_win[ingress_port] + 1'b1;
        if (rx_frame_bad) err_win[ingress_port] <= err_win[ingress_port] + 1'b1;

        if (frames_win[ingress_port] >= CNT_W'(ERR_WINDOW)) begin
          // Latch the fallback and keep it until the window is clean.
          // Oscillating between disciplines on a marginal link produces
          // a latency that varies by two orders of magnitude frame to
          // frame, which is worse for a real-time application than
          // uniformly slow.
          fallback_active[ingress_port] <=
            (err_win[ingress_port] > CNT_W'(ERR_THRESH));
          if (err_win[ingress_port] > CNT_W'(ERR_THRESH))
            worst_error_port <= ingress_port;
          err_win[ingress_port]    <= '0;
          frames_win[ingress_port] <= '0;
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// cutthrough_conformance_monitor -- checks a discipline whose defining
// property is that it decides before it knows.
//
// What it CAN check: that the commit happened at the configured octet;
// that gate 1 was never claimed to have run; that a frame found bad after
// commit was STOMPED; that the rate rule was honoured; that no frame was
// silently truncated.
//
// What it CANNOT check: that the committed frame was worth forwarding.
// That is Section 16's rejected property, and its evidence arrives 12032
// bits after the decision.
// -----------------------------------------------------------------------
module cutthrough_conformance_monitor
  import cutthru_pkg::*;
#(
  parameter int LEN_W = 14,
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             frame_start,
  input  logic             committed,
  input  logic [LEN_W-1:0] commit_octet_actual,
  input  logic [LEN_W-1:0] commit_octet_expected,
  input  fwd_mode_e        mode,

  input  logic             g1_claimed_done,
  input  logic             rate_ok,

  input  logic             rx_frame_end,
  input  logic             rx_fcs_bad,
  input  logic             tx_frame_end,
  input  late_fault_e      fault,

  output logic [CNT_W-1:0] v_commit_wrong_octet,
  output logic [CNT_W-1:0] v_gate1_claimed,      // claimed the impossible
  output logic [CNT_W-1:0] v_bad_passed_intact,  // THE critical failure
  output logic [CNT_W-1:0] v_rate_violated,
  output logic [CNT_W-1:0] v_silent_truncation,
  output logic             conformant
);

  logic committed_q, bad_pending_q;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      committed_q          <= 1'b0;
      bad_pending_q        <= 1'b0;
      v_commit_wrong_octet <= '0;
      v_gate1_claimed      <= '0;
      v_bad_passed_intact  <= '0;
      v_rate_violated      <= '0;
      v_silent_truncation  <= '0;
    end else begin
      if (frame_start) begin
        committed_q   <= 1'b0;
        bad_pending_q <= 1'b0;
      end

      if (committed && !committed_q) begin
        committed_q <= 1'b1;

        // The commit landed where the configured discipline says it
        // should. A datapath wider than one octet will commit on a word
        // boundary, and this catches a design whose real commit point
        // drifted from its documented one.
        if (commit_octet_actual != commit_octet_expected)
          if (!(&v_commit_wrong_octet))
            v_commit_wrong_octet <= v_commit_wrong_octet + 1'b1;

        // THE STRUCTURAL CHECK. Under any early-commit mode, a gate 1
        // that claims to have completed is claiming to have read the FCS
        // before it arrived -- which means it read reset values, the
        // previous frame's result, or a tie-off.
        if ((mode != FM_STORE_FORWARD) && g1_claimed_done)
          if (!(&v_gate1_claimed))
            v_gate1_claimed <= v_gate1_claimed + 1'b1;

        if (!rate_ok && (mode != FM_STORE_FORWARD))
          if (!(&v_rate_violated))
            v_rate_violated <= v_rate_violated + 1'b1;
      end

      if (rx_frame_end && rx_fcs_bad && committed_q) bad_pending_q <= 1'b1;

      if (tx_frame_end) begin
        // A frame that was known bad and left with an intact check
        // sequence is the failure this whole chapter is organised
        // around: a corrupt frame wearing a valid FCS, which every
        // device downstream will accept.
        if (bad_pending_q && (fault != LF_STOMPED) && (fault != LF_TRUNCATED))
          if (!(&v_bad_passed_intact))
            v_bad_passed_intact <= v_bad_passed_intact + 1'b1;

        // A truncation that was not reported. Chapter 12.4's missing
        // copy, in a different guise: the frame simply stopped, and
        // nothing said so.
        if ((fault == LF_TRUNCATED) && !bad_pending_q && rate_ok)
          if (!(&v_silent_truncation))
            v_silent_truncation <= v_silent_truncation + 1'b1;

        bad_pending_q <= 1'b0;
      end
    end
  end

  assign conformant = (v_commit_wrong_octet == '0) &&
                      (v_gate1_claimed      == '0) &&
                      (v_bad_passed_intact  == '0) &&
                      (v_rate_violated      == '0) &&
                      (v_silent_truncation  == '0);

endmodule

// P1. The commit lands at the octet the configured discipline names.
property p_commit_at_configured_octet;
  @(posedge clk) disable iff (!rst_n)
  $rose(committed) |-> (octets_received >= commit_octet);
endproperty
a_commit_octet: assert property (p_commit_at_configured_octet);

// P2. Store-and-forward commits ONLY at the last octet.
property p_sf_commits_at_end;
  @(posedge clk) disable iff (!rst_n)
  ((mode == FM_STORE_FORWARD) && $rose(committed)) |-> frame_end;
endproperty
a_sf_late_commit: assert property (p_sf_commits_at_end);

// P3. The commit happens at most once per frame.
property p_commit_once;
  @(posedge clk) disable iff (!rst_n)
  $rose(committed) |=> committed until_with frame_start;
endproperty
a_commit_once: assert property (p_commit_once);

// P4. Every octet after the commit is counted as uninspected -- the
// honest measure of what the discipline gave up.
property p_uninspected_counted;
  @(posedge clk) disable iff (!rst_n)
  (committed && octet_valid) |=> (octets_after_commit > $past(octets_after_commit));
endproperty
a_uninspected: assert property (p_uninspected_counted);

// P5. Fragment-free commits no earlier than the minimum frame size, so a
// runt is always fully received before any decision is irrevocable.
property p_fragfree_after_min_frame;
  @(posedge clk) disable iff (!rst_n)
  ((mode == FM_FRAGMENT_FREE) && $rose(committed))
    |-> (octets_received >= LEN_W'(COMMIT_FRAGFREE));
endproperty
a_fragfree_min: assert property (p_fragfree_after_min_frame);

// P6. THE STRUCTURAL PROPERTY. Under any early-commit mode, gate 1 never
// claims to have completed. Its input does not exist yet.
property p_gate1_never_claimed_early;
  @(posedge clk) disable iff (!rst_n)
  ((mode != FM_STORE_FORWARD) && committed) |-> !g1_eligibility_done;
endproperty
a_gate1_impossible: assert property (p_gate1_never_claimed_early);

// P7. eligibility_unknown is asserted whenever the discipline cannot run
// gate 1 -- the interface states the gap rather than leaving one.
property p_eligibility_unknown_declared;
  @(posedge clk) disable iff (!rst_n)
  (mode != FM_STORE_FORWARD) |-> eligibility_unknown;
endproperty
a_unknown_declared: assert property (p_eligibility_unknown_declared);

// P8. No gate evaluates before its input has arrived.
property p_no_gate_runs_early;
  @(posedge clk) disable iff (!rst_n)
  frame_active |-> ((gates_evaluated & ~gates_available) == '0);
endproperty
a_no_early_gate: assert property (p_no_gate_runs_early);

// P9. Gate 3's answer exists by the commit point. Under cut-through at
// 10 Gb/s that is 11.2 ns, which is tighter than Chapter 12.3's 28 ns.
property p_lookup_answers_before_commit;
  @(posedge clk) disable iff (!rst_n)
  ($rose(committed) && (mode != FM_STORE_FORWARD)) |-> lookup_valid;
endproperty
a_lookup_in_time: assert property (p_lookup_answers_before_commit);

// P10. Gates 2, 4 and 5 are evaluated before the commit -- they are
// available and skipping them would be a choice, not a necessity.
property p_available_gates_all_run;
  @(posedge clk) disable iff (!rst_n)
  $rose(committed) |-> (g2_ingress_state_done && g4_filter_done &&
                        g5_egress_state_done);
endproperty
a_available_gates_run: assert property (p_available_gates_all_run);

// P11. Cut-through is granted only when the egress is no faster than the
// ingress. Violating this truncates the frame; it is not a policy.
property p_rate_rule_enforced;
  @(posedge clk) disable iff (!rst_n)
  (req_valid && cutthru_available) |-> (port_rate[egress_port] <=
                                        port_rate[ingress_port]);
endproperty
a_rate_rule: assert property (p_rate_rule_enforced);

// P12. Equal rates are permitted -- the head start is never spent.
property p_equal_rates_allowed;
  @(posedge clk) disable iff (!rst_n)
  (req_valid && (requested_mode == FM_CUT_THROUGH) &&
   (port_rate[egress_port] == port_rate[ingress_port]))
    |-> cutthru_available;
endproperty
a_equal_ok: assert property (p_equal_rates_allowed);

// P13. A rate refusal names its reason, so it is not confused with a
// configuration or an error-rate fallback.
property p_rate_refusal_classified;
  @(posedge clk) disable iff (!rst_n)
  (req_valid && !cutthru_available &&
   (port_rate[egress_port] > port_rate[ingress_port]))
    |-> (refusal == CR_EGRESS_FASTER);
endproperty
a_refusal_named: assert property (p_rate_refusal_classified);

// P14. An underrun ABORTS rather than emitting filler. Filler produces a
// wrong-length frame with a structurally valid body.
property p_underrun_aborts;
  @(posedge clk) disable iff (!rst_n)
  underrun |-> abort_transmission;
endproperty
a_underrun_aborts: assert property (p_underrun_aborts);

// P15. Under the rate rule, no underrun occurs at all.
property p_no_underrun_when_rate_ok;
  @(posedge clk) disable iff (!rst_n)
  (tx_active && rate_ok) |-> !underrun;
endproperty
a_no_underrun: assert property (p_no_underrun_when_rate_ok);

// P16. THE CENTRAL PROPERTY. A frame found bad AFTER the commit leaves
// with a deliberately wrong check sequence.
property p_bad_after_commit_is_stomped;
  @(posedge clk) disable iff (!rst_n)
  (rx_frame_end && rx_fcs_bad && committed) |-> ##[1:$] (stomped or abort_transmission);
endproperty
a_stomp_or_abort: assert property (p_bad_after_commit_is_stomped);

// P17. A frame known bad NEVER leaves with a valid check sequence. This
// is the failure the whole chapter is organised around.
property p_bad_never_passes_intact;
  @(posedge clk) disable iff (!rst_n)
  (tx_frame_end && bad_pending_q) |-> (fault inside {LF_STOMPED, LF_TRUNCATED});
endproperty
a_never_pass_bad: assert property (p_bad_never_passes_intact);

// P18. The stomp INVERTS the computed value. A constant could, once in
// 2^32 frames, coincide with the correct FCS -- once every 48 minutes on
// a loaded gigabit link.
property p_stomp_inverts;
  @(posedge clk) disable iff (!rst_n)
  stomped |-> (tx_fcs == ~computed_fcs);
endproperty
a_stomp_inverts: assert property (p_stomp_inverts);

// P19. A good frame is never stomped.
property p_good_never_stomped;
  @(posedge clk) disable iff (!rst_n)
  (tx_in_fcs && !rx_fcs_bad) |-> !stomped;
endproperty
a_good_intact: assert property (p_good_never_stomped);

// P20. Bad frames are counted by WHETHER they were containable, because
// the split is the diagnosis.
property p_bad_split_by_commit;
  @(posedge clk) disable iff (!rst_n)
  (rx_frame_end && rx_fcs_bad)
    |=> ($changed(c_bad_after_commit) ^ $changed(c_bad_before_commit));
endproperty
a_bad_split: assert property (p_bad_split_by_commit);

// P21. A truncation is never silent.
property p_truncation_reported;
  @(posedge clk) disable iff (!rst_n)
  abort_transmission |-> ##[1:4] (fault == LF_TRUNCATED);
endproperty
a_truncation_reported: assert property (p_truncation_reported);

// P22. A frame whose egress is busy is reported as CR_EGRESS_BUSY, so
// c_ct counts frames that actually streamed rather than intentions.
property p_busy_egress_reported;
  @(posedge clk) disable iff (!rst_n)
  (sel_valid && !egress_idle && (configured_mode != FM_STORE_FORWARD))
    |-> (refusal == CR_EGRESS_BUSY);
endproperty
a_busy_reported: assert property (p_busy_egress_reported);

// P23. A port with a recent error history falls back to store-and-forward
// -- containing corruption at the cost of one port's latency.
property p_error_fallback_engages;
  @(posedge clk) disable iff (!rst_n)
  (sel_valid && fallback_active[ingress_port])
    |-> (selected_mode == FM_STORE_FORWARD);
endproperty
a_error_fallback: assert property (p_error_fallback_engages);

// P24. The fallback LATCHES for a whole window. Oscillating between
// disciplines produces a latency that varies 108x frame to frame.
property p_fallback_latches;
  @(posedge clk) disable iff (!rst_n)
  ($rose(fallback_active[ingress_port]) && !window_end)
    |=> fallback_active[ingress_port];
endproperty
a_fallback_stable: assert property (p_fallback_latches);

// P25. Chapter 5.5's length/type ambiguity forces store-and-forward -- a
// frame whose end cannot be predicted cannot be streamed safely.
property p_ambiguous_length_forces_sf;
  @(posedge clk) disable iff (!rst_n)
  (sel_valid && length_ambiguous) |-> (selected_mode == FM_STORE_FORWARD);
endproperty
a_ambiguous_sf: assert property (p_ambiguous_length_forces_sf);

// P26. Exactly one discipline counter moves per selection.
property p_one_mode_counted;
  @(posedge clk) disable iff (!rst_n)
  sel_valid |=> (($changed(c_sf) + $changed(c_ff) + $changed(c_ct)) == 1);
endproperty
a_one_mode: assert property (p_one_mode_counted);

// P27. Conformance means the discipline behaved as specified -- never
// that the forwarded frames were good.
property p_conformant_definition;
  @(posedge clk) disable iff (!rst_n)
  conformant |-> ((v_commit_wrong_octet == '0) && (v_gate1_claimed == '0) &&
                  (v_bad_passed_intact == '0) && (v_rate_violated == '0) &&
                  (v_silent_truncation == '0));
endproperty
a_conformant_def: assert property (p_conformant_definition);

// P28. Store-and-forward forwards ZERO uninspected octets. The chapter's
// baseline, asserted rather than assumed.
property p_sf_inspects_everything;
  @(posedge clk) disable iff (!rst_n)
  ((mode == FM_STORE_FORWARD) && frame_end) |-> (octets_after_commit == '0);
endproperty
a_sf_full_inspection: assert property (p_sf_inspects_everything);