Disabled — A Link That Was Told to Stop

DISABLE0   announce      transmit TS1 with the Disable Link bit
DISABLE1   go quiet      transition to Electrical Idle
DISABLE2   confirm       WAIT for the partner's Electrical Idle Ordered Set,
                         then a minimum time afterwards
DISABLE3   remain        until a valid exit condition

// SYNTHESIZABLE. Normalized Disable types.
// THE TWO ENTRY PATHS are sourced (section 7). The reason encoding is
// internal diagnostic metadata -- it appears on no PCIe wire.
package disable_pkg;
 
  typedef struct packed {
    logic sw_link_disable;   // directed: Link Disable register write
    logic policy_disable;    // directed: platform/management policy
    logic remote_observed;   // observed: qualified TS with the Disable bit
  } disable_reason_t;
 
  function automatic bit any_reason(input disable_reason_t r); return (|r); endfunction
 
endpackage

import disable_pkg::*;
 
// SYNTHESIZABLE. Hold a DIRECTED disable request until the controller owns it.
// A CONFIGURATION WRITE IS A ONE-CYCLE PULSE. The Disabled controller may
// be busy -- finishing a previous sequence, or waiting on the ordered-set
// generator. A pulse wired straight into the entry condition is simply
// lost, and the software that wrote the register waits forever
// (section 16, mutation 1).
module disable_request_latch (
  input  logic clk,
  input  logic rst_n,
 
  input  logic sw_disable_pulse,      // Link Disable register write
  input  logic policy_disable_pulse,
 
  input  logic request_taken,         // the controller has ownership
  input  logic abort,                 // reset, or a dominating transition
 
  output disable_reason_t reason,
  output logic            request_pending
);
 
  disable_reason_t r_q;
  logic            p_q;
 
  assign reason          = r_q;
  assign request_pending = p_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || abort) begin
      r_q <= '0; p_q <= 1'b0;
    end else if (request_taken) begin
      // Consumed EXACTLY ONCE. The reason is NOT cleared -- it stays
      // readable for diagnostics until the next request (section 14).
      p_q <= 1'b0;
    end else begin
      // ACCUMULATE. Two sources can assert together, and a record that
      // kept only one would misattribute the disable.
      if (sw_disable_pulse)     begin r_q.sw_link_disable <= 1'b1; p_q <= 1'b1; end
      if (policy_disable_pulse) begin r_q.policy_disable  <= 1'b1; p_q <= 1'b1; end
    end
  end
 
endmodule

import disable_pkg::*;
 
