Capstone: the asynchronous FIFO with an assertion suite

Build the asynchronous FIFO to a brief a verifier can bind to, attach the FIFO rules of the Assertions track, and see which broken designs they catch and which one they cannot.

Lesson: R6.6
Time: 40 min
Runs on: Verilator
Check: 5 questions

An asynchronous FIFO lost its first words after every reset. Its full flag read 0 while the write side was still held in reset, so the producer wrote into flops that ignored it. The verification team's FIFO rules would have caught it on the first run, but nobody had attached them: the new FIFO's ports had different names.

Words taken but never storedFIFO 2 of the lab, whose flags do not wait for reset, just after power-on. Values 1 ns after read-clock edges 2 to 10. taken counts the writes the rules saw accepted; stored is the FIFO's own count.

Cycle 1
Edge 3: the reset pin is high, full is 0, and the producer's first word is taken. The write side is still in reset, so nothing is stored.
Cycle 3
Edge 5: the write side is out of reset and stores its first word. Two words are already gone.
Cycle 7
Edge 9: the first answer is 2. The rules' model expected 0, the first word written.
Cycle 8
Edge 10: in_order fails on the answer it sampled. Every later answer is two words ahead.

A probe of the lab bench. After the second reset the same FIFO lost one more word.

A brief a verifier can bind to

The design is R6.4's FIFO with R6.5's reset handling. Its brief fixes the port names of the Assertions track's FIFO. So the rule module attaches with bind and .*, which connects every port of the rules to the FIFO signal of the same name.

Design brief

Port	Direction	Width	Meaning
wclk, wrst_n	input	1	write side clock and reset; wrst_n may be released at any time
write_en	input	1	write side: write a word
write_data	input	[WIDTH-1:0]	write side: the word
full	output	1	1: do not write (also during reset)
rclk, rrst_n	input	1	read side clock and reset
read_en	input	1	a read is taken at an edge where `read_en` is 1 and `empty` was 0
read_valid	output	1	1 for one cycle after a read is taken
read_data	output	[WIDTH-1:0]	read side: the word
empty	output	1	1: nothing to read (also during reset)
read_level	output	[$clog2(DEPTH):0]	`read_level` shows what the read side believes it holds

Clock: Crossing: registered Gray pointers, two flops each way; depth 8, a power of two
Reset: each pin released through two flops of its own clock; each side raises an "up" flag after release and hears the other's through two flops. During reset: full and empty stay 1 until both sides are up, so nothing is taken
Latency: reads taken at an edge where read_en is 1 and empty was 0; read_valid and the word one cycle later
Corner cases: Verification: read_level shows what the read side believes it holds; one reset per domain for disable iff

The rules ride along by nameArrows show signals. bind afifo afifo_rules ... rules (.*); puts one rule module inside every afifo, without touching its source.

A write is taken
At a wclk edge with write_en 1 and full 0, the model pushes the word, whatever the FIFO does inside.
Follow the calls, values and waits
1. data word 0: Producer → afifo write side
2. data word 0: afifo write side → Model queue
A read is answered
At an rclk edge the rules compare the answer with the model's oldest word, and read_level with the words the model holds.
Follow the calls, values and waits
1. data expect 0: Model queue → afifo_rules

Read the diagram as text

Producer: bench, wclk
afifo write side: full, wptr
afifo read side: empty, read_level
Consumer: bench, rclk
Model queue: words taken, oldest first
afifo_rules: six rules, two clocks

Producer → afifo write side: write_en, write_data
afifo write side → afifo read side: Gray pointers
afifo read side → Consumer: read_valid, read_data
afifo write side → Model queue: write taken
afifo read side → afifo_rules: ports by name
Model queue → afifo_rules: expected word

The model reads only ports. A model built from the FIFO's own pointers would copy their bugs.

The FIFO rules, for two clocks

A8.1's rules were written for a FIFO with one clock and one count. Bound to this FIFO unchanged, they do not compile: Verilator reports Can't find definition of variable: 'clk'. Two of them also stop being true: not_both, because here the flags are late on purpose, and flags_match, because during reset full and empty are both 1. A8.1's reset_clears is dropped, since each domain clears on its own pin.

Rule	Clock	Property	Spec sentence
`no_overflow`	wclk	`take_w \|-> n < DEPTH`	no write is taken into a full FIFO
`no_underflow`	rclk	`take_r \|-> n > 0`	no read is taken from an empty FIFO
`answered`	rclk	`take_r \|=> read_valid`	every read taken is answered next cycle
`no_extra`	rclk	`!take_r \|=> !read_valid`	no answer without a read
`in_order`	rclk	`take_r \|=> read_data == exp_data`	the answer is the oldest word
`level_safe`	rclk	`read_level <= n`	the read side never sees more words than there are

n is the model's count: writes taken minus reads taken, both decided from the ports. Each rule is disabled while its own domain's reset pin is low.

level_safe replaces A8.1's exact flag rule. A late flag is correct here, so the rule asks only that the read side never be early: the safety property of R6.4.

What the rules catch, and what they cannot

FIFO in the lab	Switch	Rules that fail (count)	First failure
0: the brief	none	none	none
1: binary pointers	`BINARY`	`level_safe` (8)	rclk edge 12
2: flags that do not wait for reset	`NO_READY`	`in_order` (136), `no_overflow` (1, a false alarm: the model still counts a word lost after the second reset)	rclk edge 10
3: Gray coder in front of the synchronizer	`COMB_CROSS`	none	none

Measured on the lab bench: 304 read-clock edges with a second reset over edges 102 and 103, and the crossing model of R6.4 in every FIFO.

FIFO 3 sends to_wire(wbin_q), the output of the XOR gates, straight into the first synchronizer flop. In a zero-delay simulation that output changes once per step, one bit at a time. In gates, the XORs can glitch while the binary count settles, and a glitch caught by the first flop is a pointer value nobody sent.

