Interview Question · Concept

Assert, Assume and Cover

L1 JuniorL2 Mid-Levelsvaassumecoverformal

Likely at Broadcom
Likely at Synopsys
Likely at Qualcomm

The interviewer asks

What is the difference between assert property, assume property and cover property? Does a simulator treat them differently from a formal tool?

Reveal the Model Answer

assert states a rule the design must obey. assume states a rule the environment, meaning the inputs, must obey. cover asks to see a scenario happen at least once. A simulator checks an assume just like an assert and reports when the stimulus breaks it. A formal tool uses the assume to limit the inputs it explores, and tries to prove each assert for all remaining inputs.

Who Each Directive Talks AboutArrows show signals moving from the environment through the design. Each directive watches one side.

Read the diagram as text

Environment: Stimulus or the neighbour block; drives the inputs
assume: Rules the inputs must obey
Design under test: Turns inputs into outputs
assert: Rules the design must obey
cover: A scenario we want to see at least once

Environment → assume: inputs
assume → Design under test: legal inputs
Design under test → assert: outputs
Design under test → cover: behaviour

The same three lines mean different work in each tool, as the table shows.

Directive	In a simulator	In a formal tool
`assert`	Reports each failure on the traffic that ran	Tries to prove it for every legal input
`assume`	Checked like an assert; reports stimulus that breaks it	Limits the inputs the tool explores
`cover`	Counts each time the scenario happens	Finds a trace that reaches it, or proves it cannot happen

Self-Check

Tick each key point you covered in your answer.

Key point 1 assert states a rule the design must obey. Key point 2 assume states a rule the environment, meaning the inputs, must obey. Key point 3 cover asks to see a scenario happen at least once. Key point 4 A simulator checks an assume just like an assert and reports when the stimulus breaks it. Key point 5 A formal tool uses the assume to limit the inputs it explores, and tries to prove each assert for all remaining inputs.

What Interviewers Listen For (Junior)

A good junior answer gives one example of each: a design rule, an input rule and a scenario. It says what the simulator reports for each one.

Cross-Questions

Where the interviewer goes next. Open a node to practise that follow-up.

WhyWhat IfBreak ItCompareScale It

Assert, Assume and Cover
WhyWhy Simulation Checks AssumptionsL1 JuniorL2 Mid-Level
Why would a simulator bother to check an assume, if it cannot use it to limit the inputs?

Reveal the Model Answer

The same file runs in formal and in simulation. If the simulation stimulus breaks an assumption, either the stimulus is wrong or the assumption is too strict. Both are worth knowing, because a too-strict assumption makes formal proofs too easy.

Self-Check
Tick each key point you covered in your answer.
Key point 1 The same file runs in formal and in simulation. Key point 2 If the simulation stimulus breaks an assumption, either the stimulus is wrong or the assumption is too strict. Key point 3 Both are worth knowing, because a too-strict assumption makes formal proofs too easy.

Misconception

"A violated assume in simulation means the design is broken."

An assume is about the inputs. A violation points at the stimulus or at the assumption itself, not at the design.

Source IEEE 1800-2017 §16.14.2
- Lesson A1.1Why Assertions
Break ItAn Assumption on an Internal SignalL2 Mid-Level
Break it: an assumption names an internal signal of the DUT. What goes wrong in formal and in simulation?

Reveal the Model Answer

In formal, the assumption removes behaviour the design can really produce. A bug that needs that behaviour then disappears from the proof. In simulation it fires only if the tests reach that state, and they may never do. Write assumptions on input ports only.

Self-Check
Tick each key point you covered in your answer.
Key point 1 In formal, the assumption removes behaviour the design can really produce. Key point 2 A bug that needs that behaviour then disappears from the proof. Key point 3 In simulation it fires only if the tests reach that state, and they may never do. Key point 4 Write assumptions on input ports only.

Tool as Truth

"The assumption never fired in simulation, so it is safe."

Simulation checks it only on the traffic it ran. A proof applies it to every trace, including ones no test reached.

Source Lesson F3.2 key points
- Lesson A1.1Why Assertions
- Lesson F3.2Over-Constraint and Vacuity

CompareAn Assume vs a Randomization ConstraintL2 Mid-Level

Compare assume property (req |=> !req) with a constraint in the stimulus class that never sends two requests in a row.

Reveal the Model Answer

The constraint shapes what the testbench generates. The assume states the same rule as a property. Formal tools use it to limit their inputs, and simulators check it against whatever the stimulus did. Keeping both lets the assume catch a stimulus that breaks the rule, for example a directed test that bypasses the constraint.

	Randomization constraint	`assume property`
Shapes	What the testbench generates	Nothing in simulation; it is checked
In formal	Not used	Limits the inputs the tool explores
Catches a directed test that breaks the rule	No	Yes

Self-Check

Tick each key point you covered in your answer.

Key point 1 The constraint shapes what the testbench generates. Key point 2 The assume states the same rule as a property. Key point 3 Formal tools use it to limit their inputs, and simulators check it against whatever the stimulus did. Key point 4 Keeping both lets the assume catch a stimulus that breaks the rule, for example a directed test that bypasses the constraint.

