What a Switch Does

// SYNTHESIZABLE.
//
// Per-port ingress: extract the addresses a switch needs and classify
// the frame, so the forwarding engine has a fixed-size descriptor
// rather than a frame.
//
// WHAT A SWITCH NEEDS FROM A FRAME:
//   the DESTINATION address -- to decide where it goes
//   the SOURCE address      -- to learn where the sender is
//   the INGRESS PORT        -- which is not in the frame at all
//   the destination's TYPE  -- unicast, multicast or broadcast
//
// And nothing else. The payload is never examined; a switch is not
// looking at it and does not need to.
//
// THE INGRESS PORT IS NOT IN THE FRAME. It is a fact about which wire
// the frame arrived on, and every later step needs it: learning writes
// it, the forwarding decision compares against it (Chapter 12.3's
// filter rule), and flooding excludes it. A descriptor that omits it
// cannot be forwarded correctly by anything downstream.
package switching_pkg;
 
  localparam int unsigned MAC_BITS  = 48;
  localparam int unsigned N_PORTS   = 24;
  localparam int unsigned PORT_BITS = 5;
 
  // Frame rate arithmetic, from Section 3.
  //   minimum frame on the wire = 64 + 8 + 12 = 84 octets = 672 bits
  //   at 1 Gb/s that is 1.4881 Mpps and a 672 ns budget per frame
  localparam int unsigned MIN_FRAME_ON_WIRE = 84;
  localparam int unsigned MIN_FRAME_BITS    = MIN_FRAME_ON_WIRE * 8;
 
  typedef enum logic [1:0] {
    DST_UNICAST,
    DST_MULTICAST,
    DST_BROADCAST
  } dst_kind_e;
 
  // The fixed-size descriptor the fabric moves instead of the frame.
  typedef struct packed {
    logic [MAC_BITS-1:0]  dst;
    logic [MAC_BITS-1:0]  src;
    logic [PORT_BITS-1:0] ingress_port;
    dst_kind_e            dst_kind;
    logic                 src_is_group;   // illegal: see below
    logic [13:0]          length;
    logic                 valid;
  } descriptor_t;
 
endpackage
 
module port_ingress_classifier
  import switching_pkg::*;
