Formal Verification Interview Questions

What is the difference between formal verification and simulation?

Simulation checks the design for the input sequences that the testbench applies, one at a time. Formal verification uses mathematical analysis to check a property for every possible input sequence, either up to a given depth or for all time.

So a formal pass is exhaustive within its limits, and a formal failure always comes with a concrete trace showing how to break the property. Formal works best on control logic such as arbiters, FIFOs and protocol interfaces, while simulation remains necessary for large designs, full datapaths and software-driven tests.

Read more on Formal vs Simulation.

What do assert, assume and cover do in a formal tool?

• assert: a property the design must satisfy. The tool tries to find a trace that violates it.
• assume: a constraint on the inputs. The tool only considers traces where it holds, so it describes legal stimulus.
• cover: a scenario that should be reachable. The tool tries to find a trace that reaches it, which shows the environment is not too restrictive.

assume property (@(posedge clk) disable iff (!rst_n) !(push && full));
assert property (@(posedge clk) disable iff (!rst_n) !(full && empty));
cover  property (@(posedge clk) full);

Read more on Assert, Assume and Cover.

What is a counterexample?

A counterexample is a trace, usually a few cycles long, of input values that makes an assertion fail. The tool produces it from reset, so it can be viewed as a waveform and replayed in simulation.

The first step in debugging is to decide whether the trace shows a real design bug or an illegal input sequence. If the inputs violate the interface protocol, an assumption is missing; if they are legal, the design or the property is wrong.

Read more on Reading a Counterexample.

What is the difference between |-> and |=> in SVA?

Both are implication operators: if the left side (the antecedent) matches, the right side (the consequent) must hold. With |-> (overlapped), the consequent is checked starting in the same cycle the antecedent ends. With |=> (non-overlapped), it starts one cycle later.

assert property (@(posedge clk) req |-> ##1 gnt);  // gnt one cycle after req
assert property (@(posedge clk) req |=> gnt);      // same check

So a |=> b is the same as a |-> ##1 b. Mixing them up shifts the check by one cycle, which is a common source of false failures.

Read more on Sequences and Implication.

What is over-constraining, and how do you detect it?

Over-constraining means the assumptions forbid input sequences that can really happen, so the tool never explores them and bugs behind them are missed. In the extreme, contradictory assumptions remove every trace and every assertion passes.

It is detected with cover properties: if a scenario that should be reachable, such as a full FIFO or a back-to-back request, cannot be covered, the assumptions are too strong. Each assumption should also be justified by the interface specification, and ideally checked as an assertion on the block that drives those inputs.

Read more on Over-Constraining.

What is a vacuous pass?

An implication passes vacuously when its antecedent never matches. For example, req |-> ##[1:4] gnt passes trivially if req can never be high, perhaps because of an over-restrictive assumption or a wrong signal name.

A vacuous pass proves nothing. Tools report vacuity, and a cover on the antecedent (cover property (req)) is a simple way to check that the property is actually exercised.

Read more on Vacuity.

Why does a formal run need reset assumptions?

A formal tool starts from the initial state. If reset is not constrained, the tool may start in any state, including states that the design can never reach after a proper reset, and report failures from them.

The usual setup is to assume reset is active in the first cycle, or for a few cycles, and released afterwards. Assertions are disabled during reset with disable iff.

Read more on Reset and the Initial State.

What is bounded model checking, and why is a passing bounded check not a proof?

Bounded model checking (BMC) unrolls the design for k cycles from reset and asks a solver whether any input sequence within those k cycles violates an assertion. If none exists, the property holds for the first k cycles only.

A bug that needs more than k cycles to appear, for example after a counter wraps or a FIFO fills, is not found. So the depth must be at least as long as the deepest interesting behaviour, and a full proof needs induction or another unbounded method.

Read more on Why a Passing BMC Is Not a Proof.

Explain k-induction.

K-induction proves a property for all time in two steps. The base case is a bounded check: the property holds for the first k cycles from reset. The induction step shows that from any k consecutive cycles in which the property holds, it also holds in the next cycle, starting from any state, not only reachable ones.

If both succeed, the property holds forever. The induction step often fails on unreachable states, where the property holds for k cycles but the internal state is inconsistent. The fix is to add helper assertions (invariants) that rule out those states, or to increase k.

Read more on Induction: Base Case and Step.

What is the difference between safety and liveness properties?

A safety property says something bad never happens, for example a FIFO never overflows. A violation can be shown with a finite trace.

A liveness property says something good eventually happens, for example every request is eventually granted. A violation needs an infinite trace, such as a loop where the grant never comes. In practice liveness is often turned into a bounded safety property, such as "a grant within 8 cycles", which is easier to prove and more useful as a specification.

Read more on Safety and Liveness.

How would you verify a FIFO with formal?

• Assume the environment does not push when full or pop when empty, if the design requires that.
• Assert the flags: full and empty are never both high, and the count matches pushes minus pops.
• Check data integrity with a tracked value: choose an arbitrary data word and an arbitrary push, and assert that the same word comes out at the matching pop, which proves no data is lost, duplicated or reordered.
• Cover full, empty, and simultaneous push and pop, to show the environment reaches them.

The tracking technique checks every word with one property instead of a full reference model, because the tool tries all choices of the tracked value.

Read more on Synchronous FIFOs.

What are black boxes and cut points?

A black box removes a module from the analysis and leaves its outputs as free inputs. A cut point does the same for a single internal signal. Both make the problem smaller, which helps with state explosion.

Because the freed signals can take any value, a pass is still valid (the design works for any behaviour of the removed logic), but a failure may be false, caused by values the real logic could never produce. Then assumptions are added to describe what the removed logic can really do.

Read more on Black Boxes and Cut Points.

How does equivalence checking work?

Combinational equivalence checking compares two versions of a design, for example RTL against the synthesized netlist. It matches the state elements (flops and latches) of the two designs and proves that the logic cones between matched points compute the same functions.

When the state elements do not correspond one to one, for example after retiming, FSM re-encoding or clock gating changes, sequential equivalence checking is needed. It compares the outputs over sequences of cycles from reset and is much harder.

Read more on Combinational Equivalence and Sequential Equivalence.

Which blocks are good candidates for formal, and which are not?

Good candidates are control-heavy blocks with a clear specification and limited depth: arbiters, FIFOs, credit counters, FSMs, bus interfaces, interrupt controllers and register access logic. Formal also suits apps such as connectivity checks, X-propagation and unreachable-code analysis.

Poor candidates are large datapaths such as multipliers or floating point units, deep pipelines with very long latency, and full-chip scenarios driven by software. Those are better covered by simulation, emulation, or specialised datapath equivalence tools.

Read more on A Formal Test Plan.