Power Management DLLPs — A Request That Can Be Refused

request:     PM_Active_State_Request_L1     Data Link Layer   (DLLP)
acceptance:  PM_Request_Ack                 Data Link Layer   (DLLP)
refusal:     PM_Active_State_Nak            Transaction Layer (Message TLP)

step             1    2    3    4    5    6    7    8    9   10   11
pm_start         1    0    0    0    0    0    0    0    0    0    0
tx_inflight      1    1    0    0    0    0    0    0    0    0    0
retained_cnt     3    3    3    2    0    0    0    0    0    0    0
 
state           IDL  BLK  BLK  DRN  DRN  REQ  REQ  REQ  ACK  ACK  IDL
block_tlps       0    1    1    1    1    1    1    1    1    1    0
pm_send          0    0    0    0    0    1    1    1    0    0    0
 
rx_req_ack       0    0    0    0    0    0    0    1    0    0    0
rx_as_nak        0    0    0    0    0    0    0    0    0    0    0
quiesce_req      0    0    0    0    0    0    0    0    1    1    0

// SYNTHESIZABLE. Classify a received power-management DLLP.
// The packet names and their roles: VERIFIED (section 1). The Type values
// are PARAMETERS — this chapter does not publish the encodings.
// PM_ENTER_L23 is VERIFIED as a generated DLLP by source (c); only its
// Type ENCODING is unpublished, like the others.
package pm_dllp_pkg;
 
  typedef enum logic [2:0] {
    PM_NONE       = 3'd0,
    PM_ASR_L1     = 3'd1,   // PM_Active_State_Request_L1   (request, ASPM)
    PM_ENTER_L1   = 3'd2,   // PM_Enter_L1                  (request, PCI-PM)
    PM_ENTER_L23  = 3'd3,   // PM_Enter_L23                 (request, L2/L3)
    PM_REQ_ACK    = 3'd4    // PM_Request_Ack               (acceptance)
  } pm_kind_e;
 
  // PM_REQ_ACK is deliberately EXCLUDED. It is the answer, not a request,
  // and section 9 depends on that distinction.
  function automatic bit pm_is_request(input pm_kind_e k);
    return (k == PM_ASR_L1) || (k == PM_ENTER_L1) || (k == PM_ENTER_L23);
  endfunction
 
endpackage

import pm_dllp_pkg::*;
 
module pm_dllp_decode #(
  parameter logic [7:0] T_ASR_L1    = 8'h20,   // supplied by the integrator
  parameter logic [7:0] T_ENTER_L1  = 8'h21,
  parameter logic [7:0] T_REQ_ACK   = 8'h22,
  parameter logic [7:0] T_ENTER_L23 = 8'h23
) (
  input  logic       dllp_valid,
  input  logic [7:0] dllp_byte0,     // Type
  // Bytes 1..3 are deliberately NOT PORTS. A PM DLLP carries no information
  // beyond its Type (section 1, corroborated tier), and the safest way to
  // honour that is to make the payload UNREACHABLE from this module rather
  // than available and unused. P1 asserts the consequence.
  input  logic       dllp_integrity_ok,
 
  output pm_kind_e   pm_kind,
  output logic       pm_bad_integrity
);
 
  // INTEGRITY FIRST, for the fourth time in this curriculum (Chapters 14.1,
  // 14.5, 15.3, 15.4). Here the stake is a power-state negotiation started
  // from a corrupted Type byte.
  wire usable = dllp_valid && dllp_integrity_ok;
 
  always_comb begin
    pm_kind = PM_NONE;
    if (usable) begin
      unique case (dllp_byte0)
        T_ASR_L1    : pm_kind = PM_ASR_L1;
        T_ENTER_L1  : pm_kind = PM_ENTER_L1;
        T_REQ_ACK   : pm_kind = PM_REQ_ACK;
        T_ENTER_L23 : pm_kind = PM_ENTER_L23;
        default     : pm_kind = PM_NONE;
      endcase
    end
  end
 
  assign pm_bad_integrity = dllp_valid && !dllp_integrity_ok;
 
endmodule

import pm_dllp_pkg::*;
 
