Legacy Interrupts (INTx) — Emulating a Wire That Isn't There

Every mechanism in this curriculum so far has been about moving data between two ports. Interrupts are the first mechanism that is not about the Link at all — they are how a device tells software that something happened.

And PCIe inherited a problem. Conventional PCI signalled interrupts with four physical wires — INTA, INTB, INTC, INTD — shared across every device on a bus. A device pulled its wire low and held it until software serviced and cleared the source. Level-sensitive, shared, and completely dependent on a wire existing.

PCIe has no such wire. It is a point-to-point serial link carrying packets. Yet an enormous amount of existing software, firmware and operating-system code expects that wire's behaviour.

So how do you emulate a shared, level-sensitive wire over a packet link — and what breaks when the emulation is imperfect?

1. The Verified Sources

2. A Wire That Isn't There

Conventional PCI's interrupt mechanism was physical.

PCI (the wire)                     PCIe (the emulation)
──────────────                     ───────────────────
four shared traces                 no wires at all
device pulls the line low          device drives an internal LEVEL
line stays low until serviced      level stays high until serviced
host samples the line              host RECONSTRUCTS the level from
                                     Assert / Deassert MESSAGES

Everything about the wire's semantics was preserved. Everything about its transport was replaced.

3. Level, Not Edge — and Held Until Cleared

§1's requirement is explicit: "Each interrupt source must continue to drive a 1 until it has been serviced and cleared by software, at which time it must switch to driving 0."

That single sentence defines the contract, and it is worth being precise about what it buys.

A level cannot be missed. If the device is still asserting, the condition is still true. A host that missed a notification and looks again still sees the interrupt.

An edge can be missed. A one-cycle pulse that nobody was listening for is gone forever, and nothing indicates it happened.

So level-sensitivity is a reliability property, and it is why shared interrupts were workable at all: several devices on one wire, each holding it until serviced, and the host works through them.

4. The Round Trip

   device                     PCIe Link                      host
   ──────                     ─────────                      ────
 
   source A ─┐
   source B ─┼─ OR ─► level ─┬─ 0→1 ─► "Assert INTx"  ──►  believes ASSERTED
   source C ─┘                │
                              └─ 1→0 ─► "Deassert INTx" ──► believes deasserted

Three conversions, and each can go wrong differently.

Level to edge. §1: "sends an Interrupt Assert message on each 0 to 1 transition and an Interrupt De-Assert Message on each 1 to 0 transition." The transport carries only changes.

Edge to transport. The messages are TLPs on a Link that may be busy, retraining, or in a power state — and §6 is about what happens when the transport cannot keep up.

Transport to level. The host maintains a belief and updates it on each message. It never samples the actual line, because there is no line to sample.

That last point is the one to internalize. In conventional PCI the host could always look. Here the host's belief is a reconstruction, and its only inputs are the messages it received — so the reconstruction is exactly as correct as the message stream, and no better.

5. Balance Is the Whole Invariant

Because the host's belief is built only from messages, one property matters above all others:

When the device's level settles, the host's belief must equal it.

Two ways to violate it, and they are opposites.

6. Merging

§1 states it plainly: "Transitions which occur too close together to be independently transmitted are merged."

This is not an optimization; it is unavoidable. The level is a signal in the device's clock domain that can change every cycle. A message is a TLP — it must be framed, arbitrated, credited (Chapter 16.5) and transmitted. The level can change faster than messages can be sent.

So some transitions will not get their own message. The question is which ones, and what the host ends up believing.

7. Shared by Construction

§1 describes two levels of OR:

within a Function:   "Each functions' interrupt sources must be logically
                      ORed together and input as legacy_interrupt_i[i]"
 
across Functions:    "The core ORs together INTA/B/C/D from all functions
                      to create an aggregated INTA/INTB/INTC/INTD"

So by the time a message is sent, the identity of what caused it is gone.

The host learns "INTA is asserted" and nothing more. Which Function, which source within that Function, and how many are asserting simultaneously — all of it was ORed away.

