Signoff Interview Questions

Each of four items needs evidence. Every assumption has a spec reason and a cover reachable under it. The properties map to spec rows, and a mutation sample shows they notice faults. Each result is a full proof, or a bounded pass next to the depth the counters and transactions require. A cone map names the logic no property reads, and every line carries the tool version and date.

Start from the deepest counter in the property's cone, the longest transaction and the property's own window. Then add the tool's step offset. Check the number with covers: the deepest interesting behaviour must be reached inside the bound. The book's guideline is to prove assertions deeper than the longest cover trace, ideally about twice as deep.

The number is only as good as its inputs. A counter you missed in the cone, a longer transaction or a wrong step offset makes 30 too small. Covers check it: the deepest interesting state must be reached inside the bound. A depth sweep, where a planted bug fails near the predicted depth, also checks the arithmetic.

A proof covers its property's cone of influence, the logic that can affect it, and nothing else. Draw the union of all cones: logic outside it is unverified, not wrong, and belongs in the review. The proof core is the part of the cone the engine actually used, and cutting registers one at a time measures it. Cover depths add a time view: a bounded run below the deepest cover never saw that behaviour.

The checklist puts one spec rule per row with its property, so an empty cell is a visible hole. But it trusts that each property is strong enough. Mutation changes the design on purpose and asks whether some property fails; survivors grouped by behaviour name the missing properties. In the lesson's FIFO campaign, bookkeeping properties killed 24 of 39 mutations, and adding an order property raised it to 38.

Run an equivalence check between the mutated design and the original. If they are equivalent, the mutation changed nothing visible, so it is harmless. If not, the check gives a trace where they differ. That trace names the behaviour no property watches, so write the missing property from it.

Write it before the properties. It names scope, goal, spec rows, properties, assumptions, covers, abstractions, a depth budget and sign-off criteria. Every assumption names who checks it at system level, and every bounded result sits next to its required depth. One empty field can turn an honest open item into a false sign-off.

Rank blocks by where formal pays: control-heavy logic with deep corners and clean interfaces. Examples are arbiters, credit logic, FIFOs, register blocks and protocol bridges. Give each block a goal, bug hunting or sign-off, because the exit criteria differ. Run the cheap apps across the subsystem early, plan abstractions and depth budgets per block, and bind every assumption into simulation. Track proofs, bounded results and open UNKNOWNs as a risk list.

Bug hunting aims to find failures fast. So it accepts over-constraints, shallow bounds and partial property sets, and it ends when the bug rate drops. Sign-off claims the block is correct against its spec. So it needs complete properties, justified assumptions with covers, and proofs or argued bounds. Mixing the two leads to a bug-hunting bench presented as a sign-off.

Decide per property, early. Try abstraction and decomposition first, within a time box. If that fails, ship a bounded result with its required depth and covers. Move the remaining risk to targeted simulation or emulation tests. Record the decision and its residual risk in the sign-off, so nobody reads the block as fully proven.

Yes, if the bound is argued, not hoped. The page must show the required depth from the counters and transactions, and a run that reaches it. It must also show covers of the deepest behaviour inside the bound. The page reports the result as bounded, with the depth, the tool version and the date. It also states the risk of a deeper bug.

Split by question, not by team. Formal takes control logic whose rules fit in a few cycles: protocol compliance, arbitration, FIFO and credit invariants, registers, connectivity and deadlock. Simulation keeps data flows across many blocks, long scenarios, performance and firmware interaction. Every formal assumption is also bound into simulation as an assertion, so a wrong assumption is caught at system level.

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.

Start with one-cycle safety: at most one grant, and no grant without a request. Then pin the rotation: after granting requester i, the pointer moves just past i. Finally fairness: assuming requests hold until granted, every request is granted within a bounded number of cycles. Cover each requester being granted and a full round of grants.

Fairness is checked with bench counters that count how long each request has waited. In the induction step those counters may start at any value the property allows, including combinations no real run produces. A longer window, k = 6 here, rules those starts out, while PDR finds the needed invariant by itself.

Starvation: a low-priority requester can wait forever while higher ones keep asking. Safety properties cannot see that, because no single cycle is wrong. You need a liveness property under fairness, or a bounded wait under a named stand-in assumption. Take the bound for the wait from a measured cover.

A random-request bench with a reference model and grant-latency checks finds most bugs quickly. What it misses are skips and starvation that need a specific multi-cycle pattern of requests. Random stimulus rarely produces that exact pattern. Formal finds such patterns in a few steps, which is why arbiters are a classic first formal target.

A simulation is one path. A million cycles visit at most a million states, out of up to 2 to the power of the flop count. BMC at depth k reasons about every input sequence of length k from reset in one solver query. The solver picks the inputs that break the property, so a rare three-cycle pattern costs it nothing extra.

A strong answer names the block and its spec rows, then the property kinds: end-to-end checks, glue invariants and covers. It lists each assumption with its source and how the system checks it. It names the convergence problem and the technique that solved it. It ends with the evidence for done: full or bounded with the required depth, reached covers, and a fault-injection or mutation result.

The failing step, the cause, and the fix, in that order, plus the causes you ruled out and how. Say whether it is an RTL bug, a missing assumption, a wrong property or an unmodelled reset. Point at the signal and step that decided it. Thinking aloud in that structure matters more than reaching the answer first.

A good story names the assumption, why it seemed right, and the evidence that broke it. That evidence might be an unreached cover, a bound assertion firing in system simulation, or a lab failure. It ends with what changed in the process, such as covers per assumption or binding assumptions into simulation from day one.

Give every assumption a written reason from the spec and a cover that must stay reached. Bind every block assumption into system simulation as an assertion from day one. Review the list at each milestone with someone from the neighbouring block. Then a wrong assumption shows up early, as a firing check or an unreached cover.

Keep it alive. When the lab reports a symptom, write it as a cover and the lab observations as assumptions. The shortest trace is a hypothesis for the root cause. Never assume away what the lab did not observe, since it may be the cause. Then prove the fix under the same environment before the respin.