The goal: a FIFO another team can drop in without reading it

Ask for a 6-deep FIFO and Icarus stops before simulation: ERROR: fifo_ip.sv:24: fifo_ip: DEPTH must be a power of two, at least 2. Make the same request through Verilator with -Wno-fatal, and the build succeeds, runs, and fails 507 cycles of the self-checking test. A reusable block has to refuse a bad configuration in every flow its users run, and it has to arrive with the evidence that it works.

This project takes the synchronous FIFO from the memory part, keeps its contract, and packages it with everything this part taught: a package, checked parameters, an interface with modports, assertions built into the RTL, a file list, a lint run with one justified waiver, and a bounded proof.

Read the figure as one core and the files around it.

• Top: the package is compiled first. It holds the operation type and the depth check that the core calls while it elaborates.

• Left and right: the push side and the pop side, as plain ports. Icarus, Verilator and Yosys can all read the core.

• The two accent lines: the checks travel inside the RTL. Simulators read the SVA, Yosys reads the formal block, synthesis reads neither.

• Bottom: the interface is a second view of the same ports, for flows that support interfaces.

The spec

1. Parameters. WIDTH is at least 1. DEPTH is a power of two and at least 2. Any other value stops elaboration with a message that names the rule.

2. Reset. Clears both pointers, level_o, dout_o and dout_valid_o, so empty_o is 1 and full_o is 0. The storage array is not reset.

3. Acceptance. A push is accepted when push_i && !full_o, a pop when pop_i && !empty_o. At full, a push is refused even when a pop is accepted on the same edge: the conservative rule of the sync FIFO lesson.

4. Latency. A pop accepted at edge N puts its word on dout_o after edge N, with dout_valid_o high for that cycle. A word pushed at edge N can be popped at edge N + 1.

5. Level and order. level_o is accepted pushes minus accepted pops since reset. Words leave in the order they arrived, none lost and none repeated.

6. Deliverables. The package, the core, the interface view, a file list, a waiver file, a build script, and the checks in Done when.

The almost flags of the course FIFO are left out on purpose; adding one is a stretch goal.

Before you start

• Contract and Invariants: the FIFO rules this IP keeps.

• Packages and Compile Order and Parameter Types and Guards: the package and the guards.

• Common RTL property templates: the shape of every assertion below.

• Your First Formal Run: the Yosys flow, reused unchanged.

The project also uses Generate loops and conditionals for the guards, Interfaces, Modports, and Portability for the bundle, Compile-Order and Package Errors, Decoded for the order check, and Waiver rules that scale for the waiver.

Done when

Each row is a check you can run yourself. The last column is what the reference solution printed.

Reference solution

Each // name.sv comment starts a separate file. Line numbers in tool messages count from that comment, as in the full listing under Testbench.

The package: one type, one check

1
2
3
4
5
6
7
8
9
10
11
12

// fifo_ip_pkg.sv: shared types and the parameter check
package fifo_ip_pkg;
  // What one clock edge does, from the accepted push and pop.
  typedef enum logic [1:0] {
    OP_NONE = 2'b00, OP_POP = 2'b01, OP_PUSH = 2'b10, OP_BOTH = 2'b11
  } fifo_op_t;

  // A legal depth is a power of two and at least 2.
  function automatic logic depth_ok(input int depth);
    depth_ok = depth >= 2 && (depth & (depth - 1)) == 0;
  endfunction
endpackage

• `fifo_op_t` names the four things an edge can do, so the control code compares names, not bit pairs.

• `depth_ok` is a constant function: the core calls it during elaboration. (d & (d - 1)) == 0 is true only when one bit of d is set.

• No `return`. Yosys 0.69 stopped at the return line with syntax error, unexpected TOK_ID. Assigning to the function name works in all three tools.

• No `import`. Yosys 0.69 rejected import fifo_ip_pkg::*; in the module header and in the body (syntax error, unexpected TOK_IMPORT), so the core writes every package name in full, such as fifo_ip_pkg::depth_ok. Full names also rule out the two-package clash of case 3 in the errors lesson.

Parameters and the guard

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

