Polling — Can We Read Each Other?

PHY lock and alignment        →  can I sample and frame the incoming stream?
Training recognition          →  does the framed stream contain valid training information?

qualifying observation  → count up
disqualifying observation → count resets
count reaches threshold → this is trustworthy

step             1     2     3     4     5     6     7     8     9    10
cdr_lock         0     1     1     1     1     1     1     1     1     1
rx_aligned       0     0     1     1     1     1     1     1     1     1
 
obs_valid        0     0     1     1     1     0     1     1     1     1
obs_kind         -     -   TS1   TS1   BAD    -   TS1   TS1   TS1   TS1
qual_count       0     0     1     2     0     0     1     2     3     4
threshold_met    0     0     0     0     0     0     0     0     0     1
 
polling_done     0     0     0     0     0     0     0     0     0     1
traffic_enabled  0     0     0     0     0     0     0     0     0     0

// SYNTHESIZABLE. Normalized training-observation representation.
// THE KINDS are canonical (section 5: TS1 and TS2 are distinct ordered
// sets carrying training context). THE FIELD WIDTHS here are INTERNAL
// NORMALIZED widths, not verified normative field widths -- section 1
// declines to publish TS layouts, and Chapter 18.4 goes deeper on the
// link and lane fields.
package polling_pkg;
 
  typedef enum logic [2:0] {
    OS_NONE     = 3'd0,
    OS_TS1      = 3'd1,
    OS_TS2      = 3'd2,
    OS_OTHER    = 3'd3,   // a training set this port does not qualify on
    OS_INVALID  = 3'd4    // structurally malformed
  } os_kind_e;
 
  // INTERNAL normalized widths. A design with verified normative widths
  // substitutes them here and nowhere else.
  localparam int LINK_W = 9;
  localparam int LANE_W = 5;
  localparam int RATE_W = 4;
  localparam int CTRL_W = 8;
 
  typedef struct packed {
    logic               valid;
    os_kind_e           kind;
    logic [LINK_W-1:0]  link_num;
    logic [LANE_W-1:0]  lane_num;
    logic [RATE_W-1:0]  rate;
    logic [CTRL_W-1:0]  ctrl;
  } training_obs_t;
 
  // ONLY TS1 AND TS2 QUALIFY. An unrecognised or malformed training set
  // must never count toward progress (section 12, P5).
  function automatic bit obs_qualifies(input training_obs_t o);
    return o.valid && ((o.kind == OS_TS1) || (o.kind == OS_TS2));
  endfunction
 
  function automatic bit obs_disqualifies(input training_obs_t o);
    return o.valid && ((o.kind == OS_OTHER) || (o.kind == OS_INVALID));
  endfunction
 
endpackage

import polling_pkg::*;
 
// SYNTHESIZABLE. Capture one training observation whole, and hold it while
// the consumer is busy.
// THE PARSER CANNOT BE BACKPRESSURED -- observations arrive from a
// continuously running receive path (Chapter 17.2 section 9). So an
// observation that cannot be held is REPORTED, never silently dropped.
module training_obs_capture (
  input  logic clk,
  input  logic rst_n,
 
  // ---- From the normalized ordered-set parser. NO `ready`. --------------
  input  logic          parse_valid,
  input  os_kind_e      parse_kind,
  input  logic [LINK_W-1:0] parse_link,
  input  logic [LANE_W-1:0] parse_lane,
  input  logic [RATE_W-1:0] parse_rate,
  input  logic [CTRL_W-1:0] parse_ctrl,
 
  // ---- Entering Polling clears any observation from an earlier state ----
  input  logic          state_entry,
 
  // ---- To the progress controller ----------------------------------------
  output training_obs_t obs,
  input  logic          obs_ready,
 
  output logic          obs_overflow
);
 
  training_obs_t o_q;
  logic          ovf_q;
 
  assign obs          = o_q;
  assign obs_overflow = ovf_q;
 
  wire fire     = o_q.valid && obs_ready;
  wire can_take = !o_q.valid || obs_ready;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      o_q <= '0; ovf_q <= 1'b0;
    end else if (state_entry) begin
      // ==============================================================
      // ENTERING POLLING DISCARDS ANY PENDING OBSERVATION.
      //
      // Checked FIRST, so an observation parsed just before entry cannot
      // count toward this state's qualification. A stale ordered set from
      // a previous state is exactly the kind of evidence that must not
      // contribute (section 15, mutation 6).
      // ==============================================================
      o_q <= '0;
    end else begin
      if (parse_valid && can_take) begin
        // THE WHOLE DESCRIPTOR AT ONCE. Nothing downstream re-reads the
        // parser -- an observation's fields belong to that observation.
        o_q.valid    <= 1'b1;
        o_q.kind     <= parse_kind;
        o_q.link_num <= parse_link;
        o_q.lane_num <= parse_lane;
        o_q.rate     <= parse_rate;
        o_q.ctrl     <= parse_ctrl;
      end else if (fire) begin
        o_q.valid <= 1'b0;
      end
 
      // An observation that could not be held is REPORTED. The receive
      // path did not stop; pretending it did would hide lost evidence.
      if (parse_valid && !can_take) ovf_q <= 1'b1;
    end
  end
 