// SYNTHESIZABLE. Hold "a PM request of kind K is outstanding".
// That a request is transmitted repeatedly until answered is VERIFIED
// (section 1); that the receiver must therefore COLLAPSE repeats is the
// design consequence (section 4). The kind-change report is ILLUSTRATIVE.
module pm_request_hold (
  input  logic     clk,
  input  logic     rst_n,
 
  input  pm_kind_e pm_kind,          // from pm_dllp_decode, combinational
 
  // The local decision, from the responding port's policy (NOT modelled,
  // section 3).
  input  logic     resolve,          // this request has been answered
  input  logic     abort,            // negotiation abandoned
 
  output logic     req_outstanding,
  output pm_kind_e req_kind,
  output logic     pm_kind_change    // a DIFFERENT request arrived
);
 
  logic     out_q;
  pm_kind_e kind_q;
  logic     chg_q;
 
  assign req_outstanding = out_q;
  assign req_kind        = kind_q;
  assign pm_kind_change  = chg_q;
 
  wire incoming_req = pm_is_request(pm_kind);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      out_q <= 1'b0; kind_q <= PM_NONE; chg_q <= 1'b0;
    end else begin
      // Resolution has priority. A request answered this cycle is finished
      // even if another copy of it arrives in the same cycle — the remote
      // port has not seen the answer yet and is still repeating.
      if (resolve || abort) begin
        out_q  <= 1'b0;
        kind_q <= PM_NONE;
      end else if (incoming_req) begin
        // IDEMPOTENT. A repeat of the SAME kind sets a bit that is already
        // set and rewrites a field with its own value — no counter, no
        // queue, no restart. Five hundred arrivals, one outstanding request.
        out_q  <= 1'b1;
        kind_q <= pm_kind;
      end
 
      // A DIFFERENT request while one is outstanding is a new negotiation,
      // not a repeat. Reported rather than silently absorbed (section 4).
      if (incoming_req && out_q && (pm_kind != kind_q)) chg_q <= 1'b1;
    end
  end
 
endmodule

import pm_dllp_pkg::*;
 
