Addressed State

Chapter 8.3 built the state machine and ended with a claim worth testing: that a partial reset leaves a perfectly correct state machine driving an incorrect device, and that only one property in an eight-property set notices.

This chapter is that claim's home, because Address is the first state where the question has a non-obvious answer:

What makes a device an Address-state device?

Not that an enum says so. The state is a claim about a register, and the register is what the rest of the bus actually sees.

1. What Address Means

A device is in Address after an address assignment has committed. It responds at a unique address, it has no configuration, and its function endpoints do not operate.

What is legal? Control communication at its assigned address — enough for the host to read its descriptors (Module 7) and select a configuration. Nothing else.

What is guaranteed? That the device holds a non-default address and answers there. That is the state's entire content.

How is it entered? From Default by an address commit carrying a non-default value. From Configured by an un-select (Chapter 6.5).

How is it left? Upward by a configuration commit. Downward by a bus reset, power loss or disconnection.

2. The State Is the Register

Here is the chapter's thesis, stated as plainly as possible.

Consider what the bus actually sees. Every packet on the bus carries an address, and every device compares it against the address it holds. A device "is" at address 5 because its comparator matches 5 — not because a state register somewhere says DEV_ADDRESS.

So the state enum is a summary, and the address register is the fact. The enum is useful: it gates legality, drives status, and makes the design readable. But if the two disagree, the register wins, because the register is what is wired to the thing that answers packets.

That asymmetry has a direct verification consequence:

A property about the state machine cannot detect a defect in the register, and the register is the part that determines behaviour.

Chapter 8.3 §9's M2 measured exactly this — eight properties, seven of them about transitions, and only the one that reads the register fires.

3. Composition Invariants

The relationships that have to hold between state and registers, stated as rules rather than as code.

I1 — Address implies a non-default address.

dev_state ∈ { ADDRESS, CONFIGURED }   ⟹   active_addr ≠ default

Both states, because a Configured device is also addressed. A device claiming either while holding the default address is claiming an identity it does not have.

I2 — Default or below implies the default address.

dev_state ∈ { NotAttached, Attached, Powered, Default }   ⟹   active_addr = default

Read this one carefully, because it is the direction that is easy to get wrong. I1 says if you claim an identity you must hold one. I2 says if you claim no identity you must hold none — a device reporting Default while holding address 7 violates I2 and satisfies I1 completely.

That asymmetry is the whole reason both are needed, and §5 measured what happens to a property set that has only one of them.

I3 — the address changes only at a commit or a clearing event.

active_addr changed   ⟹   an address commit, a bus reset, or physical loss

This is what forbids the register drifting on its own — and Chapter 6.3 §5 established the same rule from the register's side.

I4 — a bus reset returns both together.

bus reset   ⟹   dev_state = Default  AND  active_addr = default

The conjunction is the requirement. Chapter 8.3 §9 measured this precisely: splitting it into the state becomes Default and the address is cleared as separate properties loses the case where one holds and the other does not — which is the only case that matters.

4. The Composition Checker

Chapter 8.3's state machine already maintains these invariants. This block checks them, and it is deliberately separate from the design.

// ─────────────────────────────────────────────────────────────────────────
// usb_addr_composition_check
//
// Classification: VERIFICATION MODEL. Not synthesizable and not part of any
// device. It is bound alongside the state machine and watches it.
//
// WHAT IT MODELS. Section 3's invariants I1 to I4 -- the relationships
// between the protocol state and the address register that no property
// written inside either one can express.
//
// WHY IT IS A SEPARATE BLOCK. Not because it must be, but because making it
// separate makes the SCOPE explicit: this checker consumes signals from two
// owners and belongs to neither. A reader can see at a glance that it is
// the thing nobody's block-level plan would have produced.
//
// WHAT IT DOES NOT MODEL. Transitions (Chapter 8.3 owns them), the commit
// decision (Chapter 6.3), configuration (Chapter 8.5), endpoints (Module 9),
// or anything about transfers.
// ─────────────────────────────────────────────────────────────────────────
module usb_addr_composition_check
  import usb_state_pkg::*;
