// SVA form of the properties (used by commercial formal tools):
//   m_resp: assume property (@(posedge clk) disable iff (rst) resp |-> cnt != 2'd0);
//   a_max:  assert property (@(posedge clk) disable iff (rst) !(req && cnt == 2'd3));
//   a_dec:  assert property (@(posedge clk) disable iff (rst) resp && !req |=> cnt == $past(cnt) - 2'd1);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module txn_tracker (input clk, input rst, input go, input resp,
                    output req, output [1:0] outstanding);
  // issues read requests to a memory, at most 3 in flight
  reg [1:0] cnt;
  assign outstanding = cnt;
  assign req = go && (cnt != 2'd3);
  always @(posedge clk)
    if (rst)               cnt <= 2'd0;
    else if (req && !resp) cnt <= cnt + 2'd1;
    else if (!req && resp) cnt <= cnt - 2'd1;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // the memory only responds to a request that is in flight
  always @(*) if (!init) assume (!resp || cnt != 2'd0);
  // never more than 3 in flight, and no request when 3 are in flight
  always @(posedge clk) if (!init) assert (!(req && cnt == 2'd3));
  // a response always matches a request in flight: cnt never wraps
  always @(posedge clk) if (!init && !$past(rst) && $past(resp) && !$past(req)) assert (cnt == $past(cnt) - 2'd1 && $past(cnt) != 2'd0);
`endif
endmodule