Convergence Interview Questions

First work out which of three causes it is. The depth needed is huge, the cone holds hard logic such as a multiplier, or the property is not inductive. Read the cone and the engine log rather than guessing. Then change the question to match. Abstract the counter, cut datapath the property does not read, add helper invariants, split cases or switch engines. Every reduction gets a written reason and a rerun of a known-buggy version.

Reaching expiry from reset takes as many steps as the count. BMC must unroll every one of them, so the required depth runs into the tens of thousands. Instead, abstract the counter to the few values that matter and prove the abstraction on the real counter in a side run. A one-transition property can also be proven by induction at full width without ever reaching expiry.

The abstract counter can do everything the real one does, plus more, such as expiring early. So a pass on the abstract model holds for the real design. The extra behaviour can cause false failures, for example an early timeout. Check each failure against the real counter, and prove the values you kept on the real design.

A blackbox turns every output of a module into a free input. That suits memories and arithmetic the property does not depend on. A cut point frees a single internal node. So you can remove one hard cone, such as a CRC check, without dropping the module around it. Both add behaviour, so a pass stays sound and a failure must be checked at the freed signal.

Run the proof once per case, each with an assumption that pins the case variable. Prove separately that the cases together cover every value. Pin the case for the whole run, from a value fixed at the start. A split that lets the case change each cycle can hide interleavings between cases. The slow case then shows you where the hard logic is.

Agree on a few habits before RTL is written. These are right-sized state, control separated from data, parameterised timers and depths, one reset, and important state exposed or named. Show one measured before-and-after from your own project, because that persuades more than a rule. Designers who run formal on fresh RTL also find bugs while they still remember the code.

Freeing a signal lets it take any value, so the cut model has every behaviour of the real design and more. A pass on the cut model is therefore a real pass, but a failure may be one the cut invented. Check each failure at the freed signal. If no real logic could produce that value there, add an assumption that restores the fact. Then prove that assumption on the uncut logic.

The replacement was not a superset of the real logic. Something narrowed it. Typically that is an assumption added to silence a false failure, or a model that leaves out a legal case. A sound abstraction must keep every concrete behaviour. The unreached cover is the evidence; fix the abstraction, not the cover.

A cut only adds behaviour, so a pass on the cut model still holds for the real design. An assumption on the cut signal removes behaviour again. If it removes something the real logic can do, a real bug disappears. So prove each such assumption on the uncut logic in a side run.

Look at the freed signal in the trace. If the real logic could produce that value from the trace's inputs, the failure is real. Running the uncut design to the same step confirms it. If not, the cut invented it, and you either restore the missing fact with a proven assumption or choose a different cut.

Prove each block's guarantee while assuming the other's, then compose. For safety this is sound when each assumption is only needed for earlier cycles, not the current one. If each block assumes the other's guarantee in the same cycle, the proofs lean on each other. Both can then pass with a real bug. In the lesson's credit link the circular version passes; assuming only last cycle's guarantees finds the bug.

It turns the pair of proofs into induction over time. At reset both guarantees hold. Suppose both held up to cycle t minus one. Then each block's proof shows its own guarantee at cycle t, so both hold at t. A same-cycle assumption breaks that chain, because each guarantee at t would rest on the other at t.

Block A assumes B sends good data this cycle, and B assumes the same of A. Suppose both send bad data in the same cycle. Each proof rules that case out by its own assumption, so both pass. The time shift breaks the circle, because cycle t then rests only on cycle t minus one.

Write one contract per boundary from the interface spec. Prove each block against the contracts of its neighbours, assumed with the time-shift rule. Each contract is asserted on its owner and bound into system simulation as a check. The end-to-end goals that cross several blocks then rest on proven contracts, and a contract change triggers a review of both sides.