Default State

Chapter 8.2 left the device powered, ready, and visible. Its own initiative is spent. The host now acts, and its first action is the one this chapter is about.

Default is the state a bus reset produces, and it has a property no other state has:

Default is reachable from everywhere. Every other state is entered from exactly one place by exactly one event. Default is entered from all of them, by an event the host can generate at any moment without the device's cooperation and without knowing what state the device is in.

That single edge is why a USB device is recoverable from any condition, and it is why Chapter 6.6 could say enumeration needs exactly one error-recovery path.

This is also where the module's state machine gets built.

1. What Default Means

A device is in Default after a bus reset has completed. It responds to the default address (Chapter 6.3 §1), it has no assigned address, and it has no configuration.

What is legal? Control communication at the default address. That is enough for the host to interrogate it and assign it an identity, and it is deliberately not enough for anything else.

What is guaranteed? That the device's protocol-visible state has defined values — not the values it had, but the values the specification says it must have. That guarantee is the entire content of the state, and §5 is about what it costs to provide.

How is it entered? By a bus reset, from any state.

How is it left? Upward by an address commit (Chapter 6.3), producing Address. Downward by losing power or being disconnected. And back into itself, by another bus reset.

2. The State Machine

Here is the module's state machine, assembled from the states established so far and the two Module 6 developed.

Read the edges by who causes them.

The pattern is the chapter's structural point. Every transition that adds protocol identity requires the device to do something correctly. Every transition that removes it requires nothing. A device can always be stripped of state and never be given state without participating — which is exactly the property a recovery mechanism needs.

3. Events Are Not States

A distinction that shapes the RTL, and one engineers get wrong in a specific, recognisable way.

Address is a state. It persists. A device is in it for as long as nothing removes it.

An address commit is an event. It happens at one moment and is then over.

The confusion produces a specific defect: treating a request as though it were a state — holding a set_address_in_progress flag that behaves like a state, or worse, moving the state machine when a request arrives rather than when it completes. Chapter 6.3 measured the second of those: committing on receipt breaks the very transfer that carries the request, with a failure signature so distinctive it is nearly diagnostic.

So the rule for this module's RTL: the state machine consumes events, which are single-cycle, already-qualified, and already-committed. Whatever decides that a transfer completed correctly lives elsewhere — Chapter 6.3 built it, and Module 13 owns the transfer mechanics beneath it.

That separation is why the state machine in §4 is small. It is not doing less than a real controller does; it is doing the one job that is genuinely the state machine's, and consuming the results of the jobs that are not.

4. The Device State Machine, as RTL

// ─────────────────────────────────────────────────────────────────────────
// usb_device_state
//
// Classification: SIMPLIFIED SYNTHESIZABLE TEACHING RTL. It models the
// protocol state machine of section 2 and the architectural state that must
// agree with it -- and deliberately nothing else.
//
// WHAT IT MODELS. The five wired states, the events that move between them,
// event PRIORITY when several arrive together (section 5), and the reset
// cleanup that makes the resulting state honest rather than merely named
// (section 6).
//
// WHAT IT DOES NOT MODEL. Anything that DECIDES an event occurred: transfer
// completion (Chapter 6.3 and Module 13), reset detection (Chapter 3.7),
// attach debounce (Chapter 6.1), the pull-up (Chapter 8.2). Nor endpoints
// (Module 9), packets (Modules 11-12), descriptors (Module 7), or suspend
// (Chapter 8.6 adds it as an overlay rather than a sixth peer state).
//
// ARCHITECTURAL NOTE. This block is NOT the controller. It is the small
// authoritative abstraction that gates the controller -- Chapter 8.1
// section 3's point. Everything here is a few registers and a case
// statement precisely because the hard work belongs to other blocks.
// ─────────────────────────────────────────────────────────────────────────
module usb_device_state
  import usb_state_pkg::*;
