// Properties use a reference count n kept by the formal code:
//   a_full: assert property (@(posedge clk) disable iff (rst) full == (n == 3'd4));
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module fifo_ptr (input clk, input rst, input push, input [7:0] din, input pop,
                 output [7:0] dout, output full, output empty);
  // 4-entry FIFO with pointers only (no count register)
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;
  assign empty = (wptr == rptr);
  assign full  = (wptr + 2'd1 == rptr);          // bug: this FIFO can only hold 3 words
  assign dout  = mem[rptr];
  wire do_push = push && !full;
  wire do_pop  = pop && !empty;
  always @(posedge clk)
    if (rst) begin
      wptr <= 2'd0; rptr <= 2'd0;
    end else begin
      if (do_push) begin mem[wptr] <= din; wptr <= wptr + 2'd1; end
      if (do_pop)  rptr <= rptr + 2'd1;
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // reference count, kept by the formal code from the accepted operations
  reg [2:0] n = 3'd0;
  always @(posedge clk) n <= rst ? 3'd0 : n + do_push - do_pop;
  // specification: 4 entries, full exactly at 4, empty exactly at 0
  always @(*) if (!init) assert (n <= 3'd4);
  always @(*) if (!init) assert (full == (n == 3'd4));
  always @(*) if (!init) assert (empty == (n == 3'd0));
`endif
endmodule