Packet Types — The Taxonomy That Drives Everything Else

Module 11 has built a packet from the outside in. Chapter 11.1 framed what a TLP is, 11.2 counted it, 11.3 decoded its header, 11.4 moved its data, 11.5 sent it somewhere, and 11.6 attached policy to it.

Every one of those chapters said, at some point, this depends on what kind of packet it is.

This is that chapter.

What are the major TLP packet families, how are they classified, and what semantic differences determine their payload, routing, posted/non-posted behaviour, and Completion expectations?

1. Type Is Not One Fact Among Many — It Is the Selector

Look back at what the module has established, and notice how much of it was conditional.

Six chapters, one recurring dependency. Packet type is not a property alongside the others — it is the discriminant that decides what the others mean.

And it has an architectural consequence that this chapter's RTL is built around: if type determines all of that, then type should be decoded once and the consequences should be carried forward, rather than each consumer re-deriving them. §8 is that principle stated properly.

2. The Verified Taxonomy

3. The Family Table

Encodings tell you how to recognise a packet. This tells you what recognising it obliges you to do.

Every cell above is a canonical statement about the family's ordinary form. Variants exist, and the module chapters that own each family cover them. This table is for building a classifier, not for reasoning about edge cases.

4. The Families, Briefly

Each of these is owned in depth elsewhere. What follows is the semantic lifecycle each family represents — enough to classify, not enough to implement the family.

Memory

The dominant traffic on almost every link. Address-routed, targeting the memory space a Function exposes through its BARs (Chapter 9.2).

Memory Read is a non-posted Request. It carries no payload — it carries a request for one. The data returns in Completion with Data packets, and Chapter 12.1 traces that lifecycle end to end.

Memory Write is posted in the canonical model. It carries its payload, and no Completion normally returns.

Both exist in 3 DW and 4 DW forms, chosen by the address width the operation needs (Chapter 11.3 §13).

I/O

Architecturally distinct because it targets I/O address space, not memory space — a separate space with its own semantics (Chapter 9.3).

Both I/O Read and I/O Write are non-posted, so both expect a Completion. Both use the 3 DW form — I/O space has no 64-bit form, which is a structural consequence of the space itself rather than a packet-format choice.

On modern systems I/O space is uncommon and its use is discouraged for new designs. Chapter 9.3 covered why. It appears here because the taxonomy is not complete without it and because a receiver must classify it correctly even if it then rejects it.

Configuration

Targets a Function's configuration space rather than any address space, which is why it is ID-routed (Chapter 11.5 §5) — and why enumeration works before a single BAR has been assigned.

Type 0 and Type 1 are different packet types, 00100 and 00101, and the distinction is about how far the access has travelled through the hierarchy rather than about what it does. Both read and write forms are non-posted.

The configuration mechanism itself, ECAM, and the header layouts are Modules 7–8's and are not re-taught here.

Completion

A Completion is a TLP. That sentence corrects a mental model more often than it informs one — Completions are routinely imagined as some lower-level acknowledgement rather than as a packet with a header, a type and a routing mechanism like any other.

Two forms at the taxonomy level:

• Completion (Cpl) — no data. It answers an operation that returns none: the completion of a write, or a Request that ended without data.
• Completion with Data (CplD) — carries the requested data.

A Completion for Locked Read is a distinct type (01011), separate from the ordinary Completion type.

Completion Status, Byte Count, Lower Address, and the rules governing how a Request's answer may be split across several Completions are Module 13's and are not published here. Chapter 10.2 covered the transaction-level role.

Message

Not every protocol action is an address-based data access. Some notifications and actions between components have no natural address and no natural data transfer — an event signalled toward the host, a power-management action, a platform-level notification.

Messages exist for those. They always use a 4 DW header — the extra DW carries the Message's own destination or context, since it may be routed by address, by ID, or implicitly depending on the r[2:0] sub-field.

Msg and MsgD are distinguished by Fmt, exactly as elsewhere: 001b for no data, 011b for with data.

The Message taxonomy and its routing encodings belong to later Message material and are not enumerated here.

5. Packet Type Drives Local Dispatch

6. RTL — Packet Type Classifier

