// Base case: depth 10. Induction step: uncomment `define INDUCTION_STEP, depth 2.
// 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
// `define INDUCTION_STEP      // uncomment to run the induction step (depth 2) instead of the base case (depth 10)
  // reference count from the accepted operations
  reg [AW+1:0] n;                                  // no initial value: free in the induction step
  always @(posedge clk) n <= rst ? 0 : n + do_push - do_pop;
  // tracked value
  (* anyconst *) reg [W-1:0] magic;
  reg [AW+1:0] ahead; reg tracking, done;
  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
  // the properties
  wire p_flags = (full == (n == (1 << AW))) && (empty == (n == 0));
  wire p_order = !(tracking && ahead == 0 && do_pop) || dout == magic;
  // the helpers that make them inductive
  wire [AW:0]   diff = wptr - rptr;
  wire [AW-1:0] mpos = rptr[AW-1:0] + ahead[AW-1:0];
  wire h_count = (n == diff) && (n <= (1 << AW));
  wire h_magic = !tracking || (ahead < n && mem[mpos] == magic);
  wire all_ok  = p_flags && p_order && h_count && h_magic;
`ifndef INDUCTION_STEP
  // base case: from reset
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init && !rst) assert (all_ok);
`else
  // induction step, K = 1: start anywhere, all properties hold in step 0, check step 1
  always @(*) assume (!rst);
  reg [7:0] step = 8'd0;
  always @(posedge clk) step <= step + 8'd1;
  always @(*) if (step < 8'd1) assume (all_ok);
  always @(*) if (step == 8'd1) assert (all_ok);
`endif
`endif
endmodule