(
  input  logic clk,
  input  logic rst_n,               // LOCAL hardware reset -- not a bus reset

  // ── Physical domain (Chapter 8.1) ─────────────────────────────────────
  input  logic phys_connected,      // debounced
  input  logic phys_powered,        // operating power present

  // ── Protocol events. Each is a single-cycle, ALREADY-QUALIFIED pulse.
  // "Qualified" means the transfer that carried the request completed
  // correctly -- section 3, and Chapter 6.3 built the block that decides it.
  input  logic       bus_reset,     // LEVEL while asserted (Chapter 6.2)
  input  logic       addr_commit,
  input  logic [6:0] addr_value,
  input  logic       config_commit,
  input  logic [7:0] config_value,  // zero is an un-select (Chapter 6.5)

  // ── Authoritative protocol state, and the registers that must agree ──
  output usb_dev_state_e dev_state,
  output logic [6:0]     active_addr,
  output logic [7:0]     active_config,

  // ── Derived, not stored. Chapter 8.5 develops why this matters.
  output logic           function_eps_enabled,

  // ── A 1-cycle pulse on any state change, for status and debug.
  output logic           state_changed
);

  usb_dev_state_e next_state;

  // Derived rather than registered: two registers that must always agree
  // are two registers that eventually will not. Chapter 8.5 measures it.
  assign function_eps_enabled = (dev_state == DEV_CONFIGURED);

  // ── Next-state logic ────────────────────────────────────────────────────
  always_comb begin
    // Deterministic default: hold. Every arm below must therefore state a
    // change explicitly, and no path can leave next_state unassigned.
    next_state = dev_state;

    // ── PRIORITY, highest first. Section 5 argues the ordering. ─────────
    if (!phys_connected || !phys_powered) begin
      // Physical loss dominates everything. A device that is unplugged or
      // unpowered has no protocol state, whatever else arrived this cycle.
      //
      // if/else rather than a ternary: a conditional between two enum
      // literals is not directly assignable to an enum-typed target without
      // an explicit cast, and the cast obscures the intent.
      if (phys_connected) next_state = DEV_ATTACHED;
      else                next_state = DEV_NOTATTACHED;
    end
    else if (bus_reset) begin
      // The unconditional edge of section 1: reset reaches Default from
      // ANY state, so this arm deliberately has no antecedent on dev_state.
      // The moment a reset arm needs to know where the device was, reset
      // has stopped being unconditional (Chapter 6.6 section 5 reached the
      // same conclusion about writing the property).
      next_state = DEV_DEFAULT;
    end
    else begin
      unique case (dev_state)

        DEV_NOTATTACHED:
          next_state = DEV_ATTACHED;          // guarded by the branch above

        DEV_ATTACHED:
          if (phys_powered) next_state = DEV_POWERED;

        DEV_POWERED:
          // No arm for addr_commit or config_commit. A device that has not
          // been reset has no business accepting either, and the ABSENCE of
          // those arms is what enforces it -- section 7's first mutation
          // adds one and measures the result.
          ;

        DEV_DEFAULT:
          // The default address is not an assignment (Chapter 6.3 section 2),
          // so committing it must not move the device to Address.
          if (addr_commit && (addr_value != USB_DEFAULT_ADDR))
            next_state = DEV_ADDRESS;

        DEV_ADDRESS:
          if (config_commit && (config_value != USB_NO_CONFIG))
            next_state = DEV_CONFIGURED;

        DEV_CONFIGURED:
          // Chapter 6.5's un-select: the VALUE decides, not the request.
          if (config_commit && (config_value == USB_NO_CONFIG))
            next_state = DEV_ADDRESS;

        default:
          // Illegal encoding. Recover to a state that is always safe rather
          // than holding -- an FSM that can be stuck in an illegal state is
          // an FSM a single upset can disable permanently.
          next_state = DEV_NOTATTACHED;
      endcase
    end
  end

  // ── State and the architectural registers that must agree with it ───────
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      dev_state     <= DEV_NOTATTACHED;
      active_addr   <= USB_DEFAULT_ADDR;
      active_config <= USB_NO_CONFIG;
      state_changed <= 1'b0;
    end else begin
      dev_state     <= next_state;
      state_changed <= (next_state != dev_state);

      // ── SECTION 6'S POINT. Reset does not merely move the state enum;
      // it must return every protocol-visible register to its defined
      // value. Clearing the enum alone leaves a device that CLAIMS Default
      // while holding an address from before the reset -- which section 7
      // measures passing every check written about the state machine.
      if (!phys_connected || !phys_powered || bus_reset) begin
        active_addr   <= USB_DEFAULT_ADDR;
        active_config <= USB_NO_CONFIG;
      end else begin
        // Registers follow their commits, gated on the SAME conditions the
        // state machine uses. Duplicating the condition is deliberate: it
        // keeps the register and the state arm impossible to update
        // independently, which is how they drift apart.
        if (addr_commit   && (dev_state == DEV_DEFAULT)
                          && (addr_value != USB_DEFAULT_ADDR))
          active_addr <= addr_value;

        if (config_commit && ((dev_state == DEV_ADDRESS)
                           || (dev_state == DEV_CONFIGURED)))
          active_config <= config_value;
      end
    end
  end

