Skip to content

PCIe · Module 10

Posted Transactions — Ownership That Ends on the Forward Path

A posted Request requires no Completion, so the Requester's ownership ends going out rather than coming back. Which Requests are posted, what the Requester consequently cannot know, why no Completion still means buffering and flow control, and the queue RTL that gets payload ownership right.

Chapter 10.2 built the return half of a split transaction and rested throughout on a division it did not justify: the definition of a Sequence is "a single Request and zero or more Completions."

This chapter is the zero.

What does it mean for a PCIe Request to be posted, and what ownership, buffering, observability, and error-handling consequences follow from not receiving a Completion?

1. Which Requests Are Posted

Two things in that table are worth reading against your instincts.

Not every write is posted. Memory Writes are posted. I/O Writes and Configuration Writes are non-posted and require Completion. A mental model of "reads wait, writes don't" is wrong in two of the four write cases, and Chapter 10.4 §2 is built around that correction.

Messages are posted. They are the other posted class, and they matter because Module 19's interrupt mechanisms and Module 15's power-management signalling ride on them. "Posted" is not a Memory-Write-only concept.

This chapter uses Memory Write as its canonical example — because Chapter 9.6 already followed one from a CPU store to a resource offset, so the learner arrives with the whole forward path already in mind.

2. Following a Posted Write

The path is Chapter 9.6 §3's, now with the transaction named and one thing deliberately absent.

Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
host store to an assigned address
   → Requester's Transaction Layer constructs a Memory Write Request
   → the Request, carrying its payload, traverses the fabric
   → the Completer accepts it
   → the payload is applied at the resource offset

And that is the end of the diagram. Nothing returns to the Requester at the Transaction Layer. There is no Completion, so there is nothing to correlate, nothing to time out at the Sequence level, and no entry in Chapter 10.2 §10's table.

A posted Memory Write. A local producer offers a write with its address, byte enables and payload to the posted queue. The queue accepts it, at which point the producer may release its buffer. The queue offers a Memory Write Request carrying the payload to the fabric, which delivers it to the Completer's Transaction Layer, which applies the payload at the target resource offset. No Completion returns to the Requester.A posted Memory Write, forward path onlyLocal producerPosted queueFabricCompleter TLTarget resourcewrite offered -addr, BE, payloadaccepted - producermay releaseMemory Write Request+ payloaddelivered to theCompleterpayload applied atoffset
Figure 1 — a posted write. The producer's ownership ends at the handoff to the outbound queue; the transaction then travels forward and is applied. No Completion returns, so the figure ends where the Requester's direct knowledge ends — which is the point, not an omission.

The dashed message going back to the producer is not a Completion. It is a local handshake — the queue telling its own producer that ownership has transferred. It never leaves the device. Conflating that acknowledgement with a PCIe Completion is one of the terminology errors this chapter exists to prevent, and §13 names it.

3. What the Requester Therefore Cannot Know

This is the section that separates a working mental model from a dangerous one.

After the transaction leaves, the Requester knows exactly one thing: it left. Everything else in the list below is not established by the absence of a Completion, because absence establishes nothing.

Tempting conclusionWhy it does not follow
"The write succeeded"No transaction reported success; none was required to
"The payload has been applied at the destination"The Requester has no evidence of the destination's state
"Every downstream stage accepted it"Forward acceptance at one boundary says nothing about the next
"No error can have occurred"Errors remain possible; what changed is the Requester's ability to attribute one to this Request
"Software has synchronous proof of the write"There is nothing for software to poll or wait on at this level

The normative statement that makes this precise is the one in §1: the Completion Status field "is the only method of error reporting in PCI Express which enables the Requestor to associate an error with a specific Request."

4. Posted Does Not Mean Unbounded

The second dangerous simplification is that a transaction requiring no answer requires no resources.

Flow Control distinguishes three types of TLP, and posted Requests are one of them. Of the six credit types tracked per Virtual Channel, two — Posted Request Headers and Posted Request Data payload — exist specifically for them. A posted Request consumes flow-control resources on its way out exactly as a non-posted one does.

What that means operationally:

  • A transmitter cannot send a posted Request whenever it likes. It sends when the receiver has advertised room, and not before.
  • A receiver that stops making room stops posted traffic, and the back-pressure propagates to the queue, then to the producer.
  • So the throughput limit on posted traffic is a forward-path resource limit, not a latency limit — which is the whole of §13.

Module 16 owns Flow Control: the credit unit, how credits are advertised and returned, how a transmitter accounts for them, and what happens when a pool is exhausted. This chapter states only the fact that posted traffic participates, because a design or a mental model built on "posted means unlimited send" is wrong before it starts.

5. Where Ownership Actually Ends

The design question a posted transaction poses is not "what comes back" — nothing does — but "when may the producer stop caring."

