Formal Verification Interview Questions

Simulation checks the paths your stimulus happens to drive, so a rare corner is found only if some test reaches it. Formal treats the inputs as free. It asks a solver whether any input sequence breaks a property, within a bound or for all time. Pick formal for control logic with deep corners such as arbiters, FIFOs, protocol rules and registers. Keep simulation for long end-to-end flows, performance and whole-chip behaviour.

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.

Formal struggles when a property's cone is deep or hard: long counters, wide multipliers, big memories and whole-chip flows. A bounded run then stops short of the behaviour and a proof may never finish. One option is to change the question with cut points, abstraction and smaller parameters. The other is to leave that part to simulation and prove the control logic around it.

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.

The proof was true of what was written, not of what was meant. Common causes are a missing or weak property, or an assumption that removed legal inputs. Others are a bounded result read as a proof, or a bug outside every property's cone. The defences are a spec checklist, covers under the assumptions, a stated required depth and a cone map.

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.

Full formal searches every trace from reset, so a few thousand cycles of depth is out of reach. Semiformal starts the solver from a waypoint instead: a simulation or cover trace that has already run close to the event. It then searches exhaustively from there. It finds deep bugs that neither method finds alone. But it proves nothing about the states it skipped, so it counts as bug hunting, not sign-off.

An assertion is a goal: the tool searches for any legal input sequence that breaks it. An assumption is taken as true, so it removes input sequences from the search. A cover asks the tool to reach a condition and return a trace that does. The working rule is to assume what the environment does, assert what the design does and cover what should be possible.

A cover shows the design moving under your assumptions: reset releases, the FIFO fills, each state is entered. If the bench is over-constrained, the covers come back unreached before any assertion can mislead you with a pass. In this run the arbiter's output is assumed one-hot, and the cover of a double grant is unreached.

A simulator checks an assume exactly like an assert. So the system testbench tells you when the real environment breaks a block-level assumption. Covers are counted as they are hit, and restrict is ignored. Binding block assumptions into system simulation is the cheapest way to validate them.

The real neighbour broke a rule that the block proof relied on. So the block proof does not cover that traffic. Decide from the spec which side is wrong. Either fix the neighbour, or relax the assumption and rerun the proof, which may now fail.

A covergroup bin counts what your tests happened to do. A formal cover asks whether any legal input sequence can reach the condition and returns the shortest trace that does. An unreached formal cover within a bound only says the depth was too short or an assumption blocks it. A proof of the negation is what makes a bin truly unreachable.

It means no input sequence breaks the property within the first 20 steps from reset, and nothing more. A bug that needs a longer run, such as a counter reaching its limit, is invisible at that depth. Either compute the depth the logic needs and show covers reach it, or run a prove mode for an unbounded answer.

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.

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.

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.

Start at the failing step and walk backwards to the first value that set the design on the wrong path. Then sort the cause into one of four: an RTL bug, a missing assumption, a wrong property, or reset not modelled. The state at step 0 and the inputs the solver chose usually decide it. An input sequence the real environment never produces calls for an assumption, not an RTL change.

BMC checks depth 1, then 2, and so on, and stops at the first satisfiable depth, so no shorter failing trace exists. The solver also chooses every input directly instead of waiting for random stimulus to line up. An IC3/PDR counterexample (from the engine that builds its own invariant) starts at reset too but need not be the shortest.

Check how the design starts. A failure that early usually has one of two causes. Either reset was not assumed in the first step, or a flop with no reset started at a value the solver chose. Look at step 0. If a register holds a value reset would never give it, fix the bench or add the reset, not the logic.

Then the start value is an assumption, not a fact. Write it as an initial-state assumption that the register holds its boot value. Put it on the sign-off list, so someone checks it against the boot code. Add a cover that the block still runs, so the assumption did not empty the bench.

A simulation failure is one run, often thousands of cycles long, with the cause buried somewhere in the middle. A formal trace is short and stands for a whole family of failures. If it shows an illegal input, you add an assumption and re-solve. The tool then returns another trace or proves the case is gone, which new random seeds can never tell you.

Expect most early failures to be environment problems, not RTL bugs. Bucket them by cause from step 0 and the solver-chosen inputs, fix reset and missing assumptions first, and rerun; many failures collapse together. Each assumption added is written from a spec row, reviewed, and paired with a cover. Only the failures that survive go to the designer as bugs.

Nothing told the tool how the design starts, so every state, including count = 12, was a legal initial state. Assume reset in the first step, for example if ($initstate) assume(rst), or declare initial values. A flop with no reset or initial value stays a free choice at step 0. The solver picks whichever value breaks the property.

