What is the cone of influence?

Exactly the logic that can affect the property: reduction to it is exact and never over-constrains. Over-constraint comes from assumptions or unsound abstraction, never from the cone.

Blaming the cone for a vacuous pass.

COI reduction is exact

What justifies data independence?

No control path from the data values: the block moves words without looking at them. Proved by inspection of the control fan-in or broken explicitly per relevant bit.

Abstracting data the control branches on.

Data independence

Counter too wide to bound?

Replace it with a saturating counter at a small threshold and prove behaviour identical below it, or prove the real counter by induction. The 32-bit timeout becomes 2 bits with a bound of 5.

Bounding below the behaviour and filing it.

Counters and widths

Memory too large to include?

Track one symbolic address with a shadow value and a valid bit: 41 bits stand in for 8192. Constrain the address to the legal map and cover each region.

An unconstrained address hiding failures.

Memory and tracked entry

What is a sound cut point?

A signal replaced by a free variable plus a contract proved on the real driver. The contract travels with the proof; replaying the trace on the unabstracted design checks it.

A free cut with no contract.

Cut points

When is symmetry sound?

When requesters are interchangeable in the property and the design treats them uniformly. Prove one, argue the mapping, and mutate a second to check the uniformity.

Assuming symmetry the arbiter does not have.

Arbiter grant latency proof

What does a miter prove?

That two implementations agree on every checked input from a common reset, mode by mode. Never that either is correct; the spec proof still has to exist.

Shipping on agreement alone.

Miter construction

Retimed logic fails equivalence: setup or real?

First suspect the state mapping: retiming moves registers across logic, so the outputs agree but the internal registers differ. Prove equal outputs with the cut invariant or a larger k, not equal internal state.

Demanding equal internal state instead of equal outputs plus the cut invariant.

Retiming and the limits of LEC

An ECO touches one mode: what proves it?

Per-mode miters with the constraint listed on each run, plus the intended-difference property pinning the change to its mode. The untouched modes must still prove equal.

One constrained run waiving the rest.

ECO equivalence flow

What closes a formal signoff?

Proven or bounded-with-justification for every property, reached covers, reviewed assumptions each discharged, cone coverage, mutation results, rerun on the final hash, waivers with reasons.

Not-failed counted as proven.

The signoff checklist

What does formal own in a CDC signoff?

Protocol checks of the crossing with the synchroniser abstracted, not structural analysis. Metastability and structural rules belong to their own checks.

Proving the synchroniser safe in the open flow.

Formal in CDC and CPU flows

What does the CSR proof cover?

Reset values, read-write behaviour, write-1-to-clear with hardware-set priority, read-only registers ignoring writes, and isolation between registers. Access timing matches the wait states: same cycle with none.

Checking data without the access rules.

W1C, read-only and reset values