endmodule

What it models. The five wired states, the events between them, event priority, and the reset cleanup that keeps the architectural registers consistent with the state.

Why this hardware exists. Because what is legal now has to be a fact something holds, and because the registers that give a state its meaning have to move with it.

Inputs. Clock and local reset; the two physical-domain signals; a decoded bus reset; and two qualified commit events with their values.

State retained. The protocol state, the active address, the active configuration.

Outputs. The state, the two registers, a derived enable, and a change pulse.

Reset behaviour. The local reset clears everything to the not-attached state. A bus reset is an input, not a reset — a distinction §6 is entirely about.

Hardware implied. A 3-bit state register, a 7-bit and an 8-bit register, a small comparator tree and a case statement. That is the whole block, and its smallness is the architectural point of Chapter 8.1 §3.

Assumptions. That phys_connected is debounced; that bus_reset is decoded and synchronised; that addr_commit and config_commit are single-cycle pulses already qualified as successful completions; and that their values are stable during the pulse.

Deliberately omits. Everything that decides an event occurred, plus endpoints, packets, descriptors and suspend.

What DV should verify. Every legal transition; that no illegal one is possible; that a bus reset from every state produces Default with both registers cleared; that the derived enable never disagrees with the state; that the default address is not treated as an assignment; and that priority behaves as §5 states when events coincide.

5. Event Priority

Real controllers see more than one condition in the same cycle. The ordering in §4 is a design decision that has to be stated and defended.

The ordering is: physical loss, then bus reset, then normal transitions.

Physical loss dominates because it invalidates the premise of everything else. A configuration commit arriving in the same cycle the device is unplugged is a commit for a device that is no longer there. Applying it produces a device claiming Configured with nothing connected — Chapter 8.1 §6's D1, and a state that survives into the next attachment.

Bus reset dominates normal transitions for the same reason one level down. A reset means the host has abandoned whatever was in progress. A commit arriving in that cycle belongs to a transfer the host is no longer conducting, and honouring it would leave the device in a state the host does not believe it is in.

The general principle, stated once and reused:

Events that invalidate context dominate events that build on it.

And the reason this needs stating at all is that the intuitive ordering is the opposite. Reading the state machine top-down, it is natural to handle the "normal" transitions first and treat loss and reset as exceptional cases bolted on afterwards. That produces exactly the priority inversion above — and Chapter 6.7 §8 measured a closely related ordering defect that survived every test until the conditions were made to coincide deliberately.

6. Clearing a State Register Is Not Clearing a State

The chapter's central lesson, and the one that produces its most valuable bug.

A naive reset handler does this:

if (bus_reset) dev_state <= DEV_DEFAULT;

And it is wrong, not because the assignment is incorrect, but because it is incomplete.

Ask what Default means. §1 said it: the device responds to the default address, has no assigned address, and has no configuration. Those are claims about registers, not about an enum. A device whose state register says DEV_DEFAULT while its address register holds 7 is not in Default — it is a device claiming Default while behaving like something else.

