The Formal Verification Plan

Write the nine-field plan before the properties, fill it for a real block from measured results, and read it the way a lead reviews it.

Lesson: F7.5
Time: 20 min
Runs on: SymbiYosys
Check: 5 questions

A team proved properties for three months and arrived at review without a plan. Which spec rules were covered, which assumptions held, which proofs were bounded and how deep: every answer was in someone's shell history. The work was good, but nobody could review it.

Nine Fields on One Page

The template. Nine fields; the first five are written before any property, the rest as the work fills them.

FORMAL VERIFICATION PLAN            block: ________   rev: __   date: ________
1 Scope          RTL files, interfaces, what is left out and why
2 Goal           bug hunting | sign-off          (sets the exit criteria)
3 Spec rows      one row per rule: kind, source sentence
4 Properties     name, kind, spec row, form (SVA / immediate)
5 Assumptions    each: reason (spec row), who checks it in the system
6 Covers         behaviours that must be reachable, with target depth
7 Abstractions   each: what it drops, soundness note, faulty twin replayed
8 Depth budget   per property: full proof, or required depth + worksheet
9 Sign-off       the four Cs with the numbers they must show

The plan is the sign-off argument written before the work. Goal decides the exit criteria: bug hunting stops when the risky areas stop yielding bugs, sign-off stops when every field is closed. The structure is the same.

Two fields carry most of the judgment. Each assumption names who checks it in the system, because a block proof is only as good as its promises (F7.4). The depth budget says, per property, whether only a full proof will do or which bounded depth would count.

The Plan, Filled for the Spine FIFO

Field	fifo4sb, the 4 × 8 FIFO of F3.4
Scope	the whole RTL, memory kept at full width; push/pop interface
Goal	sign-off
Spec rows	bound, bookkeeping, data and order, acceptance; `rdata` while empty undefined (F7.2)
Properties	`a_count`, `a_empty`, `a_full`, `a_level`, `a_e2e`, `a_accept`
Assumptions	reset in step 0 only; a push when full is legal and refused, so none on inputs
Covers	one entry: step 3; full: step 6; full, push and pop together: step 6; full again after two reads: step 8
Abstractions	none
Depth budget	full proof (`abc pdr`, Prove PASS (abc pdr), 1.7 s). Bounded fallback: required 9 from the deepest cover, `bmc` 9: BMC PASS to depth 9; twice that, 18: no verdict in 20 s
Sign-off	all proofs full; covers reached; cone map covers the whole FIFO state (F7.1); mutation 36 of 36 killed, 40 edits, seed 7 (F7.2)

Every number is measured: the proof, covers and fallback for this plan, the cone map and mutation score from F7.1 and F7.2.

Read the depth budget: the bounded fallback stops being affordable well before twice the deepest cover. The plan therefore depends on the full proof, and says so before anyone discovers it at review.

Two Plans, One Difference

tmo_blk plan, no depth budget

Depth budget:  (blank)
Result:        TMO = 12, bmc depth 12: PASS

Not reviewable: PASS against nothing.

Same plan, budget filled

Depth budget:  required 17 (worksheet, F7.3)
Result:        bounded, depth 12, required 17: open

The reviewer asks for depth 17 or a proof: Prove PASS (abc pdr).

No run changed; one field did. The same bmc result (BMC PASS to depth 12) reads as a sign-off on the left and as an open item on the right, which is what it is.

The Questions a Lead Asks

Review question	Field that answers it
Which spec rows have no property?	Spec rows against Properties
Which assumptions has nobody checked in the system?	Assumptions (F7.4)
Which covers are unreached?	Covers
Which proofs are bounded, and is each above its budget?	Depth budget
Which abstractions were never replayed on a faulty twin?	Abstractions (F4.5)
What was the mutation sample?	Sign-off

A plan that answers all six can be signed. A question with no field, such as "which solver is fastest?", is a run-time fact, not a plan entry.

A Plan Lives Through the Whole ProjectWritten first, filled during bring-up, re-checked in regression, closed at review.

Read the diagram as text

Plan: scope, goal, spec rows, assumptions, exit criteria
Run: properties and covers written; first proofs; staging over-constraints listed
Regress: covers and proofs every night; cone map and mutation runs as milestones
Close: every field filled; open items named; the lead signs

Plan → Run
Run → Regress
Regress → Close
Regress → Run: a cover goes unreached

An over-constraint used to stage the work is a plan entry with a date to remove it, never a silent line in the bench.

Staging is normal: early runs often over-constrain on purpose to reach a first proof. The plan lists each such constraint with the milestone that removes it, and a cover shows the behaviour it blocked is reachable again.

Asked in Interviews

Question	Answer
What goes in a formal verification plan?	Scope, goal, spec rows, properties, assumptions with who checks them, covers, abstractions with soundness notes, a depth budget per property, and sign-off criteria.
What does a lead review in it?	The four Cs read off its fields: constraints, checkers, complexity, coverage. Every bounded result must sit next to its required depth.
Bug hunting or sign-off: what changes in the plan?	The goal field and the exit criteria. The fields stay the same.

Try It

