Relationship to CHI

Module 13 has built one coherency domain: permissions, windows, ownership and a state space.

Real systems have two. A host SoC runs a coherent fabric internally — on Arm-based designs, typically CHI — and reaches devices over CXL. Both are coherency protocols. They are not the same protocol, and the engineering that matters is at the seam.

1. The Engineering Problem — Two Vocabularies, One Line

A cache line inside a host SoC is described by the fabric's coherency protocol: its states, its request types, its serialisation point. The same line, cached by a device across a CXL link, is described by CXL's. Both descriptions are of one physical line, and they must never contradict each other.

That is harder than it sounds, for three reasons that have nothing to do with either protocol's details.

The vocabularies are not a bijection. A state in one protocol may have no exact counterpart in the other. A request type may have no counterpart at all. When a bridge encounters one, it has to do something, and the something it does is where correctness is won or lost.

There must be exactly one point of coherence per address. Both domains have a serialisation point — the place where conflicting requests for one address are ordered. If both of them believe they are the serialisation point for the same address, the address has no serialisation point at all. The bridge must map one onto the other, or be one; it must never quietly become a second.

The boundary can create failures neither domain has alone. Two protocols with independent flow control, joined by a bridge with a shared queue, produce a dependency cycle that exists in neither protocol's specification. Deadlock at a boundary is almost never a bug in either protocol.

2. The One-Sentence Model

A boundary translates, and translation is lossy. A crossing may weaken a permission and may add an obligation; it may never grant a permission or forgive a debt — and exactly one side of the boundary serialises any given address.

Call it weaken, never grant. Every defect in this chapter is a crossing that invented a permission, forgave a debt, or created a second point of coherence.

3. What This Chapter Owns

Deferred:

4. Teaching-Model Boundary

Every model below is a teaching model, compiled and simulated with Icarus Verilog 13.0, checked by a testbench whose oracle is structurally different from the design.

What these models are not: a coherency bridge. There is no link layer, no credit scheme, no address decode, no multi-hop routing, no error correction, and no protocol encoding of any kind. A production bridge is a protocol converter with a directory, a transaction table and an ordering engine.

The four conventions from earlier chapters carry over: checkers test cond !== 1'b1; unreachable monitors get a FAULT_INJECT build of the same source; policies are compared as one source under a parameter; and every displayed value is a captured signal.

One new convention. Where a mapping is described, the design uses abstract state and opcode numbers rather than either protocol's encodings. That is not laziness — it is the point. The constraints hold whatever the encodings are, and writing them abstractly is what keeps this chapter from becoming a table nobody can check.

5. RTL 1 — Translation Is Lossy

Take one domain with five states and one with four — the second has no state meaning "shared, dirty, and I owe the data." Four of the five map exactly. The fifth is the whole problem:

      O: begin
           // 0 narrows to S (safe), 1 widens to M, 2 widens to E. Both
           // widenings grant something the near domain never granted; they
           // differ only in which permission they invent.
           dst_st = (WIDEN_ON_DOUBT == 1) ? M :
                    (WIDEN_ON_DOUBT == 2) ? E : S;
           exact  = 1'b0;
         end

with the safety property stated separately from the mapping:

  // A mapping may lose information. It may never CREATE permission.
  assign widened_err = map_en && ((dst_st == M && src_st != M)
                               || (dst_st == E && src_st != E && src_st != M));

Three policies were driven on identical stimulus. Measured:

  state map : exact=4 lossy=1 | O narrowed to 1 (S=1); widened to M=1 to E=1

Narrowing to shared is safe. The far domain gets a permission no stronger than the near domain held, and the dirty data must be written back before the crossing — which costs a writeback, exactly the one 13.3 showed MOESI existing to avoid. That cost is the price of the boundary, and it is why a line that migrates repeatedly across a domain boundary loses the benefit of the Owned state entirely.

Both widenings were caught by the same monitor. They are worth distinguishing because they are different mistakes with the same shape: mapping O to M hands the far domain write permission on dirty data; mapping O to E hands it write permission on data it believes is clean, so the eventual writeback is skipped as well. A mapping that grants is not a rounding error. It is a permission nobody issued.

The testbench's oracle knows nothing about state encodings. It holds permission as an order — I is weaker than S is weaker than E is weaker than M — and checks only that the destination is no stronger than the source:

  // Oracle: permission strength as an ORDER, not as a state name. A mapping is
  // safe if the destination is no stronger than the source. Nothing here knows
  // any state encoding -- it knows only that I < S < E < M.

Note where O sits in that order: at the same strength as S, because ownership is a duty rather than a permission. That is the 13.3 result restated in the only form a mapping can use.

6. RTL 2 — One Point Of Coherence Per Address

Both domains have a serialisation point. For any given address, exactly one of them must be it:

  assign forward        = req &&  addr_is_far;
  // LOCAL_ANSWER lets the bridge answer for a far-serialised address, which is
  // exactly how a second point of coherence gets built by accident.
  assign answer_locally = req && (!addr_is_far || (LOCAL_ANSWER != 0));
  assign two_poc_err    = forward && answer_locally;
  assign orphan_resp_err= far_resp && !out_q;