The lab: four FIFOs, one suite

The bench builds four FIFOs from your design: the brief, and one with each switch set to 1. Each gets its own producer, consumer and R6.4's crossing model, bench code that stands in for what a zero-delay simulation never shows. The bound rules print one summary line per FIFO. Run it: the brief's line is all zeros.

Then break the brief on purpose. Change assign full = full_q || !w_ready; to assign full = full_q; and run again: now FIFO 0 fails in_order 136 times, first at rclk edge 9. Put the line back before you move on.

Asked in interviews

How do you attach assertions to a design you cannot edit?
Write them in their own module and use bind: it instantiates the module inside every instance of the design, or one instance, and connects it by name. The bound module also sees internal signals, though rules built from ports are more robust.
What does a verifier need from a designer?
Stable, documented port names, and one reset per domain to switch rules off with disable iff. Outputs that show what the design believes, such as a level. Flags that tell the truth during reset.
Which properties would you assert on an asynchronous FIFO?
No write taken when full, no read taken when empty, every read answered once, data in order against a model, and a level that is never above the true count. Pair them with a structural CDC check for the synchronizers.

Try it

FIFO 2 lost two words after power-on and one after the second reset, so in_order failed on every answer until the reset cleared the model, and again after it. FIFO 1 tore its level eight times, and the data never went wrong, as in R6.4.

Synthesize reads the design alone, with all switches at 0: 258 cells, 119 flops, 0 latches, 11 levels of logic. Set one switch at a time as a default and the counts fall to 236 cells for BINARY, 248 for NO_READY and 247 for COMB_CROSS, each with 113 flops.

RTLVerilator · simulator service · Lint: Verilator service · Synthesize: Yosys service

Edit the design, then Run, Lint or Synthesize

Expected: brief: no_overflow=0 no_underflow=0 answered=0 no_extra=0 in_order=0 level_safe=0, first: none binary: no_overflow=0 no_underflow=0 answered=0 no_extra=0 in_order=0 level_safe=8, first: level_safe at rclk edge 12 no ready: no_overflow=1 no_underflow=0 answered=0 no_extra=0 in_order=136 level_safe=0, first: in_order at rclk edge 10 comb: no_overflow=0 no_underflow=0 answered=0 no_extra=0 in_order=0 level_safe=0, first: none

Original design · 258 cells · 119 flip-flops · 0 latches · 11 logic levels. Synthesis uses Yosys; counts depend on the toolchain.

Original example source

// afifo: the asynchronous FIFO of R6.4 with the reset handling of R6.5. DEPTH words of WIDTH bits,
// written on wclk and read on rclk. The three switches build broken versions for the bench; with
// all three at 0 it is the design the brief asks for.
module afifo #(
  parameter int DEPTH = 8, WIDTH = 8,
  parameter bit BINARY     = 0,   // switch: binary pointers on the crossing wires
  parameter bit NO_READY   = 0,   // switch: flags that do not wait for both sides to be out of reset
  parameter bit COMB_CROSS = 0    // switch: the Gray coder sits in front of the synchronizer
) (
  input  logic             wclk, wrst_n,     // write domain; wrst_n may be released at any time
  input  logic             write_en,
  input  logic [WIDTH-1:0] write_data,
  output logic             full,             // 1: do not write (also during reset)
  input  logic             rclk, rrst_n,     // read domain
  input  logic             read_en,
  output logic             read_valid,       // 1 for one cycle after a read is taken
  output logic [WIDTH-1:0] read_data,
  output logic             empty,            // 1: nothing to read (also during reset)
  output logic [$clog2(DEPTH):0] read_level  // words the read side can see
);
  localparam int AW = $clog2(DEPTH);

  function automatic logic [AW:0] to_wire(input logic [AW:0] b);
    return BINARY ? b : b ^ (b >> 1);
  endfunction
  function automatic logic [AW:0] from_wire(input logic [AW:0] w);
    logic [AW:0] b;
    for (int i = 0; i <= AW; i++) b[i] = BINARY ? w[i] : ^(w >> i);
    return b;
  endfunction

  // Each side releases its own reset pin through two flops of its own clock (R6.5).
  logic wr_q1, wrst_s, rr_q1, rrst_s;
  always_ff @(posedge wclk or negedge wrst_n)
    if (!wrst_n) begin wr_q1 <= 1'b0; wrst_s <= 1'b0; end
    else         begin wr_q1 <= 1'b1; wrst_s <= wr_q1; end
  always_ff @(posedge rclk or negedge rrst_n)
    if (!rrst_n) begin rr_q1 <= 1'b0; rrst_s <= 1'b0; end
    else         begin rr_q1 <= 1'b1; rrst_s <= rr_q1; end

  // Each side raises an "up" flag after its release and hears the other's through two flops.
  logic w_up, r_up, w_rup1, w_rup2, r_wup1, r_wup2;
  always_ff @(posedge wclk or negedge wrst_s)
    if (!wrst_s) begin w_up <= 1'b0; w_rup1 <= 1'b0; w_rup2 <= 1'b0; end
    else         begin w_up <= 1'b1; w_rup1 <= r_up; w_rup2 <= w_rup1; end
  always_ff @(posedge rclk or negedge rrst_s)
    if (!rrst_s) begin r_up <= 1'b0; r_wup1 <= 1'b0; r_wup2 <= 1'b0; end
    else         begin r_up <= 1'b1; r_wup1 <= w_up; r_wup2 <= r_wup1; end
  wire w_ready = NO_READY || (w_up && w_rup2);
  wire r_ready = NO_READY || (r_up && r_wup2);

  logic [WIDTH-1:0] mem [DEPTH];
  logic [AW:0] wbin_q, wptr_q, rbin_q, rptr_q;   // word counts, and the registered copies
  logic [AW:0] wq1_rptr, wq2_rptr;           // the read pointer after one and two write-clock flops
  logic [AW:0] rq1_wptr, rq2_wptr;           // the write pointer after one and two read-clock flops
  logic        full_q, empty_q;

  // What actually crosses: the registered copy, or (COMB_CROSS) the coder's output.
  logic [AW:0] wptr_x, rptr_x;
  assign wptr_x = COMB_CROSS ? to_wire(wbin_q) : wptr_q;
  assign rptr_x = COMB_CROSS ? to_wire(rbin_q) : rptr_q;

  // Write domain.
  assign full = full_q || !w_ready;
  logic        take_w;
  logic [AW:0] wbin_d, rbin_seen;
  assign take_w    = write_en && !full;
  assign wbin_d    = wbin_q + (AW+1)'(take_w);
  assign rbin_seen = from_wire(wq2_rptr);
  always_ff @(posedge wclk or negedge wrst_s)
    if (!wrst_s) begin
      wbin_q <= '0; wptr_q <= '0; wq1_rptr <= '0; wq2_rptr <= '0; full_q <= 1'b0;
    end else begin
      wbin_q   <= wbin_d;
      wptr_q   <= to_wire(wbin_d);
      wq1_rptr <= rptr_x;
      wq2_rptr <= wq1_rptr;
      full_q   <= (wbin_d[AW] != rbin_seen[AW]) && (wbin_d[AW-1:0] == rbin_seen[AW-1:0]);
    end
  always_ff @(posedge wclk)
    if (take_w) mem[wbin_q[AW-1:0]] <= write_data;

  // Read domain.
  assign empty = empty_q || !r_ready;
  logic        take_r;
  logic [AW:0] rbin_d, wbin_seen;
  assign take_r    = read_en && !empty;
  assign rbin_d    = rbin_q + (AW+1)'(take_r);
  assign wbin_seen = from_wire(rq2_wptr);
  always_ff @(posedge rclk or negedge rrst_s)
    if (!rrst_s) begin
      rbin_q <= '0; rptr_q <= '0; rq1_wptr <= '0; rq2_wptr <= '0; empty_q <= 1'b1; read_level <= '0;
      read_valid <= 1'b0; read_data <= '0;
    end else begin
      rbin_q     <= rbin_d;
      rptr_q     <= to_wire(rbin_d);
      rq1_wptr   <= wptr_x;
      rq2_wptr   <= rq1_wptr;
      empty_q    <= (rbin_d == wbin_seen);
      read_level <= wbin_seen - rbin_d;
      read_valid <= take_r;
      if (take_r) read_data <= mem[rbin_q[AW-1:0]];
    end
