LTSSM Issues — Which Contract Inside the State Is Wrong?

// SYNTHESIZABLE. LTSSM contract-debug types, on 18.1 §10's state enum.
package ltssm_contract_pkg;
  import ltssm_pkg::*;                       // ST_DETECT, ST_POLLING, ... (18.1)
 
  parameter int N_GUARD  = 8;
  parameter int GUARD_W  = (N_GUARD <= 1) ? 1 : $clog2(N_GUARD);
  parameter int HIST_D   = 16;
  parameter int HIST_W   = (HIST_D <= 1) ? 1 : $clog2(HIST_D);
  parameter int N_MILE   = 4;
  parameter int EPOCH_W  = 8;
 
  // LOCAL guard identity. WHICH guards a state has is Module 18's; this is
  // only how this design exposes them (§5).
  typedef enum logic [GUARD_W-1:0] {
    G_RESET   = 3'd0,   // priority 1 -- outranks everything (§4)
    G_DISABLE = 3'd1,   // priority 2
    G_SUCCESS = 3'd2,   // priority 3 -- deliberately above timeout
    G_TIMEOUT = 3'd3,   // priority 4
    G_OTHER   = 3'd4
  } guard_e;
 
  typedef struct packed {
    logic [3:0]         from_state;
    logic [3:0]         to_state;
    logic [N_GUARD-1:0] guards_true;    // ALL guards true at the decision
    guard_e             selected;       // the one priority chose
    logic [EPOCH_W-1:0] epoch;
    logic [31:0]        residency;
    logic               stale_rejected; // an event was dropped this cycle
    logic [31:0]        cycle;
  } contract_event_t;
 
endpackage

import ltssm_contract_pkg::*;
 
// SYNTHESIZABLE. THE GUARD VECTOR (§5). The instrument that separates
// faults residency cannot: 25.3 §13's two identical rows differ by one bit
// here. Guards are exposed INDIVIDUALLY, never collapsed into `can_exit`.
module ltssm_guard_observe (
  input  logic clk,
  input  logic rst_n,
  input  logic g_reset,
  input  logic g_disable,
  input  logic g_success,
  input  logic g_timeout,
  input  logic g_other,
  input  logic dbg_clear,
 
  output logic [N_GUARD-1:0] guards_true,
  output guard_e             selected,
  output logic               any_guard,
  output logic               multiple_guards,   // more than one true at once
  output logic [31:0]        guard_true_count [N_GUARD],
  output logic [31:0]        contention_count   // cycles with >1 guard true
);
  logic [31:0] cnt_q [N_GUARD], cont_q;
 
  always_comb begin
    guards_true = '0;
    guards_true[G_RESET]   = g_reset;
    guards_true[G_DISABLE] = g_disable;
    guards_true[G_SUCCESS] = g_success;
    guards_true[G_TIMEOUT] = g_timeout;
    guards_true[G_OTHER]   = g_other;
    any_guard       = |guards_true;
    multiple_guards = !$onehot0(guards_true);
    // THE DECLARED PRIORITY (§4), in one place, matching the FSM's own.
    if      (g_reset)   selected = G_RESET;
    else if (g_disable) selected = G_DISABLE;
    else if (g_success) selected = G_SUCCESS;   // success ABOVE timeout
    else if (g_timeout) selected = G_TIMEOUT;
    else                selected = G_OTHER;
  end
 
  always_comb for (int i=0;i<N_GUARD;i++) guard_true_count[i]=cnt_q[i];
  assign contention_count = cont_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || dbg_clear) begin
      cont_q<='0; for (int i=0;i<N_GUARD;i++) cnt_q[i]<='0;
    end else begin
      for (int i=0;i<N_GUARD;i++)
        if (guards_true[i] && !(&cnt_q[i])) cnt_q[i] <= cnt_q[i] + 32'd1;
      // Contention is the evidence that §4's priority MATTERS in this design.
      if (multiple_guards && !(&cont_q)) cont_q <= cont_q + 32'd1;
    end
  end
endmodule

import ltssm_contract_pkg::*;
 
