Protocol Verification

Module 19 designed a link by reasoning about what the implementation should do. This module asks the opposite question: how do you prove, independently of that reasoning, that the link obeys its contracts — and how do you avoid building a verification environment that inherits the design's misconceptions and agrees with them?

1. The One-Sentence Model

Protocol verification checks promises at boundaries, not implementation choices inside them — so every check must be derivable from what one side promised the other, and any check that cannot be stated without naming an internal signal is verifying the implementation against itself.

That framing has a sharp consequence that runs through the whole chapter. A verification environment written by reading the RTL will agree with the RTL about the thing most likely to be wrong: which event means what. Three chapters of Module 19 ended with the same warning — 19.5 §56 on credit scoreboards, 19.6 §13 on legality models, 19.6 §53 on testbench defaults — and this chapter is the systematic answer.

2. What This Chapter Owns

Module 20 has seven chapters. This one is the decomposition and the methodology; it must not consume the other six.

So this chapter answers one question and hands the rest on:

What are the protocol rules, at which boundary does each one live, and what is the smallest independent model that can check it?

It owns five things specifically:

The five planes (§5) — structural validity, resource accounting, ordering and identity, reliability and exactly-once, liveness and progress — which is the decomposition every later chapter inherits.

Monitor architecture (§7–§11), and the reason a single end-to-end monitor is nearly useless for a three-layer stack: it reports that the output was wrong, not which layer first diverged.

Event discipline (§10–§15) — why events must come from handshakes and contracts rather than from state values, and why an X-check that fires on legal stimulus makes verification worse.

The safety/liveness split with assumptions written down (§25–§29), because a liveness property with no assumptions fails on the environment and gets deleted.

And four independent models (§30–§37) plus the layered scoreboard that joins them — including the specific reason a mirror model proves nothing.

3. Sourcing

4. Seven Questions Per Boundary

The recurring template. For every interface in the design, protocol verification asks the same seven questions, and the answers are the verification plan for that boundary.

Question 7 is the one people skip, and it is the one that designs the architecture. A boundary that cannot observe a class of failure is not a defective boundary — it is a statement that the check belongs somewhere else, and following that statement to its conclusion is how you end up with monitors at four boundaries rather than one.

Worked, at the protocol-to-Adapter boundary of the illustrative design:

1. acceptance — the object's handshake completes;
2. obligation — the Adapter will deliver this object to the peer's protocol layer exactly once, or report a failure;
3. stable — the payload, its metadata, its class and its framing bits, from valid until accept;
4. resolves — a delivery indication or an explicit failure, eventually;
5. forbidden — accepting an object for a disabled protocol; changing the payload under a stall; accepting when no resource was reserved;
6. eventually — every accepted object resolves, assuming the link eventually recovers and the peer eventually drains;
7. not observable here — whether the object was duplicated on the wire, and whether the peer's protocol layer saw it once. Both need a monitor at the far end, which is why §6 has four.

5. The Five Verification Planes

Protocol verification is not packet-field checking. It has five independent planes, and a plan that covers three of them has a hole the size of the other two.

Four observations.

Plane 1 is the one everybody builds and the least likely to hold a serious bug. It catches malformed stimulus and integration errors — valuable, cheap, and not where the hard failures are.

Planes 2 and 5 are the same mechanism seen from two sides, and they are the pair Module 19 kept returning to. 19.5 §42's batching deadlock is a plane 5 failure caused by plane 2 state, and no plane-1 check anywhere in the design can see it.

Plane 4 cannot be checked at one boundary. "Exactly once" is a statement relating an event at the transmitter to an event at the far receiver. Any environment with a single observation point has assumed plane 4 rather than checked it.

And plane 3 is where the expensive bugs are. A response matched to the wrong request delivers wrong data as correct data — no error is reported anywhere, and the consumer acts on it. 19.2 §29 and 19.3 §33 are two instances.

6. The Verification Architecture

Three things to read, and one absence.

Four monitors, four models, one join. The monitors are passive and know nothing about correctness; the models hold expectations; the scoreboard relates them. Collapsing any two of those roles is how a monitor ends up encoding an assumption.

The models map one-to-one onto planes 2 to 5. Plane 1 is not a model at all — it is local assertions at each boundary, which is why it appears in the top row alongside the design rather than in the model row.

The peer is an observation point, not decoration. Plane 4's properties relate an event here to an event there, so the environment must be able to observe the far end — via a peer model, a loopback, or an instrumented second instance. An environment without a far-end observation point cannot check exactly-once and should say so rather than quietly checking something weaker.

And the absence. No arrow runs from inside the DUT to any model. Every model input is a boundary observation. §31 is what happens when one of those arrows is added for convenience.

7. Why Four Monitors and Not One

A single end-to-end monitor answers one question: was the output wrong?

Four boundary monitors answer the question that gets the bug fixed: which layer first diverged?

Worked, on one failure. A memory read returns wrong data. With one monitor at the client boundary, that is the entire finding — and the investigation must now consider the protocol engine, the Adapter, the reliability mechanism, the flow control, the far end and the peer's own stack.

With four monitors:

The finding is now specific: one semantic operation became two transport objects with no error and no recovery. That is a protocol-engine or Adapter defect, and the search space has gone from six subsystems to one boundary.

Three reasons this matters more for UCIe than for a flat protocol.

The three layers have genuinely different responsibilities. The Protocol Layer owns semantics, the Adapter owns transport reliability, the Physical Layer owns bits (19.2 §1, 19.3 §1). A failure at any of the three produces a wrong output at the client, and only the layer-local observation distinguishes them.

Objects change identity between layers. 19.2 §4 established three objects — a semantic obligation, a transport object, a physical attempt — with one-to-many relationships between them. A monitor that only sees semantic operations cannot count transport objects, and the exactly-once question lives in exactly that ratio.

And a layer can be locally correct and globally wrong. The Adapter delivering an object twice is correct Adapter behaviour if the duplicate-suppression window was sized too small (19.3 §32) — a sizing defect that looks like correct logic at every internal signal. Only the semantic-layer observation shows the duplicate.

8. The Observed-Event Type

// ILLUSTRATIVE, VERIFICATION-ONLY. What a monitor emits. This is not a UCIe
// format, not a wire format, and not derived from any specification (§3).
typedef enum {
  EV_SEM_ACCEPTED,     // a semantic operation was accepted from the client
  EV_OBJ_FORMED,       // a transport object was created for it
  EV_OBJ_COMMITTED,    // the object was committed to the link
  EV_OBJ_ATTEMPTED,    // a physical transmission attempt was made
  EV_OBJ_ARRIVED,      // the far end received an attempt
  EV_OBJ_VERDICT,      // an integrity verdict was reached
  EV_OBJ_DELIVERED,    // the far end delivered it semantically
  EV_SEM_COMPLETED,    // the originating operation completed
  EV_CREDIT_CONSUMED,
  EV_CREDIT_RETURNED,
  EV_RECOVERY_ENTERED,
  EV_RECOVERY_EXITED,
  EV_CFG_COMMITTED
} event_kind_e;
 
typedef struct {
  longint unsigned cycle;        // observation time, per clock domain
  event_kind_e     kind;
  int unsigned     mon_tag;      // THE JOIN KEY — verification-only (§23)
  int unsigned     sem_id;       // as observed, may be reused (19.2 §21)
  int unsigned     obj_id;       // transport identity, as observed
  int unsigned     attempt_num;  // 1 for the first transmission
  int unsigned     cls;          // resource class
  int unsigned     cfg_epoch;    // which configuration was active
  int unsigned     link_epoch;   // which link agreement was in force
  bit [7:0]        boundary_id;  // which monitor produced this
} observed_event_t;

Five decisions in that structure.

mon_tag is separate from sem_id and obj_id. The design's identities are legitimately reused after retirement; the monitor's tag is unique for the whole simulation, which is what makes "this never happens again" a checkable statement (§23).

attempt_num exists so that a retransmission is observable as a retransmission. Without it, a second attempt of one object and a first attempt of another are the same observation — and plane 4's entire question is which one it was.

Both epochs are carried on every event. 19.6 §40 made the same argument for the first-error record: an event without its epochs cannot be reasoned about after the fact. The scoreboard needs them to answer "was this object's rule set changed under it?"

boundary_id is what makes §60's divergence analysis mechanical. Sorting events by cycle and grouping by boundary produces the table in §7 automatically.

And cycle is per clock domain. The four boundaries may be in different domains (19.6 §30). A scoreboard comparing raw cycle numbers across domains is comparing incomparable quantities, and the join must be on the tag, not on time — time is diagnostic context, not an identity.

9. Events Come From Contracts, Not From Registers

The single most important rule in this chapter.

A monitor's event must be derivable from the boundary's contract by somebody who has never read the RTL. If deriving it requires knowing what a state encoding means, or which register holds the pointer, the monitor has become part of the implementation.

What that permits:

• handshakes — valid && ready, or whatever the boundary's acceptance contract is;
• transitions of externally-contracted outputs — a busy deasserting, a status changing;
• arrival of a message at the far end;
• stimulus the environment itself generated, which is the most trustworthy source of all.

What it forbids:

• sampling an internal state register and inferring an event from its value (§11);
• reading an internal counter and treating it as the count;
• using a design signal named after the event — credit_consume_fire is a design signal, and a monitor that samples it has inherited the design's definition of consumption, which is exactly what 19.5 §17 spent five sections getting right.

One honest exception, with a rule attached. Sometimes an event genuinely has no boundary observable — an internal arbitration decision, say. Then the monitor may sample the internal signal, and the model must record that this observation is not independent and cannot be used to check the logic that produces it. A dependency that is documented is a known gap; one that is undocumented is a false pass.

10. Event-Based Rather Than Sampling-Based

