Protocol Violations

Chapters 21.4 and 21.5 assumed the observed behaviour was legal. This chapter handles the harder claim — that it was not.

1. The One-Sentence Model

A protocol violation is a failed contract, not an unusual waveform. To call something a violation you need six things, and with five of them you have a suspicion.

And the sixth is the one that gets skipped, because it requires proving a negative — which is §29's discipline and most of this chapter's difficulty.

2. What This Chapter Owns

20.3 writes checkers. This chapter is about what to do when one fires — and the answer is not to fix the design.

Four things change once a checker has fired.

The checker becomes a suspect (§8, §35). A rule applied unconditionally that is only valid in one mode fails on legal hardware — and a team that "fixes" the RTL to satisfy it has promoted the checker to a specification (§9).

The monitor becomes a suspect (§22–§25). A held valid sampled every cycle emits three transactions where one occurred, and the scoreboard reports duplicates that never happened.

The revision becomes part of the claim (§32–§34). A behaviour that violated an earlier revision may be explicitly permitted by a later one, and a report that does not name its revision cannot be evaluated.

And the first divergence stops being the first checker error (§30). The trace may have become impossible before any checker was looking — or before the capture started.

3. Sourcing

4. Three Questions, In Order

Before blaming RTL, ask in this order. A "no" at any step ends the investigation there.

Three properties of the ordering.

It is cheapest first. Question 1 is a configuration read and a rule lookup; question 2 is a waveform comparison; question 3 is an RTL investigation that may take a week.

Each step is more likely to be the answer than the next, in most teams' experience — and the ordering is routinely reversed, with the RTL investigated first and the checker's applicability examined only after nothing is found.

And skipping question 1 has a specific, lasting cost (§9): the design is changed to satisfy a checker that was wrong, so the checker's misunderstanding becomes the implementation's behaviour and the real specification is now unmet in a way no test will find.

5. Where the Contract Broke

Four things to read, and only the first is about the design.

The flag is at the dependent event, not at the acknowledgement. The checker fires when it sees a consequence whose precondition has not been observed — which is the correct place to fire and the wrong place to start investigating.

"Not observed" is not "did not happen." The acknowledgement may have occurred and the monitor missed it (§24), or it may have been attributed to a different epoch (§13). Question 2 before question 3.

The checker's record says "epoch E". If the dependent event belongs to epoch E−1 — a straggler from before a recovery — the checker is comparing events from two different agreements (§14), and there is no violation at all.

And the acknowledgement does arrive, later. Which is the shape of a reordering question (§26): were these two events ordered with respect to each other in the first place? If they were not, the trace is legal and the checker asserted an order the architecture never promised.

6. The Requirement Record

// ILLUSTRATIVE, VERIFICATION-ONLY. Tutorial-local. RULE IDENTIFIERS ARE
// PLACEHOLDERS — no official UCIe rule or test identifier appears here (§3).
typedef struct {
  string rule_id;          // YOUR specification's identifier, not an official one
  string source_revision;  // the revision this text was read from — §32
  string source_section;   // where, so a reviewer can check it
  string layer;            // WHO owns it — §15
  string mode;             // the mode/profile it applies under — §9
  string precondition;     // what must be observed to ARM the rule
  string obligation;       // what must then happen, or must not
  string exceptions;       // documented legal exceptions — §1's element 6
  string interpretation;   // if the text is ambiguous, WHICH reading — §34
} protocol_rule_t;

Architecture. One record per rule, holding everything a violation report must cite (§37). The fields are chosen so that an unfilled one is a visible gap rather than an unasked question.

State. A table, loaded from the requirement analysis. Not synthesisable and not intended to be.

Event behaviour. None — it is a static description consulted by the checker's applicability gate (§8).

Contract. source_revision and source_section must be filled from text actually read, not from memory or a summary. A rule whose source cannot be cited cannot be enforced, because a disagreement about it has no way to be resolved.

Failure. Two, and both are common. An empty mode means the rule is applied unconditionally, which is §9. An empty exceptions means element 6 of §1 was never considered — so the first legal exception encountered is reported as a violation.

Debug/DV. The record is what makes a violation report reviewable by someone else. A reviewer with the record can check the claim without re-deriving it, and a reviewer without it can only agree or disagree.

7. Applicability Is Part of the Rule

A checker must evaluate five things before it evaluates the rule.

And a rule that passes all five is armed. One that fails any is not violated — it is not applicable, which is a different and much more common answer.

8. The Applicability Gate

// ILLUSTRATIVE, VERIFICATION-ONLY. The gate is separate from the rule, so a
// checker cannot accidentally apply a conditional rule unconditionally (§9).
function automatic bit rule_applies(protocol_rule_t r, link_context_t ctx);
  if (!revision_in_range(r.source_revision, ctx.implemented_revision)) return 1'b0;
  if (r.requires_feature != "" && !ctx.feature_enabled[r.requires_feature]) return 1'b0;
  if (r.mode  != "" && r.mode  != ctx.active_mode)  return 1'b0;
  if (r.layer != "" && r.layer != ctx.event_layer)  return 1'b0;
  if (!state_in_set(ctx.link_state, r.applicable_states)) return 1'b0;
  return 1'b1;
endfunction
 
