← Formal Verification Interviews
Interview Question · Concept
Which Formal Apps to Run First
The Question
The interviewer asks
You join an SoC project that has no formal yet. Which formal apps would you run first, and why those?
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
Start with apps that need no hand-written properties: connectivity from the integration table and register checks from the register map. Both find real wiring and access-type bugs within days, which earns trust for the harder work. Then add automatic checks and X-propagation, and use unreachability analysis to prune coverage holes for the simulation team. An app proves only the properties it generates, so design rules still need your own.
Read the diagram as text
- Property verification (F1 to F4): the general case: you write every rule
- Generated from a table or the RTL: automatic checks, connectivity, registers, X, unreachability
- Generated from a second design: equivalence (F6)
- A person names the rule: CDC protocol properties, information flow, post-silicon covers
- Where a team with no formal engineer starts: connectivity and registers: a spreadsheet in, a verdict out
- Generated from a table or the RTL → Property verification (F1 to F4)
- Generated from a second design → Property verification (F1 to F4)
- A person names the rule → Property verification (F1 to F4)
- Generated from a table or the RTL → Where a team with no formal engineer starts
The generated group needs no formal expertise to run, but someone still has to read every verdict against the spec.
Measured with smtbmc yices at depth 20, RTL selects swapped. The solver needs one step out of reset and different values on uart_tx and spi_mosi. Sampled at step 1, reported at 2.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Junior)
A good junior answer names the connectivity and register apps. It says they need no hand-written properties.
What Interviewers Listen For (Senior)
A good senior answer orders the apps by return on effort, and ties each to an owner and an input table. It says which bugs each app cannot see.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItCompare
- Which Formal Apps to Run First
-
WhyWhy Register Checks Come from the MapL1 JuniorL2 Mid-Level
Why must register checks be generated from the register map, and never from the RTL?
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
Checks generated from the RTL only prove that the RTL agrees with itself. A field built with the wrong access type then passes. The map is the independent statement of intent. Each access type in it implies a fixed set of checks. For example, a write of 1 clears a W1C bit and a write of 0 keeps it.
Self-Check
Tick each key point you covered in your answer.
-
What IfWhen the Register Map Itself Is WrongL2 Mid-Level
What if the RTL and the checks both come from the same register map? One row of the map has the wrong access type.
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
Then the proof passes, because the RTL and the checks agree with the same wrong row. Formal shows that the RTL matches the map, not that the map is right. So the map needs its own review against the spec and the driver code. A firmware test of the field in system simulation catches what that review misses.
Self-Check
Tick each key point you covered in your answer.
Half-Truth
"The register proof passed, so the driver will work."
The proof compares the RTL with the map. A wrong row gives matching RTL and checks, so the proof agrees with the bug.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 7 "Specifying control register requirements"
-
Prove ItSolve F5.3.2: The Swapped Pair in the TableSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
What IfA W1C Field Built as Read-WriteL1 JuniorL2 Mid-Level
An interrupt-status field should be write-one-to-clear but was built as the line below. Which generated check catches it, and what is the subtle part?
systemverilog if (wr && paddr == 12'h108) irq_stat <= pwdata[3:0] | irq_in; // bug: plain read-write else irq_stat <= irq_stat | irq_in;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
The W1C check that a written 0 keeps a set bit fails within a few cycles: plain read-write overwrites the bit with the 0. The subtle part is priority. A hardware event that arrives in the same cycle as the clearing write must still set its bit. The bus protocol is assumed and covered, and the register behaviour is asserted one cycle after the completing write.
One W1C Bit Is a Two-State MachineEach bit of IRQ_STAT moves only on these arcs. A plain read-write register adds the forbidden arc: a write of 0 clears. Arrows mean "next cycle". call: who calls whomRead the diagram as text
- bit = 0: nothing pending
- bit = 1: an interrupt pending
- irq_in[i] = 1: hardware sets, and wins over a clearing write
- write with data[i] = 1: firmware clears what it handled
- write with data[i] = 0: must leave the bit alone
- plain RW: data[i] = 0 clears: the forbidden arc the story hit
- bit = 0 → irq_in[i] = 1
- irq_in[i] = 1 → bit = 1
- bit = 1 → write with data[i] = 1
- write with data[i] = 1 → bit = 0
- bit = 1 → write with data[i] = 0
- write with data[i] = 0 → plain RW: data[i] = 0 clears: RW only
Two arcs leave "bit = 1": a clearing write of 1, or nothing. The write-0 property catches the third arc that a plain register adds.
The measured trace from lesson F5.4: a completed write of 0 to the status register clears a bit that was set.
A write of 0 clears a W1C bit Measured with smtbmc yices at depth 20, the write-0 row only. The write completes at step 2 with the set bit's data bit at 0; at step 3
irq_statis 0. Reported at 4.Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F5.4.2: Repair Write-One-to-Clear PrioritySimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
CompareLint vs Formal Automatic ChecksL1 JuniorL2 Mid-Level
Compare lint with formal automatic checks on the same RTL.
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
Lint reads the text and flags code that could be wrong, such as a width mismatch. It does not know whether the bad case can happen. Formal automatic checks generate covers and assertions from the RTL and show whether the bad state is reachable, with a trace. In the lesson lint warned only about a truncated index, while formal failed the index, a dropped carry and an X default.
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.
Half-Truth
"Connectivity is just wires; simulation already covers it."
Simulation exercises only the pin modes a test happens to use. A swapped pad pair on a rarely used mode passes every test; the check generated from the table fails at step 2.
Run It
Checks generated from a connection table, on a pad mux with two sources swapped.
module conn_top(input clk, rst, input [11:0] src, input uart_tx, spi_mosi, input [1:0] gpio_o,
input [1:0] pad_sel, input pipe_in, output [11:0] dst, output pad41, pad42, output reg pipe_out=0);
assign dst = src;
assign pad41 = pad_sel == 2'd0 ? gpio_o[0] : pad_sel == 2'd1 ? spi_mosi : pad_sel == 2'd2 ? uart_tx : 1'b0; // bug: 1 and 2 swapped
assign pad42 = pad_sel == 2'd0 ? gpio_o[1] : pad_sel == 2'd1 ? spi_mosi : pad_sel == 2'd2 ? uart_tx : 1'b0;
always @(posedge clk) pipe_out <= rst ? 1'b0 : pipe_in;
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
reg pipe_in_q=0, rst_q=1; // last cycle's pipe_in and rst
always @(posedge clk) begin pipe_in_q <= pipe_in; rst_q <= rst; end
// generated from the connection table
always @(posedge clk) if (!rst) begin
assert(dst[0] == src[0]);
assert(dst[1] == src[1]);
assert(dst[2] == src[2]);
assert(dst[3] == src[3]);
assert(dst[4] == src[4]);
assert(dst[5] == src[5]);
assert(dst[6] == src[6]);
assert(dst[7] == src[7]);
assert(dst[8] == src[8]);
assert(dst[9] == src[9]);
assert(dst[10] == src[10]);
assert(dst[11] == src[11]);
if (pad_sel == 2'd0) assert(pad41 == gpio_o[0]);
if (pad_sel == 2'd1) assert(pad41 == uart_tx);
if (pad_sel == 2'd2) assert(pad41 == spi_mosi);
if (pad_sel == 2'd0) assert(pad42 == gpio_o[1]);
if (pad_sel == 2'd1) assert(pad42 == spi_mosi);
if (pad_sel == 2'd2) assert(pad42 == uart_tx);
if (!rst_q) assert(pipe_out == pipe_in_q);
end
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 2
See the Fix
module conn_top(input clk, rst, input [11:0] src, input uart_tx, spi_mosi, input [1:0] gpio_o,
input [1:0] pad_sel, input pipe_in, output [11:0] dst, output pad41, pad42, output reg pipe_out=0);
assign dst = src;
assign pad41 = pad_sel == 2'd0 ? gpio_o[0] : pad_sel == 2'd1 ? uart_tx : pad_sel == 2'd2 ? spi_mosi : 1'b0;
assign pad42 = pad_sel == 2'd0 ? gpio_o[1] : pad_sel == 2'd1 ? spi_mosi : pad_sel == 2'd2 ? uart_tx : 1'b0;
always @(posedge clk) pipe_out <= rst ? 1'b0 : pipe_in;
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
reg pipe_in_q=0, rst_q=1; // last cycle's pipe_in and rst
always @(posedge clk) begin pipe_in_q <= pipe_in; rst_q <= rst; end
// generated from the connection table
always @(posedge clk) if (!rst) begin
assert(dst[0] == src[0]);
assert(dst[1] == src[1]);
assert(dst[2] == src[2]);
assert(dst[3] == src[3]);
assert(dst[4] == src[4]);
assert(dst[5] == src[5]);
assert(dst[6] == src[6]);
assert(dst[7] == src[7]);
assert(dst[8] == src[8]);
assert(dst[9] == src[9]);
assert(dst[10] == src[10]);
assert(dst[11] == src[11]);
if (pad_sel == 2'd0) assert(pad41 == gpio_o[0]);
if (pad_sel == 2'd1) assert(pad41 == uart_tx);
if (pad_sel == 2'd2) assert(pad41 == spi_mosi);
if (pad_sel == 2'd0) assert(pad42 == gpio_o[1]);
if (pad_sel == 2'd1) assert(pad42 == spi_mosi);
if (pad_sel == 2'd2) assert(pad42 == uart_tx);
if (!rst_q) assert(pipe_out == pipe_in_q);
end
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
Half-Truth
"The register app passed, so the register block is verified."
It proves the checks generated per access type. Side effects, aliasing, privilege, strobes and hardware write paths need rows in the map or properties of your own.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 7 "Major challenges of control register verification"
Wrong Altitude
Lists every app the vendor sells without ranking them.
The question is about priority. A pass ranks by bugs found per week of effort and says what input each app needs.