Tool as Truth

"A simulator can generate stimulus from the assume."

Standard simulation only checks an assume. Generating inputs from properties is a feature of formal tools and of some vendor extensions.

Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §15.1

Scale ItWhich Assertions Formal Tools Can UseL3 Senior
Your team writes many immediate assertions inside testbench classes. A formal lead asks to reuse the block's checks. What do you change?

Reveal the Model Answer

Formal tools work on the design and its bound checkers, not on class-based testbench code. Checks inside class methods cannot be reused there. Rewrite the interface rules as concurrent properties over DUT signals, in a checker module you can bind. Leave only transaction-level checks in the classes. The same file then runs in simulation as assertions and in formal as proof targets, with the input rules switched to assumptions.

Self-Check
Tick each key point you covered in your answer.
Key point 1 Formal tools work on the design and its bound checkers, not on class-based testbench code. Key point 2 Checks inside class methods cannot be reused there. Key point 3 Rewrite the interface rules as concurrent properties over DUT signals, in a checker module you can bind. Key point 4 Leave only transaction-level checks in the classes. Key point 5 The same file then runs in simulation as assertions and in formal as proof targets, with the input rules switched to assumptions.

What Interviewers Listen For (Senior)
A good senior answer splits rules on signals from checks on transactions. Signal rules are bound and shared with formal; transaction checks stay in classes. It also switches input rules from assert to assume.

Misconception

"Formal can read any assertion in the testbench."

Formal analyses synthesizable design logic plus properties over it; dynamic class objects and procedural testbench code are outside that model.

Source Lesson A7.1 review claims (bind; checkers outside the RTL)
- Lesson A7.1Packaging and Binding
- Lesson F1.1Simulation Covers Paths, Formal Covers States
What IfA Proof That Passed Because of an AssumeL2 Mid-LevelL3 Senior
Asked if they mention formal

What if a formal tool proves every assertion on the first try? What do you check before you trust it?

Reveal the Model Answer

Check that the covers are reachable. Add a cover for each important scenario and for each assertion's antecedent. If a cover is unreachable, an assumption has probably removed the inputs that lead there. Then the proof says nothing about those inputs.

Self-Check
Tick each key point you covered in your answer.
Key point 1 Check that the covers are reachable. Key point 2 Add a cover for each important scenario and for each assertion's antecedent. Key point 3 If a cover is unreachable, an assumption has probably removed the inputs that lead there. Key point 4 Then the proof says nothing about those inputs.

What Interviewers Listen For (Senior)
A good senior answer asks for cover results with every proof report. It reviews assumptions as carefully as RTL.

Misconception

"Proven means the design is correct."

Proven means correct for the inputs the assumptions allow. An over-strong assumption can allow almost none.

Source Seligman et al., Formal Verification (2nd ed.), ch. 9 "Vacuity issues"
- Lesson F3.2Over-Constraint and Vacuity

What People Get Wrong

Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.

Misconception

"Simulation ignores assume; it only matters in formal."

Simulators evaluate an assume like an assert. The twin breaks an input rule in the stimulus, and the simulator reports it.

Run It

A stimulus that breaks an assume on its inputs.

RUNVerilator · simulator service

Edit the code, then run it

Expected: assume violations=1 FAIL: simulation checks an assume like an assert, so the stimulus bug was reported

module tb;
  logic clk = 0, req = 0;
  int violations = 0;
  always #5 clk = ~clk;
  // The belief: assume is only for formal tools; simulation ignores it.
  env_rule: assume property (@(posedge clk) req |=> !req) else violations++;
  initial begin
    @(negedge clk) req = 1;
    @(negedge clk) req = 1;     // the stimulus breaks the environment rule
    @(negedge clk) req = 0;
    repeat (2) @(negedge clk);
    $display("assume violations=%0d", violations);
    if (violations) $display("FAIL: simulation checks an assume like an assert, so the stimulus bug was reported");
    $finish;
  end
endmodule

Half-Truth

"Add more assumes until the formal run passes."

Each assume removes inputs from the search. Too many can remove the very input that shows a bug, and the proof then passes for the wrong reason.

Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), ch. 15

Misconception

"Cover is just an assert with the opposite sense."

A failing assert reports a bug. A cover that never hits reports a hole in the stimulus. They answer different questions.

Source IEEE 1800-2017 §16.14.3

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.

Assert, Assume and Cover

Your Answer

Self-Check

What Interviewers Listen For (Junior)

What Interviewers Listen For (Mid-Level)

What Interviewers Listen For (Senior)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What Interviewers Listen For (Senior)

Your Answer

Self-Check

What Interviewers Listen For (Senior)

What People Get Wrong

Learn It, Then Prove It

The Question

Your Answer

Self-Check

What Interviewers Listen For (Junior)

What Interviewers Listen For (Mid-Level)

What Interviewers Listen For (Senior)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What Interviewers Listen For (Senior)

Your Answer

Self-Check

What Interviewers Listen For (Senior)

What People Get Wrong

Learn It, Then Prove It