// ILLUSTRATIVE. A monitor emitting on a contracted handshake.
always @(posedge clk) begin
  if (rst_n && proto_valid && proto_ready) begin
    observed_event_t e;
    e.cycle       = cycle_count;
    e.kind        = EV_SEM_ACCEPTED;
    e.mon_tag     = next_mon_tag++;          // the monitor's own identity
    e.sem_id      = proto_payload.sem_id;    // as OBSERVED, not as tracked
    e.cls         = proto_payload.cls;
    e.cfg_epoch   = observed_cfg_epoch;
    e.boundary_id = BND_PROTOCOL;
    emit(e);
  end
end

Architecture. One if, on the boundary's acceptance contract, emitting once.

Why an edge and not a level. This is 19.5 §18's lesson applied to verification: a level held during a stall produces one observation per cycle, and the scoreboard sees eight operations where there was one. The monitor now has the same bug the design was being checked for — and worse, if both have it, they agree.

Why sem_id is copied rather than looked up. The monitor records what was on the wire. If the design's internal table says something else, that is a finding, and it can only be a finding if the monitor did not consult the table.

Why the tag is allocated by the monitor. §23.

DV of the monitor itself. Drive a stalled handshake and confirm exactly one event. A monitor is a piece of logic and it needs its own directed tests — an unverified monitor is an unverified verification environment, and it fails silently in the passing direction.

11. Wrong Monitor — Inferring an Event From a State Value

// WRONG — sampling a state register and treating its value as an event.
always @(posedge clk)
  if (tx_state == TX_SENT) emit_attempt_event();

Worked. The transmit object state machine enters TX_SENT and remains there for 5 cycles while awaiting a verdict. The monitor emits five attempt events for one transmission.

What the scoreboard concludes. One semantic operation produced five physical attempts. The reliability model reports four duplicate transmissions. The exactly-once check fires.

Four properties, and the fourth is the reason this is in the chapter.

The design is correct and the report says it is not. A false failure, which costs a day of somebody's time and — much worse — teaches the team to distrust the exactly-once check, which is the check that catches real duplication.

It is not fixable by "sampling less often". A monitor that samples every other cycle emits two or three events instead of five. The count is a function of the state's duration, which is a function of the far end's latency, so the error is load-dependent and irreproducible.

The correct form is the transition, not the value:

// RIGHT — the transition INTO the state, once per entry.
always @(posedge clk)
  if ((tx_state == TX_SENT) && (tx_state_q != TX_SENT)) emit_attempt_event();
 
// BETTER — the contracted boundary event, which needs no state at all.
always @(posedge clk)
  if (phy_tx_valid && phy_tx_ready && phy_tx_first) emit_attempt_event();

And the fourth property: the "better" form is better for a reason beyond correctness. The transition form still depends on the state encoding. When the state machine is redesigned — merged states, an added state, a different encoding — the transition monitor silently changes meaning, while the handshake monitor does not. This is 19.6 §18's public-contract argument, applied to verification collateral: a monitor built on internal structure is as fragile as an integration built on internal structure.

12. The Acceptance Event

At every boundary, exactly one event means "ownership transferred", and every plane's checks hang off it.

// ILLUSTRATIVE, for a boundary that uses a ready/valid contract. NOT a claim
// that any UCIe interface uses these signal names or this protocol (§3).
assign accept = valid && ready;

Three rules about the acceptance event.

It must be defined per boundary, not globally. A boundary with a credit-based contract has a different acceptance event than one with ready; a boundary with a message-passing contract has another. The seven questions of §4 are asked per boundary because the answers differ per boundary.

Everything else is derived from it. Stability is checked until it; X-checks are evaluated at it; the reference model's state transition happens on it; the obligation begins at it. A boundary whose acceptance event is ambiguous has no checkable contract at all, and that ambiguity — not any individual property — is the defect to escalate.

And "acceptance" is not "arrival". Ownership can transfer without the data having gone anywhere, and data can arrive without ownership transferring. 19.3 §9's admission reserves resources before accepting, precisely because accepting is a commitment rather than a movement.

13. SVA — Stability Under Stall

// MANDATORY, at every ready/valid boundary. The canonical property, and the
// one that fires most often at integration.
property p_payload_stable_under_stall;
  @(posedge clk) disable iff (!rst_n)
    (valid && !ready) |=> (valid && $stable(payload));
endproperty
a_payload_stable_under_stall: assert property (p_payload_stable_under_stall);

What the property actually says, in three parts, and all three matter.

valid stays high. A producer that withdraws valid before it was accepted has retracted an offer. Whether that is legal is a contract question — some protocols permit it, most do not — and the property is where the answer is written down.

payload is unchanged. The whole payload, not just the data field.

And |=> rather than |-> — the check is on the next cycle, because the stall condition is evaluated this cycle and the stability requirement applies from here on.

What must be included in payload, and this is where the property is usually written too narrowly:

The failure this catches. A producer whose next-item logic runs one cycle ahead updates the payload registers while ready is low. The consumer, when it finally accepts, takes the second item's payload with the first item's framing. No error is generated anywhere; the object is malformed in a way that looks like data corruption three layers downstream.

14. X-Checking at Meaningful Events

// MANDATORY. Check the CONTRACT-REQUIRED fields, at the ACCEPT event.
property p_no_x_on_meaningful_fields;
  @(posedge clk) disable iff (!rst_n)
    accept |-> !$isunknown({payload.cls, payload.first, payload.last,
                            payload.strb, payload.poison});
endproperty
a_no_x_on_meaningful_fields: assert property (p_no_x_on_meaningful_fields);
 
// MANDATORY — data bytes are checked only where the strobe says they mean
// something. This is the form that is both strict and correct.
property p_no_x_on_enabled_bytes(int b);
  @(posedge clk) disable iff (!rst_n)
    (accept && payload.strb[b]) |-> !$isunknown(payload.data[8*b +: 8]);
endproperty

Two properties, and the second is the interesting one.

Qualifying the data check by the strobe is what makes it possible to be strict about the bytes that matter without firing on the bytes that do not. The strobe exists precisely to say which bytes are meaningful, so it is exactly the right qualifier — and a design that gets its strobe wrong now fails an X-check, which is a bonus.

Why the meaningful-field list is short and specific. Every field in it is one the receiver interprets. A field the receiver ignores can be anything, and asserting otherwise is §15.

15. Wrong X-Check — Every Bit, Always

// WRONG — the entire payload, unconditionally.
property p_no_x_anywhere;
  @(posedge clk) disable iff (!rst_n)
    accept |-> !$isunknown(payload);
endproperty

Why this is wrong and not merely strict. Unused data bytes under a partial strobe are legitimately X. Reserved metadata bits are legitimately X. In a gate-level or power-aware simulation, X on an unused path is expected.

The property fires constantly on legal stimulus, and all three available responses are bad.

It gets waived, and the waiver is written broadly enough to cover the real X too.

It gets disabled, and the boundary loses X-checking entirely — including on the fields that matter.

Or the design is changed to drive don't-care bits to zero. That costs area and power, adds toggling on a die-to-die interface where toggling is the expensive thing, and removes the one signal that would have shown an uninitialised path.

The general principle, and it is bigger than X-checking. A check that fires on legal stimulus does not make verification stricter; it makes the report unreadable — and an unreadable report is where real failures go to be ignored. Every property in this chapter should be tested against known-good stimulus first, and one that fires there is wrong regardless of how sound its intent was.

16. Rules Per Boundary

The verification plan, in one table. Each row is a boundary; each entry is a rule that lives there and nowhere else.

17. Plane 1 — Structural Validity

Cheap, local, bindable, and the plane most likely to be complete. Every property is evaluated at one boundary from signals available at that boundary.

// ILLUSTRATIVE. The plane-1 set for one boundary. Note that all of them are
// local: no model, no history beyond a few cycles, no far-end observation.
 
// Framing: an object's beats are contiguous and correctly bracketed.
property p_framing_contiguous;
  @(posedge clk) disable iff (!rst_n)
    (accept && payload.first && !payload.last)
      |=> (!accept || !payload.first) until_with (accept && payload.last);
endproperty
 
// No acceptance for a protocol that is not enabled in the ACTIVE config.
property p_no_accept_disabled_protocol;
  @(posedge clk) disable iff (!rst_n)
    accept |-> cfg_active_q.proto_en[payload.cls];
endproperty
 
// Legal class index — the parameter-derived bound (19.6 §47).
property p_class_in_range;
  @(posedge clk) disable iff (!rst_n)
    accept |-> (payload.cls < NUM_CLASSES);
endproperty
 
