Four families of data rules

Timing tutorials stop at handshakes. The checks that catch corruption bugs are data rules: the value out equals the value in, delayed, selected, or held.

Delay needs a constant depth

For an in-order FIFO, the element popped now was pushed occupancy pushes ago. One assertion per occupancy covers it, generated over the legal range.

The listing below is not run in this course's checks because Verilator 5.048 does not support $past with a gate argument.

1
2
3
4
5
6
7
8
9
10

// not-run: Verilator 5.048 does not support $past with a gate argument
genvar k;
generate
  for (k = 1; k <= DEPTH; k++) begin : g_fifo_chk
    assert property (@(posedge clk) disable iff (!rst_n)
      (pop && occupancy == k) |->
        (rd_data == $past(wr_data, k, push)))
      else $error("FIFO integrity: occ=%0d", k);
  end
endgenerate

A runtime occupancy as the depth argument is illegal: the LRM requires the $past depth to be an elaboration-time constant. That boundary is the standard interview point.

Constant distance belongs to $past. Variable distance and per-transaction matching belong to sequence local variables, which capture the write data at push time and compare at the matching pop.

Hold, read back, match phases

Stability rules want level antecedents: the obligation renews every cycle of the window.

1
2
3
4
5

// snippet
assert property (@(posedge clk) disable iff (!rst_n)
  busy |-> $stable({cfg_mode, cfg_len, cfg_base}));
assert property (@(posedge clk) disable iff (!rst_n)
  (out_valid && !out_ready) |-> ##1 ($stable(out_data) && out_valid));

Write-then-readback spans an unbounded gap, so $past cannot express it. Local variables capture the address and data at the write and compare at the matching read.

The readback listing below is not run in this course's checks because Verilator 5.048 rejects the unbounded [*0:$] repetition and the ! after ##1.

1
2
3
4
5
6
7
8
9
10
11

// not-run: Verilator 5.048 rejects [*0:$] here and "!" after "##1"
property p_readback;
  logic [7:0]  a;
  logic [31:0] d;
  @(posedge clk) disable iff (!rst_n)
    (wr_en, a = wr_addr, d = wr_data) ##1
    (!(wr_en && wr_addr == a)) [*0:$] ##0
    (rd_en && rd_addr == a)
    |-> ##1 (rd_data == d);
endproperty
assert property (p_readback);

Action blocks run after the edge updates, so printing a raw signal there shows the post-edge value. $sampled in the action block reports the value the assertion actually tested.

1
2
3
4

// snippet
assert property (@(posedge clk) disable iff (!rst_n)
  req |-> gnt)
else $error("req without gnt: sampled gnt=%b", $sampled(gnt));

A one-deep address pipeline is the ideal gated-$past case: every data-phase attribute must equal the address-phase value from one transfer beat ago, skipping wait states.

The phase pack below is not run in this course's checks because Verilator 5.048 does not support $past with a gate argument.

1
2
3
4
5
6

// not-run: Verilator 5.048 does not support $past with a gate argument
logic trans_beat;
assign trans_beat = (htrans inside {2'b10, 2'b11}) && hready;
assert property (@(posedge clk) disable iff (!rst_n)
  (data_phase_active && hready) |->
    (cur_resp_addr == $past(haddr, 1, trans_beat)));

The resp_addr lane always repeats the address from the previous transfer beat. The idle value on slot 2 never enters the history.

• Slot 0: transfer beat, haddr 1; resp_addr still 0, history unfilled.

• Slot 1: transfer beat, haddr 2; resp_addr 1, the previous beat.

• Slot 2: wait slot, no transfer beat; haddr carries idle value 5, resp_addr holds 2.

• Slot 3: still no transfer beat, haddr 3; resp_addr still 2, while ungated history would show 5.

• Slot 4: transfer beat, haddr 4; resp_addr still 2, the previous beat.

• Slot 5: idle, haddr holds 4; resp_addr 4.

1
2
3
4
5
6
7

// snippet: hdr, left and xr are small state registers updated on every accepted byte
a_len_legal: assert property (@(posedge clk) disable iff (!rst_n)
  (push && hdr) |-> (in_data[3:0] inside {[1:8]} && !in_data[8])) else fail("header: len outside 1 to 8, or last set");
a_last_on_check: assert property (@(posedge clk) disable iff (!rst_n)
  (push && !hdr) |-> (in_data[8] == (left == 5'd1))) else fail("last is not on the check byte");
a_check_xor: assert property (@(posedge clk) disable iff (!rst_n)
  (push && !hdr && left == 5'd1) |-> ((xr ^ in_data[7:0]) == 8'h00)) else fail("check byte is not the XOR of the packet");

Output from the complete listing in Checking PacketFIFO:

[565] pf_checker: header: len outside 1 to 8, or last set
len 0 header: 1 new report(s)
[695] pf_checker: check byte is not the XOR of the packet
wrong check byte: 1 new report(s)
[795] pf_checker: last is not on the check byte
last on a payload byte: 1 new report(s)

Testbench

The bench checks a 4-deep in-order FIFO and two hold rules for real. The FIFO's distance back is its occupancy, which $past cannot take, so a queue in modeling code holds the expected order and a one-step property compares the popped byte. Each rule gets one planted bug.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

// A 4-deep in-order FIFO with an optional planted bug: one popped byte is corrupted.
module fifo4 (
  input  logic clk, rst_n, push, pop, bug,
  input  logic [7:0] wr_data,
  output logic [7:0] rd_data,
  output logic [2:0] count
);
  logic [7:0] mem [4];
  logic [1:0] wp = 0, rp = 0;
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) begin wp <= 0; rp <= 0; count <= 0; end
    else begin
      if (push) begin mem[wp] <= wr_data; wp <= wp + 1; end
      if (pop)  rp <= rp + 1;
      count <= count + push - pop;
    end
  assign rd_data = mem[rp] ^ (bug ? 8'h01 : 8'h00);
endmodule

FIFO, 4 pushes and 4 pops: 0 failures
FIFO with a corrupted pop: 1 failure
cfg moved while busy: 1 failure; data moved while stalled: 1 failure
PASS: the FIFO order check, the busy stability check and the stall hold check each caught their planted bug

Related topics

• Past and gated history

• One-snapshot classifiers