(
  input logic            clk,
  input logic            rst_n,

  input usb_dev_state_e  dev_state,
  input logic [6:0]      active_addr,

  input logic            bus_reset,
  input logic            addr_commit,
  input logic            phys_connected,
  input logic            phys_powered,

  output logic           composition_error
);

  logic i1, i2, i3, i4;
  logic [6:0]     p_addr;
  logic           p_reset, p_commit, p_conn, p_pwr;
  usb_dev_state_e p_state;

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      p_addr   <= USB_DEFAULT_ADDR;
      p_state  <= DEV_NOTATTACHED;
      p_reset  <= 1'b0;
      p_commit <= 1'b0;
      p_conn   <= 1'b0;
      p_pwr    <= 1'b0;
    end else begin
      p_addr   <= active_addr;
      p_state  <= dev_state;
      p_reset  <= bus_reset;
      p_commit <= addr_commit;
      p_conn   <= phys_connected;
      p_pwr    <= phys_powered;
    end
  end

  // ── I1: claiming an identity requires holding one ──────────────────────
  assign i1 = ((dev_state == DEV_ADDRESS) || (dev_state == DEV_CONFIGURED))
              && (active_addr == USB_DEFAULT_ADDR);

  // ── I2: the OTHER direction -- claiming no identity means holding none.
  // This is the invariant a partial reset violates: a device reporting
  // Default while still holding an assigned address. Section 5 measured a
  // property set WITHOUT this one letting two separate mutations through,
  // which is how it came to be written this way.
  assign i2 = (active_addr != USB_DEFAULT_ADDR)
              && ((dev_state == DEV_NOTATTACHED) || (dev_state == DEV_ATTACHED)
               || (dev_state == DEV_POWERED)     || (dev_state == DEV_DEFAULT));

  // ── I3: the register does not drift ────────────────────────────────────
  // Note this compares against the PREVIOUS cycle's event signals, because
  // a registered value reflects an event one cycle after it occurred. A
  // version comparing against the current cycle would fire on correct
  // hardware -- the mistake Chapter 8.2 section 7 warns about.
  assign i3 = (active_addr != p_addr)
              && !(p_commit || p_reset || !p_conn || !p_pwr);

  // ── I4: reset returns BOTH, as one requirement ─────────────────────────
  // The conjunction is the point. Two separate checks -- "the state became
  // Default" and "the address cleared" -- both pass on a design where only
  // one happened, which is the only case worth catching.
  assign i4 = p_reset && p_conn && p_pwr
              && !((dev_state == DEV_DEFAULT) && (active_addr == USB_DEFAULT_ADDR));

  assign composition_error = i1 | i2 | i3 | i4;

  always_ff @(posedge clk) begin
    if (rst_n) begin
      if (i1) $error("I1: state %0s while holding the default address",
                     dev_state.name());
      if (i2) $error("I2: state %0s while still holding address %0d",
                     dev_state.name(), active_addr);
      if (i3) $error("I3: active_addr changed %0d -> %0d with no event",
                     p_addr, active_addr);
      if (i4) $error("I4: after reset, state=%0s addr=%0d -- both must return",
                     dev_state.name(), active_addr);
    end
  end

endmodule

Classification. Verification model — bound alongside the design, never driving it.

What it models. §3's four invariants.

Why it exists. Because each invariant mentions two things owned by different concerns, so no property written inside either one can express it.

Inputs. The state, the address register, and the events that are permitted to change either.

State retained. One cycle of history for each input, because three of the four invariants are about change rather than about a moment.

Outputs. A single error flag plus per-invariant reporting.

Reset behaviour. History clears; reporting is suppressed while the local reset is asserted.

Hardware implied. None — this is not hardware.

Assumptions. That all inputs are in the same clock domain, and that the event signals are the same ones the state machine consumes. The second assumption matters: a checker fed different signals from the design is checking a different design.

Deliberately omits. Transitions, the commit decision, configuration, endpoints and transfers.

What DV should verify with it. That each of the four invariants fires when its specific defect is injected — §5 does exactly that.

5. Mutation Test

Five mutations, and this section reports something that happened while writing it: the first version of §3's invariant set had a hole, and two of these mutations walked straight through it. The measurement is below, and so is the correction.