// A state machine only takes arcs that exist. One property per FSM.
property p_link_state_legal_arc;
  @(posedge clk) disable iff (!rst_n)
    $changed(link_state_q) |-> legal_arc(1'($past(link_state_q)), link_state_q);
endproperty

Two notes on what belongs here and what does not.

Anything requiring history beyond a bounded window is not plane 1. "This identity was not reused within the outstanding window" needs a model of what is outstanding, so it is plane 3. The distinction matters because plane-1 properties can be bound by an integrator with no environment (19.6 §48), and a property that secretly needs a model cannot.

And legal_arc must be an independent function. 19.6 §13's rule: if it is the design's own next-state function, the property asserts that the FSM agrees with itself.

18. Plane 2 — Resource and Accounting

Everything that is counted, reserved or allocated, and the plane where bounds are the weak check and conservation is the strong one.

THE RESOURCE MODEL'S STATE, per class, per direction. Every value is derived
from OBSERVED events (§8), never read from a design register.
 
  advertised            from observed advertisements, tagged by link epoch
  consumed              counted at observed EV_CREDIT_CONSUMED
  returned              counted at observed EV_CREDIT_RETURNED
  expected_credit       = advertised - consumed + returned
  occupancy             from observed arrivals minus observed releases
  outstanding_sem       observed EV_SEM_ACCEPTED minus EV_SEM_COMPLETED
  live_replay           observed EV_OBJ_COMMITTED minus resolutions
 
CHECKS:
  C1  expected_credit matches the design's counter        -- a wrong adder
  C2  live claims <= capacity                             -- 19.5 §54
  C3  occupancy <= depth, per structure                   -- overflow
  C4  outstanding_sem <= the table's capacity             -- 19.2 §16
  C5  live_replay <= replay depth                         -- 19.3 §22
  C6  every conservation identity closes                  -- the strong check

Why C6 is the one that finds bugs. 19.5 §53 made the argument in full: every silent flow-control bug keeps the counter inside its legal range. A leak descends through legal values; a duplicate ascends through legal values; a straggler after recovery may land inside the bound. Bounds catch the gross failures and conservation catches the accounting failures, and the accounting failures are the ones that reach silicon.

What plane 2 uniquely catches that no other plane does: stranded resources. A resource that is neither in use nor available — an outstanding-table entry whose operation was completed but never retired, a replay slot whose object resolved but was not freed — produces no wrong data and no error. It produces a slow, monotonic reduction in capacity, and the only thing that sees it is a model that knows how many of each resource should be live.

19. Plane 3 — Ordering and Identity

The plane where wrong data is delivered as correct data.

THE SEMANTIC MODEL'S STATE, per operation, keyed by the MONITOR TAG (§23).
 
  mon_tag           unique for the whole simulation
  sem_id_observed   what the design used, which may be reused later
  generation        19.2 §22's aliasing guard, as observed
  accepted_cycle
  expected_response_class
  parts_expected    for multi-object operations (19.2 §32)
  parts_seen        a BITMAP, not a counter
  ordering_group    which operations this one must not overtake
  cfg_epoch_at_accept
 
CHECKS:
  O1  every response is attributable to a LIVE operation
  O2  no operation receives two responses
  O3  an identity is not reused while its previous holder is live
  O4  required orderings hold within an ordering group
  O5  each part of a multi-object operation completes exactly once
  O6  no operation's configuration epoch changes during its lifetime

Three notes.

O1 is the property that catches the most expensive bug class. A response matched to a retired operation's identity delivers one operation's data to another's requester (19.2 §29, 19.2 §21). Nothing reports an error; the requester acts on the data.

O3 needs the model's own tag, not the design's identity. Checking "an identity is not reused" using the identity as the key is circular — the model must know which operation held it, and only the tag distinguishes two operations with the same reused identity. §24 is what happens without it.

And parts_seen is a bitmap for the same reason it is a bitmap in the design. 19.2 §33: a counter cannot distinguish "part 2 arrived twice" from "parts 2 and 3 arrived once each". The model must be able to, or O5 is unverifiable. This is the ninth appearance of bitmap, not counter in this curriculum, and the first on the verification side.

20. Plane 4 — Reliability and Exactly-Once

The plane that cannot be checked from one observation point, and the one most often assumed rather than verified.

Three properties, stated precisely, because imprecise versions of them are unverifiable:

P1 — No delivery of a failed object. An object whose integrity verdict was negative is never delivered semantically to the far end's client.

P2 — A retransmission does not duplicate a semantic action. However many physical attempts a semantic operation generates, the far end's client observes it exactly once.

P3 — Recovery preserves what must survive. State whose meaning outlives a link event is present, and equal, after the recovery.

Why P2 must be stated in terms of two different object levels. 19.2 §4's hierarchy: a semantic obligation may produce several transport objects, each of which may produce several physical attempts. "Exactly once" is false at the attempt level, false at the object level under retransmission, and true only at the semantic level. A property written at the wrong level is either vacuous or falsely failing — and §55 is what that looks like in practice.

Why P3 needs a list rather than a blanket statement. 19.6 §27's reset matrix is that list, and the verification counterpart is one property per row. A blanket "state survives recovery" is wrong — link training state must not survive — so the useful property set is the matrix, checked row by row.

And what plane 4 needs that no other plane needs: a far-end observation. All three properties relate an event at one end to an event at the other. An environment with only near-end visibility can check that the design believes it delivered exactly once, which is a much weaker statement and must be labelled as such.

21. Plane 5 — Liveness and Progress

The plane where every safety check passes and the link has stopped.

Module 19 produced four distinct liveness failures, and they are worth listing together because they look identical from outside:

Two properties of this table.

All four present as "zero credit, link stopped". The distinguishing observables are all model state, not design state — which is why plane 5 needs the resource model and cannot be done with assertions alone.

And all four are unreachable by random stimulus. Each needs a burst followed by a quiet period, or a sustained asymmetric load. A regression that only runs saturating random traffic will not find any of them, which is why §59's coverage model has explicit bins for the quiet-period cases.

22. Three Objects, Three Models

19.2 §4's hierarchy is not just a design structure — it is the verification environment's structure.

Three consequences for the environment.

Each level needs its own identity space, and they are not interchangeable. A single "transaction ID" flattening all three is the most common structural mistake in a layered verification environment — it forces every check to be written at one level, and two of the three levels then have no checkable properties.

The ratios between levels are themselves checkable. Semantic operations to transport objects should be 1:1 unless the operation was fragmented; transport objects to physical attempts should be 1:1 unless there was a retransmission. A ratio anomaly with no corresponding fragmentation or retry event is a bug, and it is detectable without knowing anything about payloads.

And the levels have different lifetimes. A physical attempt's record can be discarded once its verdict is known; a transport object's persists until resolution; a semantic obligation's persists until completion, which may span several recoveries. An environment that ages out records on one timescale loses the long-lived ones.

23. The Join Key

How does the environment know that an event at the protocol boundary and an event at the link boundary refer to the same work?

Not by any field on the wire. The design's identities are reused, remapped between layers, and absent entirely at some boundaries.

// ILLUSTRATIVE. The monitor's own identity, allocated once and propagated
// through the models. It exists in NO design register and on NO wire.
int unsigned next_mon_tag = 0;
 
// Allocated at the FIRST observation of a new unit of work.
function automatic int unsigned new_tag();
  return next_mon_tag++;
endfunction

How the tag propagates when the wire carries no tag. The environment maintains a correspondence, built from the observable structure of the flow:

• at the protocol boundary, a new operation gets a new tag;
• when a transport object is observed being formed, the environment associates it with the operation whose object it is — derivable from the boundary ordering and the class, since the Adapter accepts objects in a determinable order per class;
• when an attempt is observed, it inherits its object's tag;
• at the far end, the arriving object is matched by its transport identity, which the protocol does carry between the two Adapters.

Two honest caveats, and both must be documented.

The correspondence is an inference, not an observation, at any boundary where the association is not directly visible. If that inference is wrong the environment reports false failures, so it needs its own sanity checks — a tag associated with two operations, or an object with no tag, is an environment bug and should be reported as one rather than as a DUT failure.

And where the inference cannot be made at all, the environment must degrade to counting rather than matching, and say so. A count-based check is genuinely weaker — it catches "too many" and "too few" but not "the wrong one" — and labelling it correctly is the difference between a known limitation and a false sense of coverage.

24. Wrong Join — Using a Protocol Field as the Identity

WRONG:  key the scoreboard on the design's transaction identity.

Worked. Operation A is issued with identity 7, completes, and is retired. Identity 7 is legitimately returned to the free pool and reallocated to operation B. A delayed response for A arrives after B was allocated.

What the model with a wire-field key concludes. Identity 7 is live, a response arrived for identity 7, the response is matched to operation B. The model marks B complete with A's data — and reports nothing wrong, because from its point of view everything matched.

Three consequences.

The model has reproduced the design's bug rather than detecting it. 19.2 §21 is exactly this failure in RTL, and a wire-keyed model makes the identical mistake for the identical reason: an identity is not unique over time.

The check that would have caught it becomes uncheckable. "An identity is not reused while its previous holder is live" requires distinguishing the two holders. With the identity as the key there is only one holder.

And a generation field does not fully rescue it. 19.2 §22's generation counter narrows the window enormously and is the right design mechanism — but the generation is finite and wraps, and the model has no reason to accept a finite guard when it can have an infinite one. The monitor's own tag never wraps and never aliases.

The rule. The design's identity is data to be checked, not a key to check with. Record it, assert properties about it, and join on something the design cannot influence.

25. Safety and Liveness

Two categories, two shapes, two failure modes — and conflating them is why liveness checking is usually absent.

Two consequences that shape the whole plan.

A safety-only plan cannot detect a deadlock. 19.5 §42's stranded link violates nothing: every register is legal and stable forever. The absence of liveness properties is not a gap in coverage; it is a gap in what the plan is capable of expressing.

And liveness properties are always conditional. "Every request eventually completes" is false if the downstream never accepts, and that is legal environment behaviour. The property is only meaningful together with its assumptions, which is §28.

26. Wrong Liveness Assertion — No Assumptions

// WRONG — true of no real system.
property p_req_eventually_granted;
  @(posedge clk) disable iff (!rst_n)
    req |-> s_eventually grant;
endproperty

Why it fails. A downstream consumer may legally stall indefinitely. A link may legitimately remain in recovery. A peer may legally be slow. Under any of those, the property fails — and the design is correct.

What happens next is the actual damage, and it happens in this order.

The property fails in regression. Somebody investigates and finds the environment stalled the consumer.

The property is deemed "noisy" and disabled. Or it is weakened to ##[1:1000000] grant, which is the same thing with extra steps.

Liveness checking is now absent from the plan, and it was the only thing capable of finding four of Module 19's failures (§21).

The chain from "we wrote a liveness property" to "we have no liveness checking" takes about two weeks and one regression. The property was not wrong in intent — it was incomplete, and the missing half is the assumptions.

27. The Bounded Form

// The form that works in simulation: a BOUND, with the number derived rather
// than guessed, and the derivation written in the comment.
//
//   bound = arbitration worst case          (NUM_CLASSES-1) * MAX_GAP
//         + link round trip                 RTT_MAX
//         + one recovery                    RECOVERY_MAX
//         + the peer's response budget      PEER_RSP_MAX
localparam int COMPLETION_BOUND = (NUM_CLASSES-1)*MAX_GAP + RTT_MAX
                                + RECOVERY_MAX + PEER_RSP_MAX;
 
property p_request_completes_within_bound;
  @(posedge clk) disable iff (!rst_n)
    sem_accept |-> ##[1:COMPLETION_BOUND] (sem_complete || sem_failed);
endproperty
a_request_completes_within_bound:
  assert property (p_request_completes_within_bound);

Four reasons the bounded form is better in simulation than s_eventually.

It fails at a specific cycle, so the waveform shows the moment progress stopped rather than the end of the run.

The bound is a number that was derived, and the derivation is the valuable part. Writing the comment above forces somebody to enumerate every source of delay — and that enumeration is frequently where a missing delay source is discovered, before any test is run.

It catches slow progress, not just no progress. A design that completes in ten times the expected time is not deadlocked and is broken. s_eventually passes; the bound fails.

And it is checkable at the end of a finite run, which s_eventually is not without tool-specific configuration that is easy to get wrong and easy to lose.

The cost is honest and worth stating: the bound may be wrong. Too tight and it fires falsely; too loose and it misses slow progress. Both are visible and fixable, which is more than can be said for a liveness property that was disabled.

28. Assumption Discipline

Every liveness property carries a list of assumptions, and the list is part of the property.

// The assumptions, written down, next to the property they support.
//
//  A1  the clock runs and reset is not re-asserted
//  A2  the downstream consumer eventually accepts
//  A3  the peer eventually responds to a delivered object
//  A4  injected errors eventually stop
//  A5  the link eventually exits recovery
//  A6  a requester that is eligible remains eligible until served
//
// In formal, these are assume properties. In simulation, they are constraints
// on the environment — and in BOTH cases they must be written down.
assume property (@(posedge clk) s_eventually downstream_ready);
assume property (@(posedge clk) s_eventually !error_injection_active);
assume property (@(posedge clk) s_eventually (link_state != LNK_RECOVERY));

Three rules about assumptions.

Each one must be justified by something in the real system. A2 is true because the real consumer is a memory controller that drains. A4 is true because a link with a permanent error rate is a broken link, not a case to prove liveness under. An assumption with no real-world justification is a property that was weakened until it passed, and the review question for every one is: what makes this true in silicon?

An assumption that is not true in the real system is a bug report, not an assumption. If A3 does not hold — if a peer can legitimately never respond — then the design needs a timeout, and the liveness property should be about the timeout firing rather than about the response arriving.

And assumptions must be visible in the results. A regression that reports "all liveness properties passed" without reporting which assumptions were active has reported almost nothing. The assumption list belongs in the regression summary, because tightening an assumption is how a liveness property is quietly made vacuous.

29. Environment Assumptions Are Not Design Properties

A category error worth naming, because it is easy to make and hard to see afterwards.

// WRONG — asserting an environment behaviour as though it were a DUT property.
a_downstream_eventually_ready:
  assert property (@(posedge clk) s_eventually downstream_ready);

What this does. It reports a failure of the testbench as a failure of the design. The design did nothing; the environment stalled.

Four consequences.

Failure triage goes to the wrong team, and stays there until somebody reads the property.

Real failures are camouflaged. Once the assertion report contains environment failures, the signal-to-noise ratio drops, and the response is to filter the report — which filters real failures with the same name.

And in formal it is worse than useless — it is unsound in the direction that matters. An assert on an environment behaviour makes the proof attempt fail on traces the environment would never produce; the natural fix is to constrain the environment, and if that constraint is written as an assert instead of an assume the tool has been told the design guarantees something it does not. Every property proved under it is proved under a false hypothesis.

The fourth consequence is the subtle one. The boundary between "what the design guarantees" and "what the environment provides" is itself a specification. Writing it down as assume-versus-assert is how that specification gets recorded. A plan where everything is an assert has no record of the interface contract at all — and the first integration into a system with a different environment discovers it empirically.

The rule. assert what the design must guarantee. assume what the environment provides. Never blur them, and review the assume list as carefully as the assert list — because an over-strong assumption is how a proof becomes meaningless without anybody noticing.

30. The Independent Semantic Model

THE SEMANTIC MODEL. Its inputs are OBSERVED EVENTS, and its rules come from
the CONTRACT, not from the design.
 
STATE, per operation (keyed by mon_tag):
  kind, class, ordering group
  accepted_cycle, cfg_epoch_at_accept
  parts_expected (bitmap), parts_seen (bitmap)
  expected_completion_kind
  status: OUTSTANDING | COMPLETED | FAILED
 
TRANSITIONS, each triggered by an OBSERVED event:
  EV_SEM_ACCEPTED   -> create, status OUTSTANDING
  EV_OBJ_DELIVERED  -> mark the corresponding part seen
  EV_SEM_COMPLETED  -> require all parts seen; status COMPLETED
  (a failure indication) -> status FAILED, with a reason
 
WHAT IT ASSERTS:
  - a completion arrives only for an OUTSTANDING operation
  - an operation completes exactly once
  - all expected parts were seen before completion
  - the completion kind matches what this operation kind requires
  - no operation stays OUTSTANDING beyond the bound of §27

Three properties of a model built this way.

Its rules are derivable from the contract by somebody who has not read the RTL. "A completion arrives only for an outstanding operation" is a statement about the protocol, not about the design's table. That is the test for whether a model is independent, and it is checkable by asking a colleague to derive the rule from the interface document alone.

It holds expectations, not mirrors. The model does not track the design's sem_table_q; it tracks what the contract says should be true. When the two disagree, that is the finding — and the model has no opinion about which one is right, which is exactly the neutrality wanted.

And it must be able to say "I do not know". An operation whose completion is architecturally optional, or whose ordering is unconstrained, must be modelled as unconstrained rather than as some specific expectation. A model that guesses generates false failures, and false failures cost more credibility than missed bugs cost coverage — because a team that stops trusting the scoreboard has lost every check in it.

31. Wrong Reference Model — the Mirror

WRONG:
  on the design's sem_alloc signal      -> model.create()
  on the design's sem_complete signal   -> model.complete()
  check: model.outstanding == design.outstanding_count

What this checks: that the design's counter is consistent with the design's own event signals. It is a check on an adder.

Every interesting bug survives it, and this is the table worth remembering:

Seven bugs, seven layers, one root cause: the model agreed with the design about when things happen, which is the thing most likely to be wrong.

Three practical rules that follow.

Monitors go at boundaries, not at blocks. A monitor tapping a block's inputs has already inherited that block's interpretation of them.

The model's trigger must be nameable in contract terms. "When the client's request handshake completes" is a contract event. "When sem_alloc rises" is not — and if the only way to describe the trigger is by naming a design signal, the model is a mirror.

And where a boundary genuinely cannot be observed, degrade to a weaker check and label it. 19.5 §56 reached the same conclusion: an honest bound beats a circular equality. The label is what stops the weaker check being reported as the stronger one.

32. The Resource Model

THE RESOURCE MODEL. Plane 2. One instance per resource, per class, per
direction — and the per-resource split is what makes the failure identifiable.
 
RESOURCES MODELLED SEPARATELY:
  remote credit           19.5 §55's model
  receive occupancy       per structure
  outstanding operations  19.2 §16's table
  replay entries          19.3 §20's ring
  reassembly contexts     19.3 §35
 
FOR EACH:
  capacity        from the capability structure (19.6 §20), never from RTL
  allocated       counted at the observed allocation event
  freed           counted at the observed release event
  live            = allocated - freed
  high_water      max(live)
  stranded        live entries whose work is no longer outstanding
 
CHECKS:
  live <= capacity                    -- overflow
  stranded == 0                       -- the leak check, and the valuable one
  high_water reported, not asserted   -- sizing evidence (19.4 §54)

Why stranded is the check worth building. A leaked resource is neither an overflow nor an error. It reduces capacity permanently and silently, and the only way to detect it is to compare the resources believed live against the work believed outstanding. No design assertion can do this, because the design believes the entry is legitimately allocated — that belief is the bug.

Why capacity comes from the capability structure. 19.6 §20's read-only capability registers are the elaborated parameters made observable. Taking capacity from there rather than from a testbench constant is what makes the model survive §35's parameter mutation — and 19.6 §53 is what happens otherwise.

And why the resources are modelled separately rather than as one pool. They fail independently and their failures need different responses. An aggregate "resources exhausted" report is 19.4 §39's conflated stall bin, where a replay-depth problem and a staging-depth problem are indistinguishable and need opposite fixes.

33. The Reliability Model

THE RELIABILITY MODEL. Plane 4. It is the only model that spans both ends,
which is why it needs the far-end observation point of §6.
 
STATE, per transport object (keyed by mon_tag):
  attempts           [] cycle and verdict of each physical attempt
  first_arrival      when the far end first received it
  deliveries         [] every semantic delivery observed at the far end
  resolution         how and when it was resolved
  spanned_recovery   whether a recovery occurred in its lifetime
 
CHECKS:
  R1  |deliveries| == 1 for every object whose semantic operation completed
  R2  no delivery follows a NEGATIVE verdict for that same attempt
  R3  attempts > 1 implies an observed retry trigger  -- no spontaneous retries
  R4  an object retained across recovery is re-attempted, not dropped
  R5  an object delivered before a recovery is NOT re-delivered after it
  R6  a resolution is observed for every committed object, within the bound

Three notes.

R1 is the exactly-once property, and its subject is the semantic level. An object may be attempted five times; it must be delivered once. Writing R1 at the attempt level makes it vacuously false; writing it at the object level makes it false under legitimate retransmission (§55).

R5 is the property people forget, and it is the one 19.4 §51's global-flush bug violates from the other direction. A recovery that re-baselines too aggressively causes the peer to retransmit objects that were already delivered — and if the duplicate window was cleared by the same recovery, the duplicate is delivered a second time. Two mechanisms, both correct-looking, one duplicate.

And R3 is a negative property that catches a whole class of defect cheaply. A retransmission with no observed trigger means the reliability machine retried on its own — a timeout that is too short, a spurious verdict, or a state machine taking an arc it should not. All three are serious and all three produce extra attempts that R1 alone might not catch, because the extra attempt may still result in exactly one delivery.

34. The Configuration and Link-State Model

THE LINK-STATE MODEL. It owns the CONTEXT every other model needs.
 
STATE:
  link_state          from observed management-boundary transitions
  link_epoch          incremented on observed resynchronisation
  cfg_requested / cfg_validated / cfg_active     19.6 §21
  cfg_epoch           incremented on observed commits
  active_lane_mask, configured_mask, structural_max    19.6 §25
  recovery_events     entries, exits, durations, causes
 
CHECKS:
  L1  every state transition is a legal arc     (independent arc function)
  L2  cfg_active is always legal                (independent legality model)
  L3  cfg_active changes only at an observed commit, atomically
  L4  active ⊆ configured ⊆ structural
  L5  every recovery entry has a matching exit, within a bound
  L6  no semantic operation's cfg_epoch changes during its lifetime

Why this model exists separately rather than being folded into the others.

It supplies context that the other three models cannot compute. "Was there a recovery during this object's lifetime?" is a reliability-model question answered from link-state data. "Which capacity applied when this credit was advertised?" is a resource-model question answered from configuration data. Duplicating that state into each model is how the models drift apart.

And L5 is the recovery-convergence property, which is plane 5 living in the link-state model. A recovery that enters and never exits is a hang that looks like a link problem, and it is the failure most likely to be blamed on the PHY when it is a state-machine arc that was never taken.

35. The Layered Scoreboard

Four models, one join, and one output that matters.

THE CROSS-LAYER SCOREBOARD
 
INPUTS:   observed events from four boundaries, each carrying a mon_tag
MODELS:   semantic (plane 3), resource (plane 2),
          reliability (plane 4), link-state (context + plane 5)
 
PER UNIT OF WORK, the scoreboard holds the JOINED VIEW:
 
  mon_tag
  ├── semantic     accepted, parts, completion, ordering group
  ├── transport    objects formed, committed, resolved
  ├── physical     attempts, verdicts, arrivals
  ├── resource     credits charged, entries held, when released
  └── context      cfg_epoch, link_epoch, recoveries spanned
 
CROSS-LAYER CHECKS — the ones no single model can make:
 
  X1  semantic completions == 1 while physical attempts may be many
  X2  every credit charged corresponds to a real remote allocation
  X3  no resource is released before its semantic obligation resolves
  X4  an object that spanned a recovery has consistent state at both ends
  X5  the LAYER OF FIRST DIVERGENCE for any failure  (§60)

X5 is the output that distinguishes this architecture from a flat one. It is not a pass/fail — it is the answer to "where do I start looking", computed by sorting the joined view's events by boundary and finding the earliest boundary at which observation and expectation disagree.

X3 is the check that catches a whole family. 19.5 §22's early credit return, 19.3 §45's retirement on send, 19.4 §36's ping-pong ownership — all three are "a resource was released while an obligation was still live", at three different layers, and the joined view is the only place all three are visible with one property.

36. The Join, and Its Failure Modes

The scoreboard's join is a piece of logic, and it has its own bugs. Three, and each needs its own check.

A tag with no work. An event arrives carrying a tag the scoreboard has never allocated. This is an environment bug — an inference in §23's correspondence went wrong — and it must be reported as one. Reporting it as a DUT failure sends the investigation to the wrong place, and reporting it as nothing loses the evidence that the environment is unreliable.

Work with no tag. An observed object could not be associated with any operation. This may be a DUT bug — a spontaneously generated object — or an environment gap. The scoreboard cannot tell, and should say both.

Two units of work with one tag. An inference collapsed two operations. This is always an environment bug, and it silently hides DUT failures by merging two histories into one.

The rule. The scoreboard must check its own join before it checks the design, and report join anomalies in a separate category. An environment whose join fails silently reports passes it has not earned — and it is the one failure mode a verification report cannot detect from its own output.

37. Wrong Scoreboard — One End-to-End Model

WRONG:
  observe the client's requests
  observe the client's completions
  check: every request completed with the right data

This is not useless. It is the highest-level correctness statement and it must be present.

What it cannot do is tell you anything when it fails.

Worked, on one failure. A completion arrives with wrong data. The end-to-end scoreboard reports: "operation 4,127 completed with unexpected data."

What is now unknown:

• was the request corrupted before transmission, or the response after?
• was it duplicated and did the second copy overwrite?
• was it matched to another operation's response?
• did a recovery occur in its lifetime?
• was any integrity mechanism triggered?
• did any resource run out?

Six questions, six subsystems, one data point.

Four properties of the flat approach.

Debug time scales with the depth of the stack. Three layers means three candidate layers per failure, and each elimination is a separate simulation with added probes.

Some failures are invisible to it entirely. A stranded resource, a leaked credit, a duplicate suppressed by luck rather than by design — none of these changes the client-visible outcome, so an end-to-end check reports a clean pass on a design that is accumulating a fatal condition.

And intermittent failures become unreproducible. A failure that requires a specific interleaving is reported at the client boundary long after the interleaving happened. The layered environment recorded the divergence at the moment it occurred, so the failing run's own log contains the answer.

The fourth property is the one that decides the architecture. The flat scoreboard is cheap and the layered one is not — four monitors, four models, a join and its own checks. The layered one pays for itself the first time it turns a two-week silicon debug into a two-hour one, and that is not a hypothetical: it is the difference between "the link returns wrong data" and "the Adapter formed two transport objects for one semantic operation with no retry trigger."

38. Exactly-Once, at the Right Level

"Exactly once" is true at one level of §22's hierarchy and false at the other two. Stating it at the wrong level produces either a vacuous property or a false failure.

Two refinements the correct statement still needs.

"Delivered" must mean semantically delivered, not arrived. 19.3 §30's delivery gate exists precisely because arrival and delivery are different events separated by an integrity verdict and a duplicate check. An object can arrive twice and be delivered once, which is the mechanism working.

And an operation that failed was delivered zero times, which must also be checkable. The complete property is therefore three-valued: exactly one delivery, or zero deliveries with an explicit failure reported to the originating client. A design that delivers zero times and reports success has lost work silently — the worst outcome — and a two-valued property does not express it.

39. SVA — Exactly-Once and the Delivery Gate

// MANDATORY. Delivery at most once per semantic operation, keyed on the
// MONITOR TAG (§23) because the design's identity is reused.
property p_delivered_at_most_once(int unsigned tag);
  @(posedge clk) disable iff (!rst_n)
    (deliver_fire && (deliver_tag == tag))
      |=> always !(deliver_fire && (deliver_tag == tag));
endproperty
 
// MANDATORY — nothing is delivered before its integrity verdict is known.
// This is the property 19.3 §31's design violates.
property p_no_delivery_before_verdict;
  @(posedge clk) disable iff (!rst_n)
    deliver_fire |-> (verdict_valid && verdict_good);
endproperty
a_no_delivery_before_verdict: assert property (p_no_delivery_before_verdict);
 
// MANDATORY — a negative verdict is never followed by a delivery of that
// same object. The EFFECT form, which survives a redesign of the gate.
property p_bad_verdict_never_delivered(int unsigned tag);
  @(posedge clk) disable iff (!rst_n)
    (verdict_valid && !verdict_good && (verdict_tag == tag))
      |=> always !(deliver_fire && (deliver_tag == tag) && !redelivery_authorised);
endproperty
 
// MANDATORY — every accepted operation reaches a terminal state. The
// three-valued form of §38.
property p_operation_terminates(int unsigned tag);
  @(posedge clk) disable iff (!rst_n)
    (sem_accept_fire && (sem_tag == tag))
      |-> ##[1:COMPLETION_BOUND] ((complete_fire && (complete_tag == tag))
                               || (fail_fire     && (fail_tag     == tag)));