// And the coverage that keeps the gate honest — a rule whose gate NEVER opens
// has never been tested, and its silence is not evidence (§28).
covergroup cg_rule_armed(string rule_id) @(posedge clk);
  cp_armed:   coverpoint rule_armed[rule_id] { bins armed = {1'b1}; }
  cp_trigger: coverpoint rule_triggered[rule_id] { bins fired = {1'b1}; }
  x_armed_and_triggered: cross cp_armed, cp_trigger;
endgroup

Architecture. Applicability as a separate, inspectable function rather than as conditions buried in the property's antecedent.

State. None — a pure function of a rule and the link context.

Event behaviour. Evaluated before the rule. A rule that is not applicable produces no verdict at all — neither pass nor fail, which is the important distinction: it is not "vacuously true", it is out of scope.

Contract. ctx must describe the link at the time of the observed event, not at the time of the check. After a mode change, a rule evaluated against the current context but applied to an earlier event is §14's error.

Failure. Folding applicability into the property's antecedent makes an inapplicable rule look vacuously passing, which is indistinguishable in a coverage report from a rule that was armed and satisfied (20.3 §44).

Debug/DV. The covergroup is what makes the gate reviewable: cp_armed never hitting means the rule has never been in scope, and a clean regression that includes it is reporting the absence of a test as a pass (§28).

The gate and the rule combine into a checker whose verdict is three-valued — which is the structural expression of §35's dispositions:

// ILLUSTRATIVE, VERIFICATION-ONLY. A rule checker with a THREE-valued verdict.
// "Not applicable" is not a pass, and the distinction is what makes a coverage
// report meaningful (§28).
typedef enum { VERDICT_NA, VERDICT_PASS, VERDICT_FAIL } verdict_e;
 
typedef struct {
  verdict_e     verdict;
  string        rule_id;
  string        why;             // for NA: WHICH gate closed. for FAIL: the claim.
  longint       trigger_cycle;
  longint       violation_cycle;
  logic [SEM_W-1:0] semantic_id;
} rule_result_t;
 
function automatic rule_result_t check_rule(protocol_rule_t r,
                                            link_context_t ctx,
                                            operation_history_t h);
  rule_result_t res;
  res.rule_id = r.rule_id;
 
  // GATE FIRST — and report WHICH gate closed, so "not applicable" is a
  // reviewable statement rather than silence (§9).
  if (!rule_applies(r, ctx)) begin
    res.verdict = VERDICT_NA;
    res.why     = why_not_applicable(r, ctx);   // "feature X disabled", etc.
    return res;
  end
 
  // ARMED? A rule whose precondition never occurred is NOT a pass (§28).
  if (!precondition_observed(r, h)) begin
    res.verdict = VERDICT_NA;
    res.why     = "precondition never observed in this trace";
    return res;
  end
  res.trigger_cycle = precondition_cycle(r, h);
 
  // EXCEPTIONS BEFORE OBLIGATION — element 6 of §1, and the step most often
  // skipped because it requires enumerating what is LEGAL.
  if (exception_applies(r, h)) begin
    res.verdict = VERDICT_PASS;
    res.why     = "documented exception applies";
    return res;
  end
 
  if (obligation_met(r, h)) begin
    res.verdict = VERDICT_PASS;
  end else begin
    res.verdict         = VERDICT_FAIL;
    res.violation_cycle = obligation_breach_cycle(r, h);
    res.semantic_id     = h.semantic_id;
    res.why             = r.obligation;
  end
  return res;
endfunction

Architecture. Gate, arm, exception, obligation — in that order, with a verdict that distinguishes "not applicable" from "passed".

State. None; a pure function of a rule, a context and an operation's history.

Event behaviour. Evaluated per operation at retirement, or per trigger.

Contract. why_not_applicable must name which gate closed. "Not applicable" without a reason is indistinguishable from a checker that silently does nothing, and a reviewer cannot tell the two apart.

Failure. Collapsing VERDICT_NA into VERDICT_PASS is §28 in its most damaging form: a regression report of ten thousand passes where most rules were never in scope, and nobody can tell which.

Debug/DV. The three-valued verdict maps directly onto §35's dispositions, and the counts are the useful summary: how many rules were applicable, how many were armed, how many passed on an exception. A rule that is applicable in every run and armed in none is the one to write a directed test for.

9. Wrong — the Unconditionally Applied Rule

Worked, and it is the most damaging failure in the chapter.

Five properties.

The design now behaves in a way the real specification does not require — and possibly in a way it forbids in the disabled-feature configuration.

No test will find it, because the checker that would have found it is the one that caused it. The verification environment is self-consistent and wrong.

The cost lands at interoperability, where a partner implementing the actual specification behaves differently — and that debug happens late, across organisations, with no shared trace.

The discriminating observation is question 1 of §4, and it costs a configuration read: was the feature enabled when the checker fired?

And the structural prevention is §8's separate gate, because a gate that must be filled in is a gate somebody has to think about — whereas an antecedent that silently omits a condition looks like a complete property.

10. Configuration Context on Every Event

// ILLUSTRATIVE, VERIFICATION-ONLY. Every observed event carries the context it
// occurred under, so it can never be evaluated against a later configuration
// (§14). This is the record §17 extends.
typedef struct packed {
  logic [EPOCH_W-1:0] link_epoch;    // which link agreement — 19.5 §29
  logic [CFG_W-1:0]   config_epoch;  // which configuration commitment — §27
  logic [MODE_W-1:0]  active_mode;
  logic [CLS_W-1:0]   protocol_class;
  logic [LYR_W-1:0]   layer;         // WHERE it was observed — §15
  logic [REV_W-1:0]   implemented_rev;
} event_context_t;

Architecture. Six context fields, attached to every event at the moment of observation.

State. Carried per event, not held globally.

Event behaviour. Captured at observation, from the context then — which is the entire point. A globally-held "current mode" read at check time describes the mode when the check ran.

Contract. layer must record where the event was observed, not which layer is believed to own the rule. The second is a conclusion; the first is data, and conflating them means the ownership analysis of §15 has been assumed rather than performed.

Failure. Without config_epoch, §14's stale-response case is undiagnosable. Without layer, a physical-layer event and a semantic one are indistinguishable in the log — which is §18's whole distinction.

Debug/DV. The context is what lets a captured trace be re-analysed later under the correct rules. A trace log without context cannot be re-examined, because the analysis tool has no way to know what was true when each event happened.

11. Stale Events and False Violations

Worked. A recovery occurs. The configuration is re-established. A response arrives.

Four properties.

The response may be entirely legal under E − 1's rules, and the mismatch is the checker's — it applied the wrong rule set to a correctly-formed event.

Or the straggler's existence is the bug, if the architecture requires stragglers to be drained or discarded before the new agreement opens. Those are two completely different findings, and the epoch tag is what separates them.

Either way the response is not a protocol violation of E's rules, because E's rules never applied to it — which is §4's question 1 arriving via identity rather than via configuration.

And the discriminating observation is whether the monitor tagged the epoch at observation (§10). If it did, this is a two-second check. If it did not, the trace cannot answer the question at all and must be re-captured — which is the strongest practical argument for §10's context record.

12. Which Layer Owns the Rule

Do not accuse "UCIe." A violation belongs to a layer, and naming the wrong one sends the investigation to a team that cannot find anything.

And the third column is the work. Each row's evidence is a different observation, so "which layer" is not a labelling exercise — it determines what must be captured.

Where a layer's contract is a state machine, its legality is a table rather than a set of hand-written properties:

// ILLUSTRATIVE ARCHITECTURAL CONTRACT (§3) — the states are the published link
// states; the LEGALITY of each edge comes from YOUR revision, not from here.
//
// A transition table makes the checker exhaustive by construction: every pair
// is either explicitly legal or is a violation, with no unconsidered pairs.
localparam bit LEGAL_EDGE [NUM_STATES][NUM_STATES] = '{
  // populated from the requirement analysis (§6), one entry per ordered pair
  default: 1'b0
};
 
// Every transition is checked against the table. An edge that is not in the
// table is a violation — which is the OPPOSITE default from ordering (§16),
// and deliberately so: a state machine's edges are enumerable, an ordering
// relation's are not.
property p_only_legal_transitions;
  @(posedge clk) disable iff (!por_n)
    $changed(link_state_q)
      |-> LEGAL_EDGE[$past(link_state_q)][link_state_q];
endproperty
a_only_legal_transitions: assert property (p_only_legal_transitions);
 
// A transition must have a CAUSE. A state change with no qualifying event is
// a glitch or a decode error, and it is invisible to the table above.
property p_transition_has_cause;
  @(posedge clk) disable iff (!por_n)
    $changed(link_state_q) |-> $past(transition_cause_valid);
endproperty
a_transition_has_cause: assert property (p_transition_has_cause);
 
// And the COVERAGE that keeps the table honest — a legal edge never taken has
// never been tested, and the table asserts nothing about it (§28).
covergroup cg_transitions @(posedge clk iff $changed(link_state_q));
  cp_edge: coverpoint {$past(link_state_q), link_state_q};
endgroup

Architecture. An enumerated edge table, a cause requirement, and edge coverage.

State. A compile-time constant table plus the design's state register.

Event behaviour. Checked on every state change.

Contract. The default is illegal, which is the opposite of §16's ordering default — and the difference is principled: a state machine's edges are finite and enumerable from the specification, whereas an ordering relation's pairs are not, so silence means different things in the two cases.

Failure. Populating the table from the design's state machine rather than from the requirement text is §24's independence failure: the checker then accepts exactly the edges the design produces, including the wrong ones.

Debug/DV. p_transition_has_cause catches what the table cannot — a transition to a legal state for no reason, which a decode error or a glitch produces and which the edge table will happily accept. And an uncovered legal edge is a gap in the test plan, not evidence that the edge works.

13. Physical Events Are Not Semantic Events

The distinction that prevents more false violation reports than any other.

21.3 §21 and 20.1 §19 own this. The contribution here is its use as a defence: a duplicate physical arrival is not a duplicate delivery, and reporting it as a protocol violation confuses the reliability mechanism with the thing it protects.

14. Legal Reordering

A trace where B completes before A is a violation only if A and B were ordered with respect to each other.

And the default assumption must be that ordering is not guaranteed unless the architecture states it — because asserting a global order the design never promised produces a checker that fires on legal, high-performance behaviour and will be "fixed" by serialising the design.

15. Wrong — the Global Order Assertion

VIOLATION REPORT AS WRITTEN:
 
  "Response B arrived before response A. A was issued first.
   The design has reordered responses. This is a protocol violation."
 
WHAT THE REPORT DOES NOT ESTABLISH:
 
  - were A and B in the same ordering domain?
  - was there any dependency between them?
  - does the architecture guarantee completion order at all,
    or only issue order at a boundary?
  - does it guarantee it for THIS traffic class?
 
WITHOUT THESE, THERE IS NO CLAIM.

Three properties.

"A was issued first" establishes nothing. Issue order and completion order are different properties, and most high-performance protocols deliberately decouple them.

The report's cost is the fix. Serialising completions to satisfy it is a throughput regression (21.5 §47's head-of-line consequence) introduced to satisfy a rule that was never required.

And the correct form of the claim requires an explicit dependency (§16) — which frequently does not exist, in which case the trace is simply legal.

Even where an ordering is guaranteed, the observation boundary can invert it. Worked, one operation pair, three monitors watching the same traffic:

Five readings.

All three monitors are working correctly. Nothing was missed, nothing was mis-sampled, and the timestamps are accurate at each point.

The middle row is the transmit path legitimately reordering physical attempts, which §13 establishes says nothing about semantic order — and if the guarantee is on completion order, the third row is the one that matters and the guarantee holds.

So the question is not "were they reordered" but "reordered where, and is the guarantee stated at that boundary?" An ordering promise made at completion is not violated by transmit-order inversion; one made end-to-end would be. The rule's own text names the boundary, which is why layer is a field in §6's requirement record.

A fourth trap sits underneath this: timestamp comparability. Two monitors in different clock domains produce timestamps that cannot be ordered against each other at fine granularity at all — so a 2-cycle inversion between them may be measurement resolution rather than behaviour, and only events observed at one point, or correlated through a common reference, can be ordered confidently.

And the discriminating observation is to re-run the comparison at the boundary the rule names. If that boundary shows the correct order, there is no violation and the report should never have been written — which is §35's "layer" field doing its work before the design is ever opened.

16. The Ordering Dependency Model

// ILLUSTRATIVE, VERIFICATION-ONLY. Only SOURCED dependencies are encoded. An
// edge that is not in the architecture is not in this graph — the default is
// UNORDERED (§14).
typedef struct {
  int unsigned older_id;
  int unsigned newer_id;
  string       basis;      // WHY they are ordered — cite the rule, or it is not an edge
} order_edge_t;
 
order_edge_t deps [$];
 
// Two events are ordered ONLY if a sourced edge exists. Silence means unordered.
function automatic bit must_precede(int unsigned a, int unsigned b);
  foreach (deps[i])
    if (deps[i].older_id == a && deps[i].newer_id == b) return 1'b1;
  return 1'b0;                       // DEFAULT: no ordering requirement
endfunction
 
// So the ordering violation check is narrow by construction.
function automatic bit ordering_violated(int unsigned a, int unsigned b,
                                         longint t_a, longint t_b);
  return must_precede(a, b) && (t_b < t_a);
endfunction

Architecture. An explicit dependency graph where absence of an edge means no requirement, so the checker cannot assert an order that was never promised.

State. A list of sourced edges.

Event behaviour. Consulted when two completions are compared.

Contract. Every edge carries a basis citing the rule that creates it. An edge without a basis is somebody's assumption, and the field exists so that assumption is visible to a reviewer rather than compiled into a checker.

Failure. Defaulting to ordered — the natural instinct — produces §15's report on every legal reordering, and there may be thousands.

Debug/DV. The graph is also a coverage target: an ordering rule whose dependency pair never occurred in the regression has not been tested (20.5 §11), and its silence is not evidence (§28).

Where the legal successors of a state are enumerable, the check becomes an expectation table — and the two structures answer opposite questions:

// ILLUSTRATIVE, VERIFICATION-ONLY. For each operation state, the set of event
// kinds that may legally occur next, and which of them is REQUIRED.
//
// Contrast with §16: the ordering graph is SPARSE and its default is "legal".
// The expectation table is EXHAUSTIVE and its default is "illegal" — because an
// operation's lifecycle states are finite and enumerable from the requirement.
typedef struct {
  bit legal   [obs_kind_e];   // may occur
  bit required[obs_kind_e];   // must eventually occur before retirement
  int deadline;               // -1 = no architectural bound (§29)
} expectation_t;
 
expectation_t expect_from [op_state_e];
 
function automatic rule_result_t check_expectation(op_state_e st,
                                                   observed_event_t e,
                                                   int cycles_in_state);
  rule_result_t r;
  expectation_t x = expect_from[st];
 
  // An event that is not in the legal set is a candidate violation — but the
  // claim is still only a CANDIDATE until §4's questions 1 and 2 are answered.
  if (!x.legal[e.kind]) begin
    r.verdict = VERDICT_FAIL;
    r.why     = $sformatf("event %s is not legal in state %s",
                          e.kind.name(), st.name());
    r.violation_cycle = e.cycle;
    return r;
  end
 
  // A REQUIRED event that has not arrived within an architectural deadline is
  // the missing-event case — and it is only checkable BECAUSE the deadline is
  // architectural rather than invented (§29's form 2 trap).
  if ((x.deadline >= 0) && (cycles_in_state > x.deadline)) begin
    r.verdict = VERDICT_FAIL;
    r.why     = $sformatf("required event overdue in state %s", st.name());
    return r;
  end
 
  r.verdict = VERDICT_PASS;
  return r;
endfunction
 
// The coverage that keeps the table honest: every LEGAL successor should be
// observed at least once, or the table asserts something never tested (§28).
covergroup cg_expectation @(posedge clk iff obs_valid);
  cp_state: coverpoint op_state_q;
  cp_kind:  coverpoint obs_event.kind;
  x_state_kind: cross cp_state, cp_kind;
endgroup

Architecture. A per-state legal set, a required set, and an architectural deadline — exhaustive by construction, so an unconsidered event kind is a compile-time gap rather than a silent pass.

State. A table indexed by operation state.

Event behaviour. Consulted per observed event, plus a deadline check on the required set.

Contract. The default is illegal, which is the opposite of §16's default — and the difference is principled. A lifecycle's states and their successors are finite and enumerable from the requirement text; an ordering relation's pairs are not, so silence means "unconstrained" there and "forbidden" here. Applying either default to the other structure is a bug: an exhaustive default on ordering produces §15's false report, and a sparse default on a lifecycle lets any event pass in any state.

Failure. Populating the table from the design's observed behaviour rather than from the requirement is §24 again — the table then legalises exactly what the design does, including whatever is wrong.

Debug/DV. The deadline field is where §29's discipline lives: -1 is honest and means the required event cannot be checked for lateness at all, while a positive value must be an architectural quantity. A table full of invented deadlines is a checker that will be weakened once per firing until it cannot fail.

17. Trace Normalisation

Raw waveforms cannot be compared. Normalise to semantic events first.

And the normalised form is what makes two runs comparable at all — a good run and a bad run have different cycle timing and the same event sequence, so aligning by event rather than by cycle is what produces §30's first divergence.

Normalised events go into a bounded ring, because a violation is usually noticed after the event that caused it:

// ILLUSTRATIVE. The event-history ring — bounded, with the two features that
// make a bounded history honest: a WRAPPED flag and a FREEZE (§31).
localparam int RING_DEPTH = 256;
 
observed_event_t  ring_q [RING_DEPTH];
logic [$clog2(RING_DEPTH)-1:0] ring_wr_q;
logic             ring_wrapped_q;    // the earliest entry is NOT the first event
logic             ring_frozen_q;     // stop capturing, so the cause survives
 
always_ff @(posedge clk or negedge por_n) begin
  if (!por_n) begin
    ring_wr_q      <= '0;
    ring_wrapped_q <= 1'b0;
    ring_frozen_q  <= 1'b0;
  end else begin
    // FREEZE on the first checker failure, so the ring holds the events BEFORE
    // it rather than the events after (14.5 §8's first-fault principle).
    if (violation_flag_fire && !ring_frozen_q)
      ring_frozen_q <= 1'b1;
 
    if (obs_valid && !ring_frozen_q) begin
      ring_q[ring_wr_q] <= obs_event;
      if (ring_wr_q == ($clog2(RING_DEPTH))'(RING_DEPTH-1))
        ring_wrapped_q <= 1'b1;                 // sticky
      ring_wr_q <= ring_wr_q + 1'b1;
    end
  end
end

Architecture. A fixed-depth ring of normalised events, frozen at the first violation flag.

State. RING_DEPTH records, a write pointer, and two flags.

Event behaviour. One entry per observed event. The freeze is on the first flag, not the last — so the ring holds the run-up to the violation rather than the aftermath, which is the opposite of what an unfrozen ring gives you.

Contract. ring_wrapped_q must be sticky and reported alongside the dump. A wrapped ring's earliest record looks like the beginning of history and is not (§31).

Failure. Two, and they are opposites. Without the freeze, the checker fires and the ring keeps filling with post-violation events until the cause has been overwritten — the debug equivalent of clearing the fault register before reading it. Without the wrapped flag, an analyst reasons about a "causeless" first event that was simply the oldest surviving one.

Debug/DV. A frozen, flagged ring is what makes §40's trace comparison possible on real captures. And its depth is the honest limit of any negative-evidence claim (§29): a rule requiring that something never happened cannot be proven from a window that holds 256 events.

And the ring's events are correlated into per-operation histories, which is what makes §36's four hypotheses separable:

// ILLUSTRATIVE, VERIFICATION-ONLY. One operation's full event history,
// assembled by identity — so §36's four hypotheses are separable.
typedef struct {
  logic [SEM_W-1:0] semantic_id;
  logic [GEN_W-1:0] generation;
  bit               retired;          // §29's bounded lifetime
  longint           retired_cycle;
  observed_event_t  events [$];       // in observation order
} operation_history_t;
 
operation_history_t hist [logic [SEM_W-1:0]];   // keyed by semantic id
 
function automatic void correlate(observed_event_t e);
  if (!hist.exists(e.semantic_id)) begin
    if (e.kind != OBS_ACCEPT)
      // A history that starts midstream: either the monitor missed the accept
      // (§21), or the capture began late (§31). NOT proof of an invented event.
      report_note(NOTE_HISTORY_STARTS_MIDSTREAM, e.semantic_id, e.kind.name());
    hist[e.semantic_id] = '{ e.semantic_id, e.generation, 1'b0, -1, '{} };
  end
  // A generation MISMATCH is the discriminator that separates a late response
  // to a RETIRED operation from one to the live operation that reused the id.
  else if (hist[e.semantic_id].generation != e.generation) begin
    if (hist[e.semantic_id].retired)
      report_error(ERR_RESPONSE_TO_RETIRED_GENERATION, e.semantic_id,
                   $sformatf("event gen %0d, retired gen %0d at cycle %0d",
                             e.generation, hist[e.semantic_id].generation,
                             hist[e.semantic_id].retired_cycle));
    else
      report_error(ERR_GENERATION_REUSED_WHILE_LIVE, e.semantic_id, "");
  end
  hist[e.semantic_id].events.push_back(e);
  if (e.kind == OBS_COMPLETE) begin
    hist[e.semantic_id].retired       = 1'b1;
    hist[e.semantic_id].retired_cycle = e.cycle;
  end
endfunction

Architecture. One history per operation identity, so a claim about an operation is backed by its whole observed sequence rather than by one event.

State. One entry per operation; retired entries are kept until the epoch closes, deliberately, because §36's discriminators need the retired record to still exist.

Event behaviour. Every normalised event is offered. The generation comparison is the discriminating step, and it produces two different errors — a response to a retired generation, and a generation reused while still live.

Contract. Retirement must be an observed event, not a timeout. A history retired by a timer manufactures §36's hypothesis A for every operation that was merely slow.

Failure. Deleting the history at retirement makes a late response look causeless (§31) rather than late — and destroys the only evidence that distinguishes hypothesis A from hypothesis C. Reporting the midstream start as an error rather than a note is the mirror mistake: it is far more often a truncated capture than an invented event.

Debug/DV. The two distinct errors are the point. ERR_RESPONSE_TO_RETIRED_GENERATION names a candidate identity-reuse violation; ERR_GENERATION_REUSED_WHILE_LIVE names a monitor or design tagging bug — and a single "unexpected response" error would have conflated them.

18. The Observed-Event Record

// ILLUSTRATIVE, DEBUG/VERIFICATION-ONLY. NOT a UCIe wire format (§3). The
// identity fields are what separate physical from semantic (§13).
typedef enum logic [EVENT_W-1:0] {
  OBS_ACCEPT   = 'd0,   // the protocol boundary accepted an operation
  OBS_ALLOCATE = 'd1,   // a resource was committed to it
  OBS_SEND     = 'd2,   // a PHYSICAL attempt left
  OBS_RECEIVE  = 'd3,   // a PHYSICAL attempt arrived
  OBS_DELIVER  = 'd4,   // a SEMANTIC delivery to the protocol layer
  OBS_RESPONSE = 'd5,
  OBS_COMPLETE = 'd6,
  OBS_RECOVERY = 'd7,   // an epoch boundary
  OBS_CFG_COMMIT='d8    // a configuration commitment — §27
} obs_kind_e;
 
typedef struct packed {
  logic [TIME_W-1:0] cycle;
  obs_kind_e         kind;
  logic [SEM_W-1:0]  semantic_id;  // the OPERATION — one per lifetime
  logic [GEN_W-1:0]  generation;   // so a REUSED id is distinguishable — §21
  logic [OBJ_W-1:0]  object_id;    // the transported unit
  logic [ATT_W-1:0]  attempt_id;   // WHICH attempt — 1, 2, 3 ... — §19
  event_context_t    ctx;          // §10
} observed_event_t;

Architecture. One record shape for every observation, with four separate identity fields because four different identities exist and conflating any two produces a false violation.

State. A ring of these is the trace (§31).

Event behaviour. Emitted by a monitor at each boundary. OBS_RECEIVE and OBS_DELIVER are deliberately distinct kinds — the physical arrival and the semantic delivery — which is §13 encoded in the vocabulary itself.

Contract. semantic_id is stable across attempts; attempt_id distinguishes them. generation increments when a semantic_id is reused, so a response to a retired operation is distinguishable from a response to the live one that reused its identity (20.4 §21) — which is §39's whole case.

Failure. Merging semantic_id and object_id makes a multi-object operation look like several operations. Omitting attempt_id makes every retransmission a duplicate (§19). Omitting generation makes §39 unresolvable.

Debug/DV. The record is the unit of comparison for §30's alignment and the input to every checker below — and it is deliberately independent of the design's own signalling, so a design that mislabels an attempt does not thereby mislabel the trace.

19. Legal Retry Mistaken for a Duplicate

Worked. The most common false violation in a link with retry.

Three properties.

Two receives and one delivery is exactly what a working retry mechanism produces. The Adapter's reliability layer did its job (14.2).

Reporting it as a duplicate delivery is a category error — confusing the mechanism with what it protects (§13) — and the "fix" would disable the retry.

The violation would be two OBS_DELIVER events for one semantic_id and generation (§20), which is a different observation entirely and requires the semantic monitor rather than the physical one.

20. Case — Duplicate Semantic Delivery

When it is a violation, and the check that must come first.

Two properties.

Steps 2–4 are §4's question 2, and they are cheap. Step 5 is a serious finding — a delivery guarantee is exactly what the reliability layer exists to provide.

And "delivered twice" must be checked against the architecture's definition of delivery, which may be a handshake at a specific interface rather than the first appearance of data — so the monitor's placement is part of the claim (§10's layer field).

21. A Bad Monitor Manufactures Violations

Five monitor defects, each producing a characteristic false violation.

And every one of them is cheaper to check than the RTL, which is why §4's ordering puts the monitor before the design.

The cheapest validation of all is to reconcile two monitors that should agree:

// ILLUSTRATIVE, VERIFICATION-ONLY. Two independent monitors observing the same
// logical stream at different points must agree on COUNT and IDENTITY SET.
// Disagreement localises the defect to one of them BEFORE the design is touched.
typedef struct {
  int unsigned count;
  int unsigned id_xor;                 // order-independent set signature
  int unsigned first_id, last_id;
} monitor_digest_t;
 
monitor_digest_t digest [string];       // keyed by monitor name
 
function automatic void monitor_observe(string mon_name, observed_event_t e);
  digest[mon_name].count++;
  digest[mon_name].id_xor ^= e.semantic_id;   // order-independent
  if (digest[mon_name].count == 1) digest[mon_name].first_id = e.semantic_id;
  digest[mon_name].last_id = e.semantic_id;
endfunction
 
// Reconciled at quiescence, where any in-flight difference has drained.
function automatic void reconcile_monitors(string a, string b);
  if (digest[a].count != digest[b].count)
    report_error(ERR_MONITOR_COUNT_MISMATCH, 0,
      $sformatf("%s saw %0d, %s saw %0d — one monitor is wrong, not the DUT",
                a, digest[a].count, b, digest[b].count));
  // Equal counts with different signatures means the same NUMBER of different
  // events — a correlation or identity-tagging bug, not a lost event.
  else if (digest[a].id_xor != digest[b].id_xor)
    report_error(ERR_MONITOR_IDENTITY_MISMATCH, 0,
      $sformatf("%s and %s agree on count but not on WHICH events", a, b));
endfunction

Architecture. A tiny digest per monitor — count, an order-independent identity signature, and the first and last identity seen.

State. Four integers per monitor.

Event behaviour. Updated per observation; reconciled at quiescence, where transport differences have drained (21.4 §10's in-flight argument applies unchanged).

Contract. The two monitors must observe the same logical stream, and any legitimate transformation between them — filtering, aggregation, a retry collapsing several attempts into one delivery — must be modelled, or the mismatch is expected rather than diagnostic.

Failure. The XOR signature collides (21.4 §26): two compensating identity errors XOR to zero. A matching signature is therefore weaker evidence than a mismatching one, and reporting it as proof of agreement overstates it.

Debug/DV. The two error kinds are different findings. A count mismatch means one monitor missed or invented events — §23's held-valid bug shows up here as an inflated count at the unqualified monitor. A signature mismatch with equal counts means they saw the same number of different things, which is a tagging or correlation defect. Neither is a design bug, and both are found in seconds.

22. Race-Free Sampling

// ILLUSTRATIVE, VERIFICATION-ONLY. A clocking block removes the active-region
// race that makes an event appear a cycle early or late (§21 row 1).
clocking mon_cb @(posedge clk);
  default input #1step;         // sample in the PREPONED region
  input valid, ready, payload, sem_id, attempt_id, epoch;
endclocking
 
// A transaction is emitted ONLY on a completed handshake — once, on the cycle
// the transfer occurs, regardless of how long valid was held (§25).
task automatic monitor_loop();
  forever begin
    @(mon_cb);
    if (mon_cb.valid && mon_cb.ready) begin
      observed_event_t e;
      e.cycle       = cycle_count;
      e.kind        = OBS_ACCEPT;
      e.semantic_id = mon_cb.sem_id;
      e.attempt_id  = mon_cb.attempt_id;
      e.ctx         = capture_context();     // §10, at OBSERVATION time
      emit(e);
    end
  end
endtask

Architecture. Preponed sampling plus handshake qualification — the two defects that produce most false violations, closed together.

State. None beyond the loop.

Event behaviour. One event per completed handshake. Not per cycle valid is high, which is §25.

Contract. The context is captured at observation, so a later mode change cannot retroactively reinterpret the event (§10).

Failure. Sampling without the clocking block puts the monitor in a race with the design's own non-blocking updates: the event may be recorded a cycle early or late, which breaks every ordering comparison — and produces violations that move when unrelated code changes, which is the signature.

Debug/DV. A monitor validated against the waveform is a precondition for any violation claim, not a nicety. Validate it once, deliberately, and record that you did — because the claim's credibility rests on it.

23. Flagship — the Held-Valid Monitor Bug

Worked. The single most common false-violation mechanism.

Five properties.

The scoreboard reports two duplicate requests for an operation that was issued once.

The design is entirely correct — holding valid until ready is the normal handshake discipline.

The false rate scales with backpressure, so it appears under load and vanishes in a lightly-loaded directed test. Which reads as a load-dependent design bug — the most alarming possible signature, and completely wrong.

The discriminating observation is one waveform. Look at the three "duplicate" events and note that ready was low for two of them. Two minutes, versus a week of RTL investigation.

And the structural fix is §22's valid && ready qualification, which is one line — whose absence has cost more engineering time across the industry than most real protocol bugs.

24. Checker Independence

A checker must not call the design's own function to determine legality.

20.4 §17's independence rule, applied to legality rather than to data. The checker's model must be derived from the requirement text (§6), not from the implementation — which is more work, and it is the only version that can find anything.

25. Checker Mutation

A checker that has never fired is not known to work. Test it in both directions.

Three properties.

Both directions are necessary. A checker that fires on everything passes the first test and is worthless. One that fires on nothing passes the second.

The third row is specific to this chapter and is the one usually omitted: a checker that still evaluates when its feature is disabled is §9 waiting to happen, and the mutation finds it before a legal configuration does.

And the mutation must be removed and the removal verified (20.2 §54) — an injected fault left in a regression is a worse problem than the one it was testing for.

// ILLUSTRATIVE, VERIFICATION-ONLY. A mutation harness that runs all three
// directions and FAILS THE BUILD on any unexpected result — so a blind or
// over-firing checker cannot reach a regression.
typedef enum { MUT_VIOLATE, MUT_LEGAL_EXCEPTION, MUT_FEATURE_OFF } mutation_e;
 
typedef struct {
  string     rule_id;
  mutation_e mutation;
  verdict_e  expected;      // VIOLATE->FAIL, EXCEPTION->PASS, FEATURE_OFF->NA
} mutation_case_t;
 
function automatic verdict_e expected_for(mutation_e m);
  case (m)
    MUT_VIOLATE:          return VERDICT_FAIL;
    MUT_LEGAL_EXCEPTION:  return VERDICT_PASS;   // must stay QUIET — §9's risk
    MUT_FEATURE_OFF:      return VERDICT_NA;     // the gate must close — §8
  endcase
endfunction
 
task automatic run_mutation_suite(protocol_rule_t rules[$]);
  int failures = 0;
  foreach (rules[i]) begin
    foreach (mutation_e m) begin
      rule_result_t r;
      apply_mutation(rules[i], m);              // construct the stimulus
      r = check_rule(rules[i], current_ctx(), current_history());
      if (r.verdict != expected_for(m)) begin
        failures++;
        // The DIAGNOSIS depends on which direction failed.
        case (m)
          MUT_VIOLATE:         report_error(ERR_CHECKER_BLIND,     0, rules[i].rule_id);
          MUT_LEGAL_EXCEPTION: report_error(ERR_CHECKER_OVERFIRES, 0, rules[i].rule_id);
          MUT_FEATURE_OFF:     report_error(ERR_GATE_MISSING,      0, rules[i].rule_id);
        endcase
      end
      remove_mutation(rules[i], m);
      // Verify the removal — an injected fault left behind is worse than the
      // bug it was testing for (20.2 §54).
      assert (!mutation_active(rules[i]))
        else $fatal(1, "mutation not removed for %s", rules[i].rule_id);
    end
  end
  if (failures != 0) $fatal(1, "%0d checker mutation failures", failures);
endtask

Architecture. Three mutations per rule, each with a different expected verdict, and a build failure on any mismatch.

State. None persistent — each case applies and removes its own mutation.

Event behaviour. Run as a suite, before the regression that relies on the checkers.

Contract. The removal is asserted, not assumed. And each direction's failure produces a distinct error, because they mean different things: blind, over-firing, and missing its gate are three separate defects with three separate fixes.

Failure. Running only MUT_VIOLATE — the usual practice — leaves §9's over-firing checker undetected, which is the more damaging of the two because it changes the design.

Debug/DV. A checker that has passed all three directions is one whose verdict can be cited in §35's report. One that has passed none has never been shown to distinguish legal from illegal at all, and its silence in a regression means nothing.

26. Configuration Commitment

// ILLUSTRATIVE ARCHITECTURAL CONTRACT. Requested may change at any time; ACTIVE
// changes only at a commitment, and only under quiesce (19.6 §31, 21.1 §29).
// The config_epoch (§10) increments at the commitment.
property p_active_cfg_stable_without_commit;
  @(posedge clk) disable iff (!por_n)
    !cfg_commit_fire |=> $stable(active_cfg_q);
endproperty
a_active_cfg_stable: assert property (p_active_cfg_stable_without_commit);
 
property p_commit_requires_quiesce;
  @(posedge clk) disable iff (!por_n)
    cfg_commit_fire |-> (outstanding_count_q == '0);
endproperty
a_commit_requires_quiesce: assert property (p_commit_requires_quiesce);
 
property p_epoch_advances_on_commit;
  @(posedge clk) disable iff (!por_n)
    cfg_commit_fire |=> (config_epoch_q == $past(config_epoch_q) + 1);
endproperty
a_epoch_advances: assert property (p_epoch_advances_on_commit);
 
// And requested may move freely — asserting stability on it is a FALSE rule.

Architecture. Three properties covering the requested-versus-active contract, with the epoch as the observable that ties events to configurations.

State. None beyond the design's.

Event behaviour. p_active_cfg_stable fires at the cycle the active configuration mutates without a commitment — which is §27's first divergence, exactly.

Contract. outstanding_count_q must be every outstanding obligation, not one class's. A quiesce that drains one queue and not another commits while work is still in flight under the old configuration.

Failure. Asserting stability on the requested configuration is a false rule that fires on legal software behaviour — 21.1 §29's distinction, inverted, and it is §9 in miniature.

Debug/DV. The epoch property is what makes §11's stale-event analysis possible at all: without a monotonically advancing epoch, an event cannot be attributed to a configuration, and every cross-recovery question becomes unanswerable.

27. Case — Illegal Configuration Transition

Four readings.

The first divergence is the active mutation, not the requested change. The requested change at 4,000 is legal and is a distractor.

Seventeen obligations were in flight under the old configuration, and they will complete under rules that no longer apply — which is §11's stale-event problem created by the design rather than by the monitor.

The unchanged epoch is what makes it undetectable downstream. Every event after 4,002 is tagged with the old config_epoch, so no checker can tell that the configuration underneath them changed — the instrument that would have caught it was disabled by the same bug.

And this is 19.6 §31's requested-versus-active contract violated at the atomic-commit step — a design that changes active state outside a commitment has no way to keep any of its observers in agreement.

28. Vacuity

A checker can pass because its trigger never occurred.

And a regression report showing every protocol assertion passing is compatible with none of them ever being exercised (20.3 §44). Every important rule is paired with a cover — which is §8's covergroup, and it is why the gate and the coverage are written together.

29. Negative Evidence

Many rules require proving something did not happen, and a short trace cannot.

Three properties.

"Never" needs a retirement point. An operation is either explicitly retired — completion, timeout, recovery — or the property must be bounded by an architectural window. Without one, the checker can only say "not yet."

An unbounded never is unfalsifiable within the trace, so it can only fail, never pass — and a property that cannot pass provides no positive information at all.

And this is why the object lifecycle model of 20.4 §21 is a prerequisite for most of this chapter's cases: the retirement point is what turns "never" into a checkable claim.

// ILLUSTRATIVE ARCHITECTURAL CONTRACT (§3). "No second delivery" written THREE
// ways — only the third is both checkable and honest.
 
// FORM 1 — unbounded. Can only ever fail; it never reports a pass, so it
// contributes no positive information and a clean run proves nothing (§29).
property p_no_second_delivery_UNBOUNDED(int id);
  @(posedge clk) disable iff (!por_n)
    (deliver_fire && (deliver_sem_id == id)) |=> always !(deliver_fire && (deliver_sem_id == id));
endproperty
 
// FORM 2 — bounded by an arbitrary window. Checkable, and WRONG: a second
// delivery one cycle after the window is missed entirely, and the window is a
// guess rather than an architectural quantity.
property p_no_second_delivery_ARBITRARY(int id);
  @(posedge clk) disable iff (!por_n)
    (deliver_fire && (deliver_sem_id == id))
      |=> !(deliver_fire && (deliver_sem_id == id)) [*1000];
endproperty
 
// FORM 3 — bounded by RETIREMENT, which is an OBSERVED architectural event.
// The claim becomes: no second delivery while the operation is live, and the
// generation guard handles the identity being legitimately reused afterwards.
property p_no_second_delivery_LIVE(int id);
  @(posedge clk) disable iff (!por_n)
    (deliver_fire && (deliver_sem_id == id))
      |=> (!(deliver_fire && (deliver_sem_id == id) &&
             (deliver_gen == $past(deliver_gen))))
          throughout (1'b1 [*1:$] ##0 (retire_fire && (retire_sem_id == id)));
endproperty
a_no_second_delivery: assert property (p_no_second_delivery_LIVE(TEST_ID));
 
// And the retirement must ITSELF be guaranteed to occur, or form 3 is form 1
// wearing a bound. This is the property that makes the bound legitimate.
property p_operation_eventually_retires(int id);
  @(posedge clk) disable iff (!por_n)
    (accept_fire && (accept_sem_id == id))
      |-> ##[1:MAX_OPERATION_LIFETIME] (retire_fire && (retire_sem_id == id));
endproperty

Architecture. Three formulations of one rule, and the pairing that makes the third legitimate.

State. The design's own live-operation state, plus the generation.

Event behaviour. Form 3 is bounded by an observed retirement, so it produces a real pass when the operation retires cleanly.

Contract. Form 3 is only sound if retirement is guaranteed, which is why p_operation_eventually_retires is written alongside it. Without that pairing, an operation that never retires makes form 3 vacuously true forever — the bound is present and never reached, which is form 1 with extra syntax.

Failure. Form 1 in a regression looks rigorous and reports nothing. Form 2's window will be raised the first time a slow-but-legal case fires it, and each raise weakens it further until it cannot fail.

Debug/DV. The generation guard in form 3 is what allows the identity to be legitimately reused after retirement without the property firing — which is §19's legal-retry problem in the identity domain, and omitting it produces a false violation on every reuse.

30. First Divergence Versus First Detection

The first checker failure is what the tool noticed. The first divergence is the first event for which no legal continuation of the prior trace can account. They are frequently different, and the second is the one that matters.

Three properties.

"No legal continuation can account for it" is a stronger claim than "a checker fired." It is a statement about the trace, independent of what tooling was watching.

Establishing it requires the requirement set, not just the checker set — which is why §6's records exist. A gap in the checkers is not a gap in the rules.

And it is what makes a report reviewable by a partner (§37): a shared trace with a named first divergence can be evaluated by someone with a different verification environment, whereas "our checker fired" cannot.

31. Trace Truncation

Worked, and it is the reason first-fault capture exists.

Four properties.

The first observed violation is not the first divergence (§30), and every investigation that starts inside the window will be looking at a consequence.

The signature of truncation is a causeless event — a response with no request, a completion with no allocation, a release with no allocation. 21.4 §30's "consumer without producer" check finds exactly this, and its correct interpretation is frequently "the capture started too late", not "an event was invented."

The instruments that survive truncation are the sticky ones — 14.5 §8's first-fault capture, the first-duplicate register (21.4 §27), and a wrapped flag on the event ring (21.1 §12).

And a ring without a wrapped flag is worse than no ring, because its earliest record looks like the beginning of history and is not.

Truncation removes the start of a trace. A dropped record removes something from the middle, and that is worse — because the trace still looks complete.

The instrument is one field and one check:

// ILLUSTRATIVE. A monotonic per-monitor sequence ID stamped on every emitted
// record. A GAP proves the trace is incomplete — WITHOUT it, a dropped record
// is indistinguishable from an event that never occurred (§29's negative
// evidence, which is exactly what a missing prerequisite claim rests on).
typedef struct packed {
  logic [SEQ_W-1:0] seq;         // monotonic, per monitor, never reset in-run
  logic [MON_W-1:0] monitor_id;  // WHICH monitor — gaps are per-source
  observed_event_t  ev;
} traced_record_t;
 
// Emit side: the sequence increments per RECORD, not per cycle, so a gap means
// a record was lost rather than that nothing happened.
always_ff @(posedge clk or negedge por_n) begin
  if      (!por_n)   seq_q <= '0;
  else if (obs_valid) seq_q <= seq_q + SEQ_W'(1);
end
 
// Consume side: verification-only integrity check, per monitor.
int unsigned expect_seq [int unsigned];
int unsigned dropped_total;
 
function automatic void ingest(traced_record_t r);
  if (expect_seq.exists(r.monitor_id) && (r.seq != expect_seq[r.monitor_id])) begin
    // A GAP. The trace is incomplete. Every "missing prerequisite" claim in the
    // affected span is now UNPROVABLE — not disproved, unprovable (§29).
    int unsigned gap = r.seq - expect_seq[r.monitor_id];
    dropped_total += gap;
    report_error(ERR_TRACE_RECORDS_DROPPED, r.monitor_id,
      $sformatf("%0d record(s) lost before seq %0d — negative-evidence claims in this span are void",
                gap, r.seq));
  end
  expect_seq[r.monitor_id] = r.seq + 1;
endfunction

Architecture. A monotonic sequence per monitor, checked for gaps at ingest.

State. One counter per monitor on the emit side; one expected value per monitor on the consume side.

Sampled timing. The sequence increments per emitted record, not per clock — so an idle monitor leaves no gap, and a lost record leaves exactly one.

Contract. The sequence must not reset mid-run, including across a recovery. A sequence that restarts at an epoch boundary makes every epoch transition look like a drop, and the check gets disabled.

Failure. Without it, a dropped record produces a trace where a prerequisite is genuinely absent — and §29's negative-evidence claims are built on absence. "No accept was observed for this response" becomes a violation report when it should have been "the trace is incomplete."

Debug/DV. The disposition is the important part: a detected gap does not disprove the violation, it makes it unprovable from this trace — which is a fifth outcome that §35's template must be able to express, and the honest response is to re-capture rather than to argue.

And the worked case is short. A response arrives at cycle 8,400 for an operation with no observed accept. Hypothesis: the design responded to something it was never asked. The sequence check shows a gap of 3 records at the protocol monitor around cycle 5,100 — the monitor's FIFO overflowed under burst load. The accept happened; the record did not survive. The design is clear, the instrumentation is undersized, and the discriminating observation cost one field.

32. Revision Scope

Every violation claim names its revision. A behaviour that violated an earlier revision may be permitted by a later one, and a rule may have been extended, narrowed, or made conditional.

And this is not hypothetical for UCIe. Official Consortium material records that UCIe 1.0 supported Streaming Protocols only in Raw Mode, and 1.1 permitted them on FDI (§3). A checker encoding the 1.0 behaviour, run against a 1.1 design, reports a violation of a rule that no longer exists — which is §33, from a real published change.

33. Wrong — the Remembered Rule

Three properties.

The absence of a citation is the diagnostic. A claim with source_revision and source_section (§6) can be checked in minutes; one without can only be argued about.

Memory is systematically biased toward the revision you learned first, which is usually the older one — so this failure mode is more common in experienced engineers, not less.

And the fix is procedural rather than technical: the violation report template (§37) has a mandatory revision field, and a report with it empty is returned rather than debated.

34. Interpretation Ambiguity

When two teams read the same text differently, do not silently encode one reading in a checker.

Three properties.

Silently choosing a reading turns a documented ambiguity into an undocumented assumption, which surfaces at interoperability with a partner who chose the other one.

Recording both readings costs one paragraph and makes the eventual clarification a lookup rather than a re-derivation.

And the honest disposition for a genuine ambiguity is "escalated for clarification", not "violation" — which is §38's disposition field, and it is a legitimate outcome of an investigation.

35. The Violation Report Template

The chapter's centerpiece. Every field, and why an empty one blocks the claim.

And the dispositions are five, not two.

Three of the five clear the design entirely, which is the ratio this chapter exists to make visible.

The "legal exceptions checked" field needs a list to check against. Ten behaviours that look illegal and are not — the negative-case catalogue:

Three readings.

Seven of the ten are resolved by a field rather than by an investigation — attempt, epoch, generation, ordering edge, handshake, wrapped flag, applicability. Which is the practical argument for §18's record: each field costs bits and removes a category of false claim.

Two rows are the same symptom with different causes — a response to a dead operation is either a stale epoch or a reused identity — and they are a monitor problem and a design problem respectively. Without both fields they are indistinguishable.

And the last row inverts the direction. Nine rows are false positives; the tenth is a false negative, where nothing fired and nothing was checked. A regression's silence is the hardest thing on this list to notice, because it looks exactly like success.

36. Case — a Response to a Dead Identity

Four properties.

Four hypotheses, four cheap discriminators, and three of them exonerate the design.

Discriminator 1 requires generation (§18). Without it, A and C are indistinguishable — and they are a design bug and a monitor/epoch bug respectively.

Discriminator 4 is the one teams forget: a scoreboard that flushes outstanding state at a recovery manufactures this symptom for every legitimately-outstanding operation, and the flush is usually added deliberately to stop unrelated noise.

And only after all four survive is this a violation — of an identity-reuse rule that must then be cited with its revision (§32).

37. Case — Credit Consume at Zero

Four hypotheses, and the checker is among them.

And the third and fourth are the interesting ones, because both mean the design is correct and the checker is not.

38. The Same-Cycle Checker Bug

// WRONG — checks the credit value BEFORE the same-cycle return is applied.
// Fires on every legal simultaneous return-and-consume (19.5 §14).
a_no_consume_at_zero_WRONG: assert property (
  @(posedge clk) disable iff (!por_n)
    consume_fire |-> (credit_q != '0)
);
 
// CORRECT — evaluate against the NEXT-STATE credit, which accounts for a
// return arriving in the same cycle. The arithmetic must match the design's
// documented same-cycle semantics — and if the architecture does NOT permit a
// same-cycle return to cover a consume, the WRONG form above is right and this
// one is wrong. The rule decides, not the convenience.
logic signed [CRD_W:0] credit_next;
assign credit_next = $signed({1'b0, credit_q})
                   + $signed({1'b0, return_amount_this_cycle})
                   - $signed({1'b0, consume_amount_this_cycle});
 
a_credit_never_negative: assert property (
  @(posedge clk) disable iff (!por_n)
    (credit_next >= 0)
);

Architecture. A next-state formulation, because the legality of a consume depends on events in the same cycle.

State. None — a combinational next-state expression.

Event behaviour. Evaluated every cycle against the post-update value.

Contract. This is the chapter's sharpest illustration of §4's question 1. Whether a same-cycle return may cover a consume is an architectural rule, and the two properties above are correct under opposite rules. Choosing the second because it stops the assertion firing is exactly the error of §9 — the checker being adjusted to match the design rather than the specification.

Failure. The first form under an architecture that permits same-cycle coverage fires constantly on legal hardware and is deleted, taking real over-allocation detection with it. The second form under an architecture that forbids it misses a genuine violation.

Debug/DV. Whichever is correct, a_credit_never_negative in signed arithmetic is the invariant that survives both — because a negative next-state credit is impossible under either rule (19.5 §14).

39. Case — a Corrupted Object Delivered

// MANDATORY. ILLUSTRATIVE ARCHITECTURAL CONTRACT (§3) — this chapter states no
// UCIe integrity rule, and no CRC behaviour beyond what §3 records.
//
// An object whose integrity check FAILED must not be delivered semantically.
property p_no_delivery_of_failed_object;
  @(posedge clk) disable iff (!por_n)
    (integrity_fail_fire && (fail_obj_id == check_obj_id))
      |-> !deliver_fire;
endproperty
a_no_delivery_of_failed: assert property (p_no_delivery_of_failed_object);
 
// And the EFFECT form, written against a different observable (20.3 §27) —
// every delivered object had a PASSING integrity result recorded for it.
property p_delivery_implies_integrity_pass;
  @(posedge clk) disable iff (!por_n)
    deliver_fire |-> integrity_passed_q[deliver_obj_id];
endproperty
a_delivery_implies_pass: assert property (p_delivery_implies_integrity_pass);

Architecture. A cause form and an effect form, deliberately written against different observables.

State. A per-object integrity result.

Event behaviour. The first fires at the delivery of a failed object; the second fires at the delivery of an object with no recorded pass — including one that was never checked at all, which the first form cannot detect.

Contract. integrity_passed_q must be cleared at allocation, or a stale pass from a previous object at the same index satisfies the property — a shared-index defect that makes the checker agree with the bug.

Failure. With only the cause form, an object whose integrity check never ran is delivered and nothing fires: the antecedent requires a failure, and there was no result at all.

Debug/DV. This is the clearest safety violation in the chapter and the one case where the design is almost certainly at fault — but §4's questions still apply: is deliver_fire the architecture's delivery point, or an internal signal the monitor mistook for one (§10's layer field)?

40. Comparing Two Traces

// ILLUSTRATIVE, VERIFICATION-ONLY. Align by EVENT, not by cycle (§17), and
// return the first index where the sequences diverge.
function automatic int trace_first_divergence(observed_event_t good[$],
                                              observed_event_t bad[$]);
  int n = (good.size() < bad.size()) ? good.size() : bad.size();
  for (int i = 0; i < n; i++) begin
    // Compare the SEMANTIC content, not the timing. Two correct runs differ in
    // cycle counts and must not be reported as divergent.
    if ((good[i].kind        != bad[i].kind) ||
        (good[i].semantic_id != bad[i].semantic_id) ||
        (good[i].generation  != bad[i].generation) ||
        (good[i].ctx.link_epoch != bad[i].ctx.link_epoch))
      return i;
  end
  // A prefix match with different lengths is a divergence at the shorter end —
  // usually a MISSING event, which is the harder case (§29).
  return (good.size() != bad.size()) ? n : -1;
endfunction

Architecture. Event-aligned comparison returning the first differing index.

State. None.

Event behaviour. Run offline on two captured traces.

Contract. Timing is deliberately excluded from the comparison. Two correct runs differ in cycle counts; including cycle in the comparison makes every pair divergent at index 0 and the tool is useless.

Failure. Comparing attempt_id would report every legal retry difference as a divergence (§19) — which is why it is absent from the comparison even though it is present in the record.

Debug/DV. The returned index is a candidate first divergence, not a proven one (§30): the good run is a baseline, not a specification, and both runs may be legal. It narrows where to look; §35's template is what turns it into a claim.

41. Debug Checklist

Thirty-six questions, in §4's order.

Did the rule apply? (1–10).

1. Which rule, by identifier (§6)?
2. Which revision was the text read from (§32)?
3. Which section — can a reviewer find it (§6)?
4. Is the rule in the revision this design implements (§33)?
5. Is the feature it governs enabled?
6. Is the link in the mode it applies to?
7. Is the link in an applicable state?
8. Does it apply to this protocol class?
9. Is applicability gated separately, or buried in the antecedent (§8)?
10. Are there documented exceptions, and were they checked (§1)?

Did the monitor observe correctly? (11–20). 11. Was sampling race-free (§22)? 12. Was a transaction emitted per handshake or per valid cycle (§23)? 13. Is semantic_id distinct from object_id (§18)? 14. Is attempt_id recorded — is this a legal retry (§19)? 15. Is generation recorded — could the identity have been reused (§36)? 16. Is the epoch recorded, at observation time (§10)? 17. Is the config epoch recorded (§11)? 18. Which layer was the observation taken at (§10)? 19. Was the monitor validated against the waveform? 20. Is the checker reading a design-internal signal rather than the boundary (§24)?

Is it a physical or semantic claim? (21–24). 21. Is this a duplicate arrival or a duplicate delivery (§13)? 22. Is this a reordered attempt or a reordered completion (§14)? 23. Is there a sourced ordering edge between the two events (§16)? 24. Is the ordering guaranteed end to end, and for this class (§14)?

Is the checker itself correct? (25–29). 25. Has the checker been mutation-tested in both directions (§25)? 26. Does it evaluate next-state where same-cycle events matter (§38)? 27. Does it share any function with the design (§24)? 28. Is it paired with coverage, or could it be vacuous (§28)? 29. Does the rule require negative evidence, and is the lifetime bounded (§29)?

Where and when did it diverge? (30–33). 30. Is the first checker failure the first divergence (§30)? 31. Does the trace start before the root cause (§31)? 32. Is there a causeless event — a response with no request (§31)? 33. Does the event ring have a wrapped flag (§31)?

Disposition (34–36). 34. Is the text ambiguous, and is the chosen interpretation recorded (§34)? 35. Which of the five dispositions applies (§35)? 36. Is the finding reproducible — seed, configuration, stimulus (§35)?

42. Common Misconceptions

"The checker fired, so the design is wrong." §4: three questions come before that, and two of them exonerate the design more often than not.

"The UCIe specification requires this." §32 and §33: without a revision and a section, that sentence is a recollection. This chapter never writes it (§3).

"An unusual waveform is a violation." §1: a violation is a failed contract, and it needs six elements.

"B completed before A, so ordering was violated." §15: not unless a sourced dependency exists between them.

"Two arrivals means duplicate delivery." §19: two physical attempts and one semantic delivery is a working retry mechanism.

"The monitor reports what happened." §23: a monitor without handshake qualification reports three transactions where one occurred, and worse under load.

"Applying a rule everywhere is the safe default." §9: it is the most damaging option, because the design gets changed to satisfy it and the checker becomes the specification.

"A checker that never fires is a good checker." §28: it may never have been armed, and its silence is not evidence.

"The first checker failure is the root cause." §30: checker latency, missing checkers and truncated traces all separate detection from divergence.

"A response with no request proves the design invented one." §31: it more often proves the capture started too late.

"Vacuous passes are harmless." §28: a regression of vacuous passes is indistinguishable from a regression of real ones.

"Ambiguity should be resolved in the checker." §34: that converts a documented disagreement into an undocumented assumption, which surfaces at interoperability.

"A stale response is illegal." §11: it may be perfectly legal under the epoch it belongs to — and the checker applying current rules to it is the error.

"The scoreboard is independent because it is separate code." §24: independence is about the source of the legality model, not about file boundaries.

"Simulation passing means the design is compliant." 20.7: simulation establishes agreement with your model of the rules.

43. Understanding Check

44. Summary

The five dispositions, and what each requires to reach.

Six things that carry beyond UCIe.

Applicability is part of the rule, and gating it separately from the property is what stops a conditional rule being applied unconditionally (§8) — the failure that turns a checker into a specification.

The monitor is checked before the design, because it is cheaper and because a held valid counted per cycle has cost more engineering time than most real protocol bugs (§23).

Physical and semantic events are different things. A duplicate arrival is a retry working; a duplicate delivery is a violation (§19).

Silence is not evidence of ordering. An edge that is not sourced does not exist, and asserting a global order costs throughput to satisfy a rule that was never required (§16).

The first divergence is not the first detection (§30), and a causeless event usually means the capture started too late rather than that an event was invented (§31).

And a violation claim is a document, not an opinion (§35): rule, revision, section, layer, configuration, trigger, obligation, observation, exceptions checked, monitor validation, first divergence, identity, reproduction, checker status, disposition. Any field empty is a claim that cannot be evaluated — and three of the five dispositions clear the design entirely.