// Parameters: W = data width, AW = log2(entries). The depth must cover 2^AW pushes plus a few cycles.
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module fifo_p #(parameter W = 8, parameter AW = 2) (input clk, input rst, input push, input [W-1:0] din, input pop,
                                                     output [W-1:0] dout, output full, output empty);
  reg [W-1:0] mem [0:(1<<AW)-1];
  reg [AW:0] wptr, rptr;
  assign empty = (wptr == rptr);
  assign full  = (wptr == {~rptr[AW], rptr[AW-1:0]});
  assign dout  = mem[rptr[AW-1:0]];
  wire do_push = push && !full;
  wire do_pop  = pop && !empty;
  always @(posedge clk)
    if (rst) begin wptr <= 0; rptr <= 0; end
    else begin
      if (do_push) begin mem[wptr[AW-1:0]] <= din; wptr <= wptr + 1'b1; end
      if (do_pop)  rptr <= rptr + 1'b1;
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [AW+1:0] n = 0;
  always @(posedge clk) n <= rst ? 0 : n + do_push - do_pop;
  always @(*) if (!init) assert (full == (n == (1 << AW)) && empty == (n == 0));
  // tracked value
  (* anyconst *) reg [W-1:0] magic;
  reg [AW+1:0] ahead; reg tracking = 1'b0, done = 1'b0;
  always @(posedge clk)
    if (rst) begin tracking <= 1'b0; done <= 1'b0; end
    else if (!tracking && !done && do_push && din == magic) begin tracking <= 1'b1; ahead <= n - do_pop; end
    else if (tracking && do_pop) begin
      if (ahead == 0) begin tracking <= 1'b0; done <= 1'b1; end
      else ahead <= ahead - 1'b1;
    end
  always @(*) if (!init && !rst && tracking && ahead == 0 && do_pop) assert (dout == magic);
`endif
endmodule