Protocol Verification — Three Contracts, and an Oracle That Owes You Nothing

a packet must not be duplicated
a Tag must not be reused while its transaction is outstanding
a credit must not be spent twice
a Completion must not be applied to an unknown request
a stale descriptor must not execute after an abort
packet metadata must not change while stalled
a transaction must not retire twice

// COMPILE-TIME. Verification types. Normalized metadata, NOT wire layouts.
package pcie_vplan_pkg;
 
  parameter int MAX_OUTSTANDING = 64;
  parameter int HISTORY_DEPTH   = 256;
  parameter int RID_W = 16;
  parameter int TAG_W = 8;
  parameter int LEN_W = 16;
 
  // The only stable handle a transaction has (§6).
  typedef struct packed {
    logic [RID_W-1:0] requester_id;
    logic [TAG_W-1:0] tag;
  } txn_key_t;
 
  typedef enum logic [2:0] {
    LYR_TL = 3'd0, LYR_DL = 3'd1, LYR_LINK = 3'd2, LYR_CFG = 3'd3
  } layer_e;
 
  typedef enum logic [3:0] {
    EV_REQ_ISSUED   = 4'd0,   // TL: a request transferred
    EV_CPL_RECEIVED = 4'd1,   // TL: a completion transferred
    EV_TXN_RETIRED  = 4'd2,   // TL: byte coverage or terminal
    EV_DL_ACCEPTED  = 4'd3,   // DL: the link partner accepted it
    EV_DL_REPLAY    = 4'd4,   // DL: retransmission
    EV_LINK_UP      = 4'd5,   // LINK: reached the operational state
    EV_LINK_RECOVER = 4'd6,   // LINK: left it and is recovering
    EV_CFG_WRITE    = 4'd7,   // a control-plane change
    EV_RESET        = 4'd8
  } event_e;
 
  typedef struct packed {
    logic            valid;
    layer_e          layer;
    event_e          kind;
    txn_key_t        key;         // meaningful for TL events
    logic [LEN_W-1:0] bytes;
    logic [31:0]     cycle;
    logic            is_error;
  } layer_event_t;
 
  function automatic bit key_eq(input txn_key_t a, input txn_key_t b);
    return (a.requester_id == b.requester_id) && (a.tag == b.tag);
  endfunction
 
endpackage

import pcie_vplan_pkg::*;
 