// SYNTHESIZABLE. State epoch and stale-event rejection (§8).
// §15: without this, 12,738 transitions in 200,000 cycles were fired by an
// event that belonged to a PREVIOUS state. The epoch is LOCAL state and is
// never transmitted (23.6 §7's warning).
module ltssm_state_epoch (
  input  logic clk,
  input  logic rst_n,
  input  logic       state_enter,
  input  logic       event_valid,
  input  logic [EPOCH_W-1:0] event_epoch,      // stamped AT DETECTION
  input  logic       dbg_clear,
 
  output logic [EPOCH_W-1:0] epoch,
  output logic               event_qualified,   // safe for a guard to use
  output logic               event_stale,
  output logic [31:0]        stale_rejected_count
);
  logic [EPOCH_W-1:0] ep_q;
  logic [31:0]        stale_q;
 
  assign epoch           = ep_q;
  assign event_stale     = event_valid && (event_epoch != ep_q);
  assign event_qualified = event_valid && (event_epoch == ep_q);
  assign stale_rejected_count = stale_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || dbg_clear) begin ep_q <= '0; stale_q <= '0; end
    else begin
      if (state_enter) ep_q <= ep_q + EPOCH_W'(1);
      // COUNTED, never silently dropped: a design that discards quietly
      // looks identical to one that never received the event (§8).
      if (event_stale && !(&stale_q)) stale_q <= stale_q + 32'd1;
    end
  end
endmodule

import ltssm_contract_pkg::*;
 