The chain of custody, stage by stage:

Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
the local producer owns the address, byte enables and payload
   → the outbound queue accepts them        ← ownership transfers HERE
   → the queue owns them until the Transaction Layer takes them
   → the outbound path owns them until the lower layers take them
   → ... and so on down

At each boundary a handshake transfers ownership, and before that handshake the upstream side must hold everything stable. That is Chapter 9.6 §10's discipline, and it is the whole content of "posted ownership ends on the forward path."

Posted ownership ends on forward-path acceptance. Non-posted ownership does not — it ends when a Completion resolves the Sequence, which is Chapter 10.4.

6. Microarchitecture — A Forward-Only Path

The comparison with Chapter 10.2 is the fastest way to see what a posted path is:

StructureNon-posted needs itPosted needs it
Outbound buffering for the descriptor and payloadyesyes
Flow-control accounting on the way outyesyes
A correlation keyyesno
An outstanding-request table entryyesno
A return path for the answeryesno
Local result deliveryyesno
A timeout at the Sequence levelyesno

Four of the seven rows disappear, and they are all on the return side. The two that remain are both forward-path resources — which is exactly why §13's performance discussion is about buffers and credits rather than about latency.

The block that remains is therefore a queue, not a tracker: it accepts work from a producer, holds it while the outbound path is busy, and hands it on. That is §11.

