Architecture Review Checklist

Module 29 asked what a deployment actually committed to. Module 30 asks what a design review should have caught before any of it was built, and this chapter is the first gate: the architecture review, held while the design is still a document.

The review question this chapter turns on, asked once per dimension:

What invariant does the architecture require, and what mechanism actually enforces it?

An architecture document can assert an invariant in prose. Prose enforces nothing. The job of this review is to find every place where a required property has no mechanism behind it, while it is still cheap to add one.

1. How To Use This Chapter

Each of the nine review dimensions below is written as a working review item, not a bullet. Every one answers the same eight questions, because those are the eight a reviewer actually needs:

The last facet is the one that makes the review hard. Most broken architectures produce evidence that looks reassuring, and a reviewer who does not know which reassurance is worthless will accept it.

2. The One-Sentence Model

An architecture review is sound when the architecture is described, when every required invariant has a named enforcing mechanism, when authority over every resource is single-valued, when the failure domain is stated as a count, when resources are conserved by an equation, and when every liveness claim carries its environmental assumption — and "the architecture is sound" is bit 0.

3. What This Chapter Owns

4. Teaching-Model Boundary And Source Discipline

Every RTL block in this chapter is a teaching model. Each isolates one architectural invariant so it can be examined, mutated and broken on purpose. None is a production CXL controller, an implementation of any specification flow, or a complete design.

Nothing here states a normative CXL detail. No opcode, register field, message name, timing guarantee, negotiation sequence or allocation granularity from the specification appears anywhere in this chapter. The invariants reviewed — single-valued authority, resource conservation, stated failure domains — are general architecture properties that any coherent interconnect design must satisfy, and they are examined here in their general form deliberately, so the review technique transfers.

Each model is built twice. A parameter selects between the measured build, which enforces the invariant, and a weak build that asserts it without a mechanism. Every section's headline number is the gap between them.

5. Review Item 1 — Does Every Invariant Have A Mechanism?

Under review. Every statement in the architecture document of the form "X never happens" or "Y is always true".

Invariant at risk. All of them. This item is the meta-review: it counts how many required properties have something enforcing them and how many are assertions of intent.

Where it lives. Nowhere, which is the point. A mechanism is a structure — a generation counter, a credit, an arbiter, a conservation check. If the reviewer cannot point at one, there is not one.