endproperty
 
// MANDATORY, and the one most often missing — a completion is never reported
// for an operation the environment believes failed, and vice versa.
property p_no_success_after_failure(int unsigned tag);
  @(posedge clk) disable iff (!rst_n)
    (fail_fire && (fail_tag == tag))
      |=> always !(complete_fire && (complete_tag == tag));
endproperty

Five properties, and the split between cause and effect forms is deliberate.

p_no_delivery_before_verdict is a cause check — it names the gating condition. p_bad_verdict_never_delivered is an effect check — it says what must not be observed, without naming how it is prevented. A design and a testbench that share the same misconception about what verdict_valid means will both satisfy the first and only the second can catch them, which is 19.5 §23's argument in a new place.

Why p_no_success_after_failure matters more than it looks. The dangerous direction is a late success after a reported failure: the client has already taken its error path, freed its buffers, and possibly reissued the operation. A late completion then writes into a freed buffer or duplicates the reissued work — and nothing in the exactly-once property catches it, because it is exactly one delivery.

40. Ordering — What Is Required and What Must Not Be Assumed

The most common ordering mistake in a verification environment is not a missing check. It is an assumed one.

A model that expects responses in request order will report false failures on every legitimately reordered response — and the response is to weaken the check until it passes, which usually removes the real ordering requirement along with the false one.

