Access Ports, Trunk Ports and Tag Handling

// -----------------------------------------------------------------------
// vlanport_pkg -- shared types for VLAN port modes.
//
// This chapter owns the TRANSFORMATION. Chapter 13.2 owns the tag's
// fields, Chapter 13.1 owns why VLANs exist, and Chapter 13.4 owns the
// lookup datapath this chapter feeds.
// -----------------------------------------------------------------------
package vlanport_pkg;

  localparam int VID_W  = 12;
  localparam int PCP_W  = 3;

  // What a port will accept. The third value exists for a port facing a
  // device that always tags -- a virtualisation host or a router -- and
  // is the only place a station is expected to know what a VLAN is.
  typedef enum logic [1:0] {
    AFT_ADMIT_ALL       = 2'd0,
    AFT_TAGGED_ONLY     = 2'd1,
    AFT_UNTAGGED_ONLY   = 2'd2
  } accept_types_e;

  // What the egress does to represent a VLAN on this port.
  typedef enum logic [1:0] {
    EG_STRIP  = 2'd0,   // VLAN is in this port's UNTAGGED set
    EG_TAG    = 2'd1,   // VLAN is in this port's TAGGED set
    EG_PASS   = 2'd2,   // already correct -- no transformation
    EG_DROP   = 2'd3    // port is not a member of this VLAN
  } egress_action_e;

  // Why a frame was refused. Each has a different remedy and only two of
  // them are faults.
  typedef enum logic [2:0] {
    VR_OK              = 3'd0,
    VR_WRONG_TYPE      = 3'd1,  // acceptable-frame-types said no
    VR_INGRESS_FILTER  = 3'd2,  // port is not a member of the assigned VID
    VR_RESERVED_VID    = 3'd3,  // 0 handled separately, 4095 refused
    VR_EGRESS_NOT_MEM  = 3'd4,  // Chapter 13.1's isolation, at the egress
    VR_LENGTH          = 3'd5   // transformation produced an illegal length
  } vlan_reject_e;

  // Per-port configuration. Section 4's matrix is entirely a function of
  // these five fields plus Chapter 13.1's membership array.
  typedef struct packed {
    logic [VID_W-1:0] pvid;            // assigned to untagged arrivals
    accept_types_e    accept;
    logic             ingress_filter;  // Section 8 -- optional, and it matters
    logic             is_trunk;        // annotation; behaviour comes from the sets
  } port_cfg_t;

endpackage

// -----------------------------------------------------------------------
// port_mode_config -- the per-port state that drives every transformation.
//
// "Access port" and "trunk port" are NOT modes in the hardware. They are
// names for particular settings of these fields, and a design that
// implements them as an enumerated mode has hard-coded two points of a
// continuous space and made the third case -- a hybrid port -- impossible.
// -----------------------------------------------------------------------
module port_mode_config
  import vlanport_pkg::*;
#(
  parameter int N_PORTS = 24,
  parameter int N_VLANS = 64,
  parameter int VIDX_W  = 6,
  parameter int CNT_W   = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 cfg_valid,
  input  logic [4:0]           cfg_port,
  input  port_cfg_t            cfg_data,
  input  logic                 cfg_untagged_set_we,
  input  logic [VIDX_W-1:0]    cfg_untagged_vidx,
  input  logic                 cfg_untagged_bit,

  input  logic [4:0]           rd_port,
  input  logic [VIDX_W-1:0]    rd_vidx,

  output port_cfg_t            cfg,
  output logic                 vlan_is_untagged_here,

  output logic [CNT_W-1:0]     bits_pvid,
  output logic [CNT_W-1:0]     bits_untagged_sets,
  output logic [CNT_W-1:0]     bits_total,
  output logic [5:0]           n_access_like,
  output logic [5:0]           n_trunk_like
);

  port_cfg_t          cfgs      [N_PORTS];
  // THE UNTAGGED SET. One bit per VLAN per port, and it is a SEPARATE
  // vector from Chapter 13.1's membership: a port may be a member of a
  // VLAN and carry it tagged, or be a member and carry it untagged. The
  // two questions are independent.
  logic [N_VLANS-1:0] untagged  [N_PORTS];

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int p = 0; p < N_PORTS; p++) begin
        cfgs[p]     <= '0;
        untagged[p] <= '0;
      end
    end else begin
      if (cfg_valid)           cfgs[cfg_port] <= cfg_data;
      if (cfg_untagged_set_we) untagged[cfg_port][cfg_untagged_vidx] <= cfg_untagged_bit;
    end
  end

  assign cfg                   = cfgs[rd_port];
  assign vlan_is_untagged_here = untagged[rd_port][rd_vidx];

  // Cost. Section 10 compares these against Chapter 13.1's 60 KiB.
  assign bits_pvid          = CNT_W'(N_PORTS) * CNT_W'(VID_W);
  assign bits_untagged_sets = CNT_W'(N_PORTS) * CNT_W'(N_VLANS);
  assign bits_total         = bits_pvid + bits_untagged_sets +
                              (CNT_W'(N_PORTS) * CNT_W'(3));

  // "Access-like" and "trunk-like" are DERIVED, not configured: a port
  // whose untagged set has exactly one bit behaves as an access port, and
  // one with several tagged VLANs behaves as a trunk. Reporting the
  // derived shape catches a port configured as neither.
  always_comb begin
    n_access_like = 6'd0;
    n_trunk_like  = 6'd0;
    for (int p = 0; p < N_PORTS; p++) begin
      if ($countones(untagged[p]) == 1) n_access_like = n_access_like + 6'd1;
      else if ($countones(untagged[p]) == 0) n_trunk_like = n_trunk_like + 6'd1;
    end
  end