Formal models are two-valued, and silicon powers up to some real 0 or 1 in each flop. Leaving the start value free lets the solver try every possibility in one run. Four-state simulation instead carries an X that if statements can silently resolve, so it may never show the bad value.

All three make the decade counter pass at depth 20 in the lesson. Assuming reset at $initstate checks the real reset logic and is closest to silicon. Declared initial values skip the reset path, so a bug in it can hide. A reset counter models a multi-cycle reset sequence at the cost of a little depth.

Both, about different things. In formal the unreset mode is free at step 0. So the solver picked the value that enables the block before firmware wrote anything. Simulation started mode at one value per run, and a default run never hit the bad one. Either reset the flop, or write the firmware promise as an initial-state assumption and put it on the sign-off list.

X-optimism is RTL simulation resolving an unknown too kindly, so a bug hides. For example, an if on X takes the else branch. X-pessimism is gate-level simulation spreading X further than real hardware would, which floods the run with false unknowns. Formal is two-valued and leaves the value free, so it checks both 0 and 1 and reports the one that breaks a property.

A random initial value is one draw per run. If only a few start values break the rule, most seeds pass. Formal treats the start value as free, so one run checks every value. The solver then picks a value that breaks the property, if one exists.

In this flow an explicit x becomes a free value the solver may choose on every cycle. An assertion that the debug output stays low therefore fails, here at step 2. That is useful. A stray x default in a case statement shows up as a real failure, not a silent simulation quirk.

A safety property says something bad never happens. So a finite trace that reaches the bad state breaks it at a definite step. A liveness property says something good eventually happens. So only an endless trace breaks it: a prefix and a loop where the event never comes. Liveness nearly always needs fairness assumptions, and many teams check a bounded response instead.

With free inputs, the solver can let the environment stall forever, for example by never raising ready. That endless loop breaks the property. Fairness restricts the search to paths where the environment keeps its promise, such as ready returning infinitely often. Every fairness assumption needs a spec reason and a quick check that it is not vacuous.

Deadlock is a reachable state that nothing can leave, so asserting that state never occurs is safety and bmc finds it. Livelock is a loop of states that keeps moving without progress, and starvation is one requester never served while others are. Those two are liveness; to run them in bmc you bound them with a counter and accept the number you chose.

Bounded response is a safety property: it has a failing step, runs in bmc or prove mode and gives readable traces. Its cost is a number the spec may not give, and picking it too large hides slow paths. Liveness needs no number but needs fairness and a liveness engine. Many sign-offs ship the bounded form with the deadline taken from a measured cover.

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.

An assumption deletes every input sequence that breaks it. So an assumption stronger than the real environment deletes legal behaviour along with the bug. The proof is then true of a world the chip never sees. Write assumptions only on ports, from the spec, and pair each with a cover of behaviour it should still allow. An unreached cover is the alarm.

The neighbouring block can only promise things it can see, which are the ports. A rule about internal state is a claim about the design itself, so it should be asserted and proven. Assumed instead, it can quietly delete the very states where the bug lives.

Keep the suspect assumption and replace the assertion with three covers. They are the FIFO full, a push while the count is 16, and a pop while empty. The full and pop-on-empty covers are reached, at steps 19 and 2. The push at a count of 16 is unreached, which is exactly the behaviour the assumption deleted.

From that point on no legal trace exists, so every assertion that needs to look past it passes for nothing. Some tools report a conflict when the assumptions are unsatisfiable from reset, but not every case is caught. Covers of normal behaviour after that point are the reliable check.

Add covers of normal behaviour at growing depths, and find where they stop being reached. Then disable assumptions one at a time and rerun the covers. An assumption whose removal brings them back is part of the conflict. Fix it from the spec, and keep the covers as a standing check.

Under-constraint gives false failures: they cost debug time, but every one is visible in a trace. Over-constraint gives false passes, which look exactly like real ones. Over-constraint is the dangerous one, and covers under the full assumption set are the only routine defence against it.

List every assumption with its spec row and a cover showing legal behaviour survives it. Also list where it is checked at system level, usually a bound assertion in simulation. Anything without a spec row is either removed or escalated as a design requirement. The review signs off the list, not the proof.

The inputs are free, so the solver drove a sequence no legal master sends: it changed the address during a stall. The failure is false; the bench is under-constrained. Add one assumption from the spec row and cite the row. It says arvalid stays high and the address stays stable until the handshake. Then cover the stall and the handshake so the assumption did not go too far.

A long list written up front is likely to include rules stronger than the real environment, and nothing tells you which. Starting loose means you add each assumption in answer to a trace that showed an illegal input. So every assumption has a reason and a spec row. The false failures are cheap; a silent over-constraint is not.