endmodule

import polling_pkg::*;
 
// SYNTHESIZABLE. Count CONSECUTIVE qualifying observations.
// THAT PROGRESS REQUIRES REPEATED RECOGNITION is the mechanism (section
// 7). THE THRESHOLD IS A PARAMETER and is ILLUSTRATIVE -- section 1 could
// not source the normative counts, and this chapter publishes none.
module obs_qualifier #(
  parameter int THRESH = 4,
  // GUARDED. $clog2 of a small threshold, never zero-width.
  parameter int CNT_W  = (THRESH <= 1) ? 1 : $clog2(THRESH + 1)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic          restart,          // state entry, or a lost precondition
  input  logic          qualifying,
  input  logic          disqualifying,
 
  output logic [CNT_W-1:0] count,
  output logic             threshold_met
);
 
  generate
    if (THRESH < 1) $error("THRESH must be at least 1");
    if (CNT_W  < 1) $error("CNT_W must be at least 1");
    if ((1 << CNT_W) < (THRESH + 1))
      $error("CNT_W too narrow to hold THRESH");
  endgenerate
 
  logic [CNT_W-1:0] cnt_q;
  assign count = cnt_q;
 
  // ==================================================================
  // THE COMPARISON THAT MUST BE EXACTLY RIGHT.
  //
  //   >= THRESH        CORRECT   -- asserts on the THRESH-th observation
  //   >= THRESH-1      ONE EARLY -- and INVISIBLE at THRESH == 1, which
  //                                 is why section 15 requires THRESH >= 2
  //   >  THRESH        ONE LATE  -- never asserts if the counter saturates
  //
  // Section 15 verified this exhaustively against an independent model.
  // ==================================================================
  assign threshold_met = (cnt_q >= CNT_W'(THRESH));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cnt_q <= '0;
    end else if (restart) begin
      // Restart has priority: entering the state, or losing a
      // precondition, invalidates the history regardless of this cycle's
      // observation.
      cnt_q <= '0;
    end else if (disqualifying) begin
      // CONSECUTIVE, NOT CUMULATIVE. A bad observation resets to ZERO,
      // not to one. Counting up only would let scattered good
      // observations across a mostly-bad stream reach the threshold --
      // qualifying a lane that is not working (section 7).
      cnt_q <= '0;
    end else if (qualifying) begin
      // SATURATE. A wrapping counter would drop below the threshold after
      // reaching it and de-assert threshold_met while the stream is fine.
      if (cnt_q < CNT_W'(THRESH)) cnt_q <= cnt_q + CNT_W'(1);
    end
  end
 
endmodule

import polling_pkg::*;
 
// SYNTHESIZABLE. Progress within Polling only.
// THIS IS NOT THE LTSSM and is not Polling's normative substate encoding
// (Chapter 18.1 section 9). It models the digital progression: wait for
// lock and alignment, qualify observations, report done or failed.
// The timeout limit is a PARAMETER -- no PCIe constant appears here.
module polling_progress #(
  parameter int THRESH = 4,
  parameter int CNT_W  = 24
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic          state_entry,      // entering Polling
 
  // ---- Preconditions, from the receive path -----------------------------
  // TWO SEPARATE SIGNALS, deliberately (section 4). Collapsing them into
  // one ready bit destroys the ability to say which failed.
  input  logic          cdr_lock,
  input  logic          rx_aligned,
 
  // ---- Observations ------------------------------------------------------
  input  training_obs_t obs,
  output logic          obs_ready,
 
  // ---- Timeout -----------------------------------------------------------
  input  logic [CNT_W-1:0] timeout_limit,
  input  logic             timeout_elapsed,
 
  // ---- Results ------------------------------------------------------------
  output logic          polling_done,
  output logic          polling_fail,
  output logic          waiting_for_lock,
  output logic          qualifying_now
);
 
  typedef enum logic [1:0] { S_WAIT_LOCK, S_QUALIFY, S_DONE, S_FAIL } st_e;
  st_e st_q;
 
  wire lock_ok = cdr_lock && rx_aligned;
 
  assign waiting_for_lock = (st_q == S_WAIT_LOCK);
  assign qualifying_now   = (st_q == S_QUALIFY);
  assign polling_done     = (st_q == S_DONE);
  assign polling_fail     = (st_q == S_FAIL);
 
  // Observations are consumed only while qualifying. In any other state
  // they are not evidence, and accepting them would let a stale stream
  // contribute to a qualification that has not started.
  assign obs_ready = (st_q == S_QUALIFY);
 
  wire qualifying    = (st_q == S_QUALIFY) && obs_qualifies(obs);
  wire disqualifying = (st_q == S_QUALIFY) && obs_disqualifies(obs);
 
  logic threshold_met;
  logic [$clog2(THRESH+1)-1:0] qcount;
 
  obs_qualifier #(.THRESH(THRESH)) u_q (
    .clk, .rst_n,
    // LOSING LOCK INVALIDATES THE HISTORY. Observations qualified under a
    // lock that has since been lost are not evidence about the stream now.
    .restart      (state_entry || !lock_ok),
    .qualifying, .disqualifying,
    .count        (qcount),
    .threshold_met(threshold_met)
  );
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q <= S_WAIT_LOCK;
    end else if (state_entry) begin
      // Entry has highest priority: a fresh attempt starts from scratch
      // regardless of anything else happening this cycle.
      st_q <= S_WAIT_LOCK;
    end else begin
      unique case (st_q)
        S_WAIT_LOCK :
          if (lock_ok)              st_q <= S_QUALIFY;
          else if (timeout_elapsed) st_q <= S_FAIL;
 
        S_QUALIFY :
          // ==========================================================
          // SUCCESS BEATS TIMEOUT ON THE SAME CYCLE, declared.
          //
          // A threshold met in the same cycle a timeout elapses is a
          // successful qualification -- the evidence exists. Failing
          // instead would discard a completed qualification because a
          // counter happened to reach its limit simultaneously
          // (section 15, mutation 9).
          // ==========================================================
          if (threshold_met)        st_q <= S_DONE;
          else if (!lock_ok)        st_q <= S_WAIT_LOCK;
          else if (timeout_elapsed) st_q <= S_FAIL;
 
        // Terminal. done and fail are STATES, so they cannot both assert.
        S_DONE, S_FAIL : ;
 
        default : st_q <= S_WAIT_LOCK;
      endcase
    end
  end
 