The measured result

  mutation                                    I1    I2    I3    I4
  ────────────────────────────────────────────────────────────────
  correct design                               ·     ·     ·     ·
  M1  Default → Configured shortcut            9     ·     ·     ·
  A1  partial reset (address not cleared)      ·    16     ·     3
  A2  address cleared one cycle late           ·     5     3     2
  A3  address committed, state not moved       ·    26     ·     ·
  A4  spurious change to the address           ·     ·     3     ·

A1 — the partial reset

Chapter 8.3 §9's M2, examined here properly. Reset clears the state; the address register is left alone.

Result. Every state-machine property passes — all eight, because the state machine is genuinely correct. I2 and I4 fire: I4 on the reset itself, because the conjunction it requires is not satisfied, and I2 continuously afterwards, because the device reports Default while holding an assigned address.

A2 — clear the address one cycle late

The reset clears the state immediately and the address on the following cycle.

Result. I4 fires, and so do I2 and I3 — I2 during the one-cycle window, I3 because the register changes on a cycle with no event behind it.

The window is the point. For one cycle the device reports Default while its comparator still matches its old address, and a cycle is long enough for an address comparison. A checker evaluating consistency a few cycles after a reset sees a fully settled, entirely consistent device.

A3 — commit the address without moving the state

The register updates; the state machine stays in Default.

Result. I2 alone fires, 26 times — the device holds an assigned address while claiming Default, continuously, for the rest of the run.

A4 — a spurious change to the address register

A miswired enable that perturbs the address on an unrelated event.

Result. I3 alone fires. Neither I1 nor I2 notices, because the device is in Address holding a non-default address — which is exactly what both of them require. It is simply the wrong non-default address.

That is the gap I3 exists for. I1 and I2 constrain the address's category; only I3 constrains its provenance.

M1 — the Default-to-Configured shortcut

Chapter 8.3 §9's M1, run against this checker.

Result. I1 alone fires — the device reaches Configured without ever having been addressed, so it claims an identity while holding the default address.

And I1 fires only once the stimulus issues a configuration commit while the device is in Default. With the more natural stimulus — commit a configuration only from Address, as a working host does — I1 fires on nothing, including this mutation.

6. Verification

This chapter's commit point is the device has an identity — and the identity is the register, not the state.

Stimulus. Address commits with default and non-default values; a bus reset from Address and from Configured, since both are addressed states; an un-select returning Configured to Address, which must preserve the address; a second address assignment while already addressed; and physical loss from Address.

The stimulus requirement §5 makes non-negotiable: the reset cases must be observed on the cycle they complete, not after settling. A2 is a one-cycle inconsistency, and a check that samples a few cycles later sees a perfectly consistent device.

Observation. The state and the address register together, every cycle. §5 measured a defect invisible to eight properties about the state machine.

Reference model. Expected state and expected address, compared as a pair. A scoreboard comparing them separately reports A1 as two passes.

Representative coverage — crosses:

• state × address category: default versus assigned, for every state
• bus reset from each addressed state — Address and Configured
• address commit with the default value × a normal value, in every state
• un-select from Configured, checking that the address survives it
• re-assignment while already addressed
• physical loss from Address and from Configured

Negative cases with defined outcomes: an address commit carrying the default address must not produce Address; a reset must clear the state and the address in the same cycle; an un-select must clear the configuration and not the address; and the address must never change without a commit or a clearing event.

7. Debugging: the Device at the Wrong Address

A device enumerates and works. The host resets it. Afterwards the host cannot reach it, and the device's status register reports Default.

What is the contradiction? A Default-state device answers at the default address. The host is addressing the default address. Nothing responds. So either the device is not in Default, or it is in Default and not behaving like it.

Which evidence wins? The behaviour. The status register is the device's own claim about itself, produced by the state machine; the address comparator is what the bus interacts with. §2's figure is exactly this: when the two disagree, the register the comparator uses is the fact.

What do you inspect, and when? The active address register, immediately after the reset completes. Not later — §5's A2 is a one-cycle window.