Hence the shared-interrupt handling every driver author knows. The host calls every driver registered on that INTx pin. Each one reads its device's own status registers to decide whether it has work. Drivers that find nothing return "not mine", and the cost is paid on every interrupt.

And this is the structural argument for MSI and MSI-X — not that they are faster in transport, but that they carry identity. A message-signalled interrupt says which vector; INTx says only that something happened on a wire several devices share.

The RTL consequence (§11): the OR is deliberate, and its inputs must be sticky level sources, not pulses (§3). A pulsed source ORed with a held one disappears — the OR output was already high, so no transition occurs, and no message is sent.

8. INTx Is Not an IRQ Number

A terminology collision worth heading off.

They are related by routing — Chapter 19.4 owns how an INTx assertion reaches a host interrupt — but they are not the same identifier, and the mapping is not the device's business.

A device does not choose its IRQ. It declares which INTx pin it uses, and everything after that belongs to the platform.

9. The Message Exchange

Three things to read out of the figure.

Source B produces no message. The aggregated level was already 1, so there was no transition — and this is correct. The host is already being told the line is asserted; that is all it can act on (§6).

Which is exactly why the driver must re-read status after clearing. If it cleared A, saw the level was still high because of B, and stopped — it would leave the line asserted with no further message coming. The level does not fall until the last source is cleared, and only then does a Deassert follow.

And the Deassert is the device's, not software's. Software cleared the sources; the level falling is what generates the message.

10. A Trace

Internal teaching signals. The message path is busy for two cycles after each send (§6).

cycle             1     2     3     4     5     6     7     8     9    10
src_a             0     1     1     1     1     0     0     0     0     0
src_b             0     0     0     1     1     1     1     0     0     0
intx_level        0     1     1     1     1     1     1     0     0     0
 
msg_busy          0     0     2     1     0     0     0     0     2     1
msg_valid         0     1     0     0     0     0     0     1     0     0
msg_kind         --     A    --    --    --    --    --     D    --    --
 
host_belief       0     0     1     1     1     1     1     1     0     0
belief_matches    1     0     1     1     1     1     1     0     1     1

Read cycle 2. Source A asserts, the level rises, and a message is sent immediately because the path is free.

Read cycle 4. Source B asserts — and nothing happens. intx_level was already 1; no transition, no message. §9's point, in signals.

Read cycle 6. Source A is cleared. Still nothing — B is still asserting, so the level holds. A design that sent a Deassert here would be reporting a line that is still asserted.

Read cycle 8. B is cleared, the level falls, and a Deassert goes out.

And read belief_matches across the whole trace. It is low at cycles 2 and 8 — the transport delay, which is unavoidable and harmless. What matters is that it returns to 1 and stays there. §5's invariant is about where the belief settles, not about it being instantaneous.

11. RTL — Sticky Sources and the Aggregated Level

// SYNTHESIZABLE. Normalized INTx types.
// FOUR PINS is canonical (section 1: "INTA, INTB, INTC, or INTD"). The
// message representation here is INTERNAL -- the wire encoding is not
// published in this chapter.
package intx_pkg;
 
  typedef enum logic [1:0] { INTA=2'd0, INTB=2'd1, INTC=2'd2, INTD=2'd3 } intx_pin_e;
  typedef enum logic       { MSG_ASSERT=1'b1, MSG_DEASSERT=1'b0 } intx_msg_e;
 
  typedef struct packed {
    logic      valid;
    intx_pin_e pin;
    intx_msg_e kind;
  } intx_msg_t;
 
endpackage

import intx_pkg::*;
 
