Link Verification

Chapter 20.1 established what to check at each boundary and how to build models that do not agree with the design's mistakes. This chapter composes those boundaries into one lifecycle — reset, training, configuration, traffic, fault, recovery, and back — and asks the question a boundary check cannot: did any semantic work get lost while all of that was happening?

1. The One-Sentence Model

A link is verified only when its control state and its outstanding semantic obligations are both correct across time. Reaching an operational state proves the first half; proving the second half requires a model that was alive before the fault and is still alive after the recovery.

Ten conditions, and a link that satisfies nine of them is broken. It must enter an operational state legally, agree with the peer on a usable configuration, admit traffic only when permitted, preserve accepted work, detect faults, enter recovery correctly, restore transport state, retain or explicitly resolve higher-level obligations, return to service, and deliver each semantic operation correctly exactly once.

The tenth is the one that has no local observable. Nothing in the link reports it. It is a statement relating an event before the fault to an event after the recovery, and only a model that spans both sees it.

2. What This Chapter Owns

8.1 to 8.6 designed the bring-up. 20.1 designed the checking method. This chapter is where they meet — and the meeting produces things neither can state alone:

Four lifecycles that overlap and must not be collapsed (§4). A link event, a configuration commit, a transport object and a semantic obligation each have their own clock, and almost every wrong checker below is one of them being read on another's timescale.

A reference model that never reads the design's state register (§7–§10) — the flagship principle, and the one that decides whether the environment can detect a training bug at all.

Bounds that come from the configuration rather than from a constant (§15–§17), because a legal slow configuration failing a fixed watchdog is a verification bug reported as a design bug.

Negotiation checked by an independent rule (§18–§20), because a checker that calls the design's own negotiation function agrees with it about every incompatible pair.

And six flagship traces through recovery, degradation, retry, stale credit and fatal failure — including the one where every counter matches after the recovery and work was still lost (§39).

3. Sourcing

4. Four Lifecycles, Overlapping

The single most useful decomposition in this chapter. Four things are happening at once, on four different timescales, and a checker that reads one on another's clock is wrong in a way that looks like a design bug.

Four consequences, and each is a wrong checker below.

A link event does not end a semantic lifecycle. A recovery is a physical event; the semantic obligation accepted before it is still outstanding after it. §12's checker collapses these two and hides the bug it exists to find.

A configuration change does not end a transport lifecycle either — or it must not. An object accepted under configuration epoch 3 must be interpreted under epoch 3 until it resolves (19.6 §24), which is why the transport record carries the epoch rather than reading the current one.

One semantic operation can span several transport lifecycles, and one transport object several physical attempts. 20.1 §22's hierarchy, and §32 is where it becomes an end-to-end ledger.

And the physical lifecycle is the only one with a state register. The other three are inferred — which is precisely why the environment must model them, and why an environment that models only the link state has modelled the easy one.

5. What "Verified" Means, Precisely

Ten conditions. The table is the chapter's specification of its own job.

Read condition 1 against condition 9. A link that reaches ACTIVE by an illegal shortcut satisfies 9 and fails 1 — and no traffic test will ever notice, because the link works. Only a model that tracked the path can tell.

And read condition 10 against all the others. It is the only row whose evidence is spread across the whole run. Nine conditions can be checked as the link runs; the tenth is checked by relating two events that may be thousands of cycles and one recovery apart.

6. The Link Verification Architecture

Three things to read.

The fault injector reaches the contract boundaries, not the RTL. It corrupts an object after integrity was computed, drops a feedback message, holds a lane-health input, stalls a training response. It never forces an internal register — because a forced internal register produces a state the design could not have reached on its own, and the resulting failure is not a bug report.

Four models, four lifecycles (§4). The mapping is one-to-one and deliberate.

And the link/config model is drawn in a different colour because it is the one this chapter spends most of its time on. The other three are 20.1's, deepened; this one is new, and §8 is why it is the hardest to build correctly.

7. The Reference Link Model

// ILLUSTRATIVE, VERIFICATION-ONLY. Deliberately NOT the published UCIe state
// names (§3) and deliberately NOT the DUT's enum — §8 is why. These are phases
// the ENVIRONMENT can justify from observable evidence, at the granularity the
// environment can actually distinguish.
typedef enum {
  RM_RESET,        // no evidence of any initialisation activity
  RM_TRAINING,     // initialisation is under way; no traffic permission
  RM_OPERATIONAL,  // permission observed AND a valid configuration is active
  RM_RECOVERY,     // a previously operational link is re-establishing
  RM_FAILED        // an explicit failure indication; not self-clearing
} ref_link_state_e;
 
typedef struct {
  ref_link_state_e phase;
  int unsigned     link_epoch;      // increments on each entry to OPERATIONAL
  int unsigned     phase_entry_cyc; // for the progress watchdogs of §49
  int unsigned     training_attempts;
  bit              cfg_valid;       // an agreed configuration is in force
  int unsigned     cfg_epoch;
  bit              was_operational; // distinguishes TRAINING from RECOVERY
} ref_link_t;

Architecture. Five phases, not ten. The model is coarser than the design deliberately.

Why coarser is correct, and this is the part that surprises people. The environment must only distinguish phases it can justify from evidence. If the environment cannot tell MBINIT from MBTRAIN at any boundary it observes, then modelling them as separate states means the model is guessing — and a guessing model produces false failures, which get fixed by weakening the model. Five phases that are all observable beat ten phases of which six are inferred.

Why was_operational exists. It is the only thing that distinguishes training from recovery, and they have completely different expectations: training starts with no outstanding work, recovery starts with obligations that must survive (§35). The design may or may not use different states for these; the model must, because its checks differ.

Why link_epoch increments on entry to OPERATIONAL rather than on recovery entry. It marks the beginning of an agreement, which is what stale events are tested against (19.5 §28). Incrementing on exit leaves a window in which the epoch has advanced and no new agreement exists yet.

Contract. Every field is written only by §10's evidence rules. No field is ever assigned from a design signal, and §9 is what happens when one is.

8. Never Mirror the Design's State Machine

The flagship principle of this chapter.

A reference model that derives its state from the design's state register cannot detect a state-machine bug. It will agree with the design about what phase the link is in — including every phase the link should not have been in.

Three forms of the same mistake, in increasing subtlety.

// WRONG, form 1 — the model IS the design.
expected_state = dut.link_state_q;

Nothing is being checked. The comparison is a tautology and passes forever.

// WRONG, form 2 — the model copies the design's next-state function.
always @(posedge clk)
  ref_state <= dut_next_state_function(ref_state, dut_events);

This looks like an independent model and is not. If the design's next-state function permits an illegal shortcut — TRAINING straight to OPERATIONAL without a configuration agreement — the model permits it too, and the two agree at every cycle.

// WRONG, form 3 — the model is independent but its INPUTS are internal.
if (dut.training_done_internal) ref.phase = RM_OPERATIONAL;

The subtlest one, because the model's logic is genuinely independent. But training_done_internal means whatever the design decided it means, so the model has inherited the design's definition of completion — which is exactly the thing a training bug is a bug in.

What all three have in common: the model's transitions are caused by something the design produced, rather than by something the design promised. §10 is the alternative.

9. Wrong Checker — the Model That Reads the Register

Worked, on a real bug shape.

The design's training controller has a bug: under a specific peer-timing case, it commits the negotiated configuration before the peer has confirmed it, then enters ACTIVE. The two dies now disagree about the active width. Traffic is striped one way and interpreted another.

Four readings.

The mirroring model reports nothing at cycle 495. The design says ACTIVE, the model says operational, they agree, and the admission at 496 is expected behaviour as far as the environment is concerned.

The evidence model fails at 496 and names the cause. It never saw the confirmation evidence, so it never left RM_TRAINING, and the admission is a violation of §14's property.

The symptom without the evidence model appears much later and elsewhere — as corrupted data at the far end, or as a CRC storm, or as a peer that entered recovery. All three investigations start at the wrong layer.

And the mirroring model is not merely weak here — it is actively harmful. Its silence is read as evidence that training is correct, so the training verification is declared complete and the effort moves elsewhere.

10. Deriving Phase From Evidence

The rule: every reference-model transition is caused by evidence the design promised to produce, observed at a boundary.

// ILLUSTRATIVE. Every transition is driven by an OBSERVED CONTRACT EVENT.
// No branch reads a design state register or an internal "done" signal.
always @(posedge clk) begin
  case (ref.phase)
 
    RM_RESET:
      // Evidence: initialisation activity is observable at the management
      // boundary. Not "the design left its reset state".
      if (obs_init_activity) begin
        ref.phase           = RM_TRAINING;
        ref.phase_entry_cyc = cycle;
        ref.training_attempts++;
      end
 
    RM_TRAINING, RM_RECOVERY: begin
      // Two independent pieces of evidence are BOTH required. This conjunction
      // is the whole check — §9's bug is exactly the case where one is missing.
      if (obs_traffic_permission && ref.cfg_valid) begin
        ref.phase           = RM_OPERATIONAL;
        ref.link_epoch++;
        ref.phase_entry_cyc = cycle;
      end
      else if (obs_training_error) begin
        ref.phase           = RM_TRAINING;   // restart, not recovery
        ref.phase_entry_cyc = cycle;
        ref.training_attempts++;
      end
      else if (obs_fatal_indication)
        ref.phase = RM_FAILED;
    end
 
    RM_OPERATIONAL:
      if (obs_recovery_entry) begin
        ref.phase           = RM_RECOVERY;
        ref.was_operational = 1'b1;          // §7 — this is what changes the rules
        ref.phase_entry_cyc = cycle;
        ref.cfg_valid       = 1'b0;          // agreement is void until re-established
      end
      else if (obs_fatal_indication)
        ref.phase = RM_FAILED;
 
    RM_FAILED:
      // Deliberately not self-clearing. Exit only on an observed deliberate
      // reset — §41 explains why an automatic exit destroys the evidence.
      if (obs_hard_reset) ref = '{ phase: RM_RESET, default: 0 };
 
  endcase