endmodule

// -----------------------------------------------------------------------
// acceptable_frame_filter -- does this port accept a frame of this FORM?
//
// The test is on the frame's form -- did it arrive with a tag -- and NOT
// on whether it carries a VLAN assignment. A VID-0 frame is tagged and is
// refused by an untagged-only port, even though it assigns no VLAN.
// Section 4's table has the two senses side by side.
// -----------------------------------------------------------------------
module acceptable_frame_filter
  import vlanport_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             frame_valid,
  input  logic             arrived_tagged,     // Chapter 13.2's tag_count != 0
  input  logic [VID_W-1:0] carried_vid,
  input  accept_types_e    accept,

  output logic             admit,
  output vlan_reject_e     reject,

  output logic [CNT_W-1:0] c_admitted,
  output logic [CNT_W-1:0] c_refused_type,
  output logic [CNT_W-1:0] c_vid_zero_admitted,
  output logic [CNT_W-1:0] c_reserved_refused
);

  logic vid_reserved;
  // Chapter 13.2 Section 4: 4095 is reserved and names no VLAN. Unlike 0,
  // it has no defined alternative meaning, so it is refused outright.
  assign vid_reserved = arrived_tagged && (carried_vid == 12'd4095);

  always_comb begin
    admit  = 1'b0;
    reject = VR_OK;

    if (frame_valid) begin
      if (vid_reserved) begin
        reject = VR_RESERVED_VID;
      end else begin
        unique case (accept)
          AFT_ADMIT_ALL:     admit = 1'b1;
          // THE FORM TEST. A VID-0 frame is TAGGED and passes here, even
          // though Section 7 will assign it the PVID as though it were
          // untagged.
          AFT_TAGGED_ONLY:   begin
            admit  = arrived_tagged;
            if (!arrived_tagged) reject = VR_WRONG_TYPE;
          end
          AFT_UNTAGGED_ONLY: begin
            admit  = !arrived_tagged;
            if (arrived_tagged) reject = VR_WRONG_TYPE;
          end
          default: admit = 1'b1;
        endcase
      end
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_admitted          <= '0;
      c_refused_type      <= '0;
      c_vid_zero_admitted <= '0;
      c_reserved_refused  <= '0;
    end else if (frame_valid) begin
      if (admit) begin
        c_admitted <= c_admitted + 1'b1;
        // A priority-only frame that was accepted. Chapter 13.2's
        // c_vid_zero counted them at the parser; this counts the ones
        // this port's policy let through.
        if (arrived_tagged && (carried_vid == 12'd0))
          if (!(&c_vid_zero_admitted))
            c_vid_zero_admitted <= c_vid_zero_admitted + 1'b1;
      end else begin
        if (reject == VR_WRONG_TYPE)
          if (!(&c_refused_type)) c_refused_type <= c_refused_type + 1'b1;
        if (reject == VR_RESERVED_VID)
          if (!(&c_reserved_refused))
            c_reserved_refused <= c_reserved_refused + 1'b1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// ingress_vid_assigner -- the one place a frame acquires an attribute it
// did not arrive with.
//
// After this module the frame's VLAN is fixed for the remainder of its
// path through the switch. Chapter 13.1's P6 asserted the VID does not
// change while crossing a switch; this module is where the value that
// property protects is established.
// -----------------------------------------------------------------------
module ingress_vid_assigner
  import vlanport_pkg::*;
#(
  parameter int CNT_W = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             admit,
  input  logic             arrived_tagged,
  input  logic [VID_W-1:0] carried_vid,
  input  logic [PCP_W-1:0] carried_pcp,
  input  logic [VID_W-1:0] port_pvid,
  input  logic [PCP_W-1:0] port_default_pcp,

  output logic             assign_valid,
  output logic [VID_W-1:0] assigned_vid,
  output logic [PCP_W-1:0] assigned_pcp,
  output logic             vid_was_carried,   // provenance -- Section 16
  output logic             vid_was_invented,

  output logic [CNT_W-1:0] c_carried,
  output logic [CNT_W-1:0] c_invented,
  output logic [CNT_W-1:0] c_priority_only
);

  // "Usable" is Chapter 13.2 Section 4's test: tagged, and not 0 or 4095.
  // A VID-0 frame is tagged and NOT usable, so it falls to the PVID --
  // which is the same outcome as an untagged frame by a different route.
  logic vid_usable;
  assign vid_usable = arrived_tagged &&
                      (carried_vid != 12'd0) && (carried_vid != 12'd4095);

  assign assign_valid = admit;
  assign assigned_vid = vid_usable ? carried_vid : port_pvid;

  // THE ASYMMETRY. The VID falls back to the port; the PCP does not. A
  // tagged frame's priority is honoured even when its VLAN is discarded,
  // because Chapter 13.2 Section 15 established the two fields are
  // independent and have unrelated consumers.
  assign assigned_pcp = arrived_tagged ? carried_pcp : port_default_pcp;

  // PROVENANCE. Section 16 needs to know whether this VLAN came off the
  // wire or out of a register, because a mismatch is only possible in the
  // second case.
  assign vid_was_carried  = admit && vid_usable;
  assign vid_was_invented = admit && !vid_usable;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_carried       <= '0;
      c_invented      <= '0;
      c_priority_only <= '0;
    end else if (admit) begin
      if (vid_usable) begin
        if (!(&c_carried)) c_carried <= c_carried + 1'b1;
      end else begin
        if (!(&c_invented)) c_invented <= c_invented + 1'b1;
        if (arrived_tagged)
          if (!(&c_priority_only)) c_priority_only <= c_priority_only + 1'b1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// ingress_vlan_filter -- is this port a member of the VLAN the frame was
// just assigned?
//
// Chapter 13.1 Section 12's isolation invariant is about the EGRESS. This
// is the other half of the boundary, and a switch can satisfy that
// invariant perfectly while letting any station into any VLAN.
// -----------------------------------------------------------------------
module ingress_vlan_filter
  import vlanport_pkg::*;
#(
  parameter int N_PORTS = 24,
  parameter int N_VLANS = 64,
  parameter int VIDX_W  = 6,
  parameter int CNT_W   = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 assign_valid,
  input  logic [VIDX_W-1:0]    assigned_vidx,
  input  logic [4:0]           ingress_port,
  input  logic                 vid_was_carried,
  input  logic [N_PORTS-1:0]   vlan_members [N_VLANS],
  input  logic                 filter_enable,

  output logic                 pass,
  output vlan_reject_e         reject,

  output logic [CNT_W-1:0]     c_filtered,
  output logic [CNT_W-1:0]     c_would_have_filtered,   // with the check OFF
  output logic [4:0]           worst_port,
  output logic                 admission_gap_open
);

  logic is_member;
  assign is_member = vlan_members[assigned_vidx][ingress_port];

  always_comb begin
    pass   = 1'b0;
    reject = VR_OK;
    if (assign_valid) begin
      if (filter_enable && !is_member) reject = VR_INGRESS_FILTER;
      else                             pass   = 1'b1;
    end
  end

  logic [CNT_W-1:0] by_port [N_PORTS];

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_filtered            <= '0;
      c_would_have_filtered <= '0;
      for (int p = 0; p < N_PORTS; p++) by_port[p] <= '0;
      worst_port            <= '0;
      admission_gap_open    <= 1'b0;
    end else if (assign_valid && !is_member) begin
      if (filter_enable) begin
        if (!(&c_filtered)) c_filtered <= c_filtered + 1'b1;
      end else begin
        // THE COUNTER THAT MATTERS. With the check disabled, this counts
        // frames that WOULD have been filtered -- frames admitted into a
        // VLAN through a port that is not a member of it. It costs one
        // comparator and it is the only evidence the gap is being used.
        if (!(&c_would_have_filtered))
          c_would_have_filtered <= c_would_have_filtered + 1'b1;
        by_port[ingress_port] <= by_port[ingress_port] + 1'b1;
        worst_port            <= ingress_port;
        // A frame ENTERED a VLAN it had no business entering, and
        // Chapter 13.1's isolation monitor will not see it, because every
        // port it reaches IS a member.
        admission_gap_open    <= vid_was_carried;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// egress_tag_transformer -- strip, insert, pass or drop.
//
// The action is chosen by a per-port per-VLAN bit and NOT by anything
// about the frame. Recognising the no-op case matters: Section 13 shows
// every real transformation costs an FCS recomputation, so a design that
// always strips-then-inserts pays that cost on every frame for nothing.
// -----------------------------------------------------------------------
module egress_tag_transformer
  import vlanport_pkg::*;
#(
  parameter int N_PORTS = 24,
  parameter int N_VLANS = 64,
  parameter int VIDX_W  = 6,
  parameter int CNT_W   = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 eg_valid,
  input  logic [4:0]           egress_port,
  input  logic [VIDX_W-1:0]    vidx,
  input  logic [VID_W-1:0]     vid,
  input  logic [PCP_W-1:0]     pcp,
  input  logic                 frame_is_tagged,     // as it sits in the fabric
  input  logic [13:0]          frame_len,
  input  logic [N_PORTS-1:0]   vlan_members [N_VLANS],
  input  logic                 vlan_untagged_here,

  output logic                 act_valid,
  output egress_action_e       action,
  output logic [13:0]          new_len,
  output logic [15:0]          insert_tci,
  output logic                 fcs_recompute,
  output vlan_reject_e         reject,

  output logic [CNT_W-1:0]     c_strip,
  output logic [CNT_W-1:0]     c_insert,
  output logic [CNT_W-1:0]     c_pass,
  output logic [CNT_W-1:0]     c_drop_nonmember
);

  logic is_member;
  assign is_member = vlan_members[vidx][egress_port];

  always_comb begin
    action        = EG_DROP;
    new_len       = frame_len;
    fcs_recompute = 1'b0;
    reject        = VR_OK;
    act_valid     = 1'b0;

    if (eg_valid) begin
      act_valid = 1'b1;

      // Chapter 13.1 Section 12's isolation invariant, applied here. A
      // non-member port never emits the frame, whatever its untagged set
      // happens to say about a VLAN it does not carry.
      if (!is_member) begin
        action = EG_DROP;
        reject = VR_EGRESS_NOT_MEM;

      end else if (vlan_untagged_here) begin
        if (frame_is_tagged) begin
          action        = EG_STRIP;
          new_len       = frame_len - 14'd4;
          fcs_recompute = 1'b1;
        end else begin
          // THE NO-OP. Already in the right form. Section 13 explains
          // why recognising this is worth the comparator.
          action = EG_PASS;
        end

      end else begin
        if (!frame_is_tagged) begin
          action        = EG_TAG;
          new_len       = frame_len + 14'd4;
          fcs_recompute = 1'b1;
        end else begin
          action = EG_PASS;
        end
      end
    end
  end

  // The tag this port would insert. Chapter 13.2 Section 4's TCI split,
  // rebuilt from the frame's assigned VLAN and priority -- note that the
  // DEI bit is not preserved across a strip-and-reinsert, which is a
  // small honest loss worth knowing about.
  assign insert_tci = {pcp, 1'b0, vid};

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_strip <= '0; c_insert <= '0; c_pass <= '0; c_drop_nonmember <= '0;
    end else if (eg_valid) begin
      unique case (action)
        EG_STRIP: if (!(&c_strip))  c_strip  <= c_strip + 1'b1;
        EG_TAG:   if (!(&c_insert)) c_insert <= c_insert + 1'b1;
        EG_PASS:  if (!(&c_pass))   c_pass   <= c_pass + 1'b1;
        EG_DROP:  if (!(&c_drop_nonmember))
                    c_drop_nonmember <= c_drop_nonmember + 1'b1;
        default: ;
      endcase
    end
  end

endmodule

// -----------------------------------------------------------------------
// egress_length_repair -- makes the transformed frame legal again.
//
// A strip can produce a runt; an insert can produce an oversize. Both are
// the switch's own doing, and both must be detected against the limits
// that apply AFTER the transformation rather than before it.
// -----------------------------------------------------------------------
module egress_length_repair
  import vlanport_pkg::*;
#(
  parameter int MIN_FRAME = 64,
  parameter int MAX_UNTAG = 1518,
  parameter int CNT_W     = 32
)(
  input  logic             clk,
  input  logic             rst_n,

  input  logic             act_valid,
  input  egress_action_e   action,
  input  logic [13:0]      new_len,
  input  logic [2:0]       tags_after,      // tag count AFTER the action

  output logic [13:0]      final_len,
  output logic [13:0]      pad_octets,
  output logic             need_pad,
  output logic             fcs_recompute,
  output logic             length_ok,
  output vlan_reject_e     reject,

  output logic [CNT_W-1:0] c_repadded,
  output logic [CNT_W-1:0] c_oversize_self_inflicted,
  output logic [13:0]      max_after
);

  // THE LIMIT THAT APPLIES IS THE ONE FOR THE TAG COUNT AFTER THE
  // TRANSFORMATION. Chapter 13.2 Section 6: 1518 untagged, 1522 with one
  // tag, 1526 with two. A design that checks the pre-transformation limit
  // rejects its own output.
  assign max_after = 14'(MAX_UNTAG) + (14'(tags_after) * 14'd4);

  // A strip can take a 64-octet frame to 60. Chapter 7.3 requires 64, so
  // the four octets come back as padding -- and Chapter 5.6 established
  // that padding beyond the payload's own declared length is invisible to
  // the layer above.
  assign need_pad   = act_valid && (new_len < 14'(MIN_FRAME));
  assign pad_octets = need_pad ? (14'(MIN_FRAME) - new_len) : 14'd0;
  assign final_len  = need_pad ? 14'(MIN_FRAME) : new_len;

  // Every transformation changes the frame, so the check sequence over it
  // is no longer valid. Chapter 5.8's CRC-32 is already in the datapath.
  assign fcs_recompute = act_valid &&
                         ((action == EG_STRIP) || (action == EG_TAG) || need_pad);

  always_comb begin
    length_ok = 1'b1;
    reject    = VR_OK;
    if (act_valid && (final_len > max_after)) begin
      length_ok = 1'b0;
      reject    = VR_LENGTH;
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_repadded                <= '0;
      c_oversize_self_inflicted <= '0;
    end else if (act_valid) begin
      if (need_pad)
        if (!(&c_repadded)) c_repadded <= c_repadded + 1'b1;
      // An oversize the switch CREATED by inserting a tag. Distinct from
      // an oversize that arrived, because the remedy is different: this
      // one means the far end's limit and ours disagree about tagging.
      if (!length_ok && (action == EG_TAG))
        if (!(&c_oversize_self_inflicted))
          c_oversize_self_inflicted <= c_oversize_self_inflicted + 1'b1;
    end
  end

endmodule

// -----------------------------------------------------------------------
// native_vlan_detector -- infers a native-VLAN mismatch from evidence
// available at one end.
//
// The far end's PVID is not observable. What IS observable: which
// addresses appear in which VLAN, and whether an address seen tagged in
// VLAN X on this trunk is also seen untagged. A mismatch makes those two
// populations disagree in a way a match never does.
// -----------------------------------------------------------------------
module native_vlan_detector
  import vlanport_pkg::*;
#(
  parameter int N_TRACK = 16,
  parameter int ADDR_W  = 48,
  parameter int VIDX_W  = 6,
  parameter int CNT_W   = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic                 learn_valid,
  input  logic [ADDR_W-1:0]    learn_mac,
  input  logic [VIDX_W-1:0]    learn_vidx,
  input  logic [4:0]           learn_port,
  input  logic                 arrived_tagged,
  input  logic                 port_is_trunk,
  input  logic [VIDX_W-1:0]    port_native_vidx,

  output logic [CNT_W-1:0]     c_untagged_on_trunk,
  output logic [CNT_W-1:0]     c_addr_in_two_vlans_one_trunk,
  output logic [ADDR_W-1:0]    suspect_mac,
  output logic [VIDX_W-1:0]    suspect_vidx_a,
  output logic [VIDX_W-1:0]    suspect_vidx_b,
  output logic                 native_mismatch_suspected,
  output logic [4:0]           suspect_port
);

  logic [ADDR_W-1:0] t_mac  [N_TRACK];
  logic [VIDX_W-1:0] t_vidx [N_TRACK];
  logic              t_tag  [N_TRACK];
  logic              t_val  [N_TRACK];
  logic [$clog2(N_TRACK)-1:0] wr_ptr;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < N_TRACK; i++) begin
        t_mac[i] <= '0; t_vidx[i] <= '0; t_tag[i] <= 1'b0; t_val[i] <= 1'b0;
      end
      wr_ptr                        <= '0;
      c_untagged_on_trunk           <= '0;
      c_addr_in_two_vlans_one_trunk <= '0;
      suspect_mac                   <= '0;
      suspect_vidx_a                <= '0;
      suspect_vidx_b                <= '0;
      suspect_port                  <= '0;
      native_mismatch_suspected     <= 1'b0;
    end else if (learn_valid && port_is_trunk) begin
      // Untagged arrivals on a trunk are the native VLAN's traffic. They
      // are NORMAL -- this counter is a denominator, not an alarm.
      if (!arrived_tagged)
        if (!(&c_untagged_on_trunk))
          c_untagged_on_trunk <= c_untagged_on_trunk + 1'b1;

      begin
        automatic int hit = -1;
        for (int i = 0; i < N_TRACK; i++)
          if (t_val[i] && (t_mac[i] == learn_mac)) hit = i;

        if (hit >= 0) begin
          // THE SIGNATURE. One address, seen on ONE trunk port, in TWO
          // different VLANs, where at least one sighting was untagged.
          // With matching natives this cannot happen: the untagged
          // traffic is always the same VLAN at both ends. With a
          // mismatch, the far end's native traffic arrives untagged and
          // lands in OUR native VLAN, while that same station's tagged
          // traffic lands in its real one.
          if ((t_vidx[hit] != learn_vidx) &&
              (!t_tag[hit] || !arrived_tagged)) begin
            if (!(&c_addr_in_two_vlans_one_trunk))
              c_addr_in_two_vlans_one_trunk <= c_addr_in_two_vlans_one_trunk + 1'b1;
            suspect_mac    <= learn_mac;
            suspect_vidx_a <= t_vidx[hit];
            suspect_vidx_b <= learn_vidx;
            suspect_port   <= learn_port;
            // Chapter 13.1 Section 14 established that one address in two
            // VLANs is NORMAL -- a router with several legs. What is not
            // normal is that pattern arriving through ONE trunk port with
            // an untagged sighting among them.
            native_mismatch_suspected <=
              (learn_vidx == port_native_vidx) ||
              (t_vidx[hit] == port_native_vidx);
          end
          t_vidx[hit] <= learn_vidx;
          t_tag[hit]  <= arrived_tagged;
        end else begin
          t_mac[wr_ptr]  <= learn_mac;
          t_vidx[wr_ptr] <= learn_vidx;
          t_tag[wr_ptr]  <= arrived_tagged;
          t_val[wr_ptr]  <= 1'b1;
          wr_ptr         <= wr_ptr + 1'b1;
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// portmode_conformance_monitor -- checks a datapath whose job is to
// modify frames.
//
// Chapter 12.1's P11 asserted a frame is never modified in transit. This
// chapter strips, inserts, re-pads and recomputes the FCS. So the
// invariant is restated: the addresses, the EtherType, the payload up to
// its declared length, and the VLAN ASSIGNMENT are unmodified, and
// everything else is the switch's to change.
// -----------------------------------------------------------------------
module portmode_conformance_monitor
  import vlanport_pkg::*;