The discipline: for every pair of operations, the environment must know which of three relationships holds.

Three notes.

The third row is the honest one and it is usually where the truth is. Ordering rules between different protocol classes, between a posted and a non-posted operation, or across a recovery are frequently not derivable from public material. Recording "unordered, because I could not establish otherwise" is correct; assuming an ordering and asserting it produces false failures, and assuming none where one exists misses real bugs. Only the first is honest, and only the first survives review.

Covering both orders in the second row is not optional. If A-then-B and B-then-A are both legal but only one ever occurs in regression, the design has been verified for one of them. 19.2 §51's reordered-response trace exists to force the other.

And ordering is per group, not global. Operations in different ordering groups have no relationship at all, and a model with one global order has invented constraints between unrelated work.

41. SVA — Response Matching and Ordering

// MANDATORY. A response is attributable to a LIVE operation. The single
// highest-value ordering property, and 19.2 §30's check at the environment
// level rather than inside the engine.
property p_response_to_live_operation;
  @(posedge clk) disable iff (!rst_n)
    rsp_fire |-> model_is_outstanding(rsp_tag);
endproperty
a_response_to_live_operation: assert property (p_response_to_live_operation);
 
// MANDATORY — a response's class and kind match what its operation expects.
// Catches a correctly-matched response carrying the wrong payload shape.
property p_response_kind_matches;
  @(posedge clk) disable iff (!rst_n)
    rsp_fire |-> (rsp_kind == model_expected_kind(rsp_tag))
              && (rsp_cls  == model_class(rsp_tag));
