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