Frame Format Overview

minimum frame  =  6 + 6 + 2 + 46   + 4 =   64 octets
maximum frame  =  6 + 6 + 2 + 1500 + 4 = 1518 octets

// SYNTHESIZABLE. Field offsets derived from tag depth.
//
// A field-offset TABLE is the natural way to document a frame and it encodes
// an assumption that is false the moment a VLAN tag exists. This computes
// instead, from what has already been observed.
//
// The offsets that move, and by how much:
//
//   tags   destination  source  classification  payload
//   ----   -----------  ------  --------------  -------
//     0         0          6          12           14
//     1         0          6          16           18
//     2         0          6          20           22
//
// Destination and source NEVER move -- they precede the insertion point --
// which is why Section 2's early-abandon argument survives tagging intact.
package frame_pkg;
  localparam int unsigned OCT_DA    = 6;
  localparam int unsigned OCT_SA    = 6;
  localparam int unsigned OCT_CLASS = 2;
  localparam int unsigned OCT_FCS   = 4;
  localparam int unsigned OCT_TAG   = 4;
 
  // Tag protocol identifiers, as published. A parser recognises these to
  // know a tag is present; it does not need to interpret the rest of it.
  localparam logic [15:0] TPID_C_TAG = 16'h8100;   // customer tag
  localparam logic [15:0] TPID_S_TAG = 16'h88A8;   // service tag, outer
 
  // The five decision groups of Section 3, as a parser state.
  typedef enum logic [2:0] {
    FLD_DA,
    FLD_SA,
    FLD_TAG,
    FLD_CLASS,
    FLD_PAYLOAD,
    FLD_FCS,
    FLD_DONE
  } field_e;
endpackage
 
module frame_field_positions
  import frame_pkg::*;
#(
  // Maximum tag depth this parser will follow. A BOUND is mandatory:
  // Section 4 showed tags nest, and a walker with no bound can be made to
  // walk forever by a crafted frame. Section 7 develops that.
  parameter int unsigned MAX_TAGS = 2
) (
  input  logic [$clog2(MAX_TAGS+1)-1:0] tag_count,
 
  output int unsigned off_da,
  output int unsigned off_sa,
  output int unsigned off_class,
  output int unsigned off_payload,
 
  // Frame sizes for this tag depth. Both move with tagging, and a design
  // that checks size against an untagged constant rejects legal frames.
  output int unsigned min_frame_octets,
  output int unsigned max_frame_octets
);
 
  // Destination and source are before the insertion point, so they are
  // constant. Everything after it shifts by four octets per tag.
  assign off_da      = 0;
  assign off_sa      = OCT_DA;
  assign off_class   = OCT_DA + OCT_SA + (tag_count * OCT_TAG);
  assign off_payload = off_class + OCT_CLASS;
 
  // 64 and 1518 untagged; 68 and 1522 with one tag. A design that hard-codes
  // 1518 drops legal tagged frames and reports them as oversized, which
  // sends the investigation to the far end rather than to itself.
  assign min_frame_octets = 64   + (tag_count * OCT_TAG);
  assign max_frame_octets = 1518 + (tag_count * OCT_TAG);
 
endmodule

// SYNTHESIZABLE. Streaming frame parser.
//
// IT EMITS BOUNDARIES, NOT A STRUCT, and the difference is architectural.
//
// A struct is only available once the whole frame has arrived. Producing one
// therefore requires buffering the frame and defeats the early abandonment
// Section 2 showed the field ORDER exists to enable. A parser that hands the
// address filter a struct has thrown away the reason the address is second.
//
// So this emits a pulse at each field boundary with the field's identity,
// and a consumer acts when the field it cares about completes.
module frame_stream_parser
  import frame_pkg::*;
