Device-Type Selection Discipline

10.1, 10.2 and 10.3 built the three device types and showed what each obliges. This chapter closes Module 10 with the question those three raise and none of them answers.

It is not which type should I build. 6.4 and 6.5 answered that from requirements, before any silicon existed. This is the question that appears after the answer:

What is this device when part of it is turned off?

1. The Engineering Problem — A Device That Ships as Four Devices

A team builds a Type 2 accelerator. It is verified as a Type 2, characterised as a Type 2, and documented as a Type 2.

Then a platform ships it with .mem disabled, because that platform has no use for the device's memory and the firmware team saw a way to save a configuration step. Nobody made a decision; a bit was left clear.

That configuration is a different device. It behaves as a Type 1 — the cache engine is still present, still holding host lines, still carrying every eviction obligation from 10.1. It was never verified in that mode, its obligations were never checked in that mode, and its telemetry attributes all of its uptime to a type it is not currently being.

The device did not fail. It was correct as a Type 2 and is now running as something nobody tested.

2. The One-Sentence Model

You do not select a device type once; you select every mode the device can enter. A device with two optional engines is four devices, each with a distinct effective type and a distinct set of obligations — and the ones nobody chose are the ones nobody verified.

Call it the mode space. The discipline is not choosing well at the start. It is knowing what you have chosen, in every configuration the device can reach.

3. What This Chapter Owns

This is the fourth chapter in this curriculum to touch selection, so the boundaries need stating precisely.

6.5 established that three states must stay distinct — what silicon contains, what the link negotiated, what the platform enabled. It made that a discipline. This chapter makes it hardware, and then asks the question that follows from it: if those three can differ, the device has a space of configurations, and every point in it is a device somebody must have verified.

4. Four Devices, One Die

Architectural. The arrows are configuration relationships, not signals.

Only one of those four boxes is usually verified. The device was designed as a Type 2, so the "both" mode got the test plan, the characterisation and the documentation. The other three are reachable, are different devices, and were reached for the first time in a customer's rack.

5. Teaching-model boundary

6. RTL 1 — A Two-Engine Device Is Four Devices

  // Mode index: {mem_en, cache_en}. Only combinations the silicon supports
  // are reachable at all.
  wire [1:0] mode = {mem_en, cache_en};
  assign reachable_modes = ONLY_SHIPPED ? 3'd1
                         : (HAS_CACHE && HAS_MEM) ? 3'd4
                         : (HAS_CACHE || HAS_MEM) ? 3'd2 : 3'd1;

=== EXP1: a two-engine device is FOUR devices ===
  reachable modes : both engines=4 cache only=2 mem only=2
  silicon with both engines can enter four modes           : ok
  neither enabled: io-only, not a CXL device type          : ok
  cache only: it BEHAVES as Type 1                         : ok
  memory only: it BEHAVES as Type 3                        : ok
  both: Type 2                                             : ok
  visited=1111 changes=3 coverage complete=1
  all four modes were entered                              : ok
  5 steady cycles in one mode : changes went 3 -> 4
  a steady mode added exactly one change, not one per cycle : ok
  same enables applied to single-engine silicon : cache-only flag=1 mem-only flag=1
  both single-engine devices caught being asked for an impossible mode : ok

Four modes, and the middle two are the interesting ones. A Type 2 running with .mem off is not a Type 1 — it behaves as one, which is a different and more dangerous statement. Its silicon still contains a memory engine; only its obligations have changed.

Note the last line. The same platform request — enable both — was applied to three different silicon configurations. It is legal for the two-engine device and illegal for both single-engine devices, and the checker caught each of them being asked for a mode it cannot support. That is one enable sequence and three different correct answers, which is exactly why a single as-shipped test proves so little.

Coverage is status, not a violation

The first version of this module latched an error when a reachable mode had not yet been entered — and it fired immediately, because at reset no mode has been entered. That is a coverage property, not a safety property, and expressing it as an error made a correct device fail its own regression from the first cycle.

The corrected design splits them:

      // Entering a mode this silicon cannot support is a real violation;
      // not having entered one YET is merely coverage, and is reported as
      // status rather than latched as an error.
      if (!all_modes[mode]) unreachable_mode_err <= 1'b1;