// snippet: fifo_ip.sv, lines 1 to 28 (line 1 is the file comment)
module fifo_ip #(
  parameter int WIDTH = 8,
  parameter int DEPTH = 4
) (
  input  logic                       clk,
  input  logic                       rst_n,
  // push side
  input  logic                       push_i,
  input  logic [WIDTH-1:0]           din_i,
  output logic                       full_o,
  // pop side
  input  logic                       pop_i,
  output logic [WIDTH-1:0]           dout_o,
  output logic                       dout_valid_o,
  output logic                       empty_o,
  output logic [$clog2(DEPTH+1)-1:0] level_o
);
  localparam int          AW         = $clog2(DEPTH);
  localparam logic [AW:0] FULL_LEVEL = (AW + 1)'(DEPTH);

  // Elaboration-time guards: a bad configuration does not build.
  if (!fifo_ip_pkg::depth_ok(DEPTH)) begin : g_bad_depth
    $error("fifo_ip: DEPTH must be a power of two, at least 2");
  end
  if (WIDTH < 1) begin : g_bad_width
    $error("fifo_ip: WIDTH must be at least 1");
  end

The guards are generate if blocks, so they exist only when their condition is true, and $error inside them fires at elaboration. Here is a request for DEPTH = 6 in both tools:

$ iverilog -g2012 -Wall -P fifo_ip.DEPTH=6 -o /dev/null -f files.f
ERROR: fifo_ip.sv:24: fifo_ip: DEPTH must be a power of two, at least 2
       During elaboration  Scope: g_bad_depth
1 error(s) during elaboration.

$ verilator --lint-only -Wall -GDEPTH=6 fifo_ip.vlt -f files.f
%Warning-USERERROR: fifo_ip.sv:24:5: fifo_ip: DEPTH must be a power of two, at least 2
...
%Warning-WIDTHTRUNC: fifo_ip.sv:35:20: Operator ASSIGNW expects 3 bits on the Assign RHS, but Assign RHS's SUB generates 4 bits.
...
%Error: Exiting due to 4 warning(s)

• Icarus treats $error as an error: exit status 1, and the scope g_bad_depth names the guard. Icarus 13 accepts only a single string here; a %0d argument gave sorry: Elaboration tasks currently only support a single string argument.

• Verilator reports the same message as a warning, USERERROR. It stops the build only because warnings are fatal by default. The width warnings after it are the damage a bad depth does; the Common mistakes section shows what happens when that is switched off.

Pointers with a lap bit: why the depth must be a power of two

1
2
3
4
5
6
7
8
9
10
11
12
13

