Detect — Is Anything There?

receiver present      → proceed toward Polling
receiver NOT present  → wait, and try again

Detect          → which lanes have a receiver present   ← candidates
Polling         → which lanes can carry trained communication
Configuration   → which lanes form one logical Link, and how wide it is

step             1     2     3     4     5     6     7     8     9
state           QUI   ACT   ACT   WAIT  WAIT  ACT   ACT   ACT   →POL
detect_start     0     1     0     0     0     1     0     0     0
detect_busy      0     1     1     0     0     1     1     1     0
detect_done      0     0     1     0     0     0     0     1     0
rx_present       -     -     0     -     -     -     -     1     -
 
attempt_id       0     1     1     1     1     2     2     2     2
result_valid     0     0     1     0     0     0     0     1     1
candidate_mask  00    00    00    00    00    00    00    0F    0F
 
traffic_enabled  0     0     0     0     0     0     0     0     0

// SYNTHESIZABLE. Digital wrapper around the PHY's receiver-detection
// operation.
// THAT RECEIVER DETECTION IS A PHY OPERATION WITH A DEFINED NOT-PRESENT
// OUTCOME is vendor-verified (section 1). The attempt-ID mechanism, the
// no-overlap rule and the error reports are ILLUSTRATIVE IMPLEMENTATION
// POLICY. The electrical operation itself is NOT modelled (section 9).
package detect_pkg;
 
  // An attempt identifier, wide enough that a stale result from an
  // abandoned attempt cannot alias the current one within any plausible
  // window. Two bits would wrap in four attempts; this is cheap insurance.
  localparam int ATT_W = 4;
 
  typedef struct packed {
    logic             valid;
    logic [ATT_W-1:0] attempt;
    logic             present;
  } detect_result_t;
 
endpackage

import detect_pkg::*;
 
module detect_attempt_ctrl #(
  parameter int LANES  = 16,
  // GUARDED. $clog2(1) is zero; LANES = 1 is a legal configuration.
  parameter int LANE_W = (LANES <= 1) ? 1 : $clog2(LANES)
) (
  input  logic clk,
  input  logic rst_n,
 
  // ---- From the Detect state logic ---------------------------------------
  input  logic              start_attempt,
  output logic              busy,
 
  // ---- To the PHY macro ---------------------------------------------------
  // A DECOUPLED command. The macro may not be able to accept immediately,
  // and the request must survive that without being reissued.
  output logic              detect_cmd_valid,
  input  logic              detect_cmd_ready,
 
  // ---- From the PHY macro -------------------------------------------------
  input  logic              detect_done,
  input  logic              detect_present,
 
  // ---- Result, attributed to a specific attempt --------------------------
  output detect_result_t    result,
  output logic [ATT_W-1:0]  attempt_id,
 
  output logic              err_start_while_busy,
  output logic              err_unowned_result
);
 
  generate
    if (LANES  < 1) $error("LANES must be at least 1");
    if (LANE_W < 1) $error("LANE_W must be at least 1");
  endgenerate
 
  typedef enum logic [1:0] { S_IDLE, S_ISSUE, S_WAIT, S_REPORT } st_e;
  st_e              st_q;
  logic [ATT_W-1:0] att_q;
  detect_result_t   res_q;
  logic             esb_q, eur_q;
 
  assign busy                 = (st_q != S_IDLE);
  assign attempt_id           = att_q;
  assign result               = res_q;
  assign err_start_while_busy = esb_q;
  assign err_unowned_result   = eur_q;
 
  // ==================================================================
  // THE COMMAND IS A LEVEL, HELD UNTIL THE MACRO ACCEPTS IT.
  //
  // Pulsing it for one cycle loses the request whenever the macro is not
  // ready that cycle -- and the machine then waits forever for a result
  // to an operation that was never started (section 14, mutation 1).
  // ==================================================================
  assign detect_cmd_valid = (st_q == S_ISSUE);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q  <= S_IDLE;
      att_q <= '0;
      res_q <= '0;
      esb_q <= 1'b0; eur_q <= 1'b0;
    end else begin
      unique case (st_q)
        S_IDLE :
          if (start_attempt) begin
            // A NEW ATTEMPT GETS A NEW IDENTIFIER, allocated here and
            // never again -- so a result can be checked against it.
            att_q <= att_q + ATT_W'(1);
            res_q.valid <= 1'b0;
            st_q  <= S_ISSUE;
          end
 
        // Hold the command until accepted. EXACTLY ONE acceptance per
        // start, because the state leaves S_ISSUE on the handshake.
        S_ISSUE :
          if (detect_cmd_ready) st_q <= S_WAIT;
 
        S_WAIT :
          if (detect_done) begin
            // ==========================================================
            // THE RESULT IS CAPTURED, NOT SAMPLED LATER.
            //
            // detect_present is only meaningful in the cycle detect_done
            // asserts. Reading it afterwards reads whatever the macro has
            // moved on to -- section 14's mutation 8.
            // ==========================================================
            res_q.valid   <= 1'b1;
            res_q.attempt <= att_q;
            res_q.present <= detect_present;
            st_q          <= S_REPORT;
          end
 
        S_REPORT :
          st_q <= S_IDLE;
 
        default : st_q <= S_IDLE;
      endcase
 
      // NO OVERLAPPING ATTEMPTS in this teaching model. A start while busy
      // is a caller error and is REPORTED rather than silently starting a
      // second operation whose result could not be attributed.
      if (start_attempt && busy) esb_q <= 1'b1;
 
      // A result arriving with no attempt outstanding cannot belong to
      // anything. Reported, never captured.
      if (detect_done && (st_q != S_WAIT)) eur_q <= 1'b1;
    end
  end
 
