Error Injection — One Contract at a Time, and Prove It Recovers

1. establish a baseline legal transaction that PASSES
2. identify the single field or event that carries the contract
3. corrupt exactly that, after everything else is computed
4. observe WHICH checker fires FIRST
5. observe the required recovery or containment
6. prove no unrelated resource leaked
7. prove the NEXT clean transaction succeeds

// VERIFICATION-ONLY. Fault taxonomy and control.
// LOCAL VERIFICATION POLICY -- PCIe defines none of these values (§1).
package fault_pkg;
 
  parameter int TAGS   = 8;
  parameter int TAG_W  = (TAGS <= 1) ? 1 : $clog2(TAGS);
  parameter int SEQ_W  = 12;
  parameter int CNT_W  = 32;
 
  typedef enum logic [3:0] {
    FI_NONE            = 4'd0,
    FI_BAD_INTEGRITY   = 4'd1,   // Data Link: corrupt the COMPUTED value (§4)
    FI_SEQ_CORRUPT     = 4'd2,   // Data Link: sequence discontinuity
    FI_DROP_ACK        = 4'd3,   // Data Link: withhold acknowledgement
    FI_BAD_CPL_ID      = 4'd4,   // Transaction: wrong (Requester ID, Tag)
    FI_CPL_ERR_STATUS  = 4'd5,   // Transaction: terminal status (13.2)
    FI_CREDIT_OVERSPEND= 4'd6,   // INTERNAL mutation -- SVA must fire (§3)
    FI_DROP_TRAIN_EVENT= 4'd7    // Link: withhold a training event
  } fault_kind_e;
 
  typedef enum logic [1:0] { FM_ONESHOT, FM_REPEAT, FM_DISABLED } fault_mode_e;
 
  typedef struct packed {
    logic            armed;
    fault_kind_e     kind;
    fault_mode_e     mode;
    logic [CNT_W-1:0] target_event;    // fire on the Nth qualifying EVENT
    logic [2:0]      target_port;
    logic [2:0]      target_function;
  } fault_cfg_t;
 
  // Which checker SHOULD fire first for each fault. The test asserts this
  // mapping -- a fault that trips the wrong checker is §10's mutation 4.
  function automatic string expected_checker(input fault_kind_e k);
    case (k)
      FI_BAD_INTEGRITY:    return "dl_integrity";
      FI_SEQ_CORRUPT:      return "dl_sequence";
      FI_DROP_ACK:         return "dl_replay";
      FI_BAD_CPL_ID:       return "tl_unknown_identity";
      FI_CPL_ERR_STATUS:   return "tl_terminal_status";
      FI_CREDIT_OVERSPEND: return "sva_credit_reservation";
      FI_DROP_TRAIN_EVENT: return "ltssm_progress";
      default:             return "none";
    endcase
  endfunction
 
endpackage

import fault_pkg::*;
 