endproperty
 
// MANDATORY — required precedence within an ordering group.
property p_precedence_within_group(int unsigned a, int unsigned b);
  @(posedge clk) disable iff (!rst_n)
    (model_requires_precedence(a, b) && complete_fire && (complete_tag == b))
      |-> model_is_complete(a);
endproperty
 
// MANDATORY — an identity is not reused while its previous holder is live.
// Keyed on the DESIGN identity but checked against the MODEL's liveness,
// which is what makes it non-circular (§24).
property p_identity_not_reused_early;
  @(posedge clk) disable iff (!rst_n)
    (sem_accept_fire) |-> !model_identity_live(sem_id_observed);
endproperty
a_identity_not_reused_early: assert property (p_identity_not_reused_early);

Two notes on construction.

p_identity_not_reused_early is the interesting one. It uses the design's identity as the subject — because reuse of that identity is the thing being checked — while liveness comes from the model, which is keyed on tags. That combination is what makes it a real check: keyed on the identity alone it would be circular (§24), and keyed on tags alone it would not be about identity reuse at all.

And p_response_kind_matches catches a failure p_response_to_live_operation does not. A response can be matched to a genuinely live operation and still be the wrong kind of response — a completion where data was expected, a partial response for an operation that requires a whole one. The identity was right and the content was wrong, which is a different bug in a different block.

42. Negative Testing

Half of a protocol contract is what must be rejected. A plan that only exercises legal stimulus has verified the design's happy path and none of its defences.

Four categories, and each needs its own mechanism.

Three rules.

Each negative test names the expected behaviour, and it must be specific. "Does not crash" is not an expected behaviour — "is rejected with ERR_PROTOCOL within N cycles, with the first-error record naming the boundary" is. §44 is what happens with the vague form.

Illegal stimulus must be deliberately generated, which means the environment needs a way to emit stimulus its own checkers would flag. A constrained-random generator that cannot produce illegal stimulus cannot test the defences, and the usual consequence is that the defences are never exercised until a real peer produces something unexpected.

And the adversarial-timing row is where the cheapest real bugs are. A stall injected at every cycle of every handshake finds §13's stability violations, 19.2 §39's skid-buffer bugs, and 19.5 §18's consume-on-valid leak. It costs a random-stall generator and it exercises boundary logic that ordinary traffic never stresses.

43. The Error-Injection Architecture

INJECTION POINTS, chosen so each one exercises a DIFFERENT recovery mechanism.
 
  1  client boundary       illegal requests, malformed framing
  2  protocol -> adapter   objects with bad class, bad framing
  3  transmit path         corrupt an object AFTER integrity is computed
  4  the link              corrupt bits, drop an object, delay an object
  5  return path           drop a credit return, duplicate one, delay one
  6  far end               refuse to respond; respond twice; respond late
  7  management            force a recovery; force a config change mid-traffic
 
FOR EACH INJECTION, THE PLAN RECORDS:
  - what was injected, at which cycle, on which object (by mon_tag)
  - which detection mechanism SHOULD fire
  - which recovery SHOULD occur
  - what the models expect afterwards
  - which properties should REMAIN true throughout

Three notes on the injection points.

Point 3 is the one that verifies integrity is actually protecting something. Corrupting before integrity is computed produces a well-formed object with a valid check over corrupt data — which tests nothing about the integrity mechanism, because the mechanism faithfully protected the corruption. Corrupting after is what exercises detection.

Point 5 is the flow-control injection nobody builds, and it is where 19.5 §24's duplicate-return and 18.4 §20's lost-return failures live. Dropping a credit return produces a link that slowly stops with every safety property passing, and only a conservation model detects it.

And point 7 is the one that produces cross-feature bugs. 19.5 §29's straggler, 19.2 §44's cleared semantic table and 19.6 §23's partial commit are all failures at the intersection of two features that are usually verified separately. A recovery forced during live traffic with a configuration change in flight is one test that covers all three intersections.

44. Wrong Negative Test — Inject and Check Nothing Broke

WRONG:
  inject a bit error
  run for 1000 cycles
  check: no assertion fired, simulation completed
  PASS

What this actually verified: that the design did not crash.

Four things it did not verify.

That the error was detected. If the integrity mechanism missed it, nothing fired — and "nothing fired" was the pass criterion. The test passes most convincingly when the detection is completely broken.

That the recovery occurred. If the design silently discarded the object and continued, no assertion fires and the semantic operation never completes. Unless the test checks that the operation reached a terminal state, a silently dropped object is a pass.

That the work was not lost or duplicated. The whole point of the reliability mechanism is that the object is eventually delivered exactly once. A test that does not check the delivery has not tested reliability at all — it has tested that error injection does not cause a crash.

And that the design's own report is correct. The first-error record should name the class, the boundary and the object. A test that does not read it leaves the entire diagnostic path unverified, and the first time anybody depends on that path is during a silicon debug.

The rule. Every negative test asserts a positive outcome. Not "nothing bad happened" — this specific detection fired, this specific recovery ran, this specific object was delivered exactly once afterwards, and this specific error record has these specific contents. A negative test whose pass criterion is the absence of failures is indistinguishable from a test that did not run.

45. Vacuity — the Property That Passes and Checks Nothing

An implication whose antecedent never occurs passes every cycle and checks nothing.

// This property passes 100% of a regression in which replay is disabled.
property p_replay_preserves_order;
  @(posedge clk) disable iff (!rst_n)
    replay_active |-> ordering_preserved;
endproperty

Four ways vacuity arises, and only the first is obvious.

A feature is disabled in the configuration under test. Every property about that feature is vacuous. In a parameterised design this is the norm rather than the exception (19.6 §35), and a regression across configurations has a different vacuity profile in each one.

The antecedent is unreachable for a subtler reason. A property gated on error_detected && recovery_active is vacuous in every run where errors are injected only while the link is healthy. Nobody notices, because the property is in the report as passing.

A disable iff covers the interesting window. A property disabled during recovery cannot check recovery behaviour — and that is exactly the class of property most likely to be written with disable iff (!rst_n || recovery_active) by somebody who was tired of it firing during recovery.

And an over-strong assume in formal removes the traces that would have exercised it (§29). The proof succeeds because the interesting behaviour was assumed away.

The mechanism against all four:

// For EVERY implication property, a cover for its antecedent.
c_replay_active_occurred: cover property (@(posedge clk) replay_active);
c_replay_and_ordering:    cover property (@(posedge clk)
                            replay_active ##[0:100] ordering_check_point);

The rule. A property without a cover for its antecedent is a property that has never been shown to check anything. The regression report must show both — assertions passing and their antecedents having occurred — and a passing assertion with an uncovered antecedent is a red row, not a green one.

46. Cover Properties and Assertion Coverage

Three kinds of coverage, and they answer three different questions.

The third is the one most environments do not collect, and it catches a specific, embarrassing failure. A property that is never bound — because the bind statement's path is wrong, or the module was renamed, or a generate branch removed the instance — reports nothing and appears in no report. It is not failing and it is not passing; it does not exist. A pass count of exactly zero, reported per property, is the only thing that finds it.

And the three must be read together. A property with a high pass count, a covered antecedent and no failures is genuinely checked. A property with a high pass count and an uncovered antecedent is a vacuous property being counted as evidence — and the pass count makes it look like the most thoroughly verified property in the report.

47. Formal or Simulation — Choosing Per Property

Three notes.

Formal is strongest exactly where the failures are rare orderings, which is most of Module 19's simultaneous-event bugs: 19.5 §13's consume-and-return, 19.3 §24's allocate-and-retire, 19.4 §16's payload-and-metadata. These need one specific cycle in which two things happen; simulation reaches them by luck, formal by construction.

Simulation is unavoidable wherever a payload is involved, because a reference model with data is a program, not a property.

And the split must be recorded per property, in the plan. A property that is "covered by formal" and was never actually run in formal — because the proof did not converge and was bounded to depth 12 — is covered to depth 12 and nowhere else. The plan must record the bound, and a bounded proof is a partial result that should be labelled as one.

48. Bind Architecture and Reused Collateral

19.6 §48 established that the IP ships bindable contract checkers. This chapter is where they are used — and the reuse relationship goes both ways.

// ILLUSTRATIVE. Binding the IP's own contract checkers plus the environment's
// protocol checkers, without modifying the DUT.
bind ucie_link_top ucie_ip_contract_checker #(
  .NUM_CLASSES (NUM_CLASSES),
  .TX_DEPTH    (TX_DEPTH)
) u_contract_chk (.*);
 
bind ucie_adapter ucie_adapter_protocol_checker u_adapter_chk (.*);

Three properties of this arrangement.

Plane-1 properties come with the IP; planes 2 to 5 come with the environment. The IP vendor knows its boundary contracts and can ship checkers for them. It cannot ship a semantic model, because that depends on the client's protocol and the system's ordering requirements.

The environment must not duplicate the IP's checkers. Two sets of stability assertions on the same boundary means two failures per violation and twice the triage. Bind the vendor's and add what they do not cover — and if the vendor's set is inadequate, that is feedback to the vendor rather than a reason to write a shadow set.

And the bind paths are configuration-dependent. 19.6 §15's stable-boundary rule matters here: a generate branch that removes an instance breaks the bind that targets it, silently, producing §46's zero-pass-count property. This is one of the concrete costs of an unstable boundary, and it lands on the verification team rather than the design team.

49. Verifying the Verification Environment

A monitor is logic. A model is a program. Both have bugs, and both fail in the passing direction.

Five checks the environment must run on itself.

Monitor unit tests. Drive a stalled handshake and confirm exactly one event (§10). Drive a multi-beat object and confirm one object event, not one per beat. A monitor with §11's bug reports duplicates that do not exist, and the resulting false failures teach the team to distrust the real ones.

Join anomaly reporting (§36), in its own category.

Antecedent coverage for every implication property (§45).

Assertion pass counts, to find unbound properties (§46).