// SYNTHESIZABLE. Sticky interrupt sources, cleared only by software.
// SECTION 1: "Each interrupt source must continue to drive a 1 UNTIL IT
// HAS BEEN SERVICED AND CLEARED BY SOFTWARE, at which time it must switch
// to driving 0." The device does not decide when to deassert (section 3).
module intx_sources #(parameter int N_SRC = 8) (
  input  logic clk,
  input  logic rst_n,
 
  // Condition pulses from the design. These may be single-cycle.
  input  logic [N_SRC-1:0] src_event,
 
  // Software write-1-to-clear, the same discipline as the vendor status
  // registers throughout this curriculum.
  input  logic [N_SRC-1:0] sw_clear,
 
  // Some conditions are LEVELS that are still true. Held separately so a
  // clear that does not fix the condition re-asserts honestly (section 3).
  input  logic [N_SRC-1:0] src_level,
 
  input  logic [N_SRC-1:0] src_enable,
 
  output logic [N_SRC-1:0] pending,
  output logic             func_level
);
 
  logic [N_SRC-1:0] sticky_q;
  assign pending = sticky_q;
 
  // ==================================================================
  // THE FUNCTION-LEVEL OR (section 7, first stage).
  //
  // Masked by enable so a disabled source contributes nothing -- and note
  // the OR is over LEVELS, never over events. An event ORed in directly
  // would vanish whenever another source was already asserting.
  // ==================================================================
  assign func_level = |(sticky_q & src_enable);
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) sticky_q <= '0;
    else begin
      for (int i = 0; i < N_SRC; i++) begin
        // ==============================================================
        // SET BEATS CLEAR, declared.
        //
        // A condition occurring in the same cycle software clears the
        // flag must NOT be lost -- software cleared what it had seen,
        // not what arrived afterwards. Clear-beats-set loses exactly the
        // events that arrive during servicing, which is when a busy
        // device generates most of them (section 16, mutation 2).
        // ==============================================================
        if (src_event[i] || src_level[i]) sticky_q[i] <= 1'b1;
        else if (sw_clear[i])             sticky_q[i] <= 1'b0;
      end
    end
  end
 
endmodule

Classification: synthesizable.

Two decisions, both load-bearing. Sticky, software-cleared is §1's contract restated in RTL. Set beats clear is the same-cycle rule that keeps a busy device honest — and its opposite loses precisely the events that arrive while the handler is running.

src_level is separate from src_event because some conditions are ongoing. A clear against a still-true condition re-asserts immediately, which looks like an interrupt storm and is in fact correct reporting (§3).

Failure — four. A pulsed source ORed straight into the level vanishes behind another source. Clear beats set loses events during servicing. Self-clearing sources break the level contract. And ORing before enabling lets a disabled source assert the line.

12. RTL — The Reconciler

import intx_pkg::*;
 
// SYNTHESIZABLE. THE FLAGSHIP BLOCK OF THIS CHAPTER.
//
// Converts an aggregated level into Assert/Deassert messages -- and it is
// built as a BELIEF RECONCILER, not an edge queue.
//
// The naive design queues transitions. Section 16 measured it: WRONG IN
// 11.6% of (level sequence, merge window) cases, producing both stuck and
// lost interrupts. This design tracks what the host has been TOLD and
// emits a message whenever that disagrees with the current level.
//
// Merging (section 6) is then automatic: while the message path is busy,
// the level can change any number of times, and whatever it settles on is
// what gets sent next.
module intx_reconciler (
  input  logic clk,
  input  logic rst_n,
 
  input  intx_pin_e  pin,          // build-time Interrupt Pin (section 1)
  input  logic       agg_level,    // aggregated across all Functions (section 7)
  input  logic       intx_enabled, // Legacy mode selected by software (section 14)
 
  // Decoupled message interface. The path CAN stall -- it is a TLP.
  output intx_msg_t  msg,
  input  logic       msg_ready,
 
  output logic       belief,       // what the host has been told
  output logic       in_sync
);
 
  logic belief_q;
  assign belief  = belief_q;
  assign in_sync = (belief_q == agg_level);
 
  // ==================================================================
  // THE ENTIRE ALGORITHM.
  //
  //   a message is owed  <=>  the host's belief differs from the level
  //
  // No edge detector. No queue. No pending-transition register. There is
  // nothing to lose and nothing to reorder, because the outstanding work
  // is DERIVED from a comparison rather than accumulated from history.
  //
  // Note this also emits FEWER messages than an edge queue -- section 16
  // measured 20.9% fewer -- because transitions that cancel out while the
  // path is busy never become messages at all.
  // ==================================================================
  wire owed = intx_enabled && (belief_q != agg_level);
 
  assign msg.valid = owed;
  assign msg.pin   = pin;
  // The message says what the level IS, not what changed. A design that
  // latched "the direction of the edge that started this" would send a
  // stale direction if the level moved again while stalled.
  assign msg.kind  = agg_level ? MSG_ASSERT : MSG_DEASSERT;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      belief_q <= 1'b0;
    end else if (!intx_enabled) begin
      // ==============================================================
      // LEAVING LEGACY MODE RESETS THE BELIEF.
      //
      // Section 1: when MSI or MSI-X is enabled, legacy_interrupt_i "is
      // not used for that function". A belief carried across a mode
      // change would make a later return to Legacy mode start out of
      // sync -- and the first reconciliation would send a message the
      // host did not expect (section 16, mutation 9).
      // ==============================================================
      belief_q <= 1'b0;
    end else if (msg.valid && msg_ready) begin
      // Belief advances ONLY on an accepted transfer. Advancing on
      // `valid` alone would record a message the Link never carried --
      // the same class of error as Chapter 18.9's ordered-set counter.
      belief_q <= agg_level;
    end
  end
 