The address is now stuck at its starting value, so most legal reads never happen. The pass says nothing about other addresses. A cover of a handshake at address 8'hFF comes back unreached, which shows the assumption removed legal traffic.

Write the spec rule: while arvalid waits for arready, the address holds. In this bench that is arvalid && !arready |=> araddr == araddr_q. Between transfers the address is free again. Then rerun the covers: the stall, the handshake and the handshake at 8'hFF must all be reached.

Not yet: those are glue properties about the mechanism, and they miss bugs that leave the pointers and count intact. Write an end-to-end check at the ports first: every accepted word leaves once, in order and unchanged. In the lesson, this glue set passes depth 10 on a FIFO that reads the wrong slot. The end-to-end check fails at step 3. Keep the glue to localise failures and feed induction.

Glue properties check the mechanism: pointers stay consistent with the count and full and empty agree with them. A bug in what is read, such as the wrong slot or stale data, leaves all of that intact. Only a property that compares what leaves with what entered, the purpose of the block, can see it.

Track one word whose value comes from $anyconst, so the solver picks it once, and let the cycle it enters be free. Count the words ahead of it, then assert that it is never dropped and that it leaves first in line, unchanged. The value and entry time are arbitrary. So a proof for this one word covers every word, as long as the design never inspects the data.

Without helpers the induction step may start with the tracker claiming a word is stored in a slot that holds something else. Helpers tie the tracker to the design. Its distance from the read pointer equals the count of words ahead. Memory at the tracked slot still holds the value. Without them the proof stays UNKNOWN even at k = 8; with them it closes at k = 2.

Track two writes chosen freely by the solver, the first accepted before the second. Assert that the first leaves before the second and both arrive unchanged. Because both choices are free, the check covers every pair of words, which catches reordering that a single tracker cannot see.

The solver may pick any two writes, at any times, as the tracked pair. A proof must hold for every choice it could make. So if any pair could swap, some choice of the two tracked words shows it. Two trackers then stand for all pairs, with only two sets of state.

A reference queue copies every word, so its state grows with depth times width. The solver must reason about all of it. The tracker holds one value, one slot and one count, yet covers every word through the free choice. The queue is closer to a simulation scoreboard and easier to read, so people pick it first. The tracker is what converges.

Track one symbolic packet, tagged at the moment of acceptance. Count how many packets of its flow are owed ahead of it at its output. Assert that it leaves at its turn, on the right port, unchanged. Also assert that no output delivers a packet it does not owe. Fairness is a separate question: a fixed-priority arbiter passes every one of these safety checks.

Anything that needs more than ten steps to reach a port. Examples are a pointer that wraps wrongly only after many writes, or a count that drifts and overflows later. The end-to-end check sees the effect only once the bad word is read. Glue invariants on the count and pointers catch such drift early and also help an induction proof close.

A formal bench has four parts: the DUT, assumptions on inputs, assertions on outputs and state, and covers. There is no driver, clock generator or scoreboard class, because the solver chooses every input. For the slice, assume upstream holds in_valid and its data until accepted. Assert the same rule on the output side. Cover a stall and a back-to-back transfer.

The solver treats every input as free and considers all legal values on every cycle. So writing stimulus would only narrow the search. Assumptions say what is legal. Covers replace the coverage model. Each one asks whether a behaviour is reachable under those assumptions, and returns a trace if it is.

Expect failures that no real neighbour could cause, because every input is free on every cycle. For example, the data changes while valid waits for ready. Triage each one: check the reset state, then each input against the spec. Add one assumption per spec rule, and cover the behaviour you still expect.

Capture the accepted input in modelling code. When the word leaves, assert that the output equals the same function of it, here the captured value plus one. The modelling code only reads design signals; it never drives them.

Write each rule once with its owner, and let a parameter choose assume or assert. Rules owned by the side under test are asserted, and the rest are assumed. A rule that flips from assertion to assumption is no longer checked on the new bench. So review it and cover what it might exclude. Watch for over-strict rules, such as forbidding PREADY high while PENABLE is low, which APB allows.

They check the same rule. The |=> is one flop of delay, and $stable compares with last cycle's sample. So the immediate form registers the stall condition and the data, and asserts on them a cycle later. In the lesson both forms fail the buggy slice at step 4. The immediate form helps where an engine refuses history functions on primary inputs, as this one does.

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.

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.

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.

Combinational equivalence pairs the flops of the two designs and compares the logic cone in front of each pair, with no unrolling. It suits RTL against a synthesised netlist, because synthesis mostly keeps the flops. Sequential equivalence lets the state differ and asks for equal outputs over time from reset. You need it after retiming, pipelining, state recoding or clock-gating changes.