And a deliberate-bug regression. Take a known-good design, introduce each of a set of seeded defects, and confirm that each one is caught, and by which check. This is the only direct evidence that the environment can detect anything.

The value of the seeded-defect run is not the pass rate. It is the mapping. Knowing that "an early credit return" is caught by the resource model's conservation check and by nothing else tells you what you lose if that model is disabled — and every environment eventually has a model disabled for performance reasons.

50. The Layer-Composition Problem

UCIe's three layers do not compose into one checkable interface, and that is the central structural fact this chapter is organised around.

Three specific reasons.

The layers have different notions of an object. 19.2 §4's hierarchy again: one semantic obligation, several transport objects, several physical attempts. A property written about "a transaction" is ambiguous until it says which level, and a plan that never disambiguates has properties whose meaning depends on who reads them.

The layers have different reliability guarantees, and the guarantee is configurable. The Adapter optionally provides CRC and retry (§3). So the property "a corrupt object is never delivered" is enforced by the Adapter in one configuration and by the Protocol Layer in another — and in Raw Mode the Adapter is not in the path at all (§51).

And the layers have different epochs. A link recovery voids link-epoch state and not semantic state (19.6 §27). A property that is true across a recovery at one layer is false at another, so disable iff (recovery_active) is right for some properties and catastrophic for others — the ones that check what survives.

What follows for the plan. Every property records which layer's contract it comes from, which configurations it applies in, and what it does across a recovery. A property without those three annotations will eventually be bound in a configuration where it is false, and it will be weakened rather than restricted — which removes it from the configuration where it was valuable.

51. Raw Mode Changes the Architecture

When the Adapter is bypassed, error protection moves to the Protocol Layer — and the verification architecture must move with it.

Three consequences.

Plane-4 properties must be conditional on the configuration, not deleted. A property that asserts the Adapter suppresses duplicates is false in Raw Mode, and binding it there produces a false failure that will be fixed by removing the property from everywhere.

The middle monitor loses most of its value and the outer two gain it. The architecture is the same shape with different weights, which is the argument for building four monitors even in a design that starts Adapter-managed: a later Raw Mode configuration reuses the environment rather than needing a new one.

And a design supporting both modes needs both property sets, mutually exclusive, with cover properties confirming that each set's antecedents actually occurred in the runs where that mode was active (§45). A dual-mode design verified only in one mode has one mode verified, and the coverage report is the only thing that says which.

52. Protocol-Specific and Protocol-Independent Checks

UCIe carries PCIe natively, CXL natively, and streaming protocols. That produces two categories of check that must not be mixed.

Three rules.

Protocol-independent checks must not embed protocol assumptions. A transport-level check that assumes responses return in order has embedded a protocol rule into a transport check — it will be false the first time a protocol that permits reordering is enabled, and the fix will be to weaken the transport check for all protocols.

Protocol-specific checks are the carried protocol's, and they belong to that protocol's verification. Reimplementing PCIe's ordering rules inside a UCIe environment is duplicating a large, subtle, well-specified body of work. Where a protocol VIP exists, use it at the protocol boundary and let this environment check the transport.

And the split determines what a failure means. A protocol-independent failure is a link bug. A protocol-specific failure may be a link bug that corrupted protocol semantics, or a protocol-layer bug, or a client bug — and the layered monitor architecture is exactly what distinguishes them, because the transport-level observations tell you whether the object crossed intact.

53. Flagship Scenario 1 — A Corrupted Object, Detected and Recovered

Illustrative. A bit error is injected at injection point 3 (§43), after integrity is computed.

Five readings, and each is a property doing its job.

Two physical attempts, one transport object, one semantic delivery. §38's hierarchy exactly: exactly-once holds at the semantic level and is false at the attempt level. A property written at the attempt level would fire here on correct behaviour.

Cycle 114 is a negative observation and it is the important one. No delivery followed the bad verdict — §39's p_bad_verdict_never_delivered. The check is that nothing happened, which is why it needs a model: an assertion cannot easily observe an absence over an unbounded window.

Cycle 118 satisfies R3. The retry has an observed trigger. A second attempt with no trigger at cycle 118 would be a spontaneous retransmission — a serious defect that R1 alone would not catch, because it still results in one delivery.

The replay entry is held from 102 to 131 and freed on resolution, not on send. 19.3 §45's rule, observable in the resource model as a live entry across both attempts.

And the credit is consumed once at 103 and returned once at 133 — one consumption for two attempts. Whether that is correct depends on 19.5 §51's open question, and this trace is exactly the experiment that answers it empirically for one implementation: count allocations at the far end against attempts. One allocation for two attempts means the allocation was retained.

54. Flagship Scenario 2 — Recovery With Live State

Illustrative. A recovery is forced (§43 point 7) while three operations are outstanding, one object is unresolved and credits are partially spent.

Six checks fire in this one scenario, and no other scenario exercises them together.

The semantic model's three operations survive — 19.2 §45, and the property is one row of 19.6 §27's matrix.