#(
  parameter int unsigned MAX_TAGS  = 2,
  parameter int unsigned MAX_FRAME = 1522 + 8,
  parameter int unsigned CNT_W     = $clog2(MAX_FRAME + 1)
) (
  input  logic       clk,
  input  logic       rst_n,
 
  input  logic       in_valid,
  input  logic [7:0] in_octet,
  input  logic       in_sof,      // from the layer below: a frame starts here
  input  logic       in_eof,
 
  // Boundary events. One pulse as each field completes, naming the field.
  output logic       field_done,
  output field_e     field_id,
  output logic [CNT_W-1:0] field_end_offset,
 
  // The current field, continuously, so a consumer can capture octets as
  // they pass rather than waiting for a completion pulse.
  output field_e     current_field,
  output logic [CNT_W-1:0] octet_index,
 
  // Discovered tag depth. An OUTPUT rather than a parameter, because it is
  // a property of the frame in flight.
  output logic [$clog2(MAX_TAGS+2)-1:0] tags_seen
);
 
  field_e            state_q;
  logic [CNT_W-1:0]  idx_q;
  logic [CNT_W-1:0]  field_start_q;
  logic [15:0]       class_shift_q;
  logic [$clog2(MAX_TAGS+2)-1:0] tags_q;
 
  // A candidate classification field is complete when two octets have been
  // gathered. Whether it is a TAG identifier or the real classification is
  // the decision below.
  wire [15:0] candidate_c = {class_shift_q[7:0], in_octet};
  wire is_tag_c = (candidate_c == TPID_C_TAG) || (candidate_c == TPID_S_TAG);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      state_q       <= FLD_DA;
      idx_q         <= '0;
      field_start_q <= '0;
      class_shift_q <= '0;
      tags_q        <= '0;
      field_done    <= 1'b0;
      field_id      <= FLD_DA;
    end else begin
      field_done <= 1'b0;
 
      if (in_valid && in_sof) begin
        state_q       <= FLD_DA;
        idx_q         <= '0;
        field_start_q <= '0;
        tags_q        <= '0;
      end else if (in_valid) begin
        idx_q <= idx_q + 1'b1;
 
        unique case (state_q)
          FLD_DA:
            if (idx_q == CNT_W'(OCT_DA - 1)) begin
              field_done <= 1'b1;
              field_id   <= FLD_DA;
              state_q    <= FLD_SA;
              // The earliest abandon point. A consumer acts HERE.
            end
 
          FLD_SA:
            if (idx_q == CNT_W'(OCT_DA + OCT_SA - 1)) begin
              field_done <= 1'b1;
              field_id   <= FLD_SA;
              state_q    <= FLD_CLASS;
              class_shift_q <= '0;
            end
 
          FLD_CLASS: begin
            class_shift_q <= {class_shift_q[7:0], in_octet};
            // Two octets gathered: decide whether this is a tag or the
            // classification field itself.
            if (idx_q[0] != field_start_q[0]) begin
              if (is_tag_c && (tags_q < ($clog2(MAX_TAGS+2))'(MAX_TAGS))) begin
                // A tag. Consume its remaining two octets and look again.
                tags_q     <= tags_q + 1'b1;
                field_done <= 1'b1;
                field_id   <= FLD_TAG;
                state_q    <= FLD_TAG;
              end else begin
                // Not a tag, or the depth bound is reached. This is the
                // classification field -- Chapter 5.5 owns what it means.
                field_done <= 1'b1;
                field_id   <= FLD_CLASS;
                state_q    <= FLD_PAYLOAD;
              end
            end
          end
 
          FLD_TAG:
            // The tag's two control octets, then back to look for another.
            if (idx_q[0] == field_start_q[0]) begin
              state_q       <= FLD_CLASS;
              class_shift_q <= '0;
            end
 
          FLD_PAYLOAD:
            if (in_eof) begin
              field_done <= 1'b1;
              field_id   <= FLD_PAYLOAD;
              state_q    <= FLD_DONE;
            end
 
          default: ;
        endcase
      end
    end
  end
 
  assign current_field    = state_q;
  assign octet_index      = idx_q;
  assign field_end_offset = idx_q;
  assign tags_seen        = tags_q;
 
endmodule

// SYNTHESIZABLE INSTRUMENTATION.
//
// THE IDEA: a frame that fails to parse should say WHICH FIELD it was in,
// not merely that it failed.
//
// The reason this is worth silicon is that each field is produced by a
// different part of the transmitter, so the stopping field names a
// subsystem:
//
//   stopped in DA/SA   -> truncation very early: a PHY or link fault
//   stopped in CLASS   -> a tag walk that ran out of depth, or a truncation
//                         at exactly the wrong place
//   stopped in PAYLOAD -> a MAC-side underrun (Chapter 4.3 §5's abort path)
//   stopped in FCS     -> the frame ended a few octets short: a length or
//                         padding fault, not a link fault
//
// A single "malformed frame" counter conflates four different owners.
module parse_stop_observer
  import frame_pkg::*;
#(
  parameter int unsigned CNT_W = 24,
  parameter int unsigned OFF_W = 12
) (
  input  logic   clk,
  input  logic   rst_n,
  input  logic   clear,
 
  input  logic   frame_ended,      // end of frame, from the layer below
  input  logic   parse_complete,   // the parser reached FLD_DONE cleanly
  input  field_e current_field,
  input  logic [OFF_W-1:0] octet_index,
 
  // Per-field stop counts. The whole point of the module.
  output logic [CNT_W-1:0] c_stopped_in [7],
 
  // The field the FIRST failure stopped in, and how far into the frame.
  // Held, because by the time anyone looks the counters will all have moved
  // and only ordering distinguishes a cause from its consequences.
  output field_e           first_stop_field,
  output logic [OFF_W-1:0] first_stop_offset,
  output logic             first_stop_valid,
 
  // Frames that parsed cleanly. The denominator -- a stop count without it
  // cannot distinguish a broken link from a busy one.
  output logic [CNT_W-1:0] c_parsed_ok
);
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;   // saturating, never wrapping
  endfunction
 
  wire stopped_early_c = frame_ended && !parse_complete;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int unsigned f = 0; f < 7; f++) c_stopped_in[f] <= '0;
      c_parsed_ok       <= '0;
      first_stop_field  <= FLD_DA;
      first_stop_offset <= '0;
      first_stop_valid  <= 1'b0;
    end else begin
      if (clear) begin
        for (int unsigned f = 0; f < 7; f++) c_stopped_in[f] <= '0;
        c_parsed_ok <= '0;
        // first_stop deliberately survives: it is the record of what went
        // wrong first, and clearing counters must not erase it.
      end else begin
        if (stopped_early_c)
          c_stopped_in[current_field] <= bump(c_stopped_in[current_field], 1'b1);
        c_parsed_ok <= bump(c_parsed_ok, frame_ended && parse_complete);
      end
 
      if (stopped_early_c && !first_stop_valid) begin
        first_stop_valid  <= 1'b1;
        first_stop_field  <= current_field;
        first_stop_offset <= octet_index;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE. Malformed-frame classification, as a vector.
//
// WHY A VECTOR AND NOT AN ENUM. Chapter 2.7 §7's forwarding disposition was
// one-hot because a frame goes to exactly one place. Malformation is not
// like that: a frame can be undersized AND have an unparseable tag stack
// AND fail its check value, and each of those points somewhere different.
//
// Collapsing them to one enum forces a priority that discards evidence, and
// the discarded evidence is usually the part that names the cause.
module malformed_classifier
  import frame_pkg::*;
#(
  parameter int unsigned CNT_W = 24,
  parameter int unsigned OFF_W = 12
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic             frame_ended,
  input  logic [OFF_W-1:0] frame_octets,       // excluding preamble and SFD
  input  logic [OFF_W-1:0] min_frame_octets,   // from Section 5, tag-aware
  input  logic [OFF_W-1:0] max_frame_octets,
  input  logic             parse_complete,
  input  logic             tag_depth_exceeded,
  input  logic             fcs_ok,
 
  // Independent, and several may be set on one frame.
  output logic m_undersized,
  output logic m_oversized,
  output logic m_unparseable,
  output logic m_tag_overflow,
  output logic m_bad_fcs,
  output logic m_any,
 
  output logic [CNT_W-1:0] c_undersized,
  output logic [CNT_W-1:0] c_oversized,
  output logic [CNT_W-1:0] c_unparseable,
  output logic [CNT_W-1:0] c_tag_overflow,
  output logic [CNT_W-1:0] c_bad_fcs,
 
  // Frames with MORE THAN ONE fault. Rare on a healthy link, and a rising
  // count means the faults share a cause rather than being independent --
  // which is a different investigation from any single count rising.
  output logic [CNT_W-1:0] c_multi_fault
);
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;
  endfunction
 
  always_comb begin
    // Size is checked against the TAG-AWARE limits of Section 5. Checking
    // against a hard-coded 1518 reports legal tagged frames as oversized.
    m_undersized   = frame_ended && (frame_octets < min_frame_octets);
    m_oversized    = frame_ended && (frame_octets > max_frame_octets);
    m_unparseable  = frame_ended && !parse_complete;
    m_tag_overflow = frame_ended && tag_depth_exceeded;
    m_bad_fcs      = frame_ended && !fcs_ok;
    m_any = m_undersized || m_oversized || m_unparseable
         || m_tag_overflow || m_bad_fcs;
  end
 
  logic [2:0] fault_count_c;
  always_comb begin
    fault_count_c = 3'(m_undersized) + 3'(m_oversized) + 3'(m_unparseable)
                  + 3'(m_tag_overflow) + 3'(m_bad_fcs);
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_undersized   <= '0;
      c_oversized    <= '0;
      c_unparseable  <= '0;
      c_tag_overflow <= '0;
      c_bad_fcs      <= '0;
      c_multi_fault  <= '0;
    end else begin
      c_undersized   <= bump(c_undersized,   m_undersized);
      c_oversized    <= bump(c_oversized,    m_oversized);
      c_unparseable  <= bump(c_unparseable,  m_unparseable);
      c_tag_overflow <= bump(c_tag_overflow, m_tag_overflow);
      c_bad_fcs      <= bump(c_bad_fcs,      m_bad_fcs);
      c_multi_fault  <= bump(c_multi_fault,  frame_ended && (fault_count_c > 3'd1));
    end
  end
 
endmodule

// SYNTHESIZABLE. Provisional-decision tracking.
//
// Section 9: every decision before the check value is made on unverified
// data. That is unavoidable. What is avoidable is not KNOWING which
// decisions were provisional when the check value fails.
//
// This records them and, on a failure, enumerates what must be undone --
// and separately counts how often an EXTERNALLY VISIBLE action was taken
// provisionally, because that is the number that decides whether
// cut-through is safe for a given deployment.
module provisional_tracker #(
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  // Decisions, as they are taken. Each pulses once per frame at most.
  input  logic took_address_decision,
  input  logic took_queue_decision,
  input  logic took_learning_decision,
  input  logic took_forward_decision,     // EXTERNALLY VISIBLE -- cannot be undone
 
  input  logic frame_ended,
  input  logic fcs_ok,
 
  // What was provisional on this frame, latched until the verdict.
  output logic [3:0] provisional_mask,
 
  // On a failure: what must be undone, and whether anything cannot be.
  output logic       undo_required,
  output logic [3:0] undo_mask,
  output logic       irrevocable,          // a forward already happened
 
  output logic [CNT_W-1:0] c_frames,
  output logic [CNT_W-1:0] c_fcs_fail,
  // Failures where an irrevocable action had already been taken. THIS is
  // the number that decides whether cut-through is acceptable here.
  output logic [CNT_W-1:0] c_irrevocable_on_fail,
 
  // Longest provisional window in octets, from the first decision to the
  // verdict. Sizing an undo queue from the average rather than this is the
  // same trap Chapter 4.3 §10 named for burst depth.
  input  logic [11:0]  octet_index,
  output logic [11:0]  longest_provisional_window
);
 
  logic [3:0]  mask_q;
  logic [11:0] first_decision_at_q;
  logic        window_open_q;
 
  function automatic logic [CNT_W-1:0] bump(input logic [CNT_W-1:0] v,
                                            input logic             en);
    bump = (en && !(&v)) ? (v + 1'b1) : v;
  endfunction
 
  wire any_decision_c = took_address_decision || took_queue_decision
                     || took_learning_decision || took_forward_decision;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      mask_q                     <= '0;
      first_decision_at_q        <= '0;
      window_open_q              <= 1'b0;
      c_frames                   <= '0;
      c_fcs_fail                 <= '0;
      c_irrevocable_on_fail      <= '0;
      longest_provisional_window <= '0;
    end else begin
      if (clear) begin
        c_frames              <= '0;
        c_fcs_fail            <= '0;
        c_irrevocable_on_fail <= '0;
        // longest_provisional_window deliberately survives.
      end
 
      // Open the window on the first decision of a frame.
      if (any_decision_c && !window_open_q) begin
        window_open_q       <= 1'b1;
        first_decision_at_q <= octet_index;
      end
 
      if (took_address_decision)  mask_q[0] <= 1'b1;
      if (took_queue_decision)    mask_q[1] <= 1'b1;
      if (took_learning_decision) mask_q[2] <= 1'b1;
      if (took_forward_decision)  mask_q[3] <= 1'b1;
 
      if (frame_ended) begin
        c_frames <= bump(c_frames, 1'b1);
        if (!fcs_ok) begin
          c_fcs_fail <= bump(c_fcs_fail, 1'b1);
          // A forward already happened and cannot be recalled.
          c_irrevocable_on_fail <= bump(c_irrevocable_on_fail, mask_q[3]);
        end
 
        if (window_open_q) begin
          automatic logic [11:0] w = octet_index - first_decision_at_q;
          if (w > longest_provisional_window) longest_provisional_window <= w;
        end
 
        mask_q        <= '0;
        window_open_q <= 1'b0;
      end
    end
  end
 
  assign provisional_mask = mask_q;
  assign undo_required    = frame_ended && !fcs_ok && (mask_q != '0);
  assign undo_mask        = undo_required ? mask_q : 4'd0;
  assign irrevocable      = frame_ended && !fcs_ok && mask_q[3];
 
endmodule

// ─── FRAME PROPERTY: addresses never move ──────────────────────────────────
// Destination and source precede the tag insertion point, so their offsets
// are constant at every tag depth. This is what makes Section 2's early
// abandonment survive tagging, and a design that recomputes them is either
// wrong or doing needless work.
property p_addresses_do_not_move;
  @(posedge clk) disable iff (!rst_n)
  (off_da == 0) && (off_sa == 6);
endproperty
 
// ─── FRAME PROPERTY: classification shifts four octets per tag ─────────────
// Catches a hard-coded offset 12, which reads a tag identifier as a type on
// every tagged frame -- and 0x8100 looks like an unrecognised protocol
// rather than an error, so nothing reports a failure.
property p_class_offset_tracks_tags;
  @(posedge clk) disable iff (!rst_n)
  (off_class == 12 + (tag_count * 4));
endproperty
 
// ─── FRAME PROPERTY: the size limits move with tagging ─────────────────────
// Catches a length check against a hard-coded 1518, which rejects legal
// tagged frames and reports them as oversized -- pointing the investigation
// at the transmitter for a fault in the receiver.
property p_size_limits_track_tags;
  @(posedge clk) disable iff (!rst_n)
  (max_frame_octets == 1518 + (tag_count * 4))
    && (min_frame_octets == 64 + (tag_count * 4));
endproperty
 
// ─── Ordering: fields complete in dependency order ─────────────────────────
// Section 2's argument, asserted. Catches a parser that can report a
// classification boundary before an address boundary, which means its state
// machine has a path the frame format does not have.
property p_field_order_is_monotone;
  @(posedge clk) disable iff (!rst_n)
  (field_done && (field_id == FLD_CLASS)) |-> $past(current_field != FLD_DA);
endproperty
 
// ─── Safety: the destination boundary is at octet six ──────────────────────
// The earliest abandon point. Catches a parser that reports it late, which
// silently costs the receive path the early abandonment the field order
// exists to provide.
property p_da_boundary_at_six;
  @(posedge clk) disable iff (!rst_n)
  (field_done && (field_id == FLD_DA)) |-> (field_end_offset == 5);
endproperty
 
// ─── Bounded response: the tag walk terminates ─────────────────────────────
// Tags nest, so a walker without a bound can be made to walk forever by a
// crafted frame. Catches a missing bound, which is a denial-of-service
// surface rather than merely a bug.
property p_tag_walk_bounded;
  @(posedge clk) disable iff (!rst_n)
  (tags_seen <= MAX_TAGS);
endproperty
 
// ─── Causation: a stop is recorded against the field it stopped in ─────────
// Catches telemetry that records a stop against the wrong field, which
// names the wrong subsystem with apparent authority.
property p_stop_recorded_correctly;
  @(posedge clk) disable iff (!rst_n)
  (frame_ended && !parse_complete)
    |=> (c_stopped_in[$past(current_field)] == $past(c_stopped_in[$past(current_field)]) + 1);
endproperty
 
// ─── Conservation: every ended frame is counted once ───────────────────────
// Catches a frame counted as neither parsed nor stopped, which makes the
// rate that Section 7 depends on incomputable.
property p_every_frame_classified;
  @(posedge clk) disable iff (!rst_n)
  frame_ended |-> (parse_complete ^ (current_field != FLD_DONE));
endproperty
 
// ─── Safety: malformation is a vector, not an enum ─────────────────────────
// Catches a classifier that forces one-hot, which discards evidence -- and
// the discarded evidence is usually the part that names the cause.
property p_malformation_may_be_multiple;
  @(posedge clk) disable iff (!rst_n)
  (m_undersized && m_bad_fcs) |-> m_any;
endproperty
 
// ─── Causation: size checks use the tag-aware limits ───────────────────────
// Catches a size check wired to a constant rather than to Section 5's
// output, which is the same fault as the offset table one layer up.
property p_size_check_uses_computed_limits;
  @(posedge clk) disable iff (!rst_n)
  m_oversized |-> (frame_octets > max_frame_octets);
endproperty
 
// ─── Safety: an irrevocable action is flagged on failure ───────────────────
// Catches a design that treats a forwarded frame as undoable, which it is
// not -- and the flag is what tells an operator the corruption left the box.
property p_irrevocable_flagged;
  @(posedge clk) disable iff (!rst_n)
  (frame_ended && !fcs_ok && provisional_mask[3]) |-> irrevocable;
endproperty
 
// ─── Conservation: the undo mask matches what was taken ────────────────────
// Catches an undo list that omits a decision, leaving state behind after a
// failed frame -- which then corrupts the NEXT frame's handling.
property p_undo_mask_complete;
  @(posedge clk) disable iff (!rst_n)
  undo_required |-> (undo_mask == provisional_mask);
endproperty
 
// ─── Stability: the first stop survives a clear ────────────────────────────
// Catches it folded into the clear branch, destroying the record of what
// went wrong first when everything else has moved.
property p_first_stop_survives_clear;
  @(posedge clk) disable iff (!rst_n)
  (clear && first_stop_valid) |=> first_stop_valid;
endproperty
 
// ─── Stability: the provisional window records the maximum ─────────────────
// Catches an average creeping in where a maximum belongs, which undersizes
// an undo queue for exactly the frames that need it most.
property p_window_is_maximum;
  @(posedge clk) disable iff (!rst_n)
  1'b1 |=> (longest_provisional_window >= $past(longest_provisional_window));
endproperty