The failure is not a bridge that decides to be a second serialisation point. It is a bridge that answers a request it could answer, for an address somebody else is also ordering — usually as a latency optimisation, and usually for a case that looked local. Measured:

  poc       : forwarded=1 answered=1 two_poc(local build)=1 orphan_resp=1

The correct build forwarded the far-serialised address and did not answer it. The LOCAL_ANSWER build did both, and two_poc_err fired.

orphan_resp_err catches the other direction: a response arriving with nothing outstanding. That is either a duplicate, a response to a request that already timed out, or a response for an address this bridge never forwarded — and all three are worth separating from a response that simply took a long time. The forwarded request was held outstanding across multiple cycles and only a genuine response retired it, because a bridge that clears its outstanding flag on a timer will accept the late response as an orphan and report a fault that is really its own.

7. RTL 3 — Some Requests Have No Counterpart

A state mapping can always produce something. A request mapping cannot:

      // An atomic has no counterpart: the far domain has no indivisible
      // read-modify-write, so it cannot be expressed as any single request.
      AT: begin dst_op = R;  mappable = 1'b0; end
      // A prefetch hint has no counterpart either, but for the opposite
      // reason: it is droppable, so it is not an error to have none.
      PF: begin dst_op = R;  mappable = 1'b0; end

Two unmappable requests, and only one of them is an error:

  // Dropping a hint is fine. Approximating an atomic into a plain read is not.
  assign unmappable_err   = valid && !mappable && (src_op == AT);
  assign approximated_err = valid && (APPROXIMATE != 0) && !mappable
                            && (src_op == AT);

The distinction is the content of this section. A prefetch hint is advisory: dropping it costs performance and nothing else, so a boundary that cannot carry it is allowed to discard it silently. An atomic is semantic: turning it into a plain read produces a request that will complete successfully and do the wrong thing. The lost-update measurement in 13.1 — two increments producing one, with no coherency rule broken — is exactly what an approximated atomic delivers.

Measured across six request types:

  translate : mapped=4 no-counterpart=2 unmappable_err=1 approximated(bad build)=1

Four mapped exactly, two with no counterpart, and precisely one error. The approximating build turned the atomic into a read and was caught. Every one of the four exact mappings was checked against its own counterpart rather than merely checked as "mappable" — a mutation that turned a read-unique into a plain read survived until that check was added, and it is a mapping error a real bridge could plausibly make.

8. Waveform — The Writer Crosses The Boundary

Transcribed from the printed cycle trace of the two-domain model in section 15.

The no_check row never goes low again. That is what a cross-domain SWMR violation looks like from the outside: not a crash, not an error, just a permanently inconsistent line that both domains believe they hold correctly. Over the full trace:

  grants: near=1 far=0 revocations=1
  unchecked build: near=2 swmr_err=1

The unchecked build issued two grants where the checked build issued one, which is exactly what makes it look faster in a benchmark.

9. RTL 4 — A Snoop Crossing The Boundary

A snoop must cross exactly once, and its response must return to the agent that asked:

  assign snoop_out = snoop_in && !busy_q;
  assign resp_to   = far_resp && busy_q && (far_resp_tag == tag_q);
  // FORGET_ID drops the stored requester, so the response goes to agent 0
  // whatever asked -- a response that is delivered and useless.
  assign resp_requester = (FORGET_ID != 0) ? 3'd0 : id_q;
  assign dup_forward_err = snoop_in && busy_q;
  assign misrouted_err   = resp_to && (resp_requester != id_q);

This is the identity-matching problem from 13.2 with one addition: the requester's identity is in the near domain's namespace and the tag is in the far domain's, so the bridge holds a translation for the duration of the transaction. Measured:

  forward : forwarded=2 returned=2 dup=1 misrouted(forgetful build)=1 tag=0

Two snoops crossed, each with a distinct tag, each returned. A response carrying a tag nothing was waiting on retired nothing — the check is far_resp_tag == tag_q, not merely busy_q, and a mutation that dropped the tag comparison survived until a wrong-tag response was driven while a snoop was genuinely outstanding. That is the stimulus that separates identity matching from arrival matching, and it is easy to leave out because the obvious test — a response with nothing outstanding — passes on both.

The FORGET_ID build delivered its response to agent 0 regardless of who asked. Note what that failure looks like: the response arrives, on time, well-formed, at the wrong agent. The requester times out; the recipient discards a response it did not ask for; and no counter anywhere reports a loss.

10. RTL 5 — Most Snoops Need Not Cross At All

A snoop that crosses a CXL link costs a link round trip. A snoop for a line the far domain does not hold costs nothing if the bridge knows that:

  assign must_cross  = snoop &&  far_holds;
  assign suppressed  = snoop && !far_holds;
  // The safety property: a suppressed snoop must be for a line the far domain
  // genuinely does not hold. The filter may be conservative, never optimistic.
  assign false_suppress_err = suppressed && shadow_q[snoop_line];

