PCIe · Module 23
Design Patterns — One Law, Twelve Shapes
Across four modules the same defects kept reappearing in different subsystems. Each was an ownership failure, and each has a small piece of RTL that makes it impossible. This is the catalogue, with the measurements that earned each entry.
Something has been repeating.
A switch arbiter that re-selects mid-packet (21.2 §11). A TLP generator whose header follows the live request (23.4 §4). A packetizer that resizes a stalled packet (22.4 §8). A credit engine where two producers spend the same credit (22.3 §9). Four subsystems, four teams' worth of code — and one defect.
This chapter is the catalogue. Not syntax, not a utility library: twelve shapes of one law, each with the measurement that earned it a place.
1. Sources, Scope, and What a Pattern Chapter Owes You
2. One Law, Twelve Shapes
The law is short enough to hold in your head during a review:
Exactly one owner, at every instant. Ownership transfers at exactly one defined event. Nothing the owner holds changes between transfers.
Each clause fails in a characteristic way, and each failure has a characteristic symptom:
| Clause violated | Symptom you will see |
|---|---|
| two owners | double-spend, duplicated packet, one resource used twice |
| no owner | a leak; a resource that never comes back |
| ill-defined transfer event | works until something stalls |
| the held thing changed | correct metadata, wrong data — or the reverse |
The fourth row is worth pausing on, because it is the one that reaches silicon. A packet with a correct header and the wrong payload passes every structural check downstream. It is not malformed; it is a well-formed lie, and it can only be caught where ownership was lost.
And one empirical observation across all four modules: the naive form always fails in the flattering direction and only under load. Counting on valid overstates throughput. A live header is correct until something stalls. A shared counter is right in aggregate. That is why these defects survive review and bring-up, and why the patterns are worth memorizing rather than rediscovering.
3. Ownership Patterns
4. Resource Patterns
5. Correlation Patterns
6. Arithmetic Patterns
7. Evidence Patterns
8. Where the Patterns Sit
Four things to read out of the figure.
The snapshot sits between the mutable world and everything else. Nothing downstream reads mutable config directly — that single edge is what patterns 1 exists to enforce, and cutting it is the 15.3% and 68.6% results.
There is exactly one edge back into the pool. Every terminal path converges on single release path (pattern 5), which is what turns "did we free everything?" from an audit into a property.
The context and the pipeline are on the return path, because correlation is only needed once a response can arrive out of context (patterns 7, 8).
And the two observers hang off the accounting, not off the datapath — patterns 6 and 12 watch and never drive, which is the last property in §9.
9. RTL — The Pattern Library
// COMPILE-TIME. Guarded width helpers used by every block below.
// $clog2(1) is 0, which yields a zero-width vector -- illegal, and the
// most common way a parameterized block breaks at DEPTH = 1.
package pattern_pkg;
function automatic int unsigned idx_w(input int unsigned depth);
return (depth <= 1) ? 1 : $clog2(depth);
endfunction
function automatic int unsigned cnt_w(input int unsigned maxval);
return (maxval <= 1) ? 1 : $clog2(maxval + 1);
endfunction
endpackage// SYNTHESIZABLE. PATTERN 1 -- immutable snapshot.
// Captures a whole structure at one boundary and holds it for the life of
// the ownership. `stale` is exposed so the divergence is visible rather
// than silent -- an invisible divergence is what makes the bug survive.
module snapshot_holder #(parameter int W = 32) (
input logic clk,
input logic rst_n,
input logic [W-1:0] live,
input logic take, // an ownership boundary occurred
input logic owned, // something currently holds the value
output logic [W-1:0] effective,
output logic stale // live differs from effective while owned
);
logic [W-1:0] q;
assign effective = q;
assign stale = owned && (live != q);
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) q <= '0;
else if (take && !owned) q <= live; // ONLY at the boundary
end
endmodule// SYNTHESIZABLE. PATTERN 2 -- hold until handshake.
// The canonical valid/ready holding register. `valid` never depends on
// `ready`; the payload is stable while stalled; ownership moves once.
module hold_register #(parameter int W = 32) (
input logic clk,
input logic rst_n,
input logic in_valid,
output logic in_ready,
input logic [W-1:0] in_data,
output logic out_valid,
input logic out_ready,
output logic [W-1:0] out_data
);
logic [W-1:0] d_q;
logic v_q;
assign out_valid = v_q;
assign out_data = d_q;
// Accept when empty, or when the held item is leaving this cycle.
assign in_ready = !v_q || out_ready;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin v_q <= 1'b0; d_q <= '0; end
else begin
if (in_valid && in_ready) begin d_q <= in_data; v_q <= 1'b1; end
else if (out_valid && out_ready) v_q <= 1'b0;
// Under stall NEITHER branch runs, so d_q is stable by construction.
end
end
endmoduleimport pattern_pkg::*;
// SYNTHESIZABLE. PATTERN 3 -- packet-lock arbitration.
// Select at SOP, hold until the EOP TRANSFERS. Re-arbitrating per cycle
// interleaved packets in 67.0% of runs (Chapter 21.2 §11).
module packet_lock_arbiter #(parameter int N = 4) (
input logic clk,
input logic rst_n,
input logic [N-1:0] req,
input logic [N-1:0] eop,
input logic out_ready,
input logic downstream_ok,
output logic out_valid,
output logic [idx_w(N)-1:0] owner,
output logic owner_valid
);
localparam int IW = idx_w(N);
logic [IW-1:0] own_q, rr_q;
logic held_q;
logic [IW-1:0] pick;
logic found;
assign owner = own_q;
assign owner_valid = held_q;
assign out_valid = held_q && req[own_q] && downstream_ok;
always_comb begin
pick = '0; found = 1'b0;
for (int k = N-1; k >= 0; k--) begin
int i = (int'(rr_q) + k) % N;
if (req[i]) begin pick = IW'(i); found = 1'b1; end
end
end
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin held_q <= 1'b0; own_q <= '0; rr_q <= '0; end
else if (!held_q) begin
if (found) begin own_q <= pick; held_q <= 1'b1; end
end else if (out_valid && out_ready && eop[own_q]) begin
// Released on the TRANSFERRED end of packet -- not on eop asserted.
held_q <= 1'b0;
rr_q <= (own_q == IW'(N-1)) ? '0 : (own_q + IW'(1));
end
end
endmoduleimport pattern_pkg::*;
// SYNTHESIZABLE. PATTERNS 4 + 5 -- reserve before issue, and one terminal
// event. A free bitmap with ONE next-state expression, so a same-cycle
// free and allocate cannot lose either write (Chapter 23.3 §7: the two
// forms diverge in 6.3% of coincidences).
module resource_allocator #(parameter int N = 8) (
input logic clk,
input logic rst_n,
input logic alloc_req,
input logic free_req,
input logic [idx_w(N)-1:0] free_idx,
output logic avail,
output logic grant,
output logic [idx_w(N)-1:0] grant_idx,
output logic [N-1:0] free_map,
output logic [cnt_w(N)-1:0] free_count,
output logic err_double_free // sticky
);
localparam int IW = idx_w(N);
logic [N-1:0] free_q;
logic e_q;
logic [IW-1:0] pick;
logic found;
assign free_map = free_q;
assign avail = |free_q;
assign grant = alloc_req && found;
assign grant_idx = pick;
assign err_double_free = e_q;
always_comb begin
free_count = '0;
for (int i = 0; i < N; i++) if (free_q[i]) free_count = free_count + 1'b1;
end
always_comb begin
pick = '0; found = 1'b0;
for (int i = N-1; i >= 0; i--) if (free_q[i]) begin pick = IW'(i); found = 1'b1; end
end
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin free_q <= {N{1'b1}}; e_q <= 1'b0; end
else begin
// Releasing something already free is a DOUBLE TERMINAL EVENT.
if (free_req && free_q[free_idx]) e_q <= 1'b1;
free_q <= (free_q | (free_req ? (N'(1) << free_idx) : '0))
& ~(grant ? (N'(1) << pick) : '0);
end
end
endmoduleimport pattern_pkg::*;
// SYNTHESIZABLE. PATTERN 7 -- per-transaction context table.
// Keyed by an identity the RESPONSE carries. Three outcomes, and it never
// defaults: an unmatched response applies to NOTHING.
module context_table #(parameter int N = 8, parameter int KEY_W = 16,
parameter int VAL_W = 32) (
input logic clk,
input logic rst_n,
input logic ins_valid,
input logic [KEY_W-1:0] ins_key,
input logic [VAL_W-1:0] ins_val,
input logic lkp_valid,
input logic [KEY_W-1:0] lkp_key,
input logic rem_valid,
output logic hit,
output logic miss,
output logic ambiguous,
output logic [VAL_W-1:0] hit_val,
output logic [idx_w(N)-1:0] hit_idx,
output logic ins_grant,
output logic err_dup_key // sticky
);
localparam int IW = idx_w(N);
logic [KEY_W-1:0] key_q [N];
logic [VAL_W-1:0] val_q [N];
logic [N-1:0] live_q;
logic e_q;
logic [N-1:0] mvec;
logic [IW-1:0] pick_free, pick_hit;
logic have_free, dup;
always_comb begin
for (int i = 0; i < N; i++) mvec[i] = live_q[i] && (key_q[i] == lkp_key);
pick_free = '0; have_free = 1'b0;
for (int i = N-1; i >= 0; i--) if (!live_q[i]) begin pick_free = IW'(i); have_free = 1'b1; end
dup = 1'b0;
for (int i = 0; i < N; i++) if (live_q[i] && (key_q[i] == ins_key)) dup = 1'b1;
pick_hit = '0;
if ($onehot(mvec)) for (int i = 0; i < N; i++) if (mvec[i]) pick_hit = IW'(i);
end
assign hit = lkp_valid && $onehot(mvec);
assign miss = lkp_valid && (mvec == '0);
assign ambiguous = lkp_valid && !$onehot0(mvec);
assign hit_idx = pick_hit;
assign hit_val = hit ? val_q[pick_hit] : '0; // meaningful only on hit
assign ins_grant = ins_valid && have_free && !dup;
assign err_dup_key = e_q;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin live_q <= '0; e_q <= 1'b0; end
else begin
if (ins_valid && dup) e_q <= 1'b1; // a live key must be UNIQUE
if (ins_grant) begin
key_q[pick_free] <= ins_key; val_q[pick_free] <= ins_val;
live_q[pick_free] <= 1'b1;
end
if (rem_valid && hit) live_q[pick_hit] <= 1'b0;
end
end
endmodule// SYNTHESIZABLE. PATTERN 8 -- metadata travels with its data.
// A one-stage lookup pipeline that carries the key alongside the read and
// checks the pairing at the far end. Without this, a synchronous table
// paired the wrong answer in 87.5% of cycles (Chapter 23.5 §12).
module keyed_pipe #(parameter int KEY_W = 16, parameter int META_W = 32,
parameter int VAL_W = 32) (
input logic clk,
input logic rst_n,
input logic s0_valid,
input logic [KEY_W-1:0] s0_key,
input logic [META_W-1:0] s0_meta,
input logic [KEY_W-1:0] ram_key_out, // the key stored WITH the value
input logic [VAL_W-1:0] ram_val_out,
input logic ram_val_live,
output logic s1_valid,
output logic [KEY_W-1:0] s1_key,
output logic [META_W-1:0] s1_meta,
output logic [VAL_W-1:0] s1_val,
output logic err_skew // sticky
);
logic v_q, e_q;
logic [KEY_W-1:0] k_q;
logic [META_W-1:0] m_q;
assign s1_valid = v_q; assign s1_key = k_q;
assign s1_meta = m_q; assign s1_val = ram_val_out;
assign err_skew = e_q;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin v_q <= 1'b0; k_q <= '0; m_q <= '0; e_q <= 1'b0; end
else begin
v_q <= s0_valid; k_q <= s0_key; m_q <= s0_meta;
// What emerged must be what was asked for.
if (v_q && ram_val_live && (ram_key_out != k_q)) e_q <= 1'b1;
end
end
endmoduleimport pattern_pkg::*;
// SYNTHESIZABLE. PATTERNS 9 + 10 -- next-state comparison and saturating
// diagnostics, in one accumulator. The threshold is evaluated on the
// NEXT value, and the counter saturates with a sticky flag rather than
// wrapping (a wrapped counter read 232 after saturating at 255).
module nextstate_accumulator #(parameter int W = 32) (
input logic clk,
input logic rst_n,
input logic add_valid,
input logic [W-1:0] add_delta,
input logic [W-1:0] threshold,
input logic clear,
output logic [W-1:0] count,
output logic reached, // asserted the SAME cycle the sum crosses
output logic saturated
);
logic [W-1:0] q;
logic sat_q, reach_q;
logic [W:0] wide;
logic [W-1:0] nxt;
assign count = q;
assign saturated = sat_q;
assign reached = reach_q;
always_comb begin
wide = {1'b0, q} + (add_valid ? {1'b0, add_delta} : '0);
nxt = wide[W] ? {W{1'b1}} : wide[W-1:0]; // SATURATE, never wrap
end
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n || clear) begin q <= '0; sat_q <= 1'b0; reach_q <= 1'b0; end
else begin
q <= nxt;
if (wide[W]) sat_q <= 1'b1;
// Compared on the NEXT value: `q == threshold` would be a cycle late,
// and with a delta greater than one it can be missed entirely.
if (nxt >= threshold) reach_q <= 1'b1;
end
end
endmoduleimport pattern_pkg::*;
// SYNTHESIZABLE. PATTERN 11 -- range-safe index.
// An out-of-range index REPORTS and has no effect. Aliasing to zero is
// how a decoder silently sends every orphan to entry 0.
module range_safe_lookup #(parameter int N = 8, parameter int W = 32) (
input logic clk,
input logic rst_n,
input logic req_valid,
input logic [idx_w(N)+2-1:0] req_idx, // deliberately WIDER than needed
input logic [W-1:0] table_in [N],
output logic rsp_valid,
output logic [W-1:0] rsp_data,
output logic err_out_of_range // sticky
);
logic e_q;
logic in_range;
assign in_range = (req_idx < (idx_w(N)+2)'(N));
assign rsp_valid = req_valid && in_range;
assign rsp_data = rsp_valid ? table_in[req_idx[idx_w(N)-1:0]] : '0;
assign err_out_of_range = e_q;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) e_q <= 1'b0;
else if (req_valid && !in_range) e_q <= 1'b1;
end
endmoduleimport pattern_pkg::*;
// SYNTHESIZABLE. PATTERNS 12 + 13 -- sticky first failure and epoch
// invalidation, together, because they answer the same question: what
// state is still trustworthy after something went wrong?
module epoch_and_first_failure #(parameter int EPOCH_W = 4, parameter int CAUSE_W = 8) (
input logic clk,
input logic rst_n,
input logic invalidate, // reset, abort, reconfigure
input logic item_valid,
input logic [EPOCH_W-1:0] item_epoch,
input logic fault,
input logic [CAUSE_W-1:0] fault_cause,
input logic debug_clear,
output logic [EPOCH_W-1:0] epoch,
output logic item_stale, // dequeued item is from a past epoch
output logic [31:0] stale_dropped,
output logic captured,
output logic [CAUSE_W-1:0] first_cause,
output logic [31:0] later_faults
);
logic [EPOCH_W-1:0] ep_q;
logic [31:0] drop_q, later_q;
logic cap_q;
logic [CAUSE_W-1:0] cause_q;
assign epoch = ep_q;
assign item_stale = item_valid && (item_epoch != ep_q);
assign stale_dropped = drop_q;
assign captured = cap_q;
assign first_cause = cause_q;
assign later_faults = later_q;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
ep_q <= '0; drop_q <= '0; cap_q <= 1'b0; cause_q <= '0; later_q <= '0;
end else begin
// One counter bump invalidates every queued item everywhere -- no
// per-queue flush logic, and no branch that can forget one.
if (invalidate) ep_q <= ep_q + EPOCH_W'(1);
if (item_stale && !(&drop_q)) drop_q <= drop_q + 32'd1;
if (fault) begin
if (!cap_q) begin cap_q <= 1'b1; cause_q <= fault_cause; end
else if (!(&later_q)) later_q <= later_q + 32'd1; // count, never overwrite
end
if (debug_clear) begin cap_q <= 1'b0; cause_q <= '0; later_q <= '0; end
end
end
endmoduleimport pattern_pkg::*;
// VERIFICATION-ONLY. PATTERN 6 -- resource conservation.
// The cheapest assertion in this chapter, and the one most likely to find
// a lost owner. Checked PER CLASS, never summed: an aggregate is satisfied
// by two classes being wrong in opposite directions.
module conservation_monitor #(parameter int CLASSES = 4, parameter int N = 8) (
input logic [cnt_w(N)-1:0] total [CLASSES],
input logic [cnt_w(N)-1:0] free_cnt [CLASSES],
input logic [cnt_w(N)-1:0] live_cnt [CLASSES],
output logic err_conservation,
output logic err_summed_would_pass // the aggregate check is fooled
);
logic [31:0] st, sf, sl;
always_comb begin
err_conservation = 1'b0;
st = '0; sf = '0; sl = '0;
for (int c = 0; c < CLASSES; c++) begin
if ((free_cnt[c] + live_cnt[c]) != total[c]) err_conservation = 1'b1;
st += total[c]; sf += free_cnt[c]; sl += live_cnt[c];
end
// Demonstrates WHY per-class matters: the sum can balance while the
// parts do not (Chapter 21.4 §7 measured 0% aggregate detection).
err_summed_would_pass = err_conservation && ((sf + sl) == st);
end
endmoduleClassification: eight synthesizable, one verification-only, one compile-time.
Failure — ten, one per pattern. Reading live config · advancing on valid · re-arbitrating mid-packet · acting on observed availability · freeing in several branches · a single "current transaction" · re-reading a key after a pipeline stage · comparing the old counter value · a wrapping diagnostic · aliasing an out-of-range index · overwriting the first fault · and flushing queues by hand instead of by epoch.
10. Assertions
// ---- PATTERN 1: immutable snapshot ------------------------------
// P1: the effective value never changes while something owns it.
property p_snapshot_stable_while_owned;
@(posedge clk) disable iff (!rst_n) owned |=> $stable(effective);
endproperty
// P2: it changes only at an ownership boundary.
property p_snapshot_changes_only_at_boundary;
@(posedge clk) disable iff (!rst_n)
(effective != $past(effective)) |-> $past(take && !owned);
endproperty
// P3: a divergence is REPORTED, not hidden.
property p_snapshot_stale_reported;
@(posedge clk) disable iff (!rst_n) (owned && (live != effective)) |-> stale;
endproperty
// ---- PATTERN 2: hold until handshake ----------------------------
// P4: the payload is stable while stalled.
property p_hold_stable_under_stall;
@(posedge clk) disable iff (!rst_n)
(out_valid && !out_ready) |=> (out_valid && $stable(out_data));
endproperty
// P5: no reneging.
property p_hold_no_renege;
@(posedge clk) disable iff (!rst_n) (out_valid && !out_ready) |=> out_valid;
endproperty
// P6: `valid` is not a function of `ready` -- expressed structurally.
property p_hold_valid_independent;
@(posedge clk) disable iff (!rst_n) (out_valid == v_q);
endproperty
// P7: ownership moves exactly once per item.
property p_hold_transfer_once;
@(posedge clk) disable iff (!rst_n)
(out_valid && out_ready && !(in_valid && in_ready)) |=> !out_valid;
endproperty
// ---- PATTERN 3: packet-lock arbitration -------------------------
// P8: the owner is stable until the EOP transfers.
property p_lock_owner_stable;
@(posedge clk) disable iff (!rst_n)
(owner_valid && !(out_valid && out_ready && eop[owner])) |=>
(owner_valid && $stable(owner));
endproperty
// P9: released only on a TRANSFERRED end of packet.
property p_lock_release_on_transfer;
@(posedge clk) disable iff (!rst_n)
$fell(owner_valid) |-> $past(out_valid && out_ready && eop[owner]);
endproperty
// ---- PATTERNS 4/5: reserve, and one terminal event --------------
// P10: at most one grant per cycle.
property p_alloc_single_grant;
@(posedge clk) disable iff (!rst_n) grant |-> avail;
endproperty
// P11: a granted resource was free.
property p_alloc_grants_free_only;
@(posedge clk) disable iff (!rst_n) grant |-> free_map[grant_idx];
endproperty
// P12: a granted resource is no longer free next cycle.
property p_alloc_removes_from_pool;
@(posedge clk) disable iff (!rst_n)
(grant && !(free_req && (free_idx == grant_idx))) |=> !free_map[$past(grant_idx)];
endproperty
// P13: freeing an already-free resource is a DOUBLE terminal event.
property p_no_double_free;
@(posedge clk) disable iff (!rst_n)
(free_req && free_map[free_idx]) |=> err_double_free;
endproperty
// P14: same-cycle free and allocate preserves the count.
property p_same_cycle_free_alloc;
@(posedge clk) disable iff (!rst_n)
(free_req && grant && (free_idx != grant_idx)) |=> $stable(free_count);
endproperty
// ---- PATTERN 6: conservation ------------------------------------
// P15: the accounting identity holds, PER CLASS.
property p_conservation_per_class;
@(posedge clk) disable iff (!rst_n) !err_conservation;
endproperty
// ---- PATTERN 7: context table -----------------------------------
// P16: exactly one lookup outcome.
property p_ctx_outcome_total;
@(posedge clk) disable iff (!rst_n)
lkp_valid |-> $onehot({hit, miss, ambiguous});
endproperty
// P17: a live key is unique.
property p_ctx_key_unique;
@(posedge clk) disable iff (!rst_n)
(live_q[0] && live_q[1]) |-> (key_q[0] != key_q[1]);
endproperty
// P18: a miss applies nothing -- it never aliases to entry 0.
property p_ctx_miss_no_effect;
@(posedge clk) disable iff (!rst_n) miss |=> $stable(live_q);
endproperty
// P19: a hit names an entry whose key really matches.
property p_ctx_hit_key_matches;
@(posedge clk) disable iff (!rst_n) hit |-> (key_q[hit_idx] == lkp_key);
endproperty
// P20: inserting a duplicate key is refused and reported.
property p_ctx_dup_refused;
@(posedge clk) disable iff (!rst_n)
(ins_valid && dup) |-> (!ins_grant ##1 err_dup_key);
endproperty
// ---- PATTERN 8: metadata with data ------------------------------
// P21: what emerged was fetched for the key presented with it.
property p_pipe_key_pairing;
@(posedge clk) disable iff (!rst_n)
(s1_valid && ram_val_live) |-> (ram_key_out == s1_key);
endproperty
// P22: skew is reported stickily.
property p_pipe_skew_sticky;
@(posedge clk) disable iff (!rst_n) err_skew |=> err_skew;
endproperty
// ---- PATTERNS 9/10: next-state and saturation -------------------
// P23: the threshold is evaluated on the NEXT value, not the old one.
property p_nextstate_compare;
@(posedge clk) disable iff (!rst_n)
(add_valid && ((count + add_delta) >= threshold) && !saturated) |=> reached;
endproperty
// P24: the counter saturates and never wraps.
property p_counter_saturates;
@(posedge clk) disable iff (!rst_n)
(count == {W{1'b1}}) |=> (count == {W{1'b1}});
endproperty
// P25: saturation is sticky, so the window can be discarded.
property p_saturation_sticky;
@(posedge clk) disable iff (!rst_n) saturated |=> (saturated || clear);
endproperty
// ---- PATTERN 11: range-safe index -------------------------------
// P26: an out-of-range index produces no response and is reported.
property p_range_safe;
@(posedge clk) disable iff (!rst_n)
(req_valid && !in_range) |-> (!rsp_valid ##1 err_out_of_range);
endproperty
// ---- PATTERNS 12/13: evidence -----------------------------------
// P27: the first fault is latched and locked.
property p_first_failure_sticky;
@(posedge clk) disable iff (!rst_n)
(captured && !debug_clear) |=> (captured && $stable(first_cause));
endproperty
// P28: later faults are counted, never stored over the first.
property p_later_faults_counted;
@(posedge clk) disable iff (!rst_n)
(captured && fault && !debug_clear) |=> $stable(first_cause);
endproperty
// P29: a stale-epoch item is never executed.
property p_stale_epoch_dropped;
@(posedge clk) disable iff (!rst_n)
(item_valid && (item_epoch != epoch)) |-> item_stale;
endproperty
// P30: invalidation advances the epoch exactly once.
property p_epoch_advances_once;
@(posedge clk) disable iff (!rst_n)
invalidate |=> (epoch == $past(epoch) + EPOCH_W'(1));
endproperty
// ---- CROSS-CUTTING ----------------------------------------------
// P31: diagnostics never drive the functional path.
property p_diagnostics_non_functional;
@(posedge clk) disable iff (!rst_n)
$stable({grant, out_valid, hit}) or !$stable({stale_dropped, later_faults});
endproperty
// P32: reset returns every pool to its baseline.
property p_reset_baseline;
@(posedge clk) (!rst_n) |=> ((free_map == {N{1'b1}}) && !out_valid && !captured);
endpropertyThirty-two properties, and they are deliberately generic. P4, P8 and P13 alone would have caught defects in five different chapters — the value of a pattern library is that one property, instantiated everywhere, replaces the same reasoning done from scratch each time.
11. Measured Behaviour — The Composed Harness
12. The Review Checklist
This table is meant to be used during code review, not read once. Every entry names the pattern it violates.
| # | Smell | Pattern violated |
|---|---|---|
| 1 | valid asserted only when ready is high | 2 — hold until handshake |
| 2 | payload assigned combinationally from an upstream source | 2 |
| 3 | a counter advanced inside if (valid) | 2 |
| 4 | a control register read directly in a datapath expression | 1 — snapshot |
| 5 | a snapshot taken on every cycle rather than at a boundary | 1 |
| 6 | no way to tell that live and effective have diverged | 1 |
| 7 | if (resource_available) issue() in more than one producer | 4 — reserve |
| 8 | a grant that is not one-hot | 4 |
| 9 | a resource freed in two or more case branches | 5 — one terminal event |
| 10 | an error exit that does not pass through the release path | 5 |
| 11 | a release with no check that the resource was owned | 5 |
| 12 | no TOTAL == FREE + LIVE assertion anywhere | 6 — conservation |
| 13 | a conservation check that sums across classes or jobs | 6 |
| 14 | a single "current transaction" register | 7 — context table |
| 15 | a table keyed by something that is not unique | 7 |
| 16 | a lookup miss that falls through to entry 0 | 7, 11 |
| 17 | two matches resolved by a priority encoder | 7, 11 |
| 18 | a key re-read at the far end of a pipeline | 8 — metadata with data |
| 19 | a synchronous RAM lookup with no carried metadata | 8 |
| 20 | count <= count + d; followed by if (count == X) | 9 — next state |
| 21 | a same-cycle decision made on a registered value | 9 |
| 22 | a diagnostic counter with no saturation | 10 |
| 23 | functional protocol state that saturates instead of asserting | 10 (inverted) |
| 24 | table[external_index] with no range check | 11 |
| 25 | an out-of-range index masked down instead of reported | 11 |
| 26 | a status register written by every error | 12 — first failure |
| 27 | a sticky flag that is actually a pulse | 12 |
| 28 | queue flushing written per-queue in each invalidating branch | 13 — epoch |
| 29 | an epoch or generation counter transmitted on a protocol interface | 13 (misuse) |
| 30 | an arbiter that can change owner mid-packet | 3 — packet lock |
| 31 | an owner released on eop asserted rather than transferred | 3 |
| 32 | a monitor output that feeds back into a functional decision | cross-cutting |
| 33 | a parameterized block never tested at its minimum (N=1) | cross-cutting |
| 34 | $clog2(N) used without guarding N == 1 | cross-cutting |
| 35 | a retry path that creates a second owner of the same work | 5 |
Two entries deserve a note because they are the ones reviewers argue about.
Entry 23 is deliberately inverted. Diagnostics must saturate; functional protocol state must not (22.3 §10). A credit counter that saturates has hidden an error the design is required to prevent — there, the right answer is to prove the bound and assert it, and saturation is a bug that looks like defensiveness.
Entry 29 is the misuse of an otherwise-good pattern. An epoch is local architectural state. Transmitting it invents a protocol field, exactly as Chapter 21.3 §12's hop guard would if it were transmitted. The pattern is powerful precisely because it costs nothing outside the design.
13. Debugging by Pattern
Symptom — it only fails under backpressure. Pattern 2 or 3. Something advanced on an offer instead of a transfer, or an arbiter changed owner mid-packet. Assertion to add: P4 on every decoupled interface, then P8 on any shared output. This is the single most common signature in Modules 22–23, measured at 17.7%, 79.1% and 80.7% in three different blocks.
Symptom — it only fails after a configuration write. Pattern 1. A live control value reached a datapath that already owned work. Assertion: P1 and P3 — and P3 is the one that turns an invisible race into a readable status bit.
Symptom — it only fails after errors. Pattern 5. A resource is released on the success path and not on the error path. Assertion: P13, plus a conservation check at rest. Chapter 23.3 §14 measured the engine wedging after 14 jobs.
Symptom — it only fails with more than one outstanding transaction. Pattern 7. Something is using "the current transaction" instead of a keyed context. Assertion: P16–P19. This appeared in 22.2 (80.0% of latency samples wrong), 21.4 (76.3%) and 23.5 (39.7%).
Symptom — it only fails at the minimum parameter.
Cross-cutting: $clog2(1) == 0. A zero-width index, a zero-modulus counter, or a for loop that never executes. Assertion: instantiate every parameterized block at N = 1 in regression, which is checklist entries 33 and 34.
Symptom — it passed simulation and failed on the FPGA. Pattern 8. A table that was flops in simulation became a RAM with a cycle of latency. Assertion: P21. Chapter 23.5 §12 measured 87.5% of lookups mispaired without the carried key.
Symptom — the counters read implausibly large.
Pattern 9 or 10 — an unsigned underflow, or a wrap presented as a small number. Assertion: P24. Chapter 22.3 §11's 0 − 1 = 255 and 22.1 §11's 232 after 255 are the two canonical shapes.
Symptom — six blocks report errors and none of them is the cause. Pattern 12. The status you are reading is the last consequence. Assertion: P27, P28 — and if the design has no sticky capture, the timestamped log is more trustworthy than the register.
14. Misconceptions
"These are just coding conventions." Each one has a measured failure rate attached (§1's table); a convention does not wedge an engine after 14 jobs.
"A pattern library means adding an abstraction layer." The blocks in §9 are smaller than the code they replace, and CLAUDE.md's rule against inventing abstractions still applies — lift the shape, not a framework.
"valid can wait for ready; it saves a register." It is a deadlock when the other side does the same (§3, P6).
"Snapshots cost latency." One register, and it is the difference between 15.3% correct and 100% (§3).
"An arbiter that re-evaluates is fairer." It interleaved packets in 67.0% of runs (§3).
"Availability is close enough to ownership." The race arises in 65.6% of loaded cycles (§4).
"Cleanup belongs where the error is detected." That is how one branch forgets a resource (§4).
"Conservation assertions are for formal only." They are three lines of combinational logic and they find lost owners in simulation (§4, P15).
"A miss can default to entry 0; it is an error path anyway." Then the error corrupts entry 0's transaction (§5, P18).
"The old counter value is close enough for a same-cycle decision." It is a cycle late, and with a delta greater than one it can be missed entirely (§6, P23).
"All counters should saturate." Diagnostics should; functional protocol state should be proven bounded instead (§12, entry 23).
"Range checks are defensive clutter." An unchecked index aliases silently — 24.9% in the measured case (§6).
"The latest error is the most relevant." It is a non-root-cause 96.8% of the time (§7).
"An epoch counter is basically a sequence number." It is local state; transmitting it invents a protocol (§7, entry 29).
15. Understanding Check
Q1. A reviewer sees if (credit_available) send(); in two producers and says "they both check, so it's fine." What is the precise counterargument?
Checking is observation; sending requires ownership. Both checks are correct and both act on the same free resource — nothing in either producer prevents the other from doing so. §4 measured the collective over-want at 65.6% of loaded cycles, so this is the normal case, not a corner. The fix is structural: one grant per cycle, made centrally against one snapshot of the pool (P10), after which the producers hold reservations rather than inferences.
Q2. Why is count <= count + d; if (count == expected) wrong, and why is >= not sufficient to fix it?
Because count on the right of the comparison is the old value — the decision is a cycle late. Changing == to >= fixes only the "stepped past it" case; the timing is still wrong, so a same-cycle consumer sees the flag late. The fix is to compute next_count once and use it for both the register and the comparison (§6, P23). §6's measured instance is the free bitmap: next-state and old-value forms diverge in 6.3% of coincidences.
Q3. Your context table works in simulation and fails in the FPGA build. Which pattern, and what is the one-line fix? Pattern 8. The table became a synchronous RAM, so its answer arrives a cycle after the key was presented, and 87.5% of lookups pair a context with the wrong transaction (23.5 §12). The fix is to pipeline the key alongside the RAM read and check that what emerged carries the key that was asked for — P21.
Q4. Which single assertion would you add to a design you have never seen, if you could add only one?
Conservation (P15) — TOTAL == FREE + LIVE, per class. It is three lines of combinational logic, it needs no knowledge of the protocol, and it detects both failure modes of the ownership law: two owners and no owner. §11's harness shows it catching the free-before-dequeue mutation at 151,123 violations while the design otherwise looked healthy. The one caveat is that it must be per class or per job — an aggregate is satisfied by two classes being wrong in opposite directions (21.4 §7 measured that at 0% detection).
Q5. Diagnostics saturate, but §12 says functional credit counters should not. Why the asymmetry? Because they answer different questions. A diagnostic that saturates degrades honestly — it says "at least this many", and the sticky flag tells software to discard the window. A functional credit counter that saturates has silently tolerated a condition the protocol forbids, and it will keep transmitting on the basis of a number it invented. There, the bound must be proven and asserted (22.3 §10), and reaching it is a design error rather than a measurement limit.
Q6. A colleague adds an epoch field to a packet so the far end can discard stale work. What is wrong?
An epoch is local architectural state and this makes it a protocol field (§7, checklist entry 29). The far end has no defined behaviour for it, no other implementation will honour it, and the design now depends on a mechanism the specification does not contain — the same error as transmitting Chapter 21.3 §12's hop guard as a TTL. The pattern's value is precisely that it costs nothing outside the design: bump a counter, drop non-matching items on dequeue.
16. Module 23 Complete
Six chapters built an endpoint. 23.1 placed the boundaries and their contracts; 23.2 answered which aperture owns this address; 23.3 composed Module 20's pieces into an engine without collapsing ownership; 23.4 guaranteed a header and a payload describe the same transaction; 23.5 remembered every request that was still owed an answer; and this chapter named what all five had in common.
They had one thing in common. Every measured defect across the module — and across Module 22 before it — was an ownership failure, and the flattering direction of each one is why they survive review: the naive form is correct until something stalls, until a second transaction exists, or until an error occurs.
Module 24 stops building and starts proving. 24.1 Protocol Verification frames what must be verified across the Transaction, Data Link and Link-state layers, and why an oracle that shares code with the design proves nothing. Every model in Modules 20–23 was an independent oracle; 24.1 is about doing that deliberately, at the scale of a whole environment, and about localizing a failure to the layer whose contract it broke.