So a reset must clear everything that gives the state its meaning:

And note the asymmetry in the figure. The enable does not need clearing, because it is derived from the state rather than stored. That is the architectural payoff of the assign in §4: one fewer thing that can be forgotten. Chapter 8.5 measures what the registered alternative costs.

7. The Assertions

// ─────────────────────────────────────────────────────────────────────────
// Classification: TEACHING ASSERTIONS about the device state machine.
// S-properties are SAFETY (something never happens); P-properties are
// PROGRESS (something must happen). Section 9 measures why both are needed.
// ─────────────────────────────────────────────────────────────────────────

// S1 -- LEGAL TRANSITIONS. The state may only move along the edges of
// figure 1. Written as an explicit edge list rather than as arithmetic on
// the encoding: a property that depends on enum values stops meaning
// anything the moment somebody renumbers them.
property p_legal_transitions;
  @(posedge clk) disable iff (!rst_n)
    (dev_state != $past(dev_state)) |-> (
         (dev_state == DEV_NOTATTACHED)                                  // loss
      || (dev_state == DEV_ATTACHED)                                     // loss
      || ($past(dev_state) == DEV_ATTACHED   && dev_state == DEV_POWERED)
      || (dev_state == DEV_DEFAULT    && $past(bus_reset))               // the
      || ($past(dev_state) == DEV_DEFAULT    && dev_state == DEV_ADDRESS)
      || ($past(dev_state) == DEV_ADDRESS    && dev_state == DEV_CONFIGURED)
      || ($past(dev_state) == DEV_CONFIGURED && dev_state == DEV_ADDRESS)
    );
endproperty
assert property (p_legal_transitions);

// S2 -- NO SHORTCUT. Default can never become Configured directly. This is
// implied by S1 and stated separately anyway, because it is the single
// transition whose absence a reader most wants to see asserted, and because
// section 9's first mutation targets exactly it.
property p_no_default_to_configured;
  @(posedge clk) disable iff (!rst_n)
    ($past(dev_state) == DEV_DEFAULT) |-> (dev_state != DEV_CONFIGURED);
endproperty
assert property (p_no_default_to_configured);

// S3 -- RESET IS UNCONDITIONAL. From ANY state, a bus reset reaches Default.
// Deliberately no antecedent on dev_state: the moment a reset property has
// to enumerate the states it applies from, the state it omits is where the
// bug will be (Chapter 6.6 section 5).
property p_reset_reaches_default;
  @(posedge clk) disable iff (!rst_n)
    (bus_reset && phys_connected && phys_powered) |=> (dev_state == DEV_DEFAULT);
endproperty
assert property (p_reset_reaches_default);

// S4 -- COMPOSITION. Reset clears the registers, not just the enum. This is
// section 6, and it is the property section 9's second mutation defeats
// every OTHER property to reach.
property p_reset_clears_everything;
  @(posedge clk) disable iff (!rst_n)
    (bus_reset && phys_connected && phys_powered)
      |=> (dev_state     == DEV_DEFAULT
        && active_addr   == USB_DEFAULT_ADDR
        && active_config == USB_NO_CONFIG
        && !function_eps_enabled);
endproperty
assert property (p_reset_clears_everything);

// S5 -- COMPOSITION. Being in Address or Configured means actually HOLDING
// a non-default address. Chapter 8.4 develops this; it is stated here
// because the state machine is what has to maintain it.
property p_addressed_implies_address;
  @(posedge clk) disable iff (!rst_n)
    (dev_state == DEV_ADDRESS || dev_state == DEV_CONFIGURED)
      |-> (active_addr != USB_DEFAULT_ADDR);
endproperty
assert property (p_addressed_implies_address);

// S6 -- COMPOSITION. Configured means actually holding a configuration.
property p_configured_implies_config;
  @(posedge clk) disable iff (!rst_n)
    (dev_state == DEV_CONFIGURED) |-> (active_config != USB_NO_CONFIG);
