A verification plan starts with a feature list: every behavior the specification promises, written as a verifiable statement. Three passes produce it: understand, extract every shall/must/will into a row, and hunt for what the specification does not say.
The third pass finds the most bugs. Undefined behavior and missing corners become ambiguity log entries, never guesses.
FEATURE EXTRACTION PASSES
Pass 1: Understand “What does this block do?”
Pass 2: Extract Every shall/must/will → one feature row
“FIFO shall assert full when count == DEPTH”
“Write to full FIFO shall be ignored”
Pass 3: Interrogate What is NOT specified?
“What happens on simultaneous push+pop at full?”
“Is read data valid the same cycle as pop?”
→ spec ambiguity log, NOT a guessGood row: “back-to-back writes at full rate for DEPTH+2 cycles trigger full exactly once” — stimulus plus check in one line.
Bad row: “FIFO works correctly” — not verifiable, not closeable, hides ten real features.
Each row maps to exactly one check and one or more coverage points. A row without a named check is not finished.
Not all features deserve equal effort. Rank by bug likelihood times bug cost: new logic, crossings, arbitration, and deep state rank high, while pass-through paths rank low.
The ranking decides the method. High likelihood and high cost earns random stimulus plus formal effort and the first schedule slot.
RISK MATRIX
Bug cost (silicon respin / field failure)
LOW HIGH
Bug LOW │ directed test, │ directed + assertions
likelihood │ low priority │ (cheap insurance)
─────┼──────────────────────┼─────────────────────────
HIGH │ constrained-random │ random + formal +
│ + coverage │ dedicated owner +
│ │ first on schedule
High-likelihood signals: new logic, CDC, arbitration, deep FSMs,
corner-heavy datapaths, anything the designer says “should be fine”VERIFICATION PLAN STRUCTURE
ID │ Feature │ Approach │ Coverage / Check │ Owner │ Status
──────┼──────────────────────┼───────────────────┼──────────────────────┼───────┼───────
F-001 │ full asserts at │ random + directed │ cp_count.full bin, │ SB │ open
│ count == DEPTH │ boundary test │ a_full_when_count │ │
F-002 │ write @ full ignored │ assertion + error │ a_no_push_full, │ SB │ open
│ │ injection test │ x_full_write cross │ │
F-003 │ data integrity, │ scoreboard, │ scoreboard compare │ SB │ open
│ in-order │ all tests │ count > 10k │ │
Rules:
- Approach names the methodology, not “test it”
- Coverage column names the bin/assertion — traceable to closure report
- Owner is a person, not a team
- Status is open / coded / passing / closed (closed = coverage hit + check active)Every Pass 3 question enters an ambiguity log with the date, who must answer, and the answer once given. Never resolve an ambiguity by reading the RTL: the RTL is under test, and matching it turns the checker into a tautology.
The plan is reviewed twice at minimum: before testbench coding starts, and before sign-off. Reviewers include the designer and, ideally, an engineer from outside the block.
Log entry: “Q-007: simultaneous push+pop at full — accept push? Asked arch 03-12. Answer 03-14: pop wins, push ignored, spec v1.3 updated.”
An answered ambiguity becomes a new feature row with its own check.
Unanswered ambiguities at sign-off are documented holes, not silent drops.
Gate 1, plan review: feature list against the spec walk-through, risk challenge, ambiguity triage. Exit: plan baselined.
Gate 2, mid-point health check: rows closed against schedule, spec changes folded in.
Gate 3, sign-off review: every row closed or waived with evidence attached.
Into the ambiguity log for the architect. The RTL must never answer it, since matching the RTL turns the checker into a tautology.
Not finished. A row without a named check cannot close, regardless of how precisely the feature reads.
A 4-deep FIFO carrying two plan rows: full asserts exactly at count equal to DEPTH, and a push at full is ignored. The checks below are the closable form of those rows.
module tiny_fifo #(
parameter int WIDTH = 8,
parameter int DEPTH = 4
) (
input logic clk,
input logic rst_n,
input logic push,
input logic pop,
input logic [WIDTH-1:0] wdata,
output logic [WIDTH-1:0] rdata,
output logic full,
output logic empty
);
localparam int AW = $clog2(DEPTH);
localparam int CW = $clog2(DEPTH + 1);
logic [WIDTH-1:0] mem [DEPTH];
logic [AW-1:0] wptr, rptr;
logic [CW-1:0] count;
logic do_push, do_pop;
assign do_push = push && !full;
assign do_pop = pop && !empty;
assign full = (count == DEPTH);
assign empty = (count == 0);
assign rdata = mem[rptr];
always @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
wptr <= '0;
rptr <= '0;
count <= '0;
end else begin
if (do_push) begin
mem[wptr] <= wdata;
wptr <= wptr + 1'b1;
end
if (do_pop) rptr <= rptr + 1'b1;
case ({do_push, do_pop})
2'b10: count <= count + 1'b1;
2'b01: count <= count - 1'b1;
default: count <= count;
endcase
end
end
endmodule