// SYNTHESIZABLE. Next-state timer (§7).
// §15: `== LIMIT` is one cycle late at unit steps and NEVER FIRES at steps
// of 3 or more -- a stuck state with a healthy-looking counter. It missed
// in 20.0% of trials with a counter stepping 1-3.
module ltssm_state_timer #(parameter int unsigned LIMIT = 1024) (
  input  logic clk,
  input  logic rst_n,
  input  logic        state_enter,
  input  logic [7:0]  step,                 // may exceed 1 (lane-aggregated)
  input  logic        tick,
  input  logic        dbg_clear,
 
  output logic [31:0] timer,
  output logic        timer_done,
  output logic [31:0] worst_timer,
  output logic        entered_expired       // sticky: entry did not clear (§9)
);
  logic [31:0] t_q, worst_q;
  logic        ee_q;
  logic [32:0] t_next;
 
  // NEXT-STATE comparison, and >= rather than == so an overshoot cannot
  // step over the threshold (23.6 pattern 9).
  always_comb t_next = {1'b0, t_q} + (tick ? 33'(step) : 33'd0);
  assign timer      = t_q;
  assign timer_done = (t_next >= 33'(LIMIT));
  assign worst_timer = worst_q;
  assign entered_expired = ee_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || dbg_clear) begin t_q<='0; worst_q<='0; ee_q<=1'b0; end
    else if (state_enter) begin
      // ENTRY ACTION: the timer starts at zero. A state that enters with a
      // non-zero timer can expire immediately (§9, §12's figure).
      if (t_q != '0 && worst_q < t_q) worst_q <= t_q;
      t_q <= '0;
    end else begin
      t_q <= t_next[31:0];
      // If a guard is already satisfied on the entry cycle, the entry
      // actions did not run. Report it rather than transition silently.
      if (timer_done && $past(state_enter)) ee_q <= 1'b1;
    end
  end
endmodule

import ltssm_contract_pkg::*;
 
// SYNTHESIZABLE. Entry-action observer (§9).
// §15: with entry actions omitted, 199,993 of 200,000 transitions entered
// a state with dirty counters. This block turns that into one sticky bit.
module ltssm_entry_check (
  input  logic clk,
  input  logic rst_n,
  input  logic        state_enter,
  input  logic [31:0] state_timer,
  input  logic [31:0] event_count,
  input  logic [15:0] lane_mask,
  input  logic        dbg_clear,
 
  output logic        entry_dirty,           // sticky
  output logic [3:0]  dirty_fields,          // which one was not cleared
  output logic [31:0] dirty_entry_count
);
  logic ed_q; logic [3:0] df_q; logic [31:0] cnt_q;
 
  assign entry_dirty=ed_q; assign dirty_fields=df_q; assign dirty_entry_count=cnt_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || dbg_clear) begin ed_q<=1'b0; df_q<='0; cnt_q<='0; end
    else if ($past(state_enter)) begin
      // One cycle AFTER entry, the state's own counters must read zero.
      automatic logic [3:0] d = {1'b0,
                                 (lane_mask   != '0),
                                 (event_count != '0),
                                 (state_timer != '0)};
      if (d != '0) begin
        if (!ed_q) begin ed_q <= 1'b1; df_q <= d; end   // FIRST one, latched
        if (!(&cnt_q)) cnt_q <= cnt_q + 32'd1;
      end
    end
  end
endmodule

import ltssm_contract_pkg::*;
 
// SYNTHESIZABLE. Transition-reason capture with the full guard vector.
// Records the INPUTS and the DECISION separately (§5) -- a history that
// stores only the destination cannot answer "why".
module ltssm_transition_history (
  input  logic clk,
  input  logic rst_n,
  input  logic               state_enter,
  input  logic [3:0]         state,
  input  logic [3:0]         prev_state,
  input  logic [N_GUARD-1:0] guards_true,
  input  guard_e             selected,
  input  logic [EPOCH_W-1:0] epoch,
  input  logic [31:0]        residency,
  input  logic               stale_rejected,
  input  logic [31:0]        cycle,
  input  logic               freeze,
  input  logic               dbg_clear,
 
  output contract_event_t history [HIST_D],
  output logic [HIST_W-1:0] wr_ptr,
  output logic              wrapped,
  output logic [31:0]       dropped_while_frozen
);
  contract_event_t h_q [HIST_D];
  logic [HIST_W-1:0] wr_q; logic wrap_q; logic [31:0] drop_q;
 
  always_comb for (int i=0;i<HIST_D;i++) history[i]=h_q[i];
  assign wr_ptr=wr_q; assign wrapped=wrap_q; assign dropped_while_frozen=drop_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || dbg_clear) begin
      wr_q<='0; wrap_q<=1'b0; drop_q<='0;
      for (int i=0;i<HIST_D;i++) h_q[i]<='0;
    end else if (state_enter) begin
      if (freeze) begin
        if (!(&drop_q)) drop_q <= drop_q + 32'd1;
      end else begin
        // Sampled WITH the transition. Reading guards afterwards gets the
        // NEW state's conditions (§5, §17 mutation 11).
        h_q[wr_q] <= '{from_state: prev_state, to_state: state,
                       guards_true: guards_true, selected: selected,
                       epoch: epoch, residency: residency,
                       stale_rejected: stale_rejected, cycle: cycle};
        if (HIST_D == 1) wrap_q <= 1'b1;
        else if (wr_q == HIST_W'(HIST_D-1)) begin wr_q<='0; wrap_q<=1'b1; end
        else wr_q <= wr_q + HIST_W'(1);
      end
    end
  end
endmodule

import ltssm_contract_pkg::*;
 
// SYNTHESIZABLE. Progress milestones and loop detection (§10).
// §15: two runs both re-entered 1,002 times; one gained 3 milestones and
// one gained 0. Re-entry count CANNOT separate them -- progress can.
module ltssm_progress_loop #(parameter int unsigned LOOP_LIMIT = 64) (
  input  logic clk,
  input  logic rst_n,
  input  logic       state_enter,
  input  logic [3:0] state,
  input  logic [3:0] prev_state,
  input  logic       ms_speed_phase_done,
  input  logic       ms_more_lanes_locked,
  input  logic       ms_wider_width,
  input  logic       ms_packets_flowed,
  input  logic       dbg_clear,
 
  output logic [N_MILE-1:0] milestones,
  output logic [31:0]       reentry_count,
  output logic              loop_no_progress,     // sticky: the REAL finding
  output logic [31:0]       entries_since_progress
);
  logic [N_MILE-1:0] ms_q;
  logic [31:0] re_q, since_q;
  logic loop_q;
  logic [3:0] last_from_q, last_to_q;
 
  assign milestones=ms_q; assign reentry_count=re_q;
  assign loop_no_progress=loop_q; assign entries_since_progress=since_q;
 
  logic gained;
  assign gained = (ms_speed_phase_done  && !ms_q[0])
               || (ms_more_lanes_locked && !ms_q[1])
               || (ms_wider_width       && !ms_q[2])
               || (ms_packets_flowed    && !ms_q[3]);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || dbg_clear) begin
      ms_q<='0; re_q<='0; since_q<='0; loop_q<=1'b0;
      last_from_q<='0; last_to_q<='0;
    end else begin
      // Milestones are MONOTONIC within the epoch (§10, P23).
      if (ms_speed_phase_done)  ms_q[0] <= 1'b1;
      if (ms_more_lanes_locked) ms_q[1] <= 1'b1;
      if (ms_wider_width)       ms_q[2] <= 1'b1;
      if (ms_packets_flowed)    ms_q[3] <= 1'b1;
 
      if (state_enter) begin
        // A repeat of the SAME transition pair is a re-entry.
        if ((prev_state == last_from_q) && (state == last_to_q)) begin
          if (!(&re_q)) re_q <= re_q + 32'd1;
          if (gained) since_q <= '0;
          else begin
            if (!(&since_q)) since_q <= since_q + 32'd1;
            // A loop is re-entry WITHOUT progress -- never repetition alone.
            if (since_q >= 32'(LOOP_LIMIT)) loop_q <= 1'b1;
          end
        end else if (gained) since_q <= '0;
        last_from_q <= prev_state; last_to_q <= state;
      end
    end
  end
endmodule

// ---- GUARDS AND PRIORITY (§4, §5) -------------------------------
// P1: guards are exposed individually, never collapsed.
property p_guards_individual;
  @(posedge clk) disable iff (!rst_n)
    any_guard |-> (|guards_true);
endproperty
 
// P2: the selected guard was actually true.
property p_selected_was_true;
  @(posedge clk) disable iff (!rst_n)
    any_guard |-> guards_true[selected];
endproperty
 
// P3: with no guard true, the state does not change.
property p_no_guard_no_transition;
  @(posedge clk) disable iff (!rst_n)
    (!any_guard) |=> $stable(state);
endproperty
 
// P4: RESET OUTRANKS EVERYTHING. A machine that can ignore reset because
// another guard was also true is not resettable (§4).
property p_reset_priority_absolute;
  @(posedge clk) disable iff (!rst_n)
    guards_true[G_RESET] |-> (selected == G_RESET);
endproperty
 
// P5: success outranks timeout -- the declared policy (§4).
// §15: inverting this took the wrong edge 1,333 times.
property p_success_over_timeout;
  @(posedge clk) disable iff (!rst_n)
    (guards_true[G_SUCCESS] && guards_true[G_TIMEOUT] && !guards_true[G_RESET]
      && !guards_true[G_DISABLE]) |-> (selected == G_SUCCESS);
endproperty
 
// P6: the observer's priority matches the FSM's actual choice.
property p_observer_matches_fsm;
  @(posedge clk) disable iff (!rst_n)
    (state_enter && !freeze) |=> (history[$past(wr_ptr)].selected == $past(selected));
endproperty
 
// P7: contention is COUNTED -- evidence that priority matters here.
property p_contention_counted;
  @(posedge clk) disable iff (!rst_n)
    multiple_guards |=> (contention_count == $past(contention_count) + 32'd1);
endproperty
 
// P8: EVIDENCE -- simultaneous guards actually occurred in this run.
property c_guard_contention_reached;
  @(posedge clk) disable iff (!rst_n) multiple_guards;
endproperty
 
// ---- ENTRY ACTIONS (§9) -----------------------------------------
// P9: on entry, the state's own counters read zero. §15: omitting entry
// actions produced 199,993 dirty entries out of 200,000 transitions.
property p_entry_clears_counters;
  @(posedge clk) disable iff (!rst_n)
    state_enter |=> ((state_timer == '0) && (event_count == '0));
endproperty
 
// P10: a dirty entry is REPORTED and names the field.
property p_dirty_entry_flagged;
  @(posedge clk) disable iff (!rst_n)
    ($past(state_enter) && ((state_timer != '0) || (event_count != '0)))
      |=> (entry_dirty && (dirty_fields != '0));
endproperty
 
// P11: the first dirty field is latched, not overwritten by later ones.
property p_dirty_fields_sticky;
  @(posedge clk) disable iff (!rst_n)
    (entry_dirty && !dbg_clear) |=> $stable(dirty_fields);
endproperty
 
// P12: a state does not exit on its own entry cycle -- if it does, the
// guard was satisfied by residue (§9, §12's figure).
property p_no_exit_on_entry_cycle;
  @(posedge clk) disable iff (!rst_n)
    state_enter |-> !(state_enter && $past(state_enter));
endproperty
 
// ---- TIMERS (§6, §7) --------------------------------------------
// P13: the timer restarts at entry.
property p_timer_restarts_on_entry;
  @(posedge clk) disable iff (!rst_n)
    state_enter |=> (timer == '0);
endproperty
 
// P14: `timer_done` uses the NEXT-STATE value with >=, so an overshoot
// cannot step over the threshold. §15: `== LIMIT` never fires at step 3.
property p_timer_next_state_compare;
  @(posedge clk) disable iff (!rst_n)
    (tick && ((timer + 32'(step)) >= 32'(LIMIT))) |-> timer_done;
endproperty
 
// P15: entering already expired is REPORTED, not silently transitioned.
property p_entered_expired_flagged;
  @(posedge clk) disable iff (!rst_n)
    (timer_done && $past(state_enter)) |=> entered_expired;
endproperty
 
// ---- EPOCH AND STALE EVENTS (§8) --------------------------------
// P16: the epoch increments exactly once per transition.
property p_epoch_once_per_transition;
  @(posedge clk) disable iff (!rst_n)
    state_enter |=> (epoch == $past(epoch) + EPOCH_W'(1));
endproperty
 
// P17: a stale event is never qualified. §15: 12,738 transitions fired by
// a stale event when this check is absent.
property p_stale_never_qualified;
  @(posedge clk) disable iff (!rst_n)
    (event_valid && (event_epoch != epoch)) |-> !event_qualified;
endproperty
 
// P18: rejected stale events are COUNTED, never silently dropped.
property p_stale_counted;
  @(posedge clk) disable iff (!rst_n)
    event_stale |=> (stale_rejected_count == $past(stale_rejected_count) + 32'd1);
endproperty
 
// P19: a transition never fires on a stale event.
property p_no_transition_on_stale;
  @(posedge clk) disable iff (!rst_n)
    (state_enter && $past(event_stale) && !$past(event_qualified))
      |-> (selected != G_SUCCESS);
endproperty
 
// ---- HISTORY (§13) ----------------------------------------------
// P20: guards are sampled WITH the transition, not read afterwards.
property p_guards_sampled_at_transition;
  @(posedge clk) disable iff (!rst_n)
    (state_enter && !freeze) |=> (history[$past(wr_ptr)].guards_true == $past(guards_true));
endproperty
 
// P21: a frozen history is immutable and drops are counted.
property p_frozen_history;
  @(posedge clk) disable iff (!rst_n)
    freeze |=> $stable(history[0]);
endproperty
 
// P22: the write pointer is in range -- HIST_D = 1 included.
property p_hist_ptr_range;
  @(posedge clk) disable iff (!rst_n) (wr_ptr < HIST_W'(HIST_D));
endproperty
 
// ---- PROGRESS AND LOOPS (§10) -----------------------------------
// P23: milestones are MONOTONIC within an epoch -- a link that gains and
// loses the same milestone would otherwise report progress forever.
property p_milestones_monotonic;
  @(posedge clk) disable iff (!rst_n)
    (!dbg_clear) |=> ((milestones & $past(milestones)) == $past(milestones));
endproperty
 
// P24: a re-entry WITH progress resets the no-progress counter.
property p_progress_resets_counter;
  @(posedge clk) disable iff (!rst_n)
    (state_enter && gained) |=> (entries_since_progress == '0);
endproperty
 
// P25: the loop flag requires re-entry WITHOUT progress. §15: 1,002
// re-entries with 3 milestones is a legal retrain, not a loop.
property p_loop_requires_no_progress;
  @(posedge clk) disable iff (!rst_n)
    $rose(loop_no_progress) |-> ($past(entries_since_progress) >= 32'(LOOP_LIMIT));
endproperty
 
// P26: the loop flag is sticky until an explicit clear.
property p_loop_sticky;
  @(posedge clk) disable iff (!rst_n)
    (loop_no_progress && !dbg_clear) |=> loop_no_progress;
endproperty
 
// ---- STATE HYGIENE ----------------------------------------------
// P27: the state encoding is always defined (18.1 §10).
property p_state_encoding_valid;
  @(posedge clk) disable iff (!rst_n)
    (state inside {ST_DETECT, ST_POLLING, ST_CONFIGURATION, ST_L0,
                   ST_RECOVERY, ST_L0S, ST_L1, ST_DISABLED, ST_HOT_RESET});
endproperty
 
// P28: no debug output drives the state machine.
property p_debug_non_functional;
  @(posedge clk) disable iff (!rst_n)
    $stable({state, next_state}) or !$stable({stale_rejected_count, reentry_count});
endproperty
 
// P29: reset clears every contract instrument.
property p_reset_clears_instruments;
  @(posedge clk) disable iff (!rst_n)
    (!rst_n) |=> (!entry_dirty && !loop_no_progress && (epoch == '0));
endproperty
 
// P30: counters saturate rather than wrap.
property p_counters_saturate;
  @(posedge clk) disable iff (!rst_n)
    (reentry_count == 32'hFFFF_FFFF) |=> (reentry_count == 32'hFFFF_FFFF);
endproperty
 
// P31: EVIDENCE -- a stale event was actually presented in this run.
property c_stale_event_reached;
  @(posedge clk) disable iff (!rst_n) event_stale;
endproperty