endmodule

// SYNTHESIZABLE. The wait between detection attempts.
// THE INTERVAL IS A PARAMETER. Section 1's source states 12 ms for that
// vendor device; this chapter does not publish it as a PCIe constant, and
// a design must take the required interval from the specification.
// Contract identical to Chapter 18.1 section 11's timer primitive.
module detect_interval #(
  parameter int CNT_W = 24
) (
  input  logic             clk,
  input  logic             rst_n,
  input  logic             enable,
  input  logic             restart,
  input  logic [CNT_W-1:0] limit,          // interval, in local cycles
 
  output logic [CNT_W-1:0] count,
  output logic             elapsed
);
 
  generate if (CNT_W < 1) $error("CNT_W must be at least 1"); endgenerate
 
  logic [CNT_W-1:0] cnt_q;
  assign count = cnt_q;
 
  // limit == 0 DISABLES, never expires instantly (Chapter 18.1 section 11).
  assign elapsed = enable && (limit != '0) && (cnt_q >= limit);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)               cnt_q <= '0;
    else if (restart)         cnt_q <= '0;          // restart beats counting
    else if (enable && !elapsed) cnt_q <= cnt_q + CNT_W'(1);   // saturates
  end
 
endmodule

import detect_pkg::*;
 
// SYNTHESIZABLE. Accumulate per-lane detection results into a candidate
// mask.
// THIS IS CANDIDATE PRESENCE, NOT NEGOTIATED WIDTH (section 7). Chapter
// 18.4 owns the reduction from candidates to a committed configuration.
module detect_lane_mask #(
  parameter int LANES  = 16,
  parameter int LANE_W = (LANES <= 1) ? 1 : $clog2(LANES)
) (
  input  logic clk,
  input  logic rst_n,
 
  // A new attempt invalidates everything the previous one found.
  input  logic              attempt_begin,
 
  input  logic              lane_result_valid,
  input  logic [LANE_W-1:0] lane_id,
  input  logic              lane_present,
 
  output logic [LANES-1:0]  candidate_lane_mask,
  output logic              lane_range_error
);
 
  generate
    if (LANES  < 1) $error("LANES must be at least 1");
    if (LANE_W < 1) $error("LANE_W must be at least 1");
    if ((LANES > 1) && ((1 << LANE_W) < LANES))
      $error("LANE_W too narrow to index LANES");
  endgenerate
 
  // RANGE SAFETY on an externally-supplied lane id, checked one bit wider
  // BEFORE any indexing. A LANE_W-wide value can name a lane that does not
  // exist whenever LANES is not a power of two.
  localparam int CHK = LANE_W + 1;
  wire lane_legal = (CHK'(lane_id) < CHK'(LANES));
 
  logic [LANES-1:0] mask_q;
  logic             err_q;
 
  assign candidate_lane_mask = mask_q;
  assign lane_range_error    = err_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      mask_q <= '0; err_q <= 1'b0;
    end else begin
      // ==============================================================
      // A NEW ATTEMPT CLEARS THE MASK, and this ordering is deliberate:
      // checked FIRST, so a result arriving in the same cycle as a new
      // attempt cannot be counted against the old one. Accumulating
      // across attempts would report lanes that were present once, ever
      // (section 14, mutation 6).
      // ==============================================================
      if (attempt_begin) begin
        mask_q <= '0;
      end else if (lane_result_valid && lane_legal) begin
        // ONE BIT, THE NAMED ONE. Assigning the whole vector here is
        // mutation 12, and it makes every lane share one lane's answer.
        mask_q[lane_id] <= lane_present;
      end
 
      if (lane_result_valid && !lane_legal) err_q <= 1'b1;
    end
  end
 