What are the two candidates? The address was never cleared (A1), or it was cleared late (A2). Both produce the same steady-state symptom if the host's first post-reset packet lands in the window.

How do you tell them apart? A1 leaves the address non-default indefinitely; A2 leaves it non-default for one cycle. A trace of the register across the reset separates them immediately, and a status register that exposed the address would separate them without a trace.

And the signature? A device reporting a correct state while behaving incorrectly is almost always a composition failure — because a state is a claim about registers, and the claim has stopped being true. Chasing the state machine is the natural first move and the wrong one: Chapter 8.3 §9 measured it passing every property it has.

8. Common Misconceptions

9. Reason It Through

A reviewer proposes dropping I2 on the grounds that it is the contrapositive of I1 and therefore adds nothing.

Is the logical claim true? It depends entirely on how I2 is written, and that is the whole exercise.

The contrapositive of I1 — Address or Configured implies a non-default address — is the default address implies not Address and not Configured. That statement is logically equivalent to I1, and a checker implementing it is genuinely close to redundant.

But that is not what §3's I2 says. §3's I2 is Default or below implies the default address, which is a different statement — it constrains the states I1 says nothing about, in the direction I1 does not cover.

Work out which defects each catches. I1's antecedent is true when the device claims an identity. I2's is true when the device claims none. A device reporting Default while holding address 7 makes I2's antecedent true and I1's false, so only I2 can see it.

And that device is this module's headline bug. §5 measured it: with the contrapositive version of I2, the partial reset was caught only by I4, and a state-without-register mutation was caught by nothing at all.

So what should the reviewer be told? That the proposal is correct about the version they are looking at only if that version is the contrapositive — and that the version in the design is not, deliberately, because the contrapositive was tried first and let two mutations through.

And the general rule to extract? A property set is a set of triggers, not a set of theorems. Two logically equivalent statements have different antecedents, so they are evaluated on different cycles and exercised by different stimulus. Before removing a property as redundant, do not reason about what it means — find a defect that trips one and not the other. If one exists, they are not redundant, whatever the logic says.

10. Understanding Check

11. Summary

Address is the first state whose meaning lives in a register. A device is at address 5 because its comparator matches 5 — the state enum is a summary that gates legality and drives status, and the register is the fact the bus interacts with. When they disagree, the register wins.

That produces the module's central verification consequence: a property about the state machine cannot detect a defect in the register, and the register is what determines behaviour. Chapter 8.3 measured eight state-machine properties passing against a device answering at the wrong address after a reset.

The answer is composition invariants — facts requiring two owners to state:

• I1 Address or Configured implies a non-default address
• I2 the default address implies Default or below
• I3 the address changes only at a commit or a clearing event
• I4 a bus reset returns state and address together, as one conjunction

Five mutations established that none is redundant — and found that the first version of the set had a hole. I2 was originally written as I1's literal contrapositive, and with that version a partial reset was caught only by I4 and a register-updated-without-the-state mutation was caught by nothing at all. Restating I2 as Default or below implies the default address — a different statement, not a rephrasing — closes both.

The corrected set has no redundancy: a spurious register change trips only I3, because I1 and I2 constrain the address's category and only I3 constrains its provenance; and the Default-to-Configured shortcut trips only I1.

Two rules generalise. The dangerous defects are the ones tripping exactly one invariant, because they survive any set missing it. And a property set is a set of triggers, not a set of theorems — two logically equivalent statements have different antecedents, so they fire on different cycles, and redundancy has to be established by finding a defect that separates them rather than by reasoning about meaning.

12. What Comes Next

The device has an identity. The host can reach it uniquely, read everything it claims to be, and decide what to do with it.

Chapter 8.5 is where the device becomes usable, and it takes this chapter's lesson one step further. Configured is a state whose meaning lives in a register and whose consequences reach outward into hardware that is not part of the state machine at all — endpoint enables, buffers, and whatever else a configuration brings to life.

Which introduces a failure mode Address does not have: not two things disagreeing, but many. A configuration register, a state machine, a set of endpoint enables and firmware's belief can all hold different opinions simultaneously, each locally correct.

Browse the full path on the USB tutorials index.