Part 8 · Senior & Interview Prep · Intermediate

Step 5: Assertions & Coverage

Bound assertion module (no-push-full, no-pop-empty, count consistency, data integrity with local vars) and the closure covergroup — complete code.

Bound assertion module — complete code

The checker is a separate module attached with bind — the RTL is never edited, and the checker rides along to any level where the FIFO instantiates. It keeps its own occupancy model (a simple counter) so the count-consistency check is independent of the DUT's internal count.

systemverilog

module fifo_sva #(parameter int WIDTH = 8, parameter int DEPTH = 16) (
  input logic             clk, rst_n,
  input logic             in_valid, in_ready,
  input logic [WIDTH-1:0] in_data,
  input logic             out_valid, out_ready,
  input logic [WIDTH-1:0] out_data,
  input logic             full, empty
);
  wire push = in_valid  && in_ready;
  wire pop  = out_valid && out_ready;

  // independent occupancy model
  int count;
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) count <= 0;
    else        count <= count + (push && !pop) - (pop && !push);

  default clocking cb @(posedge clk); endclocking
  default disable iff (!rst_n);

  // F-04: flag definitions (combinational mirrors)
  a_ready_def: assert property (in_ready  == !full);
  a_valid_def: assert property (out_valid == !empty);

  // F-02/F-03: flags exactly track the model count
  a_full_def:  assert property (full  == (count == DEPTH));
  a_empty_def: assert property (empty == (count == 0));

  // F-05/F-06: boundary protection
  a_no_push_full: assert property (full  |-> !push);
  a_no_pop_empty: assert property (empty |-> !pop);

  // count stays in range — catches model/DUT divergence immediately
  a_count_range: assert property (count inside {[0:DEPTH]});

  // F-01: data integrity with a local variable — a word pushed into an
  // empty FIFO must be the very next word popped, unmodified.
  // (Full in-order checking across all fill levels is the scoreboard's
  //  job; this assertion anchors the data path cycle-accurately.)
  property p_data_integ_empty;
    logic [WIDTH-1:0] d;
    (push && empty && !pop, d = in_data)   // capture the word at push
      |-> (pop [->1]) ##0 (out_data == d); // first pop returns exactly it
  endproperty
  a_data_integ_empty: assert property (p_data_integ_empty);

  // coverage hooks for the corner features
  c_simul:      cover property (push && pop);              // F-07
  c_simul_full: cover property (full && pop && in_valid);  // F-08 attempt
endmodule

// in tb_top or a bind file — attach to EVERY fifo instance:
bind fifo fifo_sva #(.WIDTH(WIDTH), .DEPTH(DEPTH)) u_sva (
  .clk(clk), .rst_n(rst_n),
  .in_valid(in_valid),   .in_ready(in_ready),   .in_data(in_data),
  .out_valid(out_valid), .out_ready(out_ready), .out_data(out_data),
  .full(full), .empty(empty)
);

Code walkthrough

push/pop are defined once as handshake terms — every property reads like the spec sentence it checks.
The independent count means a_full_def cross-checks the DUT against the spec, not against itself.
default clocking + default disable iff keep each assertion one readable line.
The data-integrity property uses a local variable to capture in_data at push; the simple form (push into empty FIFO → first pop returns it) is the tool-friendly anchor — full ordering is the scoreboard's job.
cover property on the F-07/F-08 corners — proof the scenarios occurred, paired with the assertions that they were legal.

Closure covergroup — complete code

systemverilog

class fifo_cov #(parameter int WIDTH = 8, parameter int DEPTH = 16);
  virtual fifo_if #(WIDTH) vif;
  int count;                       // mirror of occupancy, sampled per cycle
  bit was_full_backpressure;

  covergroup cg @(vif.mon_cb);     // clocking event: samples pre-edge values
    option.per_instance = 1;

    // fill levels including EXACT boundaries (F-02/F-03 closure)
    cp_count: coverpoint count {
      bins empty       = {0};
      bins one         = {1};
      bins mid         = {[2:DEPTH-2]};
      bins almost_full = {DEPTH-1};
      bins full        = {DEPTH};
    }

    // cycle operation
    cp_op: coverpoint {vif.mon_cb.in_valid && vif.mon_cb.in_ready,
                       vif.mon_cb.out_valid && vif.mon_cb.out_ready} {
      bins idle  = {2'b00};
      bins push  = {2'b10};
      bins pop   = {2'b01};
      bins both  = {2'b11};        // F-07 simultaneity
    }

    // flag observation
    cp_flags: coverpoint {vif.mon_cb.full, vif.mon_cb.empty} {
      bins normal = {2'b00};
      bins full_  = {2'b10};
      bins empty_ = {2'b01};
      illegal_bins both_flags = {2'b11};   // full && empty is impossible
    }

    // the cross that closes the corner inventory
    x_op_state: cross cp_op, cp_count {
      bins push_at_almost_full = binsof(cp_op.push) && binsof(cp_count.almost_full);
      bins both_at_full        = binsof(cp_op.both) && binsof(cp_count.full);    // F-08
      bins pop_to_empty        = binsof(cp_op.pop)  && binsof(cp_count.one);
      bins both_mid            = binsof(cp_op.both) && binsof(cp_count.mid);     // F-07
    }

    // backpressure scenario (F-10): full while producer still offering
    cp_backpressure: coverpoint
      (vif.mon_cb.full && vif.mon_cb.in_valid && !vif.mon_cb.out_ready) {
      bins seen = {1};
    }
  endgroup

  function new(virtual fifo_if #(WIDTH) vif);
    this.vif = vif;
    cg = new();
  endfunction

  task run();                      // maintain the occupancy mirror
    forever begin
      @(vif.mon_cb);
      if (!vif.rst_n) count = 0;
      else count += (vif.mon_cb.in_valid && vif.mon_cb.in_ready)
                  - (vif.mon_cb.out_valid && vif.mon_cb.out_ready);
    end
  endtask
endclass

Coverage design notes

Boundary bins are separate (empty, one, almost_full, full) — a mid-range bucket hiding DEPTH-1 would fake closure on the off-by-one zone.
illegal_bins both_flags turns an impossible state into an immediate error — coverage and checking in one line.
The x_op_state cross is the corner inventory from step 1, bin for bin — plan rows F-07/F-08 close here.
Sampling is clocked on mon_cb — pre-edge values, consistent with assertions and monitors.

Key takeaways

bind keeps the checker out of the RTL and carries it to every level for free.
An independent occupancy model makes flag checks spec-vs-DUT, not DUT-vs-itself.
Local variables capture per-attempt data (the pushed word) inside properties.
Boundary fill levels get their own bins; the op×state cross closes the corner inventory.

Common pitfalls

Checking full against the DUT's own internal count — a tautology that always passes.
One coarse fill-level bin — DEPTH-1 vs DEPTH bugs hide inside it.
Forgetting default disable iff — reset cycles spray false assertion failures.
Cover-property corners with no paired assertion — the scenario ran, but nothing checked it.

Practice this lesson