Handshake Properties

Blocks talk to each other through handshakes. A sender offers data and a receiver takes it, and both sides follow a few simple rules so that no word is lost or duplicated. Those rules are among the most valuable properties you can write, because handshake bugs show up only with particular timing between the two sides, exactly the timing a test rarely produces. This article covers the request/acknowledge and valid/ready handshakes and finds a real bug in a valid/ready sender.

10 min read | Beginner to Intermediate

What You'll Learn

• State the rules of the request/acknowledge and valid/ready handshakes as properties
• Check that a sender holds its request and keeps its data stable while waiting
• Decide which rules are assertions and which are assumptions for a given block
• Find a data-stability bug in a valid/ready sender

Request and Acknowledge

In a request/acknowledge handshake, the sender raises req and waits. The receiver answers with ack when it has taken the data. The usual rules:

// the sender holds the request until it is acknowledged
a_req_hold:  assert property (@(posedge clk) disable iff (rst) req && !ack |=> req);
// the data does not change while the request waits
a_req_data:  assert property (@(posedge clk) disable iff (rst) req && !ack |=> $stable(data));
// the receiver only acknowledges a request
a_ack_valid: assert property (@(posedge clk) disable iff (rst) ack |-> req);

Many protocols add a timing rule for the receiver, such as req |-> ##[1:8] ack, so that the sender is never left waiting forever.

Valid and Ready

The valid/ready handshake is the standard for streaming data inside chips and on buses such as AXI. The sender drives valid and data, the receiver drives ready, and a word moves in every cycle where both are high. There is no separate acknowledge. A handshake can happen in every cycle, so the interface can move one word per cycle.

The rules for the sender:

// once valid, stay valid until the handshake
a_valid_hold: assert property (@(posedge clk) disable iff (rst) valid && !ready |=> valid);
// and keep the data stable until then
a_data_hold:  assert property (@(posedge clk) disable iff (rst) valid && !ready |=> $stable(data));

The receiver may raise and drop ready whenever it likes. And the sender must not wait for ready before it raises valid, otherwise two blocks that both wait for the other would never start. That last rule is about the structure of the logic, not about a value in a cycle, so it is checked by review rather than by a property.

Assertion or Assumption?

The same rule can be an assertion or an assumption, depending on which block you check. When you check the sender, the sender rules are assertions: the sender must follow them. Rules for the receiver are assumptions: they describe the environment the sender can rely on. When you check the receiver, it is the other way round.

For a valid/ready sender, there is almost nothing to assume, because the receiver may drive ready freely. That is good news: the tool tries every possible pattern of ready, including the cruel ones, such as a receiver that is never ready.

The Design: a Valid/Ready Sender

This sender produces the words 0, 1, 2 and so on, one per handshake. go asks it to offer the next word:

module vr_sender (input clk, input rst, input go, input ready,
                  output reg valid, output reg [7:0] data);
  always @(posedge clk)
    if (rst) begin
      valid <= 1'b0;
      data  <= 8'd0;
    end else begin
      if (go)                valid <= 1'b1;
      else if (ready)        valid <= 1'b0;
      if (valid)             data  <= data + 8'd1;   // bug: should be (valid && ready)
    end
endmodule

The data counter advances whenever valid is high, not only when a handshake happens. With a receiver that is always ready, which is what a simple testbench often uses, the two are the same and the bug is invisible.

Running It in ChipVerify Lab

The |=> rules become checks on the previous cycle:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // valid is not withdrawn before the handshake
  always @(posedge clk) if (!init && !$past(rst) && $past(valid) && !$past(ready)) assert (valid);
  // data stays stable while waiting
  always @(posedge clk) if (!init && !$past(rst) && $past(valid) && !$past(ready)) assert (data == $past(data));
`endif

There is no assumption on ready or go. The run fails at step 4:

The tool chose a receiver that is never ready. valid rises in step 2 with word 0, and in step 3 the data is already 1, although no handshake has happened. Word 0 is lost. Change the condition to if (valid && ready) and the run passes.

Try the other classic sender bug too: replace else if (ready) valid <= 1'b0; with else valid <= 1'b0;. Now the sender withdraws its offer when go drops, whether or not the word was taken. The first assertion fails at step 4.

Common Mistakes

// after a handshake, the next word is the previous word plus 1
always @(posedge clk)
  if (!init && !rst && !$past(rst) && $past(valid && ready))
    assert (data == $past(data) + 8'd1);