// SYNTHESIZABLE. Classify a TLP into a normalized packet kind.
// The Fmt and Type encodings matched below: NORMATIVE (PCI Express Base
// Specification packet-type definitions, section 2).
// The enum, its encoding, and the port names: ILLUSTRATIVE normalized
// internal metadata. Conventional non-Flit representation only.
package pkt_kind_pkg;
 
  typedef enum logic [3:0] {
    PKT_MEM_RD      = 4'd0,
    PKT_MEM_WR      = 4'd1,
    PKT_IO_RD       = 4'd2,
    PKT_IO_WR       = 4'd3,
    PKT_CFG_RD      = 4'd4,
    PKT_CFG_WR      = 4'd5,
    PKT_CPL         = 4'd6,   // Completion, no data
    PKT_CPLD        = 4'd7,   // Completion with Data
    PKT_MSG         = 4'd8,
    PKT_MSGD        = 4'd9,
    PKT_UNSUPPORTED = 4'd15   // not represented by this model
  } packet_kind_e;
 
  // NORMATIVE Fmt encodings.
  localparam logic [2:0] FMT_3DW_ND = 3'b000;
  localparam logic [2:0] FMT_4DW_ND = 3'b001;
  localparam logic [2:0] FMT_3DW_D  = 3'b010;
  localparam logic [2:0] FMT_4DW_D  = 3'b011;
  localparam logic [2:0] FMT_PREFIX = 3'b100;
 
  // NORMATIVE Type encodings for the families this model represents.
  localparam logic [4:0] TYP_MEM    = 5'b00000;
  localparam logic [4:0] TYP_IO     = 5'b00010;
  localparam logic [4:0] TYP_CFG0   = 5'b00100;
  localparam logic [4:0] TYP_CFG1   = 5'b00101;
  localparam logic [4:0] TYP_CPL    = 5'b01010;
  // Messages: Type is 10rrr. Only the upper two bits are matched here; the
  // r[2:0] routing sub-field is deliberately NOT resolved (section 2).
  localparam logic [1:0] TYP_MSG_HI = 2'b10;
 
endpackage

import pkt_kind_pkg::*;
 
module tlp_kind_classify (
  // Base header fields, already extracted by the single header decoder.
  // This module does NOT slice a raw header — that happened once, upstream.
  input  logic         hdr_valid,
  input  logic [2:0]   fmt,
  input  logic [4:0]   typ,
 
  output packet_kind_e kind,
  output logic         prefix_present
);
 
  // Fmt carries two independent facts (Chapter 11.3 section 4).
  wire with_data = (fmt == FMT_3DW_D) || (fmt == FMT_4DW_D);
  wire is_4dw    = (fmt == FMT_4DW_ND) || (fmt == FMT_4DW_D);
  wire fmt_base  = (fmt == FMT_3DW_ND) || (fmt == FMT_4DW_ND)
                || (fmt == FMT_3DW_D)  || (fmt == FMT_4DW_D);
 
  assign prefix_present = hdr_valid && (fmt == FMT_PREFIX);
 
  always_comb begin
    kind = PKT_UNSUPPORTED;
 
    if (hdr_valid && fmt_base) begin
      // NOTE the shape: every arm consults BOTH typ and with_data. Memory
      // Read and Memory Write share Type 00000 and are separated only by
      // Fmt — a case on typ alone cannot distinguish them (section 2).
      unique case (typ)
        TYP_MEM:  kind = with_data ? PKT_MEM_WR : PKT_MEM_RD;
 
        // I/O has no 64-bit form: a 4 DW I/O packet is not represented.
        TYP_IO:   kind = is_4dw ? PKT_UNSUPPORTED
                                : (with_data ? PKT_IO_WR : PKT_IO_RD);
 
        // Type 0 and Type 1 are distinct packet types but the same local
        // engine consumes them; the distinction is preserved upstream in the
        // descriptor rather than collapsed here into a separate kind.
        TYP_CFG0,
        TYP_CFG1: kind = is_4dw ? PKT_UNSUPPORTED
                                : (with_data ? PKT_CFG_WR : PKT_CFG_RD);
 
        TYP_CPL:  kind = is_4dw ? PKT_UNSUPPORTED
                                : (with_data ? PKT_CPLD : PKT_CPL);
 
        default: begin
          // Messages are Type 10rrr with a 4 DW header. The r[2:0] sub-field
          // is NOT decoded here.
          if ((typ[4:3] == TYP_MSG_HI) && is_4dw)
            kind = with_data ? PKT_MSGD : PKT_MSG;
          else
            kind = PKT_UNSUPPORTED;
        end
      endcase
    end
  end
 