// VERIFICATION-ONLY. One-shot arm and trigger (§2).
// The event counter advances on the ACCEPTED event only -- counting offers
// would fire the fault on a packet that was never sent (§10, mutation 18).
// §9: one-shot fires exactly 1; a repeating variant fired 2,987.
module fault_trigger (
  input  logic clk,
  input  logic rst_n,
  input  fault_cfg_t cfg,
  input  logic       event_fire,       // a qualifying event TRANSFERRED
  input  logic       fault_consumed,   // the DUT finished recovering
 
  output logic       inject_now,
  output fault_kind_e active_kind,
  output logic       pending,
  output logic [CNT_W-1:0] event_count,
  output logic       err_fire_unarmed  // sticky: fired without an arm
);
  logic [CNT_W-1:0] cnt_q;
  logic             armed_q, pend_q, e_q;
 
  assign event_count      = cnt_q;
  assign active_kind      = cfg.kind;
  assign pending          = pend_q;
  assign err_fire_unarmed = e_q;
 
  // SAME-CYCLE RULE (§8): arm and the target event in one cycle FIRE. The
  // arm is a level, and the count is compared against the next value.
  logic [CNT_W-1:0] cnt_next;
  assign cnt_next   = event_fire ? (cnt_q + CNT_W'(1)) : cnt_q;
  assign inject_now = armed_q && event_fire
                   && (cnt_next == cfg.target_event)
                   && (cfg.mode != FM_DISABLED);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cnt_q <= '0; armed_q <= 1'b0; pend_q <= 1'b0; e_q <= 1'b0;
    end else begin
      cnt_q <= cnt_next;
      // Arming is edge-insensitive: a level that is high enables firing.
      if (cfg.armed && !armed_q) armed_q <= 1'b1;
      if (inject_now) begin
        pend_q <= 1'b1;
        if (cfg.mode == FM_ONESHOT) armed_q <= 1'b0;   // FIRES EXACTLY ONCE
      end
      if (fault_consumed) pend_q <= 1'b0;
      // A fire with no arm cannot happen; prove it rather than trust it.
      if (event_fire && (cnt_next == cfg.target_event) && !armed_q && cfg.armed)
        e_q <= 1'b1;
    end
  end
endmodule

import fault_pkg::*;
 
// VERIFICATION-ONLY. Data Link integrity corruptor (§4).
// It mutates the COMPUTED value, never the payload -- corrupting the
// payload first makes the computed value CORRECT for the corrupted data,
// and the checker rightly says nothing (§10, mutation 14).
module dl_integrity_injector #(parameter int W = 32) (
  input  logic         inject_now,
  input  logic [W-1:0] integrity_in,     // already computed over the packet
  input  logic [$clog2(W)-1:0] bit_sel,
 
  output logic [W-1:0] integrity_out,
  output logic         corrupted
);
  // Exactly one bit, exactly one packet. Everything else is untouched, so
  // the only broken contract is the integrity check (P8, P9).
  assign integrity_out = inject_now ? (integrity_in ^ (W'(1) << bit_sel))
                                    : integrity_in;
  assign corrupted     = inject_now;
endmodule

import fault_pkg::*;
 
// VERIFICATION-ONLY. Sequence-number injector.
// The WIDTH and the legal progression are the Data Link chapter's (14.4);
// this block only perturbs the transmitted value by a parameterized delta,
// so nothing here asserts a sequence-number rule.
module dl_sequence_injector (
  input  logic             inject_now,
  input  logic [SEQ_W-1:0] seq_in,
  input  logic signed [3:0] delta,       // +1 skip, -1 duplicate, etc.
 
  output logic [SEQ_W-1:0] seq_out,
  output logic             corrupted
);
  assign seq_out   = inject_now ? (seq_in + SEQ_W'(delta)) : seq_in;
  assign corrupted = inject_now;
endmodule

import fault_pkg::*;
 
// VERIFICATION-ONLY. Wrong-identity Completion injector (§3).
// The packet stays perfectly legal -- correct format, correct length, a
// valid identity. Only the WRONG one. A conformance checker sees nothing;
// the project scoreboard's matcher must catch it (24.5 §6's distinction).
module tl_cpl_identity_injector (
  input  logic            inject_now,
  input  logic [15:0]     rid_in,
  input  logic [TAG_W-1:0] tag_in,
  input  logic [TAG_W-1:0] wrong_tag,
 
  output logic [15:0]     rid_out,
  output logic [TAG_W-1:0] tag_out,
  output logic            corrupted
);
  assign rid_out   = rid_in;                       // still a legal Requester ID
  assign tag_out   = inject_now ? wrong_tag : tag_in;
  assign corrupted = inject_now;
endmodule

import fault_pkg::*;
 
// SYNTHESIZABLE debug hook. First-error capture, injection-aware.
// It records WHICH checker fired first AND what fault was pending, so a
// cascade cannot bury the mapping the test is asserting (§2, §5).
module injection_first_error (
  input  logic clk,
  input  logic rst_n,
  input  logic [7:0]  checker_id,        // which checker fired
  input  logic        checker_fire,
  input  fault_kind_e pending_kind,
  input  logic        pending_valid,
  input  logic [15:0] pkt_rid,
  input  logic [TAG_W-1:0] pkt_tag,
  input  logic [3:0]  link_state,
  input  logic [CNT_W-1:0] cycle,
  input  logic        clear,
 
  output logic        captured,
  output logic [7:0]  first_checker,
  output fault_kind_e first_fault,
  output logic [15:0] first_rid,
  output logic [TAG_W-1:0] first_tag,
  output logic [3:0]  first_link_state,
  output logic [CNT_W-1:0] first_cycle,
  output logic [CNT_W-1:0] later_errors
);
  logic cap_q; logic [7:0] chk_q; fault_kind_e fk_q;
  logic [15:0] rid_q; logic [TAG_W-1:0] tag_q; logic [3:0] ls_q;
  logic [CNT_W-1:0] cyc_q, later_q;
 
  assign captured=cap_q; assign first_checker=chk_q; assign first_fault=fk_q;
  assign first_rid=rid_q; assign first_tag=tag_q; assign first_link_state=ls_q;
  assign first_cycle=cyc_q; assign later_errors=later_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      cap_q<=1'b0; chk_q<='0; fk_q<=FI_NONE; rid_q<='0; tag_q<='0;
      ls_q<='0; cyc_q<='0; later_q<='0;
    end else if (checker_fire) begin
      if (!cap_q) begin
        // LATCH ONCE. 21.4 §11 measured last-write-wins naming a
        // non-root-cause 96.8% of the time.
        cap_q<=1'b1; chk_q<=checker_id;
        fk_q <= pending_valid ? pending_kind : FI_NONE;
        rid_q<=pkt_rid; tag_q<=pkt_tag; ls_q<=link_state; cyc_q<=cycle;
      end else if (!(&later_q)) later_q <= later_q + CNT_W'(1);
    end
  end
endmodule

import fault_pkg::*;
 
// VERIFICATION-ONLY. Recovery watchdog (§5).
// A TEST BUDGET, not a PCIe timer. It measures how long the DUT stayed in
// its declared recovery state and flags a design that detected but never
// finished. Labelled deliberately -- 24.3 §8's distinction.
module recovery_watchdog #(parameter int unsigned BUDGET = 4096) (
  input  logic clk,
  input  logic rst_n,
  input  logic fault_injected,       // one-cycle pulse
  input  logic recovery_done,        // the DUT's declared completion event
 
  output logic recovery_pending,
  output logic [CNT_W-1:0] recovery_cycles,
  output logic watchdog_expired,     // sticky
  output logic [CNT_W-1:0] worst_recovery
);
  logic pend_q, exp_q;
  logic [CNT_W-1:0] cyc_q, worst_q;
 
  assign recovery_pending = pend_q;
  assign recovery_cycles  = cyc_q;
  assign watchdog_expired = exp_q;
  assign worst_recovery   = worst_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin pend_q<=1'b0; cyc_q<='0; exp_q<=1'b0; worst_q<='0; end
    else begin
      // SAME-CYCLE: injection and completion in one cycle means the design
      // recovered immediately -- a legal zero-cycle recovery, not an error.
      if (recovery_done && pend_q) begin
        pend_q <= 1'b0;
        if (cyc_q > worst_q) worst_q <= cyc_q;
      end else if (fault_injected && !pend_q) begin
        pend_q <= 1'b1; cyc_q <= '0;
      end else if (pend_q) begin
        cyc_q <= cyc_q + CNT_W'(1);
        if (cyc_q >= CNT_W'(BUDGET)) exp_q <= 1'b1;   // test budget elapsed
      end
    end
  end
endmodule

import fault_pkg::*;
 
// SYNTHESIZABLE debug hook. THE RECOVERY INVARIANT MONITOR (§5).
// This is the block that turns "the checker fired" into "the design
// recovered". §9: every fault kind returned to 8/8 free Tags.
module recovery_invariant_monitor (
  input  logic clk,
  input  logic rst_n,
  input  logic [TAGS-1:0] tag_free_map,
  input  logic [TAGS-1:0] tag_owned_map,
  input  logic [CNT_W-1:0] buffer_reserved,
  input  logic            replay_pending,
  input  logic            fault_injected,
  input  logic            recovery_done,
  input  logic            clean_txn_completed,   // a LEGAL transaction after recovery
 
  output logic err_tag_leak,
  output logic err_buffer_leak,
  output logic err_replay_stuck,
  output logic err_no_clean_after_recovery,   // sticky
  output logic recovered_cleanly
);
  logic [TAGS-1:0] baseline_free_q;
  logic [CNT_W-1:0] baseline_buf_q;
  logic seen_fault_q, seen_recovery_q, seen_clean_q, e_q;
 
  assign err_tag_leak    = seen_recovery_q && (tag_free_map != baseline_free_q);
  assign err_buffer_leak = seen_recovery_q && (buffer_reserved != baseline_buf_q);
  assign err_replay_stuck = seen_recovery_q && replay_pending;
  assign err_no_clean_after_recovery = e_q;
  assign recovered_cleanly = seen_recovery_q && seen_clean_q
                          && !err_tag_leak && !err_buffer_leak && !err_replay_stuck;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      baseline_free_q <= {TAGS{1'b1}}; baseline_buf_q <= '0;
      seen_fault_q<=1'b0; seen_recovery_q<=1'b0; seen_clean_q<=1'b0; e_q<=1'b0;
    end else begin
      // Snapshot the resting state BEFORE the fault -- the comparison the
      // whole recovery test depends on.
      if (!seen_fault_q && !fault_injected) begin
        baseline_free_q <= tag_free_map;
        baseline_buf_q  <= buffer_reserved;
      end
      if (fault_injected)      seen_fault_q    <= 1'b1;
      if (recovery_done)       seen_recovery_q <= 1'b1;
      if (clean_txn_completed) seen_clean_q    <= 1'b1;
      // Detection without a subsequent clean transaction is a FAILED test,
      // even though every checker behaved correctly (§5).
      if (seen_recovery_q && !seen_clean_q && (tag_owned_map == '0)) e_q <= 1'b1;
    end
  end
endmodule

// ---- INJECTION DISCIPLINE (§2, §4) ------------------------------
// P1: no injection unless armed.
property p_no_inject_unarmed;
  @(posedge clk) disable iff (!rst_n) inject_now |-> cfg.armed;
endproperty
 
// P2: injection requires an ACCEPTED event, never an offer.
property p_inject_on_transfer;
  @(posedge clk) disable iff (!rst_n) inject_now |-> event_fire;
endproperty
 
// P3: the fault lands on the EXACT target event.
property p_exact_target_event;
  @(posedge clk) disable iff (!rst_n)
    inject_now |-> (event_count + CNT_W'(1) == cfg.target_event);
endproperty
 
// P4: a one-shot fault fires exactly once. §9: a repeating variant fired
// 2,987 times against the correct design's 1.
property p_oneshot_fires_once;
  @(posedge clk) disable iff (!rst_n)
    (inject_now && (cfg.mode == FM_ONESHOT)) |=> !inject_now;
endproperty
 
// P5: a second arm while a fault is pending is refused.
property p_no_rearm_while_pending;
  @(posedge clk) disable iff (!rst_n)
    (pending && cfg.armed) |-> !inject_now;
endproperty
 
// P6: firing without an arm is REPORTED, never silent.
property p_unarmed_fire_flagged;
  @(posedge clk) disable iff (!rst_n)
    (event_fire && (event_count + CNT_W'(1) == cfg.target_event)
      && !armed_q && cfg.armed) |=> err_fire_unarmed;
endproperty
 
// P7: the event counter advances only on an accepted event.
property p_event_count_on_transfer;
  @(posedge clk) disable iff (!rst_n)
    (event_count != $past(event_count)) |-> $past(event_fire);
endproperty
 
// P8: the corruptor mutates the COMPUTED value only -- the payload is
// untouched, so exactly one contract is broken (§4).
property p_payload_untouched;
  @(posedge clk) disable iff (!rst_n)
    inject_now |-> $stable(packet_payload);
endproperty
 
// P9: a non-target packet is bit-identical to the baseline.
property p_non_target_unmodified;
  @(posedge clk) disable iff (!rst_n)
    (!inject_now && pkt_valid) |-> (integrity_out == integrity_in);
endproperty
 
// P10: exactly one fault kind is active at a time.
property p_single_active_fault;
  @(posedge clk) disable iff (!rst_n)
    pending |-> (active_kind != FI_NONE);
endproperty
 
// ---- DETECTION (§2, §3) -----------------------------------------
// P11: the injected fault trips the EXPECTED checker, not another.
property p_expected_checker_fires;
  @(posedge clk) disable iff (!rst_n)
    (captured && (first_fault != FI_NONE))
      |-> (checker_name(first_checker) == expected_checker(first_fault));
endproperty
 
// P12: a clean packet never trips a checker. §9: the baseline fired NOTHING.
property p_no_false_detection;
  @(posedge clk) disable iff (!rst_n)
    (pkt_valid && !inject_now && !pending) |-> !checker_fire;
endproperty
 
// P13: an injected packet is counted as ONE transaction, not two.
property p_injected_counted_once;
  @(posedge clk) disable iff (!rst_n)
    inject_now |=> (txn_count == $past(txn_count) + 1);
endproperty
 
// P14: the first error is sticky.
property p_first_error_sticky;
  @(posedge clk) disable iff (!rst_n)
    (captured && !clear) |=> (captured && $stable(first_checker)
                                       && $stable(first_fault));
endproperty
 
// P15: later errors are counted, never stored over the first.
property p_later_errors_counted;
  @(posedge clk) disable iff (!rst_n)
    (captured && checker_fire && !clear) |=> $stable(first_cycle);
endproperty
 
// ---- RECOVERY (§5) ----------------------------------------------
// P16: recovery is pending for a bounded interval under the TEST BUDGET.
// This bounds a verification watchdog, not a PCIe timer (§1).
property p_recovery_bounded;
  @(posedge clk) disable iff (!rst_n)
    recovery_pending |-> (recovery_cycles <= CNT_W'(BUDGET)) || watchdog_expired;
endproperty
 
// P17: every Tag returns to the pre-fault baseline. §9: 8/8 for every kind.
property p_no_tag_leak_after_recovery;
  @(posedge clk) disable iff (!rst_n)
    (recovery_done && (tag_owned_map == '0)) |=> !err_tag_leak;
endproperty
 
// P18: buffer reservations return to baseline.
property p_no_buffer_leak;
  @(posedge clk) disable iff (!rst_n)
    (recovery_done && (tag_owned_map == '0)) |=> !err_buffer_leak;
endproperty
 
// P19: replay state clears -- a replayed packet is not a new transaction.
property p_replay_state_clears;
  @(posedge clk) disable iff (!rst_n)
    recovery_done |=> !err_replay_stuck;
endproperty
 
// P20: THE PROPERTY MOST OFTEN MISSING. A clean transaction after recovery
// completes normally. Detection without this is a failed test (§5).
property p_clean_after_recovery;
  @(posedge clk) disable iff (!rst_n)
    recovery_done |-> s_eventually clean_txn_completed;
endproperty
 
// P21: the error does not repeat indefinitely from one fault.
property p_no_error_storm;
  @(posedge clk) disable iff (!rst_n)
    (later_errors > CNT_W'(STORM_LIMIT)) |-> error_storm_reported;
endproperty
 
// ---- CROSS-LAYER AND HYGIENE ------------------------------------
// P22: reset clears the arm and any pending fault.
property p_reset_clears_injection;
  @(posedge clk)
    (!rst_n) |=> (!inject_now && !pending && !captured);
endproperty
 
// P23: a wrong-identity Completion never retires an INNOCENT context
// (23.5 §3's matcher must report unknown rather than default).
property p_wrong_identity_no_innocent_retire;
  @(posedge clk) disable iff (!rst_n)
    (inject_now && (active_kind == FI_BAD_CPL_ID)) |=> !unrelated_ctx_retired;
endproperty
 
// P24: an internal credit overspend is caught BEFORE the wire (§3).
property p_credit_fault_caught_internally;
  @(posedge clk) disable iff (!rst_n)
    (inject_now && (active_kind == FI_CREDIT_OVERSPEND)) |-> !tx_wire_valid;
endproperty
 
// P25: the credit ledger never underflows even under injection.
property p_ledger_no_underflow_under_injection;
  @(posedge clk) disable iff (!rst_n)
    (avail_credit <= advertised_credit);
endproperty
 
// P26: the packet owner is held through EOP even during injection --
// corruption does not release arbitration (21.2 §11's contract).
property p_packet_lock_holds_under_injection;
  @(posedge clk) disable iff (!rst_n)
    (owner_valid && inject_now) |=> (owner_valid && $stable(owner));
endproperty
 
// P27: injection logic never drives functional traffic.
property p_injector_non_functional;
  @(posedge clk) disable iff (!rst_n)
    $stable({pkt_valid, pkt_ready}) or !$stable({event_count, later_errors});
endproperty
 
// P28: EVIDENCE -- a fault was actually injected in this run.
property c_fault_injected;
  @(posedge clk) disable iff (!rst_n) inject_now;
endproperty
 
// P29: EVIDENCE -- a clean transaction followed a recovery.
property c_clean_after_recovery_reached;
  @(posedge clk) disable iff (!rst_n) (recovery_done ##[1:$] clean_txn_completed);
endproperty