One failure line, one cycle, one bug

A failing run gives you one line: [75000] %Error: hs_fifo_sva.sv:10: Assertion failed in tb_hs_fifo.dut.chk.a_out_hold. Turning it into a fix takes two skills: knowing exactly which edges each operator checks, and walking back from the failure time to the line of RTL that caused it.

Part 1 is a one-page reference for the first skill. Part 2 practises the second on a FIFO with a seeded bug. The picture shows the distinction most misreadings come from.

Each column is one rising edge of clk. A property sees only the values sampled at those edges.

• Edge 1, `|->`: ack must be high at the same edge as req. It is low, so req |-> ack fails at edge 1.

• Edge 2, `|=>`: ack must be high at the next edge. It is low, so req |=> ack fails at edge 2.

• Edges 2 to 4, `##[1:3]`: the window opens one edge after req. The ack at edge 3 is inside it, so the property passes and the attempt ends there.

Part 1: the cheat sheet

Every example is written on a 4-phase handshake: req rises, ack answers, req falls, then ack falls. In real code each property names its clock and carries disable iff (!rst_n); the table leaves both out to stay short.

Rows marked not run here are standard SVA, but the simulator used for this lesson rejected them or gave a wrong verdict on a short test trace. Check them on your own tool before relying on them. Every other example was run on a passing and a failing handshake trace.

Part 2: the bug hunt

The design is a four-entry FIFO with valid/ready on both sides and a registered output stage. load moves the oldest stored word into out_data when the stage is empty or is being emptied this cycle.

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