The lab fills the plan for tmo_blk. The run behind its depth budget is the fixed block with TMO = 12 under abc pdr: Prove PASS (abc pdr) in 0.5 s.

Fill the first five fields
Scope, goal, the spec rows (accept, grant, timeout, error pulse), the no-lost-request property, and the assumptions: reset only.
Fill the rest from F7.3
Two covers (a grant, a timeout), no abstraction, the depth budget from the worksheet (required 17), and the sign-off line.
Review it
Answer the six review questions from your plan alone. Any question you cannot answer is a missing field.

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module tmo_blk(input clk, rst, req, grant_in, output reg pending = 0, output reg err = 0);
  localparam TMO = 12;
  reg [3:0] cnt = 0;      // waiting cycles
  reg late = 0;           // the cycle after a timeout
  always @(posedge clk)
    if (rst) begin pending <= 0; cnt <= 0; err <= 0; late <= 0; end
    else begin
      err <= 0;
      late <= 0;
      if (!pending) begin
        if (req) begin pending <= 1; cnt <= 0; end
      end else if (grant_in) pending <= 0;
      else if (cnt == TMO - 1) begin pending <= 0; err <= 1; end
      else cnt <= cnt + 4'd1;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg req_q = 0;           // registered copy: a request seen while idle
  always @(posedge clk) begin
    req_q <= !rst && req && !pending;
    if (!rst && req_q) assert(pending);
  end
`endif
endmodule

Check Yourself

Predict the outputThe spine with the four plan covers, mode cover, depth 20, smtbmc yices, reset assumed in step 0. SBY reports the deepest cover at step:

module fifo4sb(input clk, rst, push, pop, input [7:0] wdata,
  output [7:0] rdata, output full, empty);
  reg [7:0] mem [0:3];
  reg [1:0] wr_ptr=0, rd_ptr=0;
  reg [2:0] count=0;
  assign full  = count == 3'd4;
  assign empty = count == 3'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; end
    else begin
      if (wr_en) begin mem[wr_ptr] <= wdata; wr_ptr <= wr_ptr + 2'd1; end
      if (rd_en) rd_ptr <= rd_ptr + 2'd1;
      count <= count + wr_en - rd_en;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  wire [1:0] f_ptr_diff = wr_ptr - rd_ptr;   // entries between the pointers, modulo 4
  // Modelling code: a shadow copy of the FIFO's contents, in order, oldest in sb0.
  reg [7:0] sb0=0, sb1=0, sb2=0, sb3=0;
  reg [2:0] sb_n=0;
  wire [2:0] slot = sb_n - (rd_en ? 3'd1 : 3'd0);   // where an accepted push lands
  always @(posedge clk)
    if (rst) sb_n <= 0;
    else begin
      if (rd_en) begin sb0 <= sb1; sb1 <= sb2; sb2 <= sb3; end
      if (wr_en) case (slot)
        3'd0: sb0 <= wdata;  3'd1: sb1 <= wdata;  3'd2: sb2 <= wdata;  default: sb3 <= wdata;
      endcase
      sb_n <= sb_n + wr_en - rd_en;
    end
  always @(posedge clk) if (!rst) begin
    if (empty) assert(wr_ptr == rd_ptr);   // glue
    if (full)  assert(wr_ptr == rd_ptr);   // glue
    assert(count <= 3'd4);                 // glue
    assert(count == f_ptr_diff || count == 3'd4 && f_ptr_diff == 2'd0);   // glue
    if (pop && !empty) assert(rdata == sb0);   // end-to-end
    c_one: cover(count == 3'd1);
    c_full: cover(full);
    c_both: cover(full && push && pop);
    c_wrap: cover(full && rd_ptr == 2'd2);
  end
`endif
endmodule

ConceptA plan lists prove for every property, and two runs return base PASS with induction failing. What does the sign-off field say for those two?

Proven: the base case passed, so the property holds from reset for all time.Open: UNKNOWN is no proof; add an invariant or a bounded run with a worksheet.Bounded sign-off at the depth k that the induction run used, no worksheet.Failed: the induction step found a reachable trace that breaks the property.

ConceptWhich plan entry would a reviewer send back?

Abstraction: timer cut to 4 bits; adds behaviour; faulty twin replayed.Depth budget: required 17 from the worksheet; target prove; fallback depth 20.Assumption: rvalid never high two cycles running (checked by: nobody).Assumption: awvalid holds until awready (AXI spec; system bench checks it).

ConceptWhy is the plan written before the properties?

It replaces the properties, so far fewer of them have to be written later.The formal tools refuse to start any run until a plan file exists on disk.Only sign-off work needs one; bug hunting can skip the plan entirely.It fixes the rules, assumptions and exit criteria the work is reviewed against.

ConceptWhich question can a verification plan not answer?

Which solver is fastest on this block?Which spec rows have no property?Which assumptions has nobody checked?Which bounded proofs are below budget?

Remember

Write the plan first: scope, goal, spec rows, properties, assumptions, covers, abstractions, depth budget, sign-off criteria.
Every assumption names who checks it in the system; every bounded result sits next to its required depth.
One empty field can turn an honest open item into a false sign-off.
Bug hunting and sign-off share the fields and differ in goal and exit criteria.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.