endmodule

Classification: synthesizable (package: compile-time).

Architecture. One combinational block consuming already-extracted fields. It does not touch the raw header — that is §8's principle, applied to the classifier itself so that even this module is not a second decode site.

State. None. Classification is a pure function of {fmt, typ}.

Contract. The caller supplies fields extracted by the single header decoder. Downstream relies on kind being stable while hdr_valid and the fields are held.

Failure — three, and the first is the one this chapter exists to prevent. A case on typ alone maps every memory packet to one kind, so every memory write is classified as a memory read and vice versa, at a 50% rate, on the most common traffic in the system. Omitting fmt_base classifies a prefix-bearing header as an ordinary packet. And matching Messages on the full typ rather than on typ[4:3] classifies seven of the eight routing sub-field values as unsupported.

Deliberately simplified: no r[2:0] resolution; no locked-transaction types; no prefix handling beyond detection; Type 0 and Type 1 configuration not separated into distinct kinds.

DV. §10's P1–P4.

7. RTL — Semantic Property Derivation

This is where a taxonomy becomes an architecture. The classifier produced a label; this produces the consequences of that label, so that no downstream block ever has to know what a PKT_IO_WR is.

// SYNTHESIZABLE. Derive local semantic properties from a normalized packet
// kind. Each mapping reflects the VERIFIED transaction semantics of section 3
// for that family's CANONICAL form; the property names, the engine enum and
// the route enum are ILLUSTRATIVE normalized metadata.
import pkt_kind_pkg::*;
import tlp_route_pkg::*;   // Chapter 11.5's routing modes
 
typedef enum logic [2:0] {
  ENG_MEM  = 3'd0,
  ENG_IO   = 3'd1,
  ENG_CFG  = 3'd2,
  ENG_CPL  = 3'd3,
  ENG_MSG  = 3'd4,
  ENG_ERR  = 3'd5
} engine_e;
 
module tlp_semantics (
  input  logic         in_valid,
  input  packet_kind_e kind,
 
  output logic         is_request,
  output logic         needs_completion,
  output logic         has_payload,
  output route_mode_e  route_mode,
  output engine_e      target_engine,
  output logic         unsupported
);
 
  always_comb begin
    // Safe defaults. Anything not explicitly enumerated falls to the error
    // path rather than to a plausible-looking guess.
    is_request       = 1'b0;
    needs_completion = 1'b0;
    has_payload      = 1'b0;
    route_mode       = ROUTE_UNKNOWN;
    target_engine    = ENG_ERR;
    unsupported      = 1'b1;
 
    if (in_valid) begin
      unique case (kind)
        // --- Memory ----------------------------------------------------
        PKT_MEM_RD: begin
          is_request = 1'b1; needs_completion = 1'b1; has_payload = 1'b0;
          route_mode = ROUTE_ADDRESS; target_engine = ENG_MEM;
          unsupported = 1'b0;
        end
        PKT_MEM_WR: begin
          // POSTED in the canonical model: payload out, no Completion back.
          is_request = 1'b1; needs_completion = 1'b0; has_payload = 1'b1;
          route_mode = ROUTE_ADDRESS; target_engine = ENG_MEM;
          unsupported = 1'b0;
        end
 
        // --- I/O — NON-POSTED IN BOTH DIRECTIONS (section 3) ------------
        // needs_completion is TRUE for the write. This is exactly the case
        // that a "writes are posted" shortcut gets wrong.
        PKT_IO_RD: begin
          is_request = 1'b1; needs_completion = 1'b1; has_payload = 1'b0;
          route_mode = ROUTE_ADDRESS; target_engine = ENG_IO;
          unsupported = 1'b0;
        end
        PKT_IO_WR: begin
          is_request = 1'b1; needs_completion = 1'b1; has_payload = 1'b1;
          route_mode = ROUTE_ADDRESS; target_engine = ENG_IO;
          unsupported = 1'b0;
        end
 
        // --- Configuration — non-posted, ID-routed ----------------------
        PKT_CFG_RD: begin
          is_request = 1'b1; needs_completion = 1'b1; has_payload = 1'b0;
          route_mode = ROUTE_ID; target_engine = ENG_CFG;
          unsupported = 1'b0;
        end
        PKT_CFG_WR: begin
          is_request = 1'b1; needs_completion = 1'b1; has_payload = 1'b1;
          route_mode = ROUTE_ID; target_engine = ENG_CFG;
          unsupported = 1'b0;
        end
 
        // --- Completion — a RESPONSE, so it needs none of its own -------
        PKT_CPL: begin
          is_request = 1'b0; needs_completion = 1'b0; has_payload = 1'b0;
          route_mode = ROUTE_ID; target_engine = ENG_CPL;
          unsupported = 1'b0;
        end
        PKT_CPLD: begin
          is_request = 1'b0; needs_completion = 1'b0; has_payload = 1'b1;
          route_mode = ROUTE_ID; target_engine = ENG_CPL;
          unsupported = 1'b0;
        end
 
        // --- Message ---------------------------------------------------
        // Route mode stays UNKNOWN: it depends on the r[2:0] sub-field,
        // which section 6 deliberately does not resolve. Reported, not
        // guessed — a default of ROUTE_IMPLICIT would be wrong for the
        // Messages that route by address or by ID (Chapter 11.5 section 6).
        PKT_MSG: begin
          is_request = 1'b1; needs_completion = 1'b0; has_payload = 1'b0;
          route_mode = ROUTE_UNKNOWN; target_engine = ENG_MSG;
          unsupported = 1'b0;
        end
        PKT_MSGD: begin
          is_request = 1'b1; needs_completion = 1'b0; has_payload = 1'b1;
          route_mode = ROUTE_UNKNOWN; target_engine = ENG_MSG;
          unsupported = 1'b0;
        end
 
        default: begin
          target_engine = ENG_ERR; unsupported = 1'b1;
        end
      endcase
    end
  end
 