// SYNTHESIZABLE. Qualify an OBSERVED disable instruction from the partner.
// SECTION 1 sources the mechanism -- "typically 2" consecutive TS OS with
// the control bit set -- AND the hazard: two consecutive corrupted TS can
// falsely assert it (section 9).
//
// THRESH IS PARAMETERISED AND ILLUSTRATIVE. Section 1 says "typically 2"
// for this implementation; this chapter publishes no normative count.
module disable_observed_qual #(
  parameter int THRESH = 2,
  parameter int CNT_W  = (THRESH <= 1) ? 1 : $clog2(THRESH + 1)
) (
  input  logic clk,
  input  logic rst_n,
 
  // ==============================================================
  // SECTION 1's MITIGATION, as an input. A system that never needs a
  // partner to disable its Link refuses the instruction entirely --
  // and the DIRECTED path is unaffected, exactly as the source states.
  // ==============================================================
  input  logic rx_ts_entry_enabled,
 
  input  logic obs_valid,          // a training observation arrived
  input  logic obs_disable_bit,    // ...with the Disable Link bit set
  input  logic restart,            // state entry, or lost lock
 
  output logic [CNT_W-1:0] count,
  output logic             observed_disable
);
 
  generate
    if (THRESH < 1) $error("THRESH must be at least 1");
    if ((1 << CNT_W) < (THRESH + 1)) $error("CNT_W too narrow for THRESH");
  endgenerate
 
  logic [CNT_W-1:0] cnt_q;
  assign count = cnt_q;
 
  // Gated by the enable, so a disabled path cannot fire at all.
  assign observed_disable = rx_ts_entry_enabled && (cnt_q >= CNT_W'(THRESH));
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)        cnt_q <= '0;
    else if (restart)  cnt_q <= '0;
    else if (obs_valid) begin
      // CONSECUTIVE, not cumulative. An observation WITHOUT the bit
      // resets to zero -- which is the entire defence against scattered
      // bit errors accumulating into an instruction (section 9).
      if (obs_disable_bit) begin
        if (cnt_q < CNT_W'(THRESH)) cnt_q <= cnt_q + CNT_W'(1);
      end else begin
        cnt_q <= '0;
      end
    end
  end
 
endmodule

// SYNTHESIZABLE. Command the ordered-set generator, and count what was
// ACTUALLY TRANSMITTED.
// SECTION 1's DISABLE0 is "Transmit 16 to 32 TS1 Ordered Sets w/ Disable
// Link bit asserted" -- a RANGE (section 6), so REQUIRED is parameterised
// within it rather than fixed.
module disable_os_sender #(
  parameter int REQUIRED = 16,
  parameter int CNT_W    = (REQUIRED <= 1) ? 1 : $clog2(REQUIRED + 1)
) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic start,
  input  logic abort,
 
  // ---- To the ordered-set generator. Decoupled. --------------------------
  output logic       os_valid,
  input  logic       os_ready,
  output logic [1:0] os_kind,        // normalized: TS1
  output logic       os_disable_bit, // the instruction being announced
 
  output logic [CNT_W-1:0] sent_count,
  output logic             send_done
);
 
  generate
    if (REQUIRED < 1) $error("REQUIRED must be at least 1");
    if ((1 << CNT_W) < (REQUIRED + 1)) $error("CNT_W too narrow");
  endgenerate
 
  logic [CNT_W-1:0] cnt_q;
  logic             busy_q;
 
  assign sent_count     = cnt_q;
  assign send_done      = (cnt_q >= CNT_W'(REQUIRED));
  assign os_valid       = busy_q && !send_done;
 
  // DESCRIPTOR FIELDS ARE CONSTANT while valid is held. They describe the
  // instruction, not the moment -- so there is nothing to become stale.
  assign os_kind        = 2'd1;      // TS1
  assign os_disable_bit = 1'b1;
 
  // ==================================================================
  // THE FIRE CONDITION. This is the whole block.
  //
  //   os_fire = os_valid && os_ready
  //
  // NOT `os_valid` alone. Counting offers instead of transfers completes
  // the announcement while the generator is stalled -- and section 15
  // measured it: 83.6% of stall patterns complete EARLY, and at
  // REQUIRED = 1 the count completes on a cycle where NOTHING WAS SENT.
  // ==================================================================
  wire os_fire = os_valid && os_ready;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || abort) begin
      cnt_q <= '0; busy_q <= 1'b0;
    end else if (start && !busy_q) begin
      cnt_q <= '0; busy_q <= 1'b1;
    end else if (busy_q) begin
      // SATURATES at REQUIRED -- and os_valid drops at send_done, so no
      // further transfers are offered. The upper end of section 1's
      // range is respected by construction.
      if (os_fire && (cnt_q < CNT_W'(REQUIRED))) cnt_q <= cnt_q + CNT_W'(1);
      if (send_done) busy_q <= 1'b0;
    end
  end
 
endmodule

import disable_pkg::*;
 
// SYNTHESIZABLE. Disabled-only controller.
// PHASES MAP ONTO SECTION 1's VERIFIED SUBSTATES and are named for them.
// This is not the LTSSM.
module disabled_controller (
  input  logic clk,
  input  logic rst_n,
 
  input  logic request_pending,     // section 12, directed
  input  logic observed_disable,    // section 12, qualified remote
  input  logic hot_reset_active,    // section 17's declared priority
 
  input  logic send_done,           // section 13: DISABLE0 complete
  input  logic idle_cmd_complete,   // PHY reached electrical idle
  input  logic partner_eios_seen,   // DISABLE2: the partner announced too
  input  logic min_idle_met,        // ...and held it for TX_IDLE_MIN
  input  logic exit_condition,      // section 11: not enumerated here
 
  output logic request_taken,
  output logic start_send,
  output logic start_idle,
  output logic in_disabled,
  output logic disabled_resident,
  output logic link_usable          // section 8's contract
);
 
  typedef enum logic [2:0] {
    S_IDLE, S_D0_ANNOUNCE, S_D1_GO_IDLE, S_D2_AWAIT_PARTNER, S_D3_RESIDENT
  } st_e;
  st_e st_q;
 
  assign request_taken     = (st_q == S_IDLE) && (request_pending || observed_disable)
                                              && !hot_reset_active;
  assign start_send        = (st_q == S_D0_ANNOUNCE);
  assign start_idle        = (st_q == S_D1_GO_IDLE);
  assign in_disabled       = (st_q != S_IDLE);
  assign disabled_resident = (st_q == S_D3_RESIDENT);
 
  // ==================================================================
  // SECTION 8's CONTRACT, AND IT IS ONE ASSIGNMENT.
  //
  // The configuration stops being USABLE the moment the sequence begins
  // -- not when the announcement finishes, and not at D3. Consumers act
  // on this continuously (Chapter 17.1 section 10), so a configuration
  // that reads usable during the disable sequence is an instruction to
  // transmit (section 16, mutation 8).
  //
  // Note this says nothing about whether the stored VALUES are cleared
  // (section 8) -- only that nothing above may act on them.
  // ==================================================================
  assign link_usable = (st_q == S_IDLE);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) st_q <= S_IDLE;
    else if (hot_reset_active) begin
      // DECLARED PRIORITY, and section 17 explains why it is declared
      // rather than claimed as normative.
      st_q <= S_IDLE;
    end else begin
      unique case (st_q)
        S_IDLE :
          if (request_pending || observed_disable) st_q <= S_D0_ANNOUNCE;
 
        // ---- DISABLE0: tell the partner FIRST (section 4) --------------
        S_D0_ANNOUNCE     : if (send_done)          st_q <= S_D1_GO_IDLE;
 
        // ---- DISABLE1: transition to Electrical Idle ------------------
        S_D1_GO_IDLE      : if (idle_cmd_complete)  st_q <= S_D2_AWAIT_PARTNER;
 
        // ---- DISABLE2: the partner confirms by going quiet too --------
        // BOTH conditions. Seeing the EIOS is not enough; section 1
        // requires a minimum time afterwards (section 5).
        S_D2_AWAIT_PARTNER: if (partner_eios_seen && min_idle_met)
                                                    st_q <= S_D3_RESIDENT;
 
        // ---- DISABLE3: residency, with NO TIMEOUT (section 10) --------
        S_D3_RESIDENT     : if (exit_condition)     st_q <= S_IDLE;
 
        default           :                         st_q <= S_IDLE;
      endcase
    end
  end
 
endmodule

import disable_pkg::*;
 
// SYNTHESIZABLE. Lab diagnostics. Saturating, edge-driven.
module disabled_diag #(parameter int CYC_W = 32, parameter int EVT_W = 16) (
  input  logic clk,
  input  logic rst_n,
  input  logic in_disabled,
  input  logic entry_pulse,
  input  logic exit_pulse,
  input  disable_reason_t reason,
  input  logic clear,
 
  output logic [EVT_W-1:0] disabled_entry_count,
  output logic [EVT_W-1:0] disabled_exit_count,
  output logic [CYC_W-1:0] cycles_disabled,
  output disable_reason_t  last_disable_reason
);
  logic [EVT_W-1:0] e_q, x_q; logic [CYC_W-1:0] c_q; disable_reason_t r_q;
  assign {disabled_entry_count, disabled_exit_count} = {e_q, x_q};
  assign cycles_disabled = c_q; assign last_disable_reason = r_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin e_q<='0; x_q<='0; c_q<='0; r_q<='0; end
    else begin
      if (in_disabled && !(&c_q)) c_q <= c_q + CYC_W'(1);
      // EDGE-driven (Chapter 18.6 section 15). A level would report
      // residency cycles as entries -- and Disabled residency is
      // unbounded, so the number would be spectacularly wrong.
      if (entry_pulse && !(&e_q)) begin e_q <= e_q + EVT_W'(1); r_q <= reason; end
      if (exit_pulse  && !(&x_q))       x_q <= x_q + EVT_W'(1);
    end
  end