`timescale 1ns/1ps
// Four-entry FIFO, valid/ready on both sides, registered output stage.
module hs_fifo #(parameter int W = 8) (
  input  logic         clk, rst_n,
  input  logic         in_valid,
  output logic         in_ready,
  input  logic [W-1:0] in_data,
  output logic         out_valid,
  input  logic         out_ready,
  output logic [W-1:0] out_data
);
  logic [W-1:0] mem [4];
  logic [1:0]   wp, rp;
  logic [2:0]   count;                          // words in mem (out_data not counted)
  wire in_fire = in_valid && in_ready;
  wire load    = (count != 0) && (!out_valid || out_ready);   // refill the output stage
  assign in_ready = (count != 3'd4);
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) begin
      wp <= '0; rp <= '0; count <= '0; out_valid <= 1'b0; out_data <= '0;
    end else begin
      if (in_fire) begin mem[wp] <= in_data; wp <= wp + 2'd1; end
      if (load) begin
        out_data <= mem[rp]; rp <= rp + 2'd1; out_valid <= 1'b1;
      end else if (out_ready) out_valid <= 1'b0;
      count <= count + {2'b0, in_fire} - {2'b0, load};
    end
endmodule

The checker holds four assertions and two covers. It is bound into the FIFO, so the RTL file stays free of verification code.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

// not-run: concurrent assertions need Verilator (--binary --timing --assert); Icarus 13 cannot parse them
`timescale 1ns/1ps
// Bound into every hs_fifo. Each property names its clock (no default clocking block).
module hs_fifo_sva (
  input logic       clk, rst_n, in_valid, in_ready, out_valid, out_ready,
  input logic [7:0] out_data,
  input logic [2:0] count
);
  // 1. Under back-pressure the output holds: valid stays up and data does not change.
  a_out_hold: assert property (@(posedge clk) disable iff (!rst_n)
    out_valid && !out_ready |=> out_valid && $stable(out_data));
  // 2. Valid only drops after a transfer.
  a_valid_drop: assert property (@(posedge clk) disable iff (!rst_n)
    $fell(out_valid) |-> $past(out_ready));
  // 3. A word accepted into an empty FIFO is offered one to three cycles later.
  a_latency: assert property (@(posedge clk) disable iff (!rst_n)
    in_valid && in_ready && count == 0 && !out_valid |-> ##[1:3] out_valid);
  // 4. Never more than four stored words.
  a_count: assert property (@(posedge clk) disable iff (!rst_n) count <= 3'd4);
  // Covers for the antecedents that matter (counted by formal or --coverage).
  c_stall: cover property (@(posedge clk) disable iff (!rst_n) out_valid && !out_ready);
  c_full:  cover property (@(posedge clk) disable iff (!rst_n) !in_ready);
endmodule

• `a_out_hold` is the ready/valid rule: under back-pressure, valid stays up and the data does not change.

• `a_valid_drop`: valid falls only after an edge where the word was taken.

• `a_latency`: a word that enters an empty FIFO is offered one to three edges later. The antecedent is narrow on purpose: a plain in_valid && in_ready |-> ##[1:3] out_valid is satisfied by any older word already in the output stage.

• `a_count`: occupancy never exceeds four.

The seeded bug

One edit drops the back-pressure term from load. It is an easy slip when a FIFO first gets a registered output.

// snippet: line 16 of hs_fifo.sv, before and after the seeded bug
  wire load    = (count != 0) && (!out_valid || out_ready);   // correct
  wire load    = (count != 0);                                  // seeded bug

$ verilator --binary --timing --assert -Wno-fatal --top-module tb_hs_fifo hs_fifo.sv hs_fifo_sva.sv tb_hs_fifo.sv
$ obj_dir/Vtb_hs_fifo
[75000] %Error: hs_fifo_sva.sv:10: Assertion failed in tb_hs_fifo.dut.chk.a_out_hold: 'assert' failed.
%Error: hs_fifo_sva.sv:10: Verilog $stop
Aborting...

From the failure line to the root cause

1. Read the time in the right unit. The time is printed in the precision unit, 1 ps here, so 75000 is 75 ns. Rising edges fall at 5, 15, 25 ns and so on, so the failure is the edge at 75 ns.

2. Find the antecedent edge. a_out_hold uses |=>, so the failure is reported at the consequent edge. The antecedent held one edge earlier, at 65 ns: out_valid high and out_ready low.

3. Print those edges. The bench's +trace option shows the sampled values (below). At 65 ns the output is stalled holding 02, yet load is 1.

4. Follow the changed signal to its driver. out_data is written only under if (load), so the question becomes why load is 1 during a stall. Its expression has no out_ready term: the stage refills even though its word has not been taken.

5. Fix it and re-run the same seed.

$ obj_dir/Vtb_hs_fifo +trace
25 ns: out_valid=0 out_ready=0 out_data=00 count=0 load=0
35 ns: out_valid=0 out_ready=0 out_data=00 count=0 load=0
45 ns: out_valid=0 out_ready=0 out_data=00 count=1 load=1
55 ns: out_valid=1 out_ready=1 out_data=01 count=1 load=1
65 ns: out_valid=1 out_ready=0 out_data=02 count=1 load=1
[75000] %Error: hs_fifo_sva.sv:10: Assertion failed in tb_hs_fifo.dut.chk.a_out_hold: 'assert' failed.

Word 02 is overwritten at 75 ns without ever being transferred. The scoreboard would catch the loss too, but later and further from the cause; the assertion names the edge. With the (!out_valid || out_ready) term restored, the same seed runs clean:

$ obj_dir/Vtb_hs_fifo
sent 1010, received 1010, scoreboard errors 0, stall cycles 987, full cycles 687
PASS: all words in order, every assertion held, stall and full both covered

A checker is only useful if each property can fail. Each of the other three assertions was also made to fire, by a mutant of its own: valid dropped during a stall, room for a fifth word, and a refill that waits for three stored words.

Common mistakes

$ obj_dir/Vtb_hs_fifo +nostall
sent 1495, received 1495, scoreboard errors 0, stall cycles 0, full cycles 0
[20130000] %Fatal: tb_hs_fifo.sv:47: Assertion failed in tb_hs_fifo: FAIL: no stall cycle, so a_out_hold was never exercised

Testbench

The bench drives a legal source (valid and data hold until accepted) and a random sink, checks order with a scoreboard, and counts stall and full cycles. +trace prints the first edges and +nostall holds out_ready high.

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
44
45
46
47
48
49
50
51
52
53

// not-run: needs hs_fifo and hs_fifo_sva and Verilator (--binary --timing --assert); Icarus 13 cannot parse the bound assertions
`timescale 1ns/1ps
module tb_hs_fifo;
  logic clk = 0, rst_n = 0;
  logic in_valid = 0, out_ready = 0, in_ready, out_valid;
  logic [7:0] in_data = 0, out_data, expect_q [$];
  int sent = 0, got = 0, errors = 0, stalls = 0, fulls = 0;
  bit nostall, trace;
  hs_fifo dut (.*);
  bind hs_fifo hs_fifo_sva chk (.clk, .rst_n, .in_valid, .in_ready, .out_valid,
                                .out_ready, .out_data, .count);
  always #5 clk = ~clk;

  // Scoreboard and event counts, on the values sampled at each edge.
  always @(posedge clk) if (rst_n) begin
    if (in_valid && in_ready) begin expect_q.push_back(in_data); sent++; end
    if (out_valid && out_ready) begin
      if (expect_q.size() == 0 || out_data !== expect_q[0]) errors++;
      if (expect_q.size() != 0) void'(expect_q.pop_front());
      got++;
    end
    if (out_valid && !out_ready) stalls++;                // the antecedent of a_out_hold
    if (!in_ready) fulls++;
    if (trace && $time <= 80)
      $display("%0d ns: out_valid=%b out_ready=%b out_data=%h count=%0d load=%b",
               $time, out_valid, out_ready, out_data, dut.count, dut.load);
  end

  // Legal source: in_valid and in_data hold until accepted. Random sink.
  initial begin
    nostall = $test$plusargs("nostall");
    trace   = $test$plusargs("trace");
    repeat (2) @(negedge clk);
    rst_n = 1;
    repeat (2000) begin
      @(negedge clk);
      if (!in_valid || in_ready) begin
        in_valid = ($urandom_range(0, 3) != 0);
        if (in_valid) in_data = in_data + 8'd1;
      end
      out_ready = nostall || ($urandom_range(0, 1) == 1);
    end
    @(negedge clk) begin in_valid = 0; out_ready = 1; end
    repeat (10) @(negedge clk);
    $display("sent %0d, received %0d, scoreboard errors %0d, stall cycles %0d, full cycles %0d",
             sent, got, errors, stalls, fulls);
    if (stalls == 0) $fatal(1, "FAIL: no stall cycle, so a_out_hold was never exercised");
    if (errors == 0 && got == sent && fulls > 0)
      $display("PASS: all words in order, every assertion held, stall and full both covered");
    else $fatal(1, "FAIL: %0d scoreboard errors, %0d of %0d words received", errors, got, sent);
    $finish;
  end
endmodule

Related topics

• Immediate vs concurrent assertions

• Common RTL property templates

• CDC assertion patterns