Formal verification questions in interviews test whether you understand what a formal tool really proves, and whether you can write and debug properties. This article collects common questions, from basic to advanced, with short answers and links to the articles that explain each topic in depth. Try to answer each question yourself before opening the answer.
12 min read | Intermediate
What You'll Learn
- Answer the most common conceptual questions about formal verification
- Explain property, assumption, cover and counterexample precisely
- Discuss depth, induction, vacuity and over-constraining with examples
- Write short SVA properties on request
Basics
1. What is the difference between formal verification and simulation?
Show Answer
Simulation checks the inputs a testbench applies. Formal verification checks a property for every possible input sequence, within a bound or for all time, by turning the question into a problem for a solver. A formal failure comes with a counterexample; a pass covers all inputs, under the assumptions. (Formal vs simulation)
2. What is a counterexample?
Show Answer
An input sequence, from reset, that makes a property fail, shown as a waveform. In bounded model checking it is the shortest such sequence. (Reading a counterexample)
3. What do assert, assume and cover do in a formal tool?
Show Answer
An assertion is checked: the tool looks for inputs that break it. An assumption is obeyed: the tool only considers inputs that satisfy it. A cover is searched for: the tool shows a trace that reaches it, or reports it unreachable. (assert, assume and cover)
4. What is the difference between an immediate and a concurrent assertion?
Show Answer
An immediate assertion checks a condition when procedural code runs. A concurrent assertion is evaluated at clock edges on sampled values and can describe behavior over several cycles with sequences. (Immediate and concurrent)
5. What is the difference between |-> and |=>?
Show Answer
a |-> b checks b in the same cycle as a; a |=> b checks it in the next cycle, the same as a |-> ##1 b. (Sequences and implication)
Quick Check
Q: Write an SVA property: "after a request, an acknowledge comes within 1 to 3 cycles".
Show Answer
assert property (@(posedge clk) disable iff (rst) req |-> ##[1:3] ack);
Intermediate
6. Why does a formal run need a reset assumption?
Show Answer
Without it, every register starts at any value, including combinations the design never reaches after reset, and the tool reports failures from them. The assumption makes the run start like a real chip. (Reset and initial state)
7. What is over-constraining, and how do you detect it?
Show Answer
An assumption that removes legal input sequences, hiding bugs that need them, while all assertions still pass. Detect it with covers for situations the specification allows: an unreachable cover is the warning. (Over-constraining)
8. What is a vacuous pass?
Show Answer
An implication that passes because its trigger never happens, so its consequence is never checked. Causes include impossible triggers, over-constraints and too little depth. Cover every trigger. (Vacuity)
9. How do you choose the depth of a bounded check?
Show Answer
From the design: reset cycles, the longest counter or timeout involved, pipeline latency, the reporting step and a margin. Confirm it with covers for each behavior the properties talk about. (Choosing a depth)
10. How would you check that a FIFO never loses or reorders data?
Show Answer
With a tracked value: let the tool pick any data word, record how many words are ahead of it when it is pushed, count them down on pops, and assert that it comes out when the count reaches zero. (Data integrity)
11. What is the difference between safety and liveness?
Show Answer
Safety: nothing bad happens; its counterexamples are finite traces. Liveness: something good eventually happens; its counterexamples are infinite loops. BMC checks liveness as a bounded deadline, which turns it into safety. (Safety and liveness)
Quick Check
Q: A colleague's property is full == (count == 3'd5), copied from the RTL. What do you tell them?
Show Answer
It restates the RTL and will pass even if the RTL is wrong. Write it from the specification instead, for example count <= DEPTH and full == (count == DEPTH) with the specified depth.
Advanced
12. Why is a passing bounded check not a proof?
Show Answer
It only covers states reachable within the depth. A proof needs either a depth beyond the reachability diameter or a method such as induction or PDR. (Why a passing BMC is not a proof)
13. Explain k-induction.
Show Answer
Base case: the property holds for the first k cycles from reset. Step: from any k consecutive states where it holds, the next state also satisfies it. Together they cover every cycle. (Induction)
14. The induction step fails but the design is correct. Why, and what do you do?
Show Answer
The step started from an unreachable state that satisfies the property but leads to a violation. Read the start state, find the relation between registers it breaks, and add that relation as a helper assertion. Or try a larger k, or the PDR engine. (Strengthening invariants)
15. What are cut points and black boxes, and when is a pass with them valid?
Show Answer
They replace logic with free values. A pass is valid for the real design, because the free values include every real one. A failure may be false and must be checked. (Cut points)
16. What is assume-guarantee reasoning?
Show Answer
Checking blocks separately: each assumes what its neighbors guarantee and proves what it guarantees. Sound when every assumption is proven on the other side and the reasoning is not circular. (Assume-guarantee)
17. How does equivalence checking work, and when is it sequential?
Show Answer
A miter feeds both designs the same inputs and flags any output difference; the solver tries to make it fire. With matching registers it is combinational, per register-to-register cone. When registers do not match, as after re-encoding or retiming, it must compare behavior over time. (Combinational, sequential)
18. Which blocks would you choose for formal, and which not?
Show Answer
Formal: control-heavy, concurrent, critical blocks of moderate size, such as arbiters, FIFOs, flow control and protocol engines. Not: wide arithmetic, whole subsystems and software-driven scenarios, which go to simulation, with formal on their control parts. (A formal test plan)
Running It in ChipVerify Lab
Most questions above have a lab example in the linked article. Practicing them in the lab, and writing each property in both SVA and the lab form, is the best preparation for the "write a property" part of an interview.
Common Mistakes
Mistake #1: Saying "formal proves the design is correct"
Formal proves the properties you wrote, under your assumptions, for the configuration checked. Interviewers listen for that precision.
Mistake #2: Forgetting covers when asked how you would verify a block
An answer with assertions only invites the follow-up "how do you know they were exercised?". Mention covers and vacuity up front.
Practice Exercise
Challenge: A Whiteboard Question
"Here is a 2-requester arbiter with registered grants. Write the properties you would check, and say which ones need assumptions." Answer as you would at a whiteboard.
Hint
Safety, validity, fairness, and the assumption fairness needs. Do not forget covers.
Solution
a_excl: assert property (@(posedge clk) disable iff (rst) !(gnt[0] && gnt[1]));
a_valid: assert property (@(posedge clk) disable iff (rst) ##1 (gnt & ~$past(req)) == 2'b00);
m_hold: assume property (@(posedge clk) disable iff (rst) req[1] && !gnt[1] |=> req[1]);
a_fair: assert property (@(posedge clk) disable iff (rst) req[1] |-> ##[0:2] gnt[1]);
c_tie: cover property (@(posedge clk) disable iff (rst) req == 2'b11 ##1 gnt[1]);
Only fairness needs an assumption: requests are held until granted. Add the mirrored fairness rule and hold assumption for requester 0, and covers for each grant and for a tie.
Summary
- Know the vocabulary precisely: property, assumption, cover, counterexample, bounded, proven, vacuous.
- Be ready to write short SVA: implications, bounded delays,
$past,$onehot0. - Explain the pitfalls with examples: over-constraining, vacuity, too little depth, restating the RTL.
- For advanced questions: induction and strengthening, cut points, assume-guarantee and equivalence.
