The PTP Message Exchange

// -----------------------------------------------------------------------
// ptp_pkg -- shared types for the IEEE 1588 message exchange.
// -----------------------------------------------------------------------
package ptp_pkg;

  localparam logic [15:0] PTP_ETHERTYPE = 16'h88F7;
  // Two reserved multicast groups: one for messages a transparent clock
  // must NOT forward unchanged, one for the rest.
  localparam logic [47:0] PTP_PRIMARY_DA = 48'h01_1B_19_00_00_00;
  localparam logic [47:0] PTP_PDELAY_DA  = 48'h01_80_C2_00_00_0E;

  typedef enum logic [3:0] {
    MSG_SYNC          = 4'h0,
    MSG_DELAY_REQ     = 4'h1,
    MSG_PDELAY_REQ    = 4'h2,
    MSG_PDELAY_RESP   = 4'h3,
    MSG_FOLLOW_UP     = 4'h8,
    MSG_DELAY_RESP    = 4'h9,
    MSG_PDELAY_RESP_FU= 4'hA,
    MSG_ANNOUNCE      = 4'hB,
    MSG_SIGNALING     = 4'hC,
    MSG_MANAGEMENT    = 4'hD
  } msg_type_e;

  // Messages 0x0..0x3 are EVENT messages: they are timestamped on
  // transmit and on receive. Everything else is a GENERAL message and
  // carries no timestamp of its own. The distinction decides which
  // messages 16.3's timestamp unit must act on.
  function automatic bit is_event(input msg_type_e t);
    is_event = (t[3] == 1'b0);
  endfunction

  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;

  // A port's identity: an 8-octet clock identity plus a 2-octet port
  // number. Every message says who sent it, and the pairing in
  // section 9 depends on it.
  typedef struct packed {
    logic [63:0] clock_id;
    logic [15:0] port_num;
  } port_id_t;

  // correctionField is signed nanoseconds in a 16.16 fixed-point form:
  // the low 16 bits are fractional nanoseconds. 16.4's transparent
  // clock accumulates residence time here.
  typedef logic signed [63:0] correction_t;

endpackage

// -----------------------------------------------------------------------
// ptp_header_parser -- recognises a PTP message and extracts the common
// header. It is a filter first and a parser second.
// -----------------------------------------------------------------------
module ptp_header_parser
  import ptp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        rx_valid,
  input  logic [7:0]  rx_octet,
  input  logic        rx_sop,
  input  logic        rx_eop,
  input  logic        rx_fcs_ok,
  input  logic        rx_tagged,      // 13.2's tag shifts every offset

  output logic        hdr_valid,
  output msg_type_e   msg_type,
  output logic        is_event_msg,
  output logic [15:0] msg_length,
  output logic [7:0]  domain,
  output logic [15:0] flags,
  output correction_t correction,
  output port_id_t    src_port,
  output logic [15:0] seq_id,

  output logic [31:0] c_by_type [16],
  output logic [31:0] c_wrong_domain,
  output logic [31:0] c_bad_fcs
);

  // 13.2 section 7: a tag moves every offset after octet 12 by four.
  // A parser with hard-coded offsets silently mis-parses a tagged PTP
  // frame, which is legal and common on a trunk.
  logic [7:0] base;
  assign base = rx_tagged ? 8'd18 : 8'd14;

  logic [7:0] idx;
  logic       in_frame, et_ok;
  logic [15:0] et_q;

  msg_type_e   mt_q;
  logic [15:0] len_q, flg_q, seq_q;
  logic [7:0]  dom_q;
  correction_t corr_q;
  port_id_t    sp_q;

  always_ff @(posedge clk or negedge rst_n) begin
    int i;
    if (!rst_n) begin
      idx <= '0; in_frame <= 1'b0; et_ok <= 1'b0; et_q <= '0;
      hdr_valid <= 1'b0; c_wrong_domain <= '0; c_bad_fcs <= '0;
      for (i = 0; i < 16; i++) c_by_type[i] <= '0;
    end else begin
      hdr_valid <= 1'b0;

      if (rx_valid && rx_sop) begin
        idx <= 8'd1; in_frame <= 1'b1; et_ok <= 1'b0;
      end else if (rx_valid && in_frame) begin
        idx <= idx + 1'b1;

        if (idx == (base - 2)) et_q[15:8] <= rx_octet;
        if (idx == (base - 1)) et_ok <= ({et_q[15:8], rx_octet} == PTP_ETHERTYPE);

        if (idx == base + 8'd0)  mt_q  <= msg_type_e'(rx_octet[3:0]);
        if (idx == base + 8'd2)  len_q[15:8] <= rx_octet;
        if (idx == base + 8'd3)  len_q[7:0]  <= rx_octet;
        if (idx == base + 8'd4)  dom_q <= rx_octet;
        if (idx == base + 8'd6)  flg_q[15:8] <= rx_octet;
        if (idx == base + 8'd7)  flg_q[7:0]  <= rx_octet;

        // correctionField, octets 8..15 of the header.
        if ((idx >= base + 8'd8) && (idx <= base + 8'd15))
          corr_q[63 - 8*(idx - base - 8)-: 8] <= rx_octet;

        // sourcePortIdentity, octets 20..29.
        if ((idx >= base + 8'd20) && (idx <= base + 8'd27))
          sp_q.clock_id[63 - 8*(idx - base - 20) -: 8] <= rx_octet;
        if (idx == base + 8'd28) sp_q.port_num[15:8] <= rx_octet;
        if (idx == base + 8'd29) sp_q.port_num[7:0]  <= rx_octet;

        if (idx == base + 8'd30) seq_q[15:8] <= rx_octet;
        if (idx == base + 8'd31) seq_q[7:0]  <= rx_octet;
      end

      if (rx_valid && rx_eop) begin
        in_frame <= 1'b0;
        if (et_ok) begin
          if (!rx_fcs_ok) c_bad_fcs <= c_bad_fcs + 1;
          else begin
            c_by_type[mt_q] <= c_by_type[mt_q] + 1;
            hdr_valid    <= 1'b1;
            msg_type     <= mt_q;
            is_event_msg <= is_event(mt_q);
            msg_length   <= len_q;
            domain       <= dom_q;
            flags        <= flg_q;
            correction   <= corr_q;
            src_port     <= sp_q;
            seq_id       <= seq_q;
          end
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// sync_followup_tracker -- pairs a Sync's RECEIVE timestamp with the
// TRANSMIT timestamp that arrives afterwards.
//
// Two-step is used here because it is the simpler shape to present:
// the Sync's own t1 field is ignored and a Follow_Up carries it. One-
// step removes the second message and is chapter 16.3's subject.
// -----------------------------------------------------------------------
module sync_followup_tracker
  import ptp_pkg::*;
#(
  parameter int PENDING = 4          // outstanding Syncs awaiting a Follow_Up
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        hdr_valid,
  input  msg_type_e   msg_type,
  input  logic [15:0] flags,
  input  logic [15:0] seq_id,
  input  port_id_t    src_port,
  input  correction_t correction,
  input  ts_t         body_ts,        // originTimestamp or preciseOrigin
  input  ts_t         rx_hw_ts,       // 16.1 section 12's capture

  input  port_id_t    cfg_master,     // whose Syncs we honour

  output logic        pair_valid,
  output logic [15:0] pair_seq,
  output ts_t         t1,
  output ts_t         t2,
  output correction_t t1_correction,
  output logic [31:0] c_sync,
  output logic [31:0] c_followup,
  output logic [31:0] c_orphan_fu,    // a Follow_Up with no Sync
  output logic [31:0] c_stale_sync    // a Sync evicted unmatched
);

  typedef struct packed {
    logic        busy;
    logic [15:0] seq;
    ts_t         t2;
    logic        twostep;
  } slot_t;

  slot_t slots [PENDING];
  logic [$clog2(PENDING)-1:0] wp;

  // flagField bit 9 (twoStepFlag) says a Follow_Up is coming. A design
  // that ignores it and always waits will stall on a one-step master;
  // one that ignores it and never waits will use an empty t1 field.
  logic two_step;
  assign two_step = flags[9];

  always_ff @(posedge clk or negedge rst_n) begin
    int i;
    if (!rst_n) begin
      for (i = 0; i < PENDING; i++) slots[i] <= '0;
      wp <= '0; pair_valid <= 1'b0;
      c_sync <= '0; c_followup <= '0;
      c_orphan_fu <= '0; c_stale_sync <= '0;
    end else begin
      pair_valid <= 1'b0;

      if (hdr_valid && (src_port.clock_id == cfg_master.clock_id)) begin
        unique case (msg_type)
          MSG_SYNC: begin
            c_sync <= c_sync + 1;
            if (!two_step) begin
              // One-step: t1 is in this frame's own body, already
              // rewritten by the master's hardware. Publish at once.
              pair_valid    <= 1'b1;
              pair_seq      <= seq_id;
              t1            <= body_ts;
              t2            <= rx_hw_ts;
              t1_correction <= correction;
            end else begin
              // Two-step: park t2 and wait.
              if (slots[wp].busy) c_stale_sync <= c_stale_sync + 1;
              slots[wp].busy    <= 1'b1;
              slots[wp].seq     <= seq_id;
              slots[wp].t2      <= rx_hw_ts;
              slots[wp].twostep <= 1'b1;
              wp <= wp + 1'b1;
            end
          end

          MSG_FOLLOW_UP: begin
            automatic bit hit;
            c_followup <= c_followup + 1;
            hit = 1'b0;
            for (i = 0; i < PENDING; i++) begin
              if (slots[i].busy && (slots[i].seq == seq_id)) begin
                hit           = 1'b1;
                pair_valid    <= 1'b1;
                pair_seq      <= seq_id;
                t1            <= body_ts;
                t2            <= slots[i].t2;
                t1_correction <= correction;
                slots[i].busy <= 1'b0;
              end
            end
            if (!hit) c_orphan_fu <= c_orphan_fu + 1;
          end

          default: ;
        endcase
      end
    end
  end

endmodule

t2 = t1 + d_ms + offset
  so  t2 - t1 = d_ms + offset                         ... (1)

t4 = t3 - offset + d_sm
  so  t4 - t3 = d_sm - offset                         ... (2)

(t2 - t1) + (t4 - t3) = d_ms + d_sm = the round trip  ... (3)

(t2 - t1) - (t4 - t3) = d_ms - d_sm + 2 * offset      ... (4)

mean_path = ((t2 - t1) + (t4 - t3)) / 2               ... from (3)
offset    = ((t2 - t1) - (t4 - t3)) / 2               ... from (4)

offset_error = (d_sm - d_ms) / 2

// -----------------------------------------------------------------------
// offset_delay_calc -- turns four timestamps into an offset and a mean
// path delay.
//
// The correctionField from each message is SUBTRACTED from the
// corresponding interval: it holds the residence time a transparent
// clock accumulated, which is delay that did not happen on the wire.
// 16.4 section 12 is where those values come from.
// -----------------------------------------------------------------------
module offset_delay_calc
  import ptp_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        ms_valid,        // a (t1,t2) pair from section 5
  input  ts_t         t1,
  input  ts_t         t2,
  input  correction_t corr_ms,

  input  logic        sm_valid,        // a (t3,t4) pair from section 11
  input  ts_t         t3,
  input  ts_t         t4,
  input  correction_t corr_sm,

  output logic        result_valid,
  output logic signed [63:0] offset_ns,
  output logic signed [63:0] mean_path_ns,
  output logic signed [63:0] round_trip_ns,
  output logic        negative_path,    // the round trip came out < 0
  output logic [31:0] c_results,
  output logic [31:0] c_negative
);

  // Both halves must be present before either equation is evaluated.
  // A design that computes an offset from a fresh (t1,t2) and a stale
  // (t3,t4) has mixed two path measurements -- section 10.
  logic ms_have, sm_have;
  logic signed [63:0] d_ms, d_sm;

  function automatic logic signed [63:0] ts_diff(input ts_t a, input ts_t b);
    ts_diff = ($signed(64'(a.sec)) - $signed(64'(b.sec))) * 64'sd1_000_000_000
            + ($signed(64'(a.ns))  - $signed(64'(b.ns)));
  endfunction

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      ms_have <= 1'b0; sm_have <= 1'b0;
      d_ms <= '0; d_sm <= '0;
      result_valid <= 1'b0; offset_ns <= '0;
      mean_path_ns <= '0; round_trip_ns <= '0;
      negative_path <= 1'b0; c_results <= '0; c_negative <= '0;
    end else begin
      result_valid  <= 1'b0;
      negative_path <= 1'b0;

      // correctionField is 16.16 fixed point; take its integer part.
      if (ms_valid) begin
        d_ms    <= ts_diff(t2, t1) - (corr_ms >>> 16);
        ms_have <= 1'b1;
      end
      if (sm_valid) begin
        d_sm    <= ts_diff(t4, t3) - (corr_sm >>> 16);
        sm_have <= 1'b1;
      end

      if (ms_have && sm_have && (ms_valid || sm_valid)) begin
        automatic logic signed [63:0] a, b, rt;
        a  = ms_valid ? (ts_diff(t2, t1) - (corr_ms >>> 16)) : d_ms;
        b  = sm_valid ? (ts_diff(t4, t3) - (corr_sm >>> 16)) : d_sm;
        rt = a + b;

        round_trip_ns <= rt;
        // Equation (3): the round trip, with no assumption in it.
        mean_path_ns  <= rt >>> 1;
        // Equation (4): the offset, ASSUMING d_ms == d_sm.
        offset_ns     <= (a - b) >>> 1;
        result_valid  <= 1'b1;
        c_results     <= c_results + 1;

        // A negative round trip is arithmetically impossible and
        // therefore evidence about the INPUTS -- section 10.
        if (rt < 0) begin
          negative_path <= 1'b1;
          c_negative    <= c_negative + 1;
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// seqid_pairing_tracker -- matches a Delay_Resp back to the Delay_Req
// it answers, and detects the pairings that silently go wrong.
//
// The sequenceId is 16 bits and wraps. The requestingPortIdentity in a
// Delay_Resp names WHICH slave asked, which matters because the
// Delay_Resp is multicast on most deployments and every slave sees it.
// -----------------------------------------------------------------------
module seqid_pairing_tracker
  import ptp_pkg::*;
#(
  parameter int OUTSTANDING = 8,
  parameter int TIMEOUT_CYCLES = 2_500_000_000/1000   // 5 ms at 500 MHz
)(
  input  logic        clk,
  input  logic        rst_n,

  // Our own Delay_Req, as it leaves.
  input  logic        dreq_sent,
  input  logic [15:0] dreq_seq,
  input  ts_t         dreq_t3,

  // An arriving Delay_Resp.
  input  logic        dresp_valid,
  input  logic [15:0] dresp_seq,
  input  port_id_t    dresp_requesting,
  input  ts_t         dresp_t4,
  input  correction_t dresp_correction,

  input  port_id_t    cfg_self,

  output logic        sm_valid,
  output ts_t         t3,
  output ts_t         t4,
  output correction_t corr_sm,
  output logic [31:0] c_matched,
  output logic [31:0] c_not_for_us,
  output logic [31:0] c_unmatched,
  output logic [31:0] c_timed_out
);

  typedef struct packed {
    logic        busy;
    logic [15:0] seq;
    ts_t         t3;
    logic [31:0] age;
  } entry_t;

  entry_t q [OUTSTANDING];
  logic [$clog2(OUTSTANDING)-1:0] wp;

  always_ff @(posedge clk or negedge rst_n) begin
    int i;
    if (!rst_n) begin
      for (i = 0; i < OUTSTANDING; i++) q[i] <= '0;
      wp <= '0; sm_valid <= 1'b0;
      c_matched <= '0; c_not_for_us <= '0;
      c_unmatched <= '0; c_timed_out <= '0;
    end else begin
      sm_valid <= 1'b0;

      // Age every outstanding request; a Delay_Resp that never comes
      // must free its slot or the tracker fills and stops matching.
      for (i = 0; i < OUTSTANDING; i++) begin
        if (q[i].busy) begin
          q[i].age <= q[i].age + 1;
          if (q[i].age == TIMEOUT_CYCLES-1) begin
            q[i].busy   <= 1'b0;
            c_timed_out <= c_timed_out + 1;
          end
        end
      end

      if (dreq_sent) begin
        q[wp].busy <= 1'b1;
        q[wp].seq  <= dreq_seq;
        q[wp].t3   <= dreq_t3;
        q[wp].age  <= '0;
        wp <= wp + 1'b1;
      end

      if (dresp_valid) begin
        // Gate 1 -- is this answering US? A multicast Delay_Resp is
        // seen by every slave on the segment and answers one of them.
        if (dresp_requesting.clock_id != cfg_self.clock_id) begin
          c_not_for_us <= c_not_for_us + 1;
        end else begin
          automatic bit hit;
          hit = 1'b0;
          for (i = 0; i < OUTSTANDING; i++) begin
            if (q[i].busy && (q[i].seq == dresp_seq)) begin
              hit       = 1'b1;
              sm_valid  <= 1'b1;
              t3        <= q[i].t3;
              t4        <= dresp_t4;
              corr_sm   <= dresp_correction;
              q[i].busy <= 1'b0;
              c_matched <= c_matched + 1;
            end
          end
          if (!hit) c_unmatched <= c_unmatched + 1;
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// delay_req_resp_engine -- issues Delay_Req messages at a randomised
// interval and consumes the Delay_Resp that answers them.
//
// The randomisation is not cosmetic. Every slave on a segment that
// issues Delay_Req on a fixed period synchronised to the Sync it just
// received will transmit at the SAME instant, and the master receives
// N requests in one burst -- section 12's callout.
// -----------------------------------------------------------------------
module delay_req_resp_engine
  import ptp_pkg::*;
#(
  parameter int CLK_HZ = 500_000_000,
  parameter int LOG_INTERVAL = 0        // 2^0 = 1 s between requests
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        sync_received,     // a fresh Sync landed
  input  logic [15:0] rand_bits,         // from an LFSR
  input  logic        tx_ready,

  output logic        dreq_tx,
  output logic [15:0] dreq_seq,
  input  ts_t         dreq_hw_ts,        // 16.3's TX capture
  input  logic        dreq_hw_ts_valid,

  output logic        dreq_sent,
  output logic [15:0] dreq_sent_seq,
  output ts_t         dreq_t3,

  output logic [31:0] c_issued,
  output logic [31:0] c_no_tx_ts,
  output logic [31:0] interval_ms
);

  localparam int NOMINAL = CLK_HZ;                 // 2^LOG_INTERVAL sec
  localparam int PERIOD  = NOMINAL <<< LOG_INTERVAL;

  logic [31:0] cnt, target;
  logic [15:0] seq_q;
  logic        awaiting_ts;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cnt <= '0; seq_q <= '0; dreq_tx <= 1'b0;
      awaiting_ts <= 1'b0; dreq_sent <= 1'b0;
      c_issued <= '0; c_no_tx_ts <= '0;
      // The first interval is randomised too, so a rack of devices
      // powering up together does not stay in lockstep.
      target <= PERIOD;
      interval_ms <= '0;
    end else begin
      dreq_tx   <= 1'b0;
      dreq_sent <= 1'b0;

      cnt <= cnt + 1;
      if (cnt >= target) begin
        if (tx_ready && !awaiting_ts) begin
          dreq_tx     <= 1'b1;
          dreq_seq    <= seq_q;
          seq_q       <= seq_q + 1'b1;
          awaiting_ts <= 1'b1;
          c_issued    <= c_issued + 1;
          cnt         <= '0;
          // Uniform over [0.75, 1.25] of the nominal period. The
          // standard requires the mean to be the configured interval
          // and the individual intervals to be spread.
          target      <= PERIOD - (PERIOD >> 2)
                       + ((PERIOD >> 1) * 32'(rand_bits)) / 32'd65536;
          interval_ms <= target / (CLK_HZ / 1000);
        end
      end

      // The TRANSMIT timestamp arrives from the hardware after the
      // frame has left. Until it does, t3 does not exist -- which is
      // the same structural problem 16.3 solves for Sync.
      if (awaiting_ts) begin
        if (dreq_hw_ts_valid) begin
          awaiting_ts   <= 1'b0;
          dreq_sent     <= 1'b1;
          dreq_sent_seq <= seq_q - 1'b1;
          dreq_t3       <= dreq_hw_ts;
        end else if (cnt == target) begin
          // A whole interval with no transmit timestamp: the capture
          // was lost. The request is unusable and must be abandoned.
          awaiting_ts <= 1'b0;
          c_no_tx_ts  <= c_no_tx_ts + 1;
        end
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// announce_dataset -- holds the local clock's advertised quality and
// the best remote dataset seen, and decides which is better.
//
// There is no election. Every clock advertises what it is; every clock
// independently applies the same comparison; and the one that finds
// nothing better than itself becomes master. Section 14.
// -----------------------------------------------------------------------
module announce_dataset
  import ptp_pkg::*;
#(
  parameter int ANNOUNCE_TIMEOUT = 3     // 3 announce intervals
)(
  input  logic        clk,
  input  logic        rst_n,

  // What we are.
  input  logic [7:0]  local_priority1,
  input  logic [7:0]  local_class,
  input  logic [7:0]  local_accuracy,
  input  logic [15:0] local_variance,
  input  logic [7:0]  local_priority2,
  input  logic [63:0] local_clock_id,

  // An arriving Announce.
  input  logic        ann_valid,
  input  logic [7:0]  rx_priority1,
  input  logic [7:0]  rx_class,
  input  logic [7:0]  rx_accuracy,
  input  logic [15:0] rx_variance,
  input  logic [7:0]  rx_priority2,
  input  logic [63:0] rx_clock_id,
  input  logic [7:0]  rx_steps_removed,

  input  logic        announce_tick,     // one per announce interval

  output logic        we_are_master,
  output logic [63:0] best_master_id,
  output logic [7:0]  best_steps_removed,
  output logic [31:0] c_announces,
  output logic [31:0] c_master_changes,
  output logic [31:0] c_timeouts
);

  // The best master clock algorithm's comparison, in order. Each field
  // is only consulted if every earlier one ties. The LAST tiebreak is
  // the clock identity, which is unique by construction -- so the
  // comparison is TOTAL and two clocks can never both decide they win.
  function automatic bit remote_is_better(
      input logic [7:0]  rp1, input logic [7:0]  rc,
      input logic [7:0]  ra,  input logic [15:0] rv,
      input logic [7:0]  rp2, input logic [63:0] rid,
      input logic [7:0]  lp1, input logic [7:0]  lc,
      input logic [7:0]  la,  input logic [15:0] lv,
      input logic [7:0]  lp2, input logic [63:0] lid);
    begin
      if (rp1 != lp1) return (rp1 < lp1);
      if (rc  != lc)  return (rc  < lc);
      if (ra  != la)  return (ra  < la);
      if (rv  != lv)  return (rv  < lv);
      if (rp2 != lp2) return (rp2 < lp2);
      return (rid < lid);          // total order, always decides
    end
  endfunction

  logic [7:0]  b_p1, b_cls, b_acc, b_p2;
  logic [15:0] b_var;
  logic [63:0] b_id;
  logic        have_best;
  logic [7:0]  age;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      have_best <= 1'b0; age <= '0;
      b_p1 <= '0; b_cls <= '0; b_acc <= '0; b_var <= '0;
      b_p2 <= '0; b_id <= '0;
      we_are_master <= 1'b1;        // alone until told otherwise
      best_master_id <= '0; best_steps_removed <= '0;
      c_announces <= '0; c_master_changes <= '0; c_timeouts <= '0;
    end else begin
      if (ann_valid) begin
        c_announces <= c_announces + 1;
        age         <= '0;

        // Is this Announce better than the best we hold?
        if (!have_best ||
            remote_is_better(rx_priority1, rx_class, rx_accuracy,
                             rx_variance, rx_priority2, rx_clock_id,
                             b_p1, b_cls, b_acc, b_var, b_p2, b_id)) begin
          have_best <= 1'b1;
          b_p1 <= rx_priority1; b_cls <= rx_class;
          b_acc <= rx_accuracy; b_var <= rx_variance;
          b_p2 <= rx_priority2; b_id <= rx_clock_id;
          if (b_id != rx_clock_id) c_master_changes <= c_master_changes + 1;
          best_master_id     <= rx_clock_id;
          best_steps_removed <= rx_steps_removed;
        end
      end

      if (announce_tick) begin
        if (have_best) begin
          age <= age + 1'b1;
          if (age == ANNOUNCE_TIMEOUT-1) begin
            // The master went quiet. Fall back to ourselves and let
            // the comparison run again from scratch.
            have_best  <= 1'b0;
            c_timeouts <= c_timeouts + 1;
          end
        end
      end

      // We are master exactly when nothing better has been heard.
      we_are_master <= !have_best ||
        !remote_is_better(b_p1, b_cls, b_acc, b_var, b_p2, b_id,
                          local_priority1, local_class, local_accuracy,
                          local_variance, local_priority2, local_clock_id);
    end
  end

endmodule

// -----------------------------------------------------------------------
// exchange_telemetry -- what an operator needs to decide whether a PTP
// exchange is healthy, and — separately — whether its results can be
// trusted.
//
// The second question is the one Section 8 makes necessary: an
// exchange can be perfectly healthy and produce an offset that is
// wrong by half the path's asymmetry.
// -----------------------------------------------------------------------
module exchange_telemetry
  import ptp_pkg::*;
#(
  parameter int HISTORY = 16
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        result_valid,
  input  logic signed [63:0] offset_ns,
  input  logic signed [63:0] mean_path_ns,
  input  logic signed [63:0] round_trip_ns,

  input  logic [31:0] c_sync,
  input  logic [31:0] c_stale_sync,
  input  logic [31:0] c_timed_out,
  input  logic [31:0] c_negative,
  input  logic        window_tick,

  output logic signed [63:0] path_spread_ns,   // max - min of mean_path
  output logic signed [63:0] path_median_ns,
  output logic [15:0] loss_pct_x100,
  output logic        path_is_stable,
  output logic        results_trustworthy,
  output logic [31:0] c_windows
);

  logic signed [63:0] hist [HISTORY];
  logic [$clog2(HISTORY)-1:0] wp;
  logic [$clog2(HISTORY):0]   fill;
  logic [31:0] sync_base, lost_base;

  always_ff @(posedge clk or negedge rst_n) begin
    int i;
    if (!rst_n) begin
      for (i = 0; i < HISTORY; i++) hist[i] <= '0;
      wp <= '0; fill <= '0;
      path_spread_ns <= '0; path_median_ns <= '0;
      loss_pct_x100 <= '0; path_is_stable <= 1'b0;
      results_trustworthy <= 1'b0; c_windows <= '0;
      sync_base <= '0; lost_base <= '0;
    end else begin
      if (result_valid) begin
        hist[wp] <= mean_path_ns;
        wp <= wp + 1'b1;
        if (fill != HISTORY) fill <= fill + 1'b1;
      end

      if (window_tick) begin
        automatic logic signed [63:0] mx, mn;
        automatic logic [31:0] syncs, lost;
        mx = hist[0]; mn = hist[0];
        for (i = 1; i < HISTORY; i++) begin
          if (hist[i] > mx) mx = hist[i];
          if (hist[i] < mn) mn = hist[i];
        end
        path_spread_ns <= mx - mn;
        // A crude median: the midpoint of the observed range is good
        // enough to spot a path that has changed, which is the use.
        path_median_ns <= (mx + mn) >>> 1;

        syncs = c_sync - sync_base;
        lost  = (c_stale_sync + c_timed_out) - lost_base;
        loss_pct_x100 <= (syncs == 0) ? 16'd0
                       : 16'((lost * 10000) / syncs);
        sync_base <= c_sync;
        lost_base <= c_stale_sync + c_timed_out;

        // A stable path is one whose measured delay is not moving.
        // A moving path delay means the asymmetry is also moving, so
        // no stored calibration applies.
        path_is_stable <= ((mx - mn) < 64'sd1000) && (fill == HISTORY);

        // Trustworthy means: messages are arriving, the arithmetic is
        // sane, and the path is stable enough for a calibration to
        // mean anything. It does NOT mean the offset is correct --
        // section 8, and section 19's rejected property.
        results_trustworthy <= (fill == HISTORY) &&
                               (c_negative == '0) &&
                               ((mx - mn) < 64'sd1000);
        c_windows <= c_windows + 1;
      end
    end
  end

endmodule

// -----------------------------------------------------------------------
// exchange_conformance_monitor -- one bit.
//
// Every check is evaluable from messages this device sent or received.
// Section 19's rejected property is the one check that is not, and it
// is the one an operator most wants this bit to mean.
// -----------------------------------------------------------------------
module exchange_conformance_monitor
  import ptp_pkg::*;
(
  input  logic       clk,
  input  logic       rst_n,

  input  logic       negative_round_trip,
  input  logic       paired_across_masters,   // t1,t2 and t3,t4 from different masters
  input  logic       twostep_flag_ignored,
  input  logic       resp_not_for_us_used,    // matched on seq alone
  input  logic       correction_sign_wrong,   // added instead of subtracted
  input  logic       cfg_domain_mismatch,
  input  logic       cfg_no_master_selected,
  input  logic       dreq_interval_not_random,

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

  logic v_neg, v_cross, v_flag, v_wrong_resp, v_sign, v_dom, v_nomaster, v_burst;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      v_neg <= 1'b0; v_cross <= 1'b0; v_flag <= 1'b0;
      v_wrong_resp <= 1'b0; v_sign <= 1'b0; v_burst <= 1'b0;
      v_dom <= 1'b0; v_nomaster <= 1'b0; c_violations <= '0;
    end else begin
      // Runtime violations, sticky: each is a real defect and one
      // occurrence is the finding.
      if (negative_round_trip)   begin v_neg        <= 1'b1; c_violations <= c_violations + 1; end
      if (paired_across_masters) begin v_cross      <= 1'b1; c_violations <= c_violations + 1; end
      if (twostep_flag_ignored)  begin v_flag       <= 1'b1; c_violations <= c_violations + 1; end
      if (resp_not_for_us_used)  begin v_wrong_resp <= 1'b1; c_violations <= c_violations + 1; end
      if (correction_sign_wrong) begin v_sign       <= 1'b1; c_violations <= c_violations + 1; end

      // Standing configuration properties -- wrong from power-on,
      // not from the first message. 14.1 section 17's argument.
      v_dom      <= cfg_domain_mismatch;
      v_nomaster <= cfg_no_master_selected;
      v_burst    <= dreq_interval_not_random;
    end
  end

  assign conformant = !(v_neg || v_cross || v_flag || v_wrong_resp ||
                        v_sign || v_dom || v_nomaster || v_burst);
  assign fault_vector = {v_burst, v_nomaster, v_dom, v_sign,
                         v_wrong_resp, v_flag, v_cross, v_neg};

endmodule

// P1. A PTP message is recognised only on the PTP EtherType.
property p_ethertype_gate;
  @(posedge clk) disable iff (!rst_n)
  hdr_valid |-> $past(et_ok);
endproperty

// P2. Nothing is published on a bad FCS.
property p_no_commit_bad_fcs;
  @(posedge clk) disable iff (!rst_n)
  (rx_eop && !rx_fcs_ok) |-> !hdr_valid;
endproperty

// P3. The event/general split is exactly the top bit of the message
// type. 16.3's timestamp unit depends on this being cheap.
property p_event_is_top_bit;
  @(posedge clk) disable iff (!rst_n)
  hdr_valid |-> (is_event_msg == !msg_type[3]);
endproperty

// P4. A tagged frame is parsed at the shifted offsets. 13.2 section 7.
property p_tag_shifts_offsets;
  @(posedge clk) disable iff (!rst_n)
  (hdr_valid && rx_tagged) |-> (base == 8'd18);
endproperty

// P5. Exactly one type counter moves per accepted message.
property p_type_counter_partition;
  @(posedge clk) disable iff (!rst_n)
  hdr_valid |=> ($countones(type_counter_changed) == 1);
endproperty

// P6. A one-step Sync publishes immediately and never parks.
property p_onestep_is_immediate;
  @(posedge clk) disable iff (!rst_n)
  (hdr_valid && (msg_type == MSG_SYNC) && !flags[9]) |=> pair_valid;
endproperty

// P7. A two-step Sync never publishes on its own.
property p_twostep_waits;
  @(posedge clk) disable iff (!rst_n)
  (hdr_valid && (msg_type == MSG_SYNC) && flags[9]) |=> !pair_valid;
endproperty

// P8. A published pair's t2 came from the Sync with the SAME
// sequence id as the Follow_Up that completed it.
property p_pair_is_same_sequence;
  @(posedge clk) disable iff (!rst_n)
  pair_valid |-> (pair_seq == $past(seq_id));
endproperty

// P9. Only the configured master's Syncs are honoured.
property p_only_our_master;
  @(posedge clk) disable iff (!rst_n)
  pair_valid |-> ($past(src_port.clock_id) == cfg_master.clock_id);
endproperty

// P10. An evicted unmatched Sync is always counted.
property p_eviction_counted;
  @(posedge clk) disable iff (!rst_n)
  (hdr_valid && (msg_type == MSG_SYNC) && flags[9] && slots[wp].busy)
    |=> $changed(c_stale_sync);
endproperty

// P11. The round trip is non-negative. It is a physical duration and
// a negative value is evidence about the inputs.
property p_round_trip_is_physical;
  @(posedge clk) disable iff (!rst_n)
  (result_valid && !negative_path) |-> (round_trip_ns >= 0);
endproperty

// P12. mean_path is exactly half the round trip -- equation (3),
// which carries no premise.
property p_mean_path_is_half_round_trip;
  @(posedge clk) disable iff (!rst_n)
  result_valid |-> (mean_path_ns == (round_trip_ns >>> 1));
endproperty

// P13. The correction field is SUBTRACTED. Adding it doubles the
// error transparent clocks were correcting.
property p_correction_is_subtracted;
  @(posedge clk) disable iff (!rst_n)
  (ms_valid && (corr_ms > 0)) |=> (d_ms < ts_diff(t2, t1));
endproperty

// P14. No result is published until BOTH halves have been seen.
property p_needs_both_halves;
  @(posedge clk) disable iff (!rst_n)
  result_valid |-> (ms_have && sm_have);
endproperty

// P15. A negative round trip is always flagged and counted.
property p_negative_flagged;
  @(posedge clk) disable iff (!rst_n)
  (result_valid && (round_trip_ns < 0)) |-> negative_path;
endproperty

// P16. Under the premise, the offset is exact. The premise is an
// explicit antecedent -- section 19's rejected property is what
// happens when it is left implicit.
property p_offset_correct_when_symmetric;
  @(posedge clk) disable iff (!rst_n)
  (result_valid && (tb_d_ms == tb_d_sm)) |->
    (offset_ns == (tb_slave_ns - tb_master_ns));
endproperty

// P17. And when the premise fails, the error is EXACTLY half the
// imbalance. A stronger and more useful claim than the one refused.
property p_error_is_half_the_imbalance;
  @(posedge clk) disable iff (!rst_n)
  result_valid |-> ((offset_ns - (tb_slave_ns - tb_master_ns)) ==
                    ((tb_d_sm - tb_d_ms) >>> 1));
endproperty

// P18. A Delay_Resp addressed to another slave is never used.
property p_resp_must_be_for_us;
  @(posedge clk) disable iff (!rst_n)
  sm_valid |-> ($past(dresp_requesting.clock_id) == cfg_self.clock_id);
endproperty

// P19. A matched pair's t3 came from the request with that sequence id.
property p_t3_matches_sequence;
  @(posedge clk) disable iff (!rst_n)
  sm_valid |-> ($past(dresp_seq) inside {outstanding_seqs});
endproperty

// P20. Every outstanding request eventually frees its slot -- matched
// or aged out. Without this the tracker fills and stops silently.
property p_slots_always_free;
  @(posedge clk) disable iff (!rst_n)
  $rose(q[i].busy) |-> ##[1:TIMEOUT_CYCLES+1] !q[i].busy;
endproperty

// P21. A Delay_Req is never issued while its predecessor's transmit
// timestamp is outstanding.
property p_one_outstanding_tx_ts;
  @(posedge clk) disable iff (!rst_n)
  (dreq_tx) |-> !$past(awaiting_ts);
endproperty

// P22. The Delay_Req interval is randomised: consecutive intervals
// are not equal. A fixed interval produces section 11's burst.
property p_interval_is_randomised;
  @(posedge clk) disable iff (!rst_n)
  dreq_tx |=> (target != $past(target));
endproperty

// P23. The comparison is a TOTAL order: it never returns "equal",
// because the clock identity always decides.
property p_comparison_is_total;
  @(posedge clk) disable iff (!rst_n)
  (a_id != b_id) |-> (remote_is_better(a) != remote_is_better(b));
endproperty

// P24. priority1 dominates everything. An operator override is not
// overridden by clock quality.
property p_priority1_dominates;
  @(posedge clk) disable iff (!rst_n)
  (rx_priority1 < local_priority1) |=> !we_are_master;
endproperty

// P25. We are master exactly when nothing better has been heard.
property p_master_iff_best;
  @(posedge clk) disable iff (!rst_n)
  we_are_master <-> (!have_best || !remote_is_better(best, local));
endproperty

// P26. An announce timeout falls back to ourselves rather than
// holding a master that has gone quiet.
property p_timeout_releases_master;
  @(posedge clk) disable iff (!rst_n)
  (announce_tick && (age == ANNOUNCE_TIMEOUT-1)) |=> !have_best;
endproperty

// P27. Every master change is counted -- each one costs a re-lock.
property p_master_change_counted;
  @(posedge clk) disable iff (!rst_n)
  $changed(best_master_id) |=> $changed(c_master_changes);
endproperty

// P28. Standing property: the domain matches. A device on the wrong
// domain hears everything and uses none of it.
property p_domain_matches;
  @(posedge clk) disable iff (!rst_n)
  !cfg_domain_mismatch;
endproperty

// P29. A pair is never assembled across a master change.
property p_no_cross_master_pairing;
  @(posedge clk) disable iff (!rst_n)
  result_valid |-> !paired_across_masters;
endproperty

// P30. results_trustworthy requires a stable path -- it is about the
// premise's stability, not about the offset's correctness.
property p_trustworthy_needs_stable_path;
  @(posedge clk) disable iff (!rst_n)
  results_trustworthy |-> (path_spread_ns < 64'sd1000);
endproperty

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