endmodule

// SVA over detect_attempt_ctrl, detect_interval and detect_lane_mask.
// These assert the ATTEMPT-OWNERSHIP contract. They assert NOTHING about
// the electrical detection operation (section 9), nothing about Polling
// (Chapter 18.3), and nothing about a receiver eventually existing --
// which depends on whether a card is plugged in.
 
// ---- ENVIRONMENT ------------------------------------------------------
// A1: detect_present is meaningful only in the cycle detect_done asserts.
assume property (@(posedge clk) disable iff (!rst_n)
  detect_done |-> !$isunknown(detect_present));
// A2: the macro asserts detect_done only for an operation it accepted.
assume property (@(posedge clk) disable iff (!rst_n)
  detect_done |-> $past(detect_cmd_valid && detect_cmd_ready, 1, 1, 64));
 
// ---- COMMAND OWNERSHIP ------------------------------------------------
 
// P1: THE COMMAND IS STABLE UNDER STALL. It is a held level, not a pulse.
property p_cmd_held;
  @(posedge clk) disable iff (!rst_n)
  (detect_cmd_valid && !detect_cmd_ready) |=> detect_cmd_valid;
endproperty
a_held : assert property (p_cmd_held);
 
// P2: ONE START, AT MOST ONE COMMAND ACCEPTANCE. The chapter's central
// ownership property -- section 14's counterexample fails it.
// (g_starts and g_cmds are testbench counters.)
property p_one_command_per_start;
  @(posedge clk) disable iff (!rst_n)
  (g_cmds <= g_starts);
endproperty
a_once : assert property (p_one_command_per_start);
 
// P2b: and the command drops immediately on acceptance -- it cannot be
// accepted twice in consecutive cycles.
property p_cmd_drops_on_accept;
  @(posedge clk) disable iff (!rst_n)
  (detect_cmd_valid && detect_cmd_ready) |=> !detect_cmd_valid;
endproperty
a_drop : assert property (p_cmd_drops_on_accept);
 
// ---- RESULT OWNERSHIP -------------------------------------------------
 
// P3: a result is captured only while an attempt is outstanding.
property p_result_needs_attempt;
  @(posedge clk) disable iff (!rst_n)
  $rose(result.valid) |-> ($past(st_q) == S_WAIT);
endproperty
a_owned : assert property (p_result_needs_attempt);
 
// P4: THE RESULT NAMES THE ATTEMPT THAT PRODUCED IT. Without this, a late
// result from an abandoned attempt is indistinguishable from a fresh one.
property p_result_attributed;
  @(posedge clk) disable iff (!rst_n)
  $rose(result.valid) |-> (result.attempt == attempt_id);