endmodule

Read included file: afifo_rules.sv

// afifo_rules.sv: the FIFO rules of the Assertions track (A8.1), restated for two clocks (read-only).
// The model is built from the FIFO's ports only: a write is taken at a wclk edge where write_en is 1
// and full is 0, a read at an rclk edge where read_en is 1 and empty is 0. Each rule counts its
// failures, and the first failure of any rule is remembered with its time.
module afifo_rules #(parameter int DEPTH = 8, WIDTH = 8) (
  input logic wclk, wrst_n, write_en, full,
  input logic [WIDTH-1:0] write_data,
  input logic rclk, rrst_n, read_en, read_valid, empty,
  input logic [WIDTH-1:0] read_data,
  input logic [$clog2(DEPTH):0] read_level
);
  logic [WIDTH-1:0] q [$];             // words written and not yet read, oldest first
  int               nw = 0, nr = 0;    // writes and reads taken since reset
  int               n;                 // words the FIFO should hold
  logic [WIDTH-1:0] exp_data = '0;     // the word the last read should return
  logic take_w, take_r;
  assign take_w = write_en && !full;
  assign take_r = read_en && !empty;
  assign n = nw - nr;
  always @(posedge wclk)
    if (!wrst_n) begin q.delete(); nw = 0; nr = 0; end
    else if (take_w) begin q.push_back(write_data); nw++; end
  always @(posedge rclk)
    if (!rrst_n) begin q.delete(); nw = 0; nr = 0; end
    else if (take_r) begin
      if (q.size() > 0) exp_data <= q.pop_front();
      nr++;
    end

  int f_over = 0, f_under = 0, f_answer = 0, f_extra = 0, f_order = 0, f_level = 0;
  int    redge = -1;                   // the number of the last rising edge of rclk
  always @(posedge rclk) redge++;
  string first = "none";
  int    first_e = -1;
  function automatic void note(string rule);
    if (first == "none") begin first = rule; first_e = redge; end
  endfunction

  no_overflow:  assert property (@(posedge wclk) disable iff (!wrst_n) take_w |-> n < DEPTH)
                else begin f_over++; note("no_overflow"); end
  no_underflow: assert property (@(posedge rclk) disable iff (!rrst_n) take_r |-> n > 0)
                else begin f_under++; note("no_underflow"); end
  answered:     assert property (@(posedge rclk) disable iff (!rrst_n) take_r |=> read_valid)
                else begin f_answer++; note("answered"); end
  no_extra:     assert property (@(posedge rclk) disable iff (!rrst_n) !take_r |=> !read_valid)
                else begin f_extra++; note("no_extra"); end
  in_order:     assert property (@(posedge rclk) disable iff (!rrst_n) take_r |=> read_data == exp_data)
                else begin f_order++; note("in_order"); end
  level_safe:   assert property (@(posedge rclk) disable iff (!rrst_n) int'(read_level) <= n)
                else begin f_level++; note("level_safe"); end

  function automatic string summary();
    return $sformatf("no_overflow=%0d no_underflow=%0d answered=%0d no_extra=%0d in_order=%0d level_safe=%0d, first: %s",
                     f_over, f_under, f_answer, f_extra, f_order, f_level,
                     first == "none" ? "none" : $sformatf("%s at rclk edge %0d", first, first_e));
  endfunction
endmodule

bind afifo afifo_rules #(.DEPTH(DEPTH), .WIDTH(WIDTH)) rules (.*);

Read included file: tb.sv

`timescale 1ns/1ps
module tb;
  logic clk = 0;
  always #5 clk = ~clk;                   // the sampling clock: rising edges at 5, 15, 25, ... ns
  logic wclk = 0;                      // the second clock: rising edges at 2.6, 15.6, ... ns
  initial begin
    #2.6;
    forever begin wclk = 1; #6.5; wclk = 0; #6.5; end
  end
  logic rst_n = 1;                        // falls at 1 ns: a real edge, so asynchronous resets act before any clock
  int edge_n = -1;                        // the number of the last rising edge of clk
  always @(posedge clk) edge_n = edge_n + 1;
  // FIFO 0: the brief, all switches 0.
  for (genvar g = 0; g <= 0; g++) begin : f0
    logic       write_en = 0, read_en = 0, full, empty, read_valid;
    logic [7:0] write_data = 0, read_data;
    logic [3:0] read_level;
    int         wcyc = 0;
    afifo #() dut (
      .wclk(wclk), .wrst_n(rst_n), .write_en(write_en), .write_data(write_data), .full(full),
      .rclk(clk), .rrst_n(rst_n), .read_en(read_en), .read_valid(read_valid), .read_data(read_data),
      .empty(empty), .read_level(read_level));
    // Producer: the next number at 20 of every 32 write-clock edges, as soon as rst_n is 1.
    always @(posedge wclk) begin
      if (write_en && !full) write_data <= write_data + 8'd1;
      wcyc++;
      #1 write_en = rst_n && (wcyc % 32) < 20;
    end
    // Consumer: a read at every edge, except 12 of every 40.
    always @(posedge clk) #0.5 read_en = rst_n && (edge_n % 40) < 28;
    // The crossing model of R6.4 (bench only): a pointer bit that changed less than 1.5 ns before
    // the edge keeps its old or its new value in the first flop, at random from a fixed seed.
    logic [3:0] w_old = 0, w_now = 0, r_old = 0, r_now = 0;
    realtime    w_t = -100, r_t = -100;
    int unsigned seed = 1;
    always @(dut.wptr_x) begin w_old = w_now; w_now = dut.wptr_x; w_t = $realtime; end
    always @(dut.rptr_x) begin r_old = r_now; r_now = dut.rptr_x; r_t = $realtime; end
    always @(posedge clk) if ($realtime - w_t < 1.5) #0.1 for (int i = 0; i < 4; i++) begin
      seed = seed * 1103515245 + 12345;
      if (seed[16]) dut.rq1_wptr[i] = w_old[i];
    end
    always @(posedge wclk) if ($realtime - r_t < 1.5) #0.1 for (int i = 0; i < 4; i++) begin
      seed = seed * 1103515245 + 12345;
      if (seed[16]) dut.wq1_rptr[i] = r_old[i];
    end
  end
  // FIFO 1: binary pointers.
  for (genvar g = 1; g <= 1; g++) begin : f1
    logic       write_en = 0, read_en = 0, full, empty, read_valid;
    logic [7:0] write_data = 0, read_data;
    logic [3:0] read_level;
    int         wcyc = 0;
    afifo #(.BINARY(1)) dut (
      .wclk(wclk), .wrst_n(rst_n), .write_en(write_en), .write_data(write_data), .full(full),
      .rclk(clk), .rrst_n(rst_n), .read_en(read_en), .read_valid(read_valid), .read_data(read_data),
      .empty(empty), .read_level(read_level));
    // Producer: the next number at 20 of every 32 write-clock edges, as soon as rst_n is 1.
    always @(posedge wclk) begin
      if (write_en && !full) write_data <= write_data + 8'd1;
      wcyc++;
      #1 write_en = rst_n && (wcyc % 32) < 20;
    end
    // Consumer: a read at every edge, except 12 of every 40.
    always @(posedge clk) #0.5 read_en = rst_n && (edge_n % 40) < 28;
    // The crossing model of R6.4 (bench only): a pointer bit that changed less than 1.5 ns before
    // the edge keeps its old or its new value in the first flop, at random from a fixed seed.
    logic [3:0] w_old = 0, w_now = 0, r_old = 0, r_now = 0;
    realtime    w_t = -100, r_t = -100;
    int unsigned seed = 2;
    always @(dut.wptr_x) begin w_old = w_now; w_now = dut.wptr_x; w_t = $realtime; end
    always @(dut.rptr_x) begin r_old = r_now; r_now = dut.rptr_x; r_t = $realtime; end
    always @(posedge clk) if ($realtime - w_t < 1.5) #0.1 for (int i = 0; i < 4; i++) begin
      seed = seed * 1103515245 + 12345;
      if (seed[16]) dut.rq1_wptr[i] = w_old[i];
    end
    always @(posedge wclk) if ($realtime - r_t < 1.5) #0.1 for (int i = 0; i < 4; i++) begin
      seed = seed * 1103515245 + 12345;
      if (seed[16]) dut.wq1_rptr[i] = r_old[i];
    end
  end
  // FIFO 2: flags that do not wait for reset.
  for (genvar g = 2; g <= 2; g++) begin : f2
    logic       write_en = 0, read_en = 0, full, empty, read_valid;
    logic [7:0] write_data = 0, read_data;
    logic [3:0] read_level;
    int         wcyc = 0;
    afifo #(.NO_READY(1)) dut (
      .wclk(wclk), .wrst_n(rst_n), .write_en(write_en), .write_data(write_data), .full(full),
      .rclk(clk), .rrst_n(rst_n), .read_en(read_en), .read_valid(read_valid), .read_data(read_data),
      .empty(empty), .read_level(read_level));
    // Producer: the next number at 20 of every 32 write-clock edges, as soon as rst_n is 1.
    always @(posedge wclk) begin
      if (write_en && !full) write_data <= write_data + 8'd1;
      wcyc++;
      #1 write_en = rst_n && (wcyc % 32) < 20;
    end
    // Consumer: a read at every edge, except 12 of every 40.
    always @(posedge clk) #0.5 read_en = rst_n && (edge_n % 40) < 28;
    // The crossing model of R6.4 (bench only): a pointer bit that changed less than 1.5 ns before
    // the edge keeps its old or its new value in the first flop, at random from a fixed seed.
    logic [3:0] w_old = 0, w_now = 0, r_old = 0, r_now = 0;
    realtime    w_t = -100, r_t = -100;
    int unsigned seed = 3;
    always @(dut.wptr_x) begin w_old = w_now; w_now = dut.wptr_x; w_t = $realtime; end
    always @(dut.rptr_x) begin r_old = r_now; r_now = dut.rptr_x; r_t = $realtime; end
    always @(posedge clk) if ($realtime - w_t < 1.5) #0.1 for (int i = 0; i < 4; i++) begin
      seed = seed * 1103515245 + 12345;
      if (seed[16]) dut.rq1_wptr[i] = w_old[i];
    end
    always @(posedge wclk) if ($realtime - r_t < 1.5) #0.1 for (int i = 0; i < 4; i++) begin
      seed = seed * 1103515245 + 12345;
      if (seed[16]) dut.wq1_rptr[i] = r_old[i];
    end
  end
  // FIFO 3: a Gray coder in front of the synchronizer.
  for (genvar g = 3; g <= 3; g++) begin : f3
    logic       write_en = 0, read_en = 0, full, empty, read_valid;
    logic [7:0] write_data = 0, read_data;
    logic [3:0] read_level;
    int         wcyc = 0;
    afifo #(.COMB_CROSS(1)) dut (
      .wclk(wclk), .wrst_n(rst_n), .write_en(write_en), .write_data(write_data), .full(full),
      .rclk(clk), .rrst_n(rst_n), .read_en(read_en), .read_valid(read_valid), .read_data(read_data),
      .empty(empty), .read_level(read_level));
    // Producer: the next number at 20 of every 32 write-clock edges, as soon as rst_n is 1.
    always @(posedge wclk) begin
      if (write_en && !full) write_data <= write_data + 8'd1;
      wcyc++;
      #1 write_en = rst_n && (wcyc % 32) < 20;
    end
    // Consumer: a read at every edge, except 12 of every 40.
    always @(posedge clk) #0.5 read_en = rst_n && (edge_n % 40) < 28;
    // The crossing model of R6.4 (bench only): a pointer bit that changed less than 1.5 ns before
    // the edge keeps its old or its new value in the first flop, at random from a fixed seed.
    logic [3:0] w_old = 0, w_now = 0, r_old = 0, r_now = 0;
    realtime    w_t = -100, r_t = -100;
    int unsigned seed = 4;
    always @(dut.wptr_x) begin w_old = w_now; w_now = dut.wptr_x; w_t = $realtime; end
    always @(dut.rptr_x) begin r_old = r_now; r_now = dut.rptr_x; r_t = $realtime; end
    always @(posedge clk) if ($realtime - w_t < 1.5) #0.1 for (int i = 0; i < 4; i++) begin
      seed = seed * 1103515245 + 12345;
      if (seed[16]) dut.rq1_wptr[i] = w_old[i];
    end
    always @(posedge wclk) if ($realtime - r_t < 1.5) #0.1 for (int i = 0; i < 4; i++) begin
      seed = seed * 1103515245 + 12345;
      if (seed[16]) dut.wq1_rptr[i] = r_old[i];
    end
  end

  // Advance to the next rising edge of clk, wait for the design to settle, then print.
  task automatic tick();
    @(posedge clk); #1;
    
  endtask
  initial begin
    #1 rst_n = 0; tick(); tick(); rst_n = 1;   // asserted at 1 ns, clk edges 0 and 1 in reset, released 1 ns after edge 1
    repeat (100) tick();
    rst_n = 0; tick(); tick(); rst_n = 1;     // a second reset: low at edges 102 and 103, released 1 ns after 103
    repeat (200) tick();
    $display("brief:    %s", f0[0].dut.rules.summary());
    $display("binary:   %s", f1[1].dut.rules.summary());
    $display("no ready: %s", f2[2].dut.rules.summary());
    $display("comb:     %s", f3[3].dut.rules.summary());
    $finish(0);                             // quiet: no "$finish called" line
  end
endmodule

Check yourself

Predict the outputOne FIFO with NO_READY = 1 runs for 30 read-clock edges after power-on, with the rules bound. The program prints the name of the first rule that failed. What does it print?

`timescale 1ns/1ps
module tb;
  logic clk = 0;
  always #5 clk = ~clk;                   // the sampling clock: rising edges at 5, 15, 25, ... ns
  logic wclk = 0;                      // the second clock: rising edges at 2.6, 15.6, ... ns
  initial begin
    #2.6;
    forever begin wclk = 1; #6.5; wclk = 0; #6.5; end
  end
  logic rst_n = 1;                        // falls at 1 ns: a real edge, so asynchronous resets act before any clock
  int edge_n = -1;                        // the number of the last rising edge of clk
  always @(posedge clk) edge_n = edge_n + 1;
  // FIFO 0: one FIFO.
  for (genvar g = 0; g <= 0; g++) begin : f0
    logic       write_en = 0, read_en = 0, full, empty, read_valid;
    logic [7:0] write_data = 0, read_data;
    logic [3:0] read_level;
    int         wcyc = 0;
    afifo #(.NO_READY(1)) dut (
      .wclk(wclk), .wrst_n(rst_n), .write_en(write_en), .write_data(write_data), .full(full),
      .rclk(clk), .rrst_n(rst_n), .read_en(read_en), .read_valid(read_valid), .read_data(read_data),
      .empty(empty), .read_level(read_level));
    // Producer: the next number at 20 of every 32 write-clock edges, as soon as rst_n is 1.
    always @(posedge wclk) begin
      if (write_en && !full) write_data <= write_data + 8'd1;
      wcyc++;
      #1 write_en = rst_n && (wcyc % 32) < 20;
    end
    // Consumer: a read at every edge, except 12 of every 40.
    always @(posedge clk) #0.5 read_en = rst_n && (edge_n % 40) < 28;
    // The crossing model of R6.4 (bench only): a pointer bit that changed less than 1.5 ns before
    // the edge keeps its old or its new value in the first flop, at random from a fixed seed.
    logic [3:0] w_old = 0, w_now = 0, r_old = 0, r_now = 0;
    realtime    w_t = -100, r_t = -100;
    int unsigned seed = 1;
    always @(dut.wptr_x) begin w_old = w_now; w_now = dut.wptr_x; w_t = $realtime; end
    always @(dut.rptr_x) begin r_old = r_now; r_now = dut.rptr_x; r_t = $realtime; end
    always @(posedge clk) if ($realtime - w_t < 1.5) #0.1 for (int i = 0; i < 4; i++) begin
      seed = seed * 1103515245 + 12345;
      if (seed[16]) dut.rq1_wptr[i] = w_old[i];
    end
    always @(posedge wclk) if ($realtime - r_t < 1.5) #0.1 for (int i = 0; i < 4; i++) begin
      seed = seed * 1103515245 + 12345;
      if (seed[16]) dut.wq1_rptr[i] = r_old[i];
    end
  end

  // Advance to the next rising edge of clk, wait for the design to settle, then print.
  task automatic tick();
    @(posedge clk); #1;
    
  endtask
  initial begin
    #1 rst_n = 0; tick(); tick(); rst_n = 1;   // asserted at 1 ns, clk edges 0 and 1 in reset, released 1 ns after edge 1
    repeat (30) tick();
    $display("%s", f0[0].dut.rules.first);
    $finish(0);                             // quiet: no "$finish called" line
  end