endmodule

Classification: synthesizable.

Architecture. A pure lookup from normalized kind to normalized consequences. Its value is that it is the only place these mappings exist — change one and every consumer changes with it.

State. None.

Contract. Downstream engines rely on needs_completion, has_payload and route_mode instead of re-deriving them from the packet. That reliance is the architecture, and it only works if no engine also keeps a private copy of the mapping.

Failure — and the first two are the reason each mapping is written out longhand rather than computed. Deriving needs_completion as "not a write" makes I/O writes posted, so no outstanding entry is allocated and the returning Completion has nothing to match. Deriving has_payload from needs_completion inverts the memory cases. And defaulting an unresolved route_mode to ROUTE_IMPLICIT for Messages guesses wrong for every Message that routes by address or ID.

Deliberately simplified: canonical forms only; no locked transactions; no per-variant refinement within a family; Type 0/Type 1 configuration collapsed to one engine.

Production implication: a real design refines these per variant and resolves the Message routing sub-field. What does not change is that the refinement happens here, once, and not in each consumer.

8. One Decode, One Source of Truth

9. RTL — One-Hot Engine Dispatch

// SYNTHESIZABLE. Deliver a classified packet to exactly one local consumer.
// The engine set and the interface: ILLUSTRATIVE. The one-hot guarantee and
// the stability-under-stall contract: local design requirements.
import pkt_kind_pkg::*;
 