coverage_complete became a status output the testbench checks at the end. Confusing a coverage goal with a safety property is the same category error as 9.6's warning about performance goals in assertions — and it produces the same outcome, a team that learns to ignore a failing check.

7. RTL 2 — Negotiation Reduces, and Can Never Add

  // Each stage is an intersection, never a union.
  assign negotiated = NEGOTIATE_UP ? link_offers : (link_offers & CONTAINS);
  assign enabled    = platform_wants & negotiated;

=== EXP2: negotiation reduces, and can never add ===
  contains 11, link offers 11, platform wants 11 : negotiated=11 enabled=11
  contains 01 (cache only), link offers 11        : negotiated=01 enabled=01 | up-variant negotiated=11
  negotiation intersected with what the silicon contains   : ok
  the negotiate-up variant granted memory it does not have : ok
  and was caught adding a capability                       : ok
  platform wants 01 only : enabled=01
  the platform reduced it further                          : ok

6.5's three states, as hardware. Each stage is an intersection: silicon is a ceiling, negotiation may only reduce it, enablement may only reduce that again.

The NEGOTIATE_UP variant is the failure worth naming, because it is the shape a real bug takes. Nobody writes "grant capabilities we do not have"; they write a union instead of an intersection, or they take the link's offer as authoritative because the link is the thing doing the negotiating. The result is a device advertising a memory engine it does not contain, which is 10.1's declared-type defect arriving through a different door.

The monotonic property is what makes this checkable in one line: at no stage may a capability appear that the previous stage lacked.

Each arrow narrows the set; none of them may widen it. The failure in the last two rows is never written deliberately — it appears as a union where an intersection belonged, or as treating the link's offer as authoritative because the link is the thing doing the negotiating.