Matching flops cuts both designs into small cones between key points, so each comparison is combinational and needs no unrolling. If two flops are paired wrongly, their cones compute different functions. The tool then reports a mismatch that is a mapping error, not a design bug. Debug starts at the smallest failing cone and the key points that feed it.

Then combinational LEC cannot pair those flops, because they now hold different functions. Their cones fail or stay unmapped. The retimed region needs sequential equivalence, which compares outputs over time from reset. That region then gets its own line in the sign-off.

Expect it. Equivalence of unlike multipliers grows exponentially with width on every solver. BDDs for the middle product bit are exponential for every variable order. Change the question instead of the machine. Compare at register boundaries, or split the proof into partial products and the adder tree, each of which is easy to check.

Probably not. Treating key points as free inputs throws away the relations between them. So the tool can pick combinations the real design never produces. A real difference has a consistent counterexample that is reachable from the inputs. Check that before calling it a bug. Otherwise, fix the mapping or add a constraint.

Build a miter of the old and new RTL and check conditional equivalence. Outputs must match whenever the bug's condition is false. Inside that condition, the new design must meet the spec. Write the condition from the bug report, never from the diff, or a wrong fix defines its own condition. A counterexample on inputs the spec forbids means a missing assumption, not a bad fix.

Both say where the check applies. A condition that is too wide hides real differences, exactly as an over-constraining assumption hides bugs. So it needs the same discipline. It needs a written source in the bug report or the spec. It also needs a review by someone who did not write the fix.

Inside the excluded region the old and new designs may differ freely, and the check says nothing. So a second, accidental change to another opcode in that group passes. Write the condition from the bug report, so it covers only the failing case. Then check the new design inside it against the spec.

The regression samples the input space at the points its tests reach, and it takes hours or days. The miter covers every input in the region where the old and new designs must agree. For a block-level fix, it usually takes minutes. The regression still matters for what the miter does not state. That is the behaviour inside the bug condition and the system around the block.

AXI allows WRAP bursts of only 2, 4, 8 or 16 transfers, so length 3 cannot occur; add that rule as an assumption, citing the spec. Add only what a counterexample demands: in the lesson the alignment assumption turned out unnecessary, because the check passes without it.

Every late RTL change carries a miter against the last signed-off RTL. Its condition comes from its bug report, and a second engineer reviews it. The block's formal regression and RTL-to-netlist LEC rerun on the new netlist. The ECO is closed only when all three are clean and the condition is attached to the change record.

Start with apps that need no hand-written properties: connectivity from the integration table and register checks from the register map. Both find real wiring and access-type bugs within days, which earns trust for the harder work. Then add automatic checks and X-propagation, and use unreachability analysis to prune coverage holes for the simulation team. An app proves only the properties it generates, so design rules still need your own.

Checks generated from the RTL only prove that the RTL agrees with itself. A field built with the wrong access type then passes. The map is the independent statement of intent. Each access type in it implies a fixed set of checks. For example, a write of 1 clears a W1C bit and a write of 0 keeps it.

Then the proof passes, because the RTL and the checks agree with the same wrong row. Formal shows that the RTL matches the map, not that the map is right. So the map needs its own review against the spec and the driver code. A firmware test of the field in system simulation catches what that review misses.

The W1C check that a written 0 keeps a set bit fails within a few cycles: plain read-write overwrites the bit with the 0. The subtle part is priority. A hardware event that arrives in the same cycle as the clearing write must still set its bit. The bus protocol is assumed and covered, and the register behaviour is asserted one cycle after the completing write.

Lint reads the text and flags code that could be wrong, such as a width mismatch. It does not know whether the bad case can happen. Formal automatic checks generate covers and assertions from the RTL and show whether the bad state is reachable, with a trace. In the lesson lint warned only about a truncated index, while formal failed the index, a dropped carry and an X default.

Formal can ask three things of a bin: is it reachable, proven unreachable forever, or merely unreached within N steps. Only the proof supports a waiver; a bounded unreached cover is a hint about depth. In the lesson one bin is unreached at depth 20 and reached at step 26 at depth 30. Run the proof with as few assumptions as possible, since an over-constraint makes a live bin look dead.

Free inputs allow more behaviour than the real environment. So a bin that cannot be reached even with free inputs cannot be reached in the chip. Every assumption you add shrinks the search and can make a live bin look dead. Add an assumption only when a reached trace is clearly illegal, and list it on the waiver.

Replay it as a directed test. SBY writes a small Verilog testbench for every trace. You can port the input values into the simulation environment as a sequence. The simulation team then has a test that hits the bin and keeps hitting it in regression. Every checker and scoreboard watches that test.

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.

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.

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.

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 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.