module tlp_dispatch (
  input  logic         clk,
  input  logic         rst_n,
 
  input  logic         in_valid,
  input  engine_e      target_engine,
  input  logic         unsupported,
  input  packet_kind_e kind,          // carried through as metadata
 
  // Every consumer backpressures independently.
  input  logic         mem_ready,
  input  logic         io_ready,
  input  logic         cfg_ready,
  input  logic         cpl_ready,
  input  logic         msg_ready,
  input  logic         err_ready,
 
  output logic         mem_valid,
  output logic         io_valid,
  output logic         cfg_valid,
  output logic         cpl_valid,
  output logic         msg_valid,
  output logic         err_valid,
 
  output packet_kind_e out_kind,      // shared metadata, stable under stall
  output logic         in_ready
);
 
  // Exactly one valid, always. Written as a decode of a single enum rather
  // than as independent comparisons, so two engines CANNOT both be selected —
  // the property is structural, not something the assertions merely hope for.
  wire sel_err = unsupported || (target_engine == ENG_ERR);
 
  assign mem_valid = in_valid && !sel_err && (target_engine == ENG_MEM);
  assign io_valid  = in_valid && !sel_err && (target_engine == ENG_IO);
  assign cfg_valid = in_valid && !sel_err && (target_engine == ENG_CFG);
  assign cpl_valid = in_valid && !sel_err && (target_engine == ENG_CPL);
  assign msg_valid = in_valid && !sel_err && (target_engine == ENG_MSG);
  assign err_valid = in_valid &&  sel_err;
 
  // Backpressure comes from the SELECTED engine only. A design that ANDed
  // every ready would stall on engines that are not involved.
  always_comb begin
    unique case (1'b1)
      mem_valid: in_ready = mem_ready;
      io_valid:  in_ready = io_ready;
      cfg_valid: in_ready = cfg_ready;
      cpl_valid: in_ready = cpl_ready;
      msg_valid: in_ready = msg_ready;
      err_valid: in_ready = err_ready;
      default:   in_ready = 1'b0;
    endcase
  end
 
  // Metadata is a straight pass-through: selection and metadata come from the
  // same descriptor, so they cannot drift apart under stall.
  assign out_kind = kind;
 
endmodule

Classification: synthesizable.

Architecture. A one-hot decode of a single enum. Mutual exclusion is structural — there is no configuration under which two *_valid outputs assert, because they are decodes of one value rather than independent predicates.

State. None. Stability under stall is inherited from the descriptor the caller holds, which is why §10's P8 is stated over the caller's held descriptor rather than over internal state this module does not have.

Cycle behaviour. Combinational. Transfer occurs when the selected engine's ready is high; the caller must hold in_valid and the descriptor until then.

Contract. Consumers rely on receiving a packet only when their own valid is asserted, and on never seeing a packet another engine also received. The caller relies on in_ready reflecting only the selected engine.

Failure — three. Independent per-engine comparisons instead of one enum decode allow two engines to accept the same packet if the selection logic is ever inconsistent. in_ready computed as the AND of all readies stalls a memory packet behind an unrelated busy configuration engine. And omitting the sel_err term from the normal engines lets an unsupported packet enter both a real engine and the error path.

Deliberately simplified: no data path — this dispatches descriptors, not packets; no per-engine queueing; no arbitration, since exactly one consumer is selected.

10. Assertions

// SVA over tlp_kind_classify, tlp_semantics and tlp_dispatch. These assert
// the LOCAL contracts of the taught subset plus the normative encodings of
// section 2 — not exhaustive PCIe packet legality.
 
// CLASSIFY — P1: THE CHAPTER'S CENTRAL ENCODING PROPERTY. Read and write
// within a family are separated by Fmt, not by Type. A classifier that
// switched on Type alone fails this on the first memory write.
property p_fmt_separates_read_write;
  @(posedge clk) disable iff (!rst_n)
  (hdr_valid && (typ == TYP_MEM) && fmt_base)
    |-> (kind == (with_data ? PKT_MEM_WR : PKT_MEM_RD));
endproperty
a_mem_rd_wr : assert property (p_fmt_separates_read_write);
 
// CLASSIFY — P2: a prefix-bearing header is never an ordinary packet kind.
property p_prefix_not_a_kind;
  @(posedge clk) disable iff (!rst_n)
  prefix_present |-> (kind == PKT_UNSUPPORTED);
endproperty
a_prefix : assert property (p_prefix_not_a_kind);
 
// CLASSIFY — P3: a 4 DW header is never classified as I/O, Configuration or
// Completion. Those families have no 64-bit form in the taught subset.
property p_no_4dw_for_3dw_only_families;
  @(posedge clk) disable iff (!rst_n)
  (hdr_valid && is_4dw)
    |-> !(kind inside {PKT_IO_RD, PKT_IO_WR, PKT_CFG_RD,
                       PKT_CFG_WR, PKT_CPL, PKT_CPLD});
endproperty
a_no_4dw : assert property (p_no_4dw_for_3dw_only_families);
 
// CLASSIFY — P4: Messages are 4 DW. Catches a Message matched on typ alone.
property p_msg_is_4dw;
  @(posedge clk) disable iff (!rst_n)
  (hdr_valid && (kind inside {PKT_MSG, PKT_MSGD})) |-> is_4dw;
endproperty
a_msg_4dw : assert property (p_msg_is_4dw);
 
// SEMANTICS — P5: THE I/O WRITE PROPERTY. Both I/O directions are
// non-posted. Written as a named property because it is the single mapping a
// "writes are posted" shortcut gets wrong (section 3).
property p_io_write_is_non_posted;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && (kind == PKT_IO_WR)) |-> (needs_completion && has_payload);
endproperty
a_io_wr_np : assert property (p_io_write_is_non_posted);
 