endmodule

// SVA over training_obs_capture, obs_qualifier and polling_progress.
// These assert the LOCAL progression contract. They assert NOTHING about
// the partner transmitting TS, about lock being achievable, or about
// Polling succeeding -- all of which depend on a partner and a channel
// this design does not control.
 
// ---- ENVIRONMENT ------------------------------------------------------
// A1: the parser's outputs are stable while parse_valid.
assume property (@(posedge clk) disable iff (!rst_n)
  parse_valid |-> !$isunknown({parse_kind, parse_lane, parse_link}));
// A2: state_entry is a single-cycle pulse.
assume property (@(posedge clk) disable iff (!rst_n)
  state_entry |=> !state_entry);
 
// ---- OBSERVATION OWNERSHIP --------------------------------------------
 
// P1: an observation's fields are stable while it waits.
property p_obs_stable;
  @(posedge clk) disable iff (!rst_n)
  (obs.valid && !obs_ready && !state_entry)
    |=> (obs.valid && $stable(obs.kind) && $stable(obs.lane_num)
                   && $stable(obs.link_num));
endproperty
a_stable : assert property (p_obs_stable);
 
// P2: STATE ENTRY DISCARDS a pending observation -- evidence from before
// this attempt must not contribute.
property p_entry_clears;
  @(posedge clk) disable iff (!rst_n)
  state_entry |=> !obs.valid;
endproperty
a_entry : assert property (p_entry_clears);
 
// P3: an observation that could not be held is REPORTED, never silent.
property p_overflow_reported;
  @(posedge clk) disable iff (!rst_n)
  (parse_valid && obs.valid && !obs_ready && !state_entry) |=> obs_overflow;