endproperty
assert property (p_configured_implies_config);

// S7 -- STABILITY. Without a qualifying event, the state holds. This is
// what forbids a state machine that wanders.
property p_stable_without_events;
  @(posedge clk) disable iff (!rst_n)
    (!bus_reset && !addr_commit && !config_commit
     && phys_connected && phys_powered) |=> $stable(dev_state);
endproperty
assert property (p_stable_without_events);

// P1 -- PROGRESS. Every safety property above is satisfied by a state
// machine that never leaves DEV_NOTATTACHED. This is what forbids that: a
// qualified address commit in Default MUST produce Address.
property p_address_commit_progresses;
  @(posedge clk) disable iff (!rst_n)
    (dev_state == DEV_DEFAULT && addr_commit && (addr_value != USB_DEFAULT_ADDR)
     && !bus_reset && phys_connected && phys_powered)
      |=> (dev_state == DEV_ADDRESS);
endproperty
assert property (p_address_commit_progresses);

// P2 -- PROGRESS, the configuration half.
property p_config_commit_progresses;
  @(posedge clk) disable iff (!rst_n)
    (dev_state == DEV_ADDRESS && config_commit && (config_value != USB_NO_CONFIG)
     && !bus_reset && phys_connected && phys_powered)
      |=> (dev_state == DEV_CONFIGURED);
endproperty
assert property (p_config_commit_progresses);

S1 through S7 are safety; P1 and P2 are progress, and §9 measures why stating them separately is not pedantry: a state machine that does nothing at all satisfies every safety property here.

S4, S5 and S6 are the composition properties, and they are the ones this module exists to teach. Each spans the state and a register that gives it meaning. Chapter 8.4 is built on what they catch.

S3's missing antecedent is deliberate and worth defending. It would be natural to write from Address or Configured, a reset reaches Default. That version is satisfied by a design that mishandles reset from any state the list omits — and the omitted state is always the one nobody thought about, which is the same one the design got wrong.

8. State Trace

Trace the machine by hand before trusting simulation. Track four things, because §6's point is that the state alone is not the state.

Three rows repay attention.

The un-select row. Committing configuration zero moves the state to Address and clears the configuration and drops the enable — three effects from one event, because the last two follow from the first.

The second bus-reset row. Every column returns to its default in the same cycle. §9's second mutation changes exactly one of these cells and nothing else.

The disconnect row. The address clears. A controller that only cleared on bus_reset would leave 9 there — Chapter 8.1 §9's stale-state signature, which is why §4's clearing condition includes the physical terms.

9. Mutation Test

Five mutations of §4. All were run; results are measured.

M1 — allow Default to reach Configured

The shortcut, added the way it happens: someone handles a configuration commit "wherever it arrives".

DEV_DEFAULT:
  if (config_commit) next_state = DEV_CONFIGURED;   // MUTANT M1

Result, measured: four properties fire — S1, S2, S5 and S6.

S1 and S2 catch the illegal edge itself. S5 and S6 catch its consequences: the device reaches Configured without ever having been addressed, so it holds the default address, and without its configuration register ever being written, because that register's gate still requires Address or Configured.

Which is the instructive part. One wrong arm produces a state contradicting two registers, and the properties that notice come from two different families — transition legality and composition. A defect rarely violates only the rule it most obviously breaks.

M2 — partial reset

The module's defining bug. Reset the state; leave the address.

if (!phys_connected || !phys_powered || bus_reset) begin
  active_config <= USB_NO_CONFIG;
  // MUTANT M2: active_addr deliberately not cleared
end

Result, measured across the property set — S4 is the only one that fires:

  S1 legal transitions        PASS
  S2 no shortcut              PASS
  S3 reset reaches Default    PASS
  S5 addressed has address    PASS
  S6 configured has config    PASS
  S7 stability                PASS
  P1 address progress         PASS
  P2 config progress          PASS

  S4 reset clears everything  FAILS   ← the only one

Every property about the state machine passes. The transitions are legal, reset reaches Default, progress happens, the machine is stable. S4 is the only one that fires, because it is the only one that looks at a register.