endmodule

// SVA over the Disabled blocks. LOCAL contract only. Nothing asserts that
// Disabled is ever exited -- section 11 shows the exit conditions are not
// enumerated in this chapter's evidence, and DISABLE3 has no timeout.
 
// ---- ENVIRONMENT ------------------------------------------------------
assume property (@(posedge clk) disable iff (!rst_n)
  (up_valid && !up_ready) |=> (up_valid && $stable(up_payload)));
assume property (@(posedge clk) disable iff (!rst_n)
  sw_disable_pulse |=> !sw_disable_pulse);
 
// ---- REQUEST OWNERSHIP ------------------------------------------------
 
// P1: A DIRECTED DISABLE REQUEST IS NEVER LOST. A one-cycle register write
// arriving while the controller is busy must survive (section 12).
property p_request_held;
  @(posedge clk) disable iff (!rst_n)
  (request_pending && !request_taken && !abort) |=> request_pending;
endproperty
a_held : assert property (p_request_held);
 
// P1b: and it is consumed EXACTLY ONCE.
property p_request_once;
  @(posedge clk) disable iff (!rst_n)
  (request_pending && request_taken) |=> !request_pending;
endproperty
a_once : assert property (p_request_once);
 
// P2: THE OBSERVED PATH REQUIRES CONSECUTIVE EVIDENCE, and is gated by
// section 1's mitigation. This is the defence against a noisy channel
// accumulating scattered bit errors into a disable instruction (section 9).
property p_observed_needs_consecutive;
  @(posedge clk) disable iff (!rst_n)
  observed_disable |-> (rx_ts_entry_enabled && (count >= CNT_W'(THRESH)));
endproperty
a_obs : assert property (p_observed_needs_consecutive);
 
// P2b: a non-matching observation resets the count to ZERO, not down by one.
property p_reset_to_zero;
  @(posedge clk) disable iff (!rst_n)
  (obs_valid && !obs_disable_bit) |=> (count == '0);
endproperty
a_zero : assert property (p_reset_to_zero);
 
// ---- THE ANNOUNCEMENT -------------------------------------------------
 
// P3: THE COUNT TRACKS TRANSFERS, NEVER OFFERS. Section 15 measured the
// alternative: 83.6% of stall patterns complete early, and at REQUIRED = 1
// the announcement completes having sent nothing.
property p_count_on_fire;
  @(posedge clk) disable iff (!rst_n)
  (sent_count > $past(sent_count)) |-> ($past(os_valid) && $past(os_ready));
endproperty
a_fire : assert property (p_count_on_fire);
 
// P3b: and completion requires the full required count of ACTUAL transfers.
property p_done_needs_count;
  @(posedge clk) disable iff (!rst_n)
  send_done |-> (sent_count >= CNT_W'(REQUIRED));
endproperty
a_done : assert property (p_done_needs_count);
 
// P4: the descriptor is stable while the generator stalls. A partially
// announced instruction is not an instruction.
property p_descriptor_stable;
  @(posedge clk) disable iff (!rst_n)
  (os_valid && !os_ready) |=> (os_valid && $stable(os_kind)
                                        && $stable(os_disable_bit));
endproperty
a_desc : assert property (p_descriptor_stable);
 
// P4b: and the Disable Link bit is actually set. Omitting it makes the
// announcement indistinguishable from ordinary training (section 4).
property p_disable_bit_set;
  @(posedge clk) disable iff (!rst_n) os_valid |-> os_disable_bit;
endproperty
a_bit : assert property (p_disable_bit_set);
 
// P5: the electrical-idle command is held under stall.
property p_idle_held;
  @(posedge clk) disable iff (!rst_n)
  (idle_req_valid && !idle_req_ready) |=> idle_req_valid;
endproperty
a_idle : assert property (p_idle_held);
 
// ---- SEQUENCE ORDERING ------------------------------------------------
 
// P6: RESIDENCY REQUIRES THE PARTNER'S CONFIRMATION -- both conditions.
// Section 1's DISABLE2 waits for an Electrical Idle Ordered Set AND a
// minimum time afterwards (section 5).
property p_residency_needs_partner;
  @(posedge clk) disable iff (!rst_n)
  $rose(disabled_resident) |-> ($past(partner_eios_seen) && $past(min_idle_met));
endproperty
a_partner : assert property (p_residency_needs_partner);
 
// P6b: THE ANNOUNCEMENT PRECEDES THE SILENCE. Going idle before the
// instruction is sent is section 4's whole failure mode.
property p_announce_before_idle;
  @(posedge clk) disable iff (!rst_n)
  $rose(start_idle) |-> $past(send_done);
endproperty
a_order : assert property (p_announce_before_idle);
 
// ---- TRAFFIC AND CONFIGURATION ----------------------------------------
 
// P7: NO NORMAL PACKET TRANSFER WHILE DISABLED. Note this says nothing
// about the transmitter being silent -- DISABLE0 is transmitting (section 8).
property p_no_transfer;
  @(posedge clk) disable iff (!rst_n)
  in_disabled |-> !(up_valid && up_ready);
endproperty
a_noxfer : assert property (p_no_transfer);
 
// P8: a packet offered during the sequence remains UPSTREAM-OWNED.
property p_packet_survives;
  @(posedge clk) disable iff (!rst_n)
  (up_valid && in_disabled) |=> (up_valid || $past(up_ready));
endproperty
a_survive : assert property (p_packet_survives);
 
// P8b: no loss, stated symmetrically so gating one direction cannot
// satisfy it (Chapter 18.6 P3).
property p_symmetric;
  @(posedge clk) disable iff (!rst_n)
  (up_valid && up_ready) <-> (down_valid && down_ready);
endproperty
a_sym : assert property (p_symmetric);
 
// P9: THE OPERATIONAL CONFIGURATION IS NOT USABLE FROM THE MOMENT THE
// SEQUENCE BEGINS. Section 8's declared contract -- and note it asserts
// USABILITY, not that the stored values were cleared.
property p_not_usable;
  @(posedge clk) disable iff (!rst_n) in_disabled |-> !link_usable;
endproperty
a_usable : assert property (p_not_usable);
 
// P9b: and nothing downstream acts on a configuration that is not usable.
property p_consumer_gated;
  @(posedge clk) disable iff (!rst_n)
  !link_usable |-> (dut_distributor.active_mask == '0);
endproperty
a_consumer : assert property (p_consumer_gated);
 
// ---- DIAGNOSTICS AND RESET --------------------------------------------
 
// P10: ONE ENTRY COUNTED PER ENTRY, not per residency cycle. Disabled
// residency is UNBOUNDED (section 10), so a level-driven counter
// saturates almost immediately.
property p_entry_once;
  @(posedge clk) disable iff (!rst_n)
  (disabled_entry_count > $past(disabled_entry_count)) |-> $past(entry_pulse);
endproperty
a_cnt : assert property (p_entry_once);
 
// P11: the same for exits, keeping the pair within one of each other.
property p_counter_invariant;
  @(posedge clk) disable iff (!rst_n)
  (disabled_entry_count >= disabled_exit_count)
    && ((disabled_entry_count - disabled_exit_count) <= EVT_W'(1));
endproperty
a_inv : assert property (p_counter_invariant);
 
// P12: RESET CLEARS A PENDING DISABLE REQUEST. A request surviving reset
// would disable the Link immediately after it comes up (mutation 15).
property p_reset;
  @(posedge clk)
  !rst_n |=> (!request_pending && !in_disabled && link_usable);
endproperty
a_reset : assert property (p_reset);