endproperty
a_ovf : assert property (p_overflow_reported);
 
// ---- QUALIFICATION ----------------------------------------------------
 
// P4: the count increments ONLY on a qualifying observation.
property p_count_only_on_qualify;
  @(posedge clk) disable iff (!rst_n)
  (count > $past(count)) |-> $past(qualifying);
endproperty
a_inc : assert property (p_count_only_on_qualify);
 
// P5: ONLY TS1 AND TS2 QUALIFY. An unrecognised or malformed training set
// must never contribute to progress.
property p_only_ts_qualifies;
  @(posedge clk) disable iff (!rst_n)
  (obs.valid && (obs.kind inside {OS_OTHER, OS_INVALID, OS_NONE}))
    |-> !obs_qualifies(obs);
endproperty
a_kind : assert property (p_only_ts_qualifies);
 
// P6: A DISQUALIFYING OBSERVATION RESETS TO ZERO, not to one.
// Consecutive is the requirement (section 7).
property p_bad_resets_fully;
  @(posedge clk) disable iff (!rst_n)
  disqualifying |=> (count == '0);
endproperty
a_reset : assert property (p_bad_resets_fully);
 
// P7: THE THRESHOLD CANNOT ASSERT EARLY. Restated independently of the
// module's own comparison, so an off-by-one fails rather than agreeing
// with itself.
property p_no_early_threshold;
  @(posedge clk) disable iff (!rst_n)
  threshold_met |-> (count >= CNT_W'(THRESH));
endproperty
a_early : assert property (p_no_early_threshold);
 
// P7b: and it DOES assert once the count reaches the threshold -- the
// complementary half, which an off-by-one in the other direction fails.
property p_no_late_threshold;
  @(posedge clk) disable iff (!rst_n)
  (count >= CNT_W'(THRESH)) |-> threshold_met;
endproperty
a_late : assert property (p_no_late_threshold);
 
// P8: the counter SATURATES -- it never exceeds the threshold and never
// wraps below it once reached.
property p_saturates;
  @(posedge clk) disable iff (!rst_n)
  count <= CNT_W'(THRESH);
endproperty
a_sat : assert property (p_saturates);
 
// P9: LOSING LOCK INVALIDATES the qualification history.
property p_lock_loss_restarts;
  @(posedge clk) disable iff (!rst_n)
  (!cdr_lock || !rx_aligned) |=> (count == '0);
endproperty
a_lock : assert property (p_lock_loss_restarts);
 
// ---- PROGRESSION ------------------------------------------------------
 
// P10: POLLING CANNOT COMPLETE WITHOUT BOTH lock/alignment AND
// qualification. The chapter's central progression property.
property p_done_needs_both;
  @(posedge clk) disable iff (!rst_n)
  $rose(polling_done) |-> ($past(cdr_lock) && $past(rx_aligned)
                                           && $past(threshold_met));
endproperty
a_done : assert property (p_done_needs_both);
 
// P11: done and fail are mutually exclusive.
property p_done_xor_fail;
  @(posedge clk) disable iff (!rst_n)
  !(polling_done && polling_fail);
endproperty
a_excl : assert property (p_done_xor_fail);
 
// P12: SUCCESS BEATS A SAME-CYCLE TIMEOUT -- the declared priority.
property p_success_beats_timeout;
  @(posedge clk) disable iff (!rst_n)
  (qualifying_now && threshold_met && timeout_elapsed) |=> polling_done;
endproperty
a_priority : assert property (p_success_beats_timeout);
 
// P13: observations are consumed only while qualifying -- a stale stream
// outside that window is not evidence.
property p_obs_only_when_qualifying;
  @(posedge clk) disable iff (!rst_n)
  obs_ready |-> qualifying_now;
endproperty
a_window : assert property (p_obs_only_when_qualifying);
 
// ---- SCOPE ------------------------------------------------------------
 
// P14: NO NORMAL TRAFFIC IN POLLING. Bound against Chapter 18.1's gate.
property p_no_traffic;
  @(posedge clk) disable iff (!rst_n)
  (dut_ltssm.cur_state == ST_POLLING) |-> !dut_gate.traffic_enabled;
endproperty
a_no_traffic : assert property (p_no_traffic);
 
// P15: reset and entry clear the qualification history.
property p_reset;
  @(posedge clk)
  !rst_n |=> ((count == '0) && !polling_done && !polling_fail && !obs.valid);
endproperty
a_reset : assert property (p_reset);