The direction of the safety property is the whole design. A filter that is out of date in the conservative direction sends snoops that were not needed — a performance cost, and nothing else. A filter that is out of date in the optimistic direction suppresses a snoop that had to cross, and the far domain keeps a copy the near domain believes it revoked.

The OPTIMISTIC build models the exact mechanism: it fails to record a line the far domain took, so its belief and reality diverge. The testbench maintains a shadow of what the far domain actually holds, independently of the filter, so the two can be compared. Measured:

  filter  : crossed=2 suppressed=2 false_suppress(optimistic build)=1

Two snoops crossed, two stayed local, and the optimistic build suppressed one that had to cross. The oracle for the filter is a set of plain integers rather than a bit vector, so a vector-indexing bug in the design cannot reproduce itself in the reference — and a mutation that indexed the filter with the wrong line was killed by exactly that.

The economics are in section 16, but the shape is already visible: a filter converts a link round trip into a lookup, and the fraction it converts is the only number that matters when deciding whether the filter is worth its storage.

11. RTL 6 — What Ordering Survives The Crossing

Not all of it, and the distinction is precise:

  // Completing an OLDER sequence number for an address already advanced past
  // it inverts the per-address order, which is the coherence order itself.
  assign same_addr_inversion_err = complete && seen_q[comp_addr]
                                   && (comp_seq < last_seq[comp_addr])
                                   && (REORDER_SAME_ADDR == 0);
  assign cross_addr_reorder = complete && (comp_seq < last_any_seq);

Per-address order must be preserved. It is the coherence order from 13.1 — the sequence that defines what "the latest value" means. Inverting it is not a performance artefact; it is a read returning a value that was overwritten.

Cross-address order need not be. Two requests to different addresses may complete in either order, and a bridge that preserves the ordering between them is paying for a guarantee coherency never promised. The model counts those rather than flagging them, which is the right treatment for a legal event worth measuring.

The per-address record advances only forwards:

        // Per-address progress is recorded only when it moves forward, so an
        // inversion cannot hide itself by updating the record.
        if (!seen_q[comp_addr] || comp_seq > last_seq[comp_addr]) begin
          last_seq[comp_addr] <= comp_seq;
        end

Without that guard an inversion updates the high-water mark to the older value, so repeating the same inversion stops being detected. The testbench drives the inversion twice for exactly that reason. Measured:

  order   : same-addr inversion=1 repeated=1 (permissive build=0) cross-addr reorders=4

The case that distinguishes the two rules is the last one driven: an address that has been seen before, completing a sequence number that is forward for itself but behind the global high-water mark. That is legal, and a bridge that compares against a single global counter reports it as a violation — which is worse than useless, because an ordering alarm that fires on legal traffic gets disabled.

12. RTL 7 — Weaken, Never Grant

Sections 5 through 11 are instances of one rule. This model states it directly, on two independent axes:

  // Two independent directions. Permission may only shrink; an obligation may
  // only grow. A crossing that drops a duty has silently forgiven a debt.
  assign perm_gained_err  = crossing && (dst_perm > src_perm);
  assign duty_dropped_err = crossing && src_duty && !dst_duty;
  assign cross_ok = crossing && !perm_gained_err && !duty_dropped_err;

Five crossings were driven: exact, weakening, obligation-adding, permission-gaining and debt-forgiving. Measured:

  conservative : safe=3 refused=2 | perm_gained=1 duty_dropped=1

Three safe, two refused, and the two are refused for different reasons. That separation matters in the same way the three access denials did in 13.4: a crossing that gains permission is a mapping-table error, and a crossing that forgives a debt is a writeback that was skipped. They have nothing in common except that both are unsafe.

The asymmetry is worth stating plainly, because it is counter-intuitive on first reading. Permission may only shrink; obligation may only grow. Both directions are conservative, but they point opposite ways — because a permission you did not receive costs you a retry, while a permission you should not have had costs you correctness, and an obligation you did not owe costs a writeback while an obligation you dropped costs the data.

13. RTL 8 — The Cycle That Neither Domain Has

Two protocols, each with independent flow control, joined by a bridge:

  // With separate channels a full request queue never blocks a response.
  // SHARED_CHANNEL couples them, which is where the cycle comes from.
  assign resp_ready = (rs_q < DEPTH[3:0])
                      && ((SHARED_CHANNEL == 0) || (rq_q < DEPTH[3:0]));
  assign req_ready  = (rq_q < DEPTH[3:0]);
  // The cycle: a request waiting for room while the response that would make
  // room is itself blocked behind that request.
  assign deadlock_err = req_in && !req_ready && resp_in && !resp_ready;

The request queue was filled and a response offered. Measured:

  channels : separate resp_ready=1 shared resp_ready=0 | deadlock separate=0 shared=1

