Assertions — Executable Statements About Ownership Over Time

Chapter 24.1 said what must be verified. This chapter proves the part that can be proven locally, at the interface or state boundary where the rule actually lives.

And it starts somewhere unexpected. Not with $rose, not with |=>, but with a question you must answer before writing a property:

Who owns this item right now, and what event transfers it?

Every strong PCIe assertion in this chapter is an answer to that question. The temporal operators are how you write the answer down.

1. Sources, Scope, and What the Language Tracks Already Own

2. An Assertion Is a Statement About Ownership Over Time

Take a real rule from Chapter 23.4: a packet's header must not change while the packet is being sent.

The naive translation reaches for operators first — something with $stable and |=>. The useful translation answers four questions first:

What became true?      the generator accepted a request
Who owns the item?     the packet owner, exclusively
What must stay true?   every header field
What transfers it?     the ACCEPTED end-of-packet beat

Only now is the property mechanical:

(owner_lock && $past(owner_lock)) |-> $stable(pkt.addr)

And the four answers also tell you what would be wrong. Releasing on tx_last asserted rather than accepted changes the fourth answer, so the property must be qualified by the transfer — which is why Chapter 23.4 §11's P20 exists as a separate property from P3.

This is why the chapter is organized by contract rather than by operator. Eight shapes, eight property families, and the operators fall out.

3. Eight Shapes of a Protocol Rule

Two practical consequences.

The shape determines the skeleton. A held-state contract is always owned |-> $stable(...). A conservation rule is always combinational and needs no temporal operator at all — and people write it as a sequence anyway, which is harder to read and no stronger.

And the shape determines what a failure means. A conservation failure means ownership was lost somewhere and the specific place is unknown; a matching failure names the transaction. §18's debugging works by moving from the shape that fired to the shape that is upstream of it.

4. assert, assume, cover — and the Pass That Proves Nothing

5. Sampling, $past, and the Same-Cycle Question

The SystemVerilog track owns the timing model. What is PCIe-specific is which coincidences you will actually meet — and Modules 22 and 23 measured all of them.

The single most important one: a Tag freed and allocated in the same cycle (23.3 §7, measured at a 6.3% divergence between the two implementations).

A property written on the sampled previous state answers a different question than one written on the next-state expression:

// Reads the bitmap BEFORE this cycle's free and allocate.
(alloc_fire) |-> $past(free_map)[tag_grant]
 
// Reads the value the design will actually have.
(alloc_fire) |=> !free_map[$past(tag_grant)]

Both are legitimate; they assert different things. The first says the allocator picked something that was free at the sampling point; the second says the pool reflects the allocation afterwards. A design using the next-state form (which 23.6 pattern 9 recommends) will fail the first property while being correct — because the freed Tag was not free at the sampling point and is legitimately allocatable.

The rule this chapter follows: assert the invariant, not the implementation. Conservation (FREE + LIVE == TOTAL, §13) holds under both implementations and catches the two-branch bitmap that loses a write. It is the property to reach for when the same-cycle behaviour is a design choice rather than a protocol rule.

6. Property Set 1 — Stream Ownership

7. Property Set 2 — Snapshot Immutability

8. Property Set 3 — Tag Allocator

9. Property Set 4 — Request and Completion Lifetime

10. Property Set 5 — Credit Ownership

11. Property Set 6 — Packet Lock

12. Property Set 7 — Link State, Bounded Deliberately

13. Property Set 8 — Conservation and Ghost State

14. Binding — Keeping Verification Out of the RTL

15. The Waveform

Four things to read out of the figure.

The defect is at cycle 3 and the report is at cycle 4. A concurrent assertion evaluates on sampled values, so $stable compares this edge against the previous one — the reported cycle is always one after the change, and a debugger who looks only at the reported cycle sees a stable payload and concludes the assertion is wrong.

assert_good never rises. The corrected trace holds the payload across cycles 2–4 and transfers at cycle 5, which is the same bytes delivered one cycle later.

Cycle 5 is the transfer, and only there may the payload change (cycle 7 shows the next item).

