UCIe Assertions

Chapter 20.2 built an environment that detects a lost obligation, a stranded credit or an illegal bring-up — and every one of those detections reports a consequence. The illegal cycle happened earlier, sometimes thousands of cycles earlier, in a block the report does not name. This chapter writes the properties that fail at that cycle instead.

1. The One-Sentence Model

An assertion is an executable statement about time, and its value is decided by five things that can each be independently wrong: whether its trigger means the event you think it means, whether its consequent describes a real contract rather than a current implementation, whether its reset and disable scoping leaves it awake during the window it exists to check, whether it survives overlapping transactions, and — for liveness — whether its assumptions are written down and justified.

A property can be syntactically perfect, bound correctly, reported as passing, and check nothing. Four of the five failures above produce exactly that, and §§57–60 are them.

2. What This Chapter Owns

20.1 said which contracts matter. 20.2 said where each one lives. This chapter is how each one is written, and the writing is where most of them go wrong:

Triggers that mean the wrong event (§13–§14). valid instead of an accept is the single most common defect in a protocol checker, and it is the same misconception that produces a credit leak in RTL.

Scoping that sleeps through the bug (§39–§41) — the flagship anti-pattern. A property about what survives a recovery, disabled during recovery, is asleep at exactly the cycle the state is cleared.

Properties that outgrow the language (§16–§20). One assertion cannot naturally track sixty-four overlapping transactions, and the point where local variables stop working is a real boundary that must be recognised rather than fought.

Bounds and conservation (§24–§28), because a range check on a counter passes while every event feeding it is wrong.

Four wrong properties that pass (§57–§60), each one green in a regression report.

And an inventory (§68) with the columns that make a property reviewable: its trigger, its assumptions, whether it is portable, and which bug it catches.

3. Sourcing

4. An Assertion Is a Statement About Time

Three things distinguish an assertion from a comment, and only the third is about SystemVerilog.

It names an event. Not a condition — an event, at a specific cycle, that the contract says means something. The whole of §14 is that naming this correctly is harder than it looks and is where most checkers fail.

It states a consequence over time. Immediately, next cycle, within a window, eventually. The temporal operator is a claim about the contract, and choosing |-> where the contract says |=> is a real error with a real failure mode (§9).

And it is evaluated by a tool with specific sampling semantics — values sampled in the preponed region, so an assertion sees the value before this cycle's non-blocking updates. That is the one piece of SystemVerilog mechanics this chapter re-teaches (§7), because a property that looks one cycle wrong on a waveform is usually a sampling misunderstanding rather than a design bug.

The review question for any property: "what event, what promise, over what window, under what assumptions?" A property whose author cannot answer all four in one sentence is a property nobody can review.

5. Four Classes, Two Kinds

Organise properties by what they constrain, then by what kind of statement they are. The two-dimensional grid is what makes a plan auditable — a cell with no entries is a gap, and a cell with thirty entries is probably over-invested.

Four properties of this grid.

Safety is violated by a finite trace; liveness only by an infinite one. That single fact drives everything about how they are written, tested and reported (§47).

Liveness always needs assumptions and safety never does. A safety property with an assume attached is usually a safety property that was weakened until it passed.

The interface row is the cheapest and least likely to hold a serious bug. It catches malformed stimulus and integration errors — valuable, and not where the expensive failures are.

And the reliability row's safety half cannot be checked from one observation point. "At most once" relates a transmit event to a far-end delivery. 20.1 §20's argument: an environment with a single observation point has assumed that row rather than checked it.

6. Property Anatomy

property p_example;                       // 1. the name — it appears in failures
  @(posedge clk)                          // 2. the clocking event
  disable iff (!por_n)                    // 3. the disable condition — §42
    (valid && ready)                      // 4. the antecedent (the trigger)
      |=>                                 // 5. the implication operator — §8
    (owned && $stable(obj_id));           // 6. the consequent (the promise)
endproperty
a_example: assert property (p_example);   // 7. the assertion, with a label
c_example: cover property (@(posedge clk) (valid && ready));   // 8. §49

Each of the eight lines can be independently wrong, and the failure modes differ.

Lines 3, 7 and 8 are the ones that produce a green report on an unchecked design. They are the reason this chapter spends as much space on scoping and vacuity as on temporal logic.

7. Sampling, in One Paragraph

SVA samples in the preponed region — the values a property sees at a clock edge are the values before that edge's non-blocking updates. So a property evaluated at edge n observes the design's state as of edge n−1 plus this cycle's combinational settling.

Two practical consequences, and they explain most "the waveform disagrees with the assertion" reports.

A registered signal updated by <= at edge n is not visible to a property at edge n. It is visible at edge n+1. A property that checks a register's new value in the same cycle as the event that sets it will always see the old value — which is why |=> exists and why §8 matters.

And a combinational signal is visible at the same edge, so mixing a combinational antecedent with a registered consequent under |-> is the classic off-by-one. The rule of thumb: if the consequent is a _q, you almost certainly want |=>.

8. |-> Versus |=>

// OVERLAPPING — the consequent is checked in the SAME cycle as the antecedent.
// Correct when the promise is combinational or is about the same cycle's values.
property p_accept_implies_permitted;
  @(posedge clk) disable iff (!por_n)
    obj_accept |-> link_permits_traffic;      // both combinational this cycle
endproperty
 
// NON-OVERLAPPING — the consequent is checked in the NEXT cycle.
// Correct when the promise is about state the accept CREATES.
property p_accept_creates_ownership;
  @(posedge clk) disable iff (!por_n)
    obj_accept |=> owned_q[$past(obj_slot)];  // the register updated by the accept
endproperty

The rule, stated as a question about the contract:

Does the promise describe something that must already be true at the moment of the event, or something the event brings about? The first is |->; the second is |=>.

Two UCIe-shaped examples where the answer is not obvious.

"An accepted object is owned by someone." 19.3 §11's property. Ownership is created by the acceptance, so the ownership register updates on that edge and is visible the next cycle: |=>. Writing |-> fails on correct RTL at every single accept.

"An accepted object was admitted with a credit available." The credit must have been available before the accept — it is a precondition, not a consequence — so the check is |-> on the pre-decrement value. Writing |=> checks the post-decrement value and is a different, weaker claim.

9. Wrong Overlap — The Off-By-One

// WRONG — the consequent is a register the antecedent SETS.
property p_accept_creates_ownership_bad;
  @(posedge clk) disable iff (!por_n)
    obj_accept |-> owned_q[obj_slot];     // owned_q updates on THIS edge
endproperty

What happens. owned_q[obj_slot] is written by a non-blocking assignment at the same edge obj_accept is true. The property samples the pre-update value, which is 0. The property fails at every accept.

Four properties, and the fourth is the reason this is a section rather than a footnote.

It fails on correct hardware, every time. Not intermittently — 100% of accepts.

Because it fails so reliably, it gets "fixed" fast, and the fix that gets applied is frequently to weaken the property rather than to change the operator: obj_accept |-> (owned_q[obj_slot] || obj_accept) is tautological and passes.

The reverse error is the dangerous one. A property that should be |-> written as |=> does not fail — it just checks a later, weaker condition. Nothing reports it, and the property looks like it is working. The credit-precondition example in §8 is exactly this: |=> on the post-decrement value passes on a design that consumed a credit it did not have.

And it is invisible in review. Both operators are one character apart and both read naturally in English. The only defence is the §8 question, asked deliberately for every property whose consequent names a _q.

10. $past and the Reset Boundary

// ILLUSTRATIVE. $past reaches back one cycle — and at the first cycle after
// reset there is no previous cycle, so its value is undefined or X-dependent.
property p_count_increments_bad;
  @(posedge clk) disable iff (!rst_n)
    push_fire |=> (count_q == $past(count_q) + 1);
endproperty

The hazard. On the very first evaluation after reset release, $past(count_q) reaches into the reset period. Depending on the tool and the reset modelling it returns X, the reset value, or an unknown — and a comparison against X is not false, it is unknown, so the property may pass, fail, or behave differently between simulators.

Three defences, in order of preference.

Widen the disable so the property is not evaluated until history exists:

// RIGHT — an explicit history-valid bit, one per clock domain.
logic hist_valid_q;
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) hist_valid_q <= 1'b0;
  else        hist_valid_q <= 1'b1;
 
property p_count_increments;
  @(posedge clk) disable iff (!rst_n || !hist_valid_q)
    push_fire |=> (count_q == $past(count_q) + 1);
endproperty

Use $past with an explicit gating expression, which is clearer where only some cycles have valid history: $past(count_q, 1, hist_valid_q).

Or restructure so no $past is needed at all. 19.4 §9's derived occupancy is the design-side version of this argument: a property that compares two live signals has no history problem, and where the design can be written so the invariant is instantaneous, the assertion gets simpler and stronger at once.

Note the cost of the first defence. hist_valid_q must be per clock domain (8.1 §6), and a single global one in a multi-domain design gates the wrong properties on the wrong domain's reset.

11. $stable and the Bundle

// ILLUSTRATIVE — a generic ready/valid contract, not a UCIe rule (§3).
// The consequent covers the WHOLE bundle, not just the data.
property p_bundle_stable_under_stall;
  @(posedge clk) disable iff (!por_n)
    (valid && !ready)
      |=> valid
       && $stable(payload.data)
       && $stable(payload.strb)
       && $stable(payload.meta)
       && $stable(payload.cls)
       && $stable(payload.first)
       && $stable(payload.last)
       && $stable(payload.poison);
endproperty
a_bundle_stable_under_stall: assert property (p_bundle_stable_under_stall);

Three parts, all load-bearing.

valid stays high. A producer that withdraws an offer before it was accepted has retracted it. Whether that is legal is a contract question, and the property is where the answer is recorded.

Every field is covered. §12 is what happens when it is not.

And |=> is correct here by §8's question: the stability requirement is about the next cycle onward, given that this cycle was a stall.

A note on writing it compactly. Where the payload is a packed struct, $stable(payload) covers all fields in one term and is preferable — but only if every field of that struct is contractually stable. If the struct contains a field the producer is allowed to change under stall, the compact form is over-strong and will fire on legal stimulus, which is 20.1 §15's failure. Enumerate when the contract is mixed; use the struct when it is uniform.

