Assign one method per feature class

No single methodology wins. A senior engineer assigns methods per feature class: constrained-random is the workhorse for state-rich datapaths, directed nails bring-up and exact scenarios, and emulation buys raw cycles for long software-driven runs.

Formal proves properties exhaustively over the state space and time, for the proven properties only. Its capacity is bounded by state explosion, so it fits small deep logic such as handshakes, arbiters, and FIFO control.

METHODOLOGY DECISION MATRIX

  Feature class            │ Directed │ Random  │ Formal  │ Emulation
  ─────────────────────────┼──────────┼─────────┼─────────┼──────────
  Bring-up / smoke         │   ●●●    │    ○    │    ○    │    ○
  Datapath w/ many states  │    ○     │   ●●●   │    ○    │    ●
  Arbitration fairness     │    ○     │   ●●    │   ●●●   │    ○
  CDC handshakes           │    ○     │    ●    │   ●●●   │    ○
  FIFO/counter properties  │    ●     │   ●●    │   ●●●   │    ○
  Register access          │   ●●     │   ●●    │    ●    │    ○
  Error injection          │   ●●●    │   ●●    │    ●    │    ○
  Performance / QoS        │    ○     │   ●●    │    ○    │   ●●●
  SW boot / long scenarios │    ○     │    ○    │    ○    │   ●●●

  ●●● primary   ●● strong   ● useful   ○ poor fit

  Rule of thumb: formal where state is deep but logic is small;
  random where the input space is wide; directed where the
  scenario is exact; emulation where you need millions of cycles.

• Directed gives exact control and fast bring-up, with zero discovery power. Use it for smoke, spec-mandated sequences, and bug reproduction.

• Constrained-random discovers unplanned combinations, but means nothing without a scoreboard and coverage. Use it for wide input spaces.

• Formal is exhaustive within its proven bounds, not over every input ever. Attempting it on a wide datapath burns weeks on state explosion.

• Emulation runs at megahertz with poor visibility and costly debug. Reserve it for software bring-up and performance scenarios simulation cannot reach.

The next listing is a checker module with no testbench, so this course's checks do not run it. The property itself is plain SVA: Verilator 5.048 runs it in simulation with --assert, and a formal tool can prove it.

1
2
3
4
5
6
7
8
9
10
11

// not-run: fragment: a checker module with no testbench top
module arb_fairness_fv (
  input logic clk,
  input logic rst_n,
  input logic [3:0] req,
  input logic [3:0] gnt
);
  // requester 0 is granted within 8 cycles of raising req
  assert property (@(posedge clk) disable iff (!rst_n)
    $rose(req[0]) |-> ##[1:8] gnt[0]);
endmodule

Verify once, at the cheapest level

The same feature is verified once, at the cheapest level that can observe it. Block testbenches own exhaustive corner work; top level owns integration, not block internals.

LEVEL RESPONSIBILITIES

  BLOCK level (this course's FIFO capstone)
    - All corner cases: full/empty boundaries, reset mid-traffic
    - Full constrained-random with per-block coverage closure
    - Bound assertion modules on internal signals
    └─ cheapest debug, fastest sims, full control

  SUBSYSTEM level (e.g. memory controller + arbiter + FIFOs)
    - Inter-block protocols, backpressure propagation
    - Realistic traffic patterns block TBs cannot generate
    - Re-uses block agents in passive/monitor mode

  TOP level (full chip)
    - Connectivity, address map, clocks/resets/power
    - End-to-end flows: DMA writes memory, CPU reads it
    - NOT the place to chase a FIFO boundary bug
    └─ slowest sims, debug costs 10x block level

Design checkers for passive reuse

Reuse is planned, not hoped for. Monitors, scoreboards, assertion modules, and coverage written at block level run unmodified at higher levels in passive mode, still checking while the block drivers are gone.

Checkers must therefore never depend on driver-side knowledge. At top level there is no driver, only DUT traffic.

• Interfaces and bound assertion modules attach to RTL instances and follow the block upward for free.

• Monitors and scoreboards keyed off pins, not driver intent, work passively at any level.

• Generators and sequences are block-testbench only, so each level plans its own stimulus.

• Vertical reuse is a plan-review item with a written answer naming which checkers ride upward.

Common mistakes

Testbench

One toy FIFO, one checker, two stimulus styles. Directed phases hit the full and empty boundaries exactly; a seeded hammer then pounds unplanned mixes through the same scoreboard, with manual bins recording what ran.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

module toy_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

Related topics

• Spec to Verification Plan

• Q&A: verification scenarios