endmodule

Classification: synthesizable.

Architecture. One belief register, one comparison, no queue.

Verified exhaustively (§16): over 16,376 (level sequence, merge window) cases, the reconciler's belief converges on the settled level in every case. An edge queue is wrong in 1,906 of them (11.6%), and an edge queue that drops transitions while busy is wrong in 2,883 (17.6%).

And it is cheaper: 20.9% fewer messages across 20,000 random sequences, because transitions that cancel while the path is busy never become messages.

13. RTL — Message Send Owner

import intx_pkg::*;
 
// SYNTHESIZABLE. Own the transmission of one INTx message.
// AN INTx MESSAGE IS A TLP. It needs the transmit path, and it may be
// blocked -- by arbitration, by an LTSSM state that forbids traffic
// (Chapter 18.6 section 7), or by the Link being in a power state.
//
// SAME OWNERSHIP PATTERN as Chapter 18.2's detection owner and Chapter
// 18.5's rate owner: held under stall, fields stable, one send per grant.
module intx_msg_send (
  input  logic clk,
  input  logic rst_n,
 
  input  intx_msg_t req,          // from section 12's reconciler
  output logic      req_ready,
 
  // To the TLP transmit path.
  output logic      tx_valid,
  output intx_pin_e tx_pin,
  output intx_msg_e tx_kind,
  input  logic      tx_ready,
 
  // The Link may not be able to carry a message right now.
  input  logic      link_ok,      // LTSSM permits normal traffic
 
  output logic      send_blocked
);
 
  intx_msg_t held_q;
  logic      busy_q, blocked_q;
 
  assign tx_valid     = busy_q && link_ok;
  assign tx_pin       = held_q.pin;    // CAPTURED, never re-read
  assign tx_kind      = held_q.kind;
  assign send_blocked = blocked_q;
 
  // Accept a new message only when not already carrying one.
  assign req_ready = !busy_q;
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      held_q <= '0; busy_q <= 1'b0; blocked_q <= 1'b0;
    end else begin
      if (!busy_q && req.valid) begin
        // CAPTURE THE WHOLE MESSAGE. The reconciler's outputs are
        // combinational off the current level -- re-reading them at
        // transmit time would send whatever the level is THEN, which is
        // a different message from the one that was accepted.
        held_q <= req;
        busy_q <= 1'b1;
      end else if (busy_q && tx_valid && tx_ready) begin
        busy_q <= 1'b0;
      end
 
      // A message that cannot be sent because the Link forbids traffic is
      // REPORTED. It is not an error -- section 15 explains why the
      // reconciler makes it self-correcting -- but it is worth seeing.
      if (busy_q && !link_ok) blocked_q <= 1'b1;
    end
  end
 
endmodule

Classification: synthesizable.

link_ok is the cross-module input that matters. Module 18 established that normal traffic is illegal outside L0 (Chapter 18.6 §7) and that a packet offered in a power state must wait, not be dropped (Chapter 18.7 §18). An interrupt message is subject to all of it.