// SEMANTICS — P6: a posted-class packet never requests Completion tracking.
property p_posted_needs_no_completion;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && (kind inside {PKT_MEM_WR, PKT_MSG, PKT_MSGD}))
    |-> !needs_completion;
endproperty
a_posted : assert property (p_posted_needs_no_completion);
 
// SEMANTICS — P7: a Completion is never a Request and never owes one.
property p_completion_is_a_response;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && (kind inside {PKT_CPL, PKT_CPLD}))
    |-> (!is_request && !needs_completion);
endproperty
a_cpl_response : assert property (p_completion_is_a_response);
 
// SEMANTICS — P8: payload expectation agrees with the Fmt that produced the
// kind. Ties the semantic layer back to the encoding layer, so the two
// cannot drift apart.
property p_payload_agrees_with_fmt;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && !unsupported)
    |-> (has_payload == (kind inside {PKT_MEM_WR, PKT_IO_WR,
                                      PKT_CFG_WR, PKT_CPLD, PKT_MSGD}));
endproperty
a_payload_agrees : assert property (p_payload_agrees_with_fmt);
 
// SEMANTICS — P9: route mode agrees with the family. Configuration and
// Completion are ID-routed; Memory and I/O are address-routed.
property p_route_mode_agrees_with_family;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && !unsupported)
    |-> ((kind inside {PKT_MEM_RD, PKT_MEM_WR, PKT_IO_RD, PKT_IO_WR})
           ? (route_mode == ROUTE_ADDRESS)
       : (kind inside {PKT_CFG_RD, PKT_CFG_WR, PKT_CPL, PKT_CPLD})
           ? (route_mode == ROUTE_ID)
           : (route_mode == ROUTE_UNKNOWN));
endproperty
a_route_agrees : assert property (p_route_mode_agrees_with_family);
 
// DISPATCH — P10: EXACTLY ONE consumer. Neither zero nor two.
property p_exactly_one_engine;
  @(posedge clk) disable iff (!rst_n)
  in_valid |-> ($countones({mem_valid, io_valid, cfg_valid,
                            cpl_valid, msg_valid, err_valid}) == 1);
endproperty
a_one_hot : assert property (p_exactly_one_engine);
 
// DISPATCH — P11: an unsupported packet reaches ONLY the error path.
property p_unsupported_to_error_only;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && unsupported)
    |-> (err_valid && !mem_valid && !io_valid
                   && !cfg_valid && !cpl_valid && !msg_valid);
endproperty
a_unsupported_isolated : assert property (p_unsupported_to_error_only);
 
// DISPATCH — P12: selection and metadata are stable while the selected
// engine backpressures. A packet must not migrate between engines mid-offer.
property p_selection_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && !in_ready)
    |=> (in_valid && $stable({mem_valid, io_valid, cfg_valid,
                              cpl_valid, msg_valid, err_valid, out_kind}));
endproperty
a_stable : assert property (p_selection_stable_under_stall);
 
// DISPATCH — P13: no supported packet is silently dropped. Every accepted
// offer was accepted by the engine that was selected.
property p_no_silent_drop;
  @(posedge clk) disable iff (!rst_n)
  (in_valid && in_ready)
    |-> ((mem_valid && mem_ready) || (io_valid && io_ready)
      || (cfg_valid && cfg_ready) || (cpl_valid && cpl_ready)
      || (msg_valid && msg_ready) || (err_valid && err_ready));
endproperty
a_no_drop : assert property (p_no_silent_drop);

P1 and P5 are the two encoding facts most likely to be got wrong, promoted to named properties. P1 catches a classifier that cannot tell a memory read from a memory write; P5 catches a semantics table that assumes writes are posted. Both bugs are invisible to a testbench that exercises only memory reads and memory writes, because the first is 50% wrong on traffic nobody separates and the second concerns a family many designs never test.

P10 is stated as $countones == 1 rather than as a mutual-exclusion check, because the zero case is a real failure too: a packet that reaches no engine is dropped, and dropping is what P13 rules out from the other direction.

P8 and P9 are the anti-drift properties. They tie the semantic layer back to the encoding layer, so a change to the classifier that is not reflected in the semantics table fails immediately rather than at integration. This is the assertion-level expression of §8's single-source-of-truth principle: even within one design, the two representations must be provably consistent.

