The plan on one screen

Stage 6 proves CP-1 with six evidence layers, one conservation rule checked end to end, and a list of mutations that must each fail.

The rule, per epoch: accepted = delivered + explicitly_discarded + in_flight.

CP-1 is one-to-one: each accepted input produces exactly one output, including a poisoned delivered beat, unless coordinated reset explicitly cancels it. Graceful abort drains and has discarded = 0; shared reset classifies each remaining owner once before closing the epoch.

Mutations the bench must catch, each for its intended reason:

• Wrong pointer wrap.

• Dropped valid delay.

• Clear-dominant IRQ.

• One bad ECC syndrome.

• Missing reset handshake.

• A stale-epoch reply.

• Unauthorized discard.

• Poisoned-last metadata misalignment.

Scoreboard flow

Read it as the life of one expected entry. Every path out of the queue updates exactly one term of the rule.

• The key is (recovery_epoch, operation, packet_tag, beat_index), never the tag alone.

• The expected entry holds the numeric result, keep/last and expected status, in order.

• Delivered counts only on the actual output handshake; discard counts only on an authorized cancellation event with owner and reason.

Layer monitors explain mismatches without replacing this end-to-end check.

Worked scoreboard events

Each row is one event; the four numbers always satisfy the rule. The two alternatives after A show that abort never deletes an expectation, while shared reset moves owners to discarded with a reason.

Assertions, coverage and the drain check

• Assertions: bounds, stability through the accepting edge, no overflow/underflow acceptance, command priority, and response deadlines under explicit service assumptions.

• Coverage: full/empty, simultaneous operations, nearest-even ties and saturation, CE/UE, abort with an open packet or stalled output, both idle toggle polarities, clock ratios. Add each selectable arithmetic mode only when its extension is implemented.

• Drain check: stop new offers without withdrawing a pending offer, finish an open packet, then drain under a finite watchdog. PASS requires all expected owners delivered or justified cancelled, no pending offers/responses and all epoch equations closed.

The watchdog diagnostic must list epoch, operation, oldest outstanding key, queue location, accepted/delivered/discarded totals, pending command/snapshot acknowledgement and readiness/fault states. Choose its bound from legal service gaps and clock/CDC budgets; do not merely wait forever for equal counts. Report an expected stalled-peer timeout as the fault scenario's outcome, not normal operation success.

Optional depth: epochs and the framed MAC

Epochs and tag reuse. A CE correction is not another input/output transaction; a poisoned UE delivery is not a discard. Tags restart only after old ownership retires or is cancelled, with a new operation/epoch key; old replies must be rejected, not matched to a reused tag.

Framed MAC extension. An optional framed MAC is not one-to-one. Independently count accepted contributing samples, complete frames, emitted frame results, cancelled partial frames and cancelled completed results. For fixed frame length N, split accepted samples into N*completed_frames + current_partial_samples + explicitly_discarded_partial_samples; separately conserve completed result owners. Do not compare sample count directly to output-frame count or borrow CP-1's scoreboard without changing its cardinality.

Related topics

• Assertions in RTL

• Stage 7: Constraints and implementation