Proof Engines Interview Questions

Not necessarily a bug. The induction step may start from any state where the property held for k cycles, including states reset never reaches. Read step 0 of the induction trace and name what is impossible about it. Assert that relation as a helper and rerun until the step passes. Raising k may never close the proof, while one good helper often does.

The step only assumes the property held for k consecutive cycles; it says nothing about reachability. A state can satisfy the property but break a hidden invariant, such as two equal counters being unequal. Such a state is a legal start. The fix is to make the hidden invariant part of what is proven, so those states are ruled out.

Raising k makes the step assume the property held for more cycles. That works only when every bad start state reaches a failure within k cycles. Two counters that must stay equal can drift apart and stay apart for any number of cycles. Then no k closes the proof; only a helper that states the invariant does.

IC3/PDR does not unroll but keeps frames of clauses. It proves each clause relative to the previous frame until two frames match, giving an inductive invariant it built itself. On the lesson's 16-entry FIFO, PDR proves the property with no helpers while k-induction stays UNKNOWN at k = 12. Its counterexamples start at reset but need not be the shortest. No engine wins everywhere, so teams race several.

Every helper is asserted, so it is proven, never assumed. Keep only the helpers the final proof needs, by removing them one at a time and rerunning. After each change, rerun a faulty version of the design to show the set still catches the bug. Review helpers like RTL, because they become the next engineer's spec of the block.

BMC unrolls the design k times from the initial state. It asks a SAT or SMT solver whether some input assignment reaches a bad state at any step. Satisfiable means yes, and the assignment is the counterexample trace. Unsatisfiable means no trace of that length breaks the property, which is the good news. Depths are tried in order, so the first failure found is a shortest one.

The checker asks about depth 1, then 2, then 3, and stops at the first depth the solver finds satisfiable. If a shorter failing trace existed, an earlier query would already have been satisfiable. That makes BMC traces short and easy to read, which is one reason engineers run bmc for bug hunting.

A SAT engine sees only gates, so a wide adder or multiplier becomes thousands of clauses. An SMT solver keeps words and arithmetic as theories and can simplify before it falls back to bits. The verdict is the same either way; only the time differs, and in the lesson the winner changed with the property.

Yes: if every reachable state can be reached within d steps, a BMC pass to that depth covers every reachable state. The problem is that nobody knows the diameter of a real design, and it grows with every counter. That is why full proofs use induction or IC3/PDR, an engine that builds its own invariant. Bounded results are argued from a required depth instead.

Prove mode runs k-induction (an induction proof over k steps) or IC3/PDR (an engine that builds its own invariant). It can return a PASS that holds for all time. UNKNOWN means the base case passed but the induction step did not, so no proof has been found. It is an open item, never a pass, and it can sit on a real bug deeper than the base case. On the buggy idle timer here, prove at k = 2 reports UNKNOWN rather than FAIL.