12. Wrong Stability — Data Only

// WRONG — checks the data and nothing else.
property p_data_stable_bad;
  @(posedge clk) disable iff (!por_n)
    (valid && !ready) |=> (valid && $stable(payload.data));
endproperty

Worked. A producer's next-item logic runs one cycle ahead. During a stall it updates the metadata registers — class, identity, framing bits — while holding the data.

The consumer accepts the transfer. It gets item A's data with item B's class and identity.

Five properties, and this is why the section exists.

The data is correct. Every data-integrity check passes. Every CRC passes. The bytes that crossed the link are exactly the bytes that were meant to cross.

The routing is wrong. The object is delivered to the wrong resource class, matched against the wrong outstanding request, or counted against the wrong credit pool. 19.4 §16's payload-and-metadata failure, arriving through the assertion rather than the buffer.

The symptom is maximally confusing. A correct payload delivered under a wrong identity looks like a scoreboard bug, a monitor bug, or a far-end bug. The one thing it does not look like is a stability violation on the transmit boundary.

The narrow property passed the whole time, and it appears in the report as a stability check, so a reviewer scanning for "do we check stability?" gets a yes.

And the fix is free. Adding six terms to an existing property costs nothing and closes the entire class.

13. The Acceptance Event

The single most consequential decision in a protocol checker: what event means "this happened".

// ILLUSTRATIVE. For a boundary with a ready/valid contract. This is a GENERIC
// interface contract — no claim that any UCIe interface uses these names (§3).
assign accept = valid && ready;

Everything hangs off it, and 20.1 §12 said so at the level of monitors. Here it is at the level of properties:

Two rules.

The acceptance event is defined per boundary, not globally. A credit-gated boundary, a message-passing boundary and a ready/valid boundary have three different acceptance events. A checker that assumes one shape across a whole design has assumed a uniformity the design does not have.

And "accept" is not "arrive". 19.3 §9's admission reserves resources before accepting, precisely because accepting is a commitment rather than a movement.

14. Wrong Trigger — valid Instead of Accept

The most common defect in a protocol checker, and it is the same misconception that produces a credit leak in RTL (19.5 §18).

