Revision sheet drawn from the course. Outcomes use the course vocabulary only. Every design number is a teaching value from the running designs; none is a target for any real product or process.
Outcome | Say | Never say | Next |
|---|---|---|---|
Proven | Holds for the stated model under the stated assumptions. | Closed, green, converged. | File with the assumptions and the revision. |
Counterexample | Concrete trace, earliest failing cycle named. | Spurious until classified. | Triage: legal start, assumption, artefact, bug. |
Inconclusive | Undecided: time ran out, the induction step failed from an unreachable start, or the bound was reached with no counterexample. | Pass, nearly proven. | Justify N or strengthen to an induction; diagnose, then reduce, split or strengthen. |
Bounded to N is how a bounded pass is written: no counterexample within N cycles, never "proved to N". It is reported under inconclusive.
Rule | Directive | Side |
|---|---|---|
Environment behaviour the block depends on | Assume | Inputs only, never design outputs. |
Behaviour the block owes its neighbour | Assert | Outputs only, never raw inputs. |
Every implication trigger | Cover and reach | One witness per antecedent. |
Ordinary traffic: grants, stalls, contention | Cover and reach | Unreached activity is a failure with an owner. |
A cover not reached within N is inconclusive; only a proved invariant makes it unreachable.
State the invariant: true in every reachable state, or say which states you exclude and why.
Base case: it holds in the first k states from reset. Read the base status, not only the step.
Step: any k consecutive states satisfying it imply it in the next. The step starts anywhere, including unreachable states.
On a failing step, read the CTI: spurious means strengthen with a helper, real means fix the design or the property.
Prove every helper. An assumed helper is a false pass waiting to happen.
A helper that is false on a reachable state fails its own base case once the depth reaches that state; at a shallower depth it shows up as a failing step. A helper that is too weak fails the step. Read the helper's own status first, and change one side at a time.
CTI starts in | Reading | Fix |
|---|---|---|
A reachable state | Real: the property breaks on a legal path. | Fix the design or the property; keep the trace. |
An unreachable state, property still true there | Spurious: the step is stronger than reality. | Add a helper invariant excluding the region; prove it. |
Any k-window longer than the chain, enable held low | No k decides it: the window can repeat one unreachable state for ever (never-15 on the decade counter, measured to k = 20). | Strengthen with a helper that excludes the region, do not raise k; a simple-path constraint helps only when states cannot repeat. |
A state the assumptions should exclude | Missing or wrong assumption. | Repair the assumption, discharge it, reprove. |
Want | Write | Note |
|---|---|---|
Response within N cycles | Counter from the trigger; assert below N. | Safety. State N and its source. |
Grant under contention | Bounded wait with the stall bound assumed. | Fairness on the environment only. |
Eventual response, unbounded | Liveness engine with fairness (concept here); the runnable substitute is bounded response with a stated N. | A bounded run cannot refute the unbounded form. |
No starvation | One bounded-wait property per requester. | Averages prove nothing; each waiter needs its own. |
Progress in a chain | Bounded progress under bounded stalls. | Structural cycle first, temporal proof after. |
If | Use | Sound when |
|---|---|---|
Property ignores a block | Cone reduction. | Always: it is exact, never over-constraining. |
Control never looks at data | One tracked item or bit. | No control path from data, or the bits kept. |
Counter threshold is the cost | Small saturating threshold. | Logic identical across thresholds, decided by induction. |
Memory dominates the state | One tracked address and shadow value. | Addresses constrained and covered per region. |
A stage dominates the cone | Cut point with a contract. | Neighbour proves the contract; replay kills artefacts. |
One case dominates depth | Case split with coverage of cases. | Cases proved to cover everything. |
# not-run: concept pairs for review; the Boolean forms are the ones the runnable front end reads
overlapped: req |-> resp checks resp in the SAME cycle as req
boolean form: !req || resp same cycle, runnable
non-overlapped: req |=> resp checks resp ONE cycle after req
boolean form: !$past(req) || $past(rst) || resp
one cycle later; the history gate skips the reset cycle
stable until grant is NOT one cycle:
edge form: $rose(req) |=> $stable(addr) checks one cycle only
level form: (req && !gnt) |=> $stable(addr) holds every waiting cycle
boolean, edge: !($past(req) && !$past(req, 2)) || $past(rst) || $stable(addr)
checks the first cycle after the rise
boolean, level: !($past(req) && !$past(gnt)) || $past(rst) || $stable(addr)
checks every cycle after a waiting cycle
$past(x, 1, 8) is rejected by the front end used here: the third argument gates, it is not a window.
"within the last N cycles" needs a history register or a counter.The edge and level names describe how many cycles the check covers. The words weak and strong are kept for the operator vocabulary: a weak unbounded obligation never fails while it is still open (finite prefix or loop), a strong one fails it.
An assumption hides the bug: the failing behaviour is assumed away. Activity covers expose it.
Two assumptions contradict: everything proves because nothing is legal. Covers unreached, repair the pair.
Reset held or never sequenced: the proof starts anywhere or runs nowhere. Check the harness first.
History read before it exists: $past without a valid gate fails or passes at cycle zero. Gate it.
The trigger never fires: a vacuous pass. The antecedent cover is the test.
The property is a tautology: a bound the signal can never exceed. A mutant it cannot catch is the test.
The helper is assumed, not proved: the step passes on a lie. Prove every helper.
Fairness sits on a design output: liveness proved by assumption. Fairness constrains the environment only.
A bounded pass read as proven: no justification, no induction. Report bounded to N.
Equivalence read as correctness: two implementations agree and both are wrong. Prove the golden too.
The seven lines are those of the signoff checklist lesson, in its order. Each needs its evidence.
Every property proven, or bounded with justification, or waived with evidence.
All required covers reached, with the witnesses read.
Assumption register reviewed and each assumption discharged.
Cone and mutation coverage reported.
Coverage numbers paired with bounds.
Results tied to the final source hash.
Waivers reviewed with evidence, owners and expiries.
Three checks go with the assumption line and the ledger: no assumption on a design output and no contradictory pair; no helper merely assumed; the ledger consistent by machine check, so the checker prints PASS only when every row agrees. Read The Signoff Checklist in Full before reciting it.
Turn your assumption into an assertion on the neighbour and prove it there: an assume-guarantee contract with no circular dependence, or induction on time where the blocks depend on each other.