// SVA form of the protocol rules (used by commercial formal tools):
//   m_in_hold:  assume property (@(posedge clk) disable iff (rst) in_valid && !in_ready |=> in_valid && $stable(in_data));
//   a_out_hold: assert property (@(posedge clk) disable iff (rst) out_valid && !out_ready |=> out_valid && $stable(out_data));
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module skid (input clk, input rst,
             input in_valid, output in_ready, input [7:0] in_data,
             output out_valid, input out_ready, output [7:0] out_data);
  // skid buffer: registers in_ready so that it does not depend combinationally on out_ready
  reg       full_main, full_skid;
  reg [7:0] main, skid_r;
  assign in_ready  = !full_skid;
  assign out_valid = full_main;
  assign out_data  = main;
  wire take = in_valid && in_ready;
  wire give = out_valid && out_ready;
  always @(posedge clk)
    if (rst) begin
      full_main <= 1'b0; full_skid <= 1'b0;
    end else begin
      if (full_skid) begin                       // drain the skid register first
        if (give) begin main <= skid_r; full_skid <= 1'b0; end
      end else if (take) begin
        if (!full_main)         begin main <= in_data; full_main <= 1'b1; end   // bug: ignores a word leaving main in the same cycle
        else                    begin skid_r <= in_data; full_skid <= 1'b1; end
      end else if (give) full_main <= 1'b0;
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // input side: the sender follows the valid/ready rules
  always @(posedge clk) if (!init && !$past(rst) && $past(in_valid) && !$past(in_ready)) assume (in_valid && in_data == $past(in_data));
  // output side: the buffer follows them too
  always @(posedge clk) if (!init && !$past(rst) && $past(out_valid) && !$past(out_ready)) assert (out_valid && out_data == $past(out_data));
  // data integrity: words come out in order, none lost or duplicated (tracked value)
  (* anyconst *) reg [7:0] magic;
  reg [2:0] ahead; reg tracking = 1'b0, done = 1'b0;
  wire [2:0] held = full_main + full_skid;
  always @(posedge clk)
    if (rst) begin tracking <= 1'b0; done <= 1'b0; end
    else if (!tracking && !done && take && in_data == magic) begin tracking <= 1'b1; ahead <= held - give; end
    else if (tracking && give) begin
      if (ahead == 3'd0) begin tracking <= 1'b0; done <= 1'b1; end
      else ahead <= ahead - 3'd1;
    end
  always @(*) if (!init && !rst && tracking && ahead == 3'd0 && give) assert (out_data == magic);
`endif
endmodule