Hardware Timestamping at the MAC/PHY Boundary

// -----------------------------------------------------------------------
// tsu_pkg -- shared types for the timestamp unit.
// -----------------------------------------------------------------------
package tsu_pkg;

  localparam int SEC_W = 48;
  localparam int NS_W  = 32;

  typedef struct packed {
    logic [SEC_W-1:0] sec;
    logic [NS_W-1:0]  ns;
  } ts_t;

  // The PTP originTimestamp wire format: 6 octets of seconds then 4
  // of nanoseconds. 80 bits, and the width of every patch in this
  // chapter.
  localparam int OTS_BITS = 80;
  typedef logic [OTS_BITS-1:0] ots_t;

  function automatic ots_t to_wire(input ts_t t);
    to_wire = {t.sec, t.ns};
  endfunction

  // Where the interesting fields sit, as offsets from the first octet
  // of the PTP header. 16.2 section 3's layout.
  localparam int OFF_CORRECTION = 8;    // 8 octets
  localparam int OFF_ORIGIN_TS  = 34;   // 10 octets

  // A transmit timestamp is meaningless without knowing which frame it
  // belongs to. 16.1 section 12's simplification, fixed here.
  typedef struct packed {
    logic        valid;
    logic [15:0] frame_tag;    // assigned by the transmit scheduler
    ts_t         ts;
  } tx_ts_entry_t;

endpackage

// -----------------------------------------------------------------------
// tsu_capture_point -- captures the free-running clock at the SFD, on
// receive and on transmit, for EVENT messages only.
//
// The classification is one bit -- 16.2 section 4: message types 0x0
// to 0x3 are event messages and the top bit of messageType is clear.
// Everything else needs no timestamp and must not consume a FIFO slot.
// -----------------------------------------------------------------------
module tsu_capture_point
  import tsu_pkg::*;
(
  input  logic       clk,               // the MAC clock for this direction
  input  logic       rst_n,

  input  logic       sfd,               // 4.2's reconciliation sublayer
  input  logic [3:0] sfd_lane,          // which lane of the word -- 16.1 section 12
  input  ts_t        now,

  // Late classification: the message type is not known at the SFD.
  // The timestamp is captured UNCONDITIONALLY and discarded if the
  // frame turns out not to need it.
  input  logic       class_valid,
  input  logic       class_is_event,
  input  logic [15:0] class_frame_tag,

  // Fixed, characterised corrections for everything below this point.
  input  logic [15:0] cfg_phy_delay_ns,
  input  logic [15:0] cfg_lane_ps,

  output logic       ts_valid,
  output ts_t        ts_out,
  output logic [15:0] ts_frame_tag,
  output logic [31:0] c_captured,
  output logic [31:0] c_discarded,
  output logic       overrun
);

  ts_t  held;
  logic held_valid;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      held <= '0; held_valid <= 1'b0;
      ts_valid <= 1'b0; ts_out <= '0; ts_frame_tag <= '0;
      c_captured <= '0; c_discarded <= '0; overrun <= 1'b0;
    end else begin
      ts_valid <= 1'b0;

      // The capture is unconditional and one cycle. 16.1 section 19's
      // p_capture_latency_is_fixed: a VARIABLE capture latency
      // reintroduces exactly the jitter this whole module removes.
      if (sfd) begin
        if (held_valid) overrun <= 1'b1;
        held <= '{ sec: now.sec,
                   ns:  now.ns
                        - NS_W'(cfg_phy_delay_ns)
                        - NS_W'((32'(cfg_lane_ps) * 32'(sfd_lane)) / 1000) };
        held_valid <= 1'b1;
      end

      // Classification arrives later, once the header has been parsed.
      // An event message keeps its timestamp; anything else frees it.
      if (class_valid && held_valid) begin
        held_valid <= 1'b0;
        if (class_is_event) begin
          ts_valid     <= 1'b1;
          ts_out       <= held;
          ts_frame_tag <= class_frame_tag;
          c_captured   <= c_captured + 1;
        end else begin
          c_discarded <= c_discarded + 1;
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// twostep_reporter -- takes a transmit timestamp from the FIFO and
// builds the Follow_Up that carries it.
//
// The Sync's own originTimestamp field is transmitted as ZERO and the
// twoStepFlag is set, so a conformant slave knows to wait. 16.2
// section 5's parked t2 is the other end of this.
// -----------------------------------------------------------------------
module twostep_reporter
  import tsu_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  // A Sync has been transmitted and its timestamp has come back.
  input  logic        tx_ts_valid,
  input  logic [15:0] tx_ts_tag,
  input  ts_t         tx_ts,

  // The scheduler's record of which tag was which Sync.
  input  logic [15:0] pending_tag,
  input  logic [15:0] pending_seq,
  input  logic        pending_valid,

  input  logic        tx_ready,

  output logic        fu_request,
  output logic [15:0] fu_seq,
  output ots_t        fu_precise_origin,
  output logic [31:0] c_followups,
  output logic [31:0] c_orphan_ts,     // a timestamp with no pending Sync
  output logic [31:0] latency_cycles   // capture to Follow_Up transmitted
);

  logic [31:0] age;
  logic        armed;
  logic [15:0] armed_seq;
  ots_t        armed_ts;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      armed <= 1'b0; age <= '0;
      fu_request <= 1'b0; fu_seq <= '0; fu_precise_origin <= '0;
      c_followups <= '0; c_orphan_ts <= '0; latency_cycles <= '0;
      armed_seq <= '0; armed_ts <= '0;
    end else begin
      fu_request <= 1'b0;

      if (tx_ts_valid) begin
        if (pending_valid && (pending_tag == tx_ts_tag)) begin
          armed     <= 1'b1;
          armed_seq <= pending_seq;
          armed_ts  <= to_wire(tx_ts);
          age       <= '0;
        end else begin
          // A transmit timestamp whose frame nobody is waiting for.
          // Section 13: without tags this case is undetectable and
          // the timestamp is attributed to the wrong frame.
          c_orphan_ts <= c_orphan_ts + 1;
        end
      end

      if (armed) begin
        age <= age + 1;
        if (tx_ready) begin
          fu_request        <= 1'b1;
          fu_seq            <= armed_seq;
          fu_precise_origin <= armed_ts;
          armed             <= 1'b0;
          c_followups       <= c_followups + 1;
          latency_cycles    <= age;
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// onestep_field_rewriter -- substitutes the captured transmit timestamp
// into the outgoing frame's originTimestamp field as it streams past.
//
// The datapath is W octets wide. The field is 10 octets at a known
// offset, so it may span one or two beats. Both cases must be handled
// and the two-beat case is the one that is usually wrong.
// -----------------------------------------------------------------------
module onestep_field_rewriter
  import tsu_pkg::*;