P12 is where routing and dispatch differ in their failure modes. A routing decision that wobbles sends a packet down two links; a dispatch decision that wobbles delivers one packet to two engines. Both are duplication, and only P12 catches the local one.

11. Debugging

A memory write reaches the completion engine

Classification, and specifically the Fmt/Type relationship.

Memory Write and Memory Read share Type 00000; Completion shares 01010 with Completion with Data. A design that lost the with_data term somewhere in its decode will confuse pairs, and the pairs it confuses tell you where.

Read the symptom precisely. A memory write reaching the completion engine is not a read/write confusion — those share a family and would both reach the memory engine. It is a Type mismatch, which means either the Type slice is wrong or the semantics table maps the kind to the wrong engine.

One observation separates them: print kind alongside target_engine. If kind is PKT_MEM_WR and the engine is ENG_CPL, the classifier is right and §7's table is wrong. If kind itself is a Completion kind, the classifier is wrong and §6 is where to look.

A configuration read routes correctly but never enters the config engine

Routing worked; dispatch did not. Two different layers (§5).

What "routed correctly" establishes. The packet's ID routing resolved, the bus-number ranges were right, and it arrived at the intended Function. Everything in Chapter 11.5 is exonerated.

So the fault is local, and there are three places it can be. The classifier produced PKT_UNSUPPORTED — check whether Type 00101 (Type 1) is in the case where only 00100 (Type 0) was handled. The semantics table mapped the kind to the wrong engine. Or dispatch is stalling because in_ready is the AND of every engine's ready and something unrelated is busy.

The third is distinguishable by timing: if the packet eventually arrives when other engines drain, it is backpressure, not classification.

A packet with a payload reaches an engine expecting none

Either the classification is wrong or has_payload was derived rather than mapped.

P8 is the property, and its shape explains the bug. has_payload must agree with the Fmt that produced the kind. A design that derives it — "requests with data are writes, so has_payload = is_write" — gets Completion with Data wrong, because a CplD is not a write and carries a payload.

The check: compare the with_data bit from Fmt against the engine's expectation for that specific packet. If Fmt says data and the engine expects none, the derivation replaced the mapping.

The same raw packet has different types in the routing block and the completion tracker

Stop debugging either block. The bug is that there are two decoders (§8).

Why this is the signature. A single decode cannot produce two answers. Two answers require two decoders, and the fact that they disagree means at least one is wrong — but which one is not the useful question, because the architecture is wrong regardless.

Why it is worse than either decoder being wrong alone. The design is now in a state no single block's logic can produce: the packet is simultaneously being routed as one thing and tracked as another. Outstanding state, routing decisions and error handling are all reasoning about different packets that happen to be the same packet.

The fix is structural, not a patch. Delete every decode except the one at the boundary, and have every consumer take the normalized descriptor. P8 and P9 are what keep it deleted — they assert that the semantic layer agrees with the encoding layer, so a re-introduced private decode that drifts fails immediately.

12. Verification

Monitors observe: the header fields entering the classifier; the normalized kind; every semantic output; and all six dispatch valids with their readies.

The scoreboard holds its own packet-semantics table, written from §2 and §3 — its own Fmt/Type match, its own family mapping, its own needs_completion and route_mode. It must not import pkt_kind_pkg, call tlp_kind_classify, or reuse tlp_semantics's case statement. The whole value of the semantics table is that it is the single source of truth in the design; a scoreboard that shares it verifies nothing.

Per-family classification

For every packet type in §2's table, drive its Fmt/Type pair and verify:

• the normalized kind
• has_payload against the Fmt
• route_mode against the family
• needs_completion against the transaction class
• target_engine
• exactly one dispatch valid

Specifically include, as named tests:

• Memory Read and Memory Write with the same Type 00000, differing only in Fmt. Verify they classify differently (P1).
• Both in 3 DW and 4 DW form. Four packets from one Type value.
• I/O Write. Verify needs_completion is true (P5) — the mapping a shortcut gets wrong.
• Completion and Completion with Data, same Type 01010. Verify is_request is false for both (P7).
• Configuration Type 0 and Type 1. Both must reach the configuration engine; a design handling only 00100 fails on Type 1.
• Msg and MsgD. Verify 4 DW is required (P4) and that route_mode is reported unknown rather than guessed.

Negative