#(
  parameter int N_PORTS = 24,
  parameter int N_VLANS = 64,
  parameter int VIDX_W  = 6,
  parameter int ADDR_W  = 48,
  parameter int CNT_W   = 32
)(
  input  logic                 clk,
  input  logic                 rst_n,

  input  logic [N_PORTS-1:0]   vlan_members [N_VLANS],

  input  logic                 tx_valid,
  input  logic [4:0]           egress_port,
  input  logic [VIDX_W-1:0]    frame_vidx,
  input  logic [VIDX_W-1:0]    ingress_vidx,
  input  logic                 vlan_untagged_here,
  input  logic                 emitted_tagged,
  input  logic [VID_W-1:0]     emitted_vid,
  input  logic [VID_W-1:0]     assigned_vid,
  input  logic [13:0]          emitted_len,
  input  logic [2:0]           emitted_tags,
  input  logic [ADDR_W-1:0]    in_da,  input logic [ADDR_W-1:0] out_da,
  input  logic [ADDR_W-1:0]    in_sa,  input logic [ADDR_W-1:0] out_sa,
  input  logic                 fcs_recomputed,

  output logic [CNT_W-1:0]     v_form_wrong,       // tagged where untagged
  output logic [CNT_W-1:0]     v_vid_rewritten,    // relabelled at egress
  output logic [CNT_W-1:0]     v_addr_modified,
  output logic [CNT_W-1:0]     v_illegal_length,
  output logic [CNT_W-1:0]     v_stale_fcs,        // changed without recompute
  output logic [CNT_W-1:0]     v_nonmember_emit,
  output logic                 conformant
);

  logic [13:0] max_after;
  assign max_after = 14'd1518 + (14'(emitted_tags) * 14'd4);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_form_wrong     <= '0;
      v_vid_rewritten  <= '0;
      v_addr_modified  <= '0;
      v_illegal_length <= '0;
      v_stale_fcs      <= '0;
      v_nonmember_emit <= '0;
    end else if (tx_valid) begin
      // THE FORM CHECK. The emitted frame's tagged-ness must match this
      // port's untagged set for this VLAN. A tagged frame on an untagged
      // port reaches a station that cannot parse it; an untagged frame on
      // a trunk lands in the far end's native VLAN.
      if (emitted_tagged == vlan_untagged_here)
        if (!(&v_form_wrong)) v_form_wrong <= v_form_wrong + 1'b1;

      // Chapter 13.1's P6, at the point the tag is built. Egress may
      // change the frame's FORM and never its VLAN.
      if (emitted_tagged && (emitted_vid != assigned_vid))
        if (!(&v_vid_rewritten)) v_vid_rewritten <= v_vid_rewritten + 1'b1;
      if (frame_vidx != ingress_vidx)
        if (!(&v_vid_rewritten)) v_vid_rewritten <= v_vid_rewritten + 1'b1;

      // THE RESTATED P11. Addresses survive every transformation.
      if ((out_da != in_da) || (out_sa != in_sa))
        if (!(&v_addr_modified)) v_addr_modified <= v_addr_modified + 1'b1;

      // The limit for the tag count AFTER the transformation -- Section 13.
      if ((emitted_len < 14'd64) || (emitted_len > max_after))
        if (!(&v_illegal_length)) v_illegal_length <= v_illegal_length + 1'b1;

      // A frame whose length changed and whose FCS was not recomputed is
      // a frame carrying a check sequence over bytes it no longer has.
      if ((emitted_tagged != (emitted_tags != 3'd0)) && !fcs_recomputed)
        if (!(&v_stale_fcs)) v_stale_fcs <= v_stale_fcs + 1'b1;

      // Chapter 13.1 Section 12's invariant, unchanged.
      if (!vlan_members[frame_vidx][egress_port])
        if (!(&v_nonmember_emit)) v_nonmember_emit <= v_nonmember_emit + 1'b1;
    end
  end

  assign conformant = (v_form_wrong     == '0) && (v_vid_rewritten  == '0) &&
                      (v_addr_modified  == '0) && (v_illegal_length == '0) &&
                      (v_stale_fcs      == '0) && (v_nonmember_emit == '0);

endmodule

// P1. The acceptable-frame-types test is on the frame's FORM. A VID-0
// frame is TAGGED and is refused by an untagged-only port, even though
// Section 7 will assign it the PVID as though it were untagged.
property p_form_test_uses_form;
  @(posedge clk) disable iff (!rst_n)
  (frame_valid && (accept == AFT_UNTAGGED_ONLY) && arrived_tagged) |-> !admit;
endproperty
a_form_test: assert property (p_form_test_uses_form);

// P2. A tagged-only port refuses untagged frames.
property p_tagged_only_refuses_untagged;
  @(posedge clk) disable iff (!rst_n)
  (frame_valid && (accept == AFT_TAGGED_ONLY) && !arrived_tagged)
    |-> (!admit && (reject == VR_WRONG_TYPE));
endproperty
a_tagged_only: assert property (p_tagged_only_refuses_untagged);

// P3. VID 4095 is refused outright -- unlike 0, it has no defined
// alternative meaning and no assignment rule could rescue it.
property p_vid_4095_refused;
  @(posedge clk) disable iff (!rst_n)
  (frame_valid && arrived_tagged && (carried_vid == 12'd4095))
    |-> (!admit && (reject == VR_RESERVED_VID));
endproperty
a_4095_refused: assert property (p_vid_4095_refused);

// P4. THE ASSIGNMENT RULE. A usable carried VID is the frame's VLAN;
// anything else falls back to the port's PVID.
property p_assignment_rule;
  @(posedge clk) disable iff (!rst_n)
  assign_valid |-> (assigned_vid ==
                    ((arrived_tagged && (carried_vid != 12'd0) &&
                      (carried_vid != 12'd4095)) ? carried_vid : port_pvid));
endproperty
a_assignment: assert property (p_assignment_rule);

// P5. THE ASYMMETRY. The VID falls back to the port; the PCP does not.
// A VID-0 frame's priority is honoured even though its VLAN is
// discarded, because the sender expressed one and not the other.
property p_pcp_survives_vid_fallback;
  @(posedge clk) disable iff (!rst_n)
  (assign_valid && arrived_tagged) |-> (assigned_pcp == carried_pcp);
endproperty
a_pcp_honoured: assert property (p_pcp_survives_vid_fallback);

// P6. An untagged frame takes the port's default priority, because it
// expressed none.
property p_untagged_takes_default_pcp;
  @(posedge clk) disable iff (!rst_n)
  (assign_valid && !arrived_tagged) |-> (assigned_pcp == port_default_pcp);
endproperty
a_default_pcp: assert property (p_untagged_takes_default_pcp);

// P7. PROVENANCE. Every assignment is recorded as carried or invented,
// because only an invented VLAN can be mismatched with the far end.
property p_provenance_recorded;
  @(posedge clk) disable iff (!rst_n)
  assign_valid |-> (vid_was_carried ^ vid_was_invented);
endproperty
a_provenance: assert property (p_provenance_recorded);

// P8. With filtering enabled, a frame assigned a VLAN the ingress port is
// not a member of is discarded.
property p_ingress_filter_drops_nonmember;
  @(posedge clk) disable iff (!rst_n)
  (assign_valid && filter_enable && !is_member)
    |-> (!pass && (reject == VR_INGRESS_FILTER));
endproperty
a_ingress_filter: assert property (p_ingress_filter_drops_nonmember);

// P9. With filtering DISABLED the frame passes -- and the comparison is
// still performed, because c_would_have_filtered is the only evidence
// the gap is being used.
property p_gap_is_measured;
  @(posedge clk) disable iff (!rst_n)
  (assign_valid && !filter_enable && !is_member)
    |=> (c_would_have_filtered > $past(c_would_have_filtered));
endproperty
a_gap_measured: assert property (p_gap_is_measured);

// P10. An invented VID never trips the filter -- a sensibly configured
// port is a member of its own PVID, so only a CARRIED VID can violate
// membership.
property p_invented_vid_is_a_member;
  @(posedge clk) disable iff (!rst_n)
  (assign_valid && vid_was_invented) |-> is_member;
endproperty
a_pvid_is_member: assert property (p_invented_vid_is_a_member);

// P11. Chapter 13.1's isolation invariant is about the EGRESS, so a
// missing ingress filter does not violate it. The two are different
// halves of the boundary.
property p_ingress_gap_is_not_isolation;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && !filter_enable) |-> vlan_members[frame_vidx][egress_port];
endproperty
a_egress_still_holds: assert property (p_ingress_gap_is_not_isolation);

// P12. THE ACTION IS CHOSEN BY THE PORT, not by the frame.
property p_action_from_untagged_set;
  @(posedge clk) disable iff (!rst_n)
  (act_valid && is_member)
    |-> (action == (vlan_untagged_here
                     ? (frame_is_tagged ? EG_STRIP : EG_PASS)
                     : (frame_is_tagged ? EG_PASS  : EG_TAG)));
endproperty
a_action_choice: assert property (p_action_from_untagged_set);

// P13. A non-member port drops, whatever its untagged set says about a
// VLAN it does not carry.
property p_nonmember_drops;
  @(posedge clk) disable iff (!rst_n)
  (act_valid && !is_member) |-> (action == EG_DROP);
endproperty
a_nonmember_drop: assert property (p_nonmember_drops);

// P14. THE NO-OP IS RECOGNISED. A frame already in the right form is not
// stripped and reinserted -- Section 13 shows that costs an FCS
// recomputation for nothing.
property p_noop_recognised;
  @(posedge clk) disable iff (!rst_n)
  (act_valid && (action == EG_PASS)) |-> !fcs_recompute;
endproperty
a_noop_free: assert property (p_noop_recognised);

// P15. Every real transformation changes the length by exactly 4.
property p_length_delta_is_four;
  @(posedge clk) disable iff (!rst_n)
  (act_valid && (action inside {EG_STRIP, EG_TAG}))
    |-> ((new_len == frame_len - 14'd4) || (new_len == frame_len + 14'd4));
endproperty
a_delta_four: assert property (p_length_delta_is_four);

// P16. Egress changes the frame's FORM and never its VLAN. Chapter 13.1's
// P6, at the point the tag is built.
property p_egress_never_relabels;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && emitted_tagged) |-> (emitted_vid == assigned_vid);
endproperty
a_no_relabel: assert property (p_egress_never_relabels);

// P17. THE FORM CHECK. The emitted frame's tagged-ness matches this
// port's untagged set for this VLAN.
property p_emitted_form_matches_port;
  @(posedge clk) disable iff (!rst_n)
  tx_valid |-> (emitted_tagged != vlan_untagged_here);
endproperty
a_form_matches: assert property (p_emitted_form_matches_port);

// P18. A strip that produces a runt is RE-PADDED. Chapter 7.3 requires
// 64 octets and a 64-octet tagged frame becomes 60 without one.
property p_runt_is_repadded;
  @(posedge clk) disable iff (!rst_n)
  (act_valid && (new_len < 14'd64)) |-> (need_pad && (final_len == 14'd64));
endproperty
a_repad: assert property (p_runt_is_repadded);

// P19. The limit that applies is the one for the tag count AFTER the
// transformation. A design checking the pre-transformation limit rejects
// its own output.
property p_limit_is_post_transform;
  @(posedge clk) disable iff (!rst_n)
  act_valid |-> (max_after == (14'd1518 + (14'(tags_after) * 14'd4)));
endproperty
a_post_limit: assert property (p_limit_is_post_transform);

// P20. Every length change recomputes the FCS. A frame whose bytes
// changed and whose check sequence did not is discarded by every
// receiver, and the port that changed it reports nothing.
property p_fcs_follows_every_change;
  @(posedge clk) disable iff (!rst_n)
  (act_valid && ((action inside {EG_STRIP, EG_TAG}) || need_pad))
    |-> fcs_recompute;
endproperty
a_fcs_recompute: assert property (p_fcs_follows_every_change);

// P21. A self-inflicted oversize is counted SEPARATELY from one that
// arrived -- the remedies differ.
property p_self_inflicted_counted_apart;
  @(posedge clk) disable iff (!rst_n)
  (act_valid && !length_ok && (action == EG_TAG))
    |=> (c_oversize_self_inflicted > $past(c_oversize_self_inflicted));
endproperty
a_self_oversize: assert property (p_self_inflicted_counted_apart);

// P22. THE RESTATED P11. Chapter 12.1 asserted a frame is never modified;
// this chapter modifies frames by design. What survives every
// transformation is the addresses.
property p_addresses_survive;
  @(posedge clk) disable iff (!rst_n)
  tx_valid |-> ((out_da == in_da) && (out_sa == in_sa));
endproperty
a_addresses_intact: assert property (p_addresses_survive);

// P23. Untagged arrivals on a trunk are NORMAL -- the native VLAN
// working as designed. The counter is a denominator, not an alarm.
property p_untagged_on_trunk_is_not_an_error;
  @(posedge clk) disable iff (!rst_n)
  (learn_valid && port_is_trunk && !arrived_tagged) |-> (reject == VR_OK);
endproperty
a_native_is_normal: assert property (p_untagged_on_trunk_is_not_an_error);

// P24. A mismatch is a SUSPICION, not a verdict -- proving it needs the
// far end's PVID, which is not observable.
property p_mismatch_is_advisory;
  @(posedge clk) disable iff (!rst_n)
  native_mismatch_suspected |-> (suspect_vidx_a != suspect_vidx_b);
endproperty
a_suspicion_named: assert property (p_mismatch_is_advisory);

// P25. The signature requires BOTH qualifiers: one trunk port, and an
// untagged sighting. A router with legs in several VLANs has neither.
property p_signature_needs_both_qualifiers;
  @(posedge clk) disable iff (!rst_n)
  $rose(native_mismatch_suspected) |-> port_is_trunk;
endproperty
a_both_qualifiers: assert property (p_signature_needs_both_qualifiers);

// P26. A stale FCS is caught. The frame's bytes changed and the check
// sequence over them did not.
property p_no_stale_fcs;
  @(posedge clk) disable iff (!rst_n)
  tx_valid |-> (v_stale_fcs == $past(v_stale_fcs));
endproperty
a_no_stale_fcs: assert property (p_no_stale_fcs);

// P27. Chapter 13.1 Section 12's invariant survives every transformation
// in this chapter.
property p_isolation_survives_transformation;
  @(posedge clk) disable iff (!rst_n)
  tx_valid |-> vlan_members[frame_vidx][egress_port];
endproperty
a_isolation_holds: assert property (p_isolation_survives_transformation);

// P28. Conformance means the transformation was the one this port's
// configuration calls for -- never that the frame is in the VLAN anybody
// intended.
property p_conformant_definition;
  @(posedge clk) disable iff (!rst_n)
  conformant |-> ((v_form_wrong == '0) && (v_vid_rewritten == '0) &&
                  (v_addr_modified == '0) && (v_illegal_length == '0) &&
                  (v_stale_fcs == '0) && (v_nonmember_emit == '0));
endproperty
a_conformant_def: assert property (p_conformant_definition);

// P29. "Access port" and "trunk port" are DERIVED from the untagged set,
// not configured as a mode -- a hybrid port must remain expressible.
property p_mode_is_derived;
  @(posedge clk) disable iff (!rst_n)
  ($countones(untagged[rd_port]) == 1) |-> access_like[rd_port];
endproperty
a_mode_derived: assert property (p_mode_is_derived);

// P30. Several untagged VLANs on one port is expressible and is almost
// always wrong -- they all arrive at the far end indistinguishable.
property p_multiple_untagged_flagged;
  @(posedge clk) disable iff (!rst_n)
  ($countones(untagged[rd_port]) > 1) |-> multi_untagged_warning[rd_port];
endproperty
a_multi_untagged: assert property (p_multiple_untagged_flagged);