// SYNTHESIZABLE. Requesting-side power-management front end.
// The sequence -- block TLPs, drain in-flight, WAIT FOR THE REPLAY BUFFER
// TO EMPTY, then transmit the request repeatedly until answered -- is
// VERIFIED (section 1, source b). The two separate response ports follow
// from the refusal being a Message TLP (section 6). State encoding and
// the abort input: ILLUSTRATIVE.
module pm_request_frontend #(
  parameter int CNT_W = 6            // width of the retained-occupancy count
) (
  input  logic             clk,
  input  logic             rst_n,
 
  // ---- Local request ----------------------------------------------------
  input  logic             pm_start,
  input  pm_kind_e         pm_start_kind,
  input  logic             abort,
 
  // ---- Transmit-path status --------------------------------------------
  input  logic             tx_tlp_inflight,      // a TLP is mid-transmission
  // Chapter 14.4's RETAINED OCCUPANCY. Not a pointer comparison -- the
  // counter, because emptiness inferred from pointer equality is the bug
  // that would let this FSM proceed with packets still retained.
  input  logic [CNT_W-1:0] retained_count,
 
  // ---- Responses, from TWO DIFFERENT LAYERS (section 6) -----------------
  input  logic             rx_pm_req_ack,   // DLLP,        from section 8
  input  logic             rx_pm_as_nak,    // Message TLP, from the Message
                                            // decoder -- NOT a DLLP
 
  // ---- Outputs ----------------------------------------------------------
  output logic             block_new_tlps,
  output logic             pm_send,         // LEVEL: transmit continuously
  output pm_kind_e         pm_send_kind,
  output logic             quiesce_req,     // handoff -- Module 18 owns what
                                            // happens next
  output logic             pm_refused,
  output logic             pm_done
);
 
  typedef enum logic [2:0] {
    S_IDLE, S_BLOCK, S_DRAIN, S_REQUEST, S_ACCEPTED, S_REFUSED
  } st_e;
 
  st_e      st_q;
  pm_kind_e kind_q;
 
  // THE ENTRY CONDITION (section 5). Both halves are required: no TLP may be
  // mid-transmission, and NOTHING may remain unacknowledged.
  wire tx_quiet   = !tx_tlp_inflight;
  wire replay_empty = (retained_count == '0);
 
  assign block_new_tlps = (st_q != S_IDLE);
  assign pm_send        = (st_q == S_REQUEST);
  assign pm_send_kind   = kind_q;
  assign quiesce_req    = (st_q == S_ACCEPTED);
  assign pm_refused     = (st_q == S_REFUSED);
  assign pm_done        = (st_q == S_ACCEPTED) || (st_q == S_REFUSED);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      st_q <= S_IDLE; kind_q <= PM_NONE;
    end else if (abort && (st_q != S_IDLE)) begin
      st_q <= S_IDLE; kind_q <= PM_NONE;
    end else begin
      unique case (st_q)
        S_IDLE :
          if (pm_start && pm_is_request(pm_start_kind)) begin
            st_q   <= S_BLOCK;
            kind_q <= pm_start_kind;
          end
 
        // BLOCK FIRST. block_new_tlps is already asserted here, so the
        // source is stopped before anything waits on it. Waiting for the
        // buffer to drain while still accepting new work may never converge.
        S_BLOCK :
          if (tx_quiet) st_q <= S_DRAIN;
 
        // WAIT FOR RETIREMENT. This FSM cannot make this happen -- it waits
        // for the PARTNER's acknowledgements (Chapter 14.2).
        S_DRAIN :
          if (replay_empty) st_q <= S_REQUEST;
 
        // TRANSMIT REPEATEDLY. pm_send is a level. The DLLP transmit path
        // emits the request for as long as it is held (section 1).
        S_REQUEST :
          // Acceptance is checked first. Both answers arriving together is
          // a protocol violation, and preferring the DLLP keeps the
          // resolution deterministic rather than undefined.
          if      (rx_pm_req_ack) st_q <= S_ACCEPTED;
          else if (rx_pm_as_nak)  st_q <= S_REFUSED;
 
        // REFUSAL RESUMES NORMAL OPERATION on the next cycle -- source (a):
        // on a rejection the controller "aborts the ASPM L1 entry and
        // continues to send TLPs normally". Holding block_new_tlps here
        // would stall the transmit path over a routine answer.
        S_REFUSED :
          st_q <= S_IDLE;
 
        // ACCEPTANCE is terminal. quiesce_req stays asserted, and the
        // consumer -- Module 18's -- releases the FSM by pulsing abort.
        S_ACCEPTED : ;
 
        default : st_q <= S_IDLE;
      endcase
    end
  end
 
endmodule

// SVA over pm_dllp_decode, pm_request_hold and pm_request_frontend, bound
// against Chapter 14.4's replay buffer and 14.2's retirement window.
// These assert the verified sequencing of section 1 and the LOCAL
// negotiation contract. Nothing here asserts request repetition intervals or
// response timeouts (not published, section 1), anything about the LTSSM or
// link states (Module 18), or anything about credits (Module 16).
 
// ---- ENVIRONMENT -----------------------------------------------------
// A1: retained_count is Chapter 14.4's occupancy for THIS transmit path.
assume property (@(posedge clk) disable iff (!rst_n)
  retained_count == dut_replay_buffer.occupancy);
// A2: the two responses never arrive in the same cycle -- one request has
// one answer. Violation is a protocol error, not a design case.
assume property (@(posedge clk) disable iff (!rst_n)
  !(rx_pm_req_ack && rx_pm_as_nak));
 
// ---- DECODE ----------------------------------------------------------
 
// P1: PAYLOAD INDEPENDENCE. The decoded kind is a function of the Type byte
// and the integrity verdict alone (section 1, corroborated tier -- so the
// design is made correct either way).
property p_type_only;
  @(posedge clk) disable iff (!rst_n)
  (dllp_valid && $stable(dllp_byte0) && $stable(dllp_integrity_ok))
    |-> $stable(pm_kind);
endproperty
a_type_only : assert property (p_type_only);
 
// P2: a corrupted DLLP never becomes a PM event. Here the stake is a
// power-state negotiation started from a corrupted byte.
property p_corrupt_never_decodes;
  @(posedge clk) disable iff (!rst_n)
  (dllp_valid && !dllp_integrity_ok) |-> (pm_kind == PM_NONE);
endproperty
a_corrupt : assert property (p_corrupt_never_decodes);
 
// P3: the two L1 requests stay distinct (section 3).
property p_l1_requests_distinct;
  @(posedge clk) disable iff (!rst_n)
  (dllp_valid && dllp_integrity_ok && (dllp_byte0 == T_ASR_L1))
    |-> (pm_kind == PM_ASR_L1);
endproperty
a_distinct : assert property (p_l1_requests_distinct);
 
// ---- IDEMPOTENCE -----------------------------------------------------
 
// P4: THE CHAPTER'S CENTRAL PROPERTY. N identical requests produce ONE
// outstanding request. A queue fails this on the second arrival.
// (req_assert_count is a testbench counter of req_outstanding rising edges.)
property p_repeats_collapse;
  @(posedge clk) disable iff (!rst_n)
  (req_outstanding && $stable(req_kind) && !resolve && !abort)
    |=> (req_outstanding && $stable(req_kind));
endproperty
a_idempotent : assert property (p_repeats_collapse);
 
// P4b: no restart. An outstanding request is not re-raised by a repeat.
property p_no_restart_on_repeat;
  @(posedge clk) disable iff (!rst_n)
  ($rose(req_outstanding)) |-> !$past(req_outstanding);
endproperty
a_no_restart : assert property (p_no_restart_on_repeat);
 
// ---- THE ENTRY CONDITION ---------------------------------------------
 
// P5: THE RELIABILITY GATE (section 5). A request is NEVER transmitted while
// anything remains unacknowledged. Bound against Chapter 14.4 via A1.
property p_no_request_while_retained;
  @(posedge clk) disable iff (!rst_n)
  pm_send |-> (retained_count == '0);
endproperty
a_gate : assert property (p_no_request_while_retained);
 
// P6: ORDERING. New TLP transmission is blocked before the drain wait
// begins, or the wait may never converge.
property p_block_before_drain;
  @(posedge clk) disable iff (!rst_n)
  (st_q == S_DRAIN) |-> block_new_tlps;
endproperty
a_order : assert property (p_block_before_drain);
 
// P7: the request is a LEVEL, held until answered (section 1).
property p_request_held_until_answered;
  @(posedge clk) disable iff (!rst_n)
  (pm_send && !rx_pm_req_ack && !rx_pm_as_nak && !abort)
    |=> (pm_send && $stable(pm_send_kind));
endproperty
a_level : assert property (p_request_held_until_answered);
 
// ---- THE TWO NAME TRAPS (section 6) ----------------------------------
 
// P8: PM_Request_Ack NEVER advances reliability retirement. It carries no
// sequence number; retiring against it would release packets whose delivery
// is unresolved (Chapter 14.1 section 2).
property p_req_ack_is_not_an_ack;
  @(posedge clk) disable iff (!rst_n)
  (pm_kind == PM_REQ_ACK) |-> !dut_retire_window.retire_valid;
endproperty
a_not_an_ack : assert property (p_req_ack_is_not_an_ack);
 
// P9: PM_Active_State_Nak NEVER arms a replay. It is a Message TLP meaning
// "no", not Chapter 15.4's Nak.
property p_as_nak_is_not_a_nak;
  @(posedge clk) disable iff (!rst_n)
  rx_pm_as_nak |-> !dut_retry_controller.arm_replay;
endproperty
a_not_a_nak : assert property (p_as_nak_is_not_a_nak);
 
// P10: SCOPE. A PM DLLP never touches flow-control state (Module 16 is not
// consumed by this chapter, and a design must not blur the categories).
property p_pm_touches_no_credits;
  @(posedge clk) disable iff (!rst_n)
  (pm_kind != PM_NONE) |-> !dut_fc_tracker.ret_valid;
endproperty
a_scope : assert property (p_pm_touches_no_credits);
 
// P11: quiesce is requested only after an ACCEPTANCE -- never from
// S_REQUEST, and never after a refusal.
property p_quiesce_only_after_accept;
  @(posedge clk) disable iff (!rst_n)
  quiesce_req |-> $past(rx_pm_req_ack || (st_q == S_ACCEPTED));
endproperty
a_quiesce : assert property (p_quiesce_only_after_accept);
 
// P12: a refusal ends the negotiation without quiescing (section 6).
property p_refusal_does_not_quiesce;
  @(posedge clk) disable iff (!rst_n)
  pm_refused |-> !quiesce_req;
endproperty
a_refusal : assert property (p_refusal_does_not_quiesce);
 
// P13: BOUNDED RESOLUTION. Once a response arrives, the FSM leaves
// S_REQUEST on the next cycle. A deterministic local transition, so this is
// a bound and not a fairness assumption (Chapter 14.3 section 13).
property p_response_resolves_next_cycle;
  @(posedge clk) disable iff (!rst_n)
  ((st_q == S_REQUEST) && (rx_pm_req_ack || rx_pm_as_nak))
    |=> (st_q inside {S_ACCEPTED, S_REFUSED});
endproperty
a_bounded : assert property (p_response_resolves_next_cycle);
 
// P14: reset clears the negotiation.
property p_reset_clears;
  @(posedge clk)
  !rst_n |=> (!pm_send && !quiesce_req && !req_outstanding);
endproperty
a_reset : assert property (p_reset_clears);

requests transmitted        ← wire observations, MANY per negotiation
negotiations started        ← ONE per request/answer exchange
retirement events           ← Chapter 14.2's, and PM must contribute ZERO
replay arms                 ← Chapter 14.3's, and PM must contribute ZERO