← Formal Verification Interviews
Interview Question · Concept
Safety and Liveness Properties
The Question
The interviewer asks
What is the difference between a safety property and a liveness property, and how does each one fail?
You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
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.
A prefix from reset to a request, then a loop the design can repeat forever. gnt is 0 in every state of the loop, so the promised grant never comes.
Around the loop pending stays 1 and gnt stays 0. No finite step fails; the failure is the loop itself, and only a liveness engine can return it.
Read the states and transitions
- reset: initial, depth 0.
- req seen: reachable, depth 1.
- pending, ready 0: bad, depth 2.
- pending, ready 0: bad, depth 3.
- pending, ready 0: bad, depth 4.
- gnt: unreachable, depth 0.
- reset → req seen.
- req seen → pending, ready 0.
- pending, ready 0 → pending, ready 0.
- pending, ready 0 → pending, ready 0.
- pending, ready 0 → pending, ready 0.
Illustration. A drawing, not an engine witness. The state labelled gnt is never entered on this path.
Read the diagram as text
- Deadlock: one stuck state, repeated
- Livelock: a loop of legal states: retry, back off, retry
- Starvation: a loop in which one requester is never served
- Safety, in bmc: !(sa == 1 && sb == 1): a finite trace
- Liveness: req |-> s_eventually gnt: a lasso
- Liveness plus fairness: or a round-robin fix
- Deadlock → Safety, in bmc
- Livelock → Liveness
- Starvation → Liveness plus fairness
Only deadlock is reached at a finite step. Livelock and starvation have no bad state, only a bad loop.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Junior)
A good junior answer defines both kinds. It says a safety counterexample ends at a failing step, while a liveness counterexample is a loop.
What Interviewers Listen For (Senior)
A good senior answer explains fairness, and uses a bounded response with a deadline from the spec when the schedule needs it. It says deadlock is a safety property that BMC can find.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItCompare
- Safety and Liveness Properties
-
WhyWhy Liveness Needs FairnessL2 Mid-Level
Why does almost every liveness property fail unless you add fairness assumptions?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
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.Self-Check
Tick each key point you covered in your answer.
-
CompareDeadlock, Livelock and StarvationL2 Mid-Level
Compare deadlock, livelock and starvation. Which of them can a plain bmc run find?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
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.
Deadlock found as a safety failure Measured at depth 20.
own1= 1 (A) andown2= 2 (B) from step 2 on: a single state the pair can never leave. With both machines taking lock 1 first: BMC PASS to depth 20.Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F8.4.1: Locate the Circular Handshake WaitSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
CompareLiveness vs Bounded ResponseL2 Mid-LevelL3 Senior
Compare a liveness check with a bounded-response check such as "
ackwithin 8 cycles ofreq".2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
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.
Bounded response, no fairness: the solver never lets ready rise Measured with smtbmc yices at depth 20. The window is steps 2 to 9;
readyis low in all 8 of them, so no design could grant.Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F3.7.1: An Environment That Never ServesSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
What IfWhat a Fixed-Priority Arbiter HidesL2 Mid-Level
A fixed-priority arbiter passes every safety check you wrote. What is it hiding?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
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.
BUG_FIXED_PRIO: input 1 waits while input 0 streams Measured,
bmcdepth 20: FAIL at reported step 8 ona_wait. 4 input-0 packets are accepted while input 1 waits.Self-Check
Tick each key point you covered in your answer.
What People Get Wrong
Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.
Misconception
"s_eventually ack passed in a BMC run, so the design always answers."
No finite run can show an endless wait. Liveness needs a liveness engine with fairness, or a bounded-response rewrite with a stated deadline.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 9 "Liveness properties that are not alive"
Misconception
"Deadlock is a liveness problem, so it needs a liveness engine."
A deadlock is a reachable state pair that nothing can leave. Asserting the pair never happens is safety, and bmc finds this one at step 3.
Run It
Two FSMs take two locks in opposite orders. The assertion says both are never waiting at once.
module two_fsm(input clk, rst, go_a, go_b, output reg [1:0] sa=0, output reg [1:0] sb=0);
reg [1:0] own1=0, own2=0; // owner of each lock: 0 free, 1 A, 2 B
wire [1:0] aw = sa == 2'd0 && go_a ? 2'd1 : sa == 2'd1 ? 2'd2 : 2'd0; // A: lock 1, then lock 2
wire [1:0] bw = sb == 2'd0 && go_b ? 2'd2 : sb == 2'd1 ? 2'd1 : 2'd0; // B: lock 2, then lock 1 (bug: the opposite order)
wire a_gets = aw != 0 && (aw == 2'd1 ? own1 == 0 : own2 == 0);
wire b_gets = bw != 0 && (bw == 2'd1 ? own1 == 0 : own2 == 0) && !(a_gets && aw == bw);
always @(posedge clk)
if (rst) begin sa <= 0; sb <= 0; own1 <= 0; own2 <= 0; end
else begin
sa <= a_gets ? sa + 2'd1 : sa == 2'd2 ? 2'd0 : sa;
sb <= b_gets ? sb + 2'd1 : sb == 2'd2 ? 2'd0 : sb;
own1 <= a_gets && aw == 2'd1 ? 2'd1 : b_gets && bw == 2'd1 ? 2'd2 : (sa == 2'd2 && own1 == 2'd1) || (sb == 2'd2 && own1 == 2'd2) ? 2'd0 : own1;
own2 <= a_gets && aw == 2'd2 ? 2'd1 : b_gets && bw == 2'd2 ? 2'd2 : (sa == 2'd2 && own2 == 2'd1) || (sb == 2'd2 && own2 == 2'd2) ? 2'd0 : own2;
end
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) assert(!(sa == 2'd1 && sb == 2'd1)); // no deadlock
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 3
See the Fix
module two_fsm(input clk, rst, go_a, go_b, output reg [1:0] sa=0, output reg [1:0] sb=0);
reg [1:0] own1=0, own2=0; // owner of each lock: 0 free, 1 A, 2 B
wire [1:0] aw = sa == 2'd0 && go_a ? 2'd1 : sa == 2'd1 ? 2'd2 : 2'd0; // A: lock 1, then lock 2
wire [1:0] bw = sb == 2'd0 && go_b ? 2'd1 : sb == 2'd1 ? 2'd2 : 2'd0; // B: lock 1, then lock 2
wire a_gets = aw != 0 && (aw == 2'd1 ? own1 == 0 : own2 == 0);
wire b_gets = bw != 0 && (bw == 2'd1 ? own1 == 0 : own2 == 0) && !(a_gets && aw == bw);
always @(posedge clk)
if (rst) begin sa <= 0; sb <= 0; own1 <= 0; own2 <= 0; end
else begin
sa <= a_gets ? sa + 2'd1 : sa == 2'd2 ? 2'd0 : sa;
sb <= b_gets ? sb + 2'd1 : sb == 2'd2 ? 2'd0 : sb;
own1 <= a_gets && aw == 2'd1 ? 2'd1 : b_gets && bw == 2'd1 ? 2'd2 : (sa == 2'd2 && own1 == 2'd1) || (sb == 2'd2 && own1 == 2'd2) ? 2'd0 : own1;
own2 <= a_gets && aw == 2'd2 ? 2'd1 : b_gets && bw == 2'd2 ? 2'd2 : (sa == 2'd2 && own2 == 2'd1) || (sb == 2'd2 && own2 == 2'd2) ? 2'd0 : own2;
end
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) assert(!(sa == 2'd1 && sb == 2'd1)); // no deadlock
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
Buzzword Without Mechanism
Says "add fairness" without saying what the environment promises.
Fairness is an assumption such as "ready is high infinitely often". It needs a reason from the spec and a quick check showing a fair path exists.