// SVA form of the two properties:
//   a_full_rtl: assert property (@(posedge clk) disable iff (rst) full == (count == 3'd5));   // copied from the RTL
//   a_count:    assert property (@(posedge clk) disable iff (rst) count <= 3'd4);            // from the specification
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module fifo_count (input clk, input rst, input push, input pop,
                   output reg [2:0] count, output full, output empty);
  assign full  = (count == 3'd5);     // bug: a 4-entry FIFO is full at 4
  assign empty = (count == 3'd0);
  always @(posedge clk)
    if (rst)                count <= 3'd0;
    else if (push && !full) count <= count + 3'd1;
    else if (pop && !empty) count <= count - 3'd1;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // restates the RTL: passes, because it repeats the same mistake
  always @(posedge clk) if (!init) assert (full == (count == 3'd5));
  // from the specification: a 4-entry FIFO never holds more than 4
  always @(posedge clk) if (!init) assert (count <= 3'd4);
`endif
endmodule