// VERIFICATION-ONLY. THE INDEPENDENT MODEL (§5). It knows the CONTRACT --
// identity, byte coverage, exactly-once retirement -- and nothing about
// how the DUT is built. It calls no DUT function, by construction.
// §13: 140,924 events clean, and every injected defect caught.
module outstanding_model (
  input logic clk,
  input logic rst_n,
 
  // observations, all on TRANSFERS (§6)
  input logic             req_seen,
  input txn_key_t         req_key,
  input logic [LEN_W-1:0] req_bytes,
 
  input logic             cpl_seen,
  input txn_key_t         cpl_key,
  input logic [LEN_W-1:0] cpl_bytes,
  input logic             cpl_error,
 
  input logic             retire_seen,
  input txn_key_t         retire_key,
 
  output int  outstanding,
  output logic err_duplicate_identity,   // a live key issued again
  output logic err_unknown_completion,   // no live transaction owns it
  output logic err_over_return,          // more bytes than requested
  output logic err_early_retire,         // retired before coverage
  output logic err_double_retire,
  output logic err_leak_at_end           // set by the end-of-test check
);
  txn_key_t         k    [MAX_OUTSTANDING];
  logic [LEN_W-1:0] want [MAX_OUTSTANDING];
  logic [LEN_W-1:0] got  [MAX_OUTSTANDING];
  logic             live [MAX_OUTSTANDING];
  logic             term [MAX_OUTSTANDING];
  int               n;
 
  assign outstanding = n;
 
  function automatic int find(input txn_key_t q);
    for (int i = 0; i < MAX_OUTSTANDING; i++)
      if (live[i] && key_eq(k[i], q)) return i;
    return -1;                                  // NEVER defaults to 0 (§6)
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      for (int i = 0; i < MAX_OUTSTANDING; i++) begin live[i] <= 1'b0; term[i] <= 1'b0; end
      n <= 0;
      err_duplicate_identity <= 1'b0; err_unknown_completion <= 1'b0;
      err_over_return <= 1'b0; err_early_retire <= 1'b0;
      err_double_retire <= 1'b0; err_leak_at_end <= 1'b0;
    end else begin
      // ---- a request was OBSERVED TO TRANSFER ----------------------
      if (req_seen) begin
        if (find(req_key) >= 0) err_duplicate_identity <= 1'b1;
        else for (int i = 0; i < MAX_OUTSTANDING; i++)
          if (!live[i]) begin
            live[i] <= 1'b1; k[i] <= req_key; want[i] <= req_bytes;
            got[i] <= '0; term[i] <= 1'b0; n <= n + 1;
            break;
          end
      end
 
      // ---- a completion was OBSERVED ------------------------------
      if (cpl_seen) begin
        automatic int j = find(cpl_key);
        if (j < 0) err_unknown_completion <= 1'b1;
        else if (cpl_error) term[j] <= 1'b1;
        else begin
          if ((got[j] + cpl_bytes) > want[j]) err_over_return <= 1'b1;
          else got[j] <= got[j] + cpl_bytes;      // COVERAGE, not packet count
        end
      end
 
      // ---- a retirement was OBSERVED ------------------------------
      if (retire_seen) begin
        automatic int j = find(retire_key);
        if (j < 0) err_double_retire <= 1'b1;
        else begin
          if ((got[j] < want[j]) && !term[j]) err_early_retire <= 1'b1;
          live[j] <= 1'b0; n <= n - 1;
        end
      end
    end
  end
endmodule

import pcie_vplan_pkg::*;
 
// VERIFICATION-ONLY. The event timeline (§9). A bounded ring of normalized
// observations from ALL monitors, in one order. This is what makes §15's
// triangulation a sentence you can say rather than a guess.
module event_timeline (
  input  logic clk,
  input  logic rst_n,
  input  logic         ev_valid,
  input  layer_event_t ev,
  input  logic         snapshot_req,
 
  output layer_event_t history [HISTORY_DEPTH],
  output int           depth,
  output logic         wrapped,
  output logic         err_index_range      // sticky
);
  layer_event_t h [HISTORY_DEPTH];
  int  wr;
  logic wrap_q, e_q;
 
  assign depth           = wrap_q ? HISTORY_DEPTH : wr;
  assign wrapped         = wrap_q;
  assign err_index_range = e_q;
  always_comb for (int i = 0; i < HISTORY_DEPTH; i++) history[i] = h[i];
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wr <= 0; wrap_q <= 1'b0; e_q <= 1'b0;
      for (int i = 0; i < HISTORY_DEPTH; i++) h[i] <= '0;
    end else if (ev_valid) begin
      // Range-safe by construction (Chapter 23.6 pattern 11): the write
      // index is bounded before use, and an out-of-range write is reported
      // rather than aliasing to entry 0.
      if (wr >= HISTORY_DEPTH) e_q <= 1'b1;
      else begin
        h[wr] <= ev;
        if (wr == HISTORY_DEPTH-1) begin wr <= 0; wrap_q <= 1'b1; end
        else wr <= wr + 1;
      end
    end
  end
endmodule

import pcie_vplan_pkg::*;
 