With separate channels the response is accepted even though the request queue is full. That is the property that breaks the cycle: the response drains a request, which makes room, which lets the next request in. With a shared channel the response is blocked behind the requests it would have retired, and nothing moves again.

Neither protocol specifies this bug. Each one is deadlock-free on its own, and the cycle exists only in the structure that joins them — which is why "we use two proven protocols" is not an argument about deadlock freedom at a boundary. The fifth push into a full queue was driven explicitly to confirm the queue does not silently overflow, because a bridge that overflows instead of backpressuring converts a deadlock into a data loss.

14. RTL 9 — What The Boundary Is Costing

  logic [31:0] weighted;      // 16 x 100 needs 23 bits; 16 would silently wrap
  assign total_snoops = {1'b0, n_cross} + {1'b0, n_supp};
  assign weighted     = {16'd0, n_supp} * 32'd100;
  assign suppress_pct = (total_snoops == 17'd0) ? 8'd0
                      : (weighted / {15'd0, total_snoops});
  assign mean_latency = (n_cross == 16'd0) ? 8'd0
                      : ({16'd0, total_latency} / {16'd0, n_cross});

Ten snoops were driven — three crossing at 20, 30 and 40 cycles, and seven suppressed — plus one lossy mapping and one unmappable request. Measured:

  boundary : crossed=3 suppressed=7 (70%) mean latency=30 cycles lossy=1 unmappable=1

Seventy percent of the snoop traffic never touched the link, and the thirty percent that did averaged thirty cycles. Those two numbers together are what a filter is worth: without it all ten crossings cost 30 cycles each for 300 cycles of link occupancy; with it, 90.

The n_lossy and n_unmap counters are the ones nobody thinks to add, and they are the most useful of the four. A rising lossy-mapping count means the workload is repeatedly moving lines whose state has no counterpart — every one of those crossings forcing a writeback that a single-domain system would not have paid. A non-zero unmappable count means software is issuing operations the boundary cannot express, which is a portability finding rather than a performance one.

The width commentary and the empty-sample guard are the same defect classes as in 13.3 and 13.4: the percentage reports zero rather than a hundred before any snoop, and the multiply is done at 32 bits because a 16-bit product wraps above 655 samples.

15. RTL 10 — One Writer, Two Domains

The invariant from 13.1 is unchanged. What is new is that the single writer may be in either domain, and the check has to span both:

  // A conflicting copy on the far side is REVOKED, not merely refused. The
  // grant follows in the next cycle, once the other domain is clear. This is
  // the only thing the boundary adds: the revocation crosses a link.
  assign revoke_far  = near_wants_write && fr_q && (NO_CROSS_CHECK == 0);
  assign revoke_near = far_wants_write  && nr_q && (NO_CROSS_CHECK == 0);
  assign grant_near = near_wants_write && ((NO_CROSS_CHECK != 0) || !fr_q);
  assign grant_far  = far_wants_write  && ((NO_CROSS_CHECK != 0) || !nr_q);
  assign cross_domain_swmr_err = (nw_q && fw_q) || (nw_q && fr_q) || (fw_q && nr_q);

Revoke, do not refuse. A conflicting request is not rejected — the conflicting copy is invalidated and the grant follows. Refusing would be correct and would also mean a device that never gets to write a line the host is reading.

The conflict test reads only the reader flag, which needs justifying rather than assuming:

  // A writer always holds a readable copy, so the reader flag subsumes the
  // writer flag and one test is enough. The invariant that makes that true is
  // checked below rather than assumed.
  assign writer_without_copy_err = (nw_q && !nr_q) || (fw_q && !fr_q);

That is a redundancy removed and replaced by a monitor, which is the right trade: the two-term test was unfalsifiable — the second term could never be the deciding one — and a mutation removing it was provably equivalent until the invariant was made explicit.

Measured across grants, revocations and reads in both directions:

  two domains : near grants=1 far grants=1 revocations=4 | swmr checked=0 unchecked=1
  revocations : near revoked=1 far revoked=1 | near read against a far writer admitted=0

Revocations crossed the boundary in both directions, one grant landed in each domain, and a near read against a far writer was never admitted. The NO_CROSS_CHECK build granted without looking across and produced a writer and a reader simultaneously — the cross-domain SWMR violation, which is the failure the whole boundary exists to prevent.

16. Quantitative Reasoning

What a filter is worth. Measured at 70% suppression and a 30-cycle mean crossing: ten snoops cost 90 cycles of link occupancy filtered against 300 unfiltered, a 3.3× reduction. The filter's storage is one bit per line the far domain may hold; at a 64-byte line that is 0.2% of the tracked capacity. The trade is almost always worth taking, and the only reason not to is that a filter which is wrong in the optimistic direction is worse than no filter at all.

What a lossy mapping costs. A line in the Owned state crossing the boundary must be narrowed, which forces the writeback MOESI existed to defer. At a 64-byte line, every lossy crossing is 64 bytes of write bandwidth plus the memory occupancy. A workload that migrates owned lines across a domain boundary pays the full MESI writeback cost while carrying MOESI's extra state bit — the worst of both, and n_lossy is the counter that reveals it.

Why revocation latency dominates a migration. Revoking a copy on the far side of a CXL link is a round trip, and the grant waits for it. Using the 30-cycle mean crossing from section 14, every ownership migration across the boundary costs at least one full crossing before the writer may proceed — compared with the single-cycle grant a within-domain migration needs. A line ping-ponging across the boundary pays that on every bounce.

Queue depth breaks the cycle, but only with separate channels. Deepening a shared queue postpones the deadlock; it does not remove it, because the cycle is structural. Separate channels with independent flow control remove it at any depth. Measured: with a full request queue, resp_ready was 1 on the separate-channel build and 0 on the shared one.

The bridge's transaction table is sized by the round trip. One entry per outstanding crossing, each holding the near-domain requester identity, the far-domain tag, and the address. At a 30-cycle round trip and one snoop issued every 4 cycles, roughly 8 entries are needed to keep the link busy — which sets the tag width, which sets how many crossings can be outstanding, which sets the achievable bandwidth.

17. Assertions

Presented as SystemVerilog and executed as procedural checkers — see section 19.

A crossing never grants permission.

property p_never_widen;
  @(posedge clk) disable iff (!rst_n)  crossing |-> (dst_perm <= src_perm);
endproperty

A crossing never forgives a debt.

property p_never_forgive;
  @(posedge clk) disable iff (!rst_n)  (crossing && src_duty) |-> dst_duty;
endproperty

A lossy mapping is reported.

property p_lossy_reported;
  @(posedge clk) disable iff (!rst_n)  (map_en && !exact) |-> lossy;
endproperty

Exactly one point of coherence per address.

property p_single_poc;
  @(posedge clk) disable iff (!rst_n)  !(forward && answer_locally);
endproperty

A response matches an outstanding request.

property p_no_orphan_response;
  @(posedge clk) disable iff (!rst_n)  far_resp |-> outstanding;
endproperty

An unmappable semantic request is reported, never approximated.

property p_no_approximation;
  @(posedge clk) disable iff (!rst_n)  (valid && src_op == AT) |-> unmappable_err;
endproperty

A snoop crosses at most once.

property p_no_duplicate_forward;
  @(posedge clk) disable iff (!rst_n)  (snoop_in && busy) |-> !snoop_out;
endproperty

A response returns to the agent that asked.

property p_response_routing;
  @(posedge clk) disable iff (!rst_n)  resp_to |-> (resp_requester == stored_id);
endproperty

A suppressed snoop is for a line the far domain does not hold.

property p_filter_conservative;
  @(posedge clk) disable iff (!rst_n)  suppressed |-> !far_actually_holds;
endproperty

Per-address order survives the crossing.

property p_per_address_order;
  @(posedge clk) disable iff (!rst_n)
    (complete && seen[comp_addr]) |-> (comp_seq >= last_seq[comp_addr]);
endproperty

A full request queue never blocks a response.

property p_no_channel_cycle;
  @(posedge clk) disable iff (!rst_n)  resp_in |-> ##[0:$] resp_ready;
endproperty

One writer across both domains.

property p_cross_domain_swmr;
  @(posedge clk) disable iff (!rst_n)
    !((near_writer && far_writer) || (near_writer && far_reader)
                                  || (far_writer && near_reader));
endproperty

A writer always holds a readable copy.

property p_writer_has_copy;
  @(posedge clk) disable iff (!rst_n)  near_writer |-> near_reader;
endproperty

18. Mutation Testing

74 mutations were injected into the ten models, one at a time, each a single-line change a competent engineer could plausibly write. Every one must make the testbench print RESULT: FAIL.

Representative mutations, all killed:

Fifteen mutations survived the first run. None was patched away.

Eight stimulus gaps. The bench never produced a mapping that widened to the exclusive state, never held a request outstanding across cycles without a response, never forwarded a second snoop, never sent a wrong-tagged response while a snoop was outstanding, never repeated an inversion, never pushed past a full queue, never had a far writer blocking a near write, and never had a near reader blocking a far write. Eight cases added, eight mutations killed.

Four unobserved outputs. The translated opcode, the completion count, the near-read admission against a far writer, and the state produced by the third mapping policy were all computed and never checked. The translated opcode is the instructive one: the bench checked that four requests were mappable and never once checked what they mapped to, so a mutation turning a read-unique into a plain read passed cleanly.

Two unreachable clauses, fixed by adding a third policy. The widening monitor has two clauses — one for each permission a crossing could invent — and no stimulus reached the second, because nothing in the two existing policies mapped anything to the exclusive state. A third policy was added to the same source that maps the owned state to exclusive instead of modified. It is a mistake a real bridge could make, and it is now the only thing that exercises half of the monitor.

One provably equivalent mutation, fixed in the design rather than recorded. The cross-domain conflict test read both the far reader flag and the far writer flag. A writer always holds a readable copy, so the writer term could never be the deciding one, and a mutation removing it changed nothing. The correct response was to remove the redundant term and add the invariant that justifies removing it — writer_without_copy_err — which is a checkable statement where the redundant term was an unfalsifiable assumption. The mutation was then replaced with one that breaks that invariant directly, and killed.

A survivor is a finding. Three of the fifteen here changed the design or the model set rather than the testbench, and all three were improvements independent of the mutation that prompted them.

19. Verification Strategy

The oracle must not be the design. Each testbench models the same behaviour in a structurally different representation.

For state_map the design is a case statement over state encodings. The oracle knows no encodings at all — it holds permission as an order and checks only that the destination is no stronger than the source:

      if      (s==0) strength = 0;   // I  nothing
      else if (s==1) strength = 1;   // S  read
      else if (s==4) strength = 1;   // O  read (plus a duty, which is not a permission)
      else if (s==2) strength = 2;   // E  read+write, clean
      else           strength = 3;   // M  read+write, dirty

Placing O at the same strength as S is the 13.3 result restated: ownership is an obligation, not a permission, and an oracle that treated it as a stronger permission would agree with a widening bug.

For domain_filter the design is a bit vector. The oracle is three plain integers, so a vector-indexing bug cannot reproduce itself in the reference — and a mutation that indexed the filter with the wrong signal was killed by exactly that separation.

For order_across the design holds a per-address array and a global high-water mark. The testbench drives the case that distinguishes them — an address moving forward for itself while lagging the global mark — rather than trusting that the two are different.

Every displayed value is a captured signal. No $display in these benches prints a literal, and values sampled before a later event are latched into named integers first.

Delta-cycle discipline. Every sample of a combinational output is preceded by a settle, because a continuous assignment read in the same delta as its driver changes returns the previous value.

Coverage recorded: 128 assertion sites across three testbenches; all five source states mapped under all three policies; six request types translated including both unmappable kinds; snoops forwarded, duplicated, wrongly tagged and correctly tagged; the filter driven with takes, drops, hits and misses against an independent shadow; per-address inversions driven twice and cross-address reordering driven both when the address was new and when it had been seen; the request queue filled and overfilled; and grants, revocations and reads driven in both directions across the boundary.

20. Synthesis and Implementation Reality

The mapping table is a specification document before it is logic. At the size here it is a case statement. In a real bridge it is a table with an entry per source state and per request type, reviewed against both protocols' specifications, and the review is the expensive part. The RTL is the easy half.

The snoop filter is the bridge's largest structure. One bit per line the far domain may hold, which at a large device memory is a significant array — and it is looked up on every snoop, so it is on the latency path for the crossings it does not suppress. Real filters are approximate and conservative for exactly this reason: an approximate filter that errs towards crossing is correct and merely slower, which is the only direction the safety property permits.

The transaction table is dual-namespace. Each entry holds a near-domain requester identity and a far-domain tag, and both are needed for the response to find its way home. That is not a large structure, but it is written on every crossing and read on every response, and its depth bounds the outstanding crossings and therefore the achievable bandwidth.

Separate channels are a physical commitment, not a configuration. Breaking the dependency cycle means separate queues with independent flow control from the pins inwards. It cannot be added later by making a shared queue deeper, because the cycle is structural rather than a matter of capacity.

Reset must leave the filter empty and the transaction table invalid. A filter that comes out of reset believing the far domain holds lines will send unnecessary snoops, which is merely slow. A transaction table that comes out of reset with valid entries will match a response to a transaction that never existed — which is why orphan_resp_err is a reset check as much as a protocol check.

21. Silicon Observability

Four error signals belong in silicon. widened_err, two_poc_err, false_suppress_err and cross_domain_swmr_err all detect conditions from which no correct behaviour is possible, and all four are a handful of gates over signals that already exist. Each is unreachable in a correct design, so each needs a fault-injection build behind it in the regression before a zero reading means anything.

n_lossy is the counter that explains a performance mystery. A workload whose owned lines migrate across the boundary pays a writeback on every crossing while carrying MOESI's extra state bit — MESI's cost with MOESI's overhead. Nothing else in the system reports that, and it looks like ordinary writeback traffic from every other angle.

n_forwarded minus n_returned should be the crossings currently outstanding. A persistent drift means a transaction was lost at the boundary, and it is silent until something times out — at which point the state that would explain it is gone.

22. Debug Lab

  state map : exact=4 lossy=1 | O narrowed to 1 (S=1); widened to M=1 to E=1

dst_st = S;                       // narrow, never widen
assign widened_err = map_en && ((dst_st == M && src_st != M)
                             || (dst_st == E && src_st != E && src_st != M));

  poc       : forwarded=1 answered=1 two_poc(local build)=1 orphan_resp=1

assign answer_locally = req && !addr_is_far;   // never both
assign two_poc_err    = forward && answer_locally;

  translate : mapped=4 no-counterpart=2 unmappable_err=1 approximated(bad build)=1

assign unmappable_err = valid && !mappable && (src_op == AT);   // not for hints

  forward : forwarded=2 returned=2 dup=1 misrouted(forgetful build)=1 tag=0

assign resp_to        = far_resp && busy_q && (far_resp_tag == tag_q);
assign resp_requester = id_q;                   // the stored near-domain id
assign misrouted_err  = resp_to && (resp_requester != id_q);

  filter  : crossed=2 suppressed=2 false_suppress(optimistic build)=1

assign suppressed = snoop && !far_holds;
assign false_suppress_err = suppressed && far_actually_holds;

  order   : same-addr inversion=1 repeated=1 (permissive build=0) cross-addr reorders=4

assign same_addr_inversion_err = complete && seen_q[comp_addr]
                                 && (comp_seq < last_seq[comp_addr]);
assign cross_addr_reorder      = complete && (comp_seq < last_any_seq);

  channels : separate resp_ready=1 shared resp_ready=0 | deadlock separate=0 shared=1

assign resp_ready = (rs_q < DEPTH);      // independent of the request queue
assign req_ready  = (rq_q < DEPTH);

  two domains : near grants=1 far grants=1 revocations=4 | swmr checked=0 unchecked=1

assign revoke_far = near_wants_write && fr_q;         // revoke, do not refuse
assign grant_near = near_wants_write && !fr_q;        // and grant only after

23. Design Review

What was built. Ten models: a state mapping under three policies, a point-of-coherence bridge with a locally-answering twin, a request translator that distinguishes droppable from semantic, a snoop forwarder with tag matching and a twin that forgets the requester, a snoop filter checked against an independent shadow, an ordering checker that separates per-address from cross-address, the conservative rule stated on two axes, a channel-dependency model with a shared-queue twin, boundary counters, and a two-domain SWMR enforcer with a twin that does not look across.

What was measured. Four exact mappings and one lossy, with both widening policies caught. One forwarded request and one answered locally, never both. Four requests mapped exactly, two without counterparts, and exactly one of those an error. Two snoops crossed with distinct tags and both returned to the right agent. 70% of snoop traffic suppressed, at a 30-cycle mean crossing. A per-address inversion caught twice and four legal cross-address reorderings counted. Three safe crossings and two refused, for two different reasons. A response accepted with a full request queue on separate channels and blocked on a shared one. Four revocations crossing the boundary in both directions, one grant in each domain, and the union invariant intact.

What would be different in production. The mapping tables would be reviewed line by line against two specifications, and that review would be the schedule risk rather than the RTL. The snoop filter would be approximate and compressed. The transaction table would be deeper and would carry addresses. The link layer, credits, and error correction would sit underneath all of it. None of that changes the four rules; all of it multiplies the places they can be broken.

The strongest argument against this design. Narrowing the owned state on every crossing forces a writeback that a within-domain transfer would avoid, so a workload that migrates lines across the boundary pays MESI's cost while carrying MOESI's extra state bit. That argument is correct, and the honest response is that the alternative — carrying the duty across a boundary whose far side has no state for it — means the far domain holds dirty data it does not know it owes. The measurement that decides whether the boundary is in the right place is n_lossy, and if it is high the answer is to move the line's home, not to widen the mapping.

What would be built differently next time. The cross-domain conflict test should have read one flag from the start. It read two, and the second could never be the deciding one — an unfalsifiable term that looked like defensive coding. Replacing it with an explicit invariant made the assumption checkable, and a mutation that broke the invariant was then killed rather than surviving.

24. How This Appears In Real Engineering

In an architecture review, the first question about any coherency bridge is which side serialises each address range. If the answer is anything other than a definite map, the design has two points of coherence waiting to happen.

In a bridge specification review, the mapping tables are the document. Every state and every request type needs an entry, and every entry that is not an exact counterpart needs a stated reason — either "narrowed, and here is the cost" or "no counterpart, and here is what we report."

In a bring-up, n_forwarded minus n_returned and n_lossy are the two counters to watch first. The first finds transactions lost at the boundary; the second explains writeback traffic nobody can otherwise account for.

In a deadlock investigation, the boundary is the first place to look precisely because neither protocol's specification describes it. Two formally deadlock-free protocols joined by a shared queue is the single most common way a system deadlocks in a state nobody has a name for.

In a performance investigation on a CXL system, the snoop suppression rate is the number that decides whether the filter is doing its job. At the measured 70% and a 30-cycle crossing, the filter is worth 3.3× in link occupancy — and a filter that has silently stopped working looks exactly like a fabric that has become slower.

In a portability discussion, n_unmap is a software finding rather than a hardware one. Operations that the boundary cannot express are operations the software should not be issuing across it, and the counter is the only thing that will say so.

25. Common Misconceptions

"CXL and CHI are competitors." They operate at different scopes. A coherent fabric inside an SoC and a coherent link between packages solve different problems, and a real system has both with a boundary in between. The engineering is the boundary.

"A protocol conversion is a lookup table." The table is the easy part. The hard part is the entries that have no exact counterpart, and what the bridge does with them is where correctness is decided. Measured: one of five states and two of six request types had no counterpart.

"If both protocols are correct, the system is correct." Both protocols were deadlock-free and the shared-queue bridge deadlocked anyway. The cycle exists only in the structure joining them.

"A snoop filter is a pure optimisation." It is, in one direction. A filter that under-approximates what the far domain holds suppresses a snoop that had to cross, and the far domain keeps a copy the near domain believes it revoked. That is not slower — it is wrong.

"Approximating an unmappable request is better than failing it." Not when the request is semantic. An atomic turned into a plain read completes successfully and loses updates. A prefetch hint dropped costs nothing. The distinction is the content, not the mechanism.

"Ordering must be preserved across the boundary." Per address, yes — that is the coherence order. Across addresses, no, and a checker that alarms on legal cross-address reordering gets disabled, taking the useful half of the check with it.

"Each domain's SWMR checker covers the system." Each covers its own domain, and both were satisfied while a host and a device wrote the same line. The violation exists only in the union.

"The Owned state carries across a boundary." Only if the far domain has a state for it. Where it does not, the crossing must narrow and write back — which is the cost of the boundary, measured as n_lossy, and it is the reason a frequently-migrating line loses everything the Owned state was for.

26. Interview Reasoning

27. Exercises

1. Calculation. A boundary sees 10,000 snoops with a 30-cycle crossing and a filter suppressing 70%. Compute the link occupancy saved, the filter storage for a 4 GB device memory at 64-byte lines, and the break-even suppression rate if storage costs 2% of the area budget.

2. Analysis. A system reports n_lossy rising steadily while overall throughput is flat. State what that implies about the workload's line migration pattern, what it is costing in writeback bandwidth at 64-byte lines, and what change would reduce it.

3. RTL task. Extend state_map to a target vocabulary that has a fifth state meaning "shared, clean, and I will answer reads." State which mappings become exact, which remain lossy, and what new safety check is required.

4. Assertion task. Write the property proving a crossing never grants permission. Then explain why it passes trivially on a design where source and destination use the same encoding, and what stimulus makes it meaningful.

5. Design task. Add a second bridge for a different address range. State what must be true about the address-to-bridge map, and the failure that becomes possible if one address can reach both.

6. Testbench design. Design the stimulus that distinguishes identity matching from arrival matching at a boundary. Explain why a response arriving with nothing outstanding passes on both, and state the minimum stimulus that separates them.

7. Debug task. A device continues serving reads from a line the host invalidated. The snoop filter reports normal operation. Give your investigation order and name the independent record required to check the filter at all.

8. Design review. A colleague proposes that the bridge answer requests it can satisfy from its own directory, to save a link round trip. Give the strongest version of that argument, then the condition under which it is safe, and the monitor that detects the case where it is not.

28. Summary

A boundary translates, and translation is lossy.

• Two vocabularies, not a bijection. Four of five states mapped exactly; the fifth had no counterpart. Both ways of widening it were caught by one monitor, and they are different mistakes: one grants write permission on dirty data, the other additionally skips the writeback.
• Weaken, never grant. Permission may only shrink and obligation may only grow. Measured: 3 safe crossings, 2 refused — one for gaining permission, one for forgiving a debt.
• Exactly one point of coherence per address. The correct bridge forwarded a far-serialised address and did not answer it; the build that did both was caught. Two serialisation points for one address is no serialisation point at all.
• Droppable is not the same as unmappable. 4 requests mapped exactly, 2 had no counterpart, and exactly 1 of those was an error. A dropped hint costs performance; an approximated atomic loses updates while every access stays individually correct.
• A snoop crosses once and comes home. Two crossings with distinct tags, both returned to the agent that asked; the build that forgot the requester delivered its response on time to the wrong agent, with nothing reporting a loss.
• Most snoops never cross. 70% suppressed at a 30-cycle mean crossing — 90 cycles of link occupancy against 300. The filter may over-approximate what the far domain holds and must never under-approximate.
• Per-address order survives; cross-address order need not. One inversion caught, caught again on repeat, and 4 legal cross-address reorderings counted rather than flagged.
• The boundary can deadlock where neither protocol can. With a full request queue, resp_ready was 1 on separate channels and 0 on a shared one. Depth postpones the cycle; separate flow control removes it.
• One writer, two domains. 4 revocations crossed the boundary in both directions with the union invariant intact; the build that did not look across granted immediately and had a writer and a reader from that cycle onwards, permanently.
• Verification: 128 assertion sites, 74 of 74 mutations killed, zero surviving. Fifteen first-run escapes were eight stimulus gaps, four unobserved outputs, two unreachable monitor clauses fixed by adding a third mapping policy, and one provably equivalent mutation fixed by removing a redundant term and replacing it with the invariant that justified removing it.

Module 13 is complete. Coherency began as a permission model, acquired duration, then an owner, then a state space, and finally a boundary. Module 14 walks concrete flows through all of it — the actual sequences of messages by which a host reads a line a device has modified, and an ownership transfer completes end to end.