endmodule
// afifo: the asynchronous FIFO of R6.4 with the reset handling of R6.5. DEPTH words of WIDTH bits,
// written on wclk and read on rclk. The three switches build broken versions for the bench; with
// all three at 0 it is the design the brief asks for.
module afifo #(
  parameter int DEPTH = 8, WIDTH = 8,
  parameter bit BINARY     = 0,   // switch: binary pointers on the crossing wires
  parameter bit NO_READY   = 0,   // switch: flags that do not wait for both sides to be out of reset
  parameter bit COMB_CROSS = 0    // switch: the Gray coder sits in front of the synchronizer
) (
  input  logic             wclk, wrst_n,     // write domain; wrst_n may be released at any time
  input  logic             write_en,
  input  logic [WIDTH-1:0] write_data,
  output logic             full,             // 1: do not write (also during reset)
  input  logic             rclk, rrst_n,     // read domain
  input  logic             read_en,
  output logic             read_valid,       // 1 for one cycle after a read is taken
  output logic [WIDTH-1:0] read_data,
  output logic             empty,            // 1: nothing to read (also during reset)
  output logic [$clog2(DEPTH):0] read_level  // words the read side can see
);
  localparam int AW = $clog2(DEPTH);

  function automatic logic [AW:0] to_wire(input logic [AW:0] b);
    return BINARY ? b : b ^ (b >> 1);
  endfunction
  function automatic logic [AW:0] from_wire(input logic [AW:0] w);
    logic [AW:0] b;
    for (int i = 0; i <= AW; i++) b[i] = BINARY ? w[i] : ^(w >> i);
    return b;
  endfunction

  // Each side releases its own reset pin through two flops of its own clock (R6.5).
  logic wr_q1, wrst_s, rr_q1, rrst_s;
  always_ff @(posedge wclk or negedge wrst_n)
    if (!wrst_n) begin wr_q1 <= 1'b0; wrst_s <= 1'b0; end
    else         begin wr_q1 <= 1'b1; wrst_s <= wr_q1; end
  always_ff @(posedge rclk or negedge rrst_n)
    if (!rrst_n) begin rr_q1 <= 1'b0; rrst_s <= 1'b0; end
    else         begin rr_q1 <= 1'b1; rrst_s <= rr_q1; end

  // Each side raises an "up" flag after its release and hears the other's through two flops.
  logic w_up, r_up, w_rup1, w_rup2, r_wup1, r_wup2;
  always_ff @(posedge wclk or negedge wrst_s)
    if (!wrst_s) begin w_up <= 1'b0; w_rup1 <= 1'b0; w_rup2 <= 1'b0; end
    else         begin w_up <= 1'b1; w_rup1 <= r_up; w_rup2 <= w_rup1; end
  always_ff @(posedge rclk or negedge rrst_s)
    if (!rrst_s) begin r_up <= 1'b0; r_wup1 <= 1'b0; r_wup2 <= 1'b0; end
    else         begin r_up <= 1'b1; r_wup1 <= w_up; r_wup2 <= r_wup1; end
  wire w_ready = NO_READY || (w_up && w_rup2);
  wire r_ready = NO_READY || (r_up && r_wup2);

  logic [WIDTH-1:0] mem [DEPTH];
  logic [AW:0] wbin_q, wptr_q, rbin_q, rptr_q;   // word counts, and the registered copies
  logic [AW:0] wq1_rptr, wq2_rptr;           // the read pointer after one and two write-clock flops
  logic [AW:0] rq1_wptr, rq2_wptr;           // the write pointer after one and two read-clock flops
  logic        full_q, empty_q;

  // What actually crosses: the registered copy, or (COMB_CROSS) the coder's output.
  logic [AW:0] wptr_x, rptr_x;
  assign wptr_x = COMB_CROSS ? to_wire(wbin_q) : wptr_q;
  assign rptr_x = COMB_CROSS ? to_wire(rbin_q) : rptr_q;

  // Write domain.
  assign full = full_q || !w_ready;
  logic        take_w;
  logic [AW:0] wbin_d, rbin_seen;
  assign take_w    = write_en && !full;
  assign wbin_d    = wbin_q + (AW+1)'(take_w);
  assign rbin_seen = from_wire(wq2_rptr);
  always_ff @(posedge wclk or negedge wrst_s)
    if (!wrst_s) begin
      wbin_q <= '0; wptr_q <= '0; wq1_rptr <= '0; wq2_rptr <= '0; full_q <= 1'b0;
    end else begin
      wbin_q   <= wbin_d;
      wptr_q   <= to_wire(wbin_d);
      wq1_rptr <= rptr_x;
      wq2_rptr <= wq1_rptr;
      full_q   <= (wbin_d[AW] != rbin_seen[AW]) && (wbin_d[AW-1:0] == rbin_seen[AW-1:0]);
    end
  always_ff @(posedge wclk)
    if (take_w) mem[wbin_q[AW-1:0]] <= write_data;

  // Read domain.
  assign empty = empty_q || !r_ready;
  logic        take_r;
  logic [AW:0] rbin_d, wbin_seen;
  assign take_r    = read_en && !empty;
  assign rbin_d    = rbin_q + (AW+1)'(take_r);
  assign wbin_seen = from_wire(rq2_wptr);
  always_ff @(posedge rclk or negedge rrst_s)
    if (!rrst_s) begin
      rbin_q <= '0; rptr_q <= '0; rq1_wptr <= '0; rq2_wptr <= '0; empty_q <= 1'b1; read_level <= '0;
      read_valid <= 1'b0; read_data <= '0;
    end else begin
      rbin_q     <= rbin_d;
      rptr_q     <= to_wire(rbin_d);
      rq1_wptr   <= wptr_x;
      rq2_wptr   <= rq1_wptr;
      empty_q    <= (rbin_d == wbin_seen);
      read_level <= wbin_seen - rbin_d;
      read_valid <= take_r;
      if (take_r) read_data <= mem[rbin_q[AW-1:0]];
    end