8. RTL 3 — Turning a Protocol Off Is Not the Inverse of Turning It On

  wire       quiesced = (held_lines == 8'd0);
  assign disable_done = draining_q && (DISABLE_IMMEDIATE || quiesced);

=== EXP3: turning a protocol off is not the inverse of turning it on ===
  disable requested, 3 lines still held : done=0 protocol on=1 wait=4 | immediate on=0
  the protocol is still on and the disable has not completed : ok
  it has been quiescing for exactly 4 cycles               : ok
  the immediate variant switched the protocol off at once  : ok
  and was caught disabling while it still held lines       : ok
  quiesced : protocol on=0 max quiesce wait=4
  the protocol went off only after the lines were returned : ok

Enabling a protocol is a bit. Disabling one is a sequence.

The asymmetry is total and it is the most-missed fact in this chapter. Enabling .cache gives the device permission to start holding host lines — nothing is owed to anyone at that moment. Disabling .cache while it holds three modified lines destroys the only copy of that data, exactly as 10.1's silent eviction does, but at configuration time where nobody is looking for it.

This is the third appearance of the same structure in this batch — 9.6's fence, 10.2's ownership handover, and now a protocol disable. All three are barriers whose cost is the state they must drain, and all three have a fast, wrong variant that skips the drain.

9. Waveform — Quiesce, Then Disable, Then Clear

Teaching-model timing derived from the simplified RTL in this chapter. Not CXL wire timing.

Three cycles separate the request from the effect, and the ordering is the lesson. disable_req pulses at c4 and protocol_on is still high through c7. The lines are returned at c7, the disable completes, the protocol goes off at c8, and only at c9 do the state entries clear.

Every one of those steps is required and they cannot be reordered. Clearing the state before quiescing loses it; disabling before quiescing loses it; leaving the state after disabling is §10's defect. A configuration write that appears instantaneous to software is a multi-cycle obligation in hardware.

10. RTL 4 — State Must Not Outlive Its Protocol

      if (falling && CLEAR_ON_DISABLE) entries_q <= 8'd0;
      else if (install && proto_en)    entries_q <= entries_q + 8'd1;
      ...
      if (probe_hit && !proto_en) begin
        n_residual_hit_q <= n_residual_hit_q + 16'd1;
        residual_err     <= 1'b1;
      end

=== EXP4: state must not outlive the protocol it belongs to ===
  protocol on, 3 entries installed : entries=3 present=1
  protocol off : correct entries=0 | leave-behind variant entries=3
  the correct design cleared its state on disable          : ok
  the leave-behind variant kept all three                  : ok
  probe while protocol off : correct hit=0 | variant hit=1 residual flag=1
  the variant answered from state belonging to a disabled protocol : ok
  install attempted while protocol off : entries=0
  no state was recorded while the protocol was disabled    : ok

Residual state is the defect that makes a disabled protocol act enabled — once, at the worst possible moment.

The engine is off. Software believes it is off. Then something consults a table that still has entries in it, gets a hit, and the device behaves as though the protocol were running. It happens exactly once per stale entry, it is not reproducible without recreating the enable/disable history, and it looks like a completely unrelated fault.

Both directions matter and only one is obvious. Clearing on disable is the one people implement. Refusing to install while the protocol is off is the one they forget, and it produces the same stale entries by the other route.

11. RTL 5 — Obligations Follow the Mode, Not the Silicon

This is the chapter's central mechanism, and the one that would have prevented §1's scenario.

  wire [1:0] sel = USE_SILICON ? SILICON_TYPE : effective_type;
  // Type 1 must notify evictions and refuse host memory.
  // Type 2 must notify evictions and check permission on its own memory.
  // Type 3 must do neither -- it has no cache at all.
  assign obligations = (sel == 2'd1) ? 3'b011 :
                       (sel == 2'd2) ? 3'b101 :
                       (sel == 2'd3) ? 3'b000 : 3'b000;

=== EXP5: obligations come from the CURRENT mode, not the silicon ===
  effective Type 2 : obligations=101 (permission-check, refuse-mem, evict-notify)
  effective Type 1 : obligations=011
  a Type 1 must refuse host memory and notify evictions    : ok
  effective Type 3 : obligations=000
  a Type 3 has neither obligation -- it has no cache       : ok
  degraded to Type 1, host memory SERVED : correct flag=1 | silicon-typed flag=0
  the mode-driven matrix caught the missed obligation      : ok
  the silicon-typed variant did not even look for it       : ok
  eviction with NO notification, effective Type 1 : flag=1

Read the obligation sets: they are not nested. A Type 1 must refuse host-memory accesses and a Type 2 must not — a Type 2 serves them. So a Type 2 degraded to Type 1 acquires an obligation it did not have when it was verified, and the correct behaviour in one mode is a violation in the other.

That is why "we tested the superset" is wrong here. There is no superset. The modes have overlapping but distinct obligation sets, and testing the richest configuration does not cover the poorer ones.

The USE_SILICON variant is §1's bug, in nine characters. It selects obligations from the silicon's type rather than the current mode, so a degraded Type 2 is still checked as a Type 2 — and the missed refusal is not merely unreported, it is not looked for. The correct matrix caught it; the silicon-typed one had no opinion.

12. RTL 6 — Choosing a Type Is Choosing a Verification Surface

=== EXP6: choosing a type is choosing a verification surface ===
  single-engine device : modes=2 crosses=0 cost=6 additive=6 gap=0
  two-engine device    : modes=4 crosses=4 cost=28 additive=12 gap=16 | ignore-cross cost=12
  four modes and four interactions cost 28                 : ok
  16 of that is interaction the additive view cannot see   : ok
  the additive variant reports 12 -- less than half        : ok

Six versus twenty-eight, and the additive view sees twelve. More than half the verification surface of a two-engine device is interaction that neither engine's own plan contains — 10.2 named the four crosses concretely: local access against host-holds, both directions pending, a handover with work in flight, and an identity number live in both roles.

This refines 6.5's cost model rather than repeating it. 6.5 priced protocols pre-silicon and found a 9-unit interaction term on 41. This prices modes and their crosses, which is the post-silicon surface, and finds the interaction is the majority of it. The two agree on the shape and disagree on the magnitude for a good reason: 6.5 counted the engines, and this counts the configurations they can be in.

13. RTL 7 — How Long Was It Each Thing?

=== EXP7: how long was it each thing? ===
  time as type1=15 type2=10 type3=15 changes=2 active=40
  oracle: type1=15 type2=10 type3=15 changes=2
  time in each effective type matched an independent oracle : ok
  the device really did spend time as something other than Type 2 : ok
  as-shipped variant : type2 time=40 type1 time=0
  the as-shipped variant attributed everything to Type 2   : ok

The device spent 25 of 40 cycles as something other than what it shipped as, and the as-shipped variant reports 40 out of 40 as Type 2.

That variant is not a strawman — it is what almost every device does, because telemetry is written once, against the device's nameplate type. A field investigation using it will attribute every failure to the wrong configuration, and the mode the device was actually in when it failed does not appear anywhere in the data.

Time-in-mode is the counter that makes a degraded configuration visible from the field. Without it, the only evidence that a device ever ran as something else is the absence of an explanation.

14. Quantitative Reasoning

Illustrative, with stated assumptions and teaching units.

The mode space grows exponentially

modes = 2 ^ (optional engines)

Two engines is four devices. The exponent is what makes this worth a chapter: the design added one engine and doubled the number of devices somebody has to verify.

What the surface actually costs

Using §12's teaching units of 3 per mode and 4 per cross:

one engine  : 2 modes x 3 + 0 crosses x 4 =  6
two engines : 4 modes x 3 + 4 crosses x 4 = 28

A 4.7× increase in verification surface for one additional engine, of which 16 of 28 — 57% — is interaction that neither engine's plan covers. An additive estimate gives 12 and is wrong by more than a factor of two, always in the optimistic direction.

The cost of an unverified mode

If a two-engine device verifies only its as-shipped mode, it has covered 1 of 4 modes and 0 of 4 crosses:

covered   :  3 of 28 units = 11%
unverified: 25 of 28 units = 89%

That is the honest number behind §1. The device was not lightly tested; it was thoroughly tested in one of four configurations, and the configuration a customer selected was among the other three.

What a disable costs

From §8, the quiesce took 4 cycles for 3 held lines. Scaled with 9.6's 125-outstanding figure, disabling a protocol at full occupancy costs roughly a full round trip during which the device serves nothing — and unlike a fence, it happens under a configuration write that software expects to be instantaneous.

A disable is not a register write; it is a barrier with a register write at the end of it.

15. Assertions

Icarus Verilog 13.0 does not support concurrent SVA here, so every property is synthesisable checker logic verified in simulation. 53 assertions.

Safety

Liveness

Coverage — status, not assertions

The third table is the one this chapter argues about. These are goals, reported as status and checked at end of test — not latched errors. Expressing "a mode has not been entered yet" as a violation makes a correct device fail from its first cycle, and §6 describes exactly that mistake being made and corrected.

16. Mutation Testing

Twenty-six mutations. Twenty-six killed.

The first run scored 21 of 26, and one escape taught something the previous three chapters had not.

A mutation that escaped by coincidence

Inverting the mode-change condition from != to == should be trivially detectable. It escaped — and when I ran it in isolation, the mutated design reported exactly the same count as the correct one, 3.

It was not equivalent; the two designs count entirely different things. My stimulus happened to produce the same total from both. A single number matched by accident, and the assertion could not tell the difference.

The fix was a stimulus that makes the two diverge structurally rather than numerically — hold one mode steady and assert the counter adds exactly one:

    // Hold one mode steady: a change counter must count TRANSITIONS, so a
    // steady mode must add exactly one (the transition into it) and no more.
    nc_before = ms_nc;
    ms_ce=0; ms_me=0; repeat(5) step;
    chk((ms_nc - nc_before) == 16'd1, "a steady mode added exactly one change, not one per cycle");

The general lesson is uncomfortable: a passing assertion on a mutated design is not always evidence the assertion is weak. Sometimes it is evidence the stimulus produced a coincidence, and the only defence is a test whose result differs by construction rather than by arithmetic.

The other four

One flag was already set by an earlier violation. The missed-eviction mutation escaped because the missed-refusal test — a different obligation entirely — had already latched the same instance's error flag. Splitting it onto its own instance fixed it, and the lesson generalises: a shared sticky flag makes every check after the first one vacuous.

Two were untested paths: installing state while the protocol is off, and holding a mode steady.

One law was unreachable by construction, and the honest fix was to make it reachable rather than to delete it — an ATTRIBUTE_ALWAYS parameter used only on an abuse instance, which attributes time on every cycle while activity is asserted on only some.

17. Verification Plan

The coverage cross is mode × transition direction × state held: four modes, entering and leaving, with and without outstanding state. The leaving a mode with state held points are where every defect in this chapter lives, and none of them is reachable by a test that configures the device once at boot.

18. Silicon Observability

The first row is the one this chapter exists to argue for. A device that reports only its nameplate type produces field data in which a degraded configuration is invisible, and every failure in it is attributed to a configuration the device was not in.

modes_entered from the field is the counter nobody builds and everybody needs. It answers a question no lab can: which of the configurations you shipped are customers actually using? If three of four modes are in use and one of four was verified, that is a fact worth having before the escalation rather than after.

19. Debug Lab

// test plan: configure both engines, run the Type 2 suite

  reachable modes : both engines=4 cache only=2 mem only=2
  all four modes were entered                              : ok

assign negotiated = link_offers;   // the link decides

  contains 01 (cache only), link offers 11 : negotiated=01 | up-variant negotiated=11
  the negotiate-up variant granted memory it does not have : ok
  and was caught adding a capability                       : ok

assign negotiated = link_offers & CONTAINS;
assign enabled    = platform_wants & negotiated;

if (disable_req) proto_on_q <= 1'b0;   // it's a config bit

  disable requested, 3 lines still held : done=0 protocol on=1 wait=4 | immediate on=0
  the immediate variant switched the protocol off at once  : ok
  and was caught disabling while it still held lines       : ok

wire quiesced       = (held_lines == 8'd0);
assign disable_done = draining_q && quiesced;
if (disable_done && !quiesced) disabled_dirty_err <= 1'b1;

// protocol disabled -- stop using the table, no need to clear it

  probe while protocol off : correct hit=0 | variant hit=1 residual flag=1
  the variant answered from state belonging to a disabled protocol : ok
  install attempted while protocol off : entries=0

if (falling && CLEAR_ON_DISABLE) entries_q <= 8'd0;
else if (install && proto_en)    entries_q <= entries_q + 8'd1;
if (probe_hit && !proto_en) residual_err <= 1'b1;

wire [1:0] sel = SILICON_TYPE;   // we're a Type 2 device

  degraded to Type 1, host memory SERVED : correct flag=1 | silicon-typed flag=0
  the mode-driven matrix caught the missed obligation      : ok
  the silicon-typed variant did not even look for it       : ok

wire [1:0] sel = effective_type;

// this is a Type 2 device
time_as_type2_q <= time_as_type2_q + 1;

  time as type1=15 type2=10 type3=15 changes=2 active=40
  as-shipped variant : type2 time=40 type1 time=0
  the as-shipped variant attributed everything to Type 2   : ok

time_in_type_q[effective_type] <= time_in_type_q[effective_type] + 16'd1;

// effort = cache plan + memory plan
assign total_cost = additive_cost;

  two-engine device : modes=4 crosses=4 cost=28 additive=12 gap=16
  16 of that is interaction the additive view cannot see   : ok
  the additive variant reports 12 -- less than half        : ok

assign total_cost = modes * MODE_COST + crosses * CROSS_COST;
if ((crosses != 0) && (total_cost == additive_cost)) understated_err <= 1'b1;

if ((visited_q | ~all_modes) != 4'hF) unvisited_shipped_err <= 1'b1;

  visited=1111 changes=3 coverage complete=1
  every reachable mode was entered -- coverage is complete : ok

assign coverage_complete = ((visited_q | ~all_modes) == 4'hF);   // status
if (!all_modes[mode]) unreachable_mode_err <= 1'b1;              // safety

20. Design Review

1. How many modes can this silicon enter, and which are verified?
2. Is the effective type derived from the enable state, or stored?
3. Can any stage grant a capability the previous stage lacked?
4. What must quiesce before each protocol can be disabled?
5. What is the worst-case quiesce time, and what waits on it?
6. Are disabled engines' structures empty, and can anything install into them?
7. Are obligations selected by current mode or by silicon type?
8. Which obligations differ between the modes this device can enter?
9. How many pairwise interactions does this device have, and are they in the plan?
10. Does telemetry report the current effective type or the nameplate?
11. Which checks are safety, which are coverage, and which are performance goals?

21. How This Appears in Real Engineering

Architecture. The mode count is 2^optional_engines, and it is a required output of the type decision rather than an afterthought.

RTL. Effective type derived, negotiation as intersection, quiesce before disable, and no structure that outlives its protocol.

DV. The plan is indexed by mode, not by device. The crosses are enumerated explicitly, and an empty cross list on a two-engine device is a finding.

Firmware. Every enable combination it can produce is a device somebody must have verified — and a disable is a sequence with a wait, not a register write.

Post-silicon. Time-in-mode and modes-entered are the two counters that make field configurations visible; without them a degraded device is indistinguishable from a nominal one in the data.

Programme management. The verification surface is modes times cost plus crosses times cost. The additive estimate is optimistic by more than half.

22. Common Misconceptions

23. Interview Reasoning

24. Exercises

1. Calculation. A device has three optional engines. Compute the number of reachable modes and the number of pairwise interactions. Using §12's units of 3 per mode and 4 per cross, compute the total surface and the fraction an additive estimate would miss.

2. Analysis. A fleet reports every device operating as its nameplate type 100% of the time, and failures correlate with nothing. Explain what that data cannot distinguish, name the two counters that would resolve it, and state what you would expect them to show.

3. RTL task. Extend quiesce_gate to handle two independent protocols with separate held-state counts, where either may be disabled while the other stays on. State the new invariant this creates, and the failure mode if one protocol's quiesce is allowed to observe the other's state.

4. Assertion task. Write the property that proves capability negotiation is monotonic across all three stages. Then explain why testing it only on fully-populated silicon leaves it unverified, and what silicon configuration the test actually needs.

5. Waveform analysis. Using §9's trace, identify the exact cycles of each phase — request, quiesce, disable, clear — and state what would go wrong if the clear happened one cycle earlier. Then describe what the trace would look like if the held count never reached zero, and which counter would report it.

6. Debug task. A device behaves correctly for months, then exhibits a single unexplained coherence event immediately after a reconfiguration, and never repeats it. Give your investigation order across this chapter's five alarms, and the single test that reproduces it deterministically.

7. Design review. A colleague proposes shipping a Type 2 device with a firmware option to disable .mem, arguing it adds flexibility at zero hardware cost. Give the strongest version of that argument, then state what it commits the programme to in verification surface, what obligations change in the degraded mode, and what telemetry must exist before it can be supported in the field.

25. Summary

You do not select a device type once; you select every mode the device can enter.

• A device with two optional engines is four devices — 2^optional_engines — each with a distinct effective type and a distinct obligation set.
• The obligation sets are not nested. A Type 1 must refuse host-memory accesses and a Type 2 must serve them, so "we tested the superset" is not available.
• Negotiation reduces and can never add. Silicon is a ceiling, negotiation intersects it, enablement intersects that — and the monotonic property is one line to assert.
• Enabling is a bit; disabling is a barrier. The measured quiesce took 4 cycles for 3 held lines, and disabling without it destroys data under a configuration write nobody watches.
• State must not outlive its protocol — in both directions. Clear on disable and refuse to install while off, or a disabled engine answers once, at the worst moment.
• Obligations follow the current mode, not the silicon type. The silicon-typed variant did not merely tolerate a violation; it never looked for one.
• 57% of a two-engine device's verification surface is interaction — 16 units of 28 — and an additive estimate is optimistic by more than half.
• Verifying only the as-shipped mode covers about 11% of that surface.
• Telemetry must report the current effective type. The device spent 25 of 40 cycles as something other than its nameplate, and the as-shipped counter reported 40 of 40.
• Verification: 26 of 26 mutations killed, 53 assertions. One mutation escaped by coincidence — a mutated counter that happened to produce the same number — and one escaped because a shared sticky flag had already been set by an unrelated violation. Both required fixing the stimulus, not the checker. And the first version of the mode tracker latched a coverage goal as a safety error, failing a correct device from its first cycle.

Module 10 — CXL Device Types is complete. 10.1 built the borrower, 10.3 the lender, 10.2 the device that is both and pays for it, and this chapter the discipline of knowing which one you are running at any moment.

Next: Module 11 — Memory Expansion, which turns from the device class to the system it exists to build, beginning with why a socket runs out of memory before it runs out of work.