end

Architecture. One case, every arm driven by an obs_* signal produced by a monitor from a boundary observation.

The load-bearing line is the conjunction in RM_TRAINING. Traffic permission and a valid agreed configuration, both independently established. A model that transitions on permission alone is §9's mirroring model wearing better clothes — it would have accepted cycle 495.

Why the training-error arm returns to RM_TRAINING rather than RM_RECOVERY. A restart during initialisation has no outstanding semantic work; a recovery from operational does. The model's expectations after each are different, and conflating them means the post-recovery preservation checks (§35) never run on a restart and the post-restart clean-slate checks never run on a recovery.

Why cfg_valid is cleared on recovery entry. The agreement described a link that has just gone away. Leaving it set means the model would re-enter RM_OPERATIONAL on permission alone, which is §9's bug reproduced inside the checker.

DV of the model itself. Force each obs_* in isolation and confirm exactly one transition; force two simultaneously and confirm the priority is deliberate. 20.1 §49's rule applies — a monitor is logic and a model is a program, and both fail in the passing direction.

11. Reset Verification

Reset is where the four lifecycles are created, and where a wrong scope destroys three of them.

8.1 §13 and 19.6 §27 both deliver a reset matrix. This section verifies it, row by row, and the verification is more than re-reading the table:

Three checks that are easy to omit.

No stale valid after release. A valid that survives reset offers work that no longer has a producer behind it. The property is cheap and the failure is a phantom transaction at cycle zero.

Configuration invalidated or retained per the contract, not per convenience. A reset that clears the active configuration but leaves the requested one is fine if the matrix says so, and a bug if it does not. The check is against the matrix, not against intuition.

And the semantic model's own reset policy is a separate decision — §12.

12. Wrong Checker — Clearing Everything on the Design's Reset

20.1 §31 made this argument about event triggers. Here it is at link level, where it is worse.

// WRONG — the environment's models are cleared by a DUT reset signal.
always @(posedge clk)
  if (!dut_rst_n) begin
    sem_model.clear();      // every outstanding obligation forgotten
    rel_model.clear();
    res_model.clear();
    ref_link  = '{ phase: RM_RESET, default: 0 };
  end

The bug this hides is the exact bug it should catch.

The design has a defect: its recovery path drives the same reset net as the global reset. A recoverable link event therefore clears the semantic transaction table — 19.2 §44's failure, in silicon.

What happens with the wrong checker:

Four properties.

The four operations are gone and nobody is looking for them. The client that issued them is waiting forever, and the environment has no record that they existed.

The failure is total and silent. Not a wrong value — an absence, and absences are only detectable by something that remembers.

It is the most likely single defect in a verification environment, because clearing models on reset is the obviously correct thing to do for a cold reset and is written once, for all resets, early in the project.

And the fix is not "do not clear on reset". It is that the environment has its own architectural reset policy, derived from the same matrix the design is being checked against:

// RIGHT — the environment's reset policy is derived from the CONTRACT,
// and it distinguishes the reset kinds the contract distinguishes.
always @(posedge clk) begin
  if (obs_cold_reset) begin
    // A cold reset genuinely destroys everything — including, legitimately,
    // any obligation that was outstanding. Those are REPORTED, not forgotten.
    sem_model.report_abandoned("cold reset");
    sem_model.clear(); rel_model.clear(); res_model.clear();
    ref_link = '{ phase: RM_RESET, default: 0 };
  end
  else if (obs_recovery_entry) begin
    // A recovery clears LINK-EPOCH state only. Semantic obligations survive,
    // and the check is that the design agrees (§35).
    res_model.void_credit_agreement();     // 19.5 §28
    rel_model.mark_recovery_spanned();     // 20.1 §33's R4/R5
    // sem_model is DELIBERATELY UNTOUCHED.
  end
end

Note report_abandoned. Even where clearing is correct, the obligations that were destroyed are named in the log — because "we reset while four operations were outstanding" is information, and a silent clear discards it.

13. SVA — No Traffic Before Permission

// MANDATORY. Admission requires the reference model's operational phase —
// NOT the design's state register (§8).
property p_no_admission_before_operational;
  @(posedge clk) disable iff (!por_n)
    sem_accept_fire |-> (ref_link.phase == RM_OPERATIONAL);
endproperty
a_no_admission_before_operational:
  assert property (p_no_admission_before_operational);
 
// MANDATORY — and a valid agreed configuration, independently established.
property p_admission_requires_valid_config;
  @(posedge clk) disable iff (!por_n)
    sem_accept_fire |-> (ref_link.cfg_valid && ref_cfg.agreed);
endproperty
a_admission_requires_valid_config:
  assert property (p_admission_requires_valid_config);
 
// MANDATORY — no transport attempt while the model believes the link is
// recovering. Whether the design permits this is architecture-defined, so
// the property is written against the ARCHITECTURE'S stated rule.
property p_no_attempt_during_recovery;
  @(posedge clk) disable iff (!por_n)
    (ref_link.phase == RM_RECOVERY) |-> !new_attempt_fire;
endproperty
 
// MANDATORY — nothing offered before reset release. Catches a stale valid.
property p_no_valid_before_release;
  @(posedge clk)
    (!rst_n) |-> (!proto_valid && !adapt_valid);
endproperty
a_no_valid_before_release: assert property (p_no_valid_before_release);

Two notes on construction.

The first property's right-hand side is the model, not the design. That is what makes it a check rather than a tautology — and it is why §10's model must be right, because these properties are only as strong as the phase it computes.

disable iff (!por_n), not disable iff (!rst_n). These properties must remain live through recovery and through narrower resets. 20.1 §45's third vacuity mechanism is exactly this: a property disabled during the window it exists to check is asleep during the bug, and 20.3 makes it a flagship anti-pattern.

14. Training Observability

Do not verify training by watching for the final operational signal. That signal says the design believes it finished; it says nothing about the path.

What the environment should observe, at the granularity it can justify:

Two rules.

The exact UCIe training events are source-locked (§3). Where your revision names specific handshakes, use those; where it does not, the model uses generic labels and says so — which is what obs_init_activity and obs_traffic_permission are in §10.

And permission is derived, never asserted. 8.5 §5 made this the composition rule: operational status is a conclusion from the evidence, not a signal somebody sets. A model that takes a single "training done" output as its evidence has re-centralised the very thing that chapter decentralised.

15. The Training Watchdog

// ILLUSTRATIVE. A watchdog detects the ABSENCE OF PROGRESS. It does not,
// and cannot, prove correctness.
property p_training_makes_progress;
  @(posedge clk) disable iff (!por_n)
    (ref_link.phase inside {RM_TRAINING, RM_RECOVERY})
      |-> ##[1:TRAINING_PROGRESS_BOUND] (obs_progress_event
                                      || obs_training_error
                                      || (ref_link.phase != $past(ref_link.phase)));
endproperty
a_training_makes_progress: assert property (p_training_makes_progress);

Architecture. A bounded progress property, not a bounded completion property.

Why progress rather than completion. Total training time depends on the configuration, the peer, the number of retries and the physical conditions. The time between two progress events is a much tighter and much more stable quantity, so the bound can be meaningful rather than enormous — and an enormous bound catches nothing.

Why it accepts an error as progress. A training error is a legal outcome and it is progress: the state changed, something happened, the run is not stuck. A watchdog that fails on an error path reports the error twice, once correctly and once as a hang.

What it does not do. It does not check that the path was legal, that the configuration is right, or that anything was negotiated. §9's bug passes this watchdog comfortably — the link made steady progress straight into an illegal ACTIVE.

16. Wrong Watchdog — A Fixed Bound

// WRONG — a constant, chosen from the configuration the engineer debugged with.
property p_training_completes;
  @(posedge clk) disable iff (!rst_n)
    training_start |-> ##[1:100] training_done;
endproperty

Worked. The bound was measured on an x16 configuration at the highest rate, where training completed in 82 cycles. A supported narrower or slower configuration takes 160 cycles — legally, for architectural reasons.

The property fails on correct hardware.

Four properties, and the fourth is the real cost.

The failure is reported as a design bug, and somebody spends a day proving that 160 cycles is legal.

The fix that gets applied is usually wrong. The bound is raised to 200 — which makes the property useless for the fast configuration, where a 190-cycle training run is now accepted and is a genuine defect.

The bound has no derivation, so nobody can argue about it. A number with no stated origin cannot be reviewed, cannot be updated when a configuration is added, and will be raised again the next time it fires.

And it teaches the team that watchdogs are noise. After two false failures, the property is disabled — and the real hang, when it arrives, is found by a simulation timeout with no localisation at all (§49).

17. Configuration-Aware Bounds

// RIGHT — the bound is DERIVED from the configuration under test, and the
// derivation is written down so it can be reviewed and extended.
//
//   bound = base initialisation work                     INIT_BASE
//         + per-lane qualification work                  × active_lanes
//         + rate-dependent settling                      RATE_SETTLE[rate]
//         + one permitted internal retry                 RETRY_ALLOWANCE
//         + environment response latency                 PEER_RSP_MAX
function automatic int training_bound(int lanes, int rate_idx, int retries);
  return INIT_BASE
       + lanes * PER_LANE_WORK
       + RATE_SETTLE[rate_idx]
       + retries * RETRY_ALLOWANCE
       + PEER_RSP_MAX;
endfunction
 
property p_training_bounded;
  @(posedge clk) disable iff (!por_n)
    obs_training_start
      |-> ##[1:$] (obs_traffic_permission || obs_training_error)
          within (1'b1 [*1:training_bound(ref_cfg.active_lanes,
                                          ref_cfg.rate_idx,
                                          MAX_PERMITTED_RETRIES)]);