endmodule

Read included file: afifo_rules.sv

// afifo_rules.sv: the FIFO rules of the Assertions track (A8.1), restated for two clocks (read-only).
// The model is built from the FIFO's ports only: a write is taken at a wclk edge where write_en is 1
// and full is 0, a read at an rclk edge where read_en is 1 and empty is 0. Each rule counts its
// failures, and the first failure of any rule is remembered with its time.
module afifo_rules #(parameter int DEPTH = 8, WIDTH = 8) (
  input logic wclk, wrst_n, write_en, full,
  input logic [WIDTH-1:0] write_data,
  input logic rclk, rrst_n, read_en, read_valid, empty,
  input logic [WIDTH-1:0] read_data,
  input logic [$clog2(DEPTH):0] read_level
);
  logic [WIDTH-1:0] q [$];             // words written and not yet read, oldest first
  int               nw = 0, nr = 0;    // writes and reads taken since reset
  int               n;                 // words the FIFO should hold
  logic [WIDTH-1:0] exp_data = '0;     // the word the last read should return
  logic take_w, take_r;
  assign take_w = write_en && !full;
  assign take_r = read_en && !empty;
  assign n = nw - nr;
  always @(posedge wclk)
    if (!wrst_n) begin q.delete(); nw = 0; nr = 0; end
    else if (take_w) begin q.push_back(write_data); nw++; end
  always @(posedge rclk)
    if (!rrst_n) begin q.delete(); nw = 0; nr = 0; end
    else if (take_r) begin
      if (q.size() > 0) exp_data <= q.pop_front();
      nr++;
    end

  int f_over = 0, f_under = 0, f_answer = 0, f_extra = 0, f_order = 0, f_level = 0;
  int    redge = -1;                   // the number of the last rising edge of rclk
  always @(posedge rclk) redge++;
  string first = "none";
  int    first_e = -1;
  function automatic void note(string rule);
    if (first == "none") begin first = rule; first_e = redge; end
  endfunction

  no_overflow:  assert property (@(posedge wclk) disable iff (!wrst_n) take_w |-> n < DEPTH)
                else begin f_over++; note("no_overflow"); end
  no_underflow: assert property (@(posedge rclk) disable iff (!rrst_n) take_r |-> n > 0)
                else begin f_under++; note("no_underflow"); end
  answered:     assert property (@(posedge rclk) disable iff (!rrst_n) take_r |=> read_valid)
                else begin f_answer++; note("answered"); end
  no_extra:     assert property (@(posedge rclk) disable iff (!rrst_n) !take_r |=> !read_valid)
                else begin f_extra++; note("no_extra"); end
  in_order:     assert property (@(posedge rclk) disable iff (!rrst_n) take_r |=> read_data == exp_data)
                else begin f_order++; note("in_order"); end
  level_safe:   assert property (@(posedge rclk) disable iff (!rrst_n) int'(read_level) <= n)
                else begin f_level++; note("level_safe"); end

  function automatic string summary();
    return $sformatf("no_overflow=%0d no_underflow=%0d answered=%0d no_extra=%0d in_order=%0d level_safe=%0d, first: %s",
                     f_over, f_under, f_answer, f_extra, f_order, f_level,
                     first == "none" ? "none" : $sformatf("%s at rclk edge %0d", first, first_e));
  endfunction
endmodule

bind afifo afifo_rules #(.DEPTH(DEPTH), .WIDTH(WIDTH)) rules (.*);

Spot the bugEach option sets the switches of one FIFO, which then runs 150 read-clock edges with the rules bound. The harness fails when the rules report nothing at all. Which broken FIFO gets past the rules?

.COMB_CROSS(1)

.BINARY(1), .COMB_CROSS(1)

.BINARY(1)

.NO_READY(1)

Read included file: afifo_rules.sv

// afifo_rules.sv: the FIFO rules of the Assertions track (A8.1), restated for two clocks (read-only).
// The model is built from the FIFO's ports only: a write is taken at a wclk edge where write_en is 1
// and full is 0, a read at an rclk edge where read_en is 1 and empty is 0. Each rule counts its
// failures, and the first failure of any rule is remembered with its time.
module afifo_rules #(parameter int DEPTH = 8, WIDTH = 8) (
  input logic wclk, wrst_n, write_en, full,
  input logic [WIDTH-1:0] write_data,
  input logic rclk, rrst_n, read_en, read_valid, empty,
  input logic [WIDTH-1:0] read_data,
  input logic [$clog2(DEPTH):0] read_level
);
  logic [WIDTH-1:0] q [$];             // words written and not yet read, oldest first
  int               nw = 0, nr = 0;    // writes and reads taken since reset
  int               n;                 // words the FIFO should hold
  logic [WIDTH-1:0] exp_data = '0;     // the word the last read should return
  logic take_w, take_r;
  assign take_w = write_en && !full;
  assign take_r = read_en && !empty;
  assign n = nw - nr;
  always @(posedge wclk)
    if (!wrst_n) begin q.delete(); nw = 0; nr = 0; end
    else if (take_w) begin q.push_back(write_data); nw++; end
  always @(posedge rclk)
    if (!rrst_n) begin q.delete(); nw = 0; nr = 0; end
    else if (take_r) begin
      if (q.size() > 0) exp_data <= q.pop_front();
      nr++;
    end

  int f_over = 0, f_under = 0, f_answer = 0, f_extra = 0, f_order = 0, f_level = 0;
  int    redge = -1;                   // the number of the last rising edge of rclk
  always @(posedge rclk) redge++;
  string first = "none";
  int    first_e = -1;
  function automatic void note(string rule);
    if (first == "none") begin first = rule; first_e = redge; end
  endfunction

  no_overflow:  assert property (@(posedge wclk) disable iff (!wrst_n) take_w |-> n < DEPTH)
                else begin f_over++; note("no_overflow"); end
  no_underflow: assert property (@(posedge rclk) disable iff (!rrst_n) take_r |-> n > 0)
                else begin f_under++; note("no_underflow"); end
  answered:     assert property (@(posedge rclk) disable iff (!rrst_n) take_r |=> read_valid)
                else begin f_answer++; note("answered"); end
  no_extra:     assert property (@(posedge rclk) disable iff (!rrst_n) !take_r |=> !read_valid)
                else begin f_extra++; note("no_extra"); end
  in_order:     assert property (@(posedge rclk) disable iff (!rrst_n) take_r |=> read_data == exp_data)
                else begin f_order++; note("in_order"); end
  level_safe:   assert property (@(posedge rclk) disable iff (!rrst_n) int'(read_level) <= n)
                else begin f_level++; note("level_safe"); end

  function automatic string summary();
    return $sformatf("no_overflow=%0d no_underflow=%0d answered=%0d no_extra=%0d in_order=%0d level_safe=%0d, first: %s",
                     f_over, f_under, f_answer, f_extra, f_order, f_level,
                     first == "none" ? "none" : $sformatf("%s at rclk edge %0d", first, first_e));
  endfunction
endmodule

bind afifo afifo_rules #(.DEPTH(DEPTH), .WIDTH(WIDTH)) rules (.*);

ConceptWhat does bind afifo afifo_rules rules (.*); need from the FIFO's design?

Every internal signal brought out as a port, because a bound module can see only the portsPorts whose names and widths match the rule module's ports, and a reset per domain for disable iffA single clock, because a bound module can only sample oneWrite access to the FIFO's source, to paste the rule module inside it

ConceptWhy does the brief ask for a read_level output, when empty already tells the read side what to do?

bind with .* needs at least one multi-bit output port to connect to the rule moduleIt lets the bench drop its model, since the FIFO already reports how many words it holds at each edgeThe rules can check the read side's view against the model's count, catching torn pointers the data never showsA FIFO with a level output no longer needs an empty flag, so the read side gets simpler

ConceptThe rules stay silent on the FIFO with the Gray coder in front of the synchronizer. What does that tell you?

A coder in front of a synchronizer is harmless in silicon too, so there is simply nothing to catchThe rules sample only at rclk, and the coder runs on wclk, so the rules never see its outputlevel_safe is disabled while the coder runs, so its failures are droppedIts fault is a gate-level glitch that zero-delay simulation never makes; a structural check must find it

Remember

A brief that fixes port names, gives each domain its own reset and exposes a level lets a verifier attach rules with bind and .*.
Rules for two clocks run on each side's own clock, with a model built from the ports; late flags are correct, so check that the level is never early.
Flags must tell the truth during reset: full and empty stay 1 until both sides are up, or the first words after a reset are lost.
Simulation rules catch torn pointers and lost words; logic in front of a synchronizer needs a structural CDC check.