endproperty
a_attributed : assert property (p_result_attributed);
 
// P5: the captured result is STABLE -- present is not re-sampled later.
property p_result_stable;
  @(posedge clk) disable iff (!rst_n)
  (result.valid && !start_attempt) |=> $stable(result.present);
endproperty
a_stable : assert property (p_result_stable);
 
// P6: A NOT-PRESENT RESULT CANNOT REPORT PRESENCE. The property that
// forbids fabricating a partner (section 6).
property p_absent_is_absent;
  @(posedge clk) disable iff (!rst_n)
  ($rose(result.valid) && !$past(detect_present)) |-> !result.present;
endproperty
a_absent : assert property (p_absent_is_absent);
 
// P7: an unowned result is REPORTED and never captured.
property p_unowned_reported;
  @(posedge clk) disable iff (!rst_n)
  (detect_done && (st_q != S_WAIT)) |=> (err_unowned_result && !result.valid);
endproperty
a_unowned : assert property (p_unowned_reported);
 
// P8: NO OVERLAPPING ATTEMPTS -- a start while busy is refused and
// reported, not silently started.
property p_no_overlap;
  @(posedge clk) disable iff (!rst_n)
  (start_attempt && busy) |=> (err_start_while_busy && $stable(attempt_id));
endproperty
a_overlap : assert property (p_no_overlap);
 
// ---- LANE MASK --------------------------------------------------------
 
// P9: the mask changes only on a valid, in-range lane result or a new
// attempt.
property p_mask_change_owned;
  @(posedge clk) disable iff (!rst_n)
  (!$stable(candidate_lane_mask))
    |-> $past(attempt_begin || (lane_result_valid && lane_legal));
endproperty
a_mask : assert property (p_mask_change_owned);
 
// P10: a result writes ONE lane's bit -- never the whole vector.
property p_one_lane_bit;
  @(posedge clk) disable iff (!rst_n)
  ($past(lane_result_valid && lane_legal && !attempt_begin))
    |-> ($countones(candidate_lane_mask ^ $past(candidate_lane_mask)) <= 1);
endproperty
a_one_bit : assert property (p_one_lane_bit);
 
// P11: an out-of-range lane id touches nothing and is reported.
property p_lane_range;
  @(posedge clk) disable iff (!rst_n)
  (lane_result_valid && !lane_legal)
    |=> (lane_range_error && $stable(candidate_lane_mask));
endproperty
a_range : assert property (p_lane_range);
 
// P12: A NEW ATTEMPT CLEARS THE MASK -- no accumulation across attempts.
property p_mask_cleared;
  @(posedge clk) disable iff (!rst_n)
  attempt_begin |=> (candidate_lane_mask == '0);
endproperty
a_clear : assert property (p_mask_cleared);
 
// ---- TIMER ------------------------------------------------------------
 
// P13: the interval timer's three declared contracts (Chapter 18.1 §11).
property p_timer_restart;
  @(posedge clk) disable iff (!rst_n) restart |=> (count == '0);
endproperty
a_restart : assert property (p_timer_restart);
 
property p_timer_zero_disables;
  @(posedge clk) disable iff (!rst_n) (limit == '0) |-> !elapsed;
endproperty
a_zero : assert property (p_timer_zero_disables);
 
// ---- SCOPE ------------------------------------------------------------
 
// P14: NO NORMAL TRAFFIC IN DETECT. Bound against Chapter 18.1's gate.
property p_no_traffic_in_detect;
  @(posedge clk) disable iff (!rst_n)
  (dut_ltssm.cur_state == ST_DETECT) |-> !dut_gate.traffic_enabled;
endproperty
a_no_traffic : assert property (p_no_traffic_in_detect);
 
// P15: reset abandons any pending attempt and clears the result.
property p_reset;
  @(posedge clk)
  !rst_n |=> (!busy && !result.valid && (candidate_lane_mask == '0));
endproperty
a_reset : assert property (p_reset);