// VERIFICATION-ONLY. THE LAYER CONTRACT MONITOR (§2, §4).
// It proves the educational point directly: a Transaction Layer request
// that was issued, and a Data Link acceptance, are DIFFERENT events, and
// neither implies the other. Where a layer is unobservable, its input is
// tied off and `dl_observable` says so -- rather than the environment
// pretending (§4, mutation 26).
module layer_contract_monitor #(parameter bit DL_OBSERVABLE = 1'b1) (
  input  logic clk,
  input  logic rst_n,
 
  input  logic     tl_req_fire,        // TL: request transferred
  input  txn_key_t tl_req_key,
  input  logic     dl_accept,          // DL: link partner accepted (if visible)
  input  txn_key_t dl_key,
  input  logic     dl_replay,
  input  logic     tl_rx_fire,         // TL: the answer came back
  input  txn_key_t tl_rx_key,
  input  logic     link_operational,
 
  output logic dl_observable,
  output int   tl_issued,
  output int   dl_accepted,
  output int   dl_replays,
  output int   tl_returned,
  output logic err_return_without_issue,
  output logic err_dl_without_tl,
  output logic err_issue_while_link_down
);
  assign dl_observable = DL_OBSERVABLE;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      tl_issued<=0; dl_accepted<=0; dl_replays<=0; tl_returned<=0;
      err_return_without_issue<=1'b0; err_dl_without_tl<=1'b0;
      err_issue_while_link_down<=1'b0;
    end else begin
      if (tl_req_fire) begin
        tl_issued <= tl_issued + 1;
        // A request accepted while the Link is not operational is a
        // cross-layer contract violation, not a TL bug.
        if (!link_operational) err_issue_while_link_down <= 1'b1;
      end
      if (DL_OBSERVABLE && dl_accept) begin
        dl_accepted <= dl_accepted + 1;
        // A link-layer acceptance with no corresponding TL request means
        // the two observations disagree -- exactly the case §15 triangulates.
        if (tl_issued == 0) err_dl_without_tl <= 1'b1;
      end
      if (DL_OBSERVABLE && dl_replay) dl_replays <= dl_replays + 1;
      if (tl_rx_fire) begin
        tl_returned <= tl_returned + 1;
        if (tl_returned >= tl_issued) err_return_without_issue <= 1'b1;
      end
    end
  end
endmodule

import pcie_vplan_pkg::*;
 
// SYNTHESIZABLE. Design-for-verification hooks (§4). These are SILICON
// DEBUG observability, not testbench components -- they exist so a layer
// that is otherwise invisible becomes inferable. Chapter 25 owns using
// them in the lab; this chapter owns the argument for having them.
module dfv_observability #(parameter int N_CLASS = 3) (
  input  logic clk,
  input  logic rst_n,
  input  logic             txn_issued,
  input  logic             txn_retired,
  input  logic             replay_event,
  input  logic [3:0]       link_state,
  input  logic             first_error,
  input  logic [7:0]       first_error_cause,
  input  logic [N_CLASS-1:0] credit_blocked,      // pending AND short (22.3 §5)
  input  logic             clear,
 
  output logic [15:0] outstanding_count,
  output logic [31:0] replay_count,
  output logic [3:0]  link_state_now,
  output logic        err_captured,
  output logic [7:0]  err_first_cause,
  output logic [31:0] credit_block_cycles [N_CLASS]
);
  logic [15:0] out_q; logic [31:0] rep_q; logic cap_q; logic [7:0] cause_q;
  logic [31:0] cb_q [N_CLASS];
 
  assign outstanding_count = out_q;
  assign replay_count      = rep_q;
  assign link_state_now    = link_state;
  assign err_captured      = cap_q;
  assign err_first_cause   = cause_q;
  always_comb for (int c = 0; c < N_CLASS; c++) credit_block_cycles[c] = cb_q[c];
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      out_q<='0; rep_q<='0; cap_q<=1'b0; cause_q<='0;
      for (int c = 0; c < N_CLASS; c++) cb_q[c] <= '0;
    end else begin
      // Next-state arithmetic, so a same-cycle issue and retire is exact
      // (Chapter 23.6 pattern 9).
      out_q <= out_q + 16'(txn_issued) - 16'(txn_retired);
      if (replay_event && !(&rep_q)) rep_q <= rep_q + 32'd1;
      // Sticky FIRST failure (Chapter 23.6 pattern 12).
      if (first_error && !cap_q) begin cap_q <= 1'b1; cause_q <= first_error_cause; end
      for (int c = 0; c < N_CLASS; c++)
        if (credit_blocked[c] && !(&cb_q[c])) cb_q[c] <= cb_q[c] + 32'd1;
    end
  end