// RTL 1 - an architecture claim with no enforcing mechanism.
//
// The review question this whole chapter turns on: what invariant does the
// architecture REQUIRE, and what mechanism actually ENFORCES it? A document can
// assert an invariant in prose, and prose enforces nothing.
//
// TEACHING MODEL. This isolates an architectural review property; it is not a
// production CXL controller or an implementation of any specification flow.
module claim_without_mechanism #(parameter int PROSE_IS_A_MECHANISM = 0) (
  input  logic clk, rst_n,
  input  logic        review,
  input  logic [15:0] invariants_required, mechanisms_named, claims_total, claims_enforceable,
  output logic [15:0] unenforced, named_ok, enforceable_pct, covered_pct,
  output logic        architecture_enforced,
  output logic [7:0]  n_reviews, n_unenforced,
  output logic        arch_err
);
  logic [31:0] e_q, c_q;
  logic [15:0] true_unenforced;
  logic        truly_unenforced;
  assign named_ok = (mechanisms_named > invariants_required)
                  ? invariants_required : mechanisms_named;
  assign true_unenforced = invariants_required - named_ok;
  assign unenforced = (PROSE_IS_A_MECHANISM != 0) ? 16'd0 : true_unenforced;
  // How much of the document could in principle be falsified by a review.
  assign e_q = (claims_total == 16'd0) ? 32'd0
             : (({16'd0, claims_enforceable} * 32'd100) / {16'd0, claims_total});
  assign enforceable_pct = (e_q > 32'd100) ? 16'd100 : e_q[15:0];
  assign c_q = (invariants_required == 16'd0) ? 32'd100
             : (({16'd0, named_ok} * 32'd100) / {16'd0, invariants_required});
  assign covered_pct = (PROSE_IS_A_MECHANISM != 0) ? 16'd100 : c_q[15:0];
  assign architecture_enforced = (unenforced == 16'd0) && (invariants_required != 16'd0);
  assign truly_unenforced = (true_unenforced != 16'd0);
  assign arch_err = review && truly_unenforced && architecture_enforced;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_reviews <= 8'd0; n_unenforced <= 8'd0;
    end else if (review) begin
      n_reviews <= n_reviews + 8'd1;
      if (truly_unenforced) n_unenforced <= n_unenforced + 8'd1;
    end
  end
endmodule

Seven required invariants with three mechanisms named, in a document where six of twenty claims could be falsified by a review, leaves four invariants with nothing behind them and forty-two percent coverage.

Figure 1 — the shape of a document that cannot be wrong. The upper path's claims are all true statements of intent and none of them can be falsified by reading the design, which is precisely what makes them useless as review evidence. The lower path asks for a structure per invariant, and the four it cannot find are the four that will be discovered in silicon.

Evidence to demand. For each invariant, the name of the block or the signal that enforces it. Not a section number — a structure.

What escapes. Every failure in the rest of this chapter. An unenforced invariant is not a bug yet; it is the absence of the thing that would have prevented one.

How DV proves it. It cannot, directly. This is the one review item with no test behind it, which is exactly why it must be done by reading. A property with no mechanism has no failure mode to write a test against — the test would pass trivially on a design that does nothing.

Telemetry. None. That is the finding: an invariant with no mechanism also has no counter, so it cannot be monitored in silicon either.

Misleading evidence. A long, careful, internally consistent document. Volume of prose correlates with nothing, and a document that states an invariant three times in three sections is more convincing and no more enforced.

6. Review Item 2 — Is Authority Single-Valued, And What Makes It So?

Under review. Any claim of the form "only the owner may do X".

Invariant at risk. Safety: at most one party holds authority over a resource at any instant.

Where it lives. An ownership record — holder plus generation. The generation is the mechanism; the holder alone is not.

// RTL 2 - authority over a resource must be single-valued, and the mechanism
// that enforces it is a GENERATION, not a comment.
//
// The architectural invariant: at most one holder has authority at any instant.
// The mechanism: every grant carries a generation; a revoke advances it; a
// request stamped with a stale generation is refused. Without the generation
// the table still LOOKS right - it holds one owner - while a late request from
// a previous holder is silently honoured.
//
// TEACHING MODEL. Sequential, isolating one invariant.
//   State remembered : current holder, current generation, granted flag.
//   Safety           : two holders never hold authority simultaneously.
//   Reset semantics  : async reset revokes any grant and resets the generation.
//   Concurrency      : a grant request and a revoke in the same cycle resolve to
//                      exactly one transition, revoke first.
module ownership_authority #(parameter int GENERATION_IS_OPTIONAL = 0) (
  input  logic clk, rst_n,
  input  logic       grant_req, revoke_req, use_req,
  input  logic [3:0] requester, use_gen,
  output logic [3:0] holder, generation,
  output logic       granted, use_accepted, stale_use,
  output logic [7:0] n_grants, n_revokes, n_stale, n_honoured_stale,
  output logic       auth_err
);
  logic [3:0] hold_q, gen_q;
  logic       grant_q;

  assign holder     = hold_q;
  assign generation = gen_q;
  assign granted    = grant_q;

  // The mechanism. With GENERATION_IS_OPTIONAL the stamp is ignored and any use
  // from the recorded holder is accepted - which is the architecture that says
  // "only the owner may use it" and enforces only the first half.
  assign stale_use    = grant_q && use_req && (use_gen != gen_q);
  assign use_accepted = (GENERATION_IS_OPTIONAL != 0)
                      ? (grant_q && use_req && (requester == hold_q))
                      : (grant_q && use_req && (requester == hold_q) && (use_gen == gen_q));
  // SAFETY violation: a use stamped with a dead generation was honoured.
  assign auth_err = use_accepted && stale_use;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      hold_q <= 4'd0; gen_q <= 4'd0; grant_q <= 1'b0;
      n_grants <= 8'd0; n_revokes <= 8'd0; n_stale <= 8'd0; n_honoured_stale <= 8'd0;
    end else begin
      // Revoke has priority: a resource being taken away cannot also be granted
      // in the same cycle, and resolving both would create two holders.
      if (revoke_req && grant_q) begin
        grant_q <= 1'b0; hold_q <= 4'd0;
        gen_q   <= gen_q + 4'd1;          // the mechanism: advance the generation
        n_revokes <= n_revokes + 8'd1;
      end else if (grant_req && !grant_q) begin
        grant_q <= 1'b1; hold_q <= requester;
        n_grants <= n_grants + 8'd1;
      end
      if (stale_use)    n_stale          <= n_stale + 8'd1;
      if (auth_err)     n_honoured_stale <= n_honoured_stale + 8'd1;
    end
  end
endmodule

Why the holder alone is insufficient. The table holds one owner, so it looks single-valued at every instant. What it cannot do is distinguish a request issued by the current holder from a request issued by the previous holder that is still in flight. A late request from a revoked owner arrives carrying a perfectly valid-looking identity, and a design that checks only the identity honours it.

The mechanism. Every grant carries a generation. A revoke advances it. A request stamped with a stale generation is refused. The measured build checks the stamp; the weak build checks only the holder.

Evidence to demand. The width of the generation field, and what happens when it wraps. A four-bit generation wraps after sixteen revokes, and a request that is stale by exactly sixteen generations looks current again.

What escapes. Two writers to one resource. The corruption appears far from the cause, and the ownership table looks correct at every instant anybody inspects it.

How DV proves it. Grant, use legally, revoke, re-grant, then replay a request captured before the revoke. Assert it is refused. Also drive a use from a non-holder carrying a current stamp — the campaign for this chapter found that case missing.

Telemetry. A counter of stale requests detected, and separately a counter of stale requests honoured. The second should be permanently zero; the whole difference between a correct and an incorrect design shows up in that one counter.

Misleading evidence. "The ownership table only ever holds one entry." True and irrelevant. The table is not where the second owner lives — the second owner lives in a request that is already in flight.

7. Review Item 3 — Where Does This State Live, And Whose Failure Destroys It?

Under review. Every piece of state the design depends on.

Invariant at risk. Recoverability. After any single failure, the surviving parties must hold enough state to continue or to clean up.

Where it lives. By definition, the question. State held only in the requester dies with the requester; state held only in the device dies with a device reset; state held in both survives either and costs twice.

// RTL 3 - state placement decides who loses it. The review question is not "is
// the state correct" but "whose failure destroys it, and who else needed it".
//
// State held only in the requester is lost when the requester dies. State held
// only in the device is lost when the device resets. State held in both is
// recoverable and costs twice. An architecture that does not say WHERE has not
// answered the recovery question.
//
// TEACHING MODEL.
module state_placement #(parameter int STATE_IS_SOMEWHERE = 0) (
  input  logic clk, rst_n,
  input  logic        review,
  input  logic [15:0] state_items, held_requester_only, held_device_only, held_both,
  output logic [15:0] placed_ok, unplaced, lost_on_host_fail, lost_on_device_fail,
  output logic        placement_stated,
  output logic [7:0]  n_reviews, n_unplaced,
  output logic        place_err
);
  logic [31:0] p_q;
  logic [15:0] true_placed, true_unplaced;
  logic        truly_unplaced;
  assign p_q = {16'd0, held_requester_only} + {16'd0, held_device_only}
             + {16'd0, held_both};
  assign true_placed = (p_q > {16'd0, state_items}) ? state_items : p_q[15:0];
  assign placed_ok = true_placed;
  assign true_unplaced = state_items - true_placed;
  assign unplaced = (STATE_IS_SOMEWHERE != 0) ? 16'd0 : true_unplaced;
  // Items that vanish when each side fails. Items held in BOTH survive either.
  assign lost_on_host_fail   = held_requester_only;
  assign lost_on_device_fail = held_device_only;
  assign placement_stated = (unplaced == 16'd0) && (state_items != 16'd0);
  assign truly_unplaced = (true_unplaced != 16'd0);
  assign place_err = review && truly_unplaced && placement_stated;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_reviews <= 8'd0; n_unplaced <= 8'd0;
    end else if (review) begin
      n_reviews <= n_reviews + 8'd1;
      if (truly_unplaced) n_unplaced <= n_unplaced + 8'd1;
    end
  end
endmodule

Twelve state items with three held only in the requester, four only in the device and two in both, leaves three items placed nowhere — and a host failure destroys three while a device failure destroys four.

Stated is not the same as safe, and the model is deliberate about this. A design that holds everything only in the requester has fully stated placement — nothing is unplaced — and loses everything when the host dies. The review item catches the missing answer; judging the answer is a separate act.

Evidence to demand. A table with one row per state item and a column saying where it lives. Three columns at most: item, holder, survives-what.

What escapes. A recovery path that cannot run because the information it needs died with the thing it is recovering from. This is the failure that turns a single fault into an outage.

How DV proves it. Reset one side with live state on the other and assert the survivor can still make progress. Reset at time zero proves nothing about this — the state has to be live when the reset lands.

Telemetry. Counters of recovery attempts and recovery failures, separately. A recovery path that is never exercised in production is a recovery path nobody knows is broken.

Misleading evidence. "The state is replicated." Ask where. Replicated across two structures inside the same failure domain is not replicated for this purpose.

8. Review Item 4 — How Big Is The Failure Domain, As A Count?

Under review. Every shared element: a controller, a table, a port, a control plane.

Invariant at risk. The availability model. The design's stated failure independence must match the actual dependency graph.

Where it lives. In the topology, not in a reliability figure.

// RTL 4 - a failure domain is a count of what stops, not a probability.
// The architectural review asks: when THIS element fails, how many consumers
// stop? A design with one shared element serving many consumers has a failure
// domain the size of that consumer set, however reliable the element is.
//
// TEACHING MODEL.
module failure_domain #(parameter int SHARED_IS_RELIABLE = 0) (
  input  logic clk, rst_n,
  input  logic        review,
  input  logic [15:0] consumers, served_by_shared, shared_elements, consumer_value,
  output logic [15:0] domain_size, independent, exposure, domain_pct,
  output logic        domain_bounded,
  output logic [7:0]  n_reviews, n_wide,
  output logic        dom_err
);
  logic [31:0] e_q, p_q;
  logic [15:0] served_ok, true_domain;
  logic        truly_wide;
  assign served_ok = (served_by_shared > consumers) ? consumers : served_by_shared;
  assign true_domain = served_ok;
  // The weak build reports a shared element's failure as a single-consumer event
  // because the element is "reliable" - which is an argument about frequency
  // answering a question about blast radius.
  assign domain_size = (SHARED_IS_RELIABLE != 0) ? 16'd1 : true_domain;
  assign independent = consumers - served_ok;
  assign e_q = {16'd0, domain_size} * {16'd0, consumer_value};
  assign exposure = (e_q > 32'd9999) ? 16'd9999 : e_q[15:0];
  assign p_q = (consumers == 16'd0) ? 32'd0
             : (({16'd0, true_domain} * 32'd100) / {16'd0, consumers});
  assign domain_pct = p_q[15:0];
  assign domain_bounded = (domain_size <= 16'd1) && (consumers != 16'd0);
  assign truly_wide = (true_domain > 16'd1) && (shared_elements != 16'd0);
  assign dom_err = review && truly_wide && domain_bounded;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_reviews <= 8'd0; n_wide <= 8'd0;
    end else if (review) begin
      n_reviews <= n_reviews + 8'd1;
      if (truly_wide) n_wide <= n_wide + 8'd1;
    end
  end
endmodule

Twenty-four consumers with nine served by a shared element is a nine-consumer failure domain, fifteen independent, and one thousand three hundred and fifty units of consumer value stopping together.

Evidence to demand. For each shared element, the number of consumers that stop when it fails. One number per element.

What escapes. An availability model built on device counts rather than dependency counts. Twenty-four consumers with nine on one element is not twenty-four independent units and not one — it is fifteen plus one group of nine, and any plan built on either round number is wrong in a different direction.

How DV proves it. It does not; this is an architecture review item that DV inherits as a fault-injection requirement. The test is to fail the shared element and count what stops.

Telemetry. Consumers-served per shared element, as a standing inventory figure rather than an event counter.

Misleading evidence. A reliability number. "This element has an extremely low failure rate" answers a frequency question; the review asked a blast-radius question. At sufficient scale everything fails, and the only thing left to decide is how much goes with it.

9. Review Item 5 — What Enforces The Ordering You Assumed?

Under review. Any statement that responses, completions or events arrive in a particular order.

Invariant at risk. Safety: a consumer that assumes order never acts on an out-of-order arrival.

Where it lives. Either a single ordered path, or a reorder structure keyed by transaction identity. With neither, the assumption holds whenever the fabric happens to be orderly.

// RTL 5 - an assumed ordering with no mechanism enforcing it.
//
// The architecture says responses arrive in the order requests were issued. The
// mechanism that would enforce it is either a single ordered path or a reorder
// buffer keyed by transaction id. With neither, the assumption holds whenever
// the fabric happens to be orderly and fails silently when it is not.
//
// TEACHING MODEL. Sequential.
//   State remembered : the id expected next, and a seen-bitmap for reordering.
//   Safety           : a consumer that assumes order never retires out of order.
//   Reset semantics  : async reset clears the expectation and the bitmap.
module ordering_authority #(parameter int ORDER_IS_ASSUMED = 0) (
  input  logic clk, rst_n,
  input  logic       rsp_valid,
  input  logic [3:0] rsp_id,
  output logic [3:0] expected_id,
  output logic       retire, out_of_order,
  output logic [7:0] n_rsp, n_retired, n_reordered, n_misretired,
  output logic       order_err
);
  logic [3:0] expect_q;
  assign expected_id  = expect_q;
  assign out_of_order = rsp_valid && (rsp_id != expect_q);
  // The measured build retires only the response it was expecting; anything else
  // is held for a reorder buffer this model does not implement, and is counted.
  // The assumed-order build retires whatever arrives, in arrival order.
  assign retire = (ORDER_IS_ASSUMED != 0) ? rsp_valid
                                          : (rsp_valid && (rsp_id == expect_q));
  // SAFETY violation: something was retired in the wrong order.
  assign order_err = retire && out_of_order;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      expect_q <= 4'd0;
      n_rsp <= 8'd0; n_retired <= 8'd0; n_reordered <= 8'd0; n_misretired <= 8'd0;
    end else begin
      if (rsp_valid)    n_rsp       <= n_rsp + 8'd1;
      if (out_of_order) n_reordered <= n_reordered + 8'd1;
      if (order_err)    n_misretired<= n_misretired + 8'd1;
      if (retire) begin
        n_retired <= n_retired + 8'd1;
        expect_q  <= expect_q + 4'd1;
      end
    end
  end
endmodule

The measured build retires only the response it expects and counts anything else as a reorder. The assumed-order build retires whatever arrives — so when a response for identity five arrives while two is expected, it retires five and advances its expectation to six, past three identities it has never seen.

Evidence to demand. Ask which of the two mechanisms is present. If the answer is "the fabric preserves order", ask what enforces that and under which conditions it stops being true — congestion, multiple paths, retry.

What escapes. Data used before it is valid, or a completion matched to the wrong request. Both corrupt silently and both are extremely hard to trace back, because the failure surfaces in whatever consumed the wrongly-matched data.

How DV proves it. Deliver responses out of order deliberately and assert the consumer does not retire them out of order. A test that only ever delivers in order proves the design works on an orderly fabric, which was never in doubt.

Telemetry. A reorder counter, and separately a mis-retirement counter. As with ownership, the second should be permanently zero.

Misleading evidence. A long clean run. An ordering assumption that has never been violated in testing has never been tested — the absence of reordering in the stimulus is a property of the testbench, not of the design.

10. Review Item 6 — Do The Resources Balance?

Under review. Any finite table: outstanding transactions, buffers, credits, tags.

Invariant at risk. Safety and conservation: every entry that was allocated is in exactly one of a small number of states, and the states sum to the allocations.

Where it lives. In an equation the design can check on itself:

issued == completed + abandoned + outstanding

// RTL 6 - resource conservation. The architectural invariant is an equation:
//
//     issued  ==  completed  +  outstanding  +  abandoned
//
// Every transaction that was issued is in exactly one of those buckets. A design
// where the equation does not close is leaking table entries, and the leak is
// invisible until the table fills.
//
// TEACHING MODEL. Sequential.
//   State remembered : the outstanding count and the three lifetime totals.
//   Safety           : the conservation equation holds on EVERY cycle.
//   Concurrency      : an issue and a completion in the same cycle leave the
//                      outstanding count unchanged - the classic two-assignment
//                      counter defect this model is built to expose.
//   Reset semantics  : async reset zeroes everything; a surviving outstanding
//                      count would make the equation unverifiable forever after.
module resource_conservation #(parameter int ACCOUNTING_IS_IMPLICIT = 0) (
  input  logic clk, rst_n,
  input  logic       issue, complete, abandon,
  input  logic [7:0] table_depth,
  output logic [7:0] outstanding, n_issued, n_completed, n_abandoned,
  output logic       table_full, conserved,
  output logic [7:0] high_water,
  output logic       cons_err
);
  logic [7:0] out_q, iss_q, cmp_q, abn_q, hw_q;
  logic [8:0] lhs, rhs;
  // How many entries retire THIS cycle. A complete and an abandon in the same
  // cycle refer to two different transactions, so they retire two entries - not
  // one. Collapsing them with `complete | abandon` increments two lifetime
  // counters while removing one entry, and the conservation equation opens by
  // one for the rest of time. (Baseline defect 1, found before mutation.)
  logic [1:0] retiring;
  assign retiring = {1'b0, complete} + {1'b0, abandon};

  assign outstanding = out_q;
  assign n_issued    = iss_q;
  assign n_completed = cmp_q;
  assign n_abandoned = abn_q;
  assign high_water  = hw_q;
  assign table_full  = (out_q >= table_depth) && (table_depth != 8'd0);

  // The conservation check, computed from the LIFETIME totals rather than from
  // the outstanding counter, so it is an independent statement rather than a
  // restatement of the counter's own update.
  assign lhs = {1'b0, iss_q};
  assign rhs = {1'b0, cmp_q} + {1'b0, abn_q} + {1'b0, out_q};
  assign conserved = (ACCOUNTING_IS_IMPLICIT != 0) ? 1'b1 : (lhs == rhs);
  // SAFETY violation: the design claims conservation while the equation is open.
  assign cons_err = conserved && (lhs != rhs);

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      out_q <= 8'd0; iss_q <= 8'd0; cmp_q <= 8'd0; abn_q <= 8'd0; hw_q <= 8'd0;
    end else begin
      if (issue)    iss_q <= iss_q + 8'd1;
      if (complete) cmp_q <= cmp_q + 8'd1;
      if (abandon)  abn_q <= abn_q + 8'd1;
      // ONE assignment to the outstanding counter, computed from the NUMBER of
      // retirements rather than from whether any occurred. Two separate
      // conditional assignments would make a simultaneous issue-and-complete
      // lose one; collapsing two retirements into one would leak an entry.
      if ({1'b0, issue} >= retiring)
        out_q <= out_q + ({7'd0, issue} - {6'd0, retiring});
      else if ((out_q + {7'd0, issue}) >= {6'd0, retiring})
        out_q <= out_q + {7'd0, issue} - {6'd0, retiring};
      else
        out_q <= 8'd0;                        // clamp rather than wrap
      if (issue && (retiring == 2'd0) && ((out_q + 8'd1) > hw_q))
        hw_q <= out_q + 8'd1;
    end
  end
endmodule

The concurrency case is where designs break. An issue and a completion in the same cycle must leave the outstanding count unchanged. A completion and an abandonment in the same cycle refer to two different transactions and must retire two entries. Collapsing those two events into one — complete | abandon — increments two lifetime counters while removing one entry, and the equation opens by one per occurrence.

Figure 3 — why the check is computed from the lifetime totals rather than from the live counter. If the equation were derived from the same expression that updates outstanding, it would agree with that expression by construction and could never detect its failure. The three lifetime counters are independent evidence, and the equation is the only thing that relates them.

Evidence to demand. The equation, written down, with every state a transaction can be in. If a state is missing from the equation, it is a state the design forgets about.

What escapes. A slow table leak. Entries are lost one at a time under a condition nobody drives, the table fills after hours or days, and the symptom is a hang with no obvious cause. The outstanding counter looks entirely plausible throughout.

How DV proves it. Drive the simultaneous cases explicitly — issue with complete, complete with abandon — and check the equation after every one. Then over-retire on purpose: drive more completions than there were outstanding entries and assert the design reports the breach rather than clamping quietly.

Telemetry. All three lifetime counters plus the live one, so the equation can be evaluated in the field. A high-water mark on occupancy is worth more than the instantaneous value.

Misleading evidence. A healthy-looking outstanding count. It clamps at zero, never wraps, and stays in a believable range while the lifetime totals diverge. A design that watched only outstanding would see nothing wrong at all.

11. Review Item 7 — Who Has The Authority To Declare A Transaction Dead?

Under review. Every timeout, watchdog and abandonment path.

Invariant at risk. Safety: an entry is never retired twice. Liveness: a transaction that never gets a response is eventually abandoned — assuming the timer is enabled and the clock runs.

Where it lives. In whichever party owns the timer, and in the refusal path for everybody else.

// RTL 7 - who has the authority to declare a transaction dead?
//
// If two parties can independently time out the same transaction, they can
// disagree: one abandons and frees the entry while the other is still waiting,
// or both abandon and the entry is freed twice. The architectural requirement is
// that timeout authority is single-valued and that the loser of the race is told.
//
// TEACHING MODEL. Sequential.
//   State remembered : per-transaction age and whether it has been abandoned.
//   Safety           : an entry is never abandoned twice.
//   Liveness         : a transaction that never gets a response is eventually
//                      abandoned - ASSUMING the timer is enabled and the clock
//                      runs. If the environment may withhold the response
//                      forever AND the timer is disabled, nothing completes.
module timeout_authority #(parameter int BOTH_MAY_TIMEOUT = 0) (
  input  logic clk, rst_n,
  input  logic       start, response, local_timeout, remote_timeout,
  input  logic [7:0] limit,
  output logic [7:0] age,
  output logic       active, abandoned, double_abandon,
  output logic [7:0] n_started, n_completed, n_abandoned,
  output logic       to_err
);
  logic [7:0] age_q;
  logic       act_q, abn_q;
  logic       expired, local_fire, remote_fire;

  assign age       = age_q;
  assign active    = act_q;
  assign abandoned = abn_q;
  assign expired   = act_q && (age_q >= limit) && (limit != 8'd0);

  // Single authority: only the local side may declare death. The remote request
  // is observed and refused. With BOTH_MAY_TIMEOUT either side may fire, which
  // is the architecture that says "it will time out" and never says whose job.
  assign local_fire  = act_q && (local_timeout || expired);
  assign remote_fire = act_q && remote_timeout;
  assign double_abandon = (BOTH_MAY_TIMEOUT != 0) && local_fire && remote_fire;
  // SAFETY violation: two authorities retired the same entry in one cycle.
  assign to_err = double_abandon;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      age_q <= 8'd0; act_q <= 1'b0; abn_q <= 1'b0;
      n_started <= 8'd0; n_completed <= 8'd0; n_abandoned <= 8'd0;
    end else begin
      abn_q <= 1'b0;
      if (start && !act_q) begin
        act_q <= 1'b1; age_q <= 8'd0; n_started <= n_started + 8'd1;
      end else if (act_q) begin
        if (response) begin
          act_q <= 1'b0; n_completed <= n_completed + 8'd1;
        end else if (local_fire || ((BOTH_MAY_TIMEOUT != 0) && remote_fire)) begin
          act_q <= 1'b0; abn_q <= 1'b1;
          // Counted once per cycle even when two authorities fire, so the
          // double-abandon is visible on `to_err` rather than hidden in a count
          // that merely looks high.
          n_abandoned <= n_abandoned + 8'd1;
        end else begin
          age_q <= age_q + 8'd1;
        end
      end
    end
  end
endmodule

The failure is a race between two well-intentioned parties. If both ends may independently declare a transaction dead, they can disagree: one abandons and frees the entry while the other is still waiting, or both abandon and the entry is retired twice. The measured build gives the authority to one side and observes and refuses the other's request. The weak build lets either fire.

The liveness assumption is load-bearing and the model proves it. With the limit set to zero the timer is disabled, a transaction with no response sits active through ten cycles and is never retired — and no safety property is violated. It is simply stuck. A design that promises completion without stating the timer assumption has promised something it cannot deliver.

Evidence to demand. One sentence naming the party that may declare death, and the mechanism by which the other party's request is refused rather than merely unlikely.

What escapes. A double free. An entry retired by one authority is reallocated, and the second authority's retirement then frees an entry belonging to a different transaction. The corruption is one step removed from the cause.

How DV proves it. Fire both authorities in the same cycle and assert exactly one retirement. Then fire the non-authoritative one alone and assert nothing happens. Then disable the timer and assert the transaction is not retired — proving the liveness guarantee is conditional.

Telemetry. Abandonments by authority, counted separately. Any count on the non-authoritative path is a design escape.

Misleading evidence. "Both sides time out at the same value, so they will not disagree." Equal timeouts make the race more likely, not less — the two parties are most likely to fire together precisely when they are configured identically.

12. Review Item 8 — Does The Producer Actually Read The Backpressure?

Under review. Every flow-control claim.

Invariant at risk. Safety: occupancy never exceeds capacity.

Where it lives. In a credit the producer must hold before sending — not in a signal the consumer merely asserts.

// RTL 8 - a backpressure contract is only a contract if the producer reads it.
//
// The architecture says the consumer signals when it cannot accept. The
// mechanism is a credit the producer must hold before sending. Without the
// credit check the consumer still asserts its signal, the producer still sends,
// and the overflow is discovered as data loss rather than as backpressure.
//
// TEACHING MODEL. Sequential.
//   State remembered : credits held by the producer, occupancy at the consumer.
//   Safety           : occupancy never exceeds the consumer's capacity.
//   Concurrency      : a send and a drain in the same cycle leave occupancy
//                      unchanged and return exactly one credit.
module backpressure_contract #(parameter int CREDITS_ARE_ADVISORY = 0) (
  input  logic clk, rst_n,
  input  logic       send_req, drain,
  input  logic [7:0] capacity,
  output logic [7:0] credits, occupancy, n_sent, n_dropped,
  output logic       can_send, overflow,
  output logic       bp_err
);
  logic [7:0] cred_q, occ_q;
  logic       accept;

  assign credits   = cred_q;
  assign occupancy = occ_q;
  // The mechanism. The advisory build ignores it and sends regardless.
  assign can_send  = (cred_q != 8'd0);
  assign accept    = (CREDITS_ARE_ADVISORY != 0) ? send_req : (send_req && can_send);
  assign overflow  = accept && (occ_q >= capacity) && (capacity != 8'd0);
  // SAFETY violation: something was accepted into a full consumer.
  assign bp_err    = overflow;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cred_q <= capacity; occ_q <= 8'd0; n_sent <= 8'd0; n_dropped <= 8'd0;
    end else begin
      if (accept)               n_sent    <= n_sent + 8'd1;
      if (send_req && !accept)  n_dropped <= n_dropped + 8'd1;
      // One expression each: a simultaneous send and drain must net to zero
      // rather than losing an entry or a credit.
      case ({accept, drain})
        2'b10: begin occ_q <= occ_q + 8'd1; cred_q <= (cred_q == 8'd0) ? 8'd0 : cred_q - 8'd1; end
        2'b01: begin occ_q <= (occ_q == 8'd0) ? 8'd0 : occ_q - 8'd1; cred_q <= cred_q + 8'd1; end
        default: begin occ_q <= occ_q; cred_q <= cred_q; end
      endcase
    end
  end
endmodule

A signal is advice; a credit is a mechanism. The consumer can assert "full" perfectly correctly and the producer can send anyway. The measured build refuses the send and counts the drop, making the overrun visible; the advisory build accepts it into a full consumer.

The advisory build's drop counter is the tell. It reports zero drops while overflowing, because from its point of view nothing was dropped — everything was sent. The overrun is invisible to the very counter a reviewer would check.

Evidence to demand. Where the credit is held, how it is returned, and what happens on reset. Credits that initialise to the wrong value are a whole class of bug: too many and the consumer overflows on the first burst, too few and the link never reaches its rated throughput.

What escapes. Silent data loss, or a hang if the loss corrupts a protocol state machine.

How DV proves it. Exhaust the credits and assert the next send is refused and counted. Drive a simultaneous send and drain and assert occupancy and credits both stay put. Drain an empty consumer and assert the occupancy clamps rather than wrapping.

Telemetry. Credits available, occupancy high-water, and drops — all three. Drops alone are insufficient because the failing design reports none.

Misleading evidence. A clean traffic capture. The producer and consumer agree at every point in a well-behaved test; the contract is only tested when the consumer is genuinely full, which a smooth test never achieves.

13. Review Item 9 — Does Every Liveness Claim Carry Its Assumption?

Under review. Every statement of the form "eventually", "always completes", "never hangs".

Invariant at risk. The honesty of the whole document. A liveness property is not a property of the design alone — it holds only if the environment eventually does its part.

Where it lives. In the sentence. This item is about wording, and the wording is the engineering.

// RTL 9 - a liveness claim is only a claim once its environmental assumption is
// written down.
//
// "Every request eventually completes" is not a property of the design alone. It
// holds only if the environment eventually supplies the responses the design is
// waiting for. An architecture document that states the conclusion and omits the
// assumption has stated something it cannot deliver.
//
// TEACHING MODEL.
module liveness_assumption #(parameter int LIVENESS_IS_UNCONDITIONAL = 0) (
  input  logic clk, rst_n,
  input  logic        review,
  input  logic [15:0] liveness_claims, assumptions_stated, env_may_withhold, guarded_claims,
  output logic [15:0] unconditional, stated_ok, guarded_pct, at_risk,
  output logic        liveness_sound,
  output logic [7:0]  n_reviews, n_unconditional,
  output logic        live_err
);
  logic [31:0] g_q;
  logic [15:0] true_unconditional;
  logic        truly_unconditional;
  assign stated_ok = (assumptions_stated > liveness_claims)
                   ? liveness_claims : assumptions_stated;
  assign true_unconditional = liveness_claims - stated_ok;
  assign unconditional = (LIVENESS_IS_UNCONDITIONAL != 0) ? 16'd0 : true_unconditional;
  // Claims that are unconditional AND sit in an environment permitted to
  // withhold forever are the ones that cannot be delivered at all.
  assign at_risk = (env_may_withhold != 16'd0) ? true_unconditional : 16'd0;
  assign g_q = (liveness_claims == 16'd0) ? 32'd100
             : (({16'd0, guarded_claims} * 32'd100) / {16'd0, liveness_claims});
  assign guarded_pct = (g_q > 32'd100) ? 16'd100 : g_q[15:0];
  assign liveness_sound = (unconditional == 16'd0) && (liveness_claims != 16'd0);
  assign truly_unconditional = (true_unconditional != 16'd0);
  assign live_err = review && truly_unconditional && liveness_sound;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_reviews <= 8'd0; n_unconditional <= 8'd0;
    end else if (review) begin
      n_reviews <= n_reviews + 8'd1;
      if (truly_unconditional) n_unconditional <= n_unconditional + 8'd1;
    end
  end
endmodule

Six liveness claims with two carrying their assumptions, in an environment permitted to withhold responses, leaves four unconditional promises and all four at risk.

The environment matters as much as the count. The same document in an environment that cannot withhold forever has the same four unconditional claims and none of them at risk — the model reports both numbers separately, because a document can be incomplete without being wrong.

Evidence to demand. For each liveness claim, the assumption written in the same sentence. "Every request completes" becomes "every request completes, assuming the device eventually returns a response and the timeout is enabled."

What escapes. A hang that nobody accepts responsibility for, because the design met its stated property and the environment was never stated.

How DV proves it. Bound it and prove the withdrawal. Run for a defined number of cycles and assert the good thing happened; then remove the assumption and assert it does not happen. Asserting only the success case leaves the assumption untested — the good thing happening proves nothing about whether it needed the assumption.

Telemetry. Time-in-state and oldest-entry age. A liveness failure is a transaction that is still there, so the evidence is an age distribution rather than an event.

Misleading evidence. "It has never hung in simulation." Simulation environments are almost always well-behaved by construction; the assumption being relied on is usually one the testbench satisfies automatically.

14. The Review Assembled

Nine dimensions, one summary.

// RTL 10 - an architecture review assembled. Nine review dimensions, one
// summary. "The architecture is sound" is bit 0: an opinion, and one sixth of a
// review.
module architecture_signoff #(parameter int DESCRIBED_IS_REVIEWED = 0) (
  input  logic clk, rst_n,
  input  logic        review,
  input  logic        architecture_described, mechanisms_named, authority_single,
  input  logic        failure_domain_stated, resources_conserved, liveness_qualified,
  output logic [5:0]  fail_mask,
  output logic [15:0] conditions_met, sound_pct,
  output logic        sound,
  output logic [7:0]  n_reviews, n_sound, n_claimed,
  output logic        signoff_err
);
  logic [31:0] s_q;
  logic        truly_sound, claimed;
  assign fail_mask[0] = ~architecture_described;
  assign fail_mask[1] = ~mechanisms_named;
  assign fail_mask[2] = ~authority_single;
  assign fail_mask[3] = ~failure_domain_stated;
  assign fail_mask[4] = ~resources_conserved;
  assign fail_mask[5] = ~liveness_qualified;
  assign conditions_met = {15'd0, architecture_described} + {15'd0, mechanisms_named}
                        + {15'd0, authority_single} + {15'd0, failure_domain_stated}
                        + {15'd0, resources_conserved} + {15'd0, liveness_qualified};
  assign s_q = ({16'd0, conditions_met} * 32'd100) / 32'd6;
  // No clamp: six one-bit values over six cannot exceed a hundred, so a ceiling
  // would be unreachable code.
  assign sound_pct = s_q[15:0];
  assign truly_sound = (fail_mask == 6'd0);
  assign claimed = (DESCRIBED_IS_REVIEWED != 0) ? architecture_described : truly_sound;
  assign sound = claimed;
  assign signoff_err = review && !truly_sound && claimed;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      n_reviews <= 8'd0; n_sound <= 8'd0; n_claimed <= 8'd0;
    end else if (review) begin
      n_reviews <= n_reviews + 8'd1;
      if (truly_sound) n_sound <= n_sound + 8'd1;
      if (claimed)     n_claimed <= n_claimed + 8'd1;
    end
  end
endmodule

Across the eight evaluations, the assembled model calls one review sound and the described-is-reviewed view signs off seven of eight.

The bit order is by how much of the design each condition carries. Bit 1 is first among the five because it is the meta-condition: without mechanisms the other four are being asked about assertions. Bits 2 and 4 are the two safety invariants with the sharpest silicon consequences. Bit 3 is the availability model and bit 5 is the honesty of every "eventually" in the document.

15. Quantitative Reasoning

Every figure here is a teaching parameter or a value derived from one and asserted by the testbench. None is a measurement of a real system.

Four invariants of seven unenforced, in a document where six of twenty claims could be falsified — forty-two percent coverage.

A four-bit generation wraps after sixteen revokes. That is the storage decision behind section 6: a request stale by exactly sixteen generations aliases to current. Widening to eight bits costs four flops per tracked resource and pushes the alias to two hundred and fifty-six.

Ownership table storage, derived. For N concurrently bindable resources with an H-bit host id and a G-bit generation, the table costs N × (H + G + 1) bits — the extra bit being the granted flag. At N=64, H=8, G=8 that is 64 × 17 = 1,088 bits. The generation is a quarter of it, which is the price of the mechanism in section 6.

A nine-consumer failure domain out of twenty-four, at one hundred and fifty units each, is one thousand three hundred and fifty stopping together — thirty-seven percent of the estate, and the estate is fifteen units plus one group of nine rather than twenty-four.

The conservation equation at work: five issued, five completions and one abandonment driven is six retirements for five issues, so 5 != 5 + 1 + 0 and the breach is reported — while the outstanding counter sits at zero and looks entirely normal.

Outstanding-table sizing, derived. To sustain B bytes per second over a round trip of T seconds with entries of S bytes, the table needs at least B × T / S entries. At an illustrative 32 GB/s, 600 ns and 64 B that is 32e9 × 600e-9 / 64 = 300 entries. Round up for burstiness; a table sized for the average stalls at the peak. These are illustrative figures, not CXL specification numbers.

Credit initialisation. Credits load from capacity at reset. Three credits, three sends, zero credits, and the fourth send refused and counted — while the advisory build accepts it and reports zero drops.

Six liveness claims with two qualified is fifty percent guarded, and four at risk in an environment permitted to withhold.

16. Verification Method

Order of work

compile → inspect warnings → legal baseline → reset → boundaries → simultaneous events → abuse and error cases → configuration contrasts → PASS → mutation campaign

A mutation campaign on failing RTL is invalid. A mutation of a broken design still fails the same assertions, and the kill is recorded for the wrong reason. This chapter's baseline found a real defect before any mutation ran; section 19 covers it.

Independent oracles

Expected values are reasoned from the specification of the model, never copied from its implementation.

If the oracle and the design disagree, either could be wrong. chkv prints both numbers for exactly that reason — and in this chapter it caught two cases where the design was right and my expectation was wrong.

X and Z rejected explicitly

chk(c, …) tests c !== 1'b1, so an X-valued condition fails rather than passing. chkv(got, exp, …) reduces the result and reports an explicit X/Z failure before comparing.

Pulses are latched, never sampled

Single-cycle outputs — abandoned, overflow, retire, and every safety monitor — are caught by a continuous always @(posedge clk) monitor and asserted outside any conditional. A check nested inside if (pulse) cannot fail when the defect is that the pulse never fires.

Both builds are always instantiated

Every parameterised model here has both its measured and weak build wired up and contrasted. This is carried directly from 29.5, where three sequential models had only their measured build and a mutation on a parameter-selected branch was the only thing that found it.

Safety, liveness and performance kept apart

Safety — authority stays single-valued; an entry is never retired twice; occupancy never exceeds capacity; a consumer never retires out of order. No assumptions required.

Liveness — a transaction eventually completes or is abandoned, assuming the timer is enabled and the clock runs. The model proves the withdrawal: with the limit set to zero, a transaction with no response sits active indefinitely and no safety property is violated.

Performance — a fifteen-cycle bind, a three-deep credit budget, a three-hundred-entry table. These are targets. A design that misses one is slow or small, not incorrect.

17. Assertions

The testbenches carry 428 checks — 215 across the first five models, 213 across the last five.

Every output of every model is asserted as a value, in both builds. The output-listing step reports nothing on either testbench.

Every simulator-derived value printed to the reader is asserted. The displayed-value gate scans 129 printed references and reports zero unasserted derived values. Testbench-driven inputs are excluded — those are constants the author set, not results the simulator produced.

Reset is verified with live state, not only at time zero: with a grant live, with a transaction active, with credits consumed and occupancy non-zero, and with a stale ordering expectation.

Simultaneous events are driven: grant with revoke, issue with completion, completion with abandonment, send with drain, and both timeout authorities in one cycle.

Abuse cases are driven and asserted to be no-ops: a second grant while one is live, a use from a non-holder carrying a live stamp, a revoke with nothing granted, a start while already active, a completion with nothing outstanding, and a drain on an empty consumer.

18. Mutation Testing

108 mutations injected, 108 killed. No mutation was withdrawn as equivalent in this chapter.

Eight survivors on the first run, every one classified before anything was changed.

Three were missing abuse cases in the ownership model — an early grant while one is live, a use from the wrong requester carrying a valid stamp, and a spurious revoke burning a generation. The nominal and boundary stimulus exercised the mechanism thoroughly and never asked what happens when the requester violates the protocol rather than the design.

Two were missing checkers — the weak build's error output was asserted high on the race and never asserted low on the single-authority case.

One was an imprecise observation. The high-water mark was asserted after the table had genuinely reached four, by which time both builds agree; asserted immediately after the simultaneous event, the mutation dies.

One was a coincidental result — three unenforced cases out of six reviews is exactly half, so an inverted counter reaches the same total. A seventh case makes it observable.

And one was a survivor of my own fix. The checker added for the fifth survivor did not kill it, because I placed the assertion one delta after the pulse it was meant to observe. It read a quiet cycle in which the signal is legitimately low in both builds — a check that could never fail. This is the same vacuity shape 29.5 found nested inside a conditional, arriving through a different door.

The tooling finding

The coincidental-result survivor should have been caught in advance and was not. splitcheck.py locates counter pairs by name, expecting a total ending in n and a sub-count ending in x. This chapter named its review counter …r, for reviews. The tool matched nothing and reported a confident zero.

That is the second distinct way the same tool has gone blind in two chapters — 29.5 changed the assertion idiom, 30.1 changed a net name. Both times it reported clean rather than unreadable. The counters were renamed to the shared convention, which restored the check — and it then caught a second even split, in section 13, prospectively, before that campaign ran.

The general lesson belongs in 30.3: a checker that infers its subject from a naming convention will keep failing this way, and a structural check that reports zero must be independently confirmed to have actually read its input.

19. Baseline Defects Found Before Mutation

RTL defect — duplicate retirement opened the conservation equation

Symptom. With a completion and an abandonment driven in the same cycle, the model reported issued 5, completed 2, abandoned 1, outstanding 3 — and 5 ≠ 2 + 1 + 3.

Root cause. The outstanding counter was updated from case ({issue, (complete | abandon)}). Collapsing two retirement events with an OR increments two lifetime counters while removing one entry. A completion and an abandonment in the same cycle refer to two different transactions.

Fix. Compute the number of retirements — retiring = complete + abandon — and apply issue − retiring, clamped at zero rather than wrapped.

Why it matters. One leaked table entry per simultaneous pair, invisible in the outstanding counter, surfacing as a hang when the table fills.

Testbench defects — three, all stimulus sequencing

A monitor sampled one cycle before it latches; a race driven against a build that had already retired its transaction; and a capacity changed after reset released, when credits load from it at reset.

Wrong oracles — two, both mine

One claimed a simultaneous completion and abandonment should retire one entry; the other mis-counted the unconditional-liveness cases. Neither was a design fault. Both were caught because chkv prints got-versus-expected, which is what lets an oracle be wrong out loud rather than silently agreeing with a bug.

Simulator constraints

Icarus Verilog 13.0 rejects ref task arguments, carried from 29.5. Under -Wall the ten models produce no truncation, select-width, signedness, cast, multiplication-width, shift-width or loop-width warnings. The only warning is a missing timescale on models that contain no delay constructs at all — inspected and recorded as benign rather than silenced, because adding a simulation directive to published teaching RTL would be noise in the lesson.

20. Synthesis And Implementation Reality

The generation field is the cheapest mechanism in this chapter and the one most often omitted. Four bits per tracked resource buys protection against stale identity; the cost is the alias at sixteen revokes, and widening it is linear in resources.

The ownership record is a table, and the table organisation is the real decision. Indexed by resource id it is a simple array with a one-cycle lookup. Keyed by requester it needs an associative search — a CAM, or a hash with collision handling — and the comparator count scales with the number of concurrent holders. Indexed is almost always right here, because authority is a property of the resource rather than of the requester.

The conservation counters are cheap and the equation is not free. Four counters of width W cost 4W flops; the comparison is a W+2-bit adder and an equality. It sits outside the datapath, so it costs area rather than timing — which is why it is one of the few self-checks worth leaving in production silicon.

The credit counter's width must cover the capacity, and its reset value is the capacity. That coupling is a common source of bugs when capacity is parameterised and the reset value is not updated with it.

The timeout age counter sizes the timeout window. An eight-bit age at one increment per cycle gives a window of 256 cycles; a longer window needs either a wider counter or a prescaler, and the prescaler introduces a granularity that must be accounted for when two parties compare timeouts.

Centralised versus distributed authority is the structural choice behind section 11. A single arbiter makes the authority trivially single-valued and becomes a failure domain of its own — which is section 8, applied to the mechanism from section 6.

No area, frequency or power figures appear in this chapter, because none was measured.

21. Silicon Observability

Three counters here are "must be permanently zero" counters — stale honoured, mis-retirements, and abandonments by the non-authoritative party. They cost almost nothing, they never fire in a correct design, and each one captures a safety escape that would otherwise present as data corruption far from its cause.

The pattern to read: a high stale-detected count with a zero stale-honoured count is a healthy design in a busy fabric. The same detected count with a non-zero honoured count is a different chip.

Rising occupancy high-water with a stable instantaneous occupancy means bursts are growing while the average is flat — the table is closer to full than any dashboard shows.

A conservation equation that drifts open by a constant is a leak that happened once. One that drifts steadily is a leak per event, and the event is whatever is most correlated with the drift rate.

22. DebugLabs

Lab 1 — Two hosts write the same resource and the ownership table looks correct

Symptom. Memory corruption traced to two parties writing one resource. Every inspection of the ownership table shows exactly one owner.

Evidence. Stale-requests-detected is non-zero. Stale-requests-honoured is also non-zero. Grant and revoke counts are consistent.

Hypothesis. A request issued before a revoke is being honoured after the re-grant, because the check compares the holder and not the generation.

Investigation. Capture a request's identity and its generation stamp at issue, and compare against the generation at the point it is accepted. If the stamps differ and the request was accepted, the mechanism is missing or bypassed.

Root cause. Authority enforced by identity alone. The table is single-valued at every instant and the in-flight request is the second owner.

Fix. A generation stamped at grant, advanced at revoke, and compared at use. Refuse on mismatch.

Prevention. A directed test that replays a request captured before a revoke, plus a mutation that removes the generation comparison — which must fail that test.

Telemetry. Stale-honoured as a sticky counter. It should never leave zero.

Lab 2 — The outstanding table fills after four days

Symptom. A hang after days of operation. Restarting clears it. Occupancy is at the table limit.

Evidence. Issued minus completed minus abandoned does not equal outstanding. The gap grows slowly and monotonically. Occupancy high-water reached the limit hours before the hang.

Hypothesis. An entry is leaked under some condition, and the condition is rare.

Investigation. Evaluate the conservation equation continuously rather than at inspection points. Correlate the drift rate with event counters until one matches. A drift of one per simultaneous completion-and-abandonment is the signature in this chapter's model.

Root cause. Two retirement events collapsed into one decrement. Two lifetime counters advanced; one entry was freed.

Fix. Count retirements rather than detecting that one occurred, and apply the count.

Prevention. Drive every simultaneous pair explicitly and check the equation after each. This is the defect 30.1's own baseline found.

Telemetry. All four counters exported so the equation can be evaluated in the field, plus the high-water mark.

Lab 3 — A transaction is retired twice and a different one is corrupted

Symptom. A completion is delivered for a transaction that was already abandoned, and an unrelated transaction's data is wrong.

Evidence. Abandonments-by-authority shows counts on both the local and remote paths. Total abandonments exceed the number of transactions that actually timed out.

Hypothesis. Both ends may declare death independently, and they raced.

Investigation. Check whether the non-authoritative path has any count at all. Any non-zero value there is the answer. Then check whether the two timeout values are configured identically — equal timeouts make the race more likely, not less.

Root cause. Timeout authority was never made single-valued. The architecture said "it will time out" and never said whose job it is.

Fix. Nominate one authority and refuse the other's request explicitly rather than relying on it being slower.

Prevention. Fire both in the same cycle and assert exactly one retirement; fire the non-authoritative one alone and assert nothing happens.

Telemetry. Abandonments split by authority, permanently.

Lab 4 — Data is lost under burst load and no counter shows it

Symptom. Occasional lost entries under burst traffic. Every flow-control signal behaves correctly on a capture.

Evidence. The drop counter reads zero. Occupancy briefly exceeded capacity. Credits reached zero before the overflow.

Hypothesis. The producer is sending without holding a credit. The consumer's signal is correct and unread.

Investigation. Compare sends against credits consumed. If sends exceed the credits ever issued, the producer is not gated. The drop counter is useless here — the failing design drops nothing, it sends everything.

Root cause. Backpressure implemented as advice rather than as a credit the producer must hold.

Fix. Gate the send on credit availability, and count refusals.

Prevention. Exhaust the credits and assert the next send is refused and counted. Assert occupancy never exceeds capacity as a continuous property.

Telemetry. Credits, occupancy high-water and drops together. Any one alone can look healthy while the design overflows.

Lab 5 — A completion is matched to the wrong request

Symptom. A requester receives data belonging to a different transaction. Both transactions were legal and both completed.

Evidence. The reorder counter is non-zero. The mis-retirement counter is also non-zero. The fabric has more than one path.

Hypothesis. The consumer assumes ordering that nothing enforces, and retired an out-of-order arrival against the wrong expectation.

Investigation. Check whether responses can take more than one path, and whether retry is in play. Then check whether the consumer has a reorder structure keyed by identity or is relying on arrival order.

Root cause. An ordering assumption with no mechanism. It held while the fabric was orderly.

Fix. Either force a single ordered path, or match on transaction identity rather than on arrival position.

Prevention. Deliver responses out of order deliberately. A test that only ever delivers in order proves the design works on an orderly fabric, which was never in question.

Telemetry. Reorders and mis-retirements as separate counters. The first is a fabric property; the second is a design escape.

Lab 6 — Recovery cannot run after a host failure

Symptom. A host fails. The device cannot clean up, and the resource is stuck until a full reset.

Evidence. The recovery path needs transaction context. The context was held only in the host.

Hypothesis. State placement was never reviewed — the information the recovery needs died with the thing being recovered from.

Investigation. List every state item and where it lives. Anything held only in the failed party is unavailable to the recovery.

Root cause. Placement was stated and the answer was bad, which is a different finding from placement being unstated. Both are review failures and only one looks like one.

Fix. Replicate the minimum context the recovery path needs, or move it to the surviving side.

Prevention. Reset one side with live state on the other and assert the survivor makes progress. Reset at time zero proves nothing here.

Telemetry. Recovery attempts and recovery failures counted separately, so a recovery path that never works is visible before it is needed.

Lab 7 — A transaction never completes and nothing is wrong

Symptom. A transaction sits outstanding forever. No error, no timeout, no assertion.

Evidence. Oldest-entry age grows without bound. The timeout limit is configured to zero. No safety property is violated.

Hypothesis. The liveness guarantee was conditional on a timer that is disabled.

Investigation. Check the timer configuration first, before looking at the fabric. A disabled timer produces exactly this symptom and violates nothing.

Root cause. The architecture promised completion without stating the assumption. The environment was permitted to withhold the response and the mechanism that would have bounded the wait is off.

Fix. Either enable the timer or state the assumption honestly, so whoever operates the system knows a withheld response is unbounded.

Prevention. Assert the liveness property and its withdrawal: with the timer disabled, assert the transaction is not retired.

Telemetry. Oldest-entry age. A liveness failure is not an event — it is the continued presence of something, so the evidence is an age rather than a count.

Lab 8 — The availability model said twenty-four independent units

Symptom. A single element fails and nine consumers stop, in a system rated for single-unit failures.

Evidence. Nine consumers share one element. The inventory lists twenty-four devices. The availability model used the device count.

Hypothesis. The failure domain was never counted; the device count was used as a proxy.

Investigation. For each shared element, count consumers that depend on it. The estate is fifteen independent units plus one group of nine, not twenty-four and not one.

Root cause. A reliability argument was accepted in place of a blast-radius count. "This element rarely fails" answers a frequency question.

Fix. Either reduce the sharing, or record the true domain in the availability model and engineer for it.

Prevention. A fault-injection test per shared element that counts what stops.

Telemetry. Consumers-per-shared-element as standing inventory. It changes when the topology changes, which is exactly when the availability model goes stale.

23. The Review, As A Working Checklist

Nine questions. Ask each one, and refuse the answers in the right-hand column.

Every entry in the right-hand column is something a competent engineer says in good faith. They are not evasions; they are answers to a slightly different question than the one asked. The skill being trained is noticing the substitution.

24. How This Appears In Real Engineering

The failure is an invariant everybody believes and nothing enforces, and it survives review because the belief is correct.

The most common shape is section 6. The architecture says only the owner may access the resource, and the implementation checks the owner. Every review passes. The second owner is not in the table — it is in a request that was issued before the revoke and is still in flight, and it carries a perfectly valid identity.

The second is section 10 and it is the slowest. The outstanding table leaks one entry per simultaneous retirement pair. The counter never wraps, never looks implausible, and stays in a believable range for days. The hang, when it comes, has no obvious cause and no recent change to blame.

The third is section 11 and it is found during an incident. Both ends time out. They were configured with the same value because that seemed symmetric and safe, which makes the race maximally likely rather than minimally.

The fourth is section 12. Flow control is implemented as a signal rather than a credit. The capture looks perfect, every signal behaves correctly, and the drop counter reads zero — because the failing design does not drop anything, it sends everything.

The fifth is section 13 and nobody is at fault. The design met its stated liveness property and the environment was never stated. The hang is real, the specification is satisfied, and the argument about whose bug it is takes longer than the fix.

Four of these five have a counter that would have caught them, and in three of the four that counter must read permanently zero to be useful.

25. Common Misconceptions

"The document says the invariant holds." Which structure enforces it? Section 5.

"Only one owner is in the table." The second owner is in flight. Section 6.

"The state is replicated." Across which failure domains? Section 7.

"That element almost never fails." How many consumers stop when it does? Section 8.

"The fabric preserves ordering." Under congestion? Under retry? Section 9.

"The outstanding count looks healthy." Does the equation close? Section 10.

"Both sides will time out." Then both may retire the same entry. Section 11.

"The consumer signals when it is full." Does the producer read it? Section 12.

"Every request eventually completes." Assuming what? Section 13.

26. Interview And Design-Review Questions

Architecture and review judgement

1. What is the single question an architecture review exists to ask? What invariant does the architecture require, and what mechanism enforces it. Everything else is a specialisation of that. A document can assert any property it likes; the review's job is to find the properties with nothing behind them while adding a mechanism is still cheap.

2. How do you tell a mechanism from an intention? A mechanism is a structure you can point at — a counter, a credit, an arbiter, a comparison. If the answer to "what enforces this" is a section number or a sentence, there is no mechanism.

3. Why is "the ownership table holds exactly one entry" not a proof of single-valued authority? Because the second owner is not in the table. It is a request issued by the previous holder that is still in flight, carrying an identity that is still valid. The table is single-valued at every instant you inspect it and the system is not.

4. What is the cheapest mechanism that fixes that? A generation stamped at grant, advanced at revoke, compared at use. Four bits per resource. The cost is that it aliases after sixteen revokes, which is a width decision rather than a design flaw.

5. What is the difference between "state is unplaced" and "state is badly placed"? The first is a review failure — nobody said where it lives. The second is a design decision that may be wrong. Only the first looks like a review failure, which is why a model that reports placement as fully stated can still be describing a system that loses everything when the host dies.

6. Why is a failure domain a count rather than a probability? Because at sufficient scale everything fails, so the frequency question is settled and the remaining question is how much stops. Twenty-four consumers with nine on a shared element is fifteen independent units plus one group of nine — not twenty-four, and not one.

7. An architect answers a blast-radius question with a reliability number. What has happened? A substitution. "This element rarely fails" is true and answers a different question. It is the single most common way a failure-domain review gets closed without being done.

8. When is centralising authority the right call? When single-valuedness matters more than the availability of the arbiter. Centralising makes the invariant trivial to enforce and creates a failure domain the size of everything the arbiter serves — section 8 applied to section 6's mechanism.

9. What makes a liveness claim honest? The environmental assumption in the same sentence. "Every request completes" is not a property of the design. "Every request completes, assuming the device eventually responds and the timeout is enabled" is.

10. Why can a design satisfy its liveness specification and still hang? Because the specification omitted the assumption. The design met what was written; the environment did something the document never ruled out. Nobody is at fault and the argument takes longer than the fix.

11. What do you do when an architecture states an invariant you cannot find a mechanism for? Record it as unenforced and put a number on it. Four of seven unenforced is a finding a programme can act on; "I have some concerns about the ownership section" is not.

12. Why review before RTL exists? Because every mechanism in this chapter is cheap to add to a document and expensive to retrofit into a design. A generation field is four bits at architecture time and a structural change after the ownership path is built.

RTL and microarchitecture

13. Why is the conservation equation computed from lifetime totals rather than from the live counter? Because an equation derived from the same expression that updates the counter agrees with it by construction and can never detect its failure. The three lifetime counters are independent evidence.

14. What goes wrong with case ({issue, (complete | abandon)})? A completion and an abandonment in the same cycle refer to two different transactions. The OR collapses them into one retirement, so two lifetime counters advance and one entry is freed. The equation opens by one per occurrence and the outstanding counter still looks plausible.

15. What is the correct form? Compute the number of retirements — complete + abandon — and apply issue − retiring, clamped at zero rather than wrapped.

16. Why clamp rather than wrap on underflow? Because a wrapped counter reports 255 outstanding entries where zero belong, and every downstream decision built on it is wrong in a large, obvious way that still takes hours to trace. A clamp keeps the counter plausible and lets the conservation equation report the breach.

17. What is the risk in a four-bit generation? A request stale by exactly sixteen generations aliases to current and is accepted. Widening is linear in tracked resources; the review question is whether sixteen revokes can plausibly occur inside one request's maximum lifetime.

18. Why is the ownership table indexed by resource rather than by requester? Because authority is a property of the resource. Indexed gives a one-cycle array lookup; keyed by requester needs an associative search whose comparator count scales with concurrent holders.

19. How should a simultaneous grant and revoke resolve? Revoke first, explicitly. A resource being taken away cannot also be granted, and resolving both in one cycle produces two holders. The priority must be written down and asserted, not left to synthesis.

20. What must reset do to an ownership record? Clear the holder, clear the granted flag, and reset the generation. A grant that survives reset is a resource two parties believe they hold.

21. What must reset do to a credit counter? Load it from capacity. Credits that initialise wrong are a whole bug class — too many and the consumer overflows on the first burst, too few and the link never reaches rated throughput.

22. Why is a one-deep skid with a counted reject better than a deep queue with a silent drop? Because depth does not remove the overrun, it raises the burst size that triggers it. The design question is whether the overrun is reported.

23. How do you size an outstanding-transaction table? Bandwidth times round-trip latency divided by entry size, then rounded up for burstiness. A table sized for the average stalls at the peak.

24. What does a prescaler on a timeout counter cost you? Granularity. Two parties comparing timeouts must account for it, or a design that looks like it has margin has none.

Verification

25. Why must the baseline pass before mutation testing? Because a mutation of a broken design still fails the same assertions, and the kill is recorded for the wrong reason. A perfect mutation score proves the checkers detect change; it says nothing about whether what was changed was right.

26. What is an independent oracle? An expected value reasoned from the model's specification rather than copied from its implementation. If the oracle restates the design, the test cannot fail when the design is wrong.

27. Give a case where the oracle was wrong and that was useful. Two in this chapter. Both were caught because the check prints got-versus-expected, so a disagreement identifies which side to examine rather than just failing. An oracle that can only agree is not independent.

28. How do you stop an X-valued condition passing a check? Compare against a known value. c !== 1'b1 fails on X; if (!c) does not. For data, reduce and reject unknowns before comparing.

29. Why is a check inside if (pulse) dangerous? Because a defect that suppresses the pulse also suppresses the check. Latch the event in a continuous monitor and assert the flag outside any branch.

30. This chapter found a second form of that. What was it? An assertion placed one delta after the pulse it was meant to observe. It read a quiet cycle where the signal is legitimately low in both builds — a check that could never fail, without ever being nested inside anything.

31. What is the first thing you do with a surviving mutation? Classify it, before touching the design or the testbench. Equivalent, stimulus gap, missing checker, vacuous checker, unreachable checker, masked, coincidental, or a structural configuration gap. The action differs completely.

32. What question separates an equivalent mutant from a stimulus gap? Is there any legal input for which the mutated expression is observably different? No means equivalent — withdraw it, do not manufacture stimulus. Yes means the stimulus has a hole.

33. When is a counter-inversion mutation equivalent? When the interesting cases are exactly half the total, so inverting reaches the same count. It is equivalent because of the stimulus, not the code, and one more case of either kind fixes it.

34. Three of this chapter's survivors were the same shape. Which? Missing abuse cases. The stimulus exercised the mechanism thoroughly under legal traffic and never asked what happens when the requester violates the protocol — a second grant while one is live, a use from a non-holder, a revoke with nothing granted.

35. How do you verify a liveness property in simulation? Bound it and state the assumption: run for a defined number of cycles and assert the good thing happened. Then prove the withdrawal — remove the assumption and assert it does not happen. Asserting only success leaves the assumption untested.

36. What should reset testing cover beyond time zero? Reset with live state: a live grant, an active transaction, consumed credits, a stale ordering expectation. Reset at time zero only proves the initial values.

37. Why instantiate the weak build at all? Because a parameter that changes behaviour and is never instantiated is untested behaviour. 29.5 found three sequential models with only their measured build wired up, and only a mutation on a parameter-selected branch could find it.

38. How do you know a structural check is actually reading your testbench? Run it against known-good material and confirm the count it reports. This chapter's split checker reported a confident zero because a net name did not match its expected convention. A checker that cannot parse its input reports clean, not unreadable.

39. What coverage would you write for the ownership model? Cross the request type against the generation relationship: current stamp, stale stamp, and stamp from a wrapped generation, each with a matching and a non-matching requester. The interesting bin is stale stamp with matching requester — the one the weak build honours.

Silicon and debug

40. Which counters must read permanently zero? Stale requests honoured, mis-retirements, and abandonments by the non-authoritative party. Each costs almost nothing, never fires in a correct design, and captures a safety escape that would otherwise present as corruption far from its cause.

41. Stale-detected is high and stale-honoured is zero. What does that mean? A healthy design in a busy fabric. Late identities are arriving and being refused, which is the mechanism working. The same detected count with a non-zero honoured count is a different chip.

42. The drop counter reads zero and data is being lost. What is happening? The producer is not gated on credits. It drops nothing because it sends everything. The counter a reviewer would check is the one the failing design cannot populate.

43. Occupancy is stable and the high-water mark is rising. What does that tell you? Bursts are growing while the average is flat. The table is closer to full than any instantaneous dashboard shows, and the margin is disappearing before anything looks wrong.

44. A conservation equation drifts open by a constant versus steadily. What is the difference? A constant means it happened once — a single event leaked entries. Steady drift means a leak per event, and the event is whatever correlates with the drift rate.

45. What is the only evidence of a liveness failure? The continued presence of something. A liveness failure is not an event, so the telemetry is an age distribution — oldest-entry age — rather than a counter.

46. If you could keep three counters from this whole chapter, which? Stale-honoured, the conservation equation's four totals, and oldest-entry age. The first catches a safety escape, the second catches a leak nothing else sees, and the third is the only evidence of a hang.

27. Exercises

1 — Architecture review. You are given a document stating "only the owner may access the region" and an implementation that compares a host id. Write the review finding: name the invariant at risk, the missing mechanism, the evidence you would demand, and the failure that escapes.

2 — Quantitative. An ownership table tracks 128 resources with a 10-bit host id. Compute the storage with a 4-bit and an 8-bit generation, state the aliasing window for each, and argue which you would choose given a maximum request lifetime of 200 cycles and a worst-case revoke rate of one per 50 cycles.

3 — RTL implementation. Extend the conservation model with a fourth retirement class — rejected — that removes an entry without counting as a completion. State what changes in the equation, in the retiring computation, and in the telemetry, and identify the new simultaneous case that must be tested.

4 — Assertions. Write the safety and liveness assertions for the timeout-authority model. State explicitly which is which, name the environmental assumption the liveness one requires, and explain why the safety one needs none.

5 — Testbench design. Design the stimulus that would have caught the duplicate-retirement defect in section 10 before a mutation campaign. Specify the exact simultaneous events and the check after each, and explain why a test that drives completions and abandonments separately cannot find it.

6 — Waveform reasoning. Using Figure 2, state what an observer monitoring only the holder row would conclude about cycles 2 through 6, what the gen row adds, and which single cycle contains the safety violation in the weak build.

7 — Debugging. A fleet reports stale-detected at 4,200 and stale-honoured at 3. Produce a hypothesis, state whether this is a design escape or a fabric property, and give the next measurement you would take.

8 — Coverage design. Define a functional coverage model for the backpressure contract that would have found the advisory-credit defect without anybody suspecting it. Specify the bins, the cross, and identify which bin the failing design can never hit.

28. Summary

An invariant with no mechanism is prose, and counting them is the meta-review every other item depends on.

Authority is single-valued only if a generation makes it so — the table holds one owner and the second owner is in flight.

State placement decides whose failure destroys it, and stated placement is not the same as safe placement.

A failure domain is a count of what stops, not a reliability figure.

An assumed ordering with no mechanism holds until the fabric stops being orderly, and fails silently when it does.

Resources are conserved by an equation computed from independent totals — and a healthy-looking outstanding counter hides a leak indefinitely.

Timeout authority must be single-valued, and two parties configured identically race most.

Backpressure is a credit the producer holds, not a signal the consumer asserts — and the failing design reports zero drops.

Every liveness claim carries its environmental assumption, or it is a promise the design cannot keep.

Six conditions, and "the architecture is sound" is one of them. One review of eight is sound; the described-is-reviewed view signs off seven.