7. RTL — The Posted Write Queue

Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// SYNTHESIZABLE. Outbound staging for posted writes. Descriptor and payload
// are stored TOGETHER and move TOGETHER, so ownership transfers exactly once.
// "Memory Writes are posted" is NORMATIVE; this structure is illustrative.
module posted_write_queue #(
  parameter int DEPTH  = 4,
  parameter int ADDR_W = 64,
  parameter int DATA_W = 32,
  // Derived. Never zero-width, including at DEPTH == 1.
  parameter int PTR_W  = (DEPTH <= 1) ? 1 : $clog2(DEPTH),
  parameter int BE_W   = DATA_W / 8
) (
  input  logic               clk,
  input  logic               rst_n,
 
  // ---- Local producer --------------------------------------------------
  input  logic               wr_valid,
  output logic               wr_ready,
  input  logic [ADDR_W-1:0]  wr_addr,
  input  logic [DATA_W-1:0]  wr_data,
  input  logic [BE_W-1:0]    wr_be,
 
  // ---- Outbound Transaction Layer --------------------------------------
  output logic               tx_valid,
  input  logic               tx_ready,
  output logic [ADDR_W-1:0]  tx_addr,
  output logic [DATA_W-1:0]  tx_data,
  output logic [BE_W-1:0]    tx_be,
  // Constant. A posted Request allocates no Completion-tracking state, and
  // this output is what a downstream launcher uses to know that.
  output logic               tx_needs_completion,
 
  // ---- Status ----------------------------------------------------------
  output logic               q_full,
  output logic               q_empty,
  output logic [PTR_W:0]     q_level      // 0..DEPTH, so PTR_W+1 bits
);
 
  generate
    if (DEPTH  < 1) $error("DEPTH must be at least 1");
    if (DATA_W % 8) $error("DATA_W must be a whole number of bytes");
  endgenerate
 
  // Storage. Descriptor and payload in one array, indexed together — the
  // structural expression of section 5's atomic-ownership rule.
  logic [ADDR_W-1:0] addr_q [DEPTH];
  logic [DATA_W-1:0] data_q [DEPTH];
  logic [BE_W-1:0]   be_q   [DEPTH];
 
  logic [PTR_W-1:0]  wr_ptr_q, rd_ptr_q;
  logic [PTR_W:0]    level_q;
 
  // A separate level counter rather than the pointer-MSB trick, because that
  // trick is only correct for power-of-two depths. This is exact for any
  // DEPTH, and it keeps full and empty unambiguously distinct.
  localparam logic [PTR_W:0] DEPTH_C = DEPTH[PTR_W:0];
 
  assign q_level = level_q;
  assign q_full  = (level_q == DEPTH_C);
  assign q_empty = (level_q == '0);
 
  // wr_ready depends on QUEUE STATE only — never on wr_valid, and never on
  // tx_ready. A producer is admitted because there is room, full stop.
  assign wr_ready = !q_full;
  // tx_valid depends on QUEUE STATE only — never on tx_ready. Data exists or
  // it does not.
  assign tx_valid = !q_empty;
 
  assign tx_addr = addr_q[rd_ptr_q];
  assign tx_data = data_q[rd_ptr_q];
  assign tx_be   = be_q[rd_ptr_q];
 
  // NORMATIVE: a Memory Write is posted, so nothing downstream should
  // allocate Completion-tracking state for it. Tied off rather than left to
  // a comment, so the property is carried on a wire.
  assign tx_needs_completion = 1'b0;
 
  wire push = wr_valid && wr_ready;
  wire pop  = tx_valid && tx_ready;
 
  // Explicit wrap, so a non-power-of-two DEPTH is handled correctly. The
  // pointer-increment-and-truncate idiom is only right when DEPTH is a power
  // of two, and it fails silently otherwise.
  function automatic logic [PTR_W-1:0] nxt(input logic [PTR_W-1:0] p);
    return (p == PTR_W'(DEPTH-1)) ? '0 : (p + 1'b1);
  endfunction
 
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wr_ptr_q <= '0;
      rd_ptr_q <= '0;
      level_q  <= '0;
    end else begin
      if (push) begin
        // Descriptor AND payload captured in the same cycle. After this the
        // producer owns neither, which is exactly what makes releasing its
        // buffer safe (section 5).
        addr_q[wr_ptr_q] <= wr_addr;
        data_q[wr_ptr_q] <= wr_data;
        be_q[wr_ptr_q]   <= wr_be;
        wr_ptr_q         <= nxt(wr_ptr_q);
      end
      if (pop) rd_ptr_q <= nxt(rd_ptr_q);
 
      // Push and pop in the same cycle leave the level unchanged, which is
      // why this is a case rather than two independent increments.
      case ({push, pop})
        2'b10:   level_q <= level_q + 1'b1;
        2'b01:   level_q <= level_q - 1'b1;
        default: level_q <= level_q;
      endcase
    end
  end
 
endmodule

Classification: synthesizable.

Semantics — every dimension:

DimensionBehaviour
Resetpointers and level cleared; empty, not full
wr_readyqueue state only — never wr_valid, never tx_ready
tx_validqueue state only — never tx_ready
Payload stabilitythe read port is mem[rd_ptr_q] and rd_ptr_q advances only on pop, so everything offered is stable while stalled
Ownership transferat the push handshake, atomically for descriptor and payload
Push and pop in one cyclesupported; level unchanged, both pointers advance
Full and emptydistinct by construction — the level counter, not a pointer trick
Non-power-of-two DEPTHcorrect — explicit wrap in nxt()
DEPTH = 1legal; PTR_W forced to 1, nxt() returns 0, no zero-width vector
Completion trackingnone allocatedtx_needs_completion is tied low
Byte enablescarried with the payload and delivered unchanged

Trace it for one write. The producer asserts wr_valid with an address, byte enables and data. If the queue has room, wr_ready is high and the handshake occurs: all three fields are captured, wr_ptr advances, level rises. From the next cycle the producer's buffer is free. Later, when the outbound path asserts tx_ready, tx_valid is already high, the entry is handed over, rd_ptr advances and level falls.

Trace it under stall. tx_ready low: tx_valid stays high, the read port keeps pointing at the same entry, and every offered field is bit-identical cycle after cycle. If the producer keeps pushing, level rises until q_full, at which point wr_ready falls and the back-pressure reaches the producer. Nothing is dropped at any point — the queue either has room or refuses admission.

What it teaches — four things:

  1. Descriptor and payload are one object. Captured together, indexed together, handed over together. Splitting them creates two ownership questions where there was one, and §14's third scenario is what happens when the answers disagree.
  2. Neither handshake signal depends on the other side's. wr_ready is about space; tx_valid is about content. That is the discipline stated as two one-line assignments.
  3. The level counter is not a stylistic choice. It makes full and empty distinct without sacrificing an entry and it is correct for any depth. The pointer-MSB alternative is smaller and silently wrong for DEPTH = 3.
  4. tx_needs_completion is a wire, not a comment. The posted property travels with the transaction, so a downstream launcher cannot forget it. §8 makes that classification a real function.

Deliberately simplified: one data beat per write rather than a multi-dword payload; a single write port and a single read port; no flow-control accounting (a real transmitter also needs credit before it may send — Module 16); no ordering awareness (Chapter 13.4); no error path.

Production implication: a real outbound posted path carries a payload stream sized by the maximum payload the Link permits, checks flow-control credit before offering a transaction, obeys the ordering rules relative to other traffic classes, and constructs the actual Memory Write TLP at the Data Link boundary.

8. RTL — Classifying What Needs Tracking

The single most consequential fact about a transaction, from the outbound path's point of view, is whether anything will come back for it. That deserves to be computed once, in one place.

Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// CONCEPTUAL / COMPILE-TIME. Classifies an INTERNAL transaction kind.
// The classification itself is NORMATIVE (section 1). The enum encoding is
// arbitrary internal metadata and is NOT the Fmt/Type field — Module 11 owns
// that. This extends Chapter 10.1's descriptor with the I/O kinds the
// classification needs, and widens the enum accordingly.
package posted_class_pkg;
 
  typedef enum logic [3:0] {
    TXN_MEM_RD = 4'd0,
    TXN_MEM_WR = 4'd1,
    TXN_IO_RD  = 4'd2,
    TXN_IO_WR  = 4'd3,
    TXN_CFG_RD = 4'd4,
    TXN_CFG_WR = 4'd5,
    TXN_MSG    = 4'd6,
    TXN_CPL    = 4'd7
    // Encodings 8..15 intentionally unassigned, so "a kind this model does
    // not represent" stays reachable and testable.
  } txn_kind_e;
 
  typedef struct packed {
    logic supported;         // this model knows what to do with the kind
    logic needs_completion;  // a Completion will return for it
  } txn_class_t;
 
  function automatic txn_class_t classify(input txn_kind_e k);
    txn_class_t c;
    case (k)
      // POSTED — Messages and Memory Writes (normative).
      TXN_MEM_WR,
      TXN_MSG:    c = '{supported: 1'b1, needs_completion: 1'b0};
 
      // NON-POSTED — all Reads, I/O, and Configuration Writes (normative).
      // Note that I/O Writes and Configuration Writes are here, NOT with the
      // posted group. "All writes are posted" is wrong in two cases.
      TXN_MEM_RD,
      TXN_IO_RD,
      TXN_IO_WR,
      TXN_CFG_RD,
      TXN_CFG_WR: c = '{supported: 1'b1, needs_completion: 1'b1};
 
      // A Completion is not a Request and must not be launched as one.
      TXN_CPL:    c = '{supported: 1'b0, needs_completion: 1'b0};
 
      // An unrecognised kind is NOT LAUNCHED. Both defaults are wrong:
      // guessing posted loses an operation that needed tracking, and
      // guessing non-posted allocates state nothing will ever free. The only
      // safe answer to "I do not know what this is" is to refuse it.
      default:    c = '{supported: 1'b0, needs_completion: 1'b1};
    endcase
    return c;
  endfunction
 
endpackage

Classification: conceptual / compile-time.

What it teaches — three things:

  1. The classification is a property of the transaction kind, not of the device. A Memory Write is posted whoever sends it; a Configuration Write is non-posted whoever sends it. That is why this is a pure function.
  2. "All writes are posted" is a two-case error. I/O Writes and Configuration Writes require Completion. The case groups them with the reads deliberately and comments on it, because the grouping is the surprising part.
  3. The unknown case refuses rather than guesses. Defaulting either way is a silent fault — one loses operations, the other leaks tracking state. Returning supported = 0 pushes the decision to a place where it can be reported.

Deliberately simplified: kinds only, with no sub-classification; no attributes; no address-space qualifier beyond the kind.

9. Assertions

Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// SVA over posted_write_queue and posted_class_pkg. Implementation
// invariants for THIS design plus the normative classification it carries —
// not claims about any PCIe field. Every property refers to explicit RTL.
 
// ENVIRONMENT ASSUMPTIONS. The producer owes valid-stability and payload
// stability; the liveness property below additionally needs downstream
// fairness, and neither can be proved from inside this module.
assume property (@(posedge clk) disable iff (!rst_n)
  (wr_valid && !wr_ready) |=> wr_valid);
assume property (@(posedge clk) disable iff (!rst_n)
  (wr_valid && !wr_ready) |=> ($stable(wr_addr) && $stable(wr_data)
                               && $stable(wr_be)));
// FAIRNESS: while the queue is non-empty, the outbound path becomes ready
// often enough for progress. Required for P8 and P8b, and stated rather than
// assumed silently — if downstream may stall indefinitely, an entry
// legitimately sits forever and no eventual-transfer property is provable.
assume property (@(posedge clk) disable iff (!rst_n)
  tx_valid |-> s_eventually (tx_ready));
 
// STABILITY — P1: an offered transaction is stable while stalled. The core
// handshake obligation on the outbound side.
property p_tx_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && !tx_ready) |=> (tx_valid && $stable(tx_addr)
                               && $stable(tx_data) && $stable(tx_be));
endproperty
a_tx_stable : assert property (p_tx_stable_under_stall);
 
// STABILITY — P2: tx_valid is never withdrawn except by a handoff. Catches a
// design that deasserts valid because some enable or availability changed,
// which loses a transaction the downstream had not yet taken.
property p_offer_not_withdrawn;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && !tx_ready) |=> tx_valid;
endproperty
a_no_withdraw : assert property (p_offer_not_withdrawn);
 
// CONSERVATION — P3: the level is exactly pushes minus pops. The invariant
// "accepted equals queued plus delivered", checkable in one line.
property p_level_conserved;
  @(posedge clk) disable iff (!rst_n)
  level_q == $past(level_q) + $past(push) - $past(pop);
endproperty
a_level_exact : assert property (p_level_conserved);
 
// CONSERVATION — P4: the level never leaves its legal range. A level that
// wrapped would report space that does not exist and overwrite a live entry.
property p_level_in_range;
  @(posedge clk) disable iff (!rst_n)
  level_q <= DEPTH_C;
endproperty
a_level_bounded : assert property (p_level_in_range);
 
// LEGALITY — P5: a full queue admits nothing. The back-pressure that makes
// "no write is ever dropped" true.
property p_full_blocks_push;
  @(posedge clk) disable iff (!rst_n)
  q_full |-> !push;
endproperty
a_full_blocks : assert property (p_full_blocks_push);
 
// LEGALITY — P6: an empty queue offers nothing. Catches a tx_valid that
// leaked a dependence on something other than occupancy, which would emit a
// transaction built from uninitialised storage.
property p_empty_offers_nothing;
  @(posedge clk) disable iff (!rst_n)
  q_empty |-> !tx_valid;
endproperty
a_empty_silent : assert property (p_empty_offers_nothing);
 
// CONSERVATION — P7: an entry is handed over once. Read and write pointers
// advance only on their own handshakes, so nothing is sent twice.
property p_no_duplicate_send;
  @(posedge clk) disable iff (!rst_n)
  !pop |=> $stable(rd_ptr_q);
endproperty
a_no_dup : assert property (p_no_duplicate_send);
 
// LIVENESS — P8: QUEUE-LEVEL progress only. A push is eventually followed by
// SOME pop, so the queue does not wedge. DEPENDS ON THE FAIRNESS ASSUMPTION.
//
// READ THE SCOPE EXACTLY. This says a pop happens; it does NOT say that the
// item pushed here is the item popped. A design that dropped one entry and
// kept draining the rest satisfies it. Per-item progress needs identity, and
// identity does not exist in the synthesizable interface — see P8b.
property p_queue_makes_progress;
  @(posedge clk) disable iff (!rst_n)
  push |-> s_eventually (pop);
endproperty
a_queue_progresses : assert property (p_queue_makes_progress);
 
// ---------------------------------------------------------------------
// VERIFICATION-ONLY instrumentation. A shadow sequence number attached to
// each accepted write so per-item progress can be stated at all.
//
// NOT PCIe packet state, NOT part of the synthesizable posted_write_queue
// interface, and NOT derived from the DUT's pointers — a checker that used
// rd_ptr_q or wr_ptr_q as its identity would be asserting the design against
// itself.
// ---------------------------------------------------------------------
localparam int SEQ_W = 16;
logic [SEQ_W-1:0] sb_next_seq_q;      // stamped on each accepted write
logic [SEQ_W-1:0] sb_expect_seq_q;    // expected on the next downstream item
logic [SEQ_W-1:0] sb_shadow_q [DEPTH];   // parallel to the DUT's storage
logic [PTR_W-1:0] sb_wr_q, sb_rd_q;      // the checker's OWN pointers
 
always_ff @(posedge clk or negedge rst_n) begin
  if (!rst_n) begin
    sb_next_seq_q   <= '0;
    sb_expect_seq_q <= '0;
    sb_wr_q         <= '0;
    sb_rd_q         <= '0;
  end else begin
    if (push) begin
      sb_shadow_q[sb_wr_q] <= sb_next_seq_q;
      sb_next_seq_q        <= sb_next_seq_q + 1'b1;
      sb_wr_q              <= (sb_wr_q == PTR_W'(DEPTH-1)) ? '0 : sb_wr_q + 1'b1;
    end
    if (pop) begin
      sb_expect_seq_q <= sb_expect_seq_q + 1'b1;
      sb_rd_q         <= (sb_rd_q == PTR_W'(DEPTH-1)) ? '0 : sb_rd_q + 1'b1;
    end
  end
end
 
// The sequence number the checker believes is being offered right now.
wire [SEQ_W-1:0] sb_offered_seq = sb_shadow_q[sb_rd_q];
 
// LIVENESS — P8b: PER-ITEM progress. The specific item accepted in this cycle
// is eventually the specific item transferred downstream. Local variable `s`
// captures the identity at the push, and the property waits for a pop
// carrying exactly that identity.
// DEPENDS ON THE FAIRNESS ASSUMPTION ABOVE.
property p_each_item_eventually_sent;
  logic [SEQ_W-1:0] s;
  @(posedge clk) disable iff (!rst_n)
  (push, s = sb_next_seq_q) |-> s_eventually (pop && (sb_offered_seq == s));
endproperty
a_each_item_sent : assert property (p_each_item_eventually_sent);
 
// CONSERVATION — P8c: items leave in the order they were accepted, exactly
// once each. Catches a reorder or a skip that P8b's eventual form alone
// would tolerate for a while.
property p_items_in_order;
  @(posedge clk) disable iff (!rst_n)
  pop |-> (sb_offered_seq == sb_expect_seq_q);
endproperty
a_items_ordered : assert property (p_items_in_order);
 
// CLASSIFICATION — P9: a posted transaction allocates no Completion-tracking
// state. The chapter's thesis, carried on a wire and asserted rather than
// left to a comment.
property p_posted_needs_no_completion;
  @(posedge clk) disable iff (!rst_n)
  tx_valid |-> !tx_needs_completion;
endproperty
a_posted_untracked : assert property (p_posted_needs_no_completion);
 
// CLASSIFICATION — P10: the classification is stable for the whole time a
// transaction is owned. A kind that changed under a stalled offer would let
// a transaction be launched under one contract and tracked under another.
property p_class_stable_while_offered;
  @(posedge clk) disable iff (!rst_n)
  (tx_valid && !tx_ready) |=> $stable(tx_needs_completion);
endproperty
a_class_stable : assert property (p_class_stable_while_offered);
 
// RESET — P11: reset empties the queue. LOCAL BLOCK RESET behaviour only;
// real Function and Link reset semantics are owned by later chapters, and a
// local reset does not un-send a transaction already on the fabric.
property p_reset_empties;
  @(posedge clk) !rst_n |=> (q_empty && !tx_valid);
endproperty
a_reset_empty : assert property (p_reset_empties);
 
// SAFETY — P12: no interface output is ever unknown.
property p_outputs_never_unknown;
  @(posedge clk) disable iff (!rst_n)
  !$isunknown({wr_ready, tx_valid, q_full, q_empty, tx_needs_completion});
endproperty
a_no_x : assert property (p_outputs_never_unknown);

P3 is the conservation property and it is worth more than it looks. "Accepted equals queued plus delivered" is the whole correctness argument for a queue, and stating it against $past values makes it checkable without a shadow model. A design that dropped a write under some corner — a simultaneous push and pop mishandled, a wrap miscomputed — breaks it on the cycle it happens rather than eventually, somewhere else.

P8 and P8b are two different claims, and the difference is worth more than either property alone.

P8 is queue-level progress: a push is eventually followed by some pop. It proves the queue does not wedge — and nothing about the item that was pushed. A design that quietly dropped one entry while continuing to drain the rest satisfies it completely. Written as the only liveness property and described as "this write is eventually sent," it would be overclaiming: the property is strictly weaker than the sentence.

P8b is per-item progress, and it needs something the synthesizable interface does not have — an identity for each item. So the identity is added in verification only: a shadow sequence number stamped at each accepted write, with the checker keeping its own pointers rather than reading rd_ptr_q. That independence is not a style preference; a checker that used the design's pointer to decide which item is being offered would be asserting the design against itself and could not fail on a pointer bug.

P8c closes the last gap. Eventual delivery permits arbitrary reordering in the interval; P8c requires items to leave in acceptance order, exactly once each, which is what a FIFO actually promises.

Both liveness properties carry the same assumption in plain sight. Without downstream fairness, "eventually sent" is simply false — a downstream that stalls forever holds the entry forever, and no property of this module can change that. Asserting liveness without stating the assumption, or describing a queue-level property as if it were per-item, are the same class of error: claiming a guarantee stronger than the code and the environment together provide.

P9 and P10 together are the chapter's thesis. P9 says a posted transaction never asks for Completion tracking; P10 says that classification cannot change while the transaction is being offered. The second is the one that would be omitted, and it matters because a design that recomputed the class per cycle from a source that changed under stall could launch a transaction as posted and have a downstream launcher track it — or the reverse, which leaks an outstanding entry forever.

P2 looks like a restatement of P1 and is not. P1 constrains the payload under stall; P2 constrains the offer itself. A design that withdrew tx_valid because an enable dropped, or because a classification input changed, would satisfy P1 vacuously — there is no stall to hold through if the offer disappears — and lose the transaction.

10. Verification

Monitors observe: both handshakes with all payload fields, the level and full/empty status, and tx_needs_completion.

The scoreboard counts and matches. It records each accepted write with a testbench-assigned sequence number and its full payload, and matches each downstream transfer against the oldest unmatched record. It must not read the design's pointers or level as its reference — those are what is under test. The conservation check is accepted == delivered + level, computed from the scoreboard's own counters and compared against q_level.

Basic operation

  • One write, immediately drained. Verify the payload arrives unchanged and the level returns to zero.
  • Continuous writes with tx_ready high. Verify one transfer per cycle sustained with no dead cycles and no loss.
  • A write while the queue already holds entries. Verify FIFO order is preserved.
  • Every byte-enable pattern, including all-zero and all-ones. Verify each is delivered unchanged — a queue that dropped byte enables would turn a partial write into a full-width one, which is silent data corruption at exactly the granularity software chose deliberately.
  • Distinctive payload patterns — walking ones, walking zeros, alternating — so a stuck or crossed bit in the storage array is visible.

Back-pressure and capacity

  • tx_ready held low for many cycles. Verify tx_valid stays high, every offered field is stable (P1, P2), and the level rises as the producer pushes.
  • Fill to exactly full. Verify q_full, wr_ready low, and that the entry count equals DEPTH.
  • Attempt to push while full. Verify nothing is accepted, nothing is overwritten, and the level does not move (P5).
  • One below full, then a simultaneous push and pop. Verify the level is unchanged and both entries are correct — the same-cycle case that a naive two-counter implementation gets wrong.
  • Drain from full to empty. Verify every entry emerges exactly once, in order, with its payload intact.
  • tx_ready toggling every other cycle with the producer pushing continuously. Verify the level oscillates and nothing is lost or duplicated (P3, P7).

Negative tests

  • Downstream never ready. Verify the queue fills, back-pressure reaches the producer, and nothing is dropped. Then release tx_ready and verify every write emerges. Run both liveness properties with the fairness assumption disabled and confirm they correctly fail — a liveness check that passes with no fairness assumption is not checking anything.
  • A deliberately dropped entry. Force the design to skip one item (a mutant, or a forced pointer advance) and confirm that P8 still passes while P8b and P8c fail. This is the test that demonstrates why queue-level progress is not per-item progress, and it is the reason the shadow sequence numbers exist.
  • Producer withdrawing wr_valid before its handshake. A deliberate assumption violation. Verify the assumption fires, and keep it outside the functional regression's pass/fail accounting.
  • Producer changing payload while stalled. Another deliberate violation, and the one that models §5's overwrite hazard. Verify the assumption fires.
  • Reset with entries queued. Verify the queue empties, tx_valid drops (P11), and nothing is emitted afterwards from pre-reset state.

Parameter corners

  • DEPTH = 1. Verify PTR_W is 1, no zero-width vector exists, nxt() returns 0, and full and empty are still distinct.
  • DEPTH = 3 — non-power-of-two. Verify the wrap is correct and the level never exceeds 3. A pointer-MSB implementation fails here and passes every power-of-two test, which is why this case is mandatory rather than optional.
  • DEPTH large enough that the level needs its extra bit. Verify q_level reaches DEPTH without wrapping (P4).

Coverage should include: the queue at empty, one, one-below-full and full; simultaneous push and pop at every occupancy; all byte-enable patterns; tx_ready continuously high, continuously low and randomly toggled; and reset from empty, partially full and full.

11. Why No Completion Is a Throughput Property

Posted semantics are usually explained as "faster," which is true often enough to be misleading.

What is genuinely removed. A posted Request consumes no correlation state and no return-path bandwidth, and the Requester never has to wait for anything before launching the next one. Sustained posted throughput is therefore not limited by round-trip latency — which is the real content of the claim, and it is a significant claim.

What is not removed. Every limit on the forward path still applies:

LimitWhy it still binds
Outbound bufferingthe queue of §7 has a depth, and a full queue back-pressures the producer
Flow-control resourcesa posted Request consumes Posted Request Header and Data credits (§4)
Link capacitythe bytes still have to cross
Receiver readinessa Completer that stops making room stops the traffic
Orderingposted traffic's relationship to other classes constrains what may be reordered — Chapter 13.4
The destination itselfa resource that cannot absorb writes at line rate is the limit, wherever it sits

12. Debugging

Symptom: host writes appear to succeed locally, but the Endpoint's state never changes

"Appear to succeed" means the store retired and nothing reported an error — which, for a posted write, is exactly what a completely failed operation also looks like. There is no local evidence either way, so the only method is to walk forward.

  1. Was the write accepted by the local producer's interface? wr_valid && wr_ready. If not, the producer is stalled and nothing was ever queued — the investigation is upstream of PCIe entirely.
  2. Did an entry appear in the outbound queue? q_level rising. A push handshake with no level change is §9's P3 failing.
  3. Was a transaction offered and taken downstream? tx_valid && tx_ready. A queue holding entries with tx_ready permanently low is §12's second scenario, not this one.
  4. Did the transaction cross the fabric? Every parent routing window must forward the address (Chapter 9.5 §9). This is the rung where a perfectly correct Requester and a perfectly correct Completer are separated by a bridge that was never programmed.
  5. Did the Completer receive it? If instrumentation exists at the far side, this is the single most valuable observation in the ladder, because it partitions the whole path in one measurement.
  6. Did the Completer's resource decode claim the address? Chapter 9.6 §14's rungs — Memory Space Enable, BAR value, window membership, the miss output.
  7. Did the payload reach the target at the right offset? Chapter 9.6 §5's arithmetic, and its third debugging scenario if the offset is wrong.
  8. Did the side effect occur? Only now is the resource itself a candidate.

What makes this ladder feel different from a non-posted one. There is no point at which you can ask the Requester what happened. Every rung is an observation of the transaction in transit, and if you have no visibility at a given hop, that hop stays a suspect. That is the practical cost of posted semantics, and it is why §3 insists the trade is about attribution rather than about reliability.

One shortcut worth knowing. If the same Endpoint responds correctly to a read of a neighbouring address, rungs 4 through 6 are proven — the routing works, the window is programmed, the space is enabled — and the investigation collapses to rungs 7 and 8. A read is a cheap probe for a posted write's path, precisely because it comes back.

Symptom: the posted queue fills and stays full

A full queue is a downstream problem until proven otherwise, because the queue only fills when it cannot drain.

  1. Is tx_ready ever asserting? If never, the outbound path is blocked and the queue is a victim. In a real design the most common cause is flow-control credit exhaustion — the transmitter has no room advertised to it (Module 16) — which is a receiver-side condition observed at the transmitter.
  2. Is pop occurring when tx_ready is high? If tx_ready asserts and nothing is taken, tx_valid is wrong — check P6 and the empty condition.
  3. Is the level decrementing on pop? A level that only ever rises is P3's failure and a genuine leak.
  4. Is the producer simply faster than the drain? A queue at capacity with entries flowing steadily is not a bug — it is the design at its throughput limit, which is §11's subject rather than a defect.

The distinguishing observation is the same one Chapter 10.2 §15 uses: watch the level over time. Monotonically rising to full and flat with no pops is a blockage or a leak. Oscillating near full with steady pops is saturation. The two look identical at the producer interface and demand opposite responses.

Symptom: the same write appears to happen twice

Take the "retry" hypothesis off the table first, because it is the most popular answer and usually the wrong one. The Data Link Layer's retransmission mechanism operates below the Transaction Layer and is designed to be invisible above it; blaming it without evidence sends the investigation to the wrong layer entirely (Modules 14–15).

The local candidates, all of which are ownership bugs:

  1. The read pointer did not advance on handoff. The same entry is offered again and taken again. P7 catches it; the signature is that the duplicate is bit-identical and immediately adjacent.
  2. tx_valid remained asserted after the handshake with no new entry. A valid that is not derived from occupancy re-offers stale storage. P6 catches it.
  3. The producer re-offered the same work. Its own bookkeeping thinks the write was not accepted — often because it sampled wr_ready without qualifying on wr_valid, or misread a stalled cycle as a rejection.
  4. The producer's payload buffer was reused while an offer was outstanding. This produces a duplicate address with different data rather than a true duplicate, which is a useful distinguishing detail.

The observation that classifies it in one step: compare the two transactions field by field. Bit-identical and back-to-back points at the queue (1 or 2). Same address with different payload points at the producer's buffer (4). Separated in time with an intervening gap points at the producer's bookkeeping (3).

13. Common Misconceptions

  • "Posted means the packet has already been executed remotely." It means no Completion is required. The Requester has no evidence about the destination's state at any point.
  • "Posted means no error can occur." Errors remain possible. What is removed is the Requester's ability to associate an error with this specific Request — the Completion Status field is the only mechanism that provides that, and posted Requests have none (§3).
  • "Posted means no buffering is needed." The transaction still occupies outbound storage until the next stage takes it. §7's queue exists for exactly that.
  • "Posted means no flow-control credits." Posted Requests consume Posted Request Header and Data resources like any other class (§4). "No Completion" and "no limit on sending" are unrelated claims.
  • "The producer may discard the payload as soon as it offers the write." Ownership transfers at the handshake, not at the offer. Releasing early sends whatever the buffer holds at read-out time — a well-formed transaction carrying wrong data (§5).
  • "A posted transaction has no header." It is an ordinary TLP with everything a TLP has. What it lacks is a returning Completion.
  • "Posted means an asynchronous software API." It is a protocol-level property. How a driver or an operating system exposes it is a software design choice at a different level entirely.
  • "Every write is posted." Memory Writes are posted. I/O Writes and Configuration Writes are non-posted and require Completion (§1). This is the single most common classification error.
  • "A posted write is never acknowledged anywhere in PCIe." The Data Link Layer acknowledges packets Link-locally, on every hop, for every TLP. That is a different mechanism at a different layer with a different scope, and it says nothing about the operation's outcome (§4).
  • "Without a Completion there is no way to debug a failure." There is — it is just a different method. §12's forward-path ladder is that method, and knowing to use it is most of the work.

14. Understanding Check

15. What's Next

This chapter took the zero in "zero or more Completions": which Requests are posted, what the absence of a Completion removes and — more importantly — what it does not, and where a producer's ownership actually ends.

Chapter 10.4 — Non-Posted Transactions takes the one or more. It builds the full request-lifetime controller: allocating correlation state before launch, holding it while the operation is outstanding, resolving it against a returning Completion, and freeing it exactly once — plus the correlation-ID allocation that makes reuse safe, why a timeout must never imply an automatic retry, and how outstanding depth becomes a throughput ceiling.

Chapter 10.5 then traces one complete request-to-Completion exchange across the fabric with every boundary in this module already in place.

The idea to carry forward: posted ownership ends going out; non-posted ownership ends coming back — and every structural difference between the two follows from that one sentence.