#(
  parameter int unsigned PORT_ID = 0,
  parameter int unsigned CNT_W   = 24
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic [7:0] octet,
  input  logic       octet_valid,
  input  logic       frame_start,
  input  logic       frame_end,
  input  logic       frame_bad_fcs,
 
  output descriptor_t descriptor,
  output logic        descriptor_valid,
 
  output logic [CNT_W-1:0] c_frames,
  output logic [CNT_W-1:0] c_unicast,
  output logic [CNT_W-1:0] c_multicast,
  output logic [CNT_W-1:0] c_broadcast,
  output logic [CNT_W-1:0] c_bad_fcs,
  // A frame whose SOURCE address has the group bit set. Illegal --
  // no station may own a group address -- and learning from it would
  // put a multicast address in the table, where a later destination
  // lookup would match it and unicast a multicast frame to one port.
  output logic             group_source_seen,
  output logic [CNT_W-1:0] c_group_source
);
 
  logic [5:0]  index_q;
  logic [47:0] dst_q, src_q;
  logic [13:0] len_q;
  logic        in_frame_q;
 
  // Chapter 5.3's I/G bit: the least-significant bit of the FIRST
  // octet transmitted. Set means a group address.
  wire dst_is_group = dst_q[40];
  wire dst_is_bcast = (dst_q == 48'hFFFF_FFFF_FFFF);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      index_q <= 6'd0; dst_q <= '0; src_q <= '0; len_q <= 14'd0;
      in_frame_q <= 1'b0;
      descriptor <= '0; descriptor_valid <= 1'b0;
      c_frames <= '0; c_unicast <= '0; c_multicast <= '0;
      c_broadcast <= '0; c_bad_fcs <= '0;
      group_source_seen <= 1'b0; c_group_source <= '0;
    end else begin
      descriptor_valid  <= 1'b0;
      group_source_seen <= 1'b0;
 
      if (frame_start) begin
        index_q    <= 6'd0;
        in_frame_q <= 1'b1;
        len_q      <= 14'd0;
      end
 
      if (octet_valid && in_frame_q) begin
        // The first twelve octets are the two addresses, destination
        // first. Everything after them is payload the switch does not
        // look at.
        if (index_q < 6'd6)       dst_q <= {dst_q[39:0], octet};
        else if (index_q < 6'd12) src_q <= {src_q[39:0], octet};
 
        if (index_q != 6'd63) index_q <= index_q + 6'd1;
        if (len_q != 14'h3FFF) len_q <= len_q + 14'd1;
      end
 
      if (frame_end && in_frame_q) begin
        in_frame_q <= 1'b0;
        if (!(&c_frames)) c_frames <= c_frames + 1'b1;
 
        if (frame_bad_fcs) begin
          // A frame that failed its check sequence is not forwarded and
          // not learned from. Learning from a corrupt frame writes a
          // corrupt address into the table, and Chapter 12.2 §7 shows
          // what that costs.
          if (!(&c_bad_fcs)) c_bad_fcs <= c_bad_fcs + 1'b1;
 
        end else begin
          descriptor.dst          <= dst_q;
          descriptor.src          <= src_q;
          // THE INGRESS PORT, which is not in the frame at all.
          descriptor.ingress_port <= PORT_BITS'(PORT_ID);
          descriptor.length       <= len_q;
          descriptor.valid        <= 1'b1;
          descriptor_valid        <= 1'b1;
 
          if (dst_is_bcast) begin
            descriptor.dst_kind <= DST_BROADCAST;
            if (!(&c_broadcast)) c_broadcast <= c_broadcast + 1'b1;
          end else if (dst_is_group) begin
            descriptor.dst_kind <= DST_MULTICAST;
            if (!(&c_multicast)) c_multicast <= c_multicast + 1'b1;
          end else begin
            descriptor.dst_kind <= DST_UNICAST;
            if (!(&c_unicast)) c_unicast <= c_unicast + 1'b1;
          end
 
          // A GROUP SOURCE ADDRESS is illegal: no station owns one.
          // Flagged here so Chapter 12.2's learning can refuse it,
          // because a group address in the forwarding table will later
          // MATCH a destination lookup and unicast a multicast frame.
          descriptor.src_is_group <= src_q[40];
          if (src_q[40]) begin
            group_source_seen <= 1'b1;
            if (!(&c_group_source)) c_group_source <= c_group_source + 1'b1;
          end
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Models what a switch port IS, against what a hub port is -- because
// the difference is the whole reason switching replaced sharing, and
// it is one enable bit wide.
//
// Chapter 9.2 §3 established the argument; this module makes it
// concrete enough to count. A repeater port and a switch port run the
// SAME MAC, and the difference is which of its mechanisms are ever
// reached:
//
//   REPEATER port -- every port's traffic reaches every other, so all
//        ports share ONE collision domain and every station must
//        arbitrate for it.
//   SWITCH port   -- a collision domain containing exactly one
//        transmitter, so there is nothing to arbitrate for and
//        Chapter 1.5's full duplex becomes available.
//
// AND THE CAPACITY DIFFERENCE FALLS OUT: a repeater's total is one
// link's worth however many ports it has; a switch's is ports x rate x
// two directions.
module collision_domain_model
  import switching_pkg::*;
#(
  parameter int unsigned PORTS = 24,
  parameter int unsigned LINK_MBPS = 1000,
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic is_switch,                    // 0 = repeater behaviour
  input  logic [PORTS-1:0] port_transmitting,
  input  logic [PORTS-1:0] port_full_duplex,
 
  // Repeater behaviour: any two simultaneous transmitters collide.
  output logic             collision,
  output logic [PORTS-1:0] colliding_ports,
 
  // Switch behaviour: simultaneous transmitters are simply parallel.
  output logic [5:0]       simultaneous_conversations,
 
  // The capacity each arrangement delivers, computed rather than
  // asserted -- Section 2's table, in hardware.
  output logic [17:0]      aggregate_mbps,
  output logic [17:0]      per_station_mbps,
 
  // Mechanisms present in the MAC and never reached on a switch port.
  // Chapter 9.2 §7's dormant_mechanisms, per port.
  output logic [PORTS-1:0] csma_reachable,
  output logic [4:0]       dormant_mechanism_count,
 
  output logic [CNT_W-1:0] c_collisions,
  output logic [CNT_W-1:0] c_parallel_cycles
);
 
  logic [5:0] tx_count_c;
 
  always_comb begin
    tx_count_c = 6'd0;
    for (int p = 0; p < PORTS; p = p + 1)
      if (port_transmitting[p]) tx_count_c = tx_count_c + 6'd1;
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      collision <= 1'b0; colliding_ports <= '0;
      simultaneous_conversations <= 6'd0;
      aggregate_mbps <= 18'd0; per_station_mbps <= 18'd0;
      csma_reachable <= '0; dormant_mechanism_count <= 5'd0;
      c_collisions <= '0; c_parallel_cycles <= '0;
    end else begin
      if (!is_switch) begin
        // REPEATER. Two or more transmitters at once is a collision,
        // and every port is in it -- that is what "one collision
        // domain" means.
        collision       <= (tx_count_c > 6'd1);
        colliding_ports <= (tx_count_c > 6'd1) ? port_transmitting : '0;
        simultaneous_conversations <= (tx_count_c > 6'd1) ? 6'd0 : tx_count_c;
 
        // Capacity is ONE link's worth however many ports there are.
        aggregate_mbps   <= 18'(LINK_MBPS);
        per_station_mbps <= 18'(LINK_MBPS / PORTS);
 
        // Every port's CSMA/CD is live.
        csma_reachable          <= {PORTS{1'b1}};
        dormant_mechanism_count <= 5'd0;
 
        if (tx_count_c > 6'd1)
          if (!(&c_collisions)) c_collisions <= c_collisions + 1'b1;
 
      end else begin
        // SWITCH. Simultaneous transmitters are not a collision; they
        // are the point. Each is in its own domain of one.
        collision       <= 1'b0;
        colliding_ports <= '0;
        simultaneous_conversations <= tx_count_c;
 
        // Capacity is ports x rate x BOTH DIRECTIONS.
        aggregate_mbps   <= 18'(PORTS * LINK_MBPS * 2);
        per_station_mbps <= 18'(LINK_MBPS);
 
        // CSMA/CD is reachable only on a port that is NOT full duplex.
        // Chapter 9.2 §7's conjunction: a switch port PERMITS full
        // duplex; the negotiation DECIDES it.
        csma_reachable <= ~port_full_duplex;
        // Carrier sense, collision detect, jam, backoff and slot time:
        // five mechanisms, present in the netlist and unreachable.
        dormant_mechanism_count <= (&port_full_duplex) ? 5'd5 : 5'd0;
 
        if (tx_count_c > 6'd1)
          if (!(&c_parallel_cycles)) c_parallel_cycles <= c_parallel_cycles + 1'b1;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// The forwarding engine's skeleton: descriptor in, egress port mask
// out. Chapters 12.2 through 12.4 own the three things it consults;
// this module owns the LOOP and the ordering between them.
//
// THE ORDERING IS NOT ARBITRARY:
//   1. LEARN from the source, unconditionally, before deciding.
//   2. LOOK UP the destination.
//   3. Apply the INGRESS FILTER -- never send a frame back out the
//      port it arrived on (Chapter 12.3).
//   4. Forward, flood or discard.
//
// STEP 1 BEFORE STEP 2 MATTERS, and it is easy to get wrong. A frame
// from a station that has just moved ports must UPDATE the table
// before any lookup of that station's address in the same frame -- a
// station sending to itself, or two frames back to back in opposite
// directions -- otherwise the switch forwards using an entry it is
// about to correct.
module forwarding_engine
  import switching_pkg::*;
#(
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
 
  input  descriptor_t descriptor,
  input  logic        descriptor_valid,
 
  // Learning (Chapter 12.2 owns the table).
  output logic                 learn_request,
  output logic [MAC_BITS-1:0]  learn_address,
  output logic [PORT_BITS-1:0] learn_port,
 
  // Lookup (Chapter 12.3 owns the decision).
  output logic                 lookup_request,
  output logic [MAC_BITS-1:0]  lookup_address,
  input  logic                 lookup_hit,
  input  logic [PORT_BITS-1:0] lookup_port,
  input  logic                 lookup_valid,
 
  // The result: a bitmask of egress ports, because flooding is many.
  output logic [N_PORTS-1:0]   egress_mask,
  output logic                 forward_valid,
  output logic [1:0]           forward_action,   // 0 fwd, 1 flood, 2 drop
 
  output logic [CNT_W-1:0] c_forwarded,
  output logic [CNT_W-1:0] c_flooded,
  output logic [CNT_W-1:0] c_filtered,
  output logic [CNT_W-1:0] c_learn_refused
);
 
  typedef enum logic [1:0] { F_IDLE, F_LEARN, F_LOOKUP, F_DECIDE } fstate_e;
 
  fstate_e     st_q;
  descriptor_t desc_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q <= F_IDLE; desc_q <= '0;
      learn_request <= 1'b0; learn_address <= '0; learn_port <= '0;
      lookup_request <= 1'b0; lookup_address <= '0;
      egress_mask <= '0; forward_valid <= 1'b0; forward_action <= 2'd0;
      c_forwarded <= '0; c_flooded <= '0; c_filtered <= '0;
      c_learn_refused <= '0;
    end else begin
      learn_request  <= 1'b0;
      lookup_request <= 1'b0;
      forward_valid  <= 1'b0;
 
      unique case (st_q)
        F_IDLE: if (descriptor_valid) begin
          desc_q <= descriptor;
          st_q   <= F_LEARN;
        end
 
        F_LEARN: begin
          // LEARN FIRST. A station that moved ports must update the
          // table before any lookup of its address, or a frame in the
          // opposite direction is forwarded to where it used to be.
          //
          // AND REFUSE A GROUP SOURCE. Chapter 5.3's I/G bit set in a
          // source address is illegal; learning it puts a multicast
          // address in the table, where a later destination lookup
          // will MATCH and unicast a multicast frame to one port.
          if (!desc_q.src_is_group) begin
            learn_request <= 1'b1;
            learn_address <= desc_q.src;
            learn_port    <= desc_q.ingress_port;
          end else begin
            if (!(&c_learn_refused)) c_learn_refused <= c_learn_refused + 1'b1;
          end
          st_q <= F_LOOKUP;
        end
 
        F_LOOKUP: begin
          // Broadcast and multicast are not looked up at all: their
          // answer is known without consulting the table.
          if (desc_q.dst_kind == DST_UNICAST) begin
            lookup_request <= 1'b1;
            lookup_address <= desc_q.dst;
          end
          st_q <= F_DECIDE;
        end
 
        F_DECIDE: begin
          if (desc_q.dst_kind != DST_UNICAST) begin
            // Flood, minus the ingress port.
            egress_mask    <= ~(N_PORTS'(1) << desc_q.ingress_port);
            forward_action <= 2'd1;
            forward_valid  <= 1'b1;
            if (!(&c_flooded)) c_flooded <= c_flooded + 1'b1;
            st_q <= F_IDLE;
 
          end else if (lookup_valid) begin
            if (lookup_hit) begin
              if (lookup_port == desc_q.ingress_port) begin
                // THE FILTER RULE. The destination is on the port the
                // frame came from, so the two stations already heard
                // each other directly and forwarding would duplicate
                // the frame back onto its own segment.
                egress_mask    <= '0;
                forward_action <= 2'd2;
                if (!(&c_filtered)) c_filtered <= c_filtered + 1'b1;
              end else begin
                egress_mask    <= (N_PORTS'(1) << lookup_port);
                forward_action <= 2'd0;
                if (!(&c_forwarded)) c_forwarded <= c_forwarded + 1'b1;
              end
            end else begin
              // A MISS floods. Not a failure -- the switch has not yet
              // heard from that station, and flooding is how it finds
              // out. Chapter 12.4 owns the consequences.
              egress_mask    <= ~(N_PORTS'(1) << desc_q.ingress_port);
              forward_action <= 2'd1;
              if (!(&c_flooded)) c_flooded <= c_flooded + 1'b1;
            end
            forward_valid <= 1'b1;
            st_q <= F_IDLE;
          end
        end
 
        default: st_q <= F_IDLE;
      endcase
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Arbitrates among ingress ports competing for one egress port, and --
// more importantly -- accounts for what it does when it cannot serve
// them all.
//
// WHAT REPLACED WHAT:
//   shared medium -- two transmitters at once COLLIDE. Both frames are
//        destroyed, both stations back off, and the medium is idle for
//        the duration. The loss is symmetric and the bandwidth is
//        wasted.
//   switch        -- several ingress ports want one egress port. One is
//        served, the rest QUEUE. Nothing is destroyed and no bandwidth
//        is wasted; the frame is late rather than lost.
//
// UNTIL THE QUEUE FILLS. Then something is discarded -- and that is
// the switch's equivalent of a collision, not a defect in it.
//
// SO THIS MODULE COUNTS AND ATTRIBUTES rather than preventing. Which
// port's frames were dropped, under what discipline, and how full the
// queue was when it happened.
module fabric_arbiter
  import switching_pkg::*;
#(
  parameter int unsigned QUEUE_DEPTH = 64,
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  // One request bit per ingress port wanting this egress port.
  input  logic [N_PORTS-1:0] request,
  input  logic               egress_ready,
 
  output logic [PORT_BITS-1:0] granted_port,
  output logic                 grant_valid,
 
  // Queue state.
  input  logic [7:0] queue_occupancy,
  output logic       queue_full,
  output logic       drop_now,
  output logic [PORT_BITS-1:0] dropped_from_port,
 
  // Accounting: which ingress port's frames were discarded, so a drop
  // is attributable rather than merely counted.
  output logic [CNT_W-1:0] c_grants,
  output logic [CNT_W-1:0] c_drops,
  output logic [CNT_W-1:0] drops_by_ingress [N_PORTS],
  output logic [7:0]       peak_occupancy,
 
  // Fairness, measured. A round-robin that is not actually fair
  // starves a port, and nothing else reports it.
  output logic [CNT_W-1:0] grants_by_ingress [N_PORTS],
  output logic [PORT_BITS-1:0] most_granted_port,
  output logic [PORT_BITS-1:0] least_granted_port,
  output logic                 starvation_suspected
);
 
  logic [PORT_BITS-1:0] rr_q;          // round-robin pointer
  logic [PORT_BITS-1:0] winner_c;
  logic                 any_c;
  integer i;
 
  // Round robin starting from the port after the last grant, so a
  // permanently-requesting port cannot monopolise the egress.
  always_comb begin
    winner_c = rr_q;
    any_c    = 1'b0;
    for (int k = 0; k < N_PORTS; k = k + 1) begin
      automatic int idx = (int'(rr_q) + k) % N_PORTS;
      if (!any_c && request[idx]) begin
        winner_c = PORT_BITS'(idx);
        any_c    = 1'b1;
      end
    end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      rr_q <= '0; granted_port <= '0; grant_valid <= 1'b0;
      queue_full <= 1'b0; drop_now <= 1'b0; dropped_from_port <= '0;
      c_grants <= '0; c_drops <= '0; peak_occupancy <= 8'd0;
      most_granted_port <= '0; least_granted_port <= '0;
      starvation_suspected <= 1'b0;
      for (i = 0; i < N_PORTS; i = i + 1) begin
        drops_by_ingress[i]  <= '0;
        grants_by_ingress[i] <= '0;
      end
    end else if (clear) begin
      c_grants <= '0; c_drops <= '0; peak_occupancy <= 8'd0;
      for (i = 0; i < N_PORTS; i = i + 1) begin
        drops_by_ingress[i]  <= '0;
        grants_by_ingress[i] <= '0;
      end
    end else begin
      grant_valid <= 1'b0;
      drop_now    <= 1'b0;
 
      queue_full <= (queue_occupancy >= 8'(QUEUE_DEPTH));
      if (queue_occupancy > peak_occupancy) peak_occupancy <= queue_occupancy;
 
      if (any_c) begin
        if (queue_occupancy >= 8'(QUEUE_DEPTH)) begin
          // THE DISCARD. Not an error path -- the specified response to
          // more offered load than the egress port can carry, which is
          // arithmetic. What matters is that it is ATTRIBUTED.
          drop_now          <= 1'b1;
          dropped_from_port <= winner_c;
          if (!(&c_drops)) c_drops <= c_drops + 1'b1;
          if (!(&drops_by_ingress[winner_c]))
            drops_by_ingress[winner_c] <= drops_by_ingress[winner_c] + 1'b1;
          rr_q <= (winner_c == PORT_BITS'(N_PORTS-1)) ? '0 : winner_c + 1'b1;
 
        end else if (egress_ready) begin
          granted_port <= winner_c;
          grant_valid  <= 1'b1;
          if (!(&c_grants)) c_grants <= c_grants + 1'b1;
          if (!(&grants_by_ingress[winner_c]))
            grants_by_ingress[winner_c] <= grants_by_ingress[winner_c] + 1'b1;
          // ADVANCE PAST the winner, so the next arbitration starts
          // elsewhere and a permanently-requesting port cannot hold
          // the egress indefinitely.
          rr_q <= (winner_c == PORT_BITS'(N_PORTS-1)) ? '0 : winner_c + 1'b1;
        end
      end
    end
  end
 
  // FAIRNESS, MEASURED. A round-robin that is not actually round is a
  // starved port, and nothing at the frame layer reports it.
  always_comb begin
    logic [CNT_W-1:0] hi, lo;
    hi = '0; lo = '1;
    most_granted_port  = '0;
    least_granted_port = '0;
    for (int p = 0; p < N_PORTS; p = p + 1) begin
      if (grants_by_ingress[p] > hi) begin
        hi = grants_by_ingress[p]; most_granted_port = PORT_BITS'(p);
      end
      if (grants_by_ingress[p] < lo) begin
        lo = grants_by_ingress[p]; least_granted_port = PORT_BITS'(p);
      end
    end
    // A four-to-one spread between the most and least served port is
    // not round-robin behaving; it is a pointer that is not advancing.
    starvation_suspected = (hi > (lo << 2)) && (hi > CNT_W'(1000));
  end
 
endmodule

// SYNTHESIZABLE.
//
// Measures what a switch is actually delivering, in the two units that
// characterise it -- and they rank switches differently.
//
// BITS PER SECOND is what a datasheet quotes and what an operator
// thinks about. FRAMES PER SECOND is what the forwarding engine is
// sized by, because Section 3 established that a 64-octet frame and a
// 1518-octet frame cost the SAME ONE LOOKUP and differ by eighteen
// times in the time available to make it.
//
// So a switch rated at 48 Gb/s that can make only 20 Mpps of decisions
// is a 48 Gb/s switch for large frames and a 13.4 Gb/s switch for
// small ones -- and its datasheet says 48.
//
//   20 Mpps x 672 bits = 13.44 Gb/s of minimum-length frames
//   20 Mpps x 12304 bits = 246 Gb/s of maximum-length frames
//
// The second number exceeds the ports' capacity, which is why large
// frames never expose the limit.
module port_bandwidth_accountant
  import switching_pkg::*;
#(
  parameter int unsigned CLK_MHZ = 500,
  parameter int unsigned WINDOW_MS = 100,
  parameter int unsigned CNT_W = 32
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic        frame_forwarded,
  input  logic [13:0] frame_length,
  input  logic        frame_dropped,
  input  logic [PORT_BITS-1:0] port,
 
  output logic [CNT_W-1:0] frames_in_window,
  output logic [CNT_W-1:0] octets_in_window,
  output logic [CNT_W-1:0] drops_in_window,
 
  // The two characterisations, both computed.
  output logic [17:0] mbps_delivered,
  output logic [17:0] kfps_delivered,
  output logic [13:0] mean_frame_octets,
 
  // Which limit is being approached. A switch near its FRAME rate and
  // one near its BIT rate need completely different remedies, and the
  // two are indistinguishable from throughput alone.
  output logic        near_frame_rate_limit,
  output logic        near_bit_rate_limit,
  output logic [1:0]  binding_limit,       // 0 none, 1 frames, 2 bits
 
  output logic        window_valid,
  output logic [CNT_W-1:0] c_windows,
  output logic             ever_frame_limited
);
 
  localparam int unsigned MS_TICKS   = 1000 * CLK_MHZ;
  // What this design's forwarding engine can do, and what one port can.
  localparam int unsigned MAX_KFPS   = 1488;      // 1.488 Mpps
  localparam int unsigned MAX_MBPS   = 1000;
  localparam int unsigned NEAR_PCT   = 85;
 
  logic [31:0] tick_q;
  logic [15:0] ms_q;
  logic [CNT_W-1:0] frames_q, octets_q, drops_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      tick_q <= '0; ms_q <= 16'd0;
      frames_q <= '0; octets_q <= '0; drops_q <= '0;
      frames_in_window <= '0; octets_in_window <= '0; drops_in_window <= '0;
      mbps_delivered <= 18'd0; kfps_delivered <= 18'd0;
      mean_frame_octets <= 14'd0;
      near_frame_rate_limit <= 1'b0; near_bit_rate_limit <= 1'b0;
      binding_limit <= 2'd0; window_valid <= 1'b0;
      if (!rst_n) begin c_windows <= '0; ever_frame_limited <= 1'b0; end
    end else begin
      if (frame_forwarded) begin
        if (!(&frames_q)) frames_q <= frames_q + 1'b1;
        octets_q <= octets_q + CNT_W'(frame_length);
      end
      if (frame_dropped) begin
        if (!(&drops_q)) drops_q <= drops_q + 1'b1;
      end
 
      if (tick_q == 32'(MS_TICKS - 1)) begin
        tick_q <= '0;
        ms_q   <= ms_q + 16'd1;
      end else begin
        tick_q <= tick_q + 1'b1;
      end
 
      if (ms_q == 16'(WINDOW_MS)) begin
        ms_q         <= 16'd0;
        window_valid <= 1'b1;
        frames_in_window <= frames_q;
        octets_in_window <= octets_q;
        drops_in_window  <= drops_q;
        if (!(&c_windows)) c_windows <= c_windows + 1'b1;
 
        // Both characterisations, from the same window.
        kfps_delivered <= 18'((frames_q * 1000) / 32'(WINDOW_MS) / 32'd1000);
        mbps_delivered <= 18'((octets_q * 8 * 1000) /
                              32'(WINDOW_MS) / 32'd1_000_000);
        mean_frame_octets <= (frames_q == 0) ? 14'd0
                             : 14'(octets_q / frames_q);
 
        // WHICH LIMIT BINDS. A switch at 90% of its frame rate and one
        // at 90% of its bit rate need different remedies -- more
        // forwarding capacity against more link capacity -- and
        // throughput alone cannot tell them apart.
        near_frame_rate_limit <=
          (((frames_q * 1000 / 32'(WINDOW_MS)) * 100) >
           (32'(MAX_KFPS) * 1000 * 32'(NEAR_PCT)));
        near_bit_rate_limit <=
          (((octets_q * 8 / 32'(WINDOW_MS) / 1000) * 100) >
           (32'(MAX_MBPS) * 32'(NEAR_PCT)));
 
        if (((frames_q * 1000 / 32'(WINDOW_MS)) * 100) >
            (32'(MAX_KFPS) * 1000 * 32'(NEAR_PCT))) begin
          binding_limit      <= 2'd1;
          ever_frame_limited <= 1'b1;
        end else if (((octets_q * 8 / 32'(WINDOW_MS) / 1000) * 100) >
                     (32'(MAX_MBPS) * 32'(NEAR_PCT))) begin
          binding_limit <= 2'd2;
        end else begin
          binding_limit <= 2'd0;
        end
 
        frames_q <= '0; octets_q <= '0; drops_q <= '0;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Decomposes a switch's contribution to Chapter 8.4's latency budget,
// because three of its four terms are design constants and the fourth
// is decided by the traffic.
//
//   INGRESS      fixed -- extract the addresses, build a descriptor
//   LOOKUP       fixed -- Section 3's 28 ns budget
//   QUEUEING     UNBOUNDED -- how many frames are ahead of this one
//   SERIALISATION the frame's own transmission time at the link rate,
//                which belongs to the LINK and not to the switch
//
// So a single "switch latency" figure is a statement about the first
// two terms under no load, and it tells an operator nothing about the
// third -- which is the one that grows without limit and the one they
// are actually asking about.
module switch_latency_accountant
  import switching_pkg::*;
#(
  parameter int unsigned CLK_MHZ = 500,
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  logic        frame_arrived,
  input  logic        descriptor_ready,
  input  logic        decision_made,
  input  logic        enqueued,
  input  logic        dequeued,
  input  logic        transmitted,
  input  logic [13:0] frame_length,
  input  logic [17:0] link_mbps,
 
  // The four terms, separately.
  output logic [15:0] ingress_ns,
  output logic [15:0] lookup_ns,
  output logic [19:0] queue_ns,
  output logic [19:0] serialise_ns,
  output logic [19:0] total_ns,
 
  // Worst case for each, which is the number that matters.
  output logic [15:0] worst_ingress_ns,
  output logic [15:0] worst_lookup_ns,
  output logic [19:0] worst_queue_ns,
 
  // Which term dominated. A switch whose latency is queueing and one
  // whose latency is lookup need completely different remedies.
  output logic [1:0]  dominant_term,       // 0 ing, 1 lookup, 2 queue
  output logic [6:0]  queue_share_percent,
 
  output logic        measurement_valid,
  output logic [CNT_W-1:0] c_measurements,
  // The queue contributed more than this share. Not an error, and the
  // signal that says a latency complaint is about load rather than
  // about the switch.
  output logic             queue_dominated,
  output logic             ever_queue_dominated
);
 
  logic [19:0] t_arrive_q, t_desc_q, t_decide_q, t_enq_q, t_deq_q;
  logic [19:0] tick_q;
 
  // Nanoseconds per clock, as a reciprocal-free constant.
  localparam int unsigned NS_PER_CLK = 1000 / CLK_MHZ;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      tick_q <= '0; t_arrive_q <= '0; t_desc_q <= '0;
      t_decide_q <= '0; t_enq_q <= '0; t_deq_q <= '0;
      ingress_ns <= '0; lookup_ns <= '0; queue_ns <= '0;
      serialise_ns <= '0; total_ns <= '0;
      worst_ingress_ns <= '0; worst_lookup_ns <= '0; worst_queue_ns <= '0;
      dominant_term <= 2'd0; queue_share_percent <= 7'd0;
      measurement_valid <= 1'b0; queue_dominated <= 1'b0;
      if (!rst_n) begin c_measurements <= '0; ever_queue_dominated <= 1'b0; end
    end else begin
      measurement_valid <= 1'b0;
      tick_q            <= tick_q + 1'b1;
 
      if (frame_arrived)    t_arrive_q <= tick_q;
      if (descriptor_ready) t_desc_q   <= tick_q;
      if (decision_made)    t_decide_q <= tick_q;
      if (enqueued)         t_enq_q    <= tick_q;
      if (dequeued)         t_deq_q    <= tick_q;
 
      if (transmitted) begin
        ingress_ns <= 16'((t_desc_q   - t_arrive_q) * NS_PER_CLK);
        lookup_ns  <= 16'((t_decide_q - t_desc_q)   * NS_PER_CLK);
        // THE UNBOUNDED TERM. Everything between enqueue and dequeue is
        // other frames ahead of this one, and nothing in this design
        // decides how many there are.
        queue_ns   <= 20'((t_deq_q - t_enq_q) * NS_PER_CLK);
 
        // SERIALISATION belongs to the LINK, not to the switch. Counted
        // separately so it is not attributed to the switch's design.
        serialise_ns <= (link_mbps == 0) ? 20'd0
                        : 20'((frame_length * 8 * 1000) / link_mbps);
 
        total_ns <= 20'((t_deq_q - t_arrive_q) * NS_PER_CLK) +
                    ((link_mbps == 0) ? 20'd0
                     : 20'((frame_length * 8 * 1000) / link_mbps));
 
        if (16'((t_desc_q - t_arrive_q) * NS_PER_CLK) > worst_ingress_ns)
          worst_ingress_ns <= 16'((t_desc_q - t_arrive_q) * NS_PER_CLK);
        if (16'((t_decide_q - t_desc_q) * NS_PER_CLK) > worst_lookup_ns)
          worst_lookup_ns <= 16'((t_decide_q - t_desc_q) * NS_PER_CLK);
        if (20'((t_deq_q - t_enq_q) * NS_PER_CLK) > worst_queue_ns)
          worst_queue_ns <= 20'((t_deq_q - t_enq_q) * NS_PER_CLK);
 
        measurement_valid <= 1'b1;
        if (!(&c_measurements)) c_measurements <= c_measurements + 1'b1;
 
        // WHICH TERM DOMINATED, which is what turns a latency figure
        // into an action.
        if ((t_deq_q - t_enq_q) > (t_decide_q - t_arrive_q)) begin
          dominant_term        <= 2'd2;
          queue_dominated      <= 1'b1;
          ever_queue_dominated <= 1'b1;
        end else if ((t_decide_q - t_desc_q) > (t_desc_q - t_arrive_q)) begin
          dominant_term   <= 2'd1;
          queue_dominated <= 1'b0;
        end else begin
          dominant_term   <= 2'd0;
          queue_dominated <= 1'b0;
        end
      end
    end
  end
 
endmodule

// SYNTHESIZABLE.
//
// Checks the invariants a switch must never violate, all of which are
// about what it does to a frame rather than about whether it delivers
// it.
//
// THE DISTINCTION THIS MODULE RESTS ON. A switch is ALLOWED to:
//   discard a frame          -- Section 6's arithmetic
//   flood a frame            -- on a miss, or a group destination
//   filter a frame           -- destination on the ingress port
//   delay a frame            -- arbitrarily, by queueing it
//
// A switch is NOT allowed to:
//   duplicate a frame onto one egress port
//   send a frame back out its ingress port
//   modify a frame's contents
//   reorder frames within one ingress/egress pair
//
// The second list is short, absolute, and entirely about integrity --
// which is why the properties in Section 15 are about the policy and
// never about delivery.
module switch_conformance_monitor
  import switching_pkg::*;
#(
  parameter int unsigned CNT_W = 24
) (
  input  logic clk,
  input  logic rst_n,
  input  logic clear,
 
  input  descriptor_t        descriptor,
  input  logic               forward_valid,
  input  logic [N_PORTS-1:0] egress_mask,
  input  logic [1:0]         forward_action,
 
  input  logic               frame_emitted,
  input  logic [PORT_BITS-1:0] emit_port,
  input  logic [MAC_BITS-1:0]  emit_dst,
  input  logic [MAC_BITS-1:0]  emit_src,
  input  logic [13:0]          emit_length,
 
  // The four absolute violations.
  output logic sent_to_ingress_port,
  output logic frame_modified,
  output logic duplicate_on_one_port,
  output logic reordered,
 
  output logic [CNT_W-1:0] c_ingress_echo,
  output logic [CNT_W-1:0] c_modified,
  output logic [CNT_W-1:0] c_duplicated,
  output logic [CNT_W-1:0] c_reordered,
 
  // Policy accounting -- legal outcomes, counted rather than flagged.
  output logic [CNT_W-1:0] c_forward,
  output logic [CNT_W-1:0] c_flood,
  output logic [CNT_W-1:0] c_filter,
 
  output logic       first_violation_valid,
  output logic [1:0] first_violation_kind,
  output logic       ever_violated
);
 
  descriptor_t pending_q;
  logic        pending_valid_q;
  logic [N_PORTS-1:0] emitted_mask_q;
  logic [15:0] seq_expected_q, seq_seen_q;
  logic        any_c;
  logic [1:0]  kind_c;
 
  always_comb begin
    any_c  = 1'b0;
    kind_c = 2'd0;
    if      (sent_to_ingress_port)  begin any_c = 1'b1; kind_c = 2'd0; end
    else if (frame_modified)        begin any_c = 1'b1; kind_c = 2'd1; end
    else if (duplicate_on_one_port) begin any_c = 1'b1; kind_c = 2'd2; end
    else if (reordered)             begin any_c = 1'b1; kind_c = 2'd3; end
  end
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      pending_q <= '0; pending_valid_q <= 1'b0; emitted_mask_q <= '0;
      seq_expected_q <= 16'd0; seq_seen_q <= 16'd0;
      sent_to_ingress_port <= 1'b0; frame_modified <= 1'b0;
      duplicate_on_one_port <= 1'b0; reordered <= 1'b0;
      c_ingress_echo <= '0; c_modified <= '0; c_duplicated <= '0;
      c_reordered <= '0; c_forward <= '0; c_flood <= '0; c_filter <= '0;
      first_violation_valid <= 1'b0; first_violation_kind <= 2'd0;
      ever_violated <= 1'b0;
    end else if (clear) begin
      c_ingress_echo <= '0; c_modified <= '0; c_duplicated <= '0;
      c_reordered <= '0; c_forward <= '0; c_flood <= '0; c_filter <= '0;
      first_violation_valid <= 1'b0;
      // ever_violated survives.
    end else begin
      sent_to_ingress_port  <= 1'b0;
      frame_modified        <= 1'b0;
      duplicate_on_one_port <= 1'b0;
      reordered             <= 1'b0;
 
      if (forward_valid) begin
        pending_q       <= descriptor;
        pending_valid_q <= 1'b1;
        emitted_mask_q  <= '0;
 
        // THE INGRESS-ECHO CHECK, made on the DECISION rather than on
        // the emission -- it is cheaper here and it catches the fault
        // before the frame is on a wire.
        if (egress_mask[descriptor.ingress_port]) begin
          sent_to_ingress_port <= 1'b1;
          if (!(&c_ingress_echo)) c_ingress_echo <= c_ingress_echo + 1'b1;
        end
 
        unique case (forward_action)
          2'd0: if (!(&c_forward)) c_forward <= c_forward + 1'b1;
          2'd1: if (!(&c_flood))   c_flood   <= c_flood   + 1'b1;
          2'd2: if (!(&c_filter))  c_filter  <= c_filter  + 1'b1;
          default: ;
        endcase
      end
 
      if (frame_emitted && pending_valid_q) begin
        // A SWITCH DOES NOT MODIFY. Same addresses, same length -- a
        // basic switch is a forwarding device, not a rewriting one.
        if ((emit_dst != pending_q.dst) || (emit_src != pending_q.src) ||
            (emit_length != pending_q.length)) begin
          frame_modified <= 1'b1;
          if (!(&c_modified)) c_modified <= c_modified + 1'b1;
        end
 
        // NOT TWICE ON ONE PORT. Flooding sends one copy to each of
        // many ports; two copies to one port is a duplicate.
        if (emitted_mask_q[emit_port]) begin
          duplicate_on_one_port <= 1'b1;
          if (!(&c_duplicated)) c_duplicated <= c_duplicated + 1'b1;
        end
        emitted_mask_q[emit_port] <= 1'b1;
 
        // AND NOT OUT THE INGRESS PORT.
        if (emit_port == pending_q.ingress_port) begin
          sent_to_ingress_port <= 1'b1;
          if (!(&c_ingress_echo)) c_ingress_echo <= c_ingress_echo + 1'b1;
        end
      end
 
      if (any_c) begin
        ever_violated <= 1'b1;
        if (!first_violation_valid) begin
          first_violation_valid <= 1'b1;
          first_violation_kind  <= kind_c;
        end
      end
    end
  end
 
endmodule

// P1. The ingress port is recorded. It is not in the frame, and every
// later step needs it.
property p_ingress_port_recorded;
  @(posedge clk) disable iff (!rst_n)
  descriptor_valid |-> (descriptor.ingress_port == PORT_BITS'(PORT_ID));
endproperty
a_ingress_recorded: assert property (p_ingress_port_recorded);
 
// P2. A frame that failed its check sequence produces NO descriptor --
// it is neither forwarded nor learned from.
property p_bad_fcs_no_descriptor;
  @(posedge clk) disable iff (!rst_n)
  (frame_end && frame_bad_fcs) |=> !descriptor_valid;
endproperty
a_bad_fcs_no_descriptor: assert property (p_bad_fcs_no_descriptor);
 
// P3. The destination classification follows Chapter 5.3's I/G bit and
// the all-ones broadcast address, in that priority.
property p_broadcast_classified_first;
  @(posedge clk) disable iff (!rst_n)
  (descriptor_valid && (descriptor.dst == 48'hFFFF_FFFF_FFFF))
    |-> (descriptor.dst_kind == DST_BROADCAST);
endproperty
a_broadcast_first: assert property (p_broadcast_classified_first);
 
// P4. A group SOURCE address is flagged. Learning it puts a multicast
// address in the table, where a destination lookup will match it.
property p_group_source_flagged;
  @(posedge clk) disable iff (!rst_n)
  (descriptor_valid && descriptor.src[40]) |-> descriptor.src_is_group;
endproperty
a_group_source_flagged: assert property (p_group_source_flagged);

// P5. THE ORDERING PROPERTY. Learning happens before the lookup, so a
// station that has moved updates the table before any frame in the
// opposite direction is forwarded to where it used to be.
property p_learn_before_lookup;
  @(posedge clk) disable iff (!rst_n)
  lookup_request |-> $past(learn_request || desc_q.src_is_group);
endproperty
a_learn_before_lookup: assert property (p_learn_before_lookup);
 
// P6. Learning is unconditional on the forwarding RESULT. A frame that
// will be filtered or dropped still teaches the switch where its
// sender is.
property p_learn_regardless_of_action;
  @(posedge clk) disable iff (!rst_n)
  (descriptor_valid && !descriptor.src_is_group) |-> ##[1:3] learn_request;
endproperty
a_learn_regardless: assert property (p_learn_regardless_of_action);
 
// P7. A group source is REFUSED, never learned.
property p_group_source_not_learned;
  @(posedge clk) disable iff (!rst_n)
  (st_q == F_LEARN) && desc_q.src_is_group |-> !learn_request;
endproperty
a_group_source_not_learned: assert property (p_group_source_not_learned);
 
// P8. Broadcast and multicast are not looked up at all -- their answer
// is known without consulting the table.
property p_group_dst_no_lookup;
  @(posedge clk) disable iff (!rst_n)
  ((st_q == F_LOOKUP) && (desc_q.dst_kind != DST_UNICAST))
    |-> !lookup_request;
endproperty
a_group_dst_no_lookup: assert property (p_group_dst_no_lookup);

// P9. NEVER out the ingress port. The most fundamental invariant in
// switching, and the one a flood must explicitly exclude.
property p_never_egress_on_ingress;
  @(posedge clk) disable iff (!rst_n)
  forward_valid |-> !egress_mask[descriptor.ingress_port];
endproperty
a_never_ingress_echo: assert property (p_never_egress_on_ingress);
 
// P10. NEVER twice on one port. Flooding is one copy to each of many
// ports; two to one port is a duplicate.
property p_no_duplicate_on_a_port;
  @(posedge clk) disable iff (!rst_n)
  (frame_emitted && emitted_mask_q[emit_port]) |=> duplicate_on_one_port;
endproperty
a_no_duplicate: assert property (p_no_duplicate_on_a_port);
 
// P11. NEVER modified. A basic switch forwards; it does not rewrite.
property p_frame_unmodified;
  @(posedge clk) disable iff (!rst_n)
  (frame_emitted && pending_valid_q)
    |-> ((emit_dst == pending_q.dst) && (emit_src == pending_q.src));
endproperty
a_frame_unmodified: assert property (p_frame_unmodified);
 
// P12. A unicast hit on a port OTHER than the ingress produces exactly
// ONE egress port -- not a flood, not none.
property p_unicast_hit_one_port;
  @(posedge clk) disable iff (!rst_n)
  (forward_valid && (forward_action == 2'd0)) |-> $onehot(egress_mask);
endproperty
a_unicast_one_port: assert property (p_unicast_hit_one_port);
 
// P13. A filter produces NO egress port. A successful lookup can
// legitimately send the frame nowhere.
property p_filter_no_egress;
  @(posedge clk) disable iff (!rst_n)
  (forward_valid && (forward_action == 2'd2)) |-> (egress_mask == '0);
endproperty
a_filter_no_egress: assert property (p_filter_no_egress);
 
// P14. A flood covers every port EXCEPT the ingress -- exactly.
property p_flood_is_all_but_ingress;
  @(posedge clk) disable iff (!rst_n)
  (forward_valid && (forward_action == 2'd1))
    |-> (egress_mask == ~(N_PORTS'(1) << descriptor.ingress_port));
endproperty
a_flood_all_but_ingress: assert property (p_flood_is_all_but_ingress);

// P15. THE POLICY PROPERTY. A drop happens only when the queue is
// full -- never as a shortcut, and never on an arbitrary frame.
property p_drop_only_when_full;
  @(posedge clk) disable iff (!rst_n)
  drop_now |-> (queue_occupancy >= 8'(QUEUE_DEPTH));
endproperty
a_drop_only_when_full: assert property (p_drop_only_when_full);
 
// P16. Every drop is ATTRIBUTED to an ingress port. "Port 7 is
// congested" and "port 3's traffic is filling port 7" are different
// findings.
property p_drop_attributed;
  @(posedge clk) disable iff (!rst_n)
  drop_now |-> (dropped_from_port < PORT_BITS'(N_PORTS));
endproperty
a_drop_attributed: assert property (p_drop_attributed);
 
// P17. A grant goes only to a requesting port.
property p_grant_to_requester;
  @(posedge clk) disable iff (!rst_n)
  grant_valid |-> request[granted_port];
endproperty
a_grant_to_requester: assert property (p_grant_to_requester);
 
// P18. The round-robin pointer ADVANCES past the winner, so a
// permanently-requesting port cannot monopolise the egress.
property p_pointer_advances;
  @(posedge clk) disable iff (!rst_n)
  grant_valid |=> (rr_q != $past(granted_port));
endproperty
a_pointer_advances: assert property (p_pointer_advances);
 
// P19. Drops and grants are mutually exclusive in a cycle -- a frame
// is served or discarded, never both.
property p_grant_drop_exclusive;
  @(posedge clk) disable iff (!rst_n)
  !(grant_valid && drop_now);
endproperty
a_grant_drop_exclusive: assert property (p_grant_drop_exclusive);

// P20. Both capacity characterisations are computed, because they rank
// a switch differently and only one is on the datasheet.
property p_both_rates_reported;
  @(posedge clk) disable iff (!rst_n)
  window_valid |-> ((kfps_delivered != 18'hXXXXX) &&
                    (mbps_delivered != 18'hXXXXX));
endproperty
a_both_rates: assert property (p_both_rates_reported);
 
// P21. Which limit binds is named. A frame-rate limit and a bit-rate
// limit need different remedies and look identical from throughput.
property p_binding_limit_named;
  @(posedge clk) disable iff (!rst_n)
  (window_valid && (near_frame_rate_limit || near_bit_rate_limit))
    |-> (binding_limit != 2'd0);
endproperty
a_binding_limit_named: assert property (p_binding_limit_named);
 
// P22. Serialisation is attributed to the LINK, not to the switch --
// otherwise a fast switch on a slow link measures as slow.
property p_serialisation_separate;
  @(posedge clk) disable iff (!rst_n)
  measurement_valid |-> (total_ns >= serialise_ns);
endproperty
a_serialisation_separate: assert property (p_serialisation_separate);
 
// P23. The dominant latency term is named. Queue-dominated latency is
// a load problem; lookup-dominated latency is a design problem.
property p_dominant_term_named;
  @(posedge clk) disable iff (!rst_n)
  measurement_valid |-> (dominant_term <= 2'd2);
endproperty
a_dominant_term_named: assert property (p_dominant_term_named);
 
// P24. Starvation is reported. A round-robin that is not round
// delivers all of one port's traffic and none of another's, with both
// ports showing valid links and zero errors.
property p_starvation_reported;
  @(posedge clk) disable iff (!rst_n)
  starvation_suspected |-> (most_granted_port != least_granted_port);
endproperty
a_starvation_reported: assert property (p_starvation_reported);