endproperty

Three properties of a derived bound.

It scales with the configuration automatically, so adding a supported width does not require re-tuning a constant — and 19.6 §35's parameter matrix does not silently invalidate the watchdog.

The derivation is the valuable artefact, not the number. Writing the five terms down forces somebody to enumerate every source of delay, and that enumeration is frequently where a missing term is discovered before any test runs.

And it distinguishes a test-plan bound from a protocol requirement. No UCIe timer is claimed here (§3). training_bound is the environment's expectation of this implementation under this test, and it should be labelled as such in the failure message — because a bound violation is "slower than we expected", not "violated the specification".

18. The Negotiated-Configuration Model

// ILLUSTRATIVE, VERIFICATION-ONLY. Four quantities, tracked independently.
typedef struct {
  cfg_t        local_requested;   // what this die asked for
  cfg_t        remote_capability; // what the peer advertised, AS OBSERVED
  cfg_t        expected_agreed;   // computed by an INDEPENDENT rule (§20)
  cfg_t        observed_active;   // what the design actually committed
  bit          agreed;            // an agreement has been established
  int unsigned cfg_epoch;
} ref_cfg_t;

The four are deliberately separate, and each catches a different failure.

local_requested versus remote_capability catches a request the peer cannot honour — the incompatible-configuration case of §24.

expected_agreed versus observed_active is the negotiation check itself, and it is only meaningful if expected_agreed was computed independently (§20).

agreed is the flag §10 and §13 both depend on. It is set only when the environment has observed evidence from both sides — a locally computed agreement is not an agreement, which is 8.5 §4's local-versus-bilateral distinction applied to configuration.

And cfg_epoch is what every transport and semantic record carries so §4's lifecycles do not get read on each other's clock.

19. Wrong Config Checker — Calling the Design's Function

// WRONG — the expected result is computed by the design's own helper.
assign expected_width = dut.compute_common_width(local_req, remote_cap);
 
property p_width_correct;
  @(posedge clk) disable iff (!rst_n)
    cfg_commit |-> (dut.active_width == expected_width);
endproperty

This is 19.6 §13's rule violated, and the consequence is exact.

Worked. compute_common_width has an off-by-one: when both sides support exactly one common width, it returns the next width down. Both dies are x8-capable; the function returns x4.

The link runs at half its capable width, forever, and every test passes.

Four properties.

There is no failing signal anywhere. x4 is a legal width, the link works, throughput is simply half what it should be — and nobody measures absolute throughput against a first-principles expectation in a functional regression.

It is not caught by coverage either. The x8 bin is simply never hit, and an unhit bin in a large coverage model is a routine end-of-project cleanup item, explained away as "our stimulus doesn't reach that".

The bug survives to silicon and is found by a performance engineer, months later, comparing measured bandwidth to a datasheet.

And the same shape applies to every negotiated quantity — rate, protocol selection, feature enables, class counts. Any one of them computed by a shared function is unchecked.

20. An Independent Negotiation Rule