#(
  parameter int W = 8                      // octets per beat
)(
  input  logic              clk,
  input  logic              rst_n,

  // The outgoing stream, before substitution.
  input  logic              in_valid,
  input  logic [W*8-1:0]    in_data,
  input  logic              in_sop,
  input  logic              in_eop,
  input  logic [$clog2(W+1)-1:0] in_bytes,   // valid octets on eop

  // Which frame this is and where its field sits.
  input  logic              frame_is_onestep_sync,
  input  logic [15:0]       field_offset,      // octets from frame start
  input  ots_t              new_ts,            // to_wire(captured t1)

  output logic              out_valid,
  output logic [W*8-1:0]    out_data,
  output logic              out_sop,
  output logic              out_eop,
  output logic [$clog2(W+1)-1:0] out_bytes,

  // The delta the FCS patch needs: old XOR new, positioned.
  output logic              delta_valid,
  output ots_t              delta_bits,
  output logic [15:0]       delta_offset,
  output logic [31:0]       c_rewritten,
  output logic [31:0]       c_split_across_beats
);

  logic [15:0] octet_ctr;
  ots_t        old_captured;
  logic [$clog2(OTS_BITS+1)-1:0] captured_bits;

  // For each octet lane in this beat, is it inside the field?
  logic [W-1:0]      lane_in_field;
  logic [W-1:0][7:0] lane_new;
  logic [W-1:0][7:0] lane_old;

  always_comb begin
    int L, pos;
    for (L = 0; L < W; L++) begin
      pos = int'(octet_ctr) + L;
      lane_in_field[L] = frame_is_onestep_sync &&
                         (pos >= int'(field_offset)) &&
                         (pos <  int'(field_offset) + 10);
      lane_old[L] = in_data[8*L +: 8];
      // Octet (pos - field_offset) of the 10-octet field, MSB first.
      lane_new[L] = lane_in_field[L]
                  ? new_ts[OTS_BITS - 8*(pos - int'(field_offset)) - 1 -: 8]
                  : in_data[8*L +: 8];
    end
  end

  always_ff @(posedge clk or negedge rst_n) begin
    int L;
    if (!rst_n) begin
      octet_ctr <= '0; out_valid <= 1'b0; out_data <= '0;
      out_sop <= 1'b0; out_eop <= 1'b0; out_bytes <= '0;
      delta_valid <= 1'b0; delta_bits <= '0; delta_offset <= '0;
      old_captured <= '0; captured_bits <= '0;
      c_rewritten <= '0; c_split_across_beats <= '0;
    end else begin
      out_valid   <= in_valid;
      out_sop     <= in_sop;
      out_eop     <= in_eop;
      out_bytes   <= in_bytes;
      delta_valid <= 1'b0;

      if (in_valid) begin
        // Substitute.
        for (L = 0; L < W; L++) out_data[8*L +: 8] <= lane_new[L];

        // Accumulate the OLD field content, which the FCS patch needs.
        for (L = 0; L < W; L++) begin
          if (lane_in_field[L]) begin
            automatic int k;
            k = int'(octet_ctr) + L - int'(field_offset);
            old_captured[OTS_BITS - 8*k - 1 -: 8] <= lane_old[L];
            captured_bits <= captured_bits + 8;
          end
        end

        octet_ctr <= in_sop ? 16'(W) : (octet_ctr + 16'(W));

        // Once the whole field has passed, the delta is complete and
        // the patch can be computed. On a wide datapath this is the
        // SAME beat the FCS is in -- section 8's callout.
        if (frame_is_onestep_sync &&
            ((int'(octet_ctr) + W) >= (int'(field_offset) + 10)) &&
            ((int'(octet_ctr))     <  (int'(field_offset) + 10))) begin
          delta_valid  <= 1'b1;
          delta_offset <= field_offset;
          c_rewritten  <= c_rewritten + 1;
          if (int'(octet_ctr) <= int'(field_offset))
            ; // the field fitted in one beat
          else
            c_split_across_beats <= c_split_across_beats + 1;
        end

        if (in_eop) begin
          octet_ctr     <= '0;
          captured_bits <= '0;
        end
      end
    end
  end

  // delta = old XOR new, which is zero outside the field by
  // construction. This is the only nonzero input the patch needs.
  always_comb delta_bits = old_captured ^ new_ts;

endmodule

// -----------------------------------------------------------------------
// fcs_patcher -- corrects the frame check sequence after octets were
// substituted, WITHOUT recomputing it from the frame.
//
// CRC-32 is linear over GF(2):   CRC(A xor B) = CRC(A) xor CRC(B).
// So if the frame changed by `delta` at a known position, the new FCS
// is the old FCS xor CRC(delta placed at that position) -- and that is
// a FIXED linear map from 80 delta bits to 32 FCS bits.
//
// No frame buffer. No full CRC engine. One matrix multiply.
// -----------------------------------------------------------------------
module fcs_patcher
  import tsu_pkg::*;
#(
  // Distance in octets from the END of the substituted field to the
  // start of the FCS. For a 64-octet Sync with the field at 48..57
  // and the FCS at 60..63, this is 2.
  parameter int TRAILING_OCTETS = 2
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        delta_valid,
  input  ots_t        delta_bits,        // old XOR new, 80 bits

  input  logic        fcs_valid,
  input  logic [31:0] fcs_in,

  output logic        fcs_out_valid,
  output logic [31:0] fcs_out,
  output logic [31:0] c_patched,
  output logic        patch_without_delta   // an FCS arrived unpatched
);

  // The GF(2) matrix. Row j of PATCH_M is the set of delta bits whose
  // parity forms bit j of the CRC contribution. It depends only on the
  // polynomial and on TRAILING_OCTETS, so it is a compile-time
  // constant -- generated the same way 6.4's parallel CRC tables are.
  //
  // Shown symbolically: a real design emits the 32 x 80 bit pattern
  // from a script, exactly as chapter 6.4 emits its per-width tables.
  function automatic logic [31:0] crc32_of_positioned_delta(input ots_t d);
    logic [31:0] r;
    int i;
    begin
      // Feed the delta through the CRC shift register, then advance
      // TRAILING_OCTETS zero octets to position it. Written serially
      // for clarity; synthesis unrolls it into the matrix above.
      r = 32'h0000_0000;                    // a DELTA has no init value
      for (i = OTS_BITS-1; i >= 0; i--) begin
        if (r[31] ^ d[i]) r = {r[30:0], 1'b0} ^ 32'h04C1_1DB7;
        else              r = {r[30:0], 1'b0};
      end
      for (i = 0; i < TRAILING_OCTETS*8; i++) begin
        if (r[31]) r = {r[30:0], 1'b0} ^ 32'h04C1_1DB7;
        else       r = {r[30:0], 1'b0};
      end
      crc32_of_positioned_delta = r;
    end
  endfunction

  logic [31:0] held_patch;
  logic        have_patch;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      held_patch <= '0; have_patch <= 1'b0;
      fcs_out_valid <= 1'b0; fcs_out <= '0;
      c_patched <= '0; patch_without_delta <= 1'b0;
    end else begin
      fcs_out_valid       <= 1'b0;
      patch_without_delta <= 1'b0;

      if (delta_valid) begin
        // A zero delta means the field already held the right value --
        // possible, and the patch is then the identity.
        held_patch <= crc32_of_positioned_delta(delta_bits);
        have_patch <= 1'b1;
      end

      if (fcs_valid) begin
        fcs_out_valid <= 1'b1;
        if (have_patch) begin
          fcs_out    <= fcs_in ^ held_patch;
          have_patch <= 1'b0;
          c_patched  <= c_patched + 1;
        end else begin
          // No substitution happened: pass the FCS through unchanged.
          fcs_out <= fcs_in;
        end
      end

      // A one-step Sync whose FCS arrived with no delta computed is a
      // frame that will be discarded by every receiver -- 6.3's
      // residue check. It must be counted, loudly.
      if (fcs_valid && !have_patch && delta_expected)
        patch_without_delta <= 1'b1;
    end
  end

endmodule

// -----------------------------------------------------------------------
// correction_field_updater -- adds a value to the 8-octet
// correctionField as a frame streams past, and patches the FCS.
//
// This is section 7's rewriter and section 8's patcher applied to a
// different offset and a different width. The VALUE added is 16.4
// section 12's residence time; this module is the mechanism.
//
// correctionField is signed 16.16 fixed point: nanoseconds in the
// upper 48 bits, fractional nanoseconds in the lower 16.
// -----------------------------------------------------------------------
module correction_field_updater
  import tsu_pkg::*;
#(
  parameter int W = 8
)(
  input  logic              clk,
  input  logic              rst_n,

  input  logic              in_valid,
  input  logic [W*8-1:0]    in_data,
  input  logic              in_sop,
  input  logic              in_eop,

  input  logic              frame_is_ptp_event,
  input  logic [15:0]       correction_offset,     // octets from frame start
  input  logic signed [63:0] add_value,            // 16.16 fixed point

  output logic              out_valid,
  output logic [W*8-1:0]    out_data,
  output logic              out_sop,
  output logic              out_eop,

  output logic              delta_valid,
  output logic [63:0]       delta_bits,
  output logic              overflow,              // the field saturated
  output logic [31:0]       c_updated,
  output logic [31:0]       c_overflow
);

  logic [15:0]  octet_ctr;
  logic [63:0]  old_field, new_field;
  logic [W-1:0] lane_in_field;

  always_comb begin
    int L, pos;
    for (L = 0; L < W; L++) begin
      pos = int'(octet_ctr) + L;
      lane_in_field[L] = frame_is_ptp_event &&
                         (pos >= int'(correction_offset)) &&
                         (pos <  int'(correction_offset) + 8);
    end
  end

  // The added value is signed and the field is signed, so the sum can
  // overflow in either direction. Saturating is wrong -- it produces a
  // plausible number -- so the design must SAY it overflowed.
  logic signed [64:0] sum_ext;
  always_comb begin
    sum_ext   = $signed({old_field[63], old_field}) + $signed({add_value[63], add_value});
    new_field = sum_ext[63:0];
  end

  always_ff @(posedge clk or negedge rst_n) begin
    int L;
    if (!rst_n) begin
      octet_ctr <= '0; old_field <= '0;
      out_valid <= 1'b0; out_data <= '0;
      out_sop <= 1'b0; out_eop <= 1'b0;
      delta_valid <= 1'b0; delta_bits <= '0;
      overflow <= 1'b0; c_updated <= '0; c_overflow <= '0;
    end else begin
      out_valid   <= in_valid;
      out_sop     <= in_sop;
      out_eop     <= in_eop;
      delta_valid <= 1'b0;
      overflow    <= 1'b0;

      if (in_valid) begin
        for (L = 0; L < W; L++) begin
          automatic int pos, k;
          pos = int'(octet_ctr) + L;
          k   = pos - int'(correction_offset);
          if (lane_in_field[L]) begin
            old_field[63 - 8*k -: 8] <= in_data[8*L +: 8];
            out_data[8*L +: 8]       <= new_field[63 - 8*k -: 8];
          end else begin
            out_data[8*L +: 8]       <= in_data[8*L +: 8];
          end
        end

        octet_ctr <= in_sop ? 16'(W) : (octet_ctr + 16'(W));

        if (frame_is_ptp_event &&
            ((int'(octet_ctr) + W) >= (int'(correction_offset) + 8)) &&
            ((int'(octet_ctr))     <  (int'(correction_offset) + 8))) begin
          delta_valid <= 1'b1;
          delta_bits  <= old_field ^ new_field;
          c_updated   <= c_updated + 1;
          // Sign-extension mismatch between the 65-bit sum and the
          // 64-bit field means the correction no longer fits.
          if (sum_ext[64] != sum_ext[63]) begin
            overflow   <= 1'b1;
            c_overflow <= c_overflow + 1;
          end
        end

        if (in_eop) octet_ctr <= '0;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// tx_timestamp_fifo -- holds transmit timestamps with their frame tags
// until the protocol layer collects them.
//
// 16.1 section 12's simplification was a single capture register with
// no tag. This module fixes both halves: a queue, so a burst does not
// lose entries, and a tag, so an entry cannot be attributed to the
// wrong frame.
// -----------------------------------------------------------------------
module tx_timestamp_fifo
  import tsu_pkg::*;
#(
  parameter int DEPTH = 8
)(
  input  logic        clk,
  input  logic        rst_n,

  // From the capture point.
  input  logic        push,
  input  logic [15:0] push_tag,
  input  ts_t         push_ts,

  // The protocol layer asks for a specific tag rather than taking the
  // head. A burst can complete out of order and order is not the
  // property that matters -- identity is.
  input  logic        lookup_valid,
  input  logic [15:0] lookup_tag,

  output logic        hit,
  output ts_t         hit_ts,

  output logic [$clog2(DEPTH+1)-1:0] occupancy,
  output logic        full,
  output logic [31:0] c_pushed,
  output logic [31:0] c_dropped,      // pushed while full
  output logic [31:0] c_evicted,      // aged out unclaimed
  output logic [31:0] c_miss          // looked up and not present
);

  tx_ts_entry_t e [DEPTH];
  logic [15:0]  age [DEPTH];
  logic [$clog2(DEPTH+1)-1:0] occ;

  // Any entry nobody claims must eventually leave, or a single
  // abandoned frame permanently consumes a slot.
  localparam int MAX_AGE = 16'hF000;

  always_ff @(posedge clk or negedge rst_n) begin
    int i;
    automatic bit placed;
    if (!rst_n) begin
      for (i = 0; i < DEPTH; i++) begin e[i] <= '0; age[i] <= '0; end
      occ <= '0; hit <= 1'b0; hit_ts <= '0;
      c_pushed <= '0; c_dropped <= '0; c_evicted <= '0; c_miss <= '0;
    end else begin
      hit <= 1'b0;

      for (i = 0; i < DEPTH; i++) begin
        if (e[i].valid) begin
          age[i] <= age[i] + 1'b1;
          if (age[i] == 16'(MAX_AGE)) begin
            e[i].valid <= 1'b0;
            occ        <= occ - 1'b1;
            c_evicted  <= c_evicted + 1;
          end
        end
      end

      if (push) begin
        placed = 1'b0;
        for (i = 0; i < DEPTH; i++) begin
          if (!e[i].valid && !placed) begin
            placed      = 1'b1;
            e[i].valid  <= 1'b1;
            e[i].frame_tag <= push_tag;
            e[i].ts     <= push_ts;
            age[i]      <= '0;
            occ         <= occ + 1'b1;
            c_pushed    <= c_pushed + 1;
          end
        end
        // Dropping the NEWEST is the right policy: an old entry may
        // still be claimed, and a dropped new one is detectable at
        // the protocol layer as a missing timestamp for a known frame.
        if (!placed) c_dropped <= c_dropped + 1;
      end

      if (lookup_valid) begin
        automatic bit found;
        found = 1'b0;
        for (i = 0; i < DEPTH; i++) begin
          if (e[i].valid && (e[i].frame_tag == lookup_tag)) begin
            found      = 1'b1;
            hit        <= 1'b1;
            hit_ts     <= e[i].ts;
            e[i].valid <= 1'b0;
            occ        <= occ - 1'b1;
          end
        end
        if (!found) c_miss <= c_miss + 1;
      end
    end
  end

  assign occupancy = occ;
  assign full      = (occ == DEPTH);

endmodule

// -----------------------------------------------------------------------
// tsu_telemetry -- what an operator or an integrator needs to decide
// whether a timestamp unit is behaving, without a reference clock.
//
// Every quantity here is derived from the unit's own behaviour.
// 16.1 section 19 established that accuracy cannot be among them.
// -----------------------------------------------------------------------
module tsu_telemetry
  import tsu_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        capture,
  input  logic        classify,
  input  logic        ts_published,
  input  logic        overrun,
  input  logic [31:0] c_patched,
  input  logic [31:0] c_rewritten,
  input  logic [31:0] c_dropped,
  input  logic [31:0] c_miss,
  input  logic [31:0] c_evicted,
  input  logic [$clog2(9)-1:0] fifo_occupancy,
  input  logic        window_tick,

  output logic [15:0] capture_to_classify_cycles,
  output logic [15:0] worst_capture_to_classify,
  output logic [15:0] peak_occupancy,
  output logic [15:0] patch_ratio_x100,     // patched / rewritten
  output logic        pairing_is_sound,
  output logic        unit_is_keeping_up,
  output logic [31:0] c_windows
);

  logic [15:0] lat;
  logic        timing;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      lat <= '0; timing <= 1'b0;
      capture_to_classify_cycles <= '0;
      worst_capture_to_classify <= '0;
      peak_occupancy <= '0; patch_ratio_x100 <= '0;
      pairing_is_sound <= 1'b0; unit_is_keeping_up <= 1'b0;
      c_windows <= '0;
    end else begin
      // The interval between capturing and classifying sets the FIFO
      // depth the unit needs. It is a pipeline property and nobody
      // measures it, so the depth is usually a guess.
      if (capture) begin timing <= 1'b1; lat <= '0; end
      else if (timing) begin
        lat <= lat + 1'b1;
        if (classify) begin
          timing <= 1'b0;
          capture_to_classify_cycles <= lat;
          if (lat > worst_capture_to_classify)
            worst_capture_to_classify <= lat;
        end
      end

      if (16'(fifo_occupancy) > peak_occupancy)
        peak_occupancy <= 16'(fifo_occupancy);

      if (window_tick) begin
        // Every rewritten frame must have been patched. A ratio other
        // than 100 means frames left with a stale FCS and every
        // receiver discarded them -- 6.3's residue check.
        patch_ratio_x100 <= (c_rewritten == 0) ? 16'd100
                          : 16'((c_patched * 100) / c_rewritten);

        // Pairing is sound if nothing was dropped, evicted or missed.
        // Any of the three means a timestamp and a frame may have
        // been mismatched -- section 13.
        pairing_is_sound <= (c_dropped == '0) && (c_evicted == '0) &&
                            (c_miss == '0);

        // The unit keeps up if the queue never approached full and
        // no capture was overwritten.
        unit_is_keeping_up <= (peak_occupancy < 16'd7) && !overrun;

        c_windows <= c_windows + 1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// tsu_conformance_monitor -- one bit.
//
// It asserts: fixed capture latency, correct classification, complete
// patching, sound pairing, and a characterised configuration. 16.1
// section 19 established why accuracy is not on the list and section
// 19 here refuses a different property for a different reason.
// -----------------------------------------------------------------------
module tsu_conformance_monitor
  import tsu_pkg::*;
(
  input  logic       clk,
  input  logic       rst_n,

  input  logic       variable_capture_latency,
  input  logic       rewrote_a_general_message,
  input  logic       rewrote_a_twostep_sync,
  input  logic       patch_without_delta,
  input  logic       correction_overflow,
  input  logic       pairing_unsound,
  input  logic       cfg_phy_delay_unset,
  input  logic       cfg_phy_delay_stale,     // the link mode changed
  input  logic       cfg_lane_in_ns,          // truncates to zero

  output logic       conformant,
  output logic [15:0] fault_vector,
  output logic [31:0] c_violations
);

  logic v_lat, v_gen, v_two, v_patch, v_ovf, v_pair;
  logic v_unset, v_stale, v_lane;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_lat <= 1'b0; v_gen <= 1'b0; v_two <= 1'b0;
      v_patch <= 1'b0; v_ovf <= 1'b0; v_pair <= 1'b0;
      v_unset <= 1'b0; v_stale <= 1'b0; v_lane <= 1'b0;
      c_violations <= '0;
    end else begin
      // A variable capture latency is the one violation that destroys
      // the mechanism rather than degrading it -- it reintroduces
      // exactly the jitter 16.1 removed.
      if (variable_capture_latency) begin v_lat <= 1'b1; c_violations <= c_violations + 1; end
      if (rewrote_a_general_message) begin v_gen <= 1'b1; c_violations <= c_violations + 1; end
      if (rewrote_a_twostep_sync)    begin v_two <= 1'b1; c_violations <= c_violations + 1; end
      if (patch_without_delta)       begin v_patch <= 1'b1; c_violations <= c_violations + 1; end
      if (correction_overflow)       begin v_ovf <= 1'b1; c_violations <= c_violations + 1; end
      if (pairing_unsound)           begin v_pair <= 1'b1; c_violations <= c_violations + 1; end

      // Standing configuration properties. 14.1 section 17's argument:
      // these are wrong from elaboration, not from the first frame.
      v_unset <= cfg_phy_delay_unset;
      v_stale <= cfg_phy_delay_stale;
      v_lane  <= cfg_lane_in_ns;
    end
  end

  assign conformant = !(v_lat || v_gen || v_two || v_patch || v_ovf ||
                        v_pair || v_unset || v_stale || v_lane);
  assign fault_vector = {7'b0, v_lane, v_stale, v_unset, v_pair,
                         v_ovf, v_patch, v_two, v_gen, v_lat};

endmodule

// P1. THE load-bearing property: the capture latency is exactly one
// cycle, always. A variable latency reintroduces the jitter the whole
// of chapter 16.1 was about removing.
property p_capture_latency_is_one;
  @(posedge clk) disable iff (!rst_n)
  sfd |=> held_valid;
endproperty

// P2. And nothing else ever writes the capture register.
property p_no_spurious_capture;
  @(posedge clk) disable iff (!rst_n)
  $changed(held) |-> $past(sfd);
endproperty

// P3. The lane correction is applied in picoseconds, so it does not
// truncate to zero -- 16.1 section 12's simplification, fixed.
property p_lane_correction_nonzero;
  @(posedge clk) disable iff (!rst_n)
  (sfd && (sfd_lane != '0) && (cfg_lane_ps != '0))
    |=> (held.ns != (now.ns - NS_W'(cfg_phy_delay_ns)));
endproperty

// P4. A second SFD before a classification sets overrun.
property p_overrun_flagged;
  @(posedge clk) disable iff (!rst_n)
  (sfd && held_valid) |=> overrun;
endproperty

// P5. Captures are monotonic -- checkable with no reference.
property p_captures_monotonic;
  @(posedge clk) disable iff (!rst_n)
  (ts_valid && $past(ts_valid)) |-> ((ts_out.ns >= $past(ts_out.ns)) ||
                                     (ts_out.sec > $past(ts_out.sec)));
endproperty

// P6. Only event messages publish a timestamp. 16.2 section 4's split.
property p_only_events_publish;
  @(posedge clk) disable iff (!rst_n)
  ts_valid |-> $past(class_is_event);
endproperty

// P7. A general message's capture is discarded, not leaked.
property p_general_discards;
  @(posedge clk) disable iff (!rst_n)
  (class_valid && !class_is_event && held_valid) |=> $changed(c_discarded);
endproperty

// P8. Every capture is eventually resolved -- published or discarded.
property p_every_capture_resolved;
  @(posedge clk) disable iff (!rst_n)
  $rose(held_valid) |-> ##[1:$] !held_valid;
endproperty

// P9. Classification always follows capture, never precedes it.
property p_capture_precedes_classify;
  @(posedge clk) disable iff (!rst_n)
  class_valid |-> $past(held_valid) || overrun;
endproperty

// P10. Only a one-step Sync's originTimestamp is rewritten.
property p_rewrite_only_onestep_sync;
  @(posedge clk) disable iff (!rst_n)
  delta_valid |-> frame_is_onestep_sync;
endproperty

// P11. Octets outside the field pass through unchanged.
property p_outside_field_untouched;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && !lane_in_field[L]) |=> (out_data[8*L +: 8] == $past(in_data[8*L +: 8]));
endproperty

// P12. The substituted content is exactly the captured timestamp in
// wire order -- MSB of seconds first.
property p_substitution_is_the_timestamp;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && lane_in_field[L]) |=>
    (out_data[8*L +: 8] == new_ts[OTS_BITS - 8*k - 1 -: 8]);
endproperty

// P13. The delta is zero outside the field, by construction.
property p_delta_is_confined;
  @(posedge clk) disable iff (!rst_n)
  delta_valid |-> ((delta_bits & ~field_mask) == '0);
endproperty

// P14. A field spanning two beats is handled and counted.
property p_split_field_counted;
  @(posedge clk) disable iff (!rst_n)
  (delta_valid && (octet_ctr > field_offset)) |=> $changed(c_split_across_beats);
endproperty

// P15. Every rewritten frame's FCS is patched. A ratio other than
// 100% means frames left with a stale FCS and every receiver
// discarded them -- 6.3's residue check.
property p_every_rewrite_is_patched;
  @(posedge clk) disable iff (!rst_n)
  delta_valid |-> ##[1:$] (fcs_out_valid && $past(have_patch));
endproperty

// P16. The patch is linear: patching with a zero delta is the
// identity.
property p_zero_delta_is_identity;
  @(posedge clk) disable iff (!rst_n)
  (fcs_valid && have_patch && (held_patch == '0)) |=> (fcs_out == $past(fcs_in));
endproperty

// P17. Linearity, stated directly: the patch for A xor B is the xor
// of the patches. This is the property the whole module rests on.
property p_patch_is_linear;
  @(posedge clk) disable iff (!rst_n)
  (crc32_of_positioned_delta(a ^ b) ==
   (crc32_of_positioned_delta(a) ^ crc32_of_positioned_delta(b)));
endproperty

// P18. The patch uses no initial value and no final complement --
// both cancel in a difference, and including them makes every
// patched frame fail its receiver's check.
property p_no_init_no_complement;
  @(posedge clk) disable iff (!rst_n)
  (crc32_of_positioned_delta('0) == 32'h0000_0000);
endproperty

// P19. The emitted frame's FCS is the correct CRC of the emitted
// frame -- the end-to-end check, on the PHY-side interface.
property p_emitted_frame_is_valid;
  @(posedge clk) disable iff (!rst_n)
  out_eop |-> (emitted_fcs == crc32_of(emitted_frame_body));
endproperty

// P20. An FCS arriving with no patch when one was expected is
// counted, loudly.
property p_missing_patch_flagged;
  @(posedge clk) disable iff (!rst_n)
  (fcs_valid && !have_patch && delta_expected) |=> patch_without_delta;
endproperty

// P21. The correction ACCUMULATES -- it is added, never replaced, so
// an arbitrary number of transparent clocks compose.
property p_correction_accumulates;
  @(posedge clk) disable iff (!rst_n)
  delta_valid |-> (new_field == (old_field + add_value));
endproperty

// P22. Only event messages are updated. A Follow_Up's correction is
// already correct and must not gain this switch's residence time.
property p_correction_only_events;
  @(posedge clk) disable iff (!rst_n)
  delta_valid |-> frame_is_ptp_event;
endproperty

// P23. Overflow is reported, never saturated. A clipped correction is
// a plausible wrong number that section 7 of chapter 16.2 accepts.
property p_overflow_is_reported;
  @(posedge clk) disable iff (!rst_n)
  (sum_ext[64] != sum_ext[63]) |-> overflow;
endproperty

// P24. A lookup returns the entry with that tag, or a miss. It never
// returns a different frame's timestamp.
property p_lookup_is_by_tag;
  @(posedge clk) disable iff (!rst_n)
  hit |-> ($past(e[i].frame_tag) == $past(lookup_tag));
endproperty

// P25. A hit consumes its entry exactly once.
property p_hit_consumes_once;
  @(posedge clk) disable iff (!rst_n)
  hit |=> !e[i].valid;
endproperty

// P26. Overflow drops the NEWEST, so an old entry can still be
// claimed and the loss surfaces as a miss at the protocol layer.
property p_overflow_drops_newest;
  @(posedge clk) disable iff (!rst_n)
  (push && full) |=> ($stable(e) && $changed(c_dropped));
endproperty

// P27. Every entry eventually leaves -- claimed or aged out.
property p_no_permanent_entries;
  @(posedge clk) disable iff (!rst_n)
  $rose(e[i].valid) |-> ##[1:MAX_AGE+1] !e[i].valid;
endproperty

// P28. Occupancy equals the number of valid entries.
property p_occupancy_is_exact;
  @(posedge clk) disable iff (!rst_n)
  occupancy == $countones(entry_valid_vector);
endproperty

// P29. Standing property: the PHY delay is characterised.
property p_phy_delay_characterised;
  @(posedge clk) disable iff (!rst_n)
  !cfg_phy_delay_unset;
endproperty

// P30. And is not stale -- the live link mode matches the mode the
// correction was indexed for. Section 4's operational trap.
property p_phy_delay_is_current;
  @(posedge clk) disable iff (!rst_n)
  !cfg_phy_delay_stale;
endproperty

// P31. The lane term is in picoseconds, not nanoseconds.
property p_lane_units_are_ps;
  @(posedge clk) disable iff (!rst_n)
  !cfg_lane_in_ns;
endproperty

// P32. conformant is exactly the conjunction it claims.
property p_conformant_definition;
  @(posedge clk) disable iff (!rst_n)
  conformant <-> (fault_vector == 16'h0000);
endproperty