Safety versus liveness?

Safety says nothing bad happens on any prefix; liveness says something good happens on every infinite trace. Starvation is a liveness failure, overflow is a safety failure.

Proving eventually with a bounded run.

Safety and liveness

Why is bounded response a safety property?

Waiting too long is decided on a finite prefix: the trace already violates the window. True eventually needs an infinite loop to fail.

Calling a windowed check a liveness proof.

Bounded response is safety

What is a lasso counterexample?

A finite prefix plus a loop the trace repeats for ever, showing the good event never arrives. Bounded runs cannot produce one; they can only miss the window.

Showing a long finite trace as a liveness refutation.

Lasso counterexamples

Where does fairness live?

On environment choices only: requesters persist, holders finish. Never on design outputs, where it would assume the answer.

Assuming the grant to prove the grant.

Fairness and what you may assume

Weak versus strong, in one line?

Strong forms demand the event; weak forms tolerate the trace ending first. A bounded response is a safety property: written as a sequence it is weak unless wrapped in strong, and the counter form needs no such choice.

Offering a weak eventuality as a proof.

Weak and strong

Overlapped versus non-overlapped implication?

Overlapped checks the consequent in the same cycle as the antecedent; non-overlapped in the next. State the cycle of the consequent explicitly in the runnable form.

Being off by one on the response cycle.

Overlapped and non-overlapped

What runs in the open flow?

Boolean assertions with sampled history: past, rose, fell, stable, plus free inputs and free constants. Implication operators and sequences are concept-only and always paired with the Boolean form.

Showing only the unrunnable form.

Textbook SVA to Boolean past

What does sampled history check?

The relation between the present cycle and named past cycles, with a guard skipping the cycle after reset. History before the first cycle is undefined, so the guard is load-bearing.

Unguarded history failing the good design at step 2.

Past gating and history windows

One-to-one request and response?

Track the item or count it: a symbolic tag or a counter ties each grant to its request. A lone next-cycle implication cannot match pairs.

Asserting pairing with a single implication.

Symbolic constants and tracked items

Stable-until-grant, correctly?

The request holds and the address holds until the grant arrives, checked every cycle of the wait. One stable check covers one cycle only.

Checking stability once for a multi-cycle wait.

Stable until the handshake

Edge or level: rose or high?

The edge form fires once on the rising request; the level form fires on every cycle the request is high. Most handshake properties want the edge.

Firing the property on every high cycle.

Every cycle versus rose

Starvation versus deadlock versus livelock?

Starvation serves some and never one; deadlock serves none with a cycle of waits; livelock moves without completing. Different shapes, different proofs, different fixes.

One cure for all three hangs.

Defined once, precisely