// SVA form of the data check (used by commercial formal tools):
//   m_magic: assume property (@(posedge clk) $stable(magic));
//   a_order: assert property (@(posedge clk) disable iff (rst) tracking && ahead == 3'd0 && do_pop |-> dout == magic);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module fifo4 (input clk, input rst,
              input push, input [7:0] din, input pop,
              output [7:0] dout, output full, output empty);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;
  reg [2:0] count;
  assign full  = (count == 3'd4);
  assign empty = (count == 3'd0);
  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; count <= 3'd0;
    end else begin
      if (do_push) mem[wptr] <= din;
      if (do_push && !do_pop) wptr <= wptr + 2'd1;   // bug: should be if (do_push)
      if (do_pop)  rptr <= rptr + 2'd1;
      count <= count + do_push - do_pop;
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(posedge clk) if (!init) assert (count <= 3'd4);

  // tracked value: one word, chosen freely by the tool, followed through the FIFO
  (* anyconst *) reg [7:0] magic;
  reg       tracking = 1'b0;   // magic is inside the FIFO
  reg       done     = 1'b0;   // magic has already been through once
  reg [2:0] ahead;             // number of words in front of magic
  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    <= count - do_pop;
    end else if (tracking && do_pop) begin
      if (ahead == 3'd0) begin tracking <= 1'b0; done <= 1'b1; end
      else               ahead <= ahead - 3'd1;
    end
  // when magic reaches the head of the FIFO and is popped, the output is magic
  always @(posedge clk) if (!init && !rst && tracking && ahead == 3'd0 && do_pop) assert (dout == magic);
`endif
endmodule