• A Type value outside the taught subset. Verify PKT_UNSUPPORTED and the error path only (P11).
• A prefix-bearing header. Verify it is never an ordinary kind (P2).
• A 4 DW I/O, Configuration or Completion packet. Verify unsupported (P3) — and verify the report says not represented by this model, not malformed per PCIe (§13).
• Contradictory teaching metadata: a kind asserted with a payload flag that disagrees with its Fmt. Verify the design does not accept both.

Stress and boundary

• Every engine backpressured in turn while a packet for it is offered. Verify selection stability (P12) and that unrelated engines do not stall it.
• Back-to-back packets of different families, every ordered pair. Verify no state carries between them.
• Alternating posted and non-posted. Verify needs_completion toggles correctly and that no Completion tracking is allocated for posted packets (P6).
• A different packet kind every cycle for a long run. Verify one-hot holds throughout (P10).
• Reset mid-offer. Verify no engine sees a packet after reset.
• The error path backpressured while an unsupported packet is offered. Verify it does not stall the classifier for other traffic.

Coverage should include: every packet type in §2; both header forms where a family has both; every value of each semantic output; every target_engine; every ordered pair of consecutive families; and the unsupported and prefix paths.

13. Unsupported Is Not Malformed

A wording discipline that prevents an invented protocol behaviour, carried forward from Chapter 11.3 §11 and worth restating because this chapter is where the temptation peaks.

"Unsupported by this model" means the design's classifier does not represent this encoding. The packet may be entirely legal. Messages are legal and common; §6 simply does not resolve them fully. The right response is an explicit path and a report.

"Malformed TLP" is a normative protocol condition with specification-defined triggers and specification-defined required responses. This chapter has not verified those conditions, so labelling a locally-unrecognised packet as malformed would be asserting something the design does not know.

Why it matters beyond vocabulary: the two demand different behaviour. An unrecognised-but-legal packet may need forwarding or logging. A genuinely malformed TLP has a required response that later error-handling chapters own. A design that conflates them either mishandles legal traffic or fails to report illegal traffic.

The rule: a model's coverage boundary is a statement about the design, never about the specification.

14. Common Misconceptions

• "Fmt and Type are the same thing." Two separate fields — 3 bits and 5 bits — carrying structural and semantic information respectively (§2).
• "One Type value uniquely defines the packet." Memory Read and Memory Write share Type 00000. Fmt is what separates them (§2). This is the most consequential encoding fact in the chapter.
• "Every TLP is a Request." Completions are TLPs and they are responses. Classifying every packet as a Request means allocating outstanding state for answers (§4).
• "A Completion isn't really a packet type." It has a Type encoding, a header, a routing mechanism and two forms. It is a TLP like any other (§4).
• "Every write is posted." I/O writes and configuration writes are non-posted — they expect a Completion (§3). This is the mapping a "writes are posted" shortcut gets wrong.
• "Every Request carries a payload." Reads carry none — they carry a request for one (Chapter 11.4 §1).
• "A read packet carries the returned data." The data returns in a separate Completion with Data, travelling the other way (Chapter 12.1).
• "A Message TLP is just a memory write to a magic address." Messages are their own family with their own Type range, their own 4 DW header, and their own routing sub-field (§4).
• "Packet type and routing mode are the same concept." Type determines which routing mechanism applies; the mechanism then determines the destination. Different questions, different layers (§5).
• "Packet type and target engine are the same architectural layer." Type is a protocol fact; the engine set is a local design decision. §7 maps between them precisely because they are not the same thing.
• "Every downstream block should decode Fmt and Type itself." Decode once at the boundary; carry normalized meaning inward. Duplicated decode produces blocks that disagree about the same packet (§8).
• "An unrecognised packet is a malformed TLP." Unsupported-by-this-model is a statement about the design; malformed is a normative protocol condition with defined responses (§13).

15. Understanding Check

16. Module 11 Complete

Seven chapters have taken a TLP apart:

One architecture runs through all seven: decode the wire format once, at the boundary, into a normalized descriptor — and have everything downstream consume meaning rather than bits.

Module 12 now takes real transactions end to end. Chapter 12.1 — Memory Read traces one non-posted read from a local read intent through Request generation, outstanding state, address routing, the Completer's resource access, the Completion's return, correlation, and delivery to the right local consumer — the full distributed lifecycle that every chapter in Module 11 has been building the vocabulary for.

The idea to carry forward: packet type is not one field among many — it is the discriminant that decides what all the others mean, and it should be decoded exactly once.