// snippet: fifo_ip.sv, lines 29 to 40

  logic [WIDTH-1:0]      mem [DEPTH];
  logic [AW:0]           wr_ptr, rd_ptr;  // AW address bits + 1 lap bit
  logic                  push_take, pop_take;
  fifo_ip_pkg::fifo_op_t op;

  assign level_o   = wr_ptr - rd_ptr;     // 0 to DEPTH, since DEPTH = 2**AW
  assign full_o    = (level_o == FULL_LEVEL);
  assign empty_o   = (level_o == '0);
  assign push_take = push_i && !full_o;
  assign pop_take  = pop_i && !empty_o;
  assign op        = fifo_ip_pkg::fifo_op_t'({push_take, pop_take});

Each pointer has AW address bits and one extra lap bit. The difference wr_ptr - rd_ptr is taken modulo 2^(AW+1), so it is the exact occupancy only when DEPTH = 2^AW. For DEPTH = 4 the pointers are 3 bits:

The course FIFO accepts any depth by keeping a separate count register and a wrap function. This IP drops both: its control state is the two pointers, the output register and the valid flop, 15 flops at 8x4.

Storage and control

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

// snippet: fifo_ip.sv, lines 42 to 61
  always_ff @(posedge clk) begin          // storage: no reset
    if (push_take) mem[wr_ptr[AW-1:0]] <= din_i;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wr_ptr       <= '0;
      rd_ptr       <= '0;
      dout_o       <= '0;
      dout_valid_o <= 1'b0;
    end else begin
      dout_valid_o <= pop_take;
      if (op == fifo_ip_pkg::OP_PUSH || op == fifo_ip_pkg::OP_BOTH)
        wr_ptr <= wr_ptr + 1'b1;
      if (op == fifo_ip_pkg::OP_POP || op == fifo_ip_pkg::OP_BOTH) begin
        rd_ptr <= rd_ptr + 1'b1;
        dout_o <= mem[rd_ptr[AW-1:0]];
      end
    end
  end

• Storage has no reset, so a synthesis tool can map it to RAM. Empty guarantees no stale word is ever read.

• Pointers move on the package's operation names. OP_BOTH moves both, and level_o is unchanged.

• Output is registered: dout_o and dout_valid_o change on the edge that accepts the pop, as the contract requires.

Checks that travel with the RTL

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

// snippet: fifo_ip.sv, lines 63 to 98
`ifdef FORMAL
  // Yosys reads immediate assertions only: the bounded proof.
  logic f_past = 1'b0;
  always_ff @(posedge clk) f_past <= 1'b1;
  always @(*) if (!f_past) assume (!rst_n);          // start in reset
  always @(*) if (f_past) begin
    f_bounds: assert (level_o <= FULL_LEVEL);
    f_flags:  assert (!(full_o && empty_o));
    c_full:   cover  (full_o);                       // the bound reaches full
  end
  always_ff @(posedge clk) if (f_past && $past(rst_n) && rst_n) begin
    f_no_ovf: assert (!$past(push_i && full_o) || wr_ptr == $past(wr_ptr));
    f_no_udf: assert (!$past(pop_i && empty_o) ||
                      (rd_ptr == $past(rd_ptr) && !dout_valid_o));
    f_count:  assert (level_o ==
                      $past(level_o) + $past(push_take) - $past(pop_take));
  end
`elsif SYNTHESIS
  // synthesis: no checks
`elsif __ICARUS__
  // Icarus 13 cannot parse concurrent SVA; the bench checks the same rules
`else
  // Built-in SVA, for simulators that run concurrent assertions.
  a_bounds: assert property (@(posedge clk) disable iff (!rst_n)
              level_o <= FULL_LEVEL);
  a_flags:  assert property (@(posedge clk) disable iff (!rst_n)
              !(full_o && empty_o));
  a_no_ovf: assert property (@(posedge clk) disable iff (!rst_n)
              push_i && full_o |=> $stable(wr_ptr));
  a_no_udf: assert property (@(posedge clk) disable iff (!rst_n)
              pop_i && empty_o |=> $stable(rd_ptr) && !dout_valid_o);
  a_count:  assert property (@(posedge clk) disable iff (!rst_n)
              1'b1 |=> level_o == $past(level_o) + $past(push_take)
                                                 - $past(pop_take));
`endif
endmodule

One file serves three tools, and each reads a different branch:

• Why two forms. Yosys 0.69 without a commercial front end does not parse clocked properties (syntax error, unexpected '@'), and Icarus 13 printed sorry: concurrent_assertion_item not supported and then syntax errors at |=>.

• What they check. Bounds and flags every cycle; a refused push or pop leaves its pointer still; the level changes by exactly accepted pushes minus accepted pops. The bench's model checks data order.

• `c_full` is a cover, not a check: it proves the bounded run is deep enough to reach full.

The interface view

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

// snippet: fifo_if.sv and fifo_ip_if.sv (Verilator flows)
// fifo_if.sv: one bundle, a view for each side
interface fifo_if #(parameter int WIDTH = 8, parameter int DEPTH = 4) (
  input logic clk, rst_n
);
  logic                       push, full, pop, dout_valid, empty;
  logic [WIDTH-1:0]           din, dout;
  logic [$clog2(DEPTH+1)-1:0] level;

  modport push_side (input clk, rst_n, full, output push, din);
  modport pop_side  (input clk, rst_n, dout, dout_valid, empty, level,
                     output pop);
  modport fifo      (input clk, rst_n, push, din, pop,
                     output full, dout, dout_valid, empty, level);
endinterface
// fifo_ip_if.sv: the same core behind the bundle
module fifo_ip_if #(parameter int WIDTH = 8, parameter int DEPTH = 4) (
  fifo_if.fifo bus
);
  fifo_ip #(.WIDTH(WIDTH), .DEPTH(DEPTH)) u_core (
    .clk(bus.clk), .rst_n(bus.rst_n),
    .push_i(bus.push), .din_i(bus.din), .full_o(bus.full),
    .pop_i(bus.pop), .dout_o(bus.dout), .dout_valid_o(bus.dout_valid),
    .empty_o(bus.empty), .level_o(bus.level));
endmodule

The core keeps plain ports, which is the portable boundary the interfaces lesson recommends. Teams whose tools support interfaces wrap it. A test with a producer on push_side and a consumer on pop_side ran in Verilator; Icarus 13 rejects the interface port:

$ verilator --binary --assert -Mdir obj_if --top-module tb_fifo_ip_if fifo_ip.vlt -f files.f fifo_if.sv fifo_ip_if.sv tb_fifo_ip_if.sv
$ ./obj_if/Vtb_fifo_ip_if
PASS: 1065 words through the modports, all in order

$ iverilog -g2012 -Wall -o /dev/null -f files.f fifo_if.sv fifo_ip_if.sv tb_fifo_ip_if.sv
fifo_ip_if.sv:3: syntax error
fifo_ip_if.sv:3: Errors in port declarations.
...

File list, waiver and build script

// files.f: packages first, then modules
fifo_ip_pkg.sv
fifo_ip.sv

// fifo_ip.vlt
`verilator_config
// Waiver: rule SYNCASYNCNET | scope: rst_n in fifo_ip.sv only
// Rationale: rst_n is an async reset for the flops; the "sync" use is the
// disable iff of the built-in assertions, which build no hardware.
// Owner: fifo_ip maintainer | Expiry: revisit if rst_n drives any new logic
lint_off -rule SYNCASYNCNET -file "*fifo_ip.sv" -match "*'rst_n'*"

Without the waiver file, lint stops on one warning. It is the only one, and the waiver above carries the five parts from the waiver lesson: rule, scope, rationale, owner and expiry.

$ verilator --lint-only -Wall -f files.f
%Warning-SYNCASYNCNET: fifo_ip.sv:7:38: Signal flopped as both synchronous and async: 'rst_n'
                       fifo_ip.sv:47:10: ... Location of async usage
...
                       fifo_ip.sv:86:59: ... Location of sync usage
...
%Error: Exiting due to 1 warning(s)

The build script runs every check in order. check_order.sh is the order check from Compile-Order and Package Errors, Decoded; with the two files swapped it prints ORDER: fifo_ip.sv uses fifo_ip_pkg:: but fifo_ip_pkg is not declared earlier in bad.f.

#!/bin/sh
# build.sh: order check, both simulators, lint, then the bounded proof
set -e
./check_order.sh files.f
iverilog -g2012 -Wall -o tb.vvp -f files.f tb_fifo_ip.sv
vvp -n tb.vvp
verilator --lint-only -Wall fifo_ip.vlt -f files.f
verilator --binary --assert -Mdir obj --top-module tb_fifo_ip \
  fifo_ip.vlt -f files.f tb_fifo_ip.sv > obj.log
./obj/Vtb_fifo_ip
for cfg in "8 4" "32 16" "1 2"; do ./formal.sh $cfg 24; done

The test

The bench, listed under Testbench, has one checker module per configuration, each with its own clock and a ring-buffer model of the contract. Each runs the corners first (pop on empty, fill, push on full, push and pop on full, drain), then 4000 seeded random cycles in 200-cycle phases that lean towards pushing and then towards popping, so every configuration fills and drains many times. After every edge it compares dout_valid_o, dout_o, level_o, full_o and empty_o with the model. The same bench ran in both simulators with identical output:

$ ./build.sh
order OK: fifo_ip_pkg
fifo_ip 1x2: 1841 words in order, full 960 cycles, empty 944 cycles, 1368 refused
fifo_ip 8x4: 2004 words in order, full 740 cycles, empty 643 cycles, 1039 refused
fifo_ip 32x16: 2118 words in order, full 545 cycles, empty 485 cycles, 742 refused
PASS: 3 configurations, every word in order, flags and level match the model
...

• Full and empty counts prove both edges of every configuration were reached hundreds of times, not just once in the directed part.

• Refused counts requests the FIFO turned down. Each one is a chance for an overflow or underflow bug to show.

• The order of the lines does not matter: the three checkers run in parallel and each prints when its own run ends.

The SVA on a seeded bug

Remove the full guard, a plausible slip when editing the acceptance line:

// snippet: the seeded bug in fifo_ip.sv, line 38
  assign push_take = push_i;              // seeded bug: no full guard

$ ./obj/Vtb_fifo_ip                       # Verilator, --assert
[75] %Error: fifo_ip.sv:86: Assertion failed in tb_fifo_ip.c2.dut.a_bounds: 'assert' failed.
%Error: fifo_ip.sv:86: Verilog $stop

$ vvp -n tb.vvp                            # Icarus, no SVA
FATAL: tb_fifo_ip.sv:64: FAIL: fifo_ip 1x2: 1738 bad cycles, first at 66
       Time: 40106  Scope: tb_fifo_ip.c2

• The SVA stops at time 75, the first edge after the bad push, and names the rule and the instance: the 1x2 FIFO went past DEPTH.

• The bench caught the same push at time 66, one time unit after the edge it checks, but reports only at the end of the run. Both point at the same edge; the assertion says which rule broke.

• On the good RTL the Verilator run prints no assertion message at all.

The bounded proof

formal.sh is the flow from Your First Formal Run, with chparam choosing the configuration. It runs a bounded check from reset, then induction, then the cover:

#!/bin/sh
# formal.sh WIDTH DEPTH STEPS: bounded check, induction, then cover
set -e
yosys -q -p "read_verilog -formal -sv fifo_ip_pkg.sv fifo_ip.sv;
  chparam -set WIDTH $1 -set DEPTH $2 fifo_ip; prep -top fifo_ip;
  async2sync; dffunmap; write_smt2 -wires fifo_ip.smt2"
yosys-smtbmc -s z3 -t $3 fifo_ip.smt2 | tail -1
yosys-smtbmc -s z3 -i -t $3 fifo_ip.smt2 | tail -1
yosys-smtbmc -s z3 -c -t $3 fifo_ip.smt2 | grep Reached

$ ./formal.sh 8 4 24
##   0:00:00  Status: PASSED
##   0:00:00  Status: PASSED
##   0:00:00  Reached cover statement in step 5 at fifo_ip: c_full
$ ./formal.sh 32 16 24
##   0:00:01  Status: PASSED
##   0:00:00  Status: PASSED
##   0:00:04  Reached cover statement in step 17 at fifo_ip: c_full
$ ./formal.sh 1 2 24
##   0:00:00  Status: PASSED
##   0:00:00  Status: PASSED
##   0:00:00  Reached cover statement in step 3 at fifo_ip: c_full

• First line: no input sequence breaks the five assertions in 24 cycles from reset.

• Second line: induction passes, so the bounded result holds for every cycle. f_bounds needs no helper: from any state with the level at most DEPTH, the guards keep it there.

• Third line: full is reached at step 1 + DEPTH (one reset step, then DEPTH pushes). With 12 steps the 32x16 cover was Unreached, and the overflow checks would never have seen a full FIFO.

• On the seeded bug the bounded check fails at step 6 for 8x4: Assert failed in fifo_ip: f_bounds, a fifth push into a full FIFO.

The proof covers the occupancy and flag invariants. Data order is checked by the bench's model, not proved.

Common mistakes

Stretch goals

• First-word fall-through. Add parameter bit FWFT = 0 and a generate if that chooses the registered output or a fall-through output. Add an assertion that dout_valid_o equals !empty_o in FWFT mode. See Generate loops and conditionals.

• Almost full. Add AF_LEVEL with a guard for 1 to DEPTH, as in Almost Flags and Parameter Edges, and a formal check that the flag equals level_o >= AF_LEVEL.

• AXI-Stream wrapper. Map tvalid and tready onto push and !full_o on the input side, and onto !empty_o and pop on the output side, following Core AXI-Stream Signals. The registered output needs a small skid stage to keep tdata stable while tready is low.

Related topics

• Sync FIFO verification and signoff

• Your first formal run

Testbench

The package, the core and the bench as one listing. Each // name.sv comment starts a separate file. The interface view and its test are in The interface view above.

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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195

// fifo_ip_pkg.sv: shared types and the parameter check
package fifo_ip_pkg;
  // What one clock edge does, from the accepted push and pop.
  typedef enum logic [1:0] {
    OP_NONE = 2'b00, OP_POP = 2'b01, OP_PUSH = 2'b10, OP_BOTH = 2'b11
  } fifo_op_t;

  // A legal depth is a power of two and at least 2.
  function automatic logic depth_ok(input int depth);
    depth_ok = depth >= 2 && (depth & (depth - 1)) == 0;
  endfunction
endpackage
// fifo_ip.sv: synchronous FIFO, registered output, power-of-two depth
module fifo_ip #(
  parameter int WIDTH = 8,
  parameter int DEPTH = 4
) (
  input  logic                       clk,
  input  logic                       rst_n,
  // push side
  input  logic                       push_i,
  input  logic [WIDTH-1:0]           din_i,
  output logic                       full_o,
  // pop side
  input  logic                       pop_i,
  output logic [WIDTH-1:0]           dout_o,
  output logic                       dout_valid_o,
  output logic                       empty_o,
  output logic [$clog2(DEPTH+1)-1:0] level_o
);
  localparam int          AW         = $clog2(DEPTH);
  localparam logic [AW:0] FULL_LEVEL = (AW + 1)'(DEPTH);

  // Elaboration-time guards: a bad configuration does not build.
  if (!fifo_ip_pkg::depth_ok(DEPTH)) begin : g_bad_depth
    $error("fifo_ip: DEPTH must be a power of two, at least 2");
  end
  if (WIDTH < 1) begin : g_bad_width
    $error("fifo_ip: WIDTH must be at least 1");
  end

  logic [WIDTH-1:0]      mem [DEPTH];
  logic [AW:0]           wr_ptr, rd_ptr;  // AW address bits + 1 lap bit
  logic                  push_take, pop_take;
  fifo_ip_pkg::fifo_op_t op;

  assign level_o   = wr_ptr - rd_ptr;     // 0 to DEPTH, since DEPTH = 2**AW
  assign full_o    = (level_o == FULL_LEVEL);
  assign empty_o   = (level_o == '0);
  assign push_take = push_i && !full_o;
  assign pop_take  = pop_i && !empty_o;
  assign op        = fifo_ip_pkg::fifo_op_t'({push_take, pop_take});

  always_ff @(posedge clk) begin          // storage: no reset
    if (push_take) mem[wr_ptr[AW-1:0]] <= din_i;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wr_ptr       <= '0;
      rd_ptr       <= '0;
      dout_o       <= '0;
      dout_valid_o <= 1'b0;
    end else begin
      dout_valid_o <= pop_take;
      if (op == fifo_ip_pkg::OP_PUSH || op == fifo_ip_pkg::OP_BOTH)
        wr_ptr <= wr_ptr + 1'b1;
      if (op == fifo_ip_pkg::OP_POP || op == fifo_ip_pkg::OP_BOTH) begin
        rd_ptr <= rd_ptr + 1'b1;
        dout_o <= mem[rd_ptr[AW-1:0]];
      end
    end
  end

`ifdef FORMAL
  // Yosys reads immediate assertions only: the bounded proof.
  logic f_past = 1'b0;
  always_ff @(posedge clk) f_past <= 1'b1;
  always @(*) if (!f_past) assume (!rst_n);          // start in reset
  always @(*) if (f_past) begin
    f_bounds: assert (level_o <= FULL_LEVEL);
    f_flags:  assert (!(full_o && empty_o));
    c_full:   cover  (full_o);                       // the bound reaches full
  end
  always_ff @(posedge clk) if (f_past && $past(rst_n) && rst_n) begin
    f_no_ovf: assert (!$past(push_i && full_o) || wr_ptr == $past(wr_ptr));
    f_no_udf: assert (!$past(pop_i && empty_o) ||
                      (rd_ptr == $past(rd_ptr) && !dout_valid_o));
    f_count:  assert (level_o ==
                      $past(level_o) + $past(push_take) - $past(pop_take));
  end
`elsif SYNTHESIS
  // synthesis: no checks
`elsif __ICARUS__
  // Icarus 13 cannot parse concurrent SVA; the bench checks the same rules
`else
  // Built-in SVA, for simulators that run concurrent assertions.
  a_bounds: assert property (@(posedge clk) disable iff (!rst_n)
              level_o <= FULL_LEVEL);
  a_flags:  assert property (@(posedge clk) disable iff (!rst_n)
              !(full_o && empty_o));
  a_no_ovf: assert property (@(posedge clk) disable iff (!rst_n)
              push_i && full_o |=> $stable(wr_ptr));
  a_no_udf: assert property (@(posedge clk) disable iff (!rst_n)
              pop_i && empty_o |=> $stable(rd_ptr) && !dout_valid_o);
  a_count:  assert property (@(posedge clk) disable iff (!rst_n)
              1'b1 |=> level_o == $past(level_o) + $past(push_take)
                                                 - $past(pop_take));
`endif
endmodule
// tb_fifo_ip.sv: one checker per configuration, each against a model
module fifo_ip_check #(
  parameter int WIDTH = 8, parameter int DEPTH = 4, parameter int SEED = 1
) (output logic done);
  localparam int LW = $clog2(DEPTH + 1);
  logic clk = 1'b0, rst_n = 1'b0;
  logic push_i = 1'b0, pop_i = 1'b0;
  logic [WIDTH-1:0] din_i = '0, dout_o;
  logic dout_valid_o, full_o, empty_o;
  logic [LW-1:0] level_o;

  fifo_ip #(.WIDTH(WIDTH), .DEPTH(DEPTH)) dut (.*);
  always #5 clk = ~clk;

  // Reference model: a ring of DEPTH words and a count.
  logic [WIDTH-1:0] model [DEPTH];
  int head = 0, tail = 0, count = 0;
  int errors = 0, words = 0, full_cycles = 0, empty_cycles = 0, refused = 0;
  logic [31:0] rnd = SEED;
  time first_bad;

  task automatic step(input logic push, pop, input logic [WIDTH-1:0] data);
    logic take_push, take_pop;
    logic [WIDTH-1:0] expected;
    @(negedge clk);
    push_i = push; pop_i = pop; din_i = data;
    take_push = push && (count < DEPTH);  // refused when full, even with a pop
    take_pop  = pop  && (count > 0);      // refused when empty, even with a push
    if ((push && !take_push) || (pop && !take_pop)) refused++;
    expected = model[head];
    if (take_push) begin model[tail] = data; tail = (tail + 1) % DEPTH; end
    if (take_pop)  begin head = (head + 1) % DEPTH; words++; end
    count = count + int'(take_push) - int'(take_pop);
    @(posedge clk); #1;
    if (dout_valid_o !== take_pop || (take_pop && dout_o !== expected) ||
        level_o !== LW'(count) || full_o !== (count == DEPTH) ||
        empty_o !== (count == 0)) begin
      if (errors == 0) first_bad = $time;
      errors++;
    end
    if (full_o)  full_cycles++;
    if (empty_o) empty_cycles++;
  endtask

  initial begin
    done = 1'b0;
    repeat (2) @(posedge clk);
    @(negedge clk) rst_n = 1'b1;
    step(0, 1, '0);                                   // pop on empty
    for (int i = 0; i < DEPTH; i++) step(1, 0, WIDTH'(i + 1));  // fill
    step(1, 0, '1);                                   // push on full
    step(1, 1, '1);                                   // both on full
    for (int i = 0; i < DEPTH; i++) step(0, 1, '0);   // drain
    for (int n = 0; n < 4000; n++) begin              // seeded random traffic,
      logic busy, half, fill;                         // 200-cycle phases that
      rnd  = rnd * 32'd1664525 + 32'd1013904223;      // lean to push, then pop
      busy = rnd[31] | rnd[30];                       // 3 in 4
      half = rnd[29];                                 // 1 in 2
      fill = ((n / 200) % 2 == 0);
      step(fill ? busy : half, fill ? half : busy, WIDTH'({rnd[23:8], rnd[23:8]}));
    end
    while (count > 0) step(0, 1, '0);
    if (errors != 0)
      $fatal(1, "FAIL: fifo_ip %0dx%0d: %0d bad cycles, first at %0t",
             WIDTH, DEPTH, errors, first_bad);
    if (full_cycles == 0 || empty_cycles == 0)
      $fatal(1, "FAIL: fifo_ip %0dx%0d never full or never empty", WIDTH, DEPTH);
    $display("fifo_ip %0dx%0d: %0d words in order, full %0d cycles, empty %0d cycles, %0d refused",
             WIDTH, DEPTH, words, full_cycles, empty_cycles, refused);
    done = 1'b1;
  end
endmodule

module tb_fifo_ip;
  logic d0, d1, d2;
  fifo_ip_check #(.WIDTH(8),  .DEPTH(4),  .SEED(11)) c0 (.done(d0));
  fifo_ip_check #(.WIDTH(32), .DEPTH(16), .SEED(22)) c1 (.done(d1));
  fifo_ip_check #(.WIDTH(1),  .DEPTH(2),  .SEED(33)) c2 (.done(d2));
  initial begin
    wait (d0 === 1'b1 && d1 === 1'b1 && d2 === 1'b1);
    $display("PASS: 3 configurations, every word in order, flags and level match the model");
    $finish;
  end
  initial begin #2_000_000; $fatal(1, "FAIL: timeout"); end
endmodule