Ethernet against PCIe

3 windows x 2 registers x 64 bits = 384 flip-flops per port
384 x 20 BCE = 7 680 BCE per port

// ---------------------------------------------------------------------
// pciecmp_pkg -- the constants this chapter's comparison needs, with
// every derived figure computed here rather than written as a literal.
//
// The unit is Chapter 23.3 Section 2's bitcell equivalent:
//   1 BCE = one bit of usable on-die SRAM = 0.35 GE
//   1 flip-flop = 20 BCE
//   Chapter 19.7 Section 19's MAC receive datapath = 283 320 BCE
// ---------------------------------------------------------------------
package pciecmp_pkg;

  // ---- the anchor ------------------------------------------------------
  localparam int unsigned DATAPATH_BCE   = 283_320;
  localparam int unsigned BCE_PER_FLOP   = 20;

  // ---- the Ethernet side ----------------------------------------------
  localparam int unsigned MAC_TBL_ENTRIES = 128 * 1024;
  localparam int unsigned MAC_TBL_WIDTH   = 96;
  localparam int unsigned SWITCH_PORTS    = 64;

  // ---- the PCIe side ---------------------------------------------------
  // Three decode windows -- non-prefetchable memory, prefetchable
  // memory, and I/O -- each a base and a limit, at 64 bits.
  localparam int unsigned DECODE_WINDOWS  = 3;
  localparam int unsigned DECODE_REGS     = 2;   // base, limit
  localparam int unsigned DECODE_WIDTH    = 64;

  // ---- the return path -------------------------------------------------
  // PCIe Gen5 supports 10-bit tags; the number a link NEEDS is set by
  // Little's law and is derived in Section 4 rather than assumed.
  localparam int unsigned TAG_BITS        = 10;
  localparam int unsigned TAG_ENTRY_BITS  = 128; // tag, requester, addr,
                                                 // length, BE, ptr, valid
  localparam int unsigned MAX_PAYLOAD_B   = 256;

  // ---- credits ---------------------------------------------------------
  // Three credit types (posted, non-posted, completion) x two units
  // (header 8 b, data 12 b) x three registers (limit, consumed,
  // allocated), per virtual channel, per direction.
  localparam int unsigned CREDIT_TYPES    = 3;
  localparam int unsigned CREDIT_HDR_BITS = 8;
  localparam int unsigned CREDIT_DAT_BITS = 12;
  localparam int unsigned CREDIT_REGS     = 3;
  localparam int unsigned VIRTUAL_CHANS   = 8;

  typedef enum logic [1:0] {
    XACT_POSTED     = 2'd0,   // memory write -- no completion
    XACT_NONPOSTED  = 2'd1,   // memory read  -- a completion is owed
    XACT_COMPLETION = 2'd2    // the completion itself
  } xact_e;

  typedef enum logic [1:0] {
    CPL_SUCCESSFUL      = 2'd0,
    CPL_UNSUPPORTED_REQ = 2'd1,
    CPL_ABORT           = 2'd2,
    CPL_RETRY           = 2'd3
  } cpl_status_e;

  // ---- derived: the Ethernet lookup, per port -------------------------
  function automatic int unsigned mac_table_bce();
    return MAC_TBL_ENTRIES * MAC_TBL_WIDTH;          // an array: 1 BCE/bit
  endfunction

  function automatic int unsigned mac_table_bce_per_port();
    return mac_table_bce() / SWITCH_PORTS;
  endfunction

  // ---- derived: the PCIe decode, per port ------------------------------
  function automatic int unsigned decode_flops();
    return DECODE_WINDOWS * DECODE_REGS * DECODE_WIDTH;
  endfunction

  function automatic int unsigned decode_bce_per_port();
    return decode_flops() * BCE_PER_FLOP;            // registers: 20/bit
  endfunction

  // ---- derived: Little's law at the return path ------------------------
  // bytes in flight = rate x round trip. Expressed in the units the
  // callers have: Gb/s and nanoseconds give bytes directly, because
  // 1 Gb/s x 1 ns = 0.125 bytes and the /8 does the conversion.
  function automatic int unsigned bytes_in_flight(int unsigned gbps,
                                                  int unsigned rtt_ns);
    return (gbps * rtt_ns) / 8;
  endfunction

  function automatic int unsigned tags_needed(int unsigned gbps,
                                              int unsigned rtt_ns);
    int unsigned b;
    b = bytes_in_flight(gbps, rtt_ns);
    return (b + MAX_PAYLOAD_B - 1) / MAX_PAYLOAD_B;  // round up
  endfunction

  function automatic int unsigned return_path_bce(int unsigned gbps,
                                                  int unsigned rtt_ns);
    // The tag table is an array, and so is the reorder buffer.
    return (tags_needed(gbps, rtt_ns) * TAG_ENTRY_BITS)
         + (bytes_in_flight(gbps, rtt_ns) * 8);
  endfunction

  // ---- derived: credit state -------------------------------------------
  function automatic int unsigned credit_flops_per_port();
    return VIRTUAL_CHANS * CREDIT_TYPES
         * (CREDIT_HDR_BITS + CREDIT_DAT_BITS)
         * CREDIT_REGS * 2;                          // two directions
  endfunction

  function automatic int unsigned credit_bce_per_port();
    return credit_flops_per_port() * BCE_PER_FLOP;
  endfunction

  // ---- reporting -------------------------------------------------------
  // Datapaths, in thousandths, so an integer output can carry a ratio
  // smaller than one without becoming zero.
  function automatic int unsigned datapaths_milli(int unsigned bce);
    return (bce * 1000) / DATAPATH_BCE;
  endfunction