// WRONG — a level, used as if it were an event.
property p_valid_consumes_credit;
  @(posedge clk) disable iff (!por_n)
    valid |-> (credit_q != '0);
endproperty

Worked. The producer holds valid for eight stalled cycles with credit at zero — which is exactly correct behaviour: the producer is offering work and flow control is refusing it, which is what flow control is for.

The property fires eight times on correct hardware.

Four properties.

The direction of the error matters. This one is over-strong and fires falsely. The mirror version — a scoreboard that counts on valid — is under-checked and silent, and 20.1 §31 is that case.

The response is to weaken it, and the weakening usually goes too far: valid && ready |-> (credit_q != '0) is correct, but the fix frequently applied is valid |-> (credit_q != '0) || !ready, which is the same property with a hole in it and passes on a design that transfers with zero credit if ready is somehow high.

The same shape recurs with grants. 19.5 §19: a grant is an event, not a level, so the usual review question returns the wrong answer — but a grant is a statement about arbitration, not about a transfer, and a property keyed on it becomes hostage to an arbiter change.

And the correct property is about the pre-decrement value. accept |-> (credit_q != '0) reads the credit as it was before this cycle's consumption, which is precisely what "you may not consume what you do not have" means.

15. The Assertion Trip, Cycle by Cycle

Four readings, and the third is the sampling lesson.

The property arms twice. Once at cycle 1 and once at cycle 2, because the antecedent is true in both. Two independent attempts, and one of them passes while the other fails — which is what "overlapping attempts" means concretely (§16).

The failure is reported at cycle 3, not cycle 2. The antecedent was at cycle 2; |=> moves the check to cycle 3. A debugger who looks at cycle 3 for the cause finds only the symptom — the cause is the arming condition one cycle earlier, and §64's methodology starts there deliberately.

Sampling explains why payload at cycle 3 reads B2. The change was driven by logic that updated it at edge 3, so the property at edge 3 sees... the preponed value, which is the value settled before that edge's non-blocking updates. If payload is combinational off a register that changed at edge 3, the property sees the new value; if payload is itself a register written at edge 3, the property sees A7 and the failure appears at cycle 4 instead. This is the single most common source of "the assertion fires one cycle late" confusion, and the resolution is always to determine whether the signal is combinational or registered.

And cycle 4 is why this matters at all. The transfer completes carrying B2 with M1 — a correct payload under the wrong metadata, §12's failure, delivered as valid data.

16. Overlapping Attempts

A property with a trigger that can be true on consecutive cycles starts a new attempt each time. Those attempts are independent, they overlap in time, and each one succeeds or fails on its own.

That is usually what you want — §15's waveform is exactly it — and it becomes a problem the moment the property needs to remember something about its transaction.

// This works: the property is memoryless. Every attempt is self-contained.
property p_stable_under_stall;
  @(posedge clk) disable iff (!por_n)
    (valid && !ready) |=> (valid && $stable(payload));
endproperty
 
// This is where it starts to hurt: the property needs to remember WHICH id
// it armed on, so it can check the response that comes back for THAT id.
property p_response_matches_request_naive;
  @(posedge clk) disable iff (!por_n)
    req_accept |=> ##[1:$] (rsp_valid && (rsp_id == req_id));
    //                                            ^^^^^^
    // WRONG: req_id is read at the RESPONSE cycle, not remembered from the
    // request cycle. With several requests in flight it compares against
    // whatever id happens to be on the request bus now.
endproperty

The fix inside SVA is a local variable:

// RIGHT — a local variable captures the id at the arming cycle, per attempt.
property p_response_matches_request(int unsigned bound);
  int unsigned id;
  @(posedge clk) disable iff (!por_n)
    (req_accept, id = req_id)
      |=> ##[1:bound] (rsp_valid && (rsp_id == id));
endproperty

Each attempt gets its own copy of id. Sixty-four overlapping requests produce sixty-four live attempts, each remembering its own identity.

17. Where Local Variables Stop Working

Local variables solve the remember my transaction problem and do not solve three others. Recognising the boundary is more useful than fighting it.

The three "no" rows share one shape: they are questions about the set of live transactions, and an SVA attempt is deliberately isolated from every other attempt.

When the question is about a set, use checker state — a bitmap, a counter, an associative array — maintained in ordinary procedural code and then asserted over. That is not a defeat; it is the right tool. §18 is the discipline that keeps it honest.

And the fourth row matters more than it looks. A trigger that fires far more often than intended — because it is a level (§14), or because the design has a pathological case — creates one live attempt per cycle, and a simulator tracking hundreds of thousands of live attempts slows to a crawl. A regression that suddenly runs ten times slower after an assertion is added is usually this, and the fix is the trigger, not the tool.

18. Checker State, and When It Is Legitimate

// ILLUSTRATIVE. Checker-owned state, derived ONLY from observable events.
// This is legitimate. §19 is the version that is not.
logic [NUM_IDS-1:0] chk_id_live;
 
always_ff @(posedge clk or negedge por_n) begin
  if (!por_n) begin
    chk_id_live <= '0;
  end else begin
    // Set on the OBSERVED allocation event at the boundary.
    if (alloc_accept) chk_id_live[alloc_id] <= 1'b1;
    // Clear on the OBSERVED retirement event at the boundary.
    if (retire_fire)  chk_id_live[retire_id] <= 1'b0;
  end
end

The rule that makes checker state acceptable:

Every bit of checker state is derived from events observable at a contract boundary, and from nothing else. If the checker needs a design-internal signal to maintain its state, it has become part of the implementation and its agreement with the design proves nothing.

Three notes.

The reset scope is por_n, not the design's narrow reset. 20.2 §12's argument: checker state that is cleared by a recovery cannot detect a recovery that clears design state it should not.

Simultaneous set and clear of the same index must be examined. Whether an allocation and a retirement of the same id can coincide is an architecture question; if they can, the ordering here is a decision, and an assertion should state which one the checker believes.

And the checker state itself needs verification (20.1 §49). Drive an allocation and a retirement in the same cycle, drive a retirement with no allocation, and confirm the bitmap does what the contract says.

19. Wrong Checker State — Reading the Design's Bitmap

// WRONG — the checker's notion of "live" comes from the design's own register.
property p_no_double_allocation_bad;
  @(posedge clk) disable iff (!por_n)
    alloc_accept |-> !dut.id_allocated_q[alloc_id];
endproperty

Why this proves nothing. The property asserts that the design does not allocate an id its own free-list says is allocated. That is a statement about the design's internal consistency, not about the contract.

Worked, with a real bug shape. The design's free-list is updated one cycle late relative to the allocation. Two back-to-back allocations of the same id both see id_allocated_q as 0 — the design allocates the same id twice, and the property passes both times, because it read the same stale register the allocation logic read.

Three consequences.

The bug is the register's timing, and the property inherited it. Any check built on a signal is blind to that signal's own defects.

The checker-state version catches it. §18's chk_id_live is set on the observed allocation event, so the second allocation sees it as 1 and the property fires. The checker's update rule is different from the design's, which is exactly why it can disagree.

And this is 19.6 §13's rule in a third location. A legality function, a scoreboard trigger, and now a checker's state — all three are cases of the verification artefact borrowing the design's answer to the question it is supposed to be asking.

20. Identity Uniqueness

// MANDATORY. ILLUSTRATIVE ARCHITECTURAL CONTRACT (§3) — an identity is not
// reused while its previous holder is live. Uses checker state (§18).
property p_no_reuse_while_live;
  @(posedge clk) disable iff (!por_n)
    alloc_accept |-> !chk_id_live[alloc_id];
endproperty
a_no_reuse_while_live: assert property (p_no_reuse_while_live);
 
// MANDATORY — a retirement refers to something that was allocated.
property p_retire_implies_live;
  @(posedge clk) disable iff (!por_n)
    retire_fire |-> chk_id_live[retire_id];
endproperty
a_retire_implies_live: assert property (p_retire_implies_live);
 
// MANDATORY — the count of live identities never exceeds the table's capacity.
// A cross-attempt aggregate: exactly the §17 case that needs checker state.
property p_live_count_bounded;
  @(posedge clk) disable iff (!por_n)
    ($countones(chk_id_live) <= NUM_IDS);
endproperty
a_live_count_bounded: assert property (p_live_count_bounded);

Three properties, three distinct failures.

Reuse-while-live catches 19.2 §21's aliasing — a delayed response for a retired operation arriving after its identity was reallocated.

Retire-implies-live catches a spurious retirement, which is the mirror bug and is usually a decode error. It also catches a double retirement, because the second one finds the bit already clear.

And the bounded count is the aggregate that no per-attempt property can express (§17).

On generation counters. 19.2 §22's generation narrows the aliasing window enormously and is the correct design mechanism. The checker should still use its own bitmap, because the generation is finite and wraps, while the checker's state does not have to be.

21. A Response Belongs to a Live Request

// MANDATORY. ILLUSTRATIVE ARCHITECTURAL CONTRACT (§3). The single highest-value
// ordering property in the set — its failure delivers wrong data as correct.
property p_response_to_live_request;
  @(posedge clk) disable iff (!por_n)
    rsp_accept |-> chk_id_live[rsp_id];
endproperty
a_response_to_live_request: assert property (p_response_to_live_request);
 
// MANDATORY — a request receives at most one response. Per-id, with the
// checker's own liveness as the guard against the id having been reused.
property p_at_most_one_response(int unsigned id);
  @(posedge clk) disable iff (!por_n)
    (rsp_accept && (rsp_id == id))
      |=> !(rsp_accept && (rsp_id == id)) until_with (alloc_accept && (alloc_id == id));
endproperty
 
// MANDATORY — the response's shape matches what its request expects. Catches a
// correctly-matched response carrying the wrong kind of payload.
property p_response_kind_matches;
  @(posedge clk) disable iff (!por_n)
    rsp_accept |-> (rsp_kind == chk_expected_kind[rsp_id])
                && (rsp_cls  == chk_class[rsp_id]);
endproperty

Why the third property is not redundant. The first says the identity is live; the second says it is answered once. Neither says the answer is the right kind of answer. A completion where data was expected, or a partial response for an operation requiring a whole one, satisfies both and is a different bug in a different block.

Why chk_expected_kind is checker state rather than a design lookup. §19's rule — a checker that reads the design's outstanding-request table asks the design what it expected, which is precisely the record that a mis-decode corrupted.

22. Ordering Domains

The most common way to make a checker over-constrain a legal design.

Never assert a global issue order. Assert ordering within a defined domain, and treat every pair outside a domain as unordered.

// ILLUSTRATIVE ARCHITECTURAL CONTRACT (§3). The checker knows, per pair,
// which of three relationships holds — and "unknown" is treated as unordered.
typedef enum { ORD_A_BEFORE_B, ORD_UNORDERED, ORD_UNKNOWN } ord_rel_e;
 
function automatic ord_rel_e ordering_relation(int unsigned a, int unsigned b);
  // Same ordering group AND the architecture requires precedence.
  if (chk_ord_group[a] != chk_ord_group[b]) return ORD_UNORDERED;
  if (chk_requires_precedence(a, b))        return ORD_A_BEFORE_B;
  return ORD_UNORDERED;
endfunction
 
// MANDATORY — required precedence within a group is honoured.
property p_precedence_honoured(int unsigned a, int unsigned b);
  @(posedge clk) disable iff (!por_n)
    ((ordering_relation(a, b) == ORD_A_BEFORE_B)
      && rsp_accept && (rsp_id == b))
        |-> chk_completed[a];
endproperty

Three rules.

ORD_UNKNOWN is treated as unordered, and is recorded as a gap. 20.1 §40's discipline: assuming an ordering that does not exist produces false failures; assuming none where one exists misses real bugs. Only recording the uncertainty is honest, and only the recorded gap can be closed later.

Unordered pairs must be exercised in both orders. If A-then-B and B-then-A are both legal and only one ever occurs, the design was verified for one of them. That is a coverage requirement (§67), not an assertion one.

And where UCIe carries PCIe or CXL natively, the ordering rules that apply are those protocols' rules — extensive, subtle, and specified elsewhere. Take them from the relevant protocol specification and encode them in chk_requires_precedence, which is exactly the function the abstraction exists to hold. This chapter asserts no UCIe ordering rule (§3).

23. Wrong Ordering — Global Issue Order

// WRONG — asserts that responses return in request order, globally.
property p_responses_in_order_bad;
  @(posedge clk) disable iff (!por_n)
    (req_accept, id = req_id)
      |=> ##[1:$] (rsp_accept && (rsp_id == id) && (chk_outstanding_older(id) == 0));
endproperty

Worked. Two requests to different destinations, in different resource classes, with different latencies. The second completes first, legally. The property fires.

Four properties, and the fourth is the cost that outlives the bug.

The property has become a design restriction. It says the design must not reorder — which is a stronger requirement than the architecture makes, and if anyone acts on it, the design gets a reorder buffer it did not need, costing area and latency to satisfy a checker.

The response is to weaken it, and the weakening usually removes ordering checking entirely rather than scoping it to a domain. The real ordering requirement, which does exist within a group, is then unchecked.

It hides the bug it was aimed at. Somewhere in the design there is a pair that must be ordered. Once the global property is deleted, nothing checks that pair, and the failure ships.

And it interacts with retry. A retried operation completes later than one issued after it — which is legal, expected, and indistinguishable from a reordering violation to a global-order property. So the property additionally fires on every injected fault, which is where it gets disabled.

24. Credit — The Property Set

Seven properties, and the reason to list them together is that six of them can pass while the seventh fails.

Property 7 is the one that matters and §25 is why. 19.5 §53 established it at the design level; here it is the assertion-level consequence: every silent credit bug keeps the counter inside its legal range, so a plan containing only rows 1 and 3 has verified the bounds and none of the accounting.

25. Wrong Credit Assertion — The Bound Alone

// WRONG-BY-INSUFFICIENCY — necessary, and nowhere near sufficient.
property p_credit_bounded_only;
  @(posedge clk) disable iff (!por_n)
    (credit_q <= CAPACITY);
endproperty

Five distinct bugs that pass this property forever:

Three properties of this failure.

The bound is genuinely necessary. It catches the unsigned wrap of 19.5 §15, where a two-unit deficit becomes a maximum-value grant. It should be written, and it should not be the only one.

"The counter never underflowed" is the reasoning that produces this plan, and it is the misconception §71 names. Range is the weakest property in the set.

And the fix is conservation, which requires checker state (§18) — the model's advertised, consumed and returned counts, maintained from observed events, compared against the design's register. That is a §17 aggregate, so it cannot be a pure temporal property, which is why credit checking is the clearest case in the chapter for checker-state-plus-assertion rather than SVA alone.

26. Credit Consume

// MANDATORY. GENERIC FLOW-CONTROL CONTRACT — no UCIe credit rule is claimed (§3).
 
// 3 — the flow-control guarantee, on the PRE-decrement value (§8).
property p_no_consume_without_credit;
  @(posedge clk) disable iff (!por_n)
    (consume_units != '0) |-> (consume_units <= credit_q);
endproperty
a_no_consume_without_credit: assert property (p_no_consume_without_credit);
 
// 4 — consume only on a qualifying event. Two terms, both necessary.
property p_consume_on_commit_only;
  @(posedge clk) disable iff (!por_n)
    (consume_units != '0) |-> (obj_commit_fire && requires_new_remote_allocation);
endproperty
a_consume_on_commit_only: assert property (p_consume_on_commit_only);
 
// 4b — the named form of §14's failure. Redundant with the above, and worth
// writing because it names the bug in its own failure message.
property p_no_consume_while_stalled;
  @(posedge clk) disable iff (!por_n)
    (valid && !ready) |-> (consume_units == '0);
endproperty
a_no_consume_while_stalled: assert property (p_no_consume_while_stalled);
 
// 2 — the pre-truncation range check, which fires in the SAME cycle as a wrap.
property p_next_credit_in_range;
  @(posedge clk) disable iff (!por_n)
    !advert_apply |-> (!credit_underflow && !credit_overflow);
endproperty
a_next_credit_in_range: assert property (p_next_credit_in_range);

On writing 4b even though 4 implies it. It names the failure. When 4b fires the message says "a stalled cycle consumed credit"; when 4 fires it says "the commit qualification is wrong". The first message gets the bug fixed in an afternoon, and that difference is worth one redundant property.

On property 2 versus property 1. Property 1 is evaluated on the truncated register, so a wrap landing inside the legal range is invisible to it. Property 2 is evaluated on the wider signed intermediate before truncation (19.5 §14), which is the only place an out-of-range result exists long enough to be seen.

27. Credit Return and the Duplicate Guard

// MANDATORY — 5. A return implies the storage is actually free this cycle.
property p_return_implies_released;
  @(posedge clk) disable iff (!por_n)
    credit_return_fire |-> (entry_release_fire && !entry_valid_q[pop_idx]);
endproperty
a_return_implies_released: assert property (p_return_implies_released);
 
// MANDATORY — the EFFECT form, written against a different observable so a
// shared misconception cannot satisfy it (20.1 §23). An entry whose credit was
// returned is not read again before it is reallocated.
property p_no_read_after_return(int idx);
  @(posedge clk) disable iff (!por_n)
    (credit_return_fire && (pop_idx == idx))
      |=> !(entry_read_fire && (read_idx == idx))
          until (entry_alloc_fire && (alloc_idx == idx));
endproperty
 
// MANDATORY — one return per released unit. Uses the checker's own per-entry
// guard, NOT the design's credit_returned bit (§19).
property p_return_once_per_entry(int idx);
  @(posedge clk) disable iff (!por_n)
    (credit_return_fire && (pop_idx == idx)) |-> !chk_returned[idx];
endproperty

The second property is the one worth understanding. The first can be written by a verification engineer who read the RTL and copied its release condition — and if the designer returned on a read-start rather than a release, the checker written from the RTL uses the same signal and passes. The effect form is written against a different observable — a read occurring after a return — so the same misconception cannot satisfy it. 19.5 §23 made this argument and it is the single most transferable technique in the chapter.

28. Stale Epoch Rejection and Conservation

// MANDATORY — 6. A return from a dead agreement changes nothing.
property p_stale_return_inert;
  @(posedge clk) disable iff (!por_n)
    (return_valid && (return_epoch != chk_credit_epoch))
      |=> (credit_q == $past(credit_q)) || $past(advert_apply);
endproperty
a_stale_return_inert: assert property (p_stale_return_inert);
 
// MANDATORY — the epoch advances atomically with the re-baseline, so no window
// exists in which one has moved and the other has not.
property p_epoch_atomic_with_rebaseline;
  @(posedge clk) disable iff (!por_n)
    epoch_advance |-> advert_apply;
endproperty
a_epoch_atomic_with_rebaseline: assert property (p_epoch_atomic_with_rebaseline);
 
// MANDATORY — the re-baseline sets the counter EXACTLY. Not "at least".
property p_advert_sets_exact;
  @(posedge clk) disable iff (!por_n)
    advert_apply |=> (credit_q == CREDIT_W'($past(advert_value)));
endproperty
a_advert_sets_exact: assert property (p_advert_sets_exact);
 
// MANDATORY — 7. Conservation, against CHECKER state derived from observed
// events (§18). This is the property the other six cannot substitute for.
property p_credit_conserved;
  @(posedge clk) disable iff (!por_n)
    ((chk_advertised - chk_consumed + chk_returned) == credit_q);
endproperty
a_credit_conserved: assert property (p_credit_conserved);

On p_advert_sets_exact once more. An inequality passes while a straggler is absorbed into the freshly re-baselined counter. Equality turns that into an immediate failure at the exact cycle, naming the cause, rather than an overflow several thousand cycles later in a different block. One line, and it is the highest-value single property in the credit set.

29. Queue and Buffer Properties

// MANDATORY. GENERIC STRUCTURAL CONTRACTS.
property p_no_overflow;
  @(posedge clk) disable iff (!por_n)
    push_fire |-> !full;
endproperty
 
property p_no_underflow;
  @(posedge clk) disable iff (!por_n)
    pop_fire |-> !empty;
endproperty
 
// Occupancy against the CHECKER's push/pop count — catches a drifting counter
// AND a pointer that advanced without a memory write. The design-vs-pointer
// comparison alone leaves both design registers consistent and wrong together.
property p_occupancy_matches_checker;
  @(posedge clk) disable iff (!por_n)
    (occupancy_q == chk_occupancy);
endproperty
a_occupancy_matches_checker: assert property (p_occupancy_matches_checker);
 
// The head is stable while the consumer is stalled — a queue's version of §11.
property p_head_stable_under_stall;
  @(posedge clk) disable iff (!por_n)
    (!empty && !pop_fire) |=> (!empty && $stable(head_data) && $stable(head_meta));
endproperty
 
// Conservation across the whole structure, over the run.
property p_queue_conserved;
  @(posedge clk) disable iff (!por_n)
    (chk_pushed == chk_popped + occupancy_q);
endproperty
a_queue_conserved: assert property (p_queue_conserved);

Why p_occupancy_matches_checker compares against checker state rather than against the pointer difference. 19.4 §9's argument: a design-versus-pointer comparison catches a stray counter, and a pointer that advanced without a corresponding memory write leaves both design registers consistent with each other and wrong together. Only an independently maintained count sees that.

30. Metadata Alignment

// MANDATORY. The failure 19.4 §16 designs against: payload and metadata written
// on separate events, offsetting every subsequent entry permanently.
property p_payload_meta_same_event;
  @(posedge clk) disable iff (!por_n)
    payload_write_fire <-> meta_write_fire;
endproperty
a_payload_meta_same_event: assert property (p_payload_meta_same_event);
 
property p_payload_meta_same_index;
  @(posedge clk) disable iff (!por_n)
    payload_write_fire |-> (payload_wr_idx == meta_wr_idx);
endproperty
a_payload_meta_same_index: assert property (p_payload_meta_same_index);
 
// The EFFECT form — what popped out carries the metadata that went in with it.
// Requires checker state holding the expected pairing.
property p_pairing_preserved;
  @(posedge clk) disable iff (!por_n)
    pop_fire |-> (head_meta == chk_expected_meta[chk_head_tag]);
endproperty

The <-> operator in the first property is deliberate. It asserts the events are equivalent in both directions — a metadata write with no payload write is as wrong as the reverse, and |-> would only catch one of them.

31. Replay Ownership

// MANDATORY. ILLUSTRATIVE ARCHITECTURAL CONTRACT (§3) — no UCIe replay rule is
// claimed. These describe the reliability architecture of Chapter 19.3.
 
// An accepted object is owned by SOMEONE at every cycle — 19.3 §11's property.
// The disjunction is the point: the handoff window is legal, the gap is not.
property p_object_always_owned(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (obj_accept && (obj_tag == tag))
      |=> (chk_in_staging[tag] || chk_in_replay[tag])
          until_with chk_resolved[tag];
endproperty
 
// A live history entry is never overwritten — 19.3 §21's ring invariant.
property p_no_overwrite_live_history;
  @(posedge clk) disable iff (!por_n)
    replay_write_fire |-> !chk_replay_live[replay_wr_idx];
endproperty
a_no_overwrite_live_history: assert property (p_no_overwrite_live_history);
 
// Retirement waits for resolution, not for the send — 19.3 §46.
property p_retire_on_resolution_only;
  @(posedge clk) disable iff (!por_n)
    replay_retire_fire |-> chk_resolved[replay_retire_tag];
endproperty
a_retire_on_resolution_only: assert property (p_retire_on_resolution_only);

The first property's until_with is the whole check. It says ownership is continuous from acceptance to resolution, with the staging-and-replay disjunction permitting the handoff window (19.3 §13) while forbidding a gap. A property written as two separate ownership checks would accept a single cycle in which neither owns it — which is the exact cycle an object is lost.

32. Integrity, Delivery and Duplicates

// MANDATORY — nothing is delivered before its verdict is known.
property p_no_delivery_before_verdict;
  @(posedge clk) disable iff (!por_n)
    deliver_fire |-> (verdict_valid && verdict_good);
endproperty
a_no_delivery_before_verdict: assert property (p_no_delivery_before_verdict);
 
// MANDATORY — the EFFECT form: a bad verdict is never followed by a delivery
// of that object. Written against a different observable than the gate itself.
property p_bad_verdict_never_delivered(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (verdict_valid && !verdict_good && (verdict_tag == tag))
      |=> always !(deliver_fire && (deliver_tag == tag) && !redelivery_authorised);
endproperty
 
// MANDATORY — a duplicate arrival is suppressed. Uses the checker's own record
// of what has been delivered, not the design's duplicate window (§19) — which
// is the structure whose sizing is the likely bug.
property p_duplicate_suppressed;
  @(posedge clk) disable iff (!por_n)
    (arrival_fire && chk_already_delivered[arrival_tag]) |=> !deliver_fire;
endproperty
a_duplicate_suppressed: assert property (p_duplicate_suppressed);

Why the third property must not consult the design's window. 19.3 §32's duplicate window has a size, and the failure mode is that the size is too small — an old duplicate falls outside it and is delivered again. A checker that asks the design's window "have I seen this?" gets the same wrong answer (20.1 §55's scenario). The checker's own record has no window at all, so it never forgets.

33. Exactly-Once — the Safety Half

// MANDATORY. The safety half: AT MOST ONE delivery per SEMANTIC operation.
// Note the level (§34) — this is false at the object and attempt levels.
property p_delivered_at_most_once(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (sem_deliver_fire && (sem_deliver_tag == tag))
      |=> always !(sem_deliver_fire && (sem_deliver_tag == tag));
endproperty
 
// MANDATORY — no completion after a failure was reported. The dangerous
// direction: the client has taken its error path and may have reissued.
property p_no_success_after_failure(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (sem_fail_fire && (sem_fail_tag == tag))
      |=> always !(sem_complete_fire && (sem_complete_tag == tag));
endproperty
a_no_success_after_failure: assert property (p_no_success_after_failure);

Both use the monitor tag (20.1 §23), not a wire field. A protocol identity is legitimately reused after retirement, so always keyed on it would fire falsely on a legal reuse. The monitor tag is unique for the whole simulation, which is what makes "never again" a checkable statement.

34. Exactly-Once — the Liveness Half

// MANDATORY. The liveness half, with its assumptions named.
//   A1  clocks continue; the hard reset is not re-asserted
//   A2  the peer eventually responds to a delivered object
//   A3  injected errors eventually cease
//   A4  the link eventually leaves recovery
property p_obligation_eventually_resolves(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (sem_accept_fire && (sem_tag == tag))
      |-> ##[1:OBLIGATION_BOUND] (chk_terminal[tag]);
endproperty

Why the two halves are separate properties and not one.

They fail differently. The safety half fails at a specific cycle with a duplicate in the waveform. The liveness half fails at the end of a run, or at a bound, with nothing local to look at.

They need different evidence. Safety needs no assumptions; liveness is meaningless without A1–A4.

And they can fail independently. An operation delivered twice satisfies liveness and violates safety. An operation never delivered satisfies safety — vacuously, at most once being trivially true of zero — and violates liveness. A single combined property that "the operation is delivered exactly once" is a conjunction whose failure message cannot tell you which half broke.

And note the vacuity trap in that observation. At most once is satisfied by zero deliveries. The safety property alone can be satisfied by a design that delivers nothing at all, which is why the pairing is mandatory and why §48's cover properties matter for the safety half specifically.

35. Wrong Exactly-Once — Stated at the Object Level

// WRONG — asserts that a TRANSPORT OBJECT crosses at most once.
property p_object_sent_once_bad(int unsigned obj);
  @(posedge clk) disable iff (!por_n)
    (attempt_fire && (attempt_obj == obj))
      |=> always !(attempt_fire && (attempt_obj == obj));
endproperty

A retransmission is a second attempt of the same object. The property fires on correct reliability behaviour, at every single retry.

Three levels, three different truths (20.1 §38):

And the consequence of getting the level wrong is worse than a false failure. The property fires on every error-injection test, so it is disabled in exactly the test suite where duplication is most likely — leaving the real exactly-once question unchecked precisely where retransmission is being exercised.

36. FSM Properties

// ILLUSTRATIVE IMPLEMENTATION CONTRACTS (§54 — white-box, non-portable).
// These describe the ILLUSTRATIVE controller of Chapter 19.1, not UCIe.
 
// Legal arcs only, via an INDEPENDENTLY written arc function (§19).
property p_legal_arc;
  @(posedge clk) disable iff (!por_n)
    $changed(state_q) |-> chk_legal_arc($past(state_q), state_q);
endproperty
a_legal_arc: assert property (p_legal_arc);
 
// No illegal encoding — catches an SEU or an incomplete reset.
property p_state_encoding_valid;
  @(posedge clk) disable iff (!por_n)
    state_q inside {S_RESET, S_INIT, S_TRAIN, S_ACTIVE, S_RECOVER, S_FAILED};
endproperty
a_state_encoding_valid: assert property (p_state_encoding_valid);
 
// One-hot, where the encoding is one-hot.
property p_state_onehot;
  @(posedge clk) disable iff (!por_n)
    $onehot(state_onehot_q);
endproperty
 
// State-dependent outputs — traffic permission is derived from the state.
property p_permission_only_in_active;
  @(posedge clk) disable iff (!por_n)
    traffic_permitted |-> (state_q inside {S_ACTIVE, S_DEGRADED});
endproperty

37. Configuration Lifetime

// MANDATORY. ILLUSTRATIVE ARCHITECTURAL CONTRACTS — 19.6 §24 at assertion level.
 
// The active configuration changes only on a commit.
property p_active_cfg_changes_on_commit_only;
  @(posedge clk) disable iff (!por_n)
    $changed(cfg_active_q) |-> $past(cfg_commit);
endproperty
a_active_cfg_changes_on_commit_only:
  assert property (p_active_cfg_changes_on_commit_only);
 
// The commit is exactly one cycle, so no multi-cycle mixed window exists.
property p_commit_single_cycle;
  @(posedge clk) disable iff (!por_n)
    cfg_commit |=> !cfg_commit;
endproperty
a_commit_single_cycle: assert property (p_commit_single_cycle);
 
// A requested change does not reach the datapath before the commit.
property p_requested_does_not_leak;
  @(posedge clk) disable iff (!por_n)
    (cfg_requested_q != cfg_active_q) |-> (datapath_cfg == cfg_active_q);
endproperty
a_requested_does_not_leak: assert property (p_requested_does_not_leak);
 
// THE EFFECT PROPERTY — no live object's epoch changes under it. This is what
// atomicity is FOR, and it holds regardless of how the commit is implemented.
property p_object_sees_one_epoch(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (obj_accept && (obj_tag == tag))
      |=> (chk_epoch_at_accept[tag] == chk_epoch_now)
          until_with chk_resolved[tag];
endproperty

The fourth property is the durable one. The first three describe this commit machine; the fourth describes what it exists to guarantee, and it would catch 19.6 §23's partial commit in a design with no commit machine at all — which is exactly the design that has the bug.

38. Recovery Properties

// MANDATORY. Note the disable condition on EVERY property here — §42.
 
// Semantic state is not cleared by a transport recovery.
property p_semantic_survives_recovery;
  @(posedge clk) disable iff (!por_n)
    recovery_entry |=> (chk_outstanding_count == $past(chk_outstanding_count));
endproperty
a_semantic_survives_recovery: assert property (p_semantic_survives_recovery);
 
// Per-tag, because a count can be preserved while the SET changes — one
// obligation lost and one invented leaves the count identical.
property p_every_tag_survives_recovery(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (recovery_entry && chk_outstanding[tag])
      |=> chk_outstanding[tag] until_with chk_terminal[tag];
endproperty
 
// No admission while recovery prohibits it.
property p_no_admission_during_recovery;
  @(posedge clk) disable iff (!por_n)
    (chk_phase == RM_RECOVERY) |-> !obj_accept;
endproperty
a_no_admission_during_recovery: assert property (p_no_admission_during_recovery);
 
// The first-fault record is not overwritten by a cascade.
property p_first_fault_sticky;
  @(posedge clk) disable iff (!por_n)
    first_fault_valid |=> ($stable(first_fault_record) || diag_clear_fire);
endproperty
a_first_fault_sticky: assert property (p_first_fault_sticky);
 
// A stale event from a dead epoch changes nothing.
property p_stale_event_inert;
  @(posedge clk) disable iff (!por_n)
    (event_valid && (event_epoch != chk_link_epoch)) |=> $stable(link_state_q);
endproperty

p_first_fault_sticky is the property that verifies sticky-first rather than sticky-last. 19.1 §35 and 13.3 §12 both argued that errors cascade and the last one is almost always a consequence. A last-capture implementation passes every other test in the suite and fails only this one.

39. Reset Scoping — Three Kinds, Three Answers

Not every reset should disable every property, and treating them as one is §40's flagship anti-pattern.

The rule, in one sentence:

A property is disabled by a reset only if the property has no meaning under that reset. A property about what a reset must preserve has its maximum meaning during that reset, and disabling it there is the same as deleting it.

40. Wrong disable iff — Sleeping Through the Bug

The flagship SVA anti-pattern in this chapter.

// WRONG — the property that checks recovery preservation is disabled during
// recovery. It is asleep at exactly the cycle the state is cleared.
property p_semantic_survives_recovery_bad;
  @(posedge clk) disable iff (!rst_n || recovery_active)
    recovery_entry |=> (chk_outstanding_count == $past(chk_outstanding_count));
endproperty

Worked, and it is 20.2 §12's design bug meeting a checker that cannot see it.

The property never fires. The report is green.

Five properties, and the fifth is why this is worth a whole section.

The disable iff was added for a good reason. During recovery, other properties were firing — properties about traffic, credits and framing that genuinely have no meaning while the link is down. The engineer added the term to one property and then, reasonably, to all of them.

The failure is total and silent. Not a weakened check — no check at all, for the exact window the property was written for.

It looks correct in review. disable iff (!rst_n || recovery_active) reads as careful, defensive engineering.

And it composes with §12's environment bug to produce a design that is verified by nothing. The environment's models are cleared by the recovery, the assertion is disabled by the recovery, and the design's recovery clears state it should preserve. Three independent decisions, each locally reasonable, and the result is a link that silently loses work with a fully green regression.

The fifth: it is undetectable from the report. A disabled property is not a failing property and not a vacuous one — it produces no antecedent activation, so even §48's cover-property defence shows nothing unusual unless somebody notices the cover is also zero. The defence is §39's table, applied deliberately, per property.

41. What disable iff Should Contain

A default that is right most of the time, and the three exceptions.

// THE DEFAULT — the hard reset only. Everything narrower is a decision.
disable iff (!por_n)
 
// EXCEPTION 1 — properties about traffic, framing or resource values, which
// genuinely have no meaning while the link is down.
disable iff (!por_n || !link_operational)
 
// EXCEPTION 2 — properties about a specific structure that is legitimately
// held in reset by a power or clock-gating domain.
disable iff (!por_n || !domain_active)
 
// EXCEPTION 3 — properties whose antecedent cannot occur during a window, where
// disabling is a performance optimisation rather than a semantic decision.
// Document it as such, because it is indistinguishable from a semantic one.
disable iff (!por_n || cfg_reprogramming)

Three rules that follow.

Every term beyond !por_n needs a written justification, in a comment, naming which cycles it removes and why the property has no meaning in them. A disable iff with three OR-ed terms and no comment is three unreviewed decisions.

A property about preservation, survival, stickiness or immutability almost never takes exception 1. Those are the properties whose whole content is about the window exception 1 removes.

And exception 3 is the one that silently becomes exception 1. A term added for simulation performance looks identical to a term added for semantics, and the next engineer to touch the property cannot tell which it was. Label it.

The review question for every disable iff: "name a cycle this term removes, and say what the property would have wrongly claimed at that cycle." If the answer is "nothing — it just wasn't firing", the term is hiding something.

42. Assumptions

Liveness needs assumptions. Safety does not. Getting that backwards produces either a meaningless proof or a deleted property.

// FORMAL ENVIRONMENT ASSUMPTIONS. In formal these are `assume`; in simulation
// they are constraints on the environment — and in both cases they are written
// down next to the properties they support (20.1 §28).
//
//  A1  clocks continue; the hard reset is not re-asserted
//  A2  the downstream consumer eventually accepts
//  A3  the peer eventually responds to a delivered object
//  A4  injected errors eventually cease
//  A5  arbitration is fair — an eligible requester stays eligible
//  A6  a pending request is not withdrawn while it waits
assume property (@(posedge clk) s_eventually downstream_ready);
assume property (@(posedge clk) s_eventually !error_injection_active);
assume property (@(posedge clk) s_eventually (chk_phase != RM_RECOVERY));
assume property (@(posedge clk)
  (req_pending && !req_served) |=> req_pending);          // A6

Three rules about assumptions.

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

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

And assumptions must appear in the results. A regression reporting "all liveness properties passed" without naming the active assumptions has reported almost nothing. Tightening an assumption is how a liveness property is quietly made vacuous, and only a visible assumption list makes that reviewable.

On assume versus assert — the category error worth naming. An assume on an environment behaviour written as an assert reports a testbench failure as a design failure, sends triage to the wrong team, and — in formal — is unsound in the direction that matters: the tool has been told the design guarantees something it does not, and every property proved under it is proved under a false hypothesis.

43. Wrong Assumption — Assuming the Conclusion

// WRONG — assumes the property being proved.
assume property (@(posedge clk) req |-> s_eventually grant);
 
// ... and then "proves":
property p_arbiter_eventually_grants;
  @(posedge clk) disable iff (!por_n)
    req |-> s_eventually grant;
endproperty
a_arbiter_eventually_grants: assert property (p_arbiter_eventually_grants);

The proof succeeds and establishes nothing. The assumption is the property.

Four properties, and the third is the realistic form.

The blatant form is rare and gets caught in review.

The subtle form is not. assume property (s_eventually !arbiter_blocked) where arbiter_blocked is a design-internal signal that is high exactly when the arbiter is misbehaving. The assumption removes every trace in which the bug occurs, and the liveness proof succeeds on the remaining traces.

The realistic form is an assumption on the design's own output. Any assume whose expression names a design signal rather than an environment input is a candidate for this failure — because the design's outputs are consequences, and assuming a consequence removes the counterexamples.

And the defence is mechanical. Every assume must reference only environment inputs and their timing, never a design output or internal. That is a grep-able rule and it should be a review gate.

44. Bounded Liveness

// PREFERRED IN SIMULATION — a bound, with the derivation in the comment.
//
//   bound = arbitration worst case      (NUM_CLASSES-1) * MAX_GAP
//         + link round trip             RTT_MAX
//         + one permitted retry         RETRY_MAX
//         + one recovery                RECOVERY_MAX
//         + the peer's response budget  PEER_RSP_MAX
localparam int OBLIGATION_BOUND = (NUM_CLASSES-1)*MAX_GAP + RTT_MAX
                                + RETRY_MAX + RECOVERY_MAX + PEER_RSP_MAX;
 
property p_obligation_bounded(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (sem_accept_fire && (sem_tag == tag))
      |-> ##[1:OBLIGATION_BOUND] chk_terminal[tag];
endproperty

Four reasons the bounded form beats s_eventually in simulation.

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

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

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

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

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

And a bound must never be invented where the architecture provides none (§3). A test-plan bound is a statement about this implementation under this test — label it so, because a violation means "slower than we expected", not "violated the specification". Where the architecture genuinely provides a bound, cite it.

45. Fairness

// MANDATORY where an arbiter exists. Bounded wait, per requester, under A5.
property p_bounded_wait(int unsigned c);
  @(posedge clk) disable iff (!por_n)
    (req[c] && !grant[c])
      |-> ##[1:(NUM_CLASSES-1)*MAX_GRANT_GAP] grant[c];
endproperty
 
// MANDATORY — the rotation advances only on an ACTUAL transfer, not on a grant.
// 19.5 §19's rule applied to the arbiter itself: a grant that produces no
// transfer must not consume the requester's turn.
property p_rotation_on_transfer_only;
  @(posedge clk) disable iff (!por_n)
    $changed(rr_ptr_q) |-> $past(transfer_fire);
endproperty
a_rotation_on_transfer_only: assert property (p_rotation_on_transfer_only);
 
// MANDATORY — the SYSTEM-LEVEL form, independent of the arbiter's structure.
// This is the one that survives an arbiter redesign.
property p_no_class_starved(int unsigned c);
  @(posedge clk) disable iff (!por_n)
    (chk_pending[c] != 0) |-> ##[1:STARVE_MAX] chk_served[c];
endproperty

The third property is the durable one. The first two describe this arbiter; the third describes the outcome the arbiter exists to produce. If the arbiter is replaced, the first two must be rewritten and the third does not change — and it is the third that would catch 19.5 §49's starvation in a design where the priority encoder is buried in a shared control-path multiplexer nobody thought of as an arbiter.

46. Severity

Not every property is fatal, and treating them uniformly makes the report unreadable.

Three rules.

Stopping is right when continuing produces derived failures. A credit over-allocation corrupts everything downstream; a run that continues past it produces fifty failures with one cause, and the report becomes a triage problem.

Continuing is right when the failure is localised. A single stability violation on one boundary does not invalidate the rest of the run, and the rest of the run may contain a second, different failure worth finding in the same simulation.

And a diagnostic must never be an error. A high-water mark, a retry count or a latency observation is evidence for the next design review (19.4 §54), not a defect. Making it an error trains the team to ignore the report, which is the same failure mode as §16's watchdog and §23's over-constrained ordering property.

47. Parameterised Assertions

// ILLUSTRATIVE. One property instance per resource, generated. Note the
// elaboration guard (§52) and the width discipline (19.6 §9).
generate
  for (genvar c = 0; c < NUM_CLASSES; c++) begin : g_credit_chk
    // Per-class credit bound.
    a_credit_bounded: assert property (
      @(posedge clk) disable iff (!por_n)
        (credit_q[c] <= active_capacity[c])
    );
    // Per-class consume guard, indexed from the EVENT, not from a shared reg.
    a_no_consume_without_credit: assert property (
      @(posedge clk) disable iff (!por_n)
        (consume_fire && (consume_class == CLS_W'(c)))
          |-> (consume_units <= credit_q[c])
    );
  end
 
  for (genvar i = 0; i < NUM_IDS; i++) begin : g_id_chk
    a_no_reuse_while_live: assert property (
      @(posedge clk) disable iff (!por_n)
        (alloc_accept && (alloc_id == ID_W'(i))) |-> !chk_id_live[i]
    );
  end
endgenerate

Three notes.

The comparison casts explicitly. CLS_W'(c) rather than a bare c. A genvar is an integer; comparing it against a narrow signal without a cast is where §50's truncation lives.

The index comes from the event, not from a shared register. 19.5 §47's discipline: a shared "current class" register produces a check charged to the wrong class, which keeps the total right and both individual checks wrong.

And the loop bound is the parameter, not a literal. A hardcoded 4 generates four checkers on an eight-class design and checks half of it silently — §50.

48. Vacuity

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

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

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

A feature is disabled in the configuration under test. Every property about it is vacuous. In a parameterised design that is the norm (19.6 §35), and each configuration has a different vacuity profile.

The antecedent is unreachable for a subtler reason. A property gated on error_detected && recovery_active is vacuous in every run where errors were injected only while the link was healthy.

A disable iff covers the interesting window — §40, and it is worse than ordinary vacuity because even the cover shows nothing.

An over-strong assume in formal removes the traces that would exercise it (§43).

And a safety property can be vacuous in a way that reads as correct. "At most one delivery" is satisfied by zero deliveries (§34). A design that delivers nothing at all passes it, which is why the liveness pairing is mandatory rather than optional.

The defence:

// For EVERY implication property, a cover for its antecedent.
c_replay_active:     cover property (@(posedge clk) replay_active);
c_replay_and_check:  cover property (@(posedge clk)
                       replay_active ##[0:64] chk_order_checkpoint);

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

49. cover property, and What It Does Not Prove

Three distinct things coverage tells you, and they are often conflated.

The pass count is the one most environments do not collect, and it catches a specific, embarrassing failure: a property that was never bound at all — because the bind path was wrong, the module was renamed, or a generate branch removed the instance. Such a property is neither passing nor failing; it does not exist, and only a pass count of exactly zero, reported per property, finds it.

Read together: high pass count + covered antecedent + no failures = genuinely checked. High pass count + uncovered antecedent = a vacuous property being counted as the strongest evidence in the report.

And what coverage never proves is correctness. cover property says the situation occurred. It says nothing about whether the design behaved correctly in it — that is the assertion's job, and a plan that reports 100% cover with no assertions has measured its stimulus, not its design.

50. Wrong Generate Checker — The Truncated Index

// WRONG — the comparison truncates, so only some resources are checked.
localparam int CLS_W = 2;                     // 4 classes fit
// ... but the design was later built with NUM_CLASSES = 8
 
generate
  for (genvar c = 0; c < NUM_CLASSES; c++) begin : g_chk
    a_credit: assert property (
      @(posedge clk) disable iff (!por_n)
        (consume_fire && (consume_class == CLS_W'(c)))   // 2-bit compare!
          |-> (consume_units <= credit_q[c])
    );
  end
endgenerate

Worked. CLS_W is 2, so CLS_W'(c) for c = 4 is 2'b00, and for c = 5 is 2'b01. Classes 4 through 7 generate checkers that compare against classes 0 through 3.

Consequences, and there are three distinct ones:

Classes 4–7 are unchecked. Their properties exist, are bound, and never have a true antecedent for their own class.

Classes 0–3 are double-checked, against the wrong credit register. The c = 4 instance compares consume_class == 0 against credit_q[4]. That is a false failure waiting to happen, and it will be blamed on the design.

And the coverage report shows the properties passing. Eight instances, eight non-zero pass counts, and half of them checking the wrong thing. §48's antecedent cover would show four antecedents that never fire for their own class — but only if the cover is written per class, which is exactly the discipline this bug defeats.

The fix is an elaboration check (§52), not a wider cast:

initial begin
  assert (CLS_W >= $clog2(NUM_CLASSES))
    else $fatal(1, "CLS_W=%0d cannot index NUM_CLASSES=%0d", CLS_W, NUM_CLASSES);
end

51. The Bindable Contract Checker

// ILLUSTRATIVE SKETCH — no file is created in this repository. Note the port
// list: BOUNDARY-OBSERVABLE SIGNALS ONLY. That is what makes it portable.
module ucie_adapter_contract_checker #(
  parameter int NUM_CLASSES = 3,
  parameter int NUM_IDS     = 32,
  parameter int CREDIT_W    = 6
) (
  input logic                    clk,
  input logic                    por_n,
  // protocol-facing boundary
  input logic                    in_valid, in_ready,
  input logic [PAYLOAD_W-1:0]    in_payload,
  input logic [META_W-1:0]       in_meta,
  input logic [CLS_W-1:0]        in_cls,
  input logic                    in_first, in_last, in_poison,
  // transport boundary
  input logic                    attempt_fire,
  input logic [ID_W-1:0]         attempt_id,
  input logic                    verdict_valid, verdict_good,
  input logic [ID_W-1:0]         verdict_id,
  // delivery boundary
  input logic                    deliver_fire,
  input logic [ID_W-1:0]         deliver_id,
  // flow control
  input logic [CREDIT_W-1:0]     credit_q [NUM_CLASSES],
  input logic                    consume_fire, return_fire,
  // link status — DERIVED status, not internal state
  input logic                    link_operational,
  input logic                    recovery_active
);
  // §18's checker state, §11/§20/§26/§27/§32's properties, generated per §47.
endmodule
 
// Bound by the integrator without touching the DUT.
bind ucie_adapter ucie_adapter_contract_checker #(
  .NUM_CLASSES (NUM_CLASSES), .NUM_IDS (NUM_IDS), .CREDIT_W (CREDIT_W)
) u_contract_chk (.*);

Three properties of a checker built this way.

Its port list is the contract, made executable. A signal in this port list that is not in the interface document is a coupling to the implementation — and the review question for every port is "is this in the contract?"

It ships with the IP (19.6 §48), so every integrator gets the same checks rather than re-deriving them from the RTL and getting them subtly wrong.

And it survives an internal redesign, which is exactly what a checker built on retry_pending_q does not (§58).

52. Elaboration Checks for Checkers

// ILLUSTRATIVE. A checker is parameterised code and has the same
// parameterisation hazards as the design (19.6 §10).
initial begin : g_chk_param_check
  assert (NUM_CLASSES > 0);
  assert (NUM_IDS     > 0);
  assert (CLS_W >= $clog2(NUM_CLASSES))
    else $fatal(1, "CLS_W cannot index NUM_CLASSES");        // §50
  assert (ID_W  >= $clog2(NUM_IDS))
    else $fatal(1, "ID_W cannot index NUM_IDS");
  assert (CREDIT_W >= $clog2(MAX_CAPACITY + 1))
    else $fatal(1, "CREDIT_W cannot represent MAX_CAPACITY"); // 19.5 §11
  // The checker's own bound must be at least the design's bound, or the
  // checker reports false failures on legal slow behaviour (20.2 §16).
  assert (OBLIGATION_BOUND >= DESIGN_WORST_CASE_LATENCY);
end

Why a checker needs its own elaboration checks. A width defect in a checker produces a checker that silently checks the wrong thing (§50) — which is worse than a design defect, because it removes the mechanism that would have found the design defect.

And the last assertion is the one nobody writes. 20.2 §16's failure at assertion level: a checker bound tighter than the design's legal worst case reports false failures, and the fix applied is usually to disable the property.

53. Black-Box Versus White-Box

Neither replaces the other, and the reason is in the last two rows.

A black-box checker cannot see a corrupted free-list, a pointer that passed its retirement bound, or a one-hot register with two bits set. Those are real bugs with real consequences, and they are invisible at the boundary until they produce a contract violation several hundred cycles later.

A white-box checker cannot be shipped, cannot be reused, and breaks on every refactor — so a plan built only from white-box properties has to be rewritten with the design.

Write both, in separate modules, and label which is which. The black-box module is verification collateral for the whole ecosystem; the white-box module is the design team's own tripwire, and it should live next to the RTL it constrains.

54. The White-Box Implementation Checker

// ILLUSTRATIVE SKETCH — NON-PORTABLE BY CONSTRUCTION. Every property here names
// an internal structure and will break if that structure changes. That is
// acceptable, and it is why this is a separate module from §51's.
module ucie_adapter_impl_checker (input logic clk, por_n /* + internal probes */);
 
  // The free-list is exactly the complement of the live set. Catches a leak
  // and a double-free simultaneously, and neither is visible at the boundary
  // until much later.
  a_freelist_consistent: assert property (
    @(posedge clk) disable iff (!por_n)
      (free_bitmap_q == ~live_bitmap_q)
  );
 
  // The replay ring's three pointers keep their order — 19.3 §22's invariant.
  a_ring_pointer_order: assert property (
    @(posedge clk) disable iff (!por_n)
      ((alloc_ptr_q - retire_ptr_q) <= RING_DEPTH)
  );
 
  // A one-hot state register really is one-hot.
  a_state_onehot: assert property (
    @(posedge clk) disable iff (!por_n) $onehot(state_onehot_q)
  );
 
  // Occupancy equals the wide-pointer difference — 19.4 §9. Catches a stray
  // maintained counter that has drifted.
  a_occupancy_derived: assert property (
    @(posedge clk) disable iff (!por_n)
      (occupancy_q == OCC_W'(wr_ptr_q - rd_ptr_q))
  );
 
endmodule

Why these are worth writing despite being non-portable.

They localise to a register. When a_freelist_consistent fires, the finding is "the free-list and the live set disagree at index 7" — a one-line fix, found at the cycle it happened. The same bug seen at the boundary is "an identity was allocated twice", three hundred cycles later.

They catch corruption that has not yet produced a contract violation. A pointer that has passed its bound is a bug now; the data loss happens later. The white-box property fires at the cause.

And they are the design team's tripwires during refactoring. When the buffer is redesigned, a_occupancy_derived fails immediately if the new pointer discipline is wrong — which is the fastest possible feedback and is worth more than portability inside the team that owns the block.

55. Assertion Layering

Group properties by the boundary or block they constrain, and bind each group where it belongs. The grouping is what makes a failure's location obvious before anyone opens a waveform.

Two rules.

Each group has its own file and its own bind statement, so a group can be disabled wholesale for a bring-up run and re-enabled without editing individual properties.

And the recovery group deliberately spans boundaries, which makes it the group most likely to be scoped wrongly. Every property in it needs §39's table applied individually — it is the group §40's anti-pattern lives in.

56. Configuration Conditioning

A property that is false in a supported configuration will be deleted, not scoped. So the scoping must be built in.

// ILLUSTRATIVE. Reliability properties are conditional on the configuration,
// because CRC and retry are OPTIONAL Adapter functions (§3) and Raw Mode
// bypasses the Adapter entirely.
generate
  if (REPLAY_ENABLE) begin : g_replay_props
    a_object_always_owned:        assert property (p_object_always_owned);
    a_retire_on_resolution_only:  assert property (p_retire_on_resolution_only);
    a_duplicate_suppressed:       assert property (p_duplicate_suppressed);
  end else begin : g_no_replay_props
    // The DISABLED-feature properties: the feature is genuinely inert.
    a_no_replay_activity: assert property (
      @(posedge clk) disable iff (!por_n)
        (!replay_active && (replay_attempt_count == '0))
    );
  end
 
  if (ADAPTER_IN_PATH) begin : g_adapter_props
    a_no_delivery_before_verdict: assert property (p_no_delivery_before_verdict);
  end else begin : g_raw_mode_props
    // In Raw Mode the Protocol Layer owns error protection (§3), so the
    // equivalent property binds at a DIFFERENT boundary — not nowhere.
    a_proto_owns_integrity: assert property (p_proto_layer_integrity_gate);
  end
endgenerate

Three properties of this pattern.

The else branch is not empty. A disabled feature gets a property saying it is inert (19.6 §47), and a bypassed layer gets the equivalent property at the layer that now owns the responsibility. "Not applicable" is not the same as "unchecked".

Without it, the reliability properties fire in Raw Mode and get deleted from everywhere — 20.1 §51's argument, and it is the most likely route by which a good property set becomes a bad one.

And every branch needs its own antecedent cover (§48), because a dual-mode design verified only in one mode has one mode verified — and the coverage report is the only thing that says which.

57. Flagship Wrong Property 1 — The Fixed-Latency Expectation

// WRONG — assumes the acknowledgement always arrives the next cycle.
property p_ack_next_cycle;
  @(posedge clk) disable iff (!por_n)
    attempt_fire |=> ack_valid;
endproperty

Worked. The acknowledgement latency is variable — it depends on the round trip, the peer's queueing, the return path's arbitration and whether a recovery intervened. On a clean link at low load it is often exactly one cycle, which is how the property got written and how it passed the first regression.

Four properties.

It fires the moment the link is loaded, and it fires constantly.

It gets "fixed" to ##[1:N] with an invented N — §44's warning. A bound with no derivation cannot be reviewed and will be raised until it catches nothing.

The correct form is a transaction property, not a latency property. The contract does not promise a latency; it promises that each attempt is eventually acknowledged or the object is retried. Writing the promise the contract actually makes turns a fragile property into a robust one:

// RIGHT — the contract's actual promise, with a derived bound (§44).
property p_attempt_resolved;
  @(posedge clk) disable iff (!por_n)
    (attempt_fire, id = attempt_id)
      |=> ##[1:ATTEMPT_BOUND] ((ack_valid && (ack_id == id))
                            || (nak_valid && (nak_id == id))
                            || retry_triggered_for(id));
endproperty

And the fourth: the wrong property's real cost is that it looks like a protocol check. It appears in the inventory as "acknowledgement timing", so a reviewer scanning for "do we check the ack path?" gets a yes — and the actual promise, that every attempt resolves, is never written.

58. Flagship Wrong Property 2 — The Implementation Signal

// WRONG in a PORTABLE checker — names an internal register.
property p_retry_state_consistent;
  @(posedge clk) disable iff (!por_n)
    dut.retry_pending_q |-> dut.replay_ring_occupied_q;
endproperty

Two distinct problems, and they have different consequences.

It couples the checker to the implementation. The first refactor that renames retry_pending_q, merges it into a state encoding, or eliminates it breaks the checker — and the checker is verification collateral that was supposed to be reusable (§51).

And it may be checking the design against itself. If retry_pending_q is derived from replay_ring_occupied_q, the property is a tautology. A property whose two sides are computed from the same source proves nothing, and that is invisible without reading the RTL — which the checker's author did, which is how the property got written.

The boundary-event alternative:

// RIGHT — the same intent, expressed in contract terms.
property p_retry_implies_live_history;
  @(posedge clk) disable iff (!por_n)
    (attempt_fire && (attempt_num > 1)) |-> chk_history_live[attempt_id];
endproperty

Three differences. It uses an observable event — a repeat attempt. It uses checker state for liveness rather than the design's register (§18). And it survives a redesign, because "a retransmission implies a retained copy" is a contract statement while "retry_pending_q implies replay_ring_occupied_q" is an implementation statement.

Where the implementation property belongs. §54's white-box module — where it is labelled non-portable, lives next to the RTL, and is expected to break on a refactor.

59. Flagship Wrong Property 3 — The Reset That Hides It

§40, restated as one of the four because it is the one that costs the most.

// WRONG — asleep during the window it exists to check.
property p_semantic_survives_recovery_bad;
  @(posedge clk) disable iff (!por_n || recovery_active)
    recovery_entry |=> (chk_outstanding == $past(chk_outstanding));
endproperty

What makes it the most expensive of the four. The other three either fire falsely — so somebody looks at them — or are vacuous in a way §48's cover detects. This one produces no failure, no vacuity signal, and no antecedent activation, because the antecedent (recovery_entry) coincides with the disable condition.

The report shows a property that exists, is bound, and has a pass count of zero — and a zero pass count is indistinguishable from "this configuration does not exercise recovery" unless somebody cross-references the recovery coverage. §49's three-way read is the only defence, and it only works if all three numbers are in the same report.

60. Flagship Wrong Property 4 — The Vacuous Pass

// WRONG BY OMISSION — no cover, so nobody knows whether it ever armed.
property p_degraded_recovery_preserves_semantics;
  @(posedge clk) disable iff (!por_n)
    (recovery_exit && width_reduced) |-> chk_semantics_intact;
endproperty
a_degraded: assert property (p_degraded_recovery_preserves_semantics);
// ... and no `cover property` anywhere.

The regression is green. The antecedent required a recovery that reduced the width, and no test in the suite produced one.

Three properties.

It reads as the strongest kind of evidence. A property named after the exact scenario, passing, in the report. A reviewer asking "do we check degraded recovery?" gets a yes.

The missing test is the expensive one to add later. Degraded recovery needs a lane-health injection with outstanding work (20.2 §30) — which nobody builds, because the property already passes.

And the fix is two lines:

c_degraded_recovery: cover property (
  @(posedge clk) (recovery_exit && width_reduced));
c_degraded_with_work: cover property (
  @(posedge clk) (recovery_exit && width_reduced && (chk_outstanding != 0)));

The second cover is the one that matters. A degraded recovery with nothing outstanding exercises the recovery path and not the preservation the property is about — which is 20.2 §53's coverage argument, and it is why the cover must be as specific as the scenario.

61. Formal Abstraction — the Data Token

Formal proof scales with state, and a UCIe datapath's state is dominated by data that the interesting properties do not depend on.

// ILLUSTRATIVE FORMAL ABSTRACTION. Replace a wide payload with a narrow
// symbolic token. The properties below are about IDENTITY and OWNERSHIP, and
// neither depends on the data's width.
`ifdef FORMAL
  localparam int PAYLOAD_W = 4;      // a token, not 512 bits
`else
  localparam int PAYLOAD_W = 512;
`endif
 
// The property that matters: what came out is what went in, for the same tag.
property p_payload_preserved(int unsigned tag);
  @(posedge clk) disable iff (!por_n)
    (accept_fire && (accept_tag == tag), tok = in_payload)
      |=> ##[1:$] ((deliver_fire && (deliver_tag == tag)) |-> (out_payload == tok));
endproperty

Three abstractions that buy the most, in order.

Data-width reduction. A 4-bit token distinguishes enough distinct values to catch a swap, a substitution or a stale read. 512 bits proves nothing extra and may prevent convergence entirely.

Depth reduction. Prove the ring invariant at RING_DEPTH = 4 rather than 128. Structural properties — no overwrite of a live entry, pointer ordering, occupancy bounds — are depth-independent in their statement, and a proof at small depth plus an inductive argument is worth far more than a bounded proof at full depth.

Control-state abstraction. Replace the training sequence with a nondeterministic transition into the operational phase, constrained by the evidence conjunction of 20.2 §10. The properties about traffic admission do not care how training got there — only that permission and agreement both hold.

And the discipline that keeps abstraction honest. Every abstraction is a claim that the property does not depend on what was abstracted away, and that claim must be written down. A payload-width reduction is safe for an ownership property and unsafe for a CRC property, which depends on every bit.

62. Formal Proof Targets

Two observations.

Formal is strongest exactly where Module 19's simultaneous-event bugs live — 19.5 §13's consume-and-return, 19.3 §24's allocate-and-retire, 19.4 §16's payload-and-metadata. Each needs one cycle in which two things happen; simulation reaches those by luck and formal by construction.

And a bounded proof is a partial result that must be labelled as one. A property "covered by formal" whose proof was bounded to depth 12 is covered to depth 12 and nowhere else. The plan records the bound, or it records a fiction.

63. Proof Decomposition

When a property will not converge, decompose it rather than abandoning it.

Four techniques, in the order to try them.

Split the property. "Exactly once across a recovery" is a conjunction: at-most-once (safety) and eventually-once (liveness). Prove the safety half — which is often tractable — and take the liveness half to simulation with a bound (§44).

Abstract the neighbours. Prove the Adapter's ownership invariant with the protocol engine replaced by a nondeterministic generator constrained by the boundary contract. The generator's constraints are exactly §51's checker properties, used as assumptions — which is a satisfying reuse and also a trap: an over-strong constraint removes counterexamples (§43).

Prove an inductive invariant instead of the property. "Live claims never exceed capacity" is hard to prove directly and easy to prove inductively from "a claim is set only when free, and cleared only when set" (19.5 §54). The inductive lemma is the artefact; the property follows.

And reduce parameters, then argue the generalisation. A proof at NUM_IDS = 4 plus an argument that the property is per-identity and identities do not interact is stronger evidence than a bounded proof at 32 — and the argument must be written down, because it is the part that can be wrong.

64. Assertion Debug Methodology

An assertion failed. Work in this order, and do not skip to step 8.

1 — Read the antecedent, not the failure cycle. The reported cycle is where the consequent was evaluated; the cause is the arming condition, which for |=> is one cycle earlier and for ##[1:N] may be N cycles earlier. §15's waveform is this exact confusion.

2 — Confirm the trigger was semantically valid. Did the event the antecedent names actually occur, in the sense the contract means? A valid used as an accept (§14) fires on correct hardware, and step 2 is where that is discovered rather than after a day of RTL reading.

3 — Inspect the sampled values, not the waveform values. §7. A registered signal updated at the failing edge reads as its previous value. Most "the waveform disagrees" reports end here.

4 — Check the reset and disable state. Was the property enabled? Was it enabled at the arming cycle and at the checking cycle? §40's anti-pattern is found by asking whether the disable condition overlaps the window.

5 — Check for overlapping attempts. Did the trigger fire on several consecutive cycles? Which attempt failed? With local variables, each attempt carries different captured values, and the failing one may not be the most recent.

6 — Check the assumptions. In formal, is an assume too weak — permitting an environment the real system never produces? In simulation, is the environment doing something illegal that the property correctly objects to? 20.1 §29's boundary.

7 — Find the first cycle at which anything diverged. Not the first assertion failure — the first divergence, across all properties and all models. A cascade produces many failures with one cause (20.1 §60).

8 — Only now inspect the design. By this point the finding is specific: an event at a cycle, a value that was wrong, a promise that was broken.

Steps 1 to 6 are all about the assertion. That ordering is deliberate, because a property is far more often wrong than the design it constrains — especially a new property, and especially one whose first run produced a failure.

65. Negative Testing of Assertions

A property that has never been observed to fail may be unbound, vacuous, permanently disabled, or wrong.

The procedure, per property:

1. Construct a stimulus or a forced condition that violates it. 2. Confirm the property fails, at the expected cycle, with a readable message. 3. Confirm no other property fires — or, if others do, that they are genuine consequences and are understood. 4. Remove the violation and confirm the property passes. 5. Record, in the inventory (§68), that the property has been demonstrated to fire.

Three notes.

Step 3 is the one that finds over-constrained properties. A single injected violation that trips eleven properties means ten of them are either redundant or coupled to the same signal. That is worth knowing before a real failure produces eleven simultaneous reports.

Step 5 is what makes the inventory trustworthy. A property column reading "demonstrated: yes" is evidence; a property with no such record is a hypothesis.

And this is not optional work at the end. The cheapest moment to demonstrate a property fires is the moment it is written, when the author still knows what should violate it.

66. Mutation Testing

Deliberately break the design, confirm the assertion set catches it, and revert. Mutation is the direct measurement of whether the properties are worth anything.

Three rules.

A mutation that no property catches is a gap, and the finding is the gap rather than the mutation. Write the missing property.

A mutation caught by only one property is a single point of failure — if that property is later disabled or scoped away, the bug becomes invisible. Row 6 is exactly this, and §40 is how that single property gets disabled.

And no mutation is ever left in the repository. They are applied, measured and reverted in a scratch branch or a build-time define — never committed, because a mutation that survives into a release is a defect somebody deliberately introduced.

67. Activation Coverage

The minimum coverage this chapter requires — the full functional model is 20.5's.

// One cover per implication antecedent (§48), plus the scenario covers that
// make the interesting properties non-vacuous.
 
// Antecedent activation — the vacuity defence.
c_accept:            cover property (@(posedge clk) accept);
c_stall:             cover property (@(posedge clk) (valid && !ready));
c_consume:           cover property (@(posedge clk) (consume_units != '0));
c_return:            cover property (@(posedge clk) return_fire);
c_stale_return:      cover property (@(posedge clk)
                       (return_valid && (return_epoch != chk_credit_epoch)));
c_recovery_entry:    cover property (@(posedge clk) recovery_entry);
c_cfg_commit:        cover property (@(posedge clk) cfg_commit);
c_bad_verdict:       cover property (@(posedge clk)
                       (verdict_valid && !verdict_good));
c_repeat_attempt:    cover property (@(posedge clk)
                       (attempt_fire && (attempt_num > 1)));
 
// Scenario covers — the SPECIFIC combinations that make properties meaningful.
c_recovery_with_work: cover property (@(posedge clk)
                        (recovery_entry && (chk_outstanding != 0)));
c_simultaneous_cr:    cover property (@(posedge clk)
                        ((consume_units != '0) && (return_units != '0)));
c_reuse_after_retire: cover property (@(posedge clk)
                        retire_fire ##[1:2] (alloc_accept && (alloc_id == $past(retire_id))));
c_stall_then_accept:  cover property (@(posedge clk)
                        (valid && !ready)[*4] ##1 accept);