The unresolved object survives and is re-attempted rather than dropped — R4. A design that clears its replay ring on recovery loses this object silently, and the semantic model catches it later as an operation that never terminates (§39's p_operation_terminates) — twenty cycles after the cause, in a different model. This is why §60's divergence analysis matters.

Credits are re-established by agreement and the counter equals the advertisement exactly — 19.5 §12's equality property, which fires at cycle 231 if the straggler is absorbed.

The straggler is rejected and counted — a stale return during a recovery is expected; during steady state it would be alarming. Only a counter distinguishes those, which is why 19.5 §30 names the signal rather than silently dropping the event.

Nothing delivered before the recovery is re-delivered after it — R5, and it needs both ends observed.

And the link-state model confirms one recovery entry and one exit within the bound — L5, which is the property that catches a recovery that never converges.

55. Flagship Scenario 3 — A Retry That Duplicates

Illustrative. The failure mode, and how each model responds.

The bug is at cycle 349, and it is a duplicate-suppression failure, not a retry failure.

Four readings.

Everything up to cycle 348 is correct. The acknowledgement was lost, the timeout was right to fire, the retransmission was right to happen, and the object arrived intact. The reliability mechanism did its job. 19.3 §32's duplicate window is what should have caught the second arrival, and it did not — because the window was too small, or because it was cleared, or because it keyed on something that had been reused.

No local assertion at the far end can catch this, because the far end has no way to know it already delivered this object unless it remembers — and the memory is the duplicate window, which is the thing that failed. The check must be at the level of the environment, which remembers everything.

The retry-attempt count alone would not have found it. Two attempts is legitimate. The failure is two deliveries, and only the far-end semantic observation sees that — which is §6's peer observation point earning its cost.

And the near-end view is completely clean. From the transmitter's perspective: one operation, two attempts, one acknowledgement, one completion. Every near-end property passes. An environment without far-end observation reports a pass on a link that duplicated a memory write.

56. Flagship Scenario 4 — Credit Inflation, Caught by Conservation

Illustrative. A duplicated credit return at injection point 5 (§43).

Five readings.

Cycle 407 is the bug and cycle 908 is the symptom — 501 cycles apart, in a different block. Without conservation, the investigation starts at the receive buffer.

The bound check passes at every cycle, including 407. Six is a legal credit value against a capacity of eight. 19.5 §24's whole argument, made visible: the counter never leaves its range and the relationship is broken.

The model catches it because the model counts distinct observed releases, not returns applied. A duplicated message on the return path is one release and two applications. A model that counted applications would agree with the design and see nothing — §31's mirror, one more time.

The failure direction is the overflow direction, which is why this is the class to instrument most heavily. A leak makes the link slow; inflation makes it lose data.

And the delay to symptom is load-dependent. The overflow requires the receiver to be genuinely full, which may take hours. The conservation check fires at cycle 407 regardless of load, which is the entire value of checking a relationship rather than a bound.

57. The Assertion Inventory

Three observations about the shape.

Rows 21 and 24 are effect forms. They are written against a different observable than the mechanism that implements them, so a shared misconception between designer and verifier cannot satisfy them. Every inventory should contain some, and they should be identified as such.

Rows 32 and 33 are not properties about the design at all. They are properties about the verification, and they belong in the inventory because an inventory that lists only design properties has no mechanism for noticing that half of them check nothing.

And the plane column is the audit tool. A plan with thirty plane-1 rows and two plane-5 rows has a structural gap that no amount of adding plane-1 properties will close.

58. The Verification Plan, Assembled

Everything above, as a procedure.

1. Enumerate the boundaries. Every place ownership transfers. For UCIe's stack that is at minimum the client boundary, protocol-to-Adapter, Adapter-to-PHY, the far-end mirrors of each, the credit path, and management.

2. Ask §4's seven questions at each one. The answers are the per-boundary plan, and question 7 tells you where the next monitor goes.

3. Assign every rule to a plane (§5). A boundary with no plane-4 or plane-5 rules either genuinely has none — say why — or has a gap.

4. Decide, per property, formal or simulation (§47), and record the bound if the proof is bounded.

5. Build four models, each independent (§30–§34). For each, write down the contract statement each rule comes from — and if a rule can only be stated by naming a design signal, it is a mirror.

6. Define the join key and its inference rules (§23), with its own anomaly checks (§36).

7. Write the negative-test list (§42), each entry naming a positive expected outcome.

8. Enumerate the configuration space (19.6 §35), and mark which properties apply in which configurations (§50, §51).

9. Add a cover for every antecedent and a pass-count check for every bind (§45, §46).

10. Run the seeded-defect regression (§49) and record which check catches what.

Step 10 is the one that turns the plan into evidence. Steps 1 to 9 produce a plan that looks complete. Step 10 is the only one that demonstrates the plan can detect anything, and its output — the defect-to-check mapping — is the most useful artefact the whole exercise produces.

59. Coverage

// ILLUSTRATIVE. Coverage for the VERIFICATION STRUCTURE, not for protocol
// features — 20.5 owns the full functional coverage model.
covergroup cg_protocol_verification @(posedge clk);
 
  // --- Plane 1: boundary conditions ---
  cp_stall_at_accept: coverpoint stall_length_before_accept {
    bins none = {0}; bins short = {[1:3]}; bins long = {[4:63]};
    bins very_long = {[64:$]};                     // §13's stability window
  }
  cp_framing: coverpoint {payload.first, payload.last} {
    bins single_beat = {2'b11};                    // first and last together
    bins first_only  = {2'b10};
    bins middle      = {2'b00};
    bins last_only   = {2'b01};
  }
 
  // --- Plane 3: identity and ordering ---
  cp_identity_reuse_gap: coverpoint cycles_between_retire_and_reuse {
    bins immediate = {[0:1]};                      // 19.2 §21's window
    bins short     = {[2:15]};
    bins long      = {[16:$]};
  }
  cp_response_order: coverpoint response_order_relative_to_request {
    bins in_order      = {ORD_SAME};
    bins reordered     = {ORD_DIFFERENT};          // §40 — must be covered
  }
 
  // --- Plane 4: the attempt-to-delivery ratio ---
  cp_attempts_per_object: coverpoint attempts_this_object {
    bins one = {1}; bins two = {2}; bins several = {[3:7]};
    bins many = {[8:$]};                           // §55's scenario
  }
  cp_delivery_count: coverpoint deliveries_this_operation {
    bins zero_with_failure = {0};                  // §38's third value
    bins exactly_one       = {1};
    illegal_bins duplicate = {[2:$]};              // must never happen
  }
  cp_spanned_recovery: coverpoint object_spanned_recovery {
    bins no = {1'b0};
    bins yes = {1'b1};                             // §54 — needs a directed test
  }
 
  // --- Plane 5: the quiet-period cases random stimulus never reaches ---
  cp_quiet_after_burst: coverpoint cycles_idle_after_burst {
    bins none  = {[0:15]};
    bins quiet = {[16:$]};                         // 19.5 §42's deadlock needs this
  }
  cp_zero_credit_with_free_rx: coverpoint stranded_capacity_state {
    bins never = {1'b0};
    bins seen  = {1'b1};                           // the deadlock signature
  }
 
  // --- Negative testing: every rejection path exercised ---
  cp_rejection: coverpoint rejection_reason {
    bins disabled_protocol = {REJ_PROTO_DISABLED};
    bins bad_framing       = {REJ_FRAMING};
    bins illegal_config    = {REJ_CONFIG};
    bins resource          = {REJ_RESOURCE};
  }
 
  // --- Crosses that matter ---
  x_recovery_with_outstanding: cross cp_spanned_recovery, cp_attempts_per_object;
  x_stall_and_framing:         cross cp_stall_at_accept, cp_framing;
  x_reorder_and_reuse:         cross cp_response_order, cp_identity_reuse_gap;
 
endgroup

Four notes.

cp_quiet_after_burst.quiet is the bin that finds the deadlock. 19.5 §42 needs a burst followed by silence, which random stimulus almost never produces. If this bin is empty, the batching deadlock is unverified — and it is empty by default in every saturating random regression.

cp_delivery_count uses an illegal_bins for duplicates. That is stronger than a coverage goal: it fails the run rather than reporting a gap, which is right, because a duplicate is never acceptable and should not be a coverage question.

cp_response_order.reordered must be non-empty or §40's second row was never exercised, meaning the design was verified for one of two legal orders.

And x_reorder_and_reuse is the cross that catches 19.2 §21's aliasing. An immediate identity reuse combined with a reordered response is the precise combination in which a delayed response for a retired operation meets its identity's new owner. Neither coverpoint alone reaches it.

60. Debug — Which Layer Diverged First

The output that justifies the whole architecture. Given a failure, the joined view produces a table like §7's automatically:

FAILURE: operation tag 4127 — data mismatch at the client boundary
 
  BOUNDARY          EXPECTED                    OBSERVED                   MATCH
  protocol (near)   1 accept, addr 0x1000       1 accept, addr 0x1000      yes
  adapter TX        1 object formed             2 objects formed           NO  <<<
  link TX           1 attempt per object        1 attempt per object       yes
  link RX (far)     2 arrivals                  2 arrivals                 yes
  adapter RX        1 delivery (dup suppressed) 2 deliveries               NO
  protocol (far)    1 delivery                  2 deliveries               NO
 
  FIRST DIVERGENCE: adapter TX, cycle 8,412
  CONTEXT:  cfg_epoch 3, link_epoch 7, no recovery in this window,
            no retry trigger observed
  IMPLICATION: one semantic operation produced two transport objects with no
               fragmentation and no retry — a protocol-engine or Adapter
               object-formation defect. The far-end duplicate delivery is a
               CONSEQUENCE, not the cause.

Four properties of this output.

The last line is the one that saves the week. Three boundaries reported a mismatch, and two of them are consequences. Without the ordering, three teams investigate in parallel and two of them find nothing.

The context line eliminates two entire hypotheses before anyone opens a waveform. No recovery, no retry trigger — so the duplication was not caused by the reliability mechanism, which is where the investigation would otherwise start, because duplication and reliability are associated in everyone's mind.

It is mechanical. Nothing here required judgement: sort the joined view's events by boundary, compare against the model, report the earliest disagreement. Which means it happens on every failure, automatically, including the intermittent ones that nobody would have instrumented by hand.

And it works for the failures that produce no client-visible symptom. A stranded resource or a leaked credit never reaches the client boundary. The same machinery reports the divergence at the boundary where it happened, with the same context, at the cycle it occurred.

61. Common Misconceptions

"Protocol verification means checking packet fields." Field checking is one of five planes, and the cheapest one. The failures that reach silicon are in resource accounting, ordering, exactly-once and liveness — none of which is a field check.

"One end-to-end scoreboard is enough — it checks the real requirement." It checks the real requirement and tells you nothing when it fails, misses every failure with no client-visible symptom, and makes intermittent failures unreproducible.

"The monitor should track the design's state so it knows what is happening." Then it has inherited the design's interpretation of every event, and it will agree with the design about the thing most likely to be wrong.

"A reference model should mirror the design so the comparison is meaningful." A mirror compares the design to itself. Seven bugs across four layers survive it (§31), and the model's silence is not evidence.

"If all assertions pass, the design is correct." Passing includes vacuous. A property whose antecedent never occurred passes 100% of a regression, and a property that was never bound reports nothing at all. The pass rate without antecedent coverage and pass counts is not a measurement.

"Liveness assertions are noisy and not worth it." They are noisy without assumptions. With assumptions written down and a derived bound, they are the only thing capable of finding four of Module 19's failure modes — every one of which passes every safety property forever.

"s_eventually is the way to write liveness." In simulation it fails at the end of the run or never, and it cannot detect slow progress. A derived bound fails at a specific cycle and catches ten-times-too-slow as well as never.

"An assumption is a way of making a property pass." An assumption is a claim about the real system, and it needs a justification. An assumption with no real-world justification is a property that was weakened until it passed, and in formal it makes every proof under it unsound.

"A negative test passes if nothing breaks." Then it passes most convincingly when the detection mechanism is entirely absent. Every negative test must assert a positive outcome.

"Exactly-once is a single property." It is false at the attempt level, false at the object level under retransmission, and true only at the semantic level — and it has three values, not two, because zero deliveries with an explicit failure is also correct.

"Retry duplication is a retry bug." It is a duplicate-suppression bug. The retry was correct, the acknowledgement was lost, and the mechanism that should have caught the second arrival is the window at the far end.

"The environment does not need verifying." A monitor is logic and a model is a program, and both fail in the passing direction. A monitor with a level-versus-edge bug reports duplicates that do not exist and teaches the team to distrust the real ones.

"Ordering should be checked as strictly as possible." Assumed ordering produces false failures, which get fixed by weakening the check — usually past the point where the real requirement was. Unordered pairs must be accepted in both orders and covered in both.

"Raw Mode is just a configuration." It moves error protection from the Adapter to the Protocol Layer, which moves plane-4 properties to different boundaries. A plane-4 property bound in Raw Mode fires falsely and gets deleted from everywhere.

62. Understanding Check

63. Summary and What Comes Next

Protocol verification checks promises at boundaries, not implementation choices inside them — and every check that cannot be stated without naming an internal signal is verifying the design against itself.

Five planes, not one. Structural validity is the cheapest and least likely to hold a serious bug; resource accounting, ordering and identity, reliability and exactly-once, and liveness are where the failures that reach silicon live. A plan with thirty plane-1 properties and two plane-5 properties has a structural gap.

Four monitors, because the answer that matters is which layer diverged first. One end-to-end scoreboard checks the real requirement and tells you nothing when it fails — and misses entirely every failure with no client-visible symptom.

Events come from contracts, not from registers. A monitor that infers an event from a state value counts five attempts for one transmission; a monitor that samples the design's own event signal has inherited the definition most likely to be wrong.

Check meaningful bits at meaningful events. A property that fires on legal stimulus does not make verification stricter — it makes the report unreadable, and an unreadable report is where real failures go to be ignored.

Separate safety from liveness and write the assumptions down. Safety is violated by a finite trace and needs no assumptions; liveness needs them always, and a liveness property without them fails on the environment and gets deleted — taking with it the only mechanism capable of finding a deadlock.

Four independent models, and independence is the whole point. A mirror agrees with the design about when things happen, and seven bugs across four layers survive it.

Exactly-once is true at one level of three, and it has three values. Zero deliveries with an explicit failure is correct; zero deliveries with a reported success is the worst outcome in the chapter.

Every negative test asserts a positive outcome, and every implication property has a cover for its antecedent — because a plan whose pass criterion is the absence of failures is indistinguishable from a plan that did not run.

This chapter established the decomposition. The rest of Module 20 builds on it. The next chapter takes the same architecture to the hardest scenario the link has: bring-up, where nothing is yet trusted — not the training, not the negotiated parameters, not the peer, and not the assumption that both dies agree about what state the link is in. Every model here assumed a link that was already up; the next one does not.

• 20.2 — Link Verification — end-to-end link-bring-up verification.

Browse the full path on the UCIe tutorials index.