endmodule

import pcie_vplan_pkg::*;
 
// VERIFICATION-ONLY. The failure localizer. Given the model's verdicts and
// the per-layer counters, it names the CONTRACT that broke rather than
// reporting "test failed" -- which is the entire argument of §2.
module failure_localizer (
  input logic tl_model_error,
  input logic tl_unknown_completion,
  input logic tl_early_retire,
  input logic dl_observable,
  input int   dl_replays,
  input int   dl_replay_threshold,
  input logic link_left_operational,
  input logic err_issue_while_link_down,
 
  output logic blame_transaction,
  output logic blame_data_link,
  output logic blame_link_state,
  output logic blame_unattributable      // the honest fourth answer
);
  always_comb begin
    // Link state first: if the Link was not usable, the layers above are
    // UNPROVABLE rather than false (§3).
    blame_link_state   = link_left_operational || err_issue_while_link_down;
    blame_data_link    = !blame_link_state && dl_observable
                       && (dl_replays > dl_replay_threshold);
    blame_transaction  = !blame_link_state && !blame_data_link && tl_model_error;
    // A transaction-layer symptom with an unobservable data link cannot be
    // attributed. Saying so beats guessing (§4).
    blame_unattributable = tl_model_error && !dl_observable
                        && !blame_link_state && !blame_transaction;
  end
endmodule

// ==================================================================
// OBSERVATION INTEGRITY (§6) -- monitors record what happened.
// ==================================================================
 
// P1: a request is recorded only on an observed TRANSFER, never an offer.
property p_record_on_transfer;
  @(posedge clk) disable iff (!rst_n)
    (outstanding != $past(outstanding)) |-> $past(req_seen || retire_seen);
endproperty
 
// P2: exactly one model insertion per observed request transfer.
property p_one_insert_per_request;
  @(posedge clk) disable iff (!rst_n)
    (req_seen && !err_duplicate_identity && !retire_seen)
      |=> (outstanding == $past(outstanding) + 1);
endproperty
 
// P3: a live identity is unique in the model. §6: a model that allows
// duplicates reports the correct design as broken.
property p_no_duplicate_identity;
  @(posedge clk) disable iff (!rst_n)
    (req_seen && (find(req_key) >= 0)) |=> err_duplicate_identity;
endproperty
 
// P4: a monitor's emitted event is stable for the cycle it is valid.
property p_event_stable;
  @(posedge clk) disable iff (!rst_n)
    ev_valid |-> ##0 $stable(ev.kind);
endproperty
 
// P5: every event carries a classified layer -- nothing is "unknown".
property p_event_layer_valid;
  @(posedge clk) disable iff (!rst_n)
    ev_valid |-> (ev.layer inside {LYR_TL, LYR_DL, LYR_LINK, LYR_CFG});
endproperty
 
// P6: event cycle stamps are monotonic, so the timeline is an order.
property p_timestamps_monotonic;
  @(posedge clk) disable iff (!rst_n)
    ev_valid |-> (ev.cycle >= $past(ev.cycle));
endproperty
 
// ==================================================================
// MODEL CORRECTNESS (§5, §6).
// ==================================================================
 
// P7: a completion matches a LIVE transaction or is reported unknown --
// it never defaults to entry 0.
property p_completion_matches_or_reports;
  @(posedge clk) disable iff (!rst_n)
    (cpl_seen && (find(cpl_key) < 0)) |=> err_unknown_completion;
endproperty
 
// P8: a transaction is removed exactly once.
property p_remove_once;
  @(posedge clk) disable iff (!rst_n)
    (retire_seen && (find(retire_key) < 0)) |=> err_double_retire;