And §15's property is the reassuring one: because §12 is a reconciler, a message blocked for an arbitrarily long time is not a lost interrupt. When the Link returns, the belief still disagrees with the level, and the correct message is sent then — carrying the level as it is at that moment, not as it was when the block began.

Failure — three. Re-reading the reconciler's outputs at transmit time sends a different message from the one accepted. Asserting tx_valid without link_ok offers a TLP to a Link that must not carry one. And clearing busy_q on tx_valid alone records a send that did not happen.

14. RTL — Mode Gating

import intx_pkg::*;
 
// SYNTHESIZABLE. One interrupt condition, three possible behaviours.
// SECTION 1 IS EXPLICIT: "User interrupt logic must behave differently
// depending upon whether the function is enabled for MSI-X, MSI, or
// Legacy Interrupts" -- and the core's own interrupt output is "an active
// high LEVEL-based interrupt when level-based interrupts are in use
// (MSI-X_Enable == 0 & MSI_Enable == 0) and as an active high SINGLE
// CLOCK PULSE when edge based interrupts are in use."
//
// THE SAME SOURCE MUST PRESENT AS A LEVEL OR AS A PULSE.
module intx_mode_gate (
  input  logic clk,
  input  logic rst_n,
 
  // Software-configured mode. Section 1: chosen "as part of the PCI
  // enumeration process", one mode at a time per Function.
  input  logic msi_enable,
  input  logic msix_enable,
 
  input  logic condition_sticky,   // section 11's pending level
 
  output logic legacy_level,       // to the reconciler  (LEVEL)
  output logic edge_pulse,         // to MSI / MSI-X     (PULSE)
  output logic legacy_mode
);
 
  // Section 1's exact condition, restated.
  assign legacy_mode = (msi_enable == 1'b0) && (msix_enable == 1'b0);
 
  logic prev_q;
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) prev_q <= 1'b0;
    else        prev_q <= condition_sticky;
  end
 
  // ==================================================================
  // LEVEL in legacy mode; a SINGLE-CYCLE PULSE otherwise.
  //
  // Both are gated by the mode, so exactly one is ever active. A design
  // that drove both would signal the same condition twice through two
  // mechanisms -- and section 1 states legacy_interrupt_i "is not used"
  // for a Function in MSI or MSI-X mode (section 16, mutation 10).
  // ==================================================================
  assign legacy_level = legacy_mode &&  condition_sticky;
  assign edge_pulse   = !legacy_mode && condition_sticky && !prev_q;
 
endmodule

Classification: synthesizable.

This block exists because the same hardware condition means different things in different modes. In Legacy mode the host needs a held level it can sample and clear (§3). In MSI or MSI-X mode it needs a single event, because a message-signalled interrupt is delivered once and is not re-read from a wire.

A design that ignored the mode and always produced a level would, in MSI mode, either send one message and then nothing (the condition stays high, no new edge) or send a message every cycle. Both are wrong, and neither shows up in a Legacy-mode test.

Failure — three. Ignoring the mode. Driving both outputs, signalling twice. And an edge detector with no reset seeding, which emits a spurious pulse coming out of reset.

15. Assertions

// SVA over the INTx blocks. LOCAL contract only. Nothing asserts that the
// host services an interrupt, that software ever clears a source, or that
// the Link is ever able to carry a message.
 
// ---- ENVIRONMENT ------------------------------------------------------
assume property (@(posedge clk) disable iff (!rst_n)
  intx_enabled |-> $stable(pin));      // the Interrupt Pin is build-time
 
// ---- SOURCE STICKINESS ------------------------------------------------
 
// P1: A SOURCE IS STICKY UNTIL SOFTWARE CLEARS IT. The device does not get
// to decide the condition has passed (section 3).
property p_sticky;
  @(posedge clk) disable iff (!rst_n)
  (pending[i] && !sw_clear[i]) |=> pending[i];
endproperty
a_sticky : assert property (p_sticky);
 
