← Formal Verification Interviews
Interview Question · Concept
Combinational vs Sequential Equivalence
- Likely at Google
- Likely at Intel
- Likely at Qualcomm
The Question
The interviewer asks
What is the difference between combinational and sequential equivalence checking, and when do you need each?
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
Combinational equivalence pairs the flops of the two designs and compares the logic cone in front of each pair, with no unrolling. It suits RTL against a synthesised netlist, because synthesis mostly keeps the flops. Sequential equivalence lets the state differ and asks for equal outputs over time from reset. You need it after retiming, pipelining, state recoding or clock-gating changes.
Read the diagram as text
- Shared inputs: write_en, read_en, write_data, reset, initialize
- Gold: hardware_fifo RTL: the design you verified
- Gate: Yosys netlist: 570 lines, 47 single-bit flops
- XOR on every output pair: full, empty, read_valid, read_data
- Property: the XOR is never 1: a safety property on the combined design
- Shared inputs → Gold: hardware_fifo RTL
- Shared inputs → Gate: Yosys netlist
- Gold: hardware_fifo RTL → XOR on every output pair
- Gate: Yosys netlist → XOR on every output pair
- XOR on every output pair → Property: the XOR is never 1
Two designs get the same inputs. Any input that makes an XOR output 1 is a counterexample.
Read the diagram as text
- Shared inputs: valid, a, b
- Gold: add_comb: sum = a + b, same cycle
- Gate: add_pipe2: stage 1: low bytes; stage 2: high bytes
- Modelling code: gold_q1, gold_q2: {valid, sum}, one and two cycles back
- Compare when the gate is valid: pipe_sum == gold_q2.sum
- Shared inputs → Gold: add_comb
- Shared inputs → Gate: add_pipe2
- Gold: add_comb → Modelling code: gold_q1, gold_q2
- Modelling code: gold_q1, gold_q2 → Compare when the gate is valid
- Gate: add_pipe2 → Compare when the gate is valid
Nothing pairs flop to flop, so LEC has nothing to cut at. The question becomes a property over time.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Junior)
A good junior answer defines both kinds. It names RTL against netlist as the usual combinational case.
What Interviewers Listen For (Senior)
A good senior answer explains key-point mapping, and why cut points can cause false mismatches. It plans sequential checks for retimed or recoded logic, with the latency written into the spec.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItBreak It
- Combinational vs Sequential Equivalence
-
WhyWhy LEC Needs Matched Key PointsL2 Mid-Level
Why does combinational LEC need the flops of both designs matched, and what goes wrong when the match is wrong?
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
Matching flops cuts both designs into small cones between key points, so each comparison is combinational and needs no unrolling. If two flops are paired wrongly, their cones compute different functions. The tool then reports a mismatch that is a mapping error, not a design bug. Debug starts at the smallest failing cone and the key points that feed it.
Matched State Turns One Question into Many Small OnesFlops with the same name in both designs are paired. Each pair, and each output, gets its own cone of logic to compare. call: who calls whomRead the diagram as text
- Key points in: inputs, plus every matched flop output
- One cone per key point: gold logic and gate logic, side by side
- Key points out: each flop input and each output
- Flops paired by name: wp, used, rp, response_valid, response, memory
- Key points in → One cone per key point
- One cone per key point → Key points out
- Flops paired by name → One cone per key point
EQY made 19 partitions for this FIFO: the flops above, eight read_data bits, and the named wires aw, ar, full, empty, read_valid.
Self-Check
Tick each key point you covered in your answer.
-
What IfEquivalence After RetimingL2 Mid-LevelL3 Senior
What if synthesis retimed part of the design, so some flops moved and no longer match by name?
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 combinational LEC cannot pair those flops, because they now hold different functions. Their cones fail or stay unmapped. The retimed region needs sequential equivalence, which compares outputs over time from reset. That region then gets its own line in the sign-off.
Self-Check
Tick each key point you covered in your answer.
Misconception
"The flop names changed, so map them by hand."
Retimed flops compute different functions, not renamed ones. Forcing a pair makes every cone after it mismatch.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 8 "Combinational equivalence", "Key point selection and mapping"
-
What IfAn Equivalence Check on a MultiplierL2 Mid-LevelL3 Senior
Asked if they mention datapath blocks
The equivalence check of two differently built multipliers never finishes. What do you do?
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
Expect it. Equivalence of unlike multipliers grows exponentially with width on every solver. BDDs for the middle product bit are exponential for every variable order. Change the question instead of the machine. Compare at register boundaries, or split the proof into partial products and the adder tree, each of which is easy to check.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F6.3.1: Partition the Multiplier QuestionSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Prove ItSolve F6.2.1: Align a Two-Stage AdderSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Break ItAn LEC Mismatch on Impossible InputsL2 Mid-Level
LEC reports a mismatch whose counterexample sets two internal key points to values that can never occur together. Is it 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
Probably not. Treating key points as free inputs throws away the relations between them. So the tool can pick combinations the real design never produces. A real difference has a consistent counterexample that is reachable from the inputs. Check that before calling it a bug. Otherwise, fix the mapping or add a constraint.
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
"The latency in the comparison is a tool setting, not part of the spec."
The two-stage adder is correct, yet comparing it against the reference delayed by one cycle instead of two fails at step 3. The latency is a statement about the design.
Run It
A correct two-stage adder compared with a combinational reference delayed by one cycle.
module add_comb(input [15:0] a, b, input valid, output [16:0] sum, output valid_out);
assign sum = a + b;
assign valid_out = valid;
endmodule
module add_pipe2(input clk, rst, valid, input [15:0] a, b,
output reg [16:0] sum = 0, output reg valid_out = 0);
reg [8:0] lo1 = 0; // stage 1: low bytes added, carry in bit 8
reg [7:0] ah1 = 0, bh1 = 0; // stage 1: high bytes, not yet added
reg v1 = 0;
wire [8:0] hi = ah1 + bh1 + lo1[8];
always @(posedge clk) begin
if (rst) begin v1 <= 0; valid_out <= 0; end
else begin
v1 <= valid;
valid_out <= v1;
if (valid) begin lo1 <= a[7:0] + b[7:0]; ah1 <= a[15:8]; bh1 <= b[15:8]; end
if (v1) sum <= {hi, lo1[7:0]};
end
end
endmodule
module sec_top(input clk, rst, valid, input [15:0] a, b);
wire [16:0] gold_sum, pipe_sum;
wire gold_valid, pipe_valid;
add_comb gold(.a(a), .b(b), .valid(valid), .sum(gold_sum), .valid_out(gold_valid));
add_pipe2 pipe(.clk(clk), .rst(rst), .valid(valid), .a(a), .b(b), .sum(pipe_sum), .valid_out(pipe_valid));
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
// modelling code: the gold's {valid, sum}, one and two cycles back
localparam LAT = 1;
reg [17:0] gold_q1 = 0, gold_q2 = 0;
always @(posedge clk) begin
gold_q1 <= rst ? 18'd0 : {gold_valid, gold_sum};
gold_q2 <= rst ? 18'd0 : gold_q1;
end
wire [17:0] gold_d = LAT == 1 ? gold_q1 : gold_q2;
always @(posedge clk) if (!rst) begin
assert(pipe_valid == gold_d[17]);
if (pipe_valid) assert(pipe_sum == gold_d[16:0]);
end
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 3
See the Fix
module add_comb(input [15:0] a, b, input valid, output [16:0] sum, output valid_out);
assign sum = a + b;
assign valid_out = valid;
endmodule
module add_pipe2(input clk, rst, valid, input [15:0] a, b,
output reg [16:0] sum = 0, output reg valid_out = 0);
reg [8:0] lo1 = 0; // stage 1: low bytes added, carry in bit 8
reg [7:0] ah1 = 0, bh1 = 0; // stage 1: high bytes, not yet added
reg v1 = 0;
wire [8:0] hi = ah1 + bh1 + lo1[8];
always @(posedge clk) begin
if (rst) begin v1 <= 0; valid_out <= 0; end
else begin
v1 <= valid;
valid_out <= v1;
if (valid) begin lo1 <= a[7:0] + b[7:0]; ah1 <= a[15:8]; bh1 <= b[15:8]; end
if (v1) sum <= {hi, lo1[7:0]};
end
end
endmodule
module sec_top(input clk, rst, valid, input [15:0] a, b);
wire [16:0] gold_sum, pipe_sum;
wire gold_valid, pipe_valid;
add_comb gold(.a(a), .b(b), .valid(valid), .sum(gold_sum), .valid_out(gold_valid));
add_pipe2 pipe(.clk(clk), .rst(rst), .valid(valid), .a(a), .b(b), .sum(pipe_sum), .valid_out(pipe_valid));
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
// modelling code: the gold's {valid, sum}, one and two cycles back
localparam LAT = 2;
reg [17:0] gold_q1 = 0, gold_q2 = 0;
always @(posedge clk) begin
gold_q1 <= rst ? 18'd0 : {gold_valid, gold_sum};
gold_q2 <= rst ? 18'd0 : gold_q1;
end
wire [17:0] gold_d = LAT == 1 ? gold_q1 : gold_q2;
always @(posedge clk) if (!rst) begin
assert(pipe_valid == gold_d[17]);
if (pipe_valid) assert(pipe_sum == gold_d[16:0]);
end
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
Misconception
"Combinational LEC failed after we recoded the FSM, so synthesis is broken."
Recoding changes the state encoding, so the flops no longer pair one to one, and a combinational check reports a mismatch. That change needs sequential equivalence.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 8 "Combinational equivalence", "Sequential equivalence"