And nothing fires in cycles 0–1. The antecedent valid && !ready is not met, which is precisely why §6's cover property exists — on a bench with no stalls this waveform never happens and the property is green and meaningless.

16. Measured Behaviour

17. Verification — Mutations

Each mutation names the property family that catches it. Entries marked review are defects no property can catch, because the property itself is the defect.

Two counterexamples worth stating explicitly.

Mutation 37 is the one that makes a formal sign-off worthless. Adding assume property (tag_free_map != '0) to help convergence tells the tool the Tag pool never empties. Every property then proves, including the ones that would have caught Chapter 23.3 §14's leak — a leak whose entire symptom is the pool emptying. The assumption did not model the environment; it deleted the bug, and the resulting proof is a statement about a design that does not exist.

Mutation 40 is the most common defect in real assertion suites and it produces no failure at all. A property file with forty implications and no cover properties reports forty passes on a testbench that never stalls, never exhausts credits, and never splits a Completion. §16 measured the difference at 60,205 antecedent hits versus 0 — and the assertion report is byte-identical. The fix costs one cover property per family, which is why every family in §6–§13 carries one.

18. Debugging Assertions

Symptom — the assertion fires only when ready is low. That is the property working, not a false failure (§15). Stability, no-reneging and transfer-accounting properties all have !ready in their antecedent by construction. The bug is real and load-dependent — which Chapter 24.1 §7 measured as the signature of every ownership defect in Modules 22–23.

Symptom — a known bug exists and no assertion fires. Check reachability before checking the property (§4). Read the cover properties: if the antecedent count is zero, the property was never evaluated. §16 measured a property passing with 0 antecedent hits, indistinguishable in the report from one with 60,205.

Symptom — formal cannot prove a property and does not produce a counterexample. Two causes and they need opposite fixes. An unbounded liveness property (§9's eventual-Completion) has no bounded proof — remove it and move the question to the scoreboard's residue check. Or a missing environment assumption leaves the tool free to hold ready low forever; the fix is an assume on the environment, never on a DUT output (mutation 37).

Symptom — the property fails in the first cycles after reset release. Usually $past with insufficient history, or a disable iff window that ends before the design has settled. The fix is not to widen disable iff — that masks real cycles (mutation 39). Qualify the property with a "design has been out of reset for N cycles" term, so the masking is explicit and bounded.

Symptom — a same-cycle Tag free and allocate reports a mismatch. Check which form the property asserts (§5). A property on $past(free_map) fails a correct next-state implementation, because the freed Tag was not free at the sampling point. Assert conservation (P17) instead, which is true of both implementations and false only of the two-branch bitmap that loses a write.

Symptom — one instance of a checker fails and identical instances pass. Parameter or bind mismatch (§14, mutations 33, 34). Compare the elaborated parameter values per instance. A checker bound with a narrower width compares a truncated payload and passes, so the passing instances are the suspicious ones.

Symptom — the assertion fires far downstream of where you believe the bug is. Move the property upstream toward the first violated contract. A malformed-TLP checker at the Link fires because a header field changed at the generator (§7); a scoreboard mismatch fires because a Tag was misattributed at the matcher (§9). The eight shapes of §3 give the ordering: matching and held-state failures are upstream of conservation failures, which are upstream of "the output is wrong."

Symptom — the checker itself changes the design's behaviour. Any checker that drives, gates, or is read by functional logic (mutation 43). In simulation this shows as a bug that disappears when assertions are compiled out, which is the fastest way to identify it.

19. Misconceptions

"An assertion is a syntax exercise." It is a statement about ownership over time; the operators are how you write it down (§2).

"All assertions passed, so the design is verified." They may all be vacuous — 60,205 versus 0 antecedent hits, both reported as passes (§16).

"A cover property is optional documentation." It is the only evidence an implication was ever evaluated (§4).

"assume makes formal converge, so add more." An assumption on a DUT output deletes the bug and proves a design that does not exist (mutation 37).

"Assert that every request eventually completes." That is the environment's obligation, not the DUT's (§9).

"Completions must arrive in request order." No ordering is implied between different transactions (13.3 §2, mutation 42).

"disable iff (!rst_n) is always right." Only for the reset window; widening it masks the interesting cycles (mutation 39).

"The assertion reports the wrong cycle." It reports the sampling edge after the change — that is the timing model, not a defect (§15).

"Write the property against the internal signal; it's more precise." It breaks on every refactor; bind to the interface contract (§14).

"One bind covers everything." It covers every instance of that module type, including ones you did not mean (§14).

"Conservation is too weak to be useful." It holds under every correct implementation of a same-cycle choice and fails only on the real bug (§5, P17).

"Ghost state is cheating." It is how an invariant that spans transactions becomes expressible — provided it is driven from observations, not from the DUT (§13).

"We should assert the full LTSSM." Not from memory. A fabricated transition rule fails on legal behaviour and gets the checker waived (§12).

20. Understanding Check

Q1. Your entire PCIe property file passes on the first run. What is the first thing you check, and why is it not the design? The cover properties. §16 measured an implication passing with 0 antecedent hits, reported identically to one with 60,205. A first-run all-pass on a new property file is far more likely to mean the stimulus never reached the antecedents — no stalls, no credit exhaustion, no split Completions — than that the design is perfect (§4).

Q2. Formal will not converge on "every Memory Read is eventually completed." What is wrong with the property? It asserts a liveness obligation the DUT cannot discharge (§9). The DUT does not make Completions arrive; the environment does. The decomposition is to assume the environment returns Completions and assert the DUT handles them correctly — and to move "did anything never complete?" to the scoreboard's end-of-test residue check (24.3).

Q3. A Tag is freed and allocated in the same cycle, and your property alloc_fire |-> $past(free_map)[tag_grant] fails. Is the design broken? Probably not. A next-state implementation (23.6 pattern 9) makes the freed Tag allocatable in that same cycle, so it was not free at the sampling point — the property pins an implementation choice rather than a protocol rule (§5). Assert conservation instead (P17): it holds for both implementations and fails only on the two-branch bitmap that actually loses a write.

Q4. Why does this chapter write seven separate header-stability properties instead of one $stable(pkt)? So a failure names the field that moved (23.4 §11's rationale, §7 here). $stable(pkt) tells you the packet changed; p_hdr_identity_stable tells you the Tag changed, which points directly at the request-acceptance path rather than at the address computation. The cost is six extra lines and the benefit is skipping a debugging session.

Q5. You add assume property (avail_data[0] > 0) to help a proof converge. What have you actually proven? That the design is correct when data credits never run out — which is the one condition under which the credit properties are trivially satisfiable (§4, mutation 37). The starvation behaviour Chapter 22.3 exists to describe has been assumed away, and the proof is a statement about a system that has infinite receiver buffering.

Q6. Which property in this chapter would you write first for a brand-new PCIe requester, and why? Conservation — P17 and P46. They need no protocol knowledge, no reachability argument, and they detect both failure modes of the ownership law: a resource owned twice and a resource owned by nobody (23.6 §15). They are also the properties least likely to be vacuous, because they are invariants rather than implications — there is no antecedent to miss.

21. What's Next

Assertions prove what is provable locally. Every property in this chapter fits inside one interface, one allocator, one arbiter, or one credit pool — and that is their limit.

Chapter 24.3 Scoreboards takes the questions SVA cannot answer: which transaction lost bytes, whether Completions arriving out of order were the right Completions, and whether anything was left outstanding when the test ended. §13's ghost counters catch that bytes were lost; the scoreboard names the transaction.

24.4 Coverage then answers the question §4 kept raising — how do you know the stimulus reached the antecedents? Cover properties answer it one property at a time; a coverage model answers it for the campaign.

24.5 VIP and 24.6 UVM Architecture then place all of this inside an environment, and 24.7 Error Injection builds the stimulus that makes §10's and §12's antecedents reachable in the first place — the credit exhaustion, the replay, the malformed packet. This chapter deliberately wrote no injection machinery.