← Formal Verification Interviews
Interview Question · Concept
Assert, Assume and Cover in Formal
- Likely at AMD
- Likely at Intel
The Question
The interviewer asks
In a formal run, what do assert, assume and cover each tell the tool to do?
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
An assertion is a goal: the tool searches for any legal input sequence that breaks it. An assumption is taken as true, so it removes input sequences from the search. A cover asks the tool to reach a condition and return a trace that does. The working rule is to assume what the environment does, assert what the design does and cover what should be possible.
Read the diagram as text
- No assumptions: every input value, every cycle
- The legal environment: assume what the spec promises
- Assume on outputs: or assumptions that contradict
- False failures: traces the real master never sends
- Real bugs only: every FAIL is reachable
- Nothing to check: the proof is empty
- No assumptions → False failures
- The legal environment → Real bugs only
- Assume on outputs → Nothing to check
Too few assumptions give false failures. Too many leave nothing to check. Covers catch the second case.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Fresher)
A good fresher answer defines the three verbs correctly. It says assumptions belong on inputs, and assertions on outputs and state.
What Interviewers Listen For (Mid-Level)
A good mid-level answer explains that an assumption on an output deletes the failing behaviour. It pairs every assumption with a cover. It knows that simulation checks an assume just like an assert.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItCompare
- Assert, Assume and Cover in Formal
-
WhyWhy Covers Come Before AssertsL1 Junior
Why should the first run on a new formal bench be covers, not assertions?
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 cover shows the design moving under your assumptions: reset releases, the FIFO fills, each state is entered. If the bench is over-constrained, the covers come back unreached before any assertion can mislead you with a pass. In this run the arbiter's output is assumed one-hot, and the cover of a double grant is unreached.
The cover trace: the shortest way to a double grant Measured with smtbmc yices. The tool builds the shortest input sequence that reaches the covered condition.
module arb3(input clk, rst, input [2:0] req, input [7:0] weight, output reg [2:0] gnt=0); reg lock=0; reg [1:0] reload=0; wire [2:0] pri = req[0] ? 3'b001 : req[1] ? 3'b010 : req[2] ? 3'b100 : 3'b000; wire hold = lock && |(req & gnt); always @(posedge clk) begin if (rst) begin gnt<=0; lock<=0; reload<=0; end else begin lock <= weight[7]; reload <= (weight == 8'hA5 && req == 3'b110) ? 2'd1 : (reload == 2'd1 && req == 3'b011) ? 2'd2 : 2'd0; if (reload == 2'd2 && req == 3'b111) gnt <= gnt | pri; // reload cycle: lock holds, encoder grants too else gnt <= hold ? gnt : pri; end end always @(posedge clk) begin if ($initstate) begin assume(rst); end else begin assume(!rst); end end always @(posedge clk) if (!rst) begin assume($onehot0(gnt)); cover(!$onehot0(gnt)); end endmodulePrints:
cover, depth 20 (smtbmc yices): FAIL, cover unreachedSelf-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F3.5.1: Ask for Three Directed TestsSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
What IfFormal Assumptions in SimulationL1 JuniorL2 Mid-Level
The same SVA file is compiled into the simulation testbench. What happens to the
assumeandcoverstatements there?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 simulator checks an
assumeexactly like anassert. So the system testbench tells you when the real environment breaks a block-level assumption. Covers are counted as they are hit, andrestrictis ignored. Binding block assumptions into system simulation is the cheapest way to validate them.Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F3.2.2: Restrict Is Still a PromiseSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
What IfA Block Assumption Fires in System SimulationL2 Mid-Level
What if a block assumption, bound into system simulation, fires on day 40? What does it tell you, and 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
The real neighbour broke a rule that the block proof relied on. So the block proof does not cover that traffic. Decide from the spec which side is wrong. Either fix the neighbour, or relax the assumption and rerun the proof, which may now fail.
Self-Check
Tick each key point you covered in your answer.
Misconception
"Turn the check off in simulation; formal already proved the block."
The proof holds only for inputs the assumption allows. The firing check shows real traffic outside that set, which no proof has seen.
Source Lesson F7.4 key points
-
CompareA Formal Cover vs a Covergroup BinL1 JuniorL2 Mid-Level
How does a formal
coverdiffer from a covergroup bin that simulation hits?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 covergroup bin counts what your tests happened to do. A formal cover asks whether any legal input sequence can reach the condition and returns the shortest trace that does. An unreached formal cover within a bound only says the depth was too short or an assumption blocks it. A proof of the negation is what makes a bin truly unreachable.
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
"Assuming and asserting the same property are both harmless checks."
An assumption is believed, not checked. Assuming $onehot0(gnt) on the arbiter's output removes every trace with a double grant, so the matching assertion passes and the bug disappears.
Run It
The buggy arbiter with $onehot0(gnt) both assumed and asserted. The fix asserts it only.
module arb3(input clk, rst, input [2:0] req, input [7:0] weight, output reg [2:0] gnt=0);
reg lock=0;
reg [1:0] reload=0;
wire [2:0] pri = req[0] ? 3'b001 : req[1] ? 3'b010 : req[2] ? 3'b100 : 3'b000;
wire hold = lock && |(req & gnt);
always @(posedge clk) begin
if (rst) begin gnt<=0; lock<=0; reload<=0; end
else begin
lock <= weight[7];
reload <= (weight == 8'hA5 && req == 3'b110) ? 2'd1 : (reload == 2'd1 && req == 3'b011) ? 2'd2 : 2'd0;
if (reload == 2'd2 && req == 3'b111) gnt <= gnt | pri; // reload cycle: lock holds, encoder grants too
else gnt <= hold ? gnt : pri;
end
end
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) begin
assume($onehot0(gnt));
assert($onehot0(gnt));
cover(!$onehot0(gnt));
end
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
See the Fix
module arb3(input clk, rst, input [2:0] req, input [7:0] weight, output reg [2:0] gnt=0);
reg lock=0;
reg [1:0] reload=0;
wire [2:0] pri = req[0] ? 3'b001 : req[1] ? 3'b010 : req[2] ? 3'b100 : 3'b000;
wire hold = lock && |(req & gnt);
always @(posedge clk) begin
if (rst) begin gnt<=0; lock<=0; reload<=0; end
else begin
lock <= weight[7];
reload <= (weight == 8'hA5 && req == 3'b110) ? 2'd1 : (reload == 2'd1 && req == 3'b011) ? 2'd2 : 2'd0;
if (reload == 2'd2 && req == 3'b111) gnt <= gnt | pri; // reload cycle: lock holds, encoder grants too
else gnt <= hold ? gnt : pri;
end
end
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) begin
assert($onehot0(gnt));
cover(!$onehot0(gnt));
end
endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 5
Misconception
"restrict is just another spelling of assume."
Formal tools treat both as constraints, but simulation checks an assume and ignores a restrict completely. Nothing ever tests the environment against a restriction.
Source IEEE 1800-2017 §16.2
Half-Truth
"The cover passed, so the feature works."
A reached cover shows that one trace exists. It says nothing about the other traces; that is what the assertion is for.