And the device it produces: one that reports Default, behaves as Default in every respect the state machine governs, and answers to an address from before the reset. §11 traces what that does to a host.

M3 — configuration survives a bus reset

if (!phys_connected || !phys_powered || bus_reset) begin
  active_addr <= USB_DEFAULT_ADDR;
  // MUTANT M3: active_config not cleared
end

Result, measured: S4 alone fires — and notably S6 does not, which is worth understanding.

S6 forbids a Configured device from holding no configuration. This mutant produces the opposite: a Default device holding a configuration it should have lost. S6 says nothing about that, because it constrains only one direction of the relationship.

So the catch comes entirely from S4's conjunction, which enumerates what a reset must leave behind rather than constraining states individually. That is the argument for writing it as one property over four terms rather than four properties over one term each: the conjunction covers combinations that individually-correct properties do not mention.

And the derived enable limits the damage. function_eps_enabled stays low throughout, because it follows the state rather than the configuration register — §6's figure claiming exactly this, measured. A design that registered the enable separately would have left it high.

M4 — commit on request rather than on completion

Not an arm change but an interface violation: drive the state machine from a request-decoded pulse instead of a qualified completion.

Result. The state machine cannot detect this at all, and that is correct rather than a weakness. From inside this block, a pulse is a pulse; nothing distinguishes a qualified commit from an unqualified one. The property that catches it belongs to Chapter 6.3, which owns the block that decides completion.

This is the module's architectural claim made concrete. A small state machine consuming qualified events cannot verify the qualification — and should not try. The verification has to live where the information is, which is why §4's assumptions list is explicit about what it is trusting.

M5 — remove a transition entirely

DEV_ADDRESS:
  ;   // MUTANT M5: the configuration transition deleted

Result, measured: every safety property passes and P2 alone fires.

  S1 legal transitions      PASS   — no illegal transition occurs,
                                     because no transition occurs at all
  S2 no shortcut            PASS   — vacuously
  S3 reset reaches Default  PASS
  S4 reset clears           PASS
  S5 addressed has address  PASS
  S6 configured has config  PASS   — vacuously: never Configured
  S7 stability              PASS
  P1 address progress       PASS

  P2 config progress        FAILS

A configuration commit in Address must produce Configured, and it does not. Nothing else in the set can tell, because seven of the eight are prohibitions and a machine that refuses to move violates no prohibition.

10. Verification

This chapter's commit point is the device is in a known state — the one the host can force.

Stimulus. Every legal transition in figure 1; a bus reset from every state, including Default itself; every illegal event attempted in every state; power loss and disconnection from every state; commits carrying the reserved values (the default address, configuration zero); and events arriving in the same cycle, in each priority-relevant combination.

Reset from every state is not a thoroughness gesture — it is the only way to validate S3's missing antecedent. A test that resets from Configured and Address has checked two of five.

Observation. The state, both registers, and the derived enable — together, on every event. §9's M2 is invisible to any observation of the state alone, and M2 is the defect this module exists to teach.

Reference model. A four-field model: expected state, address, configuration, enable. Drive it with the same qualified events and compare after each. The comparison must be of all four — a scoreboard checking only the state enum reports M2 as passing.

Representative coverage — crosses:

• current state × every event type, including events illegal in that state
• state × bus reset — all five states
• state × physical loss
• commit value at the reserved value × a normal value, for both address and configuration
• simultaneous events: bus reset × commit; physical loss × commit; physical loss × bus reset

Negative cases with defined outcomes: a configuration commit in Default or Powered must not change the state; an address commit carrying the default address must not produce Address; a commit arriving with a bus reset must lose; and an illegal state encoding must recover rather than hold.

11. Debugging: the Device That Claims Default

A device enumerates, works, and is then reset by the host. After the reset the host cannot reach it. The device's status register reports Default. A protocol analyser shows the host addressing the default address and nothing responding.

What does the status says Default rule out? Less than it appears. It rules out a state machine that failed to transition, which is the thing most people check first and the thing that is fine.

