ASIC Point Explore

← Formal Verification Interviews

Interview Question · Code Reading

Over-Constraint and Vacuous Proofs

L1 JuniorL2 Mid-Levelassumptionsvacuity

The interviewer asks

Your FIFO bench has the two lines below, and the proof passes. A colleague distrusts the assumption. What can it hide, and how would you show it?

systemverilog
always @(posedge clk) if (!rst) begin
  assume(!(push && count == 5'd16));
  assert(count <= 5'd16);
end
Reveal the Model Answer

An assumption deletes every input sequence that breaks it. So an assumption stronger than the real environment deletes legal behaviour along with the bug. The proof is then true of a world the chip never sees. Write assumptions only on ports, from the spec, and pair each with a cover of behaviour it should still allow. An unreached cover is the alarm.

Two Assumptions, Two Different WorldsThe same intent, "the producer never pushes into a full FIFO", written against two signals. Arrows mean "leaves the solver".
Two assumptions, two different worldsThe same intent, "the producer never pushes into a full FIFO", written against two signals. Arrows mean "leaves the solver". component No assumption pushes into a fullFIFO allowed component assume(!(push&& full)) reads the port theproducer can see component assume(!(push&& count ==16)) reads a register theproducer cannot see component False failures illegal producers(F3.3) component Every legalproducer including the one thatpushes in the lagcycle component Every legalproducer but one the push that breaksthe FIFO is gone
Read the diagram as text
  • No assumption: pushes into a full FIFO allowed
  • assume(!(push && full)): reads the port the producer can see
  • assume(!(push && count == 16)): reads a register the producer cannot see
  • False failures: illegal producers (F3.3)
  • Every legal producer: including the one that pushes in the lag cycle
  • Every legal producer but one: the push that breaks the FIFO is gone
  • No assumption → False failures
  • assume(!(push && full)) → Every legal producer
  • assume(!(push && count == 16)) → Every legal producer but one

The right-hand zone is over-constraint: the proof is true, of a world the hardware never lives in. A pass looks the same in both right-hand columns. A cover does not.

Where the internal assumption cuts

The honest run, steps 16 to 18. The internal assumption forbids the push at step 17; the honest one allows it, because full is still 0.

  1. push=1, pop=0

    count=15, full=0

    count <= 16 holds

    ✓ Holds

  2. push=1, pop=0

    count=16, full=0

    internal assumption: no push here

    Assumed for induction

  3. push=0, pop=0

    count=17, full=1

    count <= 16 fails

    × Fails

Select a frame to inspect its inputs and assertion.

The honest run, steps 16 to 18. The internal assumption forbids the push at step 17, so its proof never sees the failure.

Self-Check

Tick each key point you covered in your answer.

What Interviewers Listen For (Junior)

A good junior answer explains that assumptions remove behaviour. It suggests a cover to check that an assumption is not too strong.

Cross-Questions

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

WhyWhat IfProve ItCompareScale It

  1. Over-Constraint and Vacuous Proofs
  2. WhyWhy Assumptions Belong on PortsL1 JuniorL2 Mid-Level

    Why should assumptions be written on the block's ports and never on its internal state?

    Reveal the Model Answer

    The neighbouring block can only promise things it can see, which are the ports. A rule about internal state is a claim about the design itself, so it should be asserted and proven. Assumed instead, it can quietly delete the very states where the bug lives.

    Self-Check

    Tick each key point you covered in your answer.

  3. Prove ItA Cover That Exposes an Over-ConstraintL1 JuniorL2 Mid-Level

    You keep the suspect assumption and replace the assertion with the covers below. What do you expect back, and what does it prove?

    systemverilog
    always @(posedge clk) if (!rst) begin
  assume(!(push && count == 5'd16));
  c_full:      cover(full);
  c_push_at16: cover(count == 5'd16 && push);
  c_pop_empty: cover(pop && empty);
end
    Reveal the Model Answer

    Keep the suspect assumption and replace the assertion with three covers. They are the FIFO full, a push while the count is 16, and a pop while empty. The full and pop-on-empty covers are reached, at steps 19 and 2. The push at a count of 16 is unreached, which is exactly the behaviour the assumption deleted.

    Three Reasons a Cover Is UnreachedCheck them in this order. The cover result cannot tell them apart; you can. Arrows mean "if not, check".
    call: who calls whom
    Three reasons a cover is unreachedCheck them in this order. The cover result cannot tell them apart; you can. Arrows mean "if not, check". component 1. The depth the trace needs moresteps than the taskallows component 2. An assumption it removed everysequence thatreaches the state(F3.2) component 3. Dead logic no input sequencereaches it: a bug, or aregister to delete component Raise the depth count the steps fromreset first component Read theassumptions delete leftovers;justify the rest component Read the RTL find the conditionthat contradictsitself
    Read the diagram as text
    • 1. The depth: the trace needs more steps than the task allows
    • 2. An assumption: it removed every sequence that reaches the state (F3.2)
    • 3. Dead logic: no input sequence reaches it: a bug, or a register to delete
    • Raise the depth: count the steps from reset first
    • Read the assumptions: delete leftovers; justify the rest
    • Read the RTL: find the condition that contradicts itself
    • 1. The depth → 2. An assumption
    • 2. An assumption → 3. Dead logic
    • 1. The depth → Raise the depth
    • 2. An assumption → Read the assumptions
    • 3. Dead logic → Read the RTL

    Each reason has its own fix, and the depth is the cheapest one to rule out.

    module fifo16(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output empty, output reg full=0);
  reg [7:0] mem [0:15];
  reg [3:0] wr_ptr=0, rd_ptr=0;
  reg [4:0] count=0;
  assign empty = count == 5'd0;
  wire wr_en = push && !full, rd_en = pop && !empty;
  assign rdata = mem[rd_ptr];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; full <= 0; end
    else begin
      if (wr_en) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 4'd1; end
      if (rd_en) rd_ptr <= rd_ptr + 4'd1;
      count <= count + wr_en - rd_en;
      full <= count == 5'd16;   // bug: one cycle behind count
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assume(!(push && count == 5'd16));
    c_full:      cover(full);
    c_push_at16: cover(count == 5'd16 && push);
    c_pop_empty: cover(pop && empty);
  end
`endif
endmodule

    Prints: cover, depth 20 (smtbmc yices): FAIL at step 19, cover unreached

    Self-Check

    Tick each key point you covered in your answer.

  4. Prove ItSolve F3.2.1: The Assumption That Hides the OverflowSimulator-graded

    Show it, don't just say it: this Silicon Lab problem is graded by the simulator.

    Open Problem F3.2.1

  5. What IfTwo Assumptions That ContradictL2 Mid-Level

    Asked if they mention the tool's conflict check

    What happens if two of your assumptions contradict each other at some point in a trace?

    Reveal the Model Answer

    From that point on no legal trace exists, so every assertion that needs to look past it passes for nothing. Some tools report a conflict when the assumptions are unsatisfiable from reset, but not every case is caught. Covers of normal behaviour after that point are the reliable check.

    Self-Check

    Tick each key point you covered in your answer.

  6. Prove ItFinding the Conflicting AssumptionsL2 Mid-Level

    Prove it: how do you find which assumptions conflict when the tool does not report it?

    Reveal the Model Answer

    Add covers of normal behaviour at growing depths, and find where they stop being reached. Then disable assumptions one at a time and rerun the covers. An assumption whose removal brings them back is part of the conflict. Fix it from the spec, and keep the covers as a standing check.

    Self-Check

    Tick each key point you covered in your answer.

    Misconception

    "Every assertion passed, so the assumptions must be consistent."

    After a conflict no legal trace exists, so every assertion passes for nothing. The passes are the symptom, not the evidence.

    Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 9 "Vacuity issues"

  7. CompareUnder-Constraint vs Over-ConstraintL1 JuniorL2 Mid-Level

    Compare under-constraint and over-constraint. Which one is more dangerous?

    Reveal the Model Answer

    Under-constraint gives false failures: they cost debug time, but every one is visible in a trace. Over-constraint gives false passes, which look exactly like real ones. Over-constraint is the dangerous one, and covers under the full assumption set are the only routine defence against it.

    Self-Check

    Tick each key point you covered in your answer.

  8. Scale ItReviewing Assumptions at Sign-OffL3 Senior

    How do you review the assumptions of a block-level formal sign-off?

    Reveal the Model Answer

    List every assumption with its spec row and a cover showing legal behaviour survives it. Also list where it is checked at system level, usually a bound assertion in simulation. Anything without a spec row is either removed or escalated as a design requirement. The review signs off the list, not the proof.

    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 !(push && count == 16) is the same as assuming no push while full."

This FIFO raises full one cycle late. The internal assumption forbids exactly the push that overflows in that cycle, so the run passes; the port assumption fails at step 19.

Run It

The FIFO from lesson F3.2, with the assumption written on the internal count.

module fifo16(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output empty, output reg full=0);
  reg [7:0] mem [0:15];
  reg [3:0] wr_ptr=0, rd_ptr=0;
  reg [4:0] count=0;
  assign empty = count == 5'd0;
  wire wr_en = push && !full, rd_en = pop && !empty;
  assign rdata = mem[rd_ptr];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; full <= 0; end
    else begin
      if (wr_en) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 4'd1; end
      if (rd_en) rd_ptr <= rd_ptr + 4'd1;
      count <= count + wr_en - rd_en;
      full <= count == 5'd16;   // bug: one cycle behind count
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assume(!(push && count == 5'd16));
    assert(count <= 5'd16);
  end
`endif
endmodule

Prints: bmc, depth 20 (smtbmc yices): PASS

See the Fix
module fifo16(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output empty, output reg full=0);
  reg [7:0] mem [0:15];
  reg [3:0] wr_ptr=0, rd_ptr=0;
  reg [4:0] count=0;
  assign empty = count == 5'd0;
  wire wr_en = push && !full, rd_en = pop && !empty;
  assign rdata = mem[rd_ptr];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; full <= 0; end
    else begin
      if (wr_en) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 4'd1; end
      if (rd_en) rd_ptr <= rd_ptr + 4'd1;
      count <= count + wr_en - rd_en;
      full <= count == 5'd16;   // bug: one cycle behind count
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assume(!(push && full));
    assert(count <= 5'd16);
  end
`endif
endmodule

Prints: bmc, depth 20 (smtbmc yices): FAIL at step 19

Misconception

"restrict is safer than assume because simulation ignores it."

The prover treats it exactly like an assumption, so it hides the same bug, and simulation never checks it. In the lesson restrict(count < 16) also passes to depth 20.

Source IEEE 1800-2017 §16.2; ASIC Point lesson F3.2 (measured)

Buzzword Without Mechanism

Says "check for vacuity" but cannot say how.

The how is concrete. Write one cover per assumption for the behaviour it should still allow, and read it as reached or unreached. Add the tool's conflict check.

Learn It, Then Prove It