endpackage

// ---------------------------------------------------------------------
// address_model -- what a NAME costs against a POSITION, and the
// failure mode each one has.
//
// The area numbers are the easy half. The output that matters is
// lookup_can_miss, which is 1 on one side and 0 on the other and is
// the reason the two sides need different diagnostic chapters.
// ---------------------------------------------------------------------
module address_model
  import pciecmp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        is_ethernet,       // 1 = name lookup, 0 = decode
  input  logic [15:0] ports,
  input  logic        lookup_hit,
  input  logic        decode_hit,

  output logic [31:0] addressing_bce_per_port,
  output logic [31:0] addressing_dp_milli,
  output logic        lookup_can_miss,
  output logic [15:0] copies_on_miss,
  output logic        miss_is_reported,
  output logic        miss_occurred,
  output logic [31:0] c_misses,
  output logic [31:0] c_flooded_copies
);
  always_comb begin
    addressing_bce_per_port = is_ethernet ? 32'(mac_table_bce_per_port())
                                          : 32'(decode_bce_per_port());
    addressing_dp_milli     = 32'(datapaths_milli(addressing_bce_per_port));

    // THE difference. A name can be absent from a table; a position
    // cannot be absent from a space.
    lookup_can_miss = is_ethernet;

    // Chapter 12.4 Section 6: a miss replicates to every other port in
    // the VLAN. A decode miss produces exactly one completion.
    copies_on_miss  = is_ethernet ? (ports - 16'd1) : 16'd1;

    // And the one that decides whether a chapter like 21.6 has to exist.
    miss_is_reported = !is_ethernet;

    miss_occurred = is_ethernet ? !lookup_hit : !decode_hit;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_misses <= '0; c_flooded_copies <= '0;
    end else if (miss_occurred) begin
      c_misses         <= c_misses + 32'd1;
      c_flooded_copies <= c_flooded_copies + 32'(copies_on_miss);
    end
  end
endmodule

// ---------------------------------------------------------------------
// outstanding_reads -- the tag table and the reorder buffer a return
// path forces, sized by Little's law and reported in BCE.
//
// The important outputs are ethernet_equivalent_bce, which is zero and
// stays zero, and reorder_share_pct, which says where the cost is.
// ---------------------------------------------------------------------
module outstanding_reads
  import pciecmp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] rate_gbps,
  input  logic [15:0] rtt_ns,
  input  logic [15:0] tag_limit,        // what the design implements

  input  logic        read_issued,
  input  logic        completion_rx,

  output logic [15:0] tags_required,
  output logic [31:0] bytes_inflight,
  output logic [31:0] tag_table_bce,
  output logic [31:0] reorder_bce,
  output logic [31:0] return_path_bce_o,
  output logic [15:0] reorder_share_pct,
  output logic [31:0] return_path_dp_milli,
  output logic [31:0] ethernet_equivalent_bce,
  output logic        tag_limit_binds,
  output logic [15:0] achievable_gbps,
  output logic [15:0] outstanding_now,
  output logic [31:0] c_tag_exhausted
);
  always_comb begin
    bytes_inflight    = 32'(bytes_in_flight(int'(rate_gbps), int'(rtt_ns)));
    tags_required     = 16'(tags_needed(int'(rate_gbps), int'(rtt_ns)));

    tag_table_bce     = 32'(tags_required) * 32'(TAG_ENTRY_BITS);
    reorder_bce       = bytes_inflight * 32'd8;
    return_path_bce_o = tag_table_bce + reorder_bce;

    reorder_share_pct = (return_path_bce_o == 0) ? 16'd0
                      : 16'((reorder_bce * 100) / return_path_bce_o);

    return_path_dp_milli = 32'(datapaths_milli(return_path_bce_o));

    // The comparison, and it is a constant. An Ethernet transmitter
    // holds nothing about a frame it has sent.
    ethernet_equivalent_bce = 32'd0;

    // Chapter 21.8 Section 5's ceiling, at this boundary.
    tag_limit_binds = (tag_limit < tags_required);
    achievable_gbps = (rtt_ns == 0) ? rate_gbps
                    : 16'(((32'(tag_limit) * 32'(MAX_PAYLOAD_B) * 8) * 1000)
                          / (32'(rtt_ns) * 1000));
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      outstanding_now <= '0; c_tag_exhausted <= '0;
    end else begin
      case ({read_issued, completion_rx})
        2'b10: outstanding_now <= outstanding_now + 16'd1;
        2'b01: if (outstanding_now != 0)
                 outstanding_now <= outstanding_now - 16'd1;
        default: ;
      endcase
      if (read_issued && (outstanding_now >= tag_limit))
        c_tag_exhausted <= c_tag_exhausted + 32'd1;
    end
  end
endmodule

// Ethernet. This is true, provable locally, and nothing can make it false.
p_eth_progress: assert property (@(posedge clk) disable iff (!rst_n)
  (frame_ready && link_up && !paused) |-> ##[1:IFG_CYCLES] tx_start);

// PCIe. The same shape, and the antecedent now contains a term whose
// value the far end decides.
p_pcie_progress: assert property (@(posedge clk) disable iff (!rst_n)
  (tlp_ready && link_up && credits_available) |-> ##[1:ARB_CYCLES] tx_start);

per virtual channel, per direction:
  3 types (posted, non-posted, completion)
  x (8-bit header credit + 12-bit data credit)
  x 3 registers (limit, consumed, allocated)
  = 3 x 20 x 3 = 180 flip-flops

// ---------------------------------------------------------------------
// credit_accountant -- the three-register credit loop, per type, and
// the buffer obligation the advertisement creates.
//
// The counters are exact and small. The output that matters is
// buffer_obligation_bce, which is the promise the counters imply.
// ---------------------------------------------------------------------
module credit_accountant
  import pciecmp_pkg::*;
#(
  parameter int unsigned VCS = 8
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] rate_gbps,
  input  logic [15:0] rtt_ns,
  input  logic        per_vc_guaranteed,   // each VC gets its own space

  input  logic        tlp_sent,
  input  logic  [1:0] tlp_type,            // xact_e
  input  logic [11:0] tlp_data_credits,
  input  logic        credit_return,
  input  logic  [1:0] ret_type,
  input  logic [11:0] ret_data_credits,

  output logic [31:0] credit_flops_o,
  output logic [31:0] credit_bce_o,
  output logic [31:0] buffer_obligation_bce,
  output logic [15:0] obligation_ratio,    // buffer / counters
  output logic        may_transmit,
  output logic        stalled_on_credit,
  output logic [31:0] c_credit_stall_cycles
);
  // limit, consumed, allocated -- per type, header and data.
  logic  [7:0] hdr_limit    [3];
  logic  [7:0] hdr_consumed [3];
  logic [11:0] dat_limit    [3];
  logic [11:0] dat_consumed [3];

  always_comb begin
    credit_flops_o = 32'(credit_flops_per_port());
    credit_bce_o   = 32'(credit_bce_per_port());

    // The obligation: a round trip of buffer, times the VCs that need
    // their own guaranteed share.
    buffer_obligation_bce =
      32'(bytes_in_flight(int'(rate_gbps), int'(rtt_ns))) * 32'd8
      * (per_vc_guaranteed ? 32'(VCS) : 32'd1);

    obligation_ratio = (credit_bce_o == 0) ? 16'd0
                     : 16'(buffer_obligation_bce / credit_bce_o);

    // The gate. Note that it is checked on EVERY packet, and that at
    // reset every limit is zero -- so the default is "do not transmit".
    may_transmit = (hdr_consumed[tlp_type] < hdr_limit[tlp_type])
                && ({4'd0, dat_consumed[tlp_type]} + {4'd0, tlp_data_credits}
                    <= {4'd0, dat_limit[tlp_type]});

    stalled_on_credit = tlp_sent && !may_transmit;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < 3; i++) begin
        hdr_limit[i]    <= '0;   // zero at reset: nothing may be sent
        hdr_consumed[i] <= '0;
        dat_limit[i]    <= '0;
        dat_consumed[i] <= '0;
      end
      c_credit_stall_cycles <= '0;
    end else begin
      if (tlp_sent && may_transmit) begin
        hdr_consumed[tlp_type] <= hdr_consumed[tlp_type] + 8'd1;
        dat_consumed[tlp_type] <= dat_consumed[tlp_type] + tlp_data_credits;
      end
      if (credit_return) begin
        hdr_limit[ret_type] <= hdr_limit[ret_type] + 8'd1;
        dat_limit[ret_type] <= dat_limit[ret_type] + ret_data_credits;
      end
      if (stalled_on_credit)
        c_credit_stall_cycles <= c_credit_stall_cycles + 32'd1;
    end
  end
endmodule

producer:   write data to memory        (posted)
            write a flag to memory      (posted)
consumer:   read the flag               (non-posted)
            if set, read the data       (non-posted)

196 x 195 / 2 = 19 110 comparisons

// ---------------------------------------------------------------------
// ordering_scoreboard -- PCIe's ordering rules, enforced with a counter
// per transaction type instead of a comparison per transaction pair.
//
// The module also reports what the naive structure would have cost, so
// the specification's shape is visible as a number.
// ---------------------------------------------------------------------
module ordering_scoreboard
  import pciecmp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] outstanding_max,

  input  logic        xact_issue,
  input  logic  [1:0] xact_kind,          // xact_e
  input  logic        xact_retire,
  input  logic  [1:0] retire_kind,

  output logic        may_proceed,
  output logic        blocked_by_posted,
  output logic [15:0] pending_posted,
  output logic [15:0] pending_nonposted,
  output logic [15:0] pending_completion,
  output logic [31:0] pairwise_comparisons,
  output logic [31:0] counter_flops,
  output logic [31:0] counter_bce,
  output logic        ethernet_orders_this,
  output logic [31:0] c_order_blocks
);
  always_comb begin
    // What the rules cost, stated over types.
    counter_flops = 32'd3 * 32'd8;
    counter_bce   = counter_flops * 32'(BCE_PER_FLOP);

    // What they would have cost, stated over transactions.
    pairwise_comparisons = (32'(outstanding_max)
                            * (32'(outstanding_max) - 32'd1)) / 32'd2;

    // The rule that makes producer-consumer work: a posted write may
    // not pass an earlier posted write, and a completion may not pass
    // an earlier posted write.
    blocked_by_posted = (pending_posted != 16'd0)
                     && ((xact_kind == 2'(XACT_COMPLETION))
                      || (xact_kind == 2'(XACT_POSTED)));

    may_proceed = xact_issue && !blocked_by_posted;

    // And the comparison this chapter exists to make.
    ethernet_orders_this = 1'b0;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      pending_posted     <= '0;
      pending_nonposted  <= '0;
      pending_completion <= '0;
      c_order_blocks     <= '0;
    end else begin
      if (xact_issue && may_proceed) begin
        case (xact_kind)
          2'(XACT_POSTED):     pending_posted     <= pending_posted + 16'd1;
          2'(XACT_NONPOSTED):  pending_nonposted  <= pending_nonposted + 16'd1;
          default:             pending_completion <= pending_completion + 16'd1;
        endcase
      end
      if (xact_retire) begin
        case (retire_kind)
          2'(XACT_POSTED):
            if (pending_posted != 0)     pending_posted <= pending_posted - 16'd1;
          2'(XACT_NONPOSTED):
            if (pending_nonposted != 0)  pending_nonposted <= pending_nonposted - 16'd1;
          default:
            if (pending_completion != 0) pending_completion <= pending_completion - 16'd1;
        endcase
      end
      if (xact_issue && blocked_by_posted)
        c_order_blocks <= c_order_blocks + 32'd1;
    end
  end
endmodule

// ---------------------------------------------------------------------
// eth_pcie_bridge -- one received frame becomes a sequence of posted
// writes and one descriptor write-back, and the module reports what
// the conversion cost.
//
// The output that matters is frame_complete_ethernet against
// frame_complete_pcie: the two protocols disagree about when this
// frame is done, and Section 12 is about the disagreement.
// ---------------------------------------------------------------------
module eth_pcie_bridge
  import pciecmp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        frame_start,
  input  logic        frame_end,
  input  logic [15:0] frame_octets,
  input  logic [63:0] descriptor_addr,
  input  logic        descriptor_valid,

  input  logic        tlp_accepted,      // the PCIe side took one
  input  logic        writeback_acked,   // the descriptor write landed

  output logic        tlp_request,
  output logic  [1:0] tlp_kind,
  output logic [63:0] tlp_addr,
  output logic [15:0] tlp_octets,
  output logic [15:0] tlps_for_frame,
  output logic [15:0] payload_tlps,
  output logic [15:0] overhead_tlps,
  output logic [15:0] overhead_share_pct,
  output logic        frame_complete_ethernet,
  output logic        frame_complete_pcie,
  output logic        completions_disagree,
  output logic [31:0] c_frames_bridged,
  output logic [31:0] c_tlps_issued
);
  logic [15:0] tlps_sent;
  logic [63:0] cursor;
  logic        in_frame;

  always_comb begin
    payload_tlps  = (frame_octets + 16'(MAX_PAYLOAD_B) - 16'd1)
                  / 16'(MAX_PAYLOAD_B);
    overhead_tlps = 16'd2;                    // fetch + write-back
    tlps_for_frame = payload_tlps + overhead_tlps;

    overhead_share_pct = (tlps_for_frame == 0) ? 16'd0
                       : (overhead_tlps * 16'd100) / tlps_for_frame;

    tlp_request = in_frame && descriptor_valid
               && (tlps_sent < payload_tlps);
    tlp_kind    = 2'(XACT_POSTED);
    tlp_addr    = cursor;
    tlp_octets  = ((frame_octets - (tlps_sent * 16'(MAX_PAYLOAD_B)))
                   > 16'(MAX_PAYLOAD_B))
                ? 16'(MAX_PAYLOAD_B)
                : (frame_octets - (tlps_sent * 16'(MAX_PAYLOAD_B)));

    // THE two events. On Ethernet the frame is done when its last
    // octet arrived. On PCIe it is done when the far end says so.
    frame_complete_ethernet = frame_end;
    frame_complete_pcie     = writeback_acked;

    // They are never the same cycle, and the gap is a host round trip.
    completions_disagree = frame_complete_ethernet ^ frame_complete_pcie;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tlps_sent <= '0; cursor <= '0; in_frame <= 1'b0;
      c_frames_bridged <= '0; c_tlps_issued <= '0;
    end else begin
      if (frame_start) begin
        in_frame  <= 1'b1;
        tlps_sent <= '0;
        cursor    <= descriptor_addr;
      end
      if (tlp_accepted) begin
        tlps_sent     <= tlps_sent + 16'd1;
        cursor        <= cursor + 64'(MAX_PAYLOAD_B);
        c_tlps_issued <= c_tlps_issued + 32'd1;
      end
      if (writeback_acked) begin
        in_frame         <= 1'b0;
        c_frames_bridged <= c_frames_bridged + 32'd1;
      end
    end
  end
endmodule

// Ethernet. The transfer is complete when the last octet has left,
// and this port knows it without asking anyone.
p_tx_complete_is_local: assert property (@(posedge clk) disable iff (!rst_n)
  last_octet_sent |-> ##1 frame_complete);

// PCIe. Every term translated, the property compiles, and it asserts
// something the original never said.
p_xact_complete_is_local: assert property (@(posedge clk) disable iff (!rst_n)
  tlp_handed_to_link_layer |-> ##1 transaction_complete);

// ---------------------------------------------------------------------
// completion_timer -- the only liveness a requester can claim.
//
// Section 20 establishes that a remote completion is a report rather
// than an observation. The structural consequence is that every
// outstanding read needs a timer, and Ethernet needs none because
// nothing is outstanding.
// ---------------------------------------------------------------------
module completion_timer
  import pciecmp_pkg::*;
#(
  parameter int unsigned TAGS        = 256,
  parameter int unsigned TIMEOUT_US  = 50
)(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        tick_us,

  input  logic        read_issued,
  input  logic  [7:0] issued_tag,
  input  logic        completion_rx,
  input  logic  [7:0] cpl_tag,
  input  logic  [1:0] cpl_status,

  output logic        timeout_fired,
  output logic  [7:0] timeout_tag,
  output logic [15:0] outstanding_now,
  output logic [31:0] timer_flops,
  output logic [31:0] timer_bce,
  output logic [31:0] ethernet_timer_bce,
  output logic [31:0] c_timeouts,
  output logic [31:0] c_unexpected_cpl,
  output logic [31:0] c_error_cpl
);
  logic [15:0] age  [TAGS];
  logic        live [TAGS];

  always_comb begin
    // One age counter per tag, and the counter must span the timeout.
    timer_flops = 32'(TAGS) * 32'd16 + 32'(TAGS);
    timer_bce   = timer_flops * 32'(BCE_PER_FLOP);

    // The comparison. An Ethernet transmitter has nothing to time.
    ethernet_timer_bce = 32'd0;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < TAGS; i++) begin
        age[i] <= '0; live[i] <= 1'b0;
      end
      timeout_fired <= 1'b0; timeout_tag <= '0; outstanding_now <= '0;
      c_timeouts <= '0; c_unexpected_cpl <= '0; c_error_cpl <= '0;
    end else begin
      timeout_fired <= 1'b0;

      if (read_issued) begin
        live[issued_tag] <= 1'b1;
        age[issued_tag]  <= '0;
        outstanding_now  <= outstanding_now + 16'd1;
      end

      if (completion_rx) begin
        // Property 4 of Section 20, as a counter: a completion for a
        // tag nobody requested is evidence about the completer.
        if (!live[cpl_tag]) c_unexpected_cpl <= c_unexpected_cpl + 32'd1;
        else begin
          live[cpl_tag]   <= 1'b0;
          outstanding_now <= outstanding_now - 16'd1;
        end
        if (cpl_status != 2'(CPL_SUCCESSFUL))
          c_error_cpl <= c_error_cpl + 32'd1;
      end

      if (tick_us) begin
        for (int i = 0; i < TAGS; i++) begin
          if (live[i]) begin
            if (age[i] >= 16'(TIMEOUT_US)) begin
              live[i]       <= 1'b0;
              timeout_fired <= 1'b1;
              timeout_tag   <= 8'(i);
              c_timeouts    <= c_timeouts + 32'd1;
            end else begin
              age[i] <= age[i] + 16'd1;
            end
          end
        end
      end
    end
  end
endmodule

// ---------------------------------------------------------------------
// pcie_cmp_telemetry -- what a bridge must report for the two sides to
// be reconcilable after the fact.
//
// The design rule this module follows: every counter that exists on
// one side alone is useless, because the question at a bridge is
// always "where did the difference come from".
// ---------------------------------------------------------------------
module pcie_cmp_telemetry
  import pciecmp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,

  // the Ethernet side
  input  logic        eth_frame_rx,
  input  logic        eth_frame_dropped,
  input  logic [15:0] eth_frame_octets,

  // the PCIe side
  input  logic        tlp_issued,
  input  logic        tlp_credit_stalled,
  input  logic        cpl_received,
  input  logic        cpl_timeout,
  input  logic        cpl_unexpected,

  // the bridge's own
  input  logic        descriptor_starved,

  output logic [47:0] c_eth_frames,
  output logic [47:0] c_eth_dropped,
  output logic [47:0] c_tlps,
  output logic [47:0] c_completions,
  output logic [47:0] c_timeouts_o,
  output logic [47:0] c_unexpected_o,
  output logic [47:0] c_desc_starved,
  output logic [31:0] c_credit_stalls,
  output logic [15:0] tlps_per_frame_x100,
  output logic [15:0] loss_attributable_pct,
  output logic        sides_reconcile
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_eth_frames <= '0; c_eth_dropped <= '0; c_tlps <= '0;
      c_completions <= '0; c_timeouts_o <= '0; c_unexpected_o <= '0;
      c_desc_starved <= '0; c_credit_stalls <= '0;
    end else begin
      if (eth_frame_rx)       c_eth_frames    <= c_eth_frames + 48'd1;
      if (eth_frame_dropped)  c_eth_dropped   <= c_eth_dropped + 48'd1;
      if (tlp_issued)         c_tlps          <= c_tlps + 48'd1;
      if (cpl_received)       c_completions   <= c_completions + 48'd1;
      if (cpl_timeout)        c_timeouts_o    <= c_timeouts_o + 48'd1;
      if (cpl_unexpected)     c_unexpected_o  <= c_unexpected_o + 48'd1;
      if (descriptor_starved) c_desc_starved  <= c_desc_starved + 48'd1;
      if (tlp_credit_stalled) c_credit_stalls <= c_credit_stalls + 32'd1;
    end
  end

  always_comb begin
    // The ratio Section 10 derived, measured rather than assumed.
    tlps_per_frame_x100 = (c_eth_frames == 0) ? 16'd0
                        : 16'((c_tlps * 48'd100) / c_eth_frames);

    // Of the frames that were lost, how many can be attributed to a
    // named cause? Anything below 100% is loss with no reporter.
    loss_attributable_pct = (c_eth_dropped == 0) ? 16'd100
                          : 16'((c_desc_starved * 48'd100) / c_eth_dropped);

    // The two sides agree only if every issued read got an answer.
    sides_reconcile = (c_completions + c_timeouts_o) >= (c_tlps - c_eth_frames);
  end
endmodule

// ---------------------------------------------------------------------
// pcie_cmp_conformance -- the checks that only make sense at the
// boundary, gathered in one place.
//
// Every check here is about a RELATION between the two sides. None of
// them can be written on either side alone, which is the point.
// ---------------------------------------------------------------------
module pcie_cmp_conformance
  import pciecmp_pkg::*;
#(
  parameter int unsigned TAGS = 256
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        eth_frame_end,
  input  logic        pcie_writeback_ack,
  input  logic        read_issued,
  input  logic  [7:0] issued_tag,
  input  logic        tag_live_in,
  input  logic        completion_rx,
  input  logic  [7:0] cpl_tag,
  input  logic        cpl_tag_live,
  input  logic  [1:0] cpl_status,
  input  logic        credits_available,
  input  logic        tlp_transmitted,
  input  logic        frame_dropped,
  input  logic        drop_counted,
  input  logic [15:0] advertised_credits,
  input  logic [15:0] buffer_entries,

  output logic        v_premature_complete,
  output logic        v_tag_reuse,
  output logic        v_orphan_completion,
  output logic        v_credit_overrun,
  output logic        v_overadvertised,
  output logic        v_uncounted_drop,
  output logic  [5:0] violations,
  output logic        conformant
);
  always_comb begin
    // 1. Section 14 prohibition 1 -- the Ethernet completion is not
    //    the PCIe one, so it must not be reported as the transfer.
    v_premature_complete = eth_frame_end && !pcie_writeback_ack;

    // 2. Prohibition 2 -- a tag must be free before it is issued.
    v_tag_reuse = read_issued && tag_live_in;

    // 3. Section 20 property 4 -- a completion for a tag nobody holds.
    v_orphan_completion = completion_rx && !cpl_tag_live;

    // 4. Section 6 -- the gate is checked on every packet.
    v_credit_overrun = tlp_transmitted && !credits_available;

    // 5. Prohibition 3 -- credits may not exceed the buffer behind them.
    v_overadvertised = (advertised_credits > buffer_entries);

    // 6. Prohibition 4 -- a drop with no reporter anywhere.
    v_uncounted_drop = frame_dropped && !drop_counted;

    violations = { v_uncounted_drop, v_overadvertised, v_credit_overrun,
                   v_orphan_completion, v_tag_reuse, v_premature_complete };
    conformant = (violations == 6'b000000);
  end

  // v_premature_complete is a WARNING rather than an error: the two
  // events are legitimately a host round trip apart. It fires only if
  // something downstream treats the Ethernet event as the transfer.
endmodule

// A1. An Ethernet lookup may miss. A PCIe decode may not.
p_ad_eth_may_miss: assert property (@(posedge clk) disable iff (!rst_n)
  (is_ethernet && !lookup_hit) |-> miss_occurred);

// A2. And a decode miss is an error rather than a delivery.
p_ad_pcie_miss_is_error: assert property (@(posedge clk) disable iff (!rst_n)
  (!is_ethernet && !decode_hit) |-> (miss_occurred && miss_is_reported));

// A3. The replication factor is the port count less one, on Ethernet.
p_ad_flood_width: assert property (@(posedge clk) disable iff (!rst_n)
  (is_ethernet && miss_occurred) |-> (copies_on_miss == (ports - 16'd1)));

// A4. And exactly one, on PCIe.
p_ad_one_completion: assert property (@(posedge clk) disable iff (!rst_n)
  (!is_ethernet && miss_occurred) |-> (copies_on_miss == 16'd1));

// A5. lookup_can_miss is the addressing model, not a runtime condition.
p_ad_model_is_static: assert property (@(posedge clk) disable iff (!rst_n)
  $stable(is_ethernet) |-> $stable(lookup_can_miss));

// A6. The area figure follows the model and nothing else.
p_ad_area_follows_model: assert property (@(posedge clk) disable iff (!rst_n)
  is_ethernet |-> (addressing_bce_per_port == 32'(mac_table_bce_per_port())));

// A7. A miss always increments, so the count is never behind.
p_ad_miss_counted: assert property (@(posedge clk) disable iff (!rst_n)
  miss_occurred |=> (c_misses == $past(c_misses) + 32'd1));

// A8. Flooded copies accumulate at the replication factor.
p_ad_copies_accumulate: assert property (@(posedge clk) disable iff (!rst_n)
  miss_occurred |=> (c_flooded_copies ==
                     $past(c_flooded_copies) + 32'($past(copies_on_miss))));

// B1. Little's law, evaluated rather than assumed.
p_rp_littles_law: assert property (@(posedge clk) disable iff (!rst_n)
  (rate_gbps != 0) |-> (bytes_inflight == ((32'(rate_gbps) * 32'(rtt_ns)) / 32'd8)));

// B2. The tag count rounds up, never down.
p_rp_tags_round_up: assert property (@(posedge clk) disable iff (!rst_n)
  (32'(tags_required) * 32'(MAX_PAYLOAD_B)) >= bytes_inflight);

// B3. The reorder buffer dominates the tag table.
p_rp_reorder_dominates: assert property (@(posedge clk) disable iff (!rst_n)
  (bytes_inflight > 32'd1024) |-> (reorder_share_pct >= 16'd80));

// B4. The Ethernet comparison is a constant and stays one.
p_rp_ethernet_zero: assert property (@(posedge clk) disable iff (!rst_n)
  (ethernet_equivalent_bce == 32'd0));

// B5. Outstanding never exceeds the limit the design implements.
p_rp_within_limit: assert property (@(posedge clk) disable iff (!rst_n)
  (outstanding_now <= tag_limit));

// B6. Issue and retire move the count by exactly one.
p_rp_count_moves_by_one: assert property (@(posedge clk) disable iff (!rst_n)
  (read_issued && !completion_rx) |=>
    (outstanding_now == $past(outstanding_now) + 16'd1));

// B7. And a completion with no issue may not decrement below zero.
p_rp_no_underflow: assert property (@(posedge clk) disable iff (!rst_n)
  (completion_rx && ($past(outstanding_now) == 16'd0)) |=>
    (outstanding_now == 16'd0));

// B8. Chapter 21.8 Section 5's ceiling, stated as an implication.
p_rp_ceiling: assert property (@(posedge clk) disable iff (!rst_n)
  tag_limit_binds |-> (achievable_gbps < rate_gbps));

// B9. A tag issued beyond the limit is counted as exhaustion.
p_rp_exhaustion_counted: assert property (@(posedge clk) disable iff (!rst_n)
  (read_issued && (outstanding_now >= tag_limit)) |=>
    (c_tag_exhausted == $past(c_tag_exhausted) + 32'd1));

// B10. The return path's total is the sum of its two parts and nothing more.
p_rp_total_is_sum: assert property (@(posedge clk) disable iff (!rst_n)
  (return_path_bce_o == tag_table_bce + reorder_bce));

// C1. At reset nothing may be transmitted.
p_cr_reset_forbids: assert property (@(posedge clk)
  $rose(rst_n) |-> !may_transmit);

// C2. A packet is sent only with credit for it.
p_cr_gate_honoured: assert property (@(posedge clk) disable iff (!rst_n)
  (tlp_sent && !may_transmit) |-> stalled_on_credit);

// C3. Consumed never passes limit.
p_cr_never_overrun: assert property (@(posedge clk) disable iff (!rst_n)
  (hdr_consumed[0] <= hdr_limit[0]) &&
  (hdr_consumed[1] <= hdr_limit[1]) &&
  (hdr_consumed[2] <= hdr_limit[2]));

// C4. A credit return raises the limit and nothing else.
p_cr_return_raises_limit: assert property (@(posedge clk) disable iff (!rst_n)
  (credit_return && (ret_type == 2'd0)) |=>
    (hdr_limit[0] == $past(hdr_limit[0]) + 8'd1));

// C5. The obligation is the bandwidth-delay product, times the VCs.
p_cr_obligation: assert property (@(posedge clk) disable iff (!rst_n)
  !per_vc_guaranteed |->
    (buffer_obligation_bce ==
     32'(bytes_in_flight(int'(rate_gbps), int'(rtt_ns))) * 32'd8));

// C6. And it is always larger than the counters that account for it.
p_cr_buffer_exceeds_counters: assert property (@(posedge clk) disable iff (!rst_n)
  (rate_gbps >= 16'd100) |-> (buffer_obligation_bce > credit_bce_o));

// C7. A stall is counted on the cycle it occurs.
p_cr_stall_counted: assert property (@(posedge clk) disable iff (!rst_n)
  stalled_on_credit |=>
    (c_credit_stall_cycles == $past(c_credit_stall_cycles) + 32'd1));

// C8. The flop figure is a function of the parameters, not of traffic.
p_cr_flops_static: assert property (@(posedge clk) disable iff (!rst_n)
  (credit_flops_o == 32'(credit_flops_per_port())));

// C9. Eight guaranteed VCs is eight times one.
p_cr_vc_scaling: assert property (@(posedge clk) disable iff (!rst_n)
  (per_vc_guaranteed && (VCS == 8)) |->
    (buffer_obligation_bce ==
     32'd8 * 32'(bytes_in_flight(int'(rate_gbps), int'(rtt_ns))) * 32'd8));

// D1. A completion may not pass a pending posted write.
p_or_cpl_blocked: assert property (@(posedge clk) disable iff (!rst_n)
  (xact_issue && (xact_kind == 2'(XACT_COMPLETION)) && (pending_posted != 0))
    |-> !may_proceed);

// D2. A non-posted read is never blocked by a posted write.
p_or_np_not_blocked: assert property (@(posedge clk) disable iff (!rst_n)
  (xact_issue && (xact_kind == 2'(XACT_NONPOSTED))) |-> may_proceed);

// D3. Ethernet orders nothing, and the model says so.
p_or_ethernet_none: assert property (@(posedge clk) disable iff (!rst_n)
  (ethernet_orders_this == 1'b0));

// D4. The counter form costs three counters, always.
p_or_counter_cost: assert property (@(posedge clk) disable iff (!rst_n)
  (counter_flops == 32'd24));

// D5. And the pairwise form is quadratic in the outstanding count.
p_or_pairwise_quadratic: assert property (@(posedge clk) disable iff (!rst_n)
  (outstanding_max >= 16'd2) |->
    (pairwise_comparisons ==
     ((32'(outstanding_max) * (32'(outstanding_max) - 32'd1)) / 32'd2)));

// D6. Issue increments exactly one class.
p_or_one_class: assert property (@(posedge clk) disable iff (!rst_n)
  (xact_issue && may_proceed && (xact_kind == 2'(XACT_POSTED))) |=>
    (pending_posted == $past(pending_posted) + 16'd1));

// D7. No pending count goes negative.
p_or_no_underflow: assert property (@(posedge clk) disable iff (!rst_n)
  (pending_posted >= 16'd0) && (pending_nonposted >= 16'd0) &&
  (pending_completion >= 16'd0));

// D8. A block is counted.
p_or_block_counted: assert property (@(posedge clk) disable iff (!rst_n)
  (xact_issue && blocked_by_posted) |=>
    (c_order_blocks == $past(c_order_blocks) + 32'd1));

// E1. The payload TLP count rounds up.
p_br_tlps_round_up: assert property (@(posedge clk) disable iff (!rst_n)
  (payload_tlps * 16'(MAX_PAYLOAD_B)) >= frame_octets);

// E2. Overhead is two transactions per frame, whatever the size.
p_br_overhead_constant: assert property (@(posedge clk) disable iff (!rst_n)
  (overhead_tlps == 16'd2));

// E3. So the overhead share falls as the frame grows.
p_br_share_falls: assert property (@(posedge clk) disable iff (!rst_n)
  (frame_octets > 16'd1500) |-> (overhead_share_pct <= 16'd25));

// E4. A TLP is requested only inside a frame with a descriptor.
p_br_needs_descriptor: assert property (@(posedge clk) disable iff (!rst_n)
  tlp_request |-> descriptor_valid);

// E5. The cursor advances by the payload size on every acceptance.
p_br_cursor_advances: assert property (@(posedge clk) disable iff (!rst_n)
  tlp_accepted |=> (tlp_addr == $past(tlp_addr) + 64'(MAX_PAYLOAD_B)));

// E6. The last TLP of a frame is the remainder, not a full payload.
p_br_last_is_remainder: assert property (@(posedge clk) disable iff (!rst_n)
  (tlp_request && (tlps_for_frame - overhead_tlps == payload_tlps) &&
   (frame_octets % 16'(MAX_PAYLOAD_B) != 0)) |->
    (tlp_octets <= 16'(MAX_PAYLOAD_B)));

// E7. The two completions are never the same event.
p_br_completions_differ: assert property (@(posedge clk) disable iff (!rst_n)
  (frame_complete_ethernet && frame_complete_pcie) |-> !completions_disagree);

// E8. A frame is counted only when the PCIe side finished.
p_br_count_on_pcie: assert property (@(posedge clk) disable iff (!rst_n)
  writeback_acked |=> (c_frames_bridged == $past(c_frames_bridged) + 32'd1));

// E9. Every accepted TLP is counted.
p_br_tlps_counted: assert property (@(posedge clk) disable iff (!rst_n)
  tlp_accepted |=> (c_tlps_issued == $past(c_tlps_issued) + 32'd1));

// E10. Section 14 prohibition 1, as a bound rather than a prohibition:
//      the gap between the two completions is at most a timeout.
p_br_gap_bounded: assert property (@(posedge clk) disable iff (!rst_n)
  frame_complete_ethernet |-> ##[1:CPL_TIMEOUT_CYCLES]
    (frame_complete_pcie || cpl_timeout));