// RIGHT — the expected result is computed from the ARCHITECTURE'S rule,
// written independently in the verification environment. It is deliberately
// written differently from any plausible RTL implementation: a set
// intersection and a maximum, rather than a priority chain.
function automatic cfg_t expected_agreement(cfg_t local_req, cfg_t remote_cap);
  cfg_t r;
  int   common_widths[$];
  int   common_rates[$];
 
  // Widths supported by BOTH sides, as a set.
  foreach (SUPPORTED_WIDTHS[i])
    if (local_req.width_mask[i] && remote_cap.width_mask[i])
      common_widths.push_back(SUPPORTED_WIDTHS[i]);
 
  foreach (SUPPORTED_RATES[i])
    if (local_req.rate_mask[i] && remote_cap.rate_mask[i])
      common_rates.push_back(SUPPORTED_RATES[i]);
 
  // The architecture's stated rule: the highest common value, or no agreement.
  r.agreed = (common_widths.size() > 0) && (common_rates.size() > 0);
  r.width  = r.agreed ? common_widths[$] : 0;   // sorted ascending by construction
  r.rate   = r.agreed ? common_rates[$]  : 0;
 
  // Protocol selection: the intersection must be non-empty.
  r.proto_mask = local_req.proto_mask & remote_cap.proto_mask;
  if (r.proto_mask == '0) r.agreed = 1'b0;
 
  return r;
endfunction

Architecture. A set intersection and a maximum — structurally different from the priority-encoder or comparison-chain shape an RTL implementation would use.

Why structural difference matters, and it is not superstition. A model written in the same shape as the design tends to make the same off-by-one, because the off-by-one lives in the shape. A set-based model has no boundary to be off by one at: either a width is in both sets or it is not.

Why agreed is false rather than defaulting. A negotiation with no common value is not an agreement to use the lowest — it is a failure, and the link must not become operational. §24 is the test that exercises it, and a model that quietly returns a minimum has made the incompatible case unreachable.

Contract. SUPPORTED_WIDTHS and SUPPORTED_RATES come from the capability structure (19.6 §20) or the test's own configuration — never from a package the design also imports, or 19.6 §53's shared-default failure returns.

// MANDATORY — the committed configuration matches the independent expectation.
property p_agreement_matches_independent_rule;
  @(posedge clk) disable iff (!por_n)
    obs_cfg_commit
      |-> (ref_cfg.observed_active
             == expected_agreement(ref_cfg.local_requested,
                                   ref_cfg.remote_capability));
endproperty
a_agreement_matches_independent_rule:
  assert property (p_agreement_matches_independent_rule);
 
// MANDATORY — no agreement means no operational phase.
property p_no_operation_without_agreement;
  @(posedge clk) disable iff (!por_n)
    (ref_link.phase == RM_OPERATIONAL) |-> ref_cfg.agreed;
endproperty
a_no_operation_without_agreement:
  assert property (p_no_operation_without_agreement);

21. ACTIVE Does Not Mean the Work Has No Past

The single most important sentence in this chapter for anyone writing a post-recovery test.

A link that returns to an operational state after a recovery is not a link that has just been brought up. It has:

• semantic obligations accepted before the fault, which must still complete;
• transport objects that may or may not have been delivered, depending on how far each got;
• a resource agreement that is void and must be re-established (19.5 §28);
• a configuration that may legitimately differ from the pre-fault one (§27);
• and a first-fault record that must still name the original cause (19.1 §35).

Three consequences for the environment.

A test that ends at "the link came back" has tested one of five things. The other four are where the failures are.

The was_operational flag of §7 is what selects the check set. After a restart, the environment expects a clean slate; after a recovery, it expects survivors. One model with one expectation cannot do both, and a test written for one will falsely pass or falsely fail the other.

And the post-recovery checks must run even when the recovery was injected deliberately. 20.1 §44's rule: every negative test asserts a positive outcome. "We injected a fault and the link recovered" is not a result; "the four outstanding operations all completed exactly once after the recovery, under a re-established credit agreement" is.

22. Flagship Trace 1 — Reset to First Completion

Illustrative. A clean bring-up, with monitor events and the four models' state at each step. Every model column changes for a reason that is written in the row.

Five readings.

Cycle 150 required two independent pieces of evidence. Permission arrived at 150 and the agreement was established at 130. Had permission arrived at 120 — before the agreement — the model would have stayed in RM_TRAINING and the admission at 152 would have failed §13's property. That is §9's bug, and this trace is the shape that catches it.

Credit is 0 from cycle 0 to cycle 144. Not 8, not the configured depth. 19.5 §35: the counter is populated only by an advertisement that came from the peer, and a reset value of capacity would have let cycle 152 admit into storage nobody confirmed.

The semantic obligation outlives the transport object. Accepted at 152, completed at 182 — thirty cycles, during which the object was allocated, attempted, delivered and resolved, and the replay entry came and went. Four lifecycles, four different durations, one row each (§4).

cfg_epoch is stamped on the semantic record at 152. Nothing in this clean trace uses it. It matters at cycle 152 of the next trace, where a configuration commit lands mid-operation and the record still says which rules apply.

And every model column is fed by an observed event. No column is ever written from a design register — which is the property §8 turned into a rule and this trace demonstrates end to end.

23. Negative Bring-Up Cases

Six injections, each with a specific expected outcome. 20.1 §44's rule holds throughout: the pass criterion is a positive statement, never "nothing broke".

Two notes.

Rows 1 and 6 both test a refusal. They are the rows that verify the design can say no — and a link that never refuses anything has an untested failure path that will first execute in the field, against a peer nobody tested with.

And the last column is the point of the table. Each injection's obvious check is easy; the listed check is the one that is skipped, and it is the one that distinguishes "recovered" from "recovered correctly".

24. Incompatible Configuration

The case that must produce nothing.

The peer advertises a capability set with no common width, or no common rate, or no common protocol. §20's independent rule returns agreed = 0.

Three expectations, and all three need asserting.

No operational phase. §20's p_no_operation_without_agreement covers it — and note this is a safety property: it says the link never becomes operational, not that it eventually fails.

No traffic admission. §13's properties, which are already live.

An explicit failure indication, within a bound. This is the liveness half: the link must report the incompatibility rather than retrying forever, and the bound comes from the permitted attempt count.

// MANDATORY — an unresolvable negotiation terminates in an explicit failure,
// not in an unbounded retrain loop.
property p_incompatible_terminates;
  @(posedge clk) disable iff (!por_n)
    (obs_cfg_exchange_done && !expected_agreement(ref_cfg.local_requested,
                                                  ref_cfg.remote_capability).agreed)
      |-> ##[1:MAX_TRAIN_ATTEMPTS * training_bound(MAX_LANES, 0, 0)]
          (ref_link.phase == RM_FAILED);
endproperty

The failure this catches, and it is common. A design whose negotiation returns a default when the intersection is empty — the lowest supported width, say — becomes operational with two dies that agreed on nothing. Both sides pick their own default; if the defaults differ, every transfer is misinterpreted. The link works, trains, reports healthy, and corrupts everything, and §19's shared-function checker would have passed it.

25. Training Restart, and What It Must Not Carry Forward

A restart is not a recovery (§7). It happens before any semantic work exists, so nothing needs to survive — and that makes the interesting question the opposite one: what must be discarded?

The trap is row 2 combined with row 3. A design that restarts training but keeps the previously computed agreement will, if the peer came back with a different capability, commit an agreement the peer never made. The environment catches it only because §18 keeps remote_capability and expected_agreed as separate tracked quantities and recomputes on every exchange — a model that stores only the final agreed value has nothing to recompute from.

And the last row is an assertion, not a comment. If the semantic model is non-empty when the link model enters RM_TRAINING from RM_RESET, the environment has mis-classified a recovery as a restart — which means every preservation check in §35 was skipped for that event.

// MANDATORY — an environment self-check, not a DUT check (20.1 §49).
property p_restart_implies_no_outstanding;
  @(posedge clk) disable iff (!por_n)
    ((ref_link.phase == RM_TRAINING) && !ref_link.was_operational)
      |-> (sem_model_outstanding == 0);
endproperty

26. Flagship Trace 2 — Training Restart

Illustrative. Training reaches a late phase, a fault forces a restart, and the configuration is re-derived rather than reused.

Four readings.

The peer came back different. x16/{A,B} before the restart, x8/{A} after — a legitimate outcome if the peer itself restarted and re-evaluated, or if a lane became unavailable in between. A model that cached the first agreement would expect x16 at cycle 244 and report a false failure.

The discard at cycle 128 is the whole test. If the design commits x16 at cycle 244 because it kept the earlier computation, §20's property fires — and it fires at the commit, not later when x16-striped traffic confuses an x8 peer.

phase_entry_cyc resets at 129, which restarts §15's progress watchdog. A watchdog that measures from the original training start will fire spuriously on any restart, and that is the second-most-common false failure in bring-up regressions after §16's fixed bound.

And link_epoch is still 1 at cycle 262. It counts entries to operational, not training attempts. Two attempts, one epoch — because no agreement existed until 244, and nothing could be stale against an agreement that never took effect.

27. Lane Availability and Degraded Configuration

The structure of the test, in three parts.

Before: the link is operational at some active width N, with outstanding semantic work.

During: a lane-health event makes the usable resource set smaller. The link recovers.

After: the active configuration may be smaller. The semantic work is unchanged in meaning — same operations, same addresses, same data, same completion requirements. Only performance changed.

The environment must therefore split its expectations into two categories, and this split is the section's real content:

A checker that puts any row of column 1 into column 2 misses real bugs. A checker that puts any row of column 2 into column 1 reports false failures — and §28 is the second kind, which is the kind that gets the whole degradation test disabled.

28. Wrong Checker — Expecting the Same Width Back

// WRONG — treats the pre-fault configuration as a semantic invariant.
property p_config_restored_after_recovery;
  @(posedge clk) disable iff (!rst_n)
    obs_recovery_exit |-> (ref_cfg.observed_active == $past(ref_cfg.observed_active));
endproperty

Worked. The link was x16. A lane became unusable. The recovery legally re-established the link at x8. The property fires on correct behaviour.

Four properties, and the fourth is why this is worth a whole section.

It is reported as a design bug, and the recovery path gets investigated for a day.

The "fix" is usually to relax it to >= or to delete it, and deleting it removes the only check that the configuration was re-established at all — so a recovery that comes back with a larger width than the resource set supports, or with no valid configuration, now passes.

The correct property is a bound derived from the resource set, not an equality:

// RIGHT — the new configuration must be legal for the CURRENT resources, and
// must be an agreement, and must not exceed what is physically available.
property p_degraded_config_legal;
  @(posedge clk) disable iff (!por_n)
    obs_recovery_exit
      |-> ref_cfg.agreed
       && (ref_cfg.observed_active.width <= ref_link.usable_lane_count)
       && (ref_cfg.observed_active
             == expected_agreement(ref_cfg.local_requested_masked,
                                   ref_cfg.remote_capability));
endproperty

And the fourth property: this failure trains people to stop testing degradation at all. A degraded-recovery test that produces false failures every run is the first thing removed from the nightly regression — so the configuration in which the link is most fragile becomes the configuration with the least coverage.

29. Semantic Invariants Across a Configuration Change

The properties that must hold regardless of what the configuration did.

// MANDATORY — a semantic operation's identity and content are not affected by
// a configuration change. The check is on the MODEL's record, which was
// captured at acceptance and is immutable afterwards.
property p_semantic_content_stable_across_recovery(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (obs_recovery_exit && sem_model.exists(tag))
      |-> (sem_model.addr_of(tag)  == sem_model.addr_at_accept(tag))
       && (sem_model.kind_of(tag)  == sem_model.kind_at_accept(tag))
       && (sem_model.epoch_of(tag) == sem_model.epoch_at_accept(tag));
endproperty
 
// MANDATORY — an operation accepted under one configuration epoch is completed
// under the rules of that epoch, whatever the current epoch is. 19.6 §24's
// property, restated at link level where the epoch change is a RECOVERY.
property p_operation_epoch_immutable(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (obs_sem_complete && (obs_tag == tag))
      |-> (obs_completion_epoch == sem_model.epoch_at_accept(tag));
endproperty
 
// MANDATORY — the count is unaffected. A degraded recovery changes throughput,
// never the number of obligations.
property p_outstanding_count_unchanged_by_config;
  @(posedge clk) disable iff (!por_n)
    obs_cfg_commit |=> (sem_model_outstanding == $past(sem_model_outstanding));
endproperty

Why the epoch is captured at acceptance rather than read live. §4's lifecycle rule: the semantic lifecycle is longer than the configuration lifecycle, so an operation can outlive the configuration it was accepted under. Reading the current epoch at completion time compares an operation against rules it was never subject to.

And why the third property uses |=> rather than |->. The commit is one cycle (19.6 §22); the check is that the count is the same after it. A same-cycle check would sample the count before the commit's effects settle and pass regardless.

30. Flagship Trace 3 — A Legal Degraded Recovery

Illustrative. Three operations outstanding, one lane lost, recovery to a narrower link.

Five readings.

The width halved and the outstanding count never moved. Column 4 is 3 from cycle 500 to cycle 640 — through the fault, the recovery, the renegotiation and the re-advertisement. That column is the semantic invariant, and it is what §28's checker was distracted from.

Each completion at 640, 690 and 742 carries epoch_at_accept = 3 while the current epoch is 4. §29's second property. A design that stamps the current epoch at completion would fail here, and it would fail correctly: it would mean the operations were completed under rules they never agreed to.

The credit agreement is voided at 504 and re-established at 596. 19.5 §28. Between those cycles the resource model expects no consumption — and §13's p_no_attempt_during_recovery is what enforces it.

The completions take longer than they would have at x16, and that is not a failure. §27's column 2.

And link_epoch went 3 → 4 while the operations' cfg_epoch_at_accept stayed 3. Two different epochs, two different lifecycles, deliberately not the same counter. A design or an environment with one epoch counter cannot express this trace.

31. Retry, End to End

20.1 §55 showed a retry that duplicated. This section builds the ledger that proves one does not — and extends it from a boundary check to a link-lifetime record.

The identity hierarchy, with the expected counts for a single retried operation:

The row that distinguishes a good environment from a weak one is "arrivals". It can legitimately be 1 or 2, and which one it is tells you which failure was injected — a corruption in flight produces two arrivals with one bad verdict; a drop produces one arrival. An environment that does not distinguish them cannot confirm the injection did what it intended.

32. The Identity Ledger

// ILLUSTRATIVE, VERIFICATION-ONLY. One record per semantic operation, alive
// from acceptance to completion — across any number of link events.
typedef struct {
  int unsigned mon_tag;             // 20.1 §23's join key — never a wire field
  int unsigned sem_id_observed;     // as seen; may be legitimately reused later
  int unsigned generation;
  int unsigned obj_ids[$];          // transport objects carrying this operation
  int unsigned attempt_cycles[$];   // one entry per physical attempt
  int unsigned arrival_cycles[$];
  int unsigned verdicts[$];         // per arrival
  int unsigned deliveries;          // MUST end at exactly 1
  int unsigned completions;         // MUST end at exactly 1
  int unsigned cfg_epoch_at_accept;
  int unsigned link_epoch_at_accept;
  int unsigned recoveries_spanned;
  int unsigned accept_cycle, complete_cycle;
} sem_record_t;
 
sem_record_t ledger [int unsigned];   // keyed by mon_tag

Architecture. Queues rather than counters for anything that can happen more than once, because 20.1 §19's bitmap argument applies to verification records too: a count of attempts cannot answer "were attempts 2 and 3 the same object or different ones", and a queue of cycles can.

deliveries and completions are the only two scalars that must end at exactly one, and they are deliberately separate. A delivery that produced no completion is work that arrived and was dropped locally; a completion with no delivery is a completion invented on this side. Both are serious and they are different bugs.

recoveries_spanned is the field that turns a pass into evidence. A regression in which no record has recoveries_spanned > 0 has never tested §35, however many recoveries occurred — because the recoveries all happened when nothing was outstanding, which is the easy case.

// MANDATORY — the ledger's terminal check, run at end of test on every record.
function automatic void check_ledger_final();
  foreach (ledger[t]) begin
    assert (ledger[t].deliveries  == 1)
      else $error("tag %0d: %0d deliveries", t, ledger[t].deliveries);
    assert (ledger[t].completions == 1)
      else $error("tag %0d: %0d completions", t, ledger[t].completions);
    assert (ledger[t].attempt_cycles.size() >= 1);
    // An operation with more attempts than arrivals+1 means an attempt was
    // made that could not have been triggered by an observed failure.
    assert (ledger[t].attempt_cycles.size()
              <= ledger[t].arrival_cycles.size() + 1)
      else $error("tag %0d: unexplained retransmission", t);
  end
endfunction

The last assertion is 20.1 §33's R3 in ledger form — a retransmission with no observed trigger. It catches a spontaneous retry, which still results in exactly one delivery and would otherwise pass every other check in the function.

33. Flagship Trace 4 — One Retry, One Delivery

Illustrative. A corruption injected after integrity was computed (§43's point 3).

Terminal check: 1 semantic operation, 1 object, 2 attempts, 2 arrivals, 1 delivery, 1 completion. Every row of §31's table satisfied.

Four readings.

Object 12 appears in both attempts. obj_ids has one entry. A design that allocated a new object for the retransmission would produce obj_ids = [12, 13], which is not wrong by itself — it depends on the architecture — but it changes the credit question (19.5 §51), and the ledger is what makes that visible rather than assumed.

Cycle 719 is a negative observation and it needs the model. Nothing happened, and "nothing happened" over an unbounded window is not an assertion-shaped statement.

attempt_cycles.size() is 2 and arrival_cycles.size() is 2, so the unexplained-retransmission check passes with no slack. Had the first attempt never arrived, arrivals would be 1 and attempts 2 — still legal, still within the bound, and a different injected fault.

And one credit was consumed for two attempts. Whether that is correct is §38's question and 19.5 §51's open one. The ledger records the fact rather than asserting the rule — which is the honest position, and it makes the trace an experiment that answers the question for a given implementation pair.

34. Recovery With a Live Request

The scenario this chapter exists for. Everything before it is preparation.

The setup. A semantic operation is accepted. Its transport object is committed and attempted. Then a recoverable fault occurs — after the attempt, before any resolution. Recovery begins.

Eight things must be true, and each is a separate check:

Requirement 8 is the whole point. Requirements 1 to 7 are all locally checkable and all of them can pass while 8 fails — which is the definition of the failure class that has no local observable (§1).

35. Semantic Obligations Survive a Transport Recovery

// MANDATORY. The preservation property, stated positively: the model's
// outstanding set is UNCHANGED by a recovery. Note the disable condition —
// this must remain live THROUGH the recovery, which is exactly the window
// where a blanket `disable iff (recovery)` would put it to sleep.
property p_semantic_survives_recovery;
  @(posedge clk) disable iff (!por_n)
    obs_recovery_entry |=> (sem_model_outstanding == $past(sem_model_outstanding));
endproperty
a_semantic_survives_recovery: assert property (p_semantic_survives_recovery);
 
// MANDATORY — per-tag, because a count can be preserved while the SET changes.
// One obligation lost and one invented keeps the count identical.
property p_every_outstanding_tag_survives(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (obs_recovery_entry && sem_model.is_outstanding(tag))
      |=> sem_model.is_outstanding(tag)
          until_with (obs_sem_complete && (obs_tag == tag));
endproperty
 
// MANDATORY — the DESIGN's own outstanding state agrees. This is the property
// that catches a recovery wired to a global reset (§12's design bug).
property p_dut_retains_outstanding_across_recovery;
  @(posedge clk) disable iff (!por_n)
    obs_recovery_exit |-> (obs_dut_outstanding_count == sem_model_outstanding);
endproperty
a_dut_retains_outstanding_across_recovery:
  assert property (p_dut_retains_outstanding_across_recovery);

Three properties, three different failures.

The count property catches a wholesale clear.

The per-tag property catches something the count cannot: a substitution. One obligation dropped and another created keeps the count at four. This is not hypothetical — it is what an identity-reuse bug looks like after a recovery, where a freed slot is reallocated to a new request while the old one is still expected.

And the third property is the one that requires the environment to have survived independently. It compares the design's count to the environment's, which is only meaningful because §12's policy kept the environment's model alive. With §12's wrong checker, this property compares zero to zero and passes.

On the disable condition, which is the section's durable lesson. All three use disable iff (!por_n) — not disable iff (!rst_n || recovery_active). A property about what survives a recovery must be evaluated during that recovery. This is 20.3's flagship SVA anti-pattern and it is introduced here because this is where the consequence is concrete: the bug happens precisely while the disabled checker is asleep.

36. Flagship Trace 5 — Recovery With a Live Request

Illustrative. One operation accepted and attempted; fault; recovery; completion.

Six readings.

Column 4 is 1 for 116 cycles, across the fault, the whole recovery and the renegotiation. That is requirement 2 of §34, and it is what §12's wrong checker would have zeroed at cycle 811.

Cycles 813 to 869 contain no admissions and no attempts. §13's p_no_attempt_during_recovery. An attempt in this window would be traffic sent into a link that has no agreement.

Cycle 878 advertises exactly 8, and the counter becomes exactly 8. 19.5 §12's equality property. Note it is not 5 + something — the pre-fault agreement was void, so the new count is the new advertisement and nothing else. §40 is the trace where a straggler tries to change that.

Attempt 2 at cycle 890 consumed a credit — 8 → 7. Whether it should have is 19.5 §51's open question, and here the answer is forced: the old agreement was voided, so any transmission under the new agreement consumes new credit regardless of the retained-allocation rule. That is a genuine architectural consequence of recovery and it is worth noticing — the retained-allocation question only arises within an epoch.

arrival_cycles has one entry, not two. The first attempt never arrived — the fault destroyed it in flight. §31's row 5: one arrival, two attempts, and that combination tells you which fault was injected.

And cfg_epoch_at_accept is 5 while the completion happens under epoch 6. §29's second property, exercised.

37. Lost-Response Ambiguity

The hardest case in link verification, and the one where an environment most often asserts something it cannot know.

The situation. A request was delivered to the far end. The far end performed the semantic action — a write landed, a cache line changed state, a counter incremented. The response was lost. The local side times out.

What the local side knows: it sent a request and got no response.

What the local side does not know: whether the action happened.

Three possible architectural policies, and the environment must model whichever one applies:

The practical consequence for the data model. Where the environment tracks expected memory or cache contents, a lost response creates a location whose expected value is a set rather than a value. Subsequent reads must accept either member until something resolves the ambiguity — a subsequent write, an explicit status, or a completion. A data model with no set-valued expectation cannot represent this at all, and will report a false mismatch on the very next read.

38. Credit State Across Recovery

19.5 built the credit machine and its epoch. This section verifies it at link scale, where the epoch's purpose becomes concrete.

Four things the environment checks across a recovery:

// MANDATORY — the agreement is void from recovery entry until re-advertisement.
property p_no_consumption_without_agreement;
  @(posedge clk) disable iff (!por_n)
    obs_credit_consume |-> res_model.agreement_valid;
endproperty
a_no_consumption_without_agreement:
  assert property (p_no_consumption_without_agreement);
 
// MANDATORY — the counter equals the advertisement exactly, not "at least".
property p_credit_exactly_readvertised;
  @(posedge clk) disable iff (!por_n)
    obs_credit_advert |=> (obs_credit_count == $past(obs_advert_value));
endproperty
a_credit_exactly_readvertised: assert property (p_credit_exactly_readvertised);
 
// MANDATORY — a return tagged to a dead agreement changes nothing.
property p_stale_return_inert_at_link_level;
  @(posedge clk) disable iff (!por_n)
    (obs_credit_return && (obs_return_epoch != res_model.epoch))
      |=> (obs_credit_count == $past(obs_credit_count)) || $past(obs_credit_advert);
endproperty
 
// MANDATORY — the pending-return accumulator does not cross the epoch.
property p_pending_cleared_by_recovery;
  @(posedge clk) disable iff (!por_n)
    obs_recovery_entry |=> (obs_pending_returns == '0);
endproperty

Note the exactness of the second property, once more. It is the highest-value single line in the credit chapter and it is worth restating here because at link level it is the only thing standing between a recovery and a silent over-advertisement — the counter lands inside its legal range, every bound passes, and the receiver overflows several thousand cycles later when it happens to be full.

39. Wrong Recovery Verification — Comparing the Final Counter

// WRONG — the entire post-recovery credit check.
initial begin
  wait (recovery_done);
  assert (dut.credit_q == EXPECTED_AFTER_RECOVERY)
    else $error("credit wrong after recovery");
end

Why a final-value comparison proves nothing. The counter is a state; the failures are in the transitions. Three distinct bugs produce a correct final value:

All three are serious. All three pass.

Three properties of this failure mode.

The over-allocation case has already caused damage by the time the check runs. Two objects entered storage that did not exist; whatever the receiver did with them — dropped, overwrote, blocked — happened at the moment of over-allocation and is not undone by the counter returning to a legal value.

The second case is the one that recurs. 19.5 §53's argument in full: bounds and final values catch gross failures; conservation catches accounting failures, and accounting failures are what reaches silicon.

And the fix is to check the event stream, not the endpoint — the conservation identity evaluated continuously, plus a maximum-excursion check across the transition:

// RIGHT — conservation holds continuously, AND the excursion is bounded.
property p_credit_conserved_through_recovery;
  @(posedge clk) disable iff (!por_n)
    (res_model.advertised - res_model.consumed + res_model.returned
       == obs_credit_count);
endproperty
a_credit_conserved_through_recovery:
  assert property (p_credit_conserved_through_recovery);
 
// RIGHT — the count never exceeded capacity at ANY point, not just at the end.
property p_credit_never_exceeded_capacity;
  @(posedge clk) disable iff (!por_n)
    (obs_credit_count <= res_model.active_capacity);
endproperty
a_credit_never_exceeded_capacity:
  assert property (p_credit_never_exceeded_capacity);

40. Flagship Trace 6 — The Stale Credit Return

Illustrative. 19.5 §29's failure, observed at link level with the guard present.

And the same trace with the guard absent:

Four readings.

Cycle 1064 is one addition and it is permanent. The counter is 3 too large until the next resynchronisation.

The exactness property fires at 1064, naming the cause at the cycle it happened. The bound property also fires there — 19 exceeds 16 — but it says only "too large", and a team can spend a week deciding whether the capacity constant is wrong. Exactness says "a straggler was absorbed into the new epoch", which is a one-afternoon fix.

The stale count incrementing at 1064 is not an error. It is the guard working, and a run in which it is zero has not tested the guard — which is why it appears as a coverage bin in §53 rather than only as a diagnostic.

And the mirror failure has no symptom at all. If the re-baseline had happened after the straggler rather than before, the straggler would be overwritten and the link would run permanently 3 credits short — no assertion, no bound exceeded, just reduced throughput forever. That is why the guard must reject stale returns rather than merely ordering the updates.

41. Fatal Faults and Obligation Classification

A fatal fault does not complete anything. The outstanding obligations do not evaporate, and they do not silently succeed — they must be classified, and the classification is an architectural policy the environment models rather than invents.

Three rules.

Every outstanding obligation gets exactly one classification. The environment's terminal check (§32) requires completions == 1 for successful operations; for a fatal run it requires each record to carry exactly one terminal classification instead. A record with neither is work that vanished.

"Unknown" must be representable. §37's argument: an operation that was delivered but whose response was lost when the link died is not "failed", and calling it failed will cause a client to reissue a write that already landed.

And RM_FAILED does not self-clear (§10). A link that recovers from a fatal condition on its own has destroyed the evidence — 19.5 §32 made the same argument about the credit machine's fault state, and 19.1 §35 about the first-fault record. The exit is a deliberate, externally commanded reset.

// MANDATORY — a fatal condition does not return to operational without a
// deliberate reset. The negative form, which fails on the arc rather than
// on a symptom.
property p_fatal_requires_deliberate_reset;
  @(posedge clk) disable iff (!por_n)
    (ref_link.phase == RM_FAILED)
      |-> (ref_link.phase == RM_FAILED) until_with obs_hard_reset;
endproperty
a_fatal_requires_deliberate_reset:
  assert property (p_fatal_requires_deliberate_reset);
 
// MANDATORY — every outstanding obligation is classified, none forgotten.
property p_fatal_classifies_all_outstanding;
  @(posedge clk) disable iff (!por_n)
    obs_fatal_indication
      |-> ##[1:FATAL_REPORT_BOUND] (sem_model_unclassified == 0);
endproperty

42. Flagship Trace 7 — A Fatal Fault

Illustrative. Four operations outstanding at different stages when a persistent fault exhausts the retrain budget.

Five readings.

A and B are failed; C and D are unknown. The difference is whether the far end may already have acted. A was never transmitted and B's attempt was destroyed, so neither took effect. C was delivered — the far end did the work — and D was mid-completion. A design that classifies all four identically has given the client wrong information about two of them.

The unknown classification is the one that costs software work, and it is the correct answer. A client that reissues C's write may double-apply it; a client told C "failed" will reissue it without hesitating.

No automatic recovery between 1470 and 2000. §41's property. A link that quietly retrained at 1600 would have cleared the fault state and the first-fault record with it, and the post-mortem would have nothing.

Nothing completes. Column headers A through D never reach a completion; the ledger's terminal check for this run requires a classification instead. A test whose pass criterion is "all operations completed" cannot express this run at all and will report a failure on correct fatal handling.

And the reset at 2000 reports the abandonment rather than silently clearing (§12). Four operations were destroyed by a deliberate reset; that is information, and the log is where it goes.

43. The Fault-Injection Architecture

Seven injection points, each exercising a different mechanism. The rule throughout: inject at contract boundaries, never by forcing an internal register.

Why point 3 is stated so specifically. 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, and the distinction is the difference between a test that passes vacuously and one that verifies a feature.

Why point 5 is the one nobody builds. 19.5 §24's duplicate return and 18.4 §20's lost return both live here. A dropped credit return produces a link that slowly stops with every safety property passing, and only a conservation model detects it.

And why point 7 produces the cross-feature bugs. A recovery forced during live traffic with a configuration change in flight exercises §34, 19.5 §29's straggler, 19.2 §44's semantic table and 19.6 §23's partial commit in one test — because those are all failures at the intersection of two features that are otherwise verified separately.

The injection record. Every injection writes a record the environment can correlate against later:

// ILLUSTRATIVE. What the injector logs, so §46 can correlate.
typedef struct {
  int unsigned cycle;
  int unsigned point;          // 1..7 above
  int unsigned target_tag;     // which object/operation, where applicable
  string       description;
  int unsigned expected_detector;   // which mechanism SHOULD notice
  int unsigned expected_recovery;   // which recovery SHOULD run
} injection_record_t;

That last pair is what makes an injection a test. 20.1 §44's rule: "we injected a fault and nothing crashed" is not a result. Naming the expected detector and the expected recovery in the injection record turns each injection into a checkable statement.

44. One Cause at a Time

Single-fault determinism is a debuggability requirement, not a purity preference.

Why. The environment's most valuable output is the first divergence (20.1 §60). With two simultaneous injections, the first divergence has two candidate causes, and the environment cannot rank them — so the output degrades from "the Adapter formed two objects at cycle 8,412" to "something went wrong somewhere after cycle 8,400".

The progression.

Stage 1 — one fault, one type, at one point, in a quiet link. Every injection point gets its own directed test. The expected detector and recovery are asserted (§43). This stage is where the mechanisms are verified.

Stage 2 — one fault at a time, under load. Same injections, with traffic and backpressure. This is where interactions between a mechanism and the traffic it must not disturb appear.

Stage 3 — multiple faults, deliberately combined. Chosen combinations, not random ones: a recovery during a configuration commit; a credit-return drop during a recovery; a lane loss during a retry. Each combination is a hypothesis about an interaction, and it is worth running because §43's last paragraph is where the cross-feature bugs are.

Stage 4 — random multi-fault, with rate limits. Useful for finding what nobody hypothesised, and useful only if stages 1 to 3 pass — otherwise every failure has an ambiguous cause and the runs produce noise rather than findings.

The rule that ties the stages together: a failure found in stage 4 is reduced to a stage-1 or stage-2 test before it is fixed. A bug that can only be reproduced by a random multi-fault seed is a bug whose fix cannot be verified.

45. Wrong Injection — Everything At Once

// WRONG — the "stress test" that finds bugs nobody can fix.
initial forever begin
  @(posedge clk);
  if ($urandom_range(0,99) < 5) inject_crc_error();
  if ($urandom_range(0,99) < 3) drop_credit_return();
  if ($urandom_range(0,99) < 2) force_recovery();
  if ($urandom_range(0,99) < 1) drop_lane();
end

What this produces. A run that fails. Somewhere in it, four injection types occurred hundreds of times, and the environment reports a semantic loss at cycle 40,000.

Four properties.

The first divergence is ambiguous by construction. Was the loss caused by the CRC error at 39,800, the recovery at 39,850, or the credit return dropped at 39,900? All three are plausible and the environment cannot say.

It is not reproducible in a useful sense. The seed reproduces the failure, and the failure is 40,000 cycles into a run with four concurrent fault streams. Reducing it by hand is days of work, and it is the work that must happen before anybody can fix anything.

The injection rates interact. A forced recovery every ~50 cycles means the link is almost never operational, so the traffic-path mechanisms this test was supposed to stress are barely exercised — and the coverage report will show it, if anybody reads it.

And it hides the mechanisms that are entirely broken. If credit-return dropping is never detected, the run fails for other reasons long before anybody notices that one specific detector never fired. Stage-1 directed tests fail loudly and specifically; the stress test fails vaguely and often.

Random multi-fault injection is a last stage, not a first one. It is valuable for finding interactions nobody predicted, and it is worthless as a substitute for the directed tests that prove each mechanism works at all.

46. First-Fault Correlation

The environment knows what it injected first. The design reports what it saw first. Comparing them verifies the diagnostic path — which is otherwise unverified until somebody depends on it during a silicon debug.

// ILLUSTRATIVE. Compare the design's first-fault record against the injection
// log. Note what is and is not compared.
function automatic void check_first_fault();
  injection_record_t first = injection_log[0];
 
  // COMPARED: that a first-fault record exists at all.
  assert (dut_first_fault.valid)
    else $error("fault injected at cycle %0d; no first-fault record", first.cycle);
 
  // COMPARED: the CLASS, which the contract defines (19.6 §39).
  assert (dut_first_fault.err_class == first.expected_detector)
    else $error("first fault class %0d, expected %0d",
                dut_first_fault.err_class, first.expected_detector);
 
  // COMPARED: that it names the FIRST event, not a later cascade.
  assert (dut_first_fault.cycle <= first.cycle + DETECT_LATENCY_MAX)
    else $error("first-fault record names a later event (cascade captured)");
 
  // COMPARED: the epochs, which turn "an error happened" into a reproducible
  // statement (19.6 §40).
  assert (dut_first_fault.link_epoch == ref_link.link_epoch_at(first.cycle));
 
  // NOT COMPARED: the internal error code, the state snapshot, or any encoding
  // the contract does not define. Those are forwarded to the vendor, not
  // decoded by the environment (19.6 §40).
endfunction

Three notes.

The third assertion is the valuable one. 19.1 §35 and 13.3 §12 both established sticky-first rather than sticky-last, because errors cascade. This check is the only thing that verifies the design actually implemented first rather than last — and a last-capture implementation passes every other test in the suite.

What is deliberately not compared is anything whose encoding the contract does not define. Asserting on an internal error code couples the environment to the implementation (19.6 §18), and the first internal refactor breaks the test.

And this check requires §44's single-fault discipline. With four concurrent injection streams, "the first injected fault" is not well defined, and the comparison is meaningless.

47. Link Liveness, With the Assumptions Written Down

// The assumptions, stated next to the property they support. In formal these
// are `assume`; in simulation they are constraints on the environment — and in
// BOTH cases they must be written down (20.1 §28).
//
//  A1  clocks continue and the hard reset is not re-asserted
//  A2  the peer eventually responds to a delivered object
//  A3  injected errors eventually cease
//  A4  the downstream client eventually accepts completions
//  A5  arbitration is fair — an eligible requester remains eligible
//  A6  the physical conditions permit training to succeed at SOME configuration
assume property (@(posedge clk) s_eventually !injection_active);
assume property (@(posedge clk) s_eventually downstream_ready);
 
// MANDATORY — a recoverable link returns to service or fails explicitly.
// Note it is a DISJUNCTION: an explicit failure is a legal outcome.
property p_recovery_converges;
  @(posedge clk) disable iff (!por_n)
    (ref_link.phase == RM_RECOVERY)
      |-> ##[1:RECOVERY_BOUND] ((ref_link.phase == RM_OPERATIONAL)
                             || (ref_link.phase == RM_FAILED));
endproperty
a_recovery_converges: assert property (p_recovery_converges);
 
// MANDATORY — every accepted obligation reaches a terminal state, including
// a classification (§41). This is the link-level completion property.
property p_obligation_terminates(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (obs_sem_accept && (obs_tag == tag))
      |-> ##[1:OBLIGATION_BOUND] (sem_model.is_terminal(tag));
endproperty

Three notes.

p_recovery_converges is a disjunction and that is deliberate. An explicit failure is a correct outcome for an unrecoverable link. A property that demands a return to RM_OPERATIONAL fails on correct fatal handling — §42's trace — and gets weakened until it checks nothing.

A6 is the assumption that is easy to forget and easy to violate. A test that injects a permanent physical fault has broken A6, so p_recovery_converges is not expected to hold in the operational direction — it holds in the failure direction, and the test's pass criterion is §41's classification check rather than a return to service.

And OBLIGATION_BOUND must include a recovery. A bound derived from clean-link latency will fire on every run that injects a fault. The derivation is the artefact (20.1 §27): round trip, plus the maximum permitted retries, plus one full recovery, plus the peer's response budget.

48. Deadlock Versus Failed Training

Two conditions that both present as "the link is not making progress" and have nothing else in common.

The distinguishing observable is the link phase, and it is available immediately. A single "test timed out" report distinguishes neither, which is why §49 exists.

Three deadlock shapes the link environment must be able to name, all of which occur with the link fully operational:

Stranded capacity — sender credit zero, receiver occupancy below capacity, pending returns non-zero and stable. 19.5 §42's batching deadlock or 19.5 §49's return starvation.

Progress-reserve exhaustion — receiver full of requests whose completions cannot be admitted. 19.5 §46.

Scheduler starvation — one traffic kind never scheduled, with resources available. 19.3 §41.

None of these is a link-lifecycle problem, and all of them will be investigated as one unless the environment reports the phase alongside the timeout.

49. Per-Layer Progress Watchdogs

One global timeout tells you the run hung. Four scoped watchdogs tell you where.

// ILLUSTRATIVE. One age counter per layer, each with its own derived bound.
// The FIRST one to expire is the diagnostic.
typedef struct {
  int unsigned training_phase_age;   // since the last progress event (§15)
  int unsigned oldest_object_age;    // since the oldest Adapter object was committed
  int unsigned oldest_sem_age;       // since the oldest semantic accept
  int unsigned pending_return_age;   // since returns first became pending
  int unsigned recovery_age;         // since recovery entry
} progress_ages_t;
 
// Each bound is DERIVED, and each expiry names a different subsystem.
always @(posedge clk) begin
  if (ages.training_phase_age > training_bound(cfg.lanes, cfg.rate_idx, 0))
    $error("PROGRESS: training stalled — see §15, §16");
  if (ages.oldest_object_age  > OBJECT_BOUND)
    $error("PROGRESS: transport object unresolved — reliability or scheduler");
  if (ages.oldest_sem_age     > OBLIGATION_BOUND)
    $error("PROGRESS: semantic obligation unresolved — response path");
  if (ages.pending_return_age > FLUSH_TIMEOUT + RETURN_PATH_MAX)
    $error("PROGRESS: credit returns not emitted — 19.5 §42 / §49");
  if (ages.recovery_age       > RECOVERY_BOUND)
    $error("PROGRESS: recovery not converging — §47");
end

Three properties of scoped watchdogs.

The first to expire is the localisation. If the credit-return age expires while the semantic age is still climbing, the semantic stall is a consequence of the credit stall — and the investigation starts at flow control rather than at the protocol engine.

Each bound is derived from a different quantity, so each is meaningful. A single bound large enough for the slowest of them is far too large for the fastest, which is why one global timeout catches only total hangs and never slow progress.

And they must run in passing tests too. A watchdog that only reports on failure has no baseline. Logging the maximum observed age per layer per run turns them into a slow-degradation detector, which is how a link that is getting worse over a release is noticed before it stops.

50. The Cross-Layer Trace Record

One record per semantic operation, and it is the artefact that survives into post-silicon.

Three uses, and the third is why this section is here rather than in 20.4.

Failure localisation. 20.1 §60's first-divergence table is computed directly from these records, sorted by boundary.

Latency analysis in a passing run. delivery_cycle − accept_cycle split by recoveries_spanned separates clean-path latency from recovery-inflated latency — which is the number 15.2 needs and which no aggregate average provides.

And the same record shape works in silicon. A hardware trace buffer that captures object identity, attempt count, epoch and cycle produces the same table with fewer columns. The environment that debugs pre-silicon failures with this record is the environment whose engineers already know how to read the post-silicon one — and the diagnostic vocabulary transfers with it.

51. Five Models at Link Level

20.1 §30 to §34 built four. Link verification adds a fifth, and the addition is the point.

Why the fault model is a model rather than a log. It carries expectations: which detector should fire, which recovery should run, what the models should look like afterwards. A log records what was injected; a model states what should follow — and §46's first-fault correlation is only possible because the expectation was recorded at injection time rather than reconstructed afterwards.

Why they are five rather than one. 20.1 §37's argument, sharpened by the link lifecycle: the five fail independently and the failing one is the localisation. A semantic-model failure means work was lost; a link-model failure means the phase was wrong; a resource-model failure means accounting broke; a fault-model failure means a detector did not fire. Merging any two loses the distinction that makes the report actionable.

20.4 owns how these are implemented — the data structures, the matching engines, the distribution across a UVM environment. This chapter owns what they must contain, and the distinction is deliberate: a model whose contents are wrong cannot be rescued by a good implementation.

52. The SVA Inventory

Representative, not exhaustive — 20.3 owns the full catalogue. These are the properties link verification cannot do without.

Three observations.

Rows 1, 2, 7 and 14 all compare the design against the model. They are the rows that make §8's principle operational — and every one of them is a tautology if the model reads the design's registers.

Rows 19 and 20 replace what a naive plan would write as one endpoint comparison (§39). The continuous forms catch three bugs the endpoint form cannot.

And row 9 is not a design property at all. It is the environment checking itself — 20.1 §49's discipline — and an inventory with no such rows has no mechanism for noticing that its own classification of events is wrong.

53. Coverage

// ILLUSTRATIVE. Link-lifecycle coverage — the FOUNDATION scenarios. The full
// functional-coverage model is 20.5's subject; these are the bins without
// which the checks above are unexercised.
covergroup cg_link_lifecycle @(posedge clk);
 
  // --- Lifecycle phases and the arcs between them ---
  cp_phase: coverpoint ref_link.phase {
    bins reset = {RM_RESET};        bins training    = {RM_TRAINING};
    bins oper  = {RM_OPERATIONAL};  bins recovery    = {RM_RECOVERY};
    bins failed = {RM_FAILED};
  }
  cp_arc: coverpoint ref_link.phase {
    bins train_to_oper  = (RM_TRAINING    => RM_OPERATIONAL);
    bins train_restart  = (RM_TRAINING    => RM_TRAINING);      // §26
    bins oper_to_recov  = (RM_OPERATIONAL => RM_RECOVERY);
    bins recov_to_oper  = (RM_RECOVERY    => RM_OPERATIONAL);
    bins recov_to_fail  = (RM_RECOVERY    => RM_FAILED);        // §42
    bins train_to_fail  = (RM_TRAINING    => RM_FAILED);        // §24
  }
 
  // --- Configuration outcomes, including the refusal ---
  cp_negotiation: coverpoint ref_cfg_outcome {
    bins agreed_full     = {NEG_FULL};
    bins agreed_degraded = {NEG_DEGRADED};                      // §30
    bins incompatible    = {NEG_NONE};                          // §24
  }
  cp_active_width: coverpoint ref_cfg.observed_active.width {
    bins supported[] = {SUPPORTED_WIDTHS};
  }
  cp_width_change: coverpoint width_changed_by_recovery {
    bins same     = {1'b0};
    bins narrower = {1'b1};                                     // §27, §30
  }
 
  // --- The cases that make the recovery checks meaningful ---
  cp_outstanding_at_event: coverpoint sem_model_outstanding iff (obs_recovery_entry) {
    bins none = {0};                    // the easy case
    bins one  = {1};
    bins many = {[2:$]};                // §35 — the case that must be non-empty
  }
  cp_recoveries_spanned: coverpoint ledger_recoveries_spanned iff (obs_sem_complete) {
    bins none = {0};
    bins one  = {1};                                            // §36
    bins many = {[2:$]};
  }
  cp_attempts: coverpoint ledger_attempt_count iff (obs_sem_complete) {
    bins one     = {1};
    bins two     = {2};                                         // §33
    bins several = {[3:$]};
  }
 
  // --- Credit events across the epoch boundary ---
  cp_stale_return: coverpoint stale_return_seen {
    bins never = {1'b0};
    bins seen  = {1'b1};                                        // §40
  }
  cp_credit_at_recovery: coverpoint credit_count iff (obs_recovery_entry) {
    bins zero    = {0};
    bins partial = {[1:$]};             // returns may be in flight — §40
  }
 
  // --- Reset scenarios (§11) ---
  cp_reset_kind: coverpoint reset_kind {
    bins cold = {RST_COLD}; bins recovery = {RST_RECOVERY}; bins config = {RST_CFG};
  }
  cp_reset_with_work: coverpoint sem_model_outstanding iff (obs_any_reset) {
    bins idle    = {0};
    bins working = {[1:$]};             // §11 — the row that matters
  }
 
  // --- Fault injection: every point exercised (§43) ---
  cp_injection_point: coverpoint injection_point {
    bins pts[] = {[1:7]};
  }
 
  // --- Crosses ---
  x_recovery_with_work:  cross cp_outstanding_at_event, cp_width_change;
  x_reset_with_work:     cross cp_reset_kind, cp_reset_with_work;
  x_attempts_x_recovery: cross cp_attempts, cp_recoveries_spanned;
  x_negotiation_x_arc:   cross cp_negotiation, cp_arc;
 
endgroup

Four notes on which bins earn their place.

cp_outstanding_at_event.many is the bin that validates §35. A regression where every recovery happened with nothing outstanding has exercised the recovery path and never tested preservation — which is the whole subject of §34 to §36.

cp_reset_with_work.working is the same argument for reset. 19.6 §60 made it for the reset matrix: a reset applied to an idle design preserves nothing and clears nothing observable.

cp_stale_return.seen proves the epoch guard was exercised, not merely present. An unhit bin here means §40's flagship failure is unverified.

And cp_negotiation.incompatible is the refusal bin. A link that has never been asked to refuse has an untested failure path — and it is the path that first executes against a peer nobody tested with.

54. Debug Taxonomy

Seven symptoms, each with a first place to look.

Never reaches operational. Training or negotiation. Check which evidence the model is missing (§10) — the model's phase and its cfg_valid flag together say whether permission or agreement is the blocker, and they are different subsystems.

Operational but cannot send. Credit, admission or configuration. The link phase is RM_OPERATIONAL, so this is not a lifecycle problem (§48). Check credit against receiver occupancy; if occupancy is below capacity with zero credit, capacity is stranded and the fault is in the return path.

Traffic works until the first retry. Reliability identity or history. The ledger's obj_ids and attempt_cycles (§32) say immediately whether the retransmission reused the object or allocated a new one — and whether the retry had an observed trigger.

A response is lost after a recovery. Semantic state lifetime. This is §12's design bug or §35's property failing. Check whether the design's outstanding count matches the model's at recovery exit; if the design is at zero and the model is not, a recovery cleared semantic state.

Credit exceeds capacity after a recovery. Epoch or resynchronisation. §40. stale_return_q and the exactness property together say whether a straggler was absorbed or the guard is missing entirely — if both the stale count and the failure are zero, the guard was never exercised rather than working.

Only the degraded-width scenario fails. A configuration-dependent checker or a configuration-dependent design path. §28 first — the checker is more often wrong than the design here — then a parameter-derived width in the design (19.6 §45).

A timeout with no assertion firing. Missing progress localisation. §49. A single global timeout produces exactly this report; five scoped watchdogs produce a named subsystem.

55. Debug Checklist

A link-level failure is reported. In order:

1. What phase does the reference model believe the link is in? Not the design — the model.
2. Do the model and the design agree about the phase? If not, that disagreement is the finding.
3. Is there an agreed configuration, and does it match the independent rule (§20)?
4. What is the active width and rate, and is it legal for the current usable resources?
5. Which link epoch is in force, and when did it last change?
6. Which configuration epoch is in force?
7. How many semantic obligations are outstanding, in the model and in the design?
8. Do those two numbers agree? If the design is lower, semantic state was cleared.
9. For each outstanding obligation: what is its age (§49), and what is it waiting for?
10. Has any obligation spanned a recovery? If recoveries_spanned is zero everywhere, §35 is untested.
11. What is the oldest unresolved transport object, and how many attempts has it had?
12. Does any object have more attempts than arrivals + 1? (§32) — an unexplained retransmission.
13. What is the credit count, and what is the receiver's occupancy?
14. Is occupancy at capacity, or below it? This one comparison splits congestion from a stranded link.
15. Are pending returns non-zero and unchanging? (§48) — the batching or arbitration deadlock.
16. Has a stale return been rejected, and was it during a recovery or during steady state?
17. Does conservation close, evaluated continuously rather than at the end (§39)?
18. Did the credit count exceed capacity at any point, not just at the end?
19. Which fault was injected first, and at which point (§43)?
20. Did the expected detector fire? If not, the detection mechanism is the bug, not the recovery.
21. Did the expected recovery run?
22. Does the design's first-fault record name the first injected event, or a cascade (§46)?
23. Were multiple faults injected concurrently? If so, reduce to a single-fault test before continuing (§44).
24. Which progress watchdog expired first (§49)? The first is the localisation; the rest are consequences.
25. Did any reset occur, and of which kind?
26. Was there outstanding work at that reset, and was it classified or silently dropped (§12)?
27. If the link is in a fatal state: is every outstanding obligation classified, and is any of them unknown (§37, §41)?
28. Is the environment's own model self-consistent? — a restart with outstanding work (§25), a tag with no work, or work with no tag (20.1 §36) are environment bugs, and they must be excluded before any design conclusion.

56. Common Misconceptions

"Link verification is bring-up testing." Bring-up is one of ten conditions (§5). The other nine include everything that happens after the link works, and the tenth — semantic delivery exactly once across faults — has no local observable at all.

"ACTIVE means the link is correct." It means the design believes initialisation finished. §9's bug reaches ACTIVE by committing an unconfirmed configuration, and the link then works, reports healthy, and misinterprets every transfer.

"The scoreboard should follow the DUT's state machine." Then it agrees with the design about every phase the link should not have been in, and its silence is read as evidence that training is verified.

"Recovery resets the verification model." Then a design that wires recovery to a global reset clears its semantic table, the environment clears too, both report zero outstanding, and four operations vanish with no failure ever reported (§12).

"A retry is another transaction." It is another attempt at the same transport object carrying the same semantic obligation. One operation, one object, two attempts, one delivery (§31) — and an environment that counts it as two transactions reports a duplicate that does not exist.

"The same width and rate must come back after a recovery." A degraded recovery is legal and correct. §28's checker fails on it, gets deleted, and takes the only check that the configuration was re-established at all with it.

"One timeout is enough." One timeout says the run hung. Five scoped watchdogs say which layer stopped, and the first to expire is the localisation while the rest are consequences (§49).

"Reaching operational proves the training path was legal." It proves the endpoint. Condition 1 of §5 is about the path, and only a model that tracked the evidence can distinguish a legal bring-up from a shortcut that happened to work.

"Fault injection should combine everything for maximum stress." Then the first divergence has four candidate causes, the failure takes days to reduce, and mechanisms that never fire at all are invisible behind the noise (§45).

"End-to-end packet success proves credit correctness." Packets succeeding proves the link carried them. A leak, a duplicate return and a straggler all keep the counter in range and all let packets through until the receiver happens to be full (§39).

"A clean link after recovery means no semantic work was lost." The link being clean is exactly the state in which lost work is invisible. Only a model that was alive before the fault can tell, which is why §12 is the most consequential single defect an environment can have.

57. Understanding Check

58. Summary and What Comes Next

A link is verified when its control state and its outstanding obligations are both correct across time — and only the second half requires a model that was alive before the fault and is still alive after the recovery.

Four lifecycles, deliberately not collapsed. A link event, a configuration commit, a transport object and a semantic obligation run on four different clocks, and almost every wrong checker in this chapter is one of them read on another's timescale.

Never mirror the design's state machine. A model that reads the register, copies the next-state function, or takes an internal "done" signal as evidence agrees with the design about every phase it should not have been in — and its silence is read as proof that training is verified.

Derive bounds; do not choose them. A fixed watchdog fails a legal slow configuration, gets raised until it catches nothing, and teaches the team that watchdogs are noise.

Compute the expected agreement independently. A checker that calls the design's own negotiation function passes a link running at half its capable width, forever, with no failing signal anywhere.

The environment needs its own reset policy. Clearing the models on the design's reset hides a recovery wired to a global reset — four obligations vanish and nothing ever reports it.

Split semantic invariants from performance variables. A degraded recovery changes the width and changes nothing about what any operation means, and a checker that confuses the two gets the degradation test deleted.

Check conservation continuously, not the counter at the end. Three distinct serious bugs leave the final count correct.

And inject one cause at a time. The first divergence is the environment's most valuable output, and it is destroyed by concurrent injection long before the stress test finds anything.

The link environment now knows which contracts matter and where each one lives. But every check in this chapter reported a consequence — a model disagreed, a count was wrong, an obligation never terminated — and the consequence can be thousands of cycles after the illegal cycle that caused it. The next chapter turns these contracts into temporal properties that fail at the first illegal cycle, name the boundary, and do it without asserting implementation details, going vacuous, or sleeping through the window they exist to check.

• 20.3 — UCIe Assertions — SVA for protocol and ordering rules.

Browse the full path on the UCIe tutorials index.