Valid/Ready Pipelines and Skid Buffers

Long valid/ready pipelines have a timing problem: the ready signal travels backwards through every stage in one clock cycle. A skid buffer breaks that path by registering ready, at the cost of a second register that catches the one word that arrives while the output stalls. The control logic is small and full of corner cases, exactly the kind of block where formal finds bugs that tests miss. This article checks a skid buffer for protocol rules and data integrity and finds a word that is sent twice.

10 min read | Intermediate

What You'll Learn

• Explain what a skid buffer does and why its ready signal is a register
• Check a pipeline stage with input assumptions and output assertions
• Use a tracked value to detect lost, duplicated and reordered words
• Find a duplication bug that appears when a word arrives and leaves in the same cycle

Why a Skid Buffer

In a plain pipeline stage, in_ready is a function of out_ready: the stage can accept a word if its output is being taken. Chain ten such stages and the ready signal passes through ten levels of logic in one cycle. A skid buffer makes in_ready a register instead. Because the sender sees the stall one cycle late, one more word may arrive after the output stops, and the skid register holds it.

The Properties

A pipeline stage sits between two interfaces, so it gets assumptions on one side and assertions on the other, as in the input protocol assumptions article:

• Input side (assumptions): the sender holds in_valid and in_data while in_ready is low.
• Output side (assertions): the buffer holds out_valid and out_data while out_ready is low.
• Data integrity (assertion): every accepted word comes out exactly once, in order, unchanged.

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 data check uses a tracked value: when the word magic is accepted, record how many words are ahead of it in the buffer, count them down as words leave, and check that the next word out is magic when the count reaches 0.

The Design

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);
  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
endmodule

When a word arrives while main is full, the design parks it in the skid register. That is right if main is stalled, but wrong if main is handing out its word in the same cycle: then the new word should go straight into main.

Running It in ChipVerify Lab

The example contains the input assumption, the output assertion and the tracked-value check, written in the lab form. The run fails at step 3, and the tool chose magic = 254:

In step 1, the word 255 is accepted into main. In step 2, 255 is handed out (out_ready is high) while 254 arrives. The bug sends 254 to the skid register and leaves full_main set, so in step 3 the old word 255 is handed out a second time. The tracked value expected 254. With the fix, if (!full_main || give), all checks pass.

Corner Cases the Tool Explores

• A word arrives and leaves in the same cycle, at every fill level.
• The output stalls for one cycle, for many cycles, or toggles every cycle.
• The skid register fills and drains while new words wait at the input.
• Reset in the middle of all of these.

A simulation test would need a carefully designed traffic pattern for each. The formal run explores all of them in seconds, and the meant-to-fail check assert (!full_skid) confirms that the skid register is really used, at step 3.

Common Mistakes