← Formal Verification Interviews
Interview Question · Code Reading
Is a Cut Point Safe?
- Likely at Intel
- Likely at NVIDIA
The Question
The interviewer asks
In a packet buffer's bench you replace the CRC check with the cut below. Can that make a buggy design pass? Can it make a correct design fail?
wire bad = $anyseq; // cut point: was crc16(head[47:0]) != head[63:48]
assign fwd = !empty && !bad;
wire do_rd = !empty && (bad || rd); // a corrupt head word is droppedYou 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
Freeing a signal lets it take any value, so the cut model has every behaviour of the real design and more. A pass on the cut model is therefore a real pass, but a failure may be one the cut invented. Check each failure at the freed signal. If no real logic could produce that value there, add an assumption that restores the fact. Then prove that assumption on the uncut logic.
Read the diagram as text
- wdata, wr: 64-bit words: CRC in the top 16 bits
- memory, 16 × 64: cut B: blackbox, every output free
- CRC-16 check: cut A: bad becomes a free input
- full flag: cut C: control, gives a false failure
- wr_ptr, rd_ptr, count: a corrupt head word is dropped
- assertions: empty |-> pointers equal; count <= 16
- wdata, wr → memory, 16 × 64
- memory, 16 × 64 → CRC-16 check: head word
- CRC-16 check → wr_ptr, rd_ptr, count: drop
- full flag → wr_ptr, rd_ptr, count: write enable
- wr_ptr, rd_ptr, count → full flag: count == 16
- wr_ptr, rd_ptr, count → assertions
Cuts A and B remove the datapath from the cone. Cut C removes a fact the assertions depend on.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Mid-Level)
A good mid-level answer says a cut point allows more behaviour than the real logic. So a pass is sound, but a failure needs checking.
What Interviewers Listen For (Senior)
A good senior answer cuts only datapath the property does not read, never the control it depends on. It proves every restoring assumption on the real logic. It reruns a known-buggy version after every cut.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItBreak ItCompare
- Is a Cut Point Safe?
-
Break ItWhen an Abstraction Removes the BugL2 Mid-LevelL3 Senior
An abstract model of a buffer passes, but its full-write cover is unreached. How did the abstraction remove a real bug?
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 replacement was not a superset of the real logic. Something narrowed it. Typically that is an assumption added to silence a false failure, or a model that leaves out a legal case. A sound abstraction must keep every concrete behaviour. The unreached cover is the evidence; fix the abstraction, not the cover.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F4.2.2: The Cut That Removed the BugSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
WhyWhy an Assumption on a Cut Is RiskyL2 Mid-LevelL3 Senior
Why is an assumption placed on a cut signal more dangerous than the cut itself?
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
A cut only adds behaviour, so a pass on the cut model still holds for the real design. An assumption on the cut signal removes behaviour again. If it removes something the real logic can do, a real bug disappears. So prove each such assumption on the uncut logic in a side run.
Self-Check
Tick each key point you covered in your answer.
Misconception
"The assumption only removes a false failure, so it is safe."
A false failure and a real one can need the same cut value. Removing the value removes both, unless the assumption is proven on the real logic.
Source Lesson F4.2 key points
-
Prove ItSolve F4.2.1: A Free CRC CutSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
CompareBlackbox vs Cut PointL2 Mid-Level
Compare blackboxing a submodule with placing a cut point.
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
A blackbox turns every output of a module into a free input. That suits memories and arithmetic the property does not depend on. A cut point frees a single internal node. So you can remove one hard cone, such as a CRC check, without dropping the module around it. Both add behaviour, so a pass stays sound and a failure must be checked at the freed signal.
Self-Check
Tick each key point you covered in your answer.
-
What IfIs the Cut Model's Failure Real?L2 Mid-Level
The cut model fails. How do you decide whether the failure is real?
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
Look at the freed signal in the trace. If the real logic could produce that value from the trace's inputs, the failure is real. Running the uncut design to the same step confirms it. If not, the cut invented it, and you either restore the missing fact with a proven assumption or choose a different cut.
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.
Missed Corner
"Cut the control signal that makes the proof slow."
If the property depends on it, the free value produces false failures. Cutting full in this buffer lets it write past 16 entries, a failure at step 19 the real design cannot reach.
Run It
The packet buffer from lesson F4.2 with full cut instead of the CRC check.
module pbuf_mem(input clk, we, input [3:0] wa, ra, input [63:0] wd, output [63:0] rd);
reg [63:0] m [0:15];
always @(posedge clk) if (we) m[wa] <= wd;
assign rd = m[ra];
endmodule
module pbuf(input clk, rst, wr, rd, input [63:0] wdata, output [63:0] rdata, output fwd, empty);
reg [4:0] wr_ptr = 0, rd_ptr = 0, count = 0;
wire full = $anyseq; // cut point on a control signal
assign empty = count == 5'd0;
wire do_wr = wr && !full;
wire [63:0] head;
pbuf_mem u_mem(.clk(clk), .we(do_wr), .wa(wr_ptr[3:0]), .ra(rd_ptr[3:0]), .wd(wdata), .rd(head));
function [15:0] crc16(input [47:0] d); // CRC-16/CCITT over the payload
integer i; reg [15:0] x;
begin x = 16'hFFFF;
for (i = 47; i >= 0; i = i - 1) x = {x[14:0], 1'b0} ^ ((x[15] ^ d[i]) ? 16'h1021 : 16'h0000);
crc16 = x;
end
endfunction
wire bad = crc16(head[47:0]) != head[63:48];
assign rdata = head;
assign fwd = !empty && !bad;
wire do_rd = !empty && (bad || rd); // a corrupt head word is dropped
always @(posedge clk)
if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
else begin
if (do_wr) wr_ptr <= wr_ptr + 5'd1;
if (do_rd) rd_ptr <= rd_ptr + 5'd1;
count <= count + do_wr - do_rd;
end
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) begin
if (empty) assert(wr_ptr == rd_ptr);
assert(count <= 5'd16);
end
endmodule
Prints: bmc, depth 24 (smtbmc yices): FAIL at step 19
See the Fix
module pbuf_mem(input clk, we, input [3:0] wa, ra, input [63:0] wd, output [63:0] rd);
reg [63:0] m [0:15];
always @(posedge clk) if (we) m[wa] <= wd;
assign rd = m[ra];
endmodule
module pbuf(input clk, rst, wr, rd, input [63:0] wdata, output [63:0] rdata, output fwd, empty);
reg [4:0] wr_ptr = 0, rd_ptr = 0, count = 0;
wire full = count == 5'd16;
assign empty = count == 5'd0;
wire do_wr = wr && !full;
wire [63:0] head;
pbuf_mem u_mem(.clk(clk), .we(do_wr), .wa(wr_ptr[3:0]), .ra(rd_ptr[3:0]), .wd(wdata), .rd(head));
function [15:0] crc16(input [47:0] d); // CRC-16/CCITT over the payload
integer i; reg [15:0] x;
begin x = 16'hFFFF;
for (i = 47; i >= 0; i = i - 1) x = {x[14:0], 1'b0} ^ ((x[15] ^ d[i]) ? 16'h1021 : 16'h0000);
crc16 = x;
end
endfunction
wire bad = $anyseq; // cut point on the datapath
assign rdata = head;
assign fwd = !empty && !bad;
wire do_rd = !empty && (bad || rd); // a corrupt head word is dropped
always @(posedge clk)
if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
else begin
if (do_wr) wr_ptr <= wr_ptr + 5'd1;
if (do_rd) rd_ptr <= rd_ptr + 5'd1;
count <= count + do_wr - do_rd;
end
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) begin
if (empty) assert(wr_ptr == rd_ptr);
assert(count <= 5'd16);
end
endmodule
Prints: prove, depth 4 (abc pdr): PASS
Misconception
"A cut point can hide a bug, so never use one."
A pure cut only adds behaviour, so it cannot remove a real failing trace. What can hide a bug is an assumption added afterwards to silence a false failure.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 10 "Cut points"