What does nothing responds at the default address tell you? That the device is not answering where a Default-state device must. So the device's behaviour and its reported state disagree — and behaviour is the evidence, since the status register is the device's own claim about itself.

What could make a Default device not answer at the default address? It is answering somewhere else. Its address comparison is matching a different value — one from before the reset.

Which is §9's M2 exactly. The state register cleared; the address register did not.

Why did no state-machine assertion catch it? Because the state machine is correct. M2's measurement is precisely this: seven properties pass, and only the one that reads the address register fires.

What is the first thing to inspect, concretely? The active address register, immediately after the reset. If it is non-zero while the state says Default, the diagnosis is complete and the fix is one line in the reset clearing.

And the signature to memorise? Works, gets reset, then disappears — reporting a correct state. A device that reports the right state and behaves wrongly is almost always a composition failure, because a state is a claim about registers and the claim has stopped being true.

12. Common Misconceptions

13. Reason It Through

A reviewer proposes simplifying §4 by removing the default arm of the case statement, on the grounds that all six encodings of a 3-bit state are either used or unreachable.

Is the premise true? Almost. Six of eight encodings are used, so two are unreachable by the design's own logic.

So why keep the arm? Because unreachable by the logic is not unreachable. A single-bit upset in the state register produces an encoding the design cannot produce, and the question is what happens next.

What happens with the arm? The machine recovers to a state that is always safe, the host's reset reaches it, and enumeration restarts. The device glitches and continues.

What happens without it? With no default arm and next_state defaulting to hold, the machine stays in the illegal encoding. It matches no arm, so nothing moves it — and a bus reset does reach it, because §4's reset branch sits above the case. So it recovers anyway.

Which makes the arm redundant? No — and this is the part worth working through. It is redundant given that the reset branch has priority over the case. That is a property of §5's ordering, not of the case statement. A refactor that moved the reset handling into the case, which is a natural tidying, would remove the protection without touching the default arm at all.

What is the general lesson? The same one §5's callout drew: when a structure is protected by something that was not built to protect it, the protection is invisible to the next person. Keeping the default arm costs nothing and makes recovery a local property rather than one that depends on the ordering of a branch somewhere else.

14. Understanding Check

15. Summary

Default is the state a bus reset produces, and it is reachable from everywhere. That single unconditional edge is what makes a USB device recoverable from any condition — and its defining feature is that it requires nothing from the device, because the moment a recovery path needs the failing party to act correctly it stops being one.

The state machine has a structural asymmetry worth naming: every transition that adds protocol identity requires a device commit; every transition that removes it requires nothing. A device can always be stripped of state and never given state without participating.

Events are not states. Address persists; an address commit happens once. The state machine consumes already-qualified single-cycle events, which is why it is small — it does the one job that is genuinely a state machine's and consumes the results of the jobs that are not.

Event priority is a design decision: physical loss, then bus reset, then normal transitions — because events that invalidate context dominate events that build on it. The intuitive ordering is the reverse, which is why it needs stating.

The chapter's central lesson is that clearing a state register is not clearing a state. Default means the default address and no configuration, so a reset must return everything the state's meaning depends on. §9 measured a partial reset passing every state-machine property — legal transitions, reset reaches Default, progress, stability — and being caught only by the one property that reads a register.

And §9's other half: deleting a transition passes every safety property, several vacuously, because safety forbids and never requires. Together the two mutations establish that a property set needs safety, progress and composition, and that each catches defects the others cannot see.

16. What Comes Next

The device has an identity in one sense — it is in a known state and the host can talk to it — and none in the sense that matters, because it answers at an address every freshly-reset device answers at.

Chapter 8.4 is where that changes, and it takes §6's lesson and makes it the whole subject. Address is the first state whose entire meaning lives in a register, and the first where the question what makes this device an Address-state device? has an answer that is not the enum says so.

It is also where §9's M2 stops being a mutation and becomes the chapter's organising bug.

Browse the full path on the USB tutorials index.