Formal Verification vs Simulation: How Interviewers Test Both

Your arbiter testbench ran 100,000 random request patterns and never saw two grants at once. Is the arbiter correct? A good interviewer will not accept "yes," and will not accept "no" either. They want to hear what that result does and does not tell you.

That gap between "I did not see a bug" and "there is no bug" is where simulation and formal verification split. This guide draws on public tutorials from ChipVerify (on formal verification and assertion-based verification) and Doulos (on coverage-driven verification). The practice prompts are ours, not questions reported from any employer.

What does simulation show, and what does it leave open?

Simulation applies specific stimulus and watches what the design does. ChipVerify puts the limitation bluntly: checks are sampled, so a property can pass for millions of cycles and still miss a bug. The testbench only covers scenarios it actually exercises.

That is not an argument against simulation. It is how you check a whole subsystem with realistic stimulus and scoreboards. See our UVM interview guide for verification engineers.

The honest answer to "is it correct?" after a clean regression is: "It passed the scenarios we generated, and I can tell you how well those scenarios cover the plan."

What does formal verification add?

ChipVerify describes formal as building a mathematical model of the design and reasoning about all legal inputs. You give the tool the RTL, properties written in SVA, and assumptions that define legal inputs. It either proves each property or returns a counterexample, a specific input sequence that triggers the violation. The page notes that the counterexample is minimal, which makes it easier to read than a long simulation failure.

Two distinctions come up in interviews:

• Bounded vs unbounded. Bounded model checking shows no violation within a set number of cycles. ChipVerify says it is fast and useful for many handshake and control bugs, but it is not a full proof if the bound is too short. A full proof covers all time and needs an inductive invariant. Complex designs may never converge.
• Inconclusive is not "pass." The page says an inconclusive result reflects tool limits such as time or memory, not a verdict on correctness. It also says formal scales to blocks, not full chips.

The other trap is assumptions. If they are too restrictive and rule out the buggy scenario, the proof is vacuous: technically correct, practically meaningless.

Assertions and coverage, in the same breath

SVA ties both worlds together. ChipVerify describes assert as a rule the design must satisfy, assume as a constraint on inputs, and cover as a check that a scenario actually occurred. In simulation, it says, an assume is treated as a comment, while in formal it limits the explored input space. It also recommends pairing an assert with a cover on its antecedent, because an assertion can pass vacuously if its trigger never happens.

Doulos separates two kinds of coverage. Code coverage measures execution of the RTL and is largely automatic. Functional coverage checks whether features in the verification plan were exercised, and the Doulos page says its quality depends on the diligence of the people who write that plan. The page says high quality verification benefits from both.

Doulos also gives a useful warning: it is possible to reach 100% code coverage with only 50% functional coverage, for example when the design is half complete. And coverage collected without comprehensive checking is, in its words, meaningless.

Turn the documentation into a study plan

The distinctions below come from the sources above. The practice prompts are MockVise's suggested exercises, not an employer's rubric.

Topic	Documented distinction	Practice prompt
Sampling vs exhaustive	Simulation samples scenarios; formal reasons over all legal inputs	What would a clean 100,000-pattern run not tell you?
Bounded proof	No violation within k cycles is not a full proof	How would you pick a bound, and how would you report the result?
Vacuity	Over-restrictive assumptions or unreachable antecedents can make results meaningless	How would you check that a passing property is not vacuous?
Assert, assume, cover	Assume constrains formal inputs; cover confirms a scenario happened	Which of the three would you write for "grant only follows a request"?
Code vs functional coverage	Code coverage is automatic; functional coverage depends on the plan	Why can 100% code coverage sit next to gaps in functional coverage?

An illustrative choice scenario

Here is a scenario of our own. Your team has a small round-robin arbiter and a full subsystem that contains it. A reviewer asks where you would use formal and where simulation. There is no single correct answer, but here is one way to structure yours:

1. Ask what the requirements are: no double grant, grant only after a request, and maybe a latency limit.
2. Say that the arbiter is a block-sized, control-heavy design, which ChipVerify lists among strong use cases for formal.
3. Write the properties and the input assumptions, and state which assumptions you would want a reviewer to challenge.
4. Add covers so you can show the properties are not passing vacuously. If the tool only reaches a bounded result, report the depth rather than calling it proven.
5. Keep simulation for the subsystem, where scoreboards, realistic traffic, and coverage-driven stimulus matter, and say the two approaches are complementary.
6. If a counterexample appears, read the shortest trace first, then decide whether it is an RTL bug or a missing assumption.

This is a way to practice your reasoning, not a prescribed flow. Real teams differ in tools and sign-off criteria.

Prepare for the follow-up questions

Expect interviewers to probe the edges: what happens if the proof does not converge, how you would debug a failing assertion that only fails in gate-level simulation, or whether you would trust a coverage report with weak checkers. If you have not used a formal tool, say so, then show how you would reason about properties and assumptions on a small example.

For adjacent preparation, our guide to RTL design interview questions helps with the design side of those properties, and pre-silicon verification versus post-silicon validation covers where each kind of evidence fits in the larger flow. If you are weighing career paths, see verification engineer versus RTL design engineer.

You can also book a mock interview on MockVise to practice defending a verification plan out loud, including what you would not claim.

Sources: ChipVerify, Formal Verification, ChipVerify, Assertion Based Verification, Doulos, Coverage-Driven Verification Methodology. This article provides general preparation guidance, not company interview questions. Interview formats vary, so confirm the format with your recruiter. MockVise is not affiliated with or endorsed by ChipVerify or Doulos.

FAQ

Q: Is a design correct after a clean simulation regression? Not necessarily. The honest answer is that it passed the scenarios generated, and you can say how well those scenarios cover the plan.

Q: What is the difference between bounded and unbounded formal proofs? Bounded model checking shows no violation within a set number of cycles and is not a full proof if the bound is too short. A full proof covers all time and needs an inductive invariant.

Q: What does it mean if a formal proof is vacuous? If assumptions are too restrictive and rule out the buggy scenario, the proof is technically correct but practically meaningless. Pairing an assert with a cover on its antecedent helps show the property is not passing vacuously.

Q: Can 100 percent code coverage mean the design is fully verified? No. Doulos notes it is possible to reach 100 percent code coverage with only 50 percent functional coverage, and coverage collected without comprehensive checking is meaningless.