endproperty
 
// P9: same-cycle retire and issue of the same key is handled exactly --
// the key is free for the new transaction.
property p_same_cycle_retire_issue;
  @(posedge clk) disable iff (!rst_n)
    (retire_seen && req_seen && key_eq(retire_key, req_key))
      |=> !err_duplicate_identity;
endproperty
 
// P10: retirement before byte coverage, with no terminal outcome, is
// REPORTED -- the environment's version of Chapter 23.5's 80.8% cascade.
property p_early_retire_reported;
  @(posedge clk) disable iff (!rst_n)
    err_early_retire |=> err_early_retire;
endproperty
 
// P11: model population equals the live entry count -- conservation.
property p_population_consistent;
  @(posedge clk) disable iff (!rst_n)
    (outstanding >= 0) && (outstanding <= MAX_OUTSTANDING);
endproperty
 
// ==================================================================
// TIMELINE (§9) -- bounded, and never out of range.
// ==================================================================
 
// P12: the write index is always within the ring.
property p_history_index_safe;
  @(posedge clk) disable iff (!rst_n)
    (wr >= 0) && (wr < HISTORY_DEPTH);
endproperty
 
// P13: an out-of-range write is reported, never aliased.
property p_history_range_reported;
  @(posedge clk) disable iff (!rst_n)
    (ev_valid && (wr >= HISTORY_DEPTH)) |=> err_index_range;
endproperty
 
// P14: depth never exceeds the ring's capacity.
property p_depth_bounded;
  @(posedge clk) disable iff (!rst_n) (depth <= HISTORY_DEPTH);
endproperty
 
// ==================================================================
// LAYER SEPARATION (§2, §4).
// ==================================================================
 
// P15: a Data Link acceptance is NOT treated as end-to-end delivery --
// the two counters are independent (Chapter 21.2 §3).
property p_dl_accept_is_not_tl_delivery;
  @(posedge clk) disable iff (!rst_n)
    (dl_accept && DL_OBSERVABLE) |-> ##0 !$rose(tl_returned);
endproperty
 
// P16: a replay does not count as a new Transaction Layer request.
property p_replay_is_not_new_request;
  @(posedge clk) disable iff (!rst_n)
    dl_replay |=> $stable(tl_issued);
endproperty
 
// P17: an unobservable layer is declared, not assumed.
property p_unobservable_declared;
  @(posedge clk) disable iff (!rst_n)
    (!dl_observable) |-> ((dl_accepted == 0) && (dl_replays == 0));
endproperty
 
// P18: a transaction-layer symptom with an unobservable data link is
// reported UNATTRIBUTABLE rather than blamed on the transaction layer.
property p_honest_attribution;
  @(posedge clk) disable iff (!rst_n)
    (tl_model_error && !dl_observable && !blame_link_state)
      |-> (blame_unattributable || blame_transaction);
endproperty
 
// P19: link-state failure outranks the layers above -- they become
// unprovable, not false (§3).
property p_link_state_outranks;
  @(posedge clk) disable iff (!rst_n)
    blame_link_state |-> (!blame_data_link && !blame_transaction);
endproperty
 
// ==================================================================
// RESET AND NON-INTERFERENCE.
// ==================================================================
 
// P20: reset clears the model completely -- no stale transaction survives.
property p_reset_clears_model;
  @(posedge clk) (!rst_n) |=> (outstanding == 0);
endproperty
 
// P21: an observation in the cycle after reset finds an empty model and
// is reported unknown, rather than matching a stale entry.
property p_no_stale_match_after_reset;
  @(posedge clk) disable iff (!rst_n)
    ($past(!rst_n) && cpl_seen) |=> err_unknown_completion;
endproperty
 
// P22: verification logic never drives the DUT.
property p_verification_non_functional;
  @(posedge clk) disable iff (!rst_n)
    $stable({req_seen, cpl_seen}) or !$stable({outstanding, dl_replays});
endproperty