// P2: SET BEATS CLEAR in the same cycle -- an event arriving while
// software is clearing must not be lost (section 11).
property p_set_wins;
  @(posedge clk) disable iff (!rst_n)
  (src_event[i] && sw_clear[i]) |=> pending[i];
endproperty
a_setwins : assert property (p_set_wins);
 
// P3: a disabled source cannot raise the Function level.
property p_enable_gates;
  @(posedge clk) disable iff (!rst_n)
  func_level |-> |(pending & src_enable);
endproperty
a_enable : assert property (p_enable_gates);
 
// ---- THE RECONCILER -- THE CENTRAL PROPERTIES -------------------------
 
// P4: A MESSAGE IS OWED EXACTLY WHEN BELIEF DISAGREES WITH THE LEVEL.
// Stated independently of the DUT's own `owed` wire so a miswiring fails
// rather than agreeing with itself.
property p_owed_iff_mismatch;
  @(posedge clk) disable iff (!rst_n)
  intx_enabled |-> (msg.valid == (belief != agg_level));
endproperty
a_owed : assert property (p_owed_iff_mismatch);
 
// P5: THE MESSAGE REPORTS THE CURRENT LEVEL, not a remembered direction.
property p_kind_matches_level;
  @(posedge clk) disable iff (!rst_n)
  msg.valid |-> (msg.kind == (agg_level ? MSG_ASSERT : MSG_DEASSERT));
endproperty
a_kind : assert property (p_kind_matches_level);
 
// P6: BELIEF ADVANCES ONLY ON AN ACCEPTED TRANSFER. Advancing on `valid`
// records a message the Link never carried.
property p_belief_on_fire;
  @(posedge clk) disable iff (!rst_n)
  (belief != $past(belief)) |-> ($past(msg.valid) && $past(msg_ready))
                             || $past(!intx_enabled) || $past(!rst_n);
endproperty
a_fire : assert property (p_belief_on_fire);
 
// P7: THE CONVERGENCE PROPERTY. If the level is stable and messages are
// being accepted, the belief matches within one transfer. This is section
// 5's invariant, bounded rather than stated as liveness.
property p_converges;
  @(posedge clk) disable iff (!rst_n)
  ($stable(agg_level) && intx_enabled && msg.valid && msg_ready)
    |=> in_sync;
endproperty
a_converge : assert property (p_converges);
 
// P8: NO STUCK INTERRUPT -- belief cannot remain asserted while the level
// is deasserted and messages are flowing.
property p_no_stuck;
  @(posedge clk) disable iff (!rst_n)
  (belief && !agg_level && intx_enabled) |-> msg.valid;
endproperty
a_stuck : assert property (p_no_stuck);
 
// P9: NO LOST INTERRUPT -- the mirror image.
property p_no_lost;
  @(posedge clk) disable iff (!rst_n)
  (!belief && agg_level && intx_enabled) |-> msg.valid;
endproperty
a_lost : assert property (p_no_lost);
 
// ---- TRANSMISSION -----------------------------------------------------
 
// P10: the message is HELD and STABLE while the transmit path stalls.
property p_held_stable;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && !tx_ready) |=> (tx_valid && $stable(tx_pin) && $stable(tx_kind));
endproperty
a_held : assert property (p_held_stable);
 
// P11: NO INTERRUPT MESSAGE WHILE THE LINK FORBIDS NORMAL TRAFFIC.
// Bound against Module 18's gate -- an INTx message is a TLP.
property p_no_traffic_outside_l0;
  @(posedge clk) disable iff (!rst_n)
  tx_valid |-> link_ok;
endproperty
a_link : assert property (p_no_traffic_outside_l0);
 
// P12: a blocked message is NOT lost -- the reconciler still owes it.
property p_blocked_recovers;
  @(posedge clk) disable iff (!rst_n)
  (send_blocked && (belief != agg_level) && intx_enabled) |-> msg.valid;
endproperty
a_blocked : assert property (p_blocked_recovers);
 
// ---- MODE -------------------------------------------------------------
 
// P13: EXACTLY ONE MECHANISM IS ACTIVE. Section 1: legacy_interrupt_i "is
// not used" for a Function in MSI or MSI-X mode.
property p_one_mechanism;
  @(posedge clk) disable iff (!rst_n)
  !(legacy_level && edge_pulse);
endproperty
a_mode : assert property (p_one_mechanism);
 
// P14: no INTx message at all outside Legacy mode.
property p_no_intx_in_msi;
  @(posedge clk) disable iff (!rst_n)
  (msi_enable || msix_enable) |-> !msg.valid;
endproperty
a_nointx : assert property (p_no_intx_in_msi);
 
// P15: the edge form is a single cycle.
property p_pulse_is_one_cycle;
  @(posedge clk) disable iff (!rst_n) edge_pulse |=> !edge_pulse;
endproperty
a_pulse : assert property (p_pulse_is_one_cycle);
 
// P16: reset.
property p_reset;
  @(posedge clk) !rst_n |=> (!belief && !msg.valid && (pending == '0));
endproperty
a_reset : assert property (p_reset);

P8 and P9 are §5's two failure modes stated as properties, and they are deliberately separate: P8 forbids a stuck interrupt, P9 forbids a lost one. An implementation can violate either without the other, and §16's two mutations do exactly that.

P4 is the reconciler's definition, restated so a miswired owed fails rather than agreeing with itself.

And P12 is the property that makes §13's blocking benign. A message that cannot be sent is not lost, because the obligation is derived from a comparison, not stored in a queue.

No liveness. "The interrupt is eventually serviced" depends on the host; "the message is eventually sent" depends on the Link. P7 is the bounded form — convergence within one accepted transfer.

16. Verification, Fault Injection, and Model Verification

Executed before publication — and the first formulation was wrong, which is how the numbers below came to exist.

Level reconstruction — exhaustive

Every level sequence up to length 11 × four merge-window depths — 16,376 cases — checking §5's invariant: when the level settles, does the host's belief equal it?

And the two broken formulations fail in opposite directions, which is the finding worth the whole section:

Read the first witness carefully. Three messages for a line that ended up asserted, and the last one is a Deassert — a stale pending transition flushed after a newer one had already been sent directly. The host's final belief is wrong, and nothing will correct it.

The reconciler is also cheaper. Over 20,000 random sequences at window 2: 78,586 messages versus 99,396 — 20.9% fewer, because transitions that cancel while the path is busy never become messages (§6).

Directed tests

• Single source asserts and is cleared — verify exactly one Assert and one Deassert.
• Second source asserts mid-episode — verify no message (§9). Required.
• First source cleared while the second still asserts — verify no Deassert until the last is cleared. Required.
• Event and sw_clear in the same cycle — verify the event survives (P2). Required.
• A still-true src_level cleared by software — verify it re-asserts (§3), and that this is reported rather than suppressed.
• Level toggles faster than the message path — every pattern from §16's exhaustive set; verify convergence (P7).
• Transmit path stalls for 1, 2 and 50 cycles — verify hold and field stability (P10).
• link_ok low across a level change — verify no message, and that the correct message is sent when it returns (P11, P12). Required.
• Mode switched to MSI mid-episode — verify belief resets and no INTx message follows (P14).
• Mode switched back to Legacy with the level high — verify an Assert is sent (the belief was reset, so a message is owed).
• All four pins; N_SRC = 1, 2, 8, 32; reset with the level high.

The scoreboard maintains its own belief model from (agg_level, msg accepted) alone and never reads belief, in_sync or the DUT's owed.

Mutations

Same-cycle audit

17. Debugging

Symptom → which direction the belief diverged → signal → distinguishing experiment.

The handler runs constantly with nothing to do

A stuck interrupt (§5) — the host believes asserted, the device is not.

Two candidates, and they are distinguished by looking at the device, not the host.

If agg_level is low and belief is high, the emulation diverged — mutation 1, the queue formulation, or mutation 5, a belief advanced on valid. P8 is that check made permanent.

If agg_level is genuinely high, nothing is wrong with the interrupt path: a source is still asserting. Read pending (§11) and find which. Common causes are a condition that is still true (§3), or a driver clearing one source while another remains — §9's exact case.

The distinguishing experiment: read pending and agg_level on the device. They separate "the emulation is broken" from "the device really is interrupting" in one look, and the two lead to completely different investigations.

The device is asserting and nothing happens

A lost interrupt (§5) — the quiet failure, and usually discovered as a timeout rather than as an interrupt problem at all.

Check in_sync (§12). If belief is low while agg_level is high and no message is outstanding, the belief desynchronized — mutation 1's A,A,D witness produces exactly this.

Then check send_blocked (§13). If the Link has been outside L0 — retraining, or in a power state (Chapter 18.7, Chapter 18.8) — the message is waiting, not lost, and P12 guarantees it goes out when the Link returns. A long block looks identical to a lost interrupt from the host's side and is not one.

And check the mode (§14). A Function switched to MSI while the driver still expects INTx will see nothing on the INTx path — correctly, per §1.

Every driver on the pin is being called

Expected (§7). The OR discards identity, so the host must ask every registered driver.

What is worth investigating is the rate. A shared pin with a storm from one device penalizes every driver on it — so the first question is which device is asserting, answered by reading each device's pending, not by instrumenting the host.

And it is the structural argument for MSI: a message-signalled interrupt carries identity, so there is nobody else to poll.

Interrupts work until the Link enters a power state

Read send_blocked (§13) and the LTSSM state together.

An INTx message is a TLP, so it obeys every rule Module 18 established: no normal traffic outside L0 (Chapter 18.6 §7), and a packet offered during L0s or L1 waits rather than being dropped (Chapter 18.7 §18).

So the interrupt latency includes the Link's wake latency — Chapter 18.8 §11's exit latency encodings reach "more than 64 μs". An interrupt that seems slow may be waiting on a Link that is asleep, which is a power-policy finding rather than an interrupt one.

18. Common Misconceptions

• "PCIe has interrupt wires." It has messages that emulate them (§2).
• "INTx is edge-triggered." Level-sensitive, held until software clears it (§3).
• "The device deasserts when the condition passes." Software decides, by clearing the source (§3).
• "Every transition produces a message." Transitions too close together are merged (§6).
• "Merging loses interrupts." It cannot, if the design reconciles state rather than queueing edges (§6, §12).
• "The host samples the interrupt line." There is no line; the host holds a reconstruction (§4).
• "An INTx message identifies the source." Two stages of OR discard that (§7).
• "A second source asserting sends a second message." The level never changed (§9).
• "INTA is an IRQ number." Different identifiers, different owners (§8).
• "A device can use INTx and MSI together." §1: legacy is "not used" for a Function in MSI or MSI-X mode (§14).
• "The interrupt condition is the same signal in every mode." Level in Legacy, pulse in MSI/MSI-X (§14).
• "An interrupt message bypasses flow control." It is a TLP, subject to credits and to LTSSM state (§13).
• "A blocked message is a lost interrupt." Not with a reconciler (P12).
• "Interrupt storms mean broken hardware." Often a source that is still legitimately asserting (§17).

19. Understanding Check

20. What's Next

INTx is a wire that does not exist, emulated well enough that software cannot tell.

The emulation is a level → edge → level round trip (§4), and its correctness rests on one invariant: when the level settles, the host's belief must equal it (§5). Violate it one way and the handler runs forever; violate it the other and nothing ever runs again.

And the architecture that gets it right is not the obvious one. Queueing transitions is wrong in 11.6% of cases; reconciling belief against level is exact and sends 20.9% fewer messages (§16).

What INTx cannot do is carry identity. Two stages of OR discard which Function, which source, and how many (§7) — so every driver on a shared pin is called on every interrupt, and each one polls its own registers to find out whether it has work.

Chapter 19.2 — MSI removes exactly that. An interrupt becomes a memory write — a TLP the device transmits to an address the host supplied — and that one change gives it identity, removes the sharing, and makes the interrupt travel the same path as data. It also introduces constraints INTx never had: a vector count that must be a power of two, and an interrupt that is now subject to flow control and ordering like any other write.

The idea to carry forward: transmit state, not transitions — a state-based protocol repairs its own mistakes.