Progress in a Handshake Chain

On this page

Part 5 of 10, lesson 10 of 20Formal ApplicationsAll levels

Why it matters

A valid that waits for a ready, behind a ready that waits for that valid, closes a cycle of waits: each side waits for the other to move first and nothing moves. The symptom is a hang that appears from the first beat, or only when both stages fill together, which is why block-level tests with an always-ready neighbour can miss the second form. The structural check finds the cycle in seconds from the handshake lines; the temporal proof then shows beats actually drain, with a bound.

The core idea

Do the cheap check first. List every wait relation between the handshake signals of the chain, a signal waits for another when its value, or the value it will load, is conditioned on it, and look for a cycle: the same graph search as the definitions lesson, now on real signal names. A cycle through a register is still a wait cycle, because the register only changes when its condition is met. Only when the graph is acyclic does the temporal proof begin: accept a beat, then bound the cycles until something is delivered, with the downstream ready left free except for the documented stall bound. A bound on delivery is a safety property, provable in the open flow; true eventually is not.

Worked example: the dependency checker

The lesson-local chain has two one-beat stages. Its handshake lines come in two forms, the intended one and the buggy one in which stage 1 raises valid only after stage 2 has raised its ready flag, and the flag rises only after valid. The checker below reads those exact lines, the same text that is pasted into the module further down, builds the wait-for edges, and searches for a cycle. The intended form is acyclic; the buggy form closes the cycle s1_valid to rdy2 and back:

example.py

import re

OK_LINES = [
    "assign s1_valid = v1;",
    "assign s2_ready = !v2 || out_ready;",
    "always @(posedge clk) rdy2 <= 1'b0;",
]
BUG_LINES = [
    "assign s1_valid = v1 && rdy2;",
    "assign s2_ready = rdy2;",
    "always @(posedge clk) rdy2 <= !rst && s1_valid && (!v2 || out_ready);",
]
SIGNALS = {"v1", "v2", "rdy2", "s1_valid", "s2_ready", "out_ready", "rst"}

def edges(lines):
    graph = {}
    for line in lines:
        m = re.match(r"(?:assign|always @\(posedge clk\))\s+(\w+)\s*(?:=|<=)\s*(.*);", line)
        target, rhs = m.group(1), m.group(2)
        graph.setdefault(target, set()).update(w for w in re.findall(r"[A-Za-z_][A-Za-z_0-9]*", rhs) if w in SIGNALS)
    return {k: sorted(v) for k, v in graph.items()}

def find_cycle(graph):
    colour = {}
    def visit(node, stack):
        colour[node] = 1
        for nxt in graph.get(node, []):
            if colour.get(nxt, 0) == 1:
                return stack + [nxt]
            if colour.get(nxt, 0) == 0:
                hit = visit(nxt, stack + [nxt])
                if hit:
                    return hit
        colour[node] = 2
        return None
    for node in list(graph):
        if colour.get(node, 0) == 0:
            hit = visit(node, [node])
            if hit:
                return hit
    return None

assert find_cycle(edges(OK_LINES)) is None
cycle = find_cycle(edges(BUG_LINES))
assert cycle is not None and cycle[0] == cycle[-1]
assert "s1_valid" in cycle and "rdy2" in cycle
# the check can fail the other way too: remove the valid-to-ready edge and the cycle disappears
fixed = [BUG_LINES[0].replace(" && rdy2", ""), BUG_LINES[1], BUG_LINES[2]]
assert find_cycle(edges(fixed)) is None
print("PASS: intended lines acyclic; buggy lines close the cycle", " -> ".join(cycle))

Worked example: bounded progress proved and stuck

The temporal proof uses an age counter: the number of cycles since the last delivery while the chain holds a beat. The bound is derived, not tuned: a beat spends one cycle in stage 1 before it moves, then the downstream may stall it at most two consecutive cycles, so the age reaches three at the delivering cycle and no higher. One assumption on the environment keeps that honest: the downstream is not stalled for a third consecutive cycle while it holds a beat. It constrains out_ready only, never a design output. A bound on stalls is a stronger statement than fairness (ready infinitely often) and, like any environment assumption, must be asserted on the neighbour that owes it; the fairness lesson shows what happens without it. The intended chain proves bounded progress with induction, and the cover run shows traffic flows and a two-cycle stall is exercised:

chain2.sv

// formal: prove 4 expect pass slang top chain2
`define FORMAL
module chain2 #(parameter BUG = 0, parameter FAIR = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  output wire       in_ready,
  input  wire       out_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  reg       v1, v2;       // stage 1 and stage 2 hold a beat
  reg [7:0] d1, d2;
  reg       rdy2;         // stage 2 ready flag used by the BUG 1 variant
  wire      s1_valid, s2_ready;

  assign in_ready  = !v1;
  assign out_valid = v2;
  assign out_data  = d2;

  generate if (BUG == 1) begin : g_bug
    assign s1_valid = v1 && rdy2;
    assign s2_ready = rdy2;
    always @(posedge clk) rdy2 <= !rst && s1_valid && (!v2 || out_ready);
  end else begin : g_ok
    assign s1_valid = v1;
    assign s2_ready = !v2 || out_ready;
    always @(posedge clk) rdy2 <= 1'b0;
  end endgenerate

  wire move = s1_valid && s2_ready;

  always @(posedge clk) begin
    if (rst) begin v1 <= 1'b0; v2 <= 1'b0; end
    else begin
      if (move) v1 <= 1'b0;
      else if (in_valid && in_ready) begin v1 <= 1'b1; d1 <= in_data; end
      if (move) begin v2 <= 1'b1; d2 <= d1; end
      else if (v2 && out_ready) v2 <= 1'b0;
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // stall counter: consecutive cycles in which the downstream holds a beat and is not ready
  reg [1:0] sc;
  always @(posedge clk) begin
    if (rst) sc <= 2'd0;
    else if (v2 && !out_ready && sc != 2'd2) sc <= sc + 2'd1;
    else if (!v2 || out_ready) sc <= 2'd0;
  end
  // environment assumption on the downstream only (never on a design output)
  always @(*) if (!init && FAIR == 0) assume (!(v2 && !out_ready && sc == 2'd2));
  always @(*) if (!init && FAIR == 1) assume (out_ready);

  // bounded progress: cycles since the last delivery while the chain holds a beat
  reg [2:0] age;
  always @(posedge clk) begin
    if (rst) age <= 3'd0;
    else if ((v1 || v2) && !(v2 && out_ready)) age <= age + 3'd1;
    else age <= 3'd0;
  end

  always @(*) if (!init) begin
    p_age:  assert (age <= 3'd3);
    c_flow: cover (v2 && out_ready);
    c_stall_two: cover (v2 && out_ready && sc == 2'd2);
  end
  always @(posedge clk) if (!init && !$past(rst)) begin
    p_hold: assert (!($past(v2) && !$past(out_ready)) || d2 == $past(d2));
  end
`endif
endmodule

chain2.sv

// formal: bmc 20 expect pass slang top chain2
`define FORMAL
module chain2 #(parameter BUG = 0, parameter FAIR = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  output wire       in_ready,
  input  wire       out_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  reg       v1, v2;       // stage 1 and stage 2 hold a beat
  reg [7:0] d1, d2;
  reg       rdy2;         // stage 2 ready flag used by the BUG 1 variant
  wire      s1_valid, s2_ready;

  assign in_ready  = !v1;
  assign out_valid = v2;
  assign out_data  = d2;

  generate if (BUG == 1) begin : g_bug
    assign s1_valid = v1 && rdy2;
    assign s2_ready = rdy2;
    always @(posedge clk) rdy2 <= !rst && s1_valid && (!v2 || out_ready);
  end else begin : g_ok
    assign s1_valid = v1;
    assign s2_ready = !v2 || out_ready;
    always @(posedge clk) rdy2 <= 1'b0;
  end endgenerate

  wire move = s1_valid && s2_ready;

  always @(posedge clk) begin
    if (rst) begin v1 <= 1'b0; v2 <= 1'b0; end
    else begin
      if (move) v1 <= 1'b0;
      else if (in_valid && in_ready) begin v1 <= 1'b1; d1 <= in_data; end
      if (move) begin v2 <= 1'b1; d2 <= d1; end
      else if (v2 && out_ready) v2 <= 1'b0;
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // stall counter: consecutive cycles in which the downstream holds a beat and is not ready
  reg [1:0] sc;
  always @(posedge clk) begin
    if (rst) sc <= 2'd0;
    else if (v2 && !out_ready && sc != 2'd2) sc <= sc + 2'd1;
    else if (!v2 || out_ready) sc <= 2'd0;
  end
  // environment assumption on the downstream only (never on a design output)
  always @(*) if (!init && FAIR == 0) assume (!(v2 && !out_ready && sc == 2'd2));
  always @(*) if (!init && FAIR == 1) assume (out_ready);

  // bounded progress: cycles since the last delivery while the chain holds a beat
  reg [2:0] age;
  always @(posedge clk) begin
    if (rst) age <= 3'd0;
    else if ((v1 || v2) && !(v2 && out_ready)) age <= age + 3'd1;
    else age <= 3'd0;
  end

  always @(*) if (!init) begin
    p_age:  assert (age <= 3'd3);
    c_flow: cover (v2 && out_ready);
    c_stall_two: cover (v2 && out_ready && sc == 2'd2);
  end
  always @(posedge clk) if (!init && !$past(rst)) begin
    p_hold: assert (!($past(v2) && !$past(out_ready)) || d2 == $past(d2));
  end
`endif
endmodule

chain2.sv

// formal: cover 10 expect reached slang top chain2
`define FORMAL
module chain2 #(parameter BUG = 0, parameter FAIR = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  output wire       in_ready,
  input  wire       out_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  reg       v1, v2;       // stage 1 and stage 2 hold a beat
  reg [7:0] d1, d2;
  reg       rdy2;         // stage 2 ready flag used by the BUG 1 variant
  wire      s1_valid, s2_ready;

  assign in_ready  = !v1;
  assign out_valid = v2;
  assign out_data  = d2;

  generate if (BUG == 1) begin : g_bug
    assign s1_valid = v1 && rdy2;
    assign s2_ready = rdy2;
    always @(posedge clk) rdy2 <= !rst && s1_valid && (!v2 || out_ready);
  end else begin : g_ok
    assign s1_valid = v1;
    assign s2_ready = !v2 || out_ready;
    always @(posedge clk) rdy2 <= 1'b0;
  end endgenerate

  wire move = s1_valid && s2_ready;

  always @(posedge clk) begin
    if (rst) begin v1 <= 1'b0; v2 <= 1'b0; end
    else begin
      if (move) v1 <= 1'b0;
      else if (in_valid && in_ready) begin v1 <= 1'b1; d1 <= in_data; end
      if (move) begin v2 <= 1'b1; d2 <= d1; end
      else if (v2 && out_ready) v2 <= 1'b0;
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // stall counter: consecutive cycles in which the downstream holds a beat and is not ready
  reg [1:0] sc;
  always @(posedge clk) begin
    if (rst) sc <= 2'd0;
    else if (v2 && !out_ready && sc != 2'd2) sc <= sc + 2'd1;
    else if (!v2 || out_ready) sc <= 2'd0;
  end
  // environment assumption on the downstream only (never on a design output)
  always @(*) if (!init && FAIR == 0) assume (!(v2 && !out_ready && sc == 2'd2));
  always @(*) if (!init && FAIR == 1) assume (out_ready);

  // bounded progress: cycles since the last delivery while the chain holds a beat
  reg [2:0] age;
  always @(posedge clk) begin
    if (rst) age <= 3'd0;
    else if ((v1 || v2) && !(v2 && out_ready)) age <= age + 3'd1;
    else age <= 3'd0;
  end

  always @(*) if (!init) begin
    p_age:  assert (age <= 3'd3);
    c_flow: cover (v2 && out_ready);
    c_stall_two: cover (v2 && out_ready && sc == 2'd2);
  end
  always @(posedge clk) if (!init && !$past(rst)) begin
    p_hold: assert (!($past(v2) && !$past(out_ready)) || d2 == $past(d2));
  end
`endif
endmodule

The buggy chain never moves the first beat. Read the trace as a parked beat: accepted at step 1, held in stage 1 from step 2, rdy2 low throughout, so s1_valid stays low and rdy2 never rises. The downstream value of out_ready makes no difference, because stage 2 is empty and the stall assumption does not apply. The age climbs one per step and passes the bound at step 6:

Step	in_valid	v1 (stage 1 holds)	age	Outcome
1	1	0	0	beat accepted
2	0	1	0	parked: `s1_valid` waits for `rdy2`
3	0	1	1	still parked
4	0	1	2	still parked
5	0	1	3	at the bound
6	0	1	4	counterexample: `p_age` fails, no delivery within the bound

The bound is one step short at depth 6 and exact at depth 7. A bounded run to 6 passes, a bounded run to 7 finds the stuck state:

chain2.sv

// formal: bmc 6 expect pass slang top chain2 define BUG=1
`define FORMAL
module chain2 #(parameter BUG = 0, parameter FAIR = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  output wire       in_ready,
  input  wire       out_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  reg       v1, v2;       // stage 1 and stage 2 hold a beat
  reg [7:0] d1, d2;
  reg       rdy2;         // stage 2 ready flag used by the BUG 1 variant
  wire      s1_valid, s2_ready;

  assign in_ready  = !v1;
  assign out_valid = v2;
  assign out_data  = d2;

  generate if (BUG == 1) begin : g_bug
    assign s1_valid = v1 && rdy2;
    assign s2_ready = rdy2;
    always @(posedge clk) rdy2 <= !rst && s1_valid && (!v2 || out_ready);
  end else begin : g_ok
    assign s1_valid = v1;
    assign s2_ready = !v2 || out_ready;
    always @(posedge clk) rdy2 <= 1'b0;
  end endgenerate

  wire move = s1_valid && s2_ready;

  always @(posedge clk) begin
    if (rst) begin v1 <= 1'b0; v2 <= 1'b0; end
    else begin
      if (move) v1 <= 1'b0;
      else if (in_valid && in_ready) begin v1 <= 1'b1; d1 <= in_data; end
      if (move) begin v2 <= 1'b1; d2 <= d1; end
      else if (v2 && out_ready) v2 <= 1'b0;
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // stall counter: consecutive cycles in which the downstream holds a beat and is not ready
  reg [1:0] sc;
  always @(posedge clk) begin
    if (rst) sc <= 2'd0;
    else if (v2 && !out_ready && sc != 2'd2) sc <= sc + 2'd1;
    else if (!v2 || out_ready) sc <= 2'd0;
  end
  // environment assumption on the downstream only (never on a design output)
  always @(*) if (!init && FAIR == 0) assume (!(v2 && !out_ready && sc == 2'd2));
  always @(*) if (!init && FAIR == 1) assume (out_ready);

  // bounded progress: cycles since the last delivery while the chain holds a beat
  reg [2:0] age;
  always @(posedge clk) begin
    if (rst) age <= 3'd0;
    else if ((v1 || v2) && !(v2 && out_ready)) age <= age + 3'd1;
    else age <= 3'd0;
  end

  always @(*) if (!init) begin
    p_age:  assert (age <= 3'd3);
    c_flow: cover (v2 && out_ready);
    c_stall_two: cover (v2 && out_ready && sc == 2'd2);
  end
  always @(posedge clk) if (!init && !$past(rst)) begin
    p_hold: assert (!($past(v2) && !$past(out_ready)) || d2 == $past(d2));
  end
`endif
endmodule

chain2.sv

// formal: bmc 7 expect fail slang top chain2 define BUG=1
`define FORMAL
module chain2 #(parameter BUG = 0, parameter FAIR = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire       in_valid,
  input  wire [7:0] in_data,
  output wire       in_ready,
  input  wire       out_ready,
  output wire       out_valid,
  output wire [7:0] out_data
);
  reg       v1, v2;       // stage 1 and stage 2 hold a beat
  reg [7:0] d1, d2;
  reg       rdy2;         // stage 2 ready flag used by the BUG 1 variant
  wire      s1_valid, s2_ready;

  assign in_ready  = !v1;
  assign out_valid = v2;
  assign out_data  = d2;

  generate if (BUG == 1) begin : g_bug
    assign s1_valid = v1 && rdy2;
    assign s2_ready = rdy2;
    always @(posedge clk) rdy2 <= !rst && s1_valid && (!v2 || out_ready);
  end else begin : g_ok
    assign s1_valid = v1;
    assign s2_ready = !v2 || out_ready;
    always @(posedge clk) rdy2 <= 1'b0;
  end endgenerate

  wire move = s1_valid && s2_ready;

  always @(posedge clk) begin
    if (rst) begin v1 <= 1'b0; v2 <= 1'b0; end
    else begin
      if (move) v1 <= 1'b0;
      else if (in_valid && in_ready) begin v1 <= 1'b1; d1 <= in_data; end
      if (move) begin v2 <= 1'b1; d2 <= d1; end
      else if (v2 && out_ready) v2 <= 1'b0;
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  // stall counter: consecutive cycles in which the downstream holds a beat and is not ready
  reg [1:0] sc;
  always @(posedge clk) begin
    if (rst) sc <= 2'd0;
    else if (v2 && !out_ready && sc != 2'd2) sc <= sc + 2'd1;
    else if (!v2 || out_ready) sc <= 2'd0;
  end
  // environment assumption on the downstream only (never on a design output)
  always @(*) if (!init && FAIR == 0) assume (!(v2 && !out_ready && sc == 2'd2));
  always @(*) if (!init && FAIR == 1) assume (out_ready);

  // bounded progress: cycles since the last delivery while the chain holds a beat
  reg [2:0] age;
  always @(posedge clk) begin
    if (rst) age <= 3'd0;
    else if ((v1 || v2) && !(v2 && out_ready)) age <= age + 3'd1;
    else age <= 3'd0;
  end

  always @(*) if (!init) begin
    p_age:  assert (age <= 3'd3);
    c_flow: cover (v2 && out_ready);
    c_stall_two: cover (v2 && out_ready && sc == 2'd2);
  end
  always @(posedge clk) if (!init && !$past(rst)) begin
    p_hold: assert (!($past(v2) && !$past(out_ready)) || d2 == $past(d2));
  end
`endif
endmodule

Root cause: a wait cycle between valid and ready, found structurally before any proof ran. Fix: ready must not wait for valid. The intended chain's stage 2 ready depends only on its own occupancy and the downstream ready.

What the review looks for

The dependency list is complete: every wait relation across the chain, including conditions on registers, not just the forwarding path.
The progress bound is derived from stage depth plus the assumed stall bound, never tuned to the run.
The stuck trace is classified correctly: a parked beat with nothing enabled is deadlock-shaped, not starvation.
The stall assumption constrains the downstream only, and the downstream owner asserts it.

Verify and debug

Run the structural check on every topology change; it is instant and it fails before the temporal proof wastes an hour. A progress failure with a stage that holds a beat and an enabled downstream is a drain bug inside the stage; a failure only when the downstream stalls needs the stall bound revisited, which is the next lesson.

Check yourself The dependency graph has no cycle but the progress proof still fails with the downstream always ready. What now?

The defect is not a wait cycle but a drain bug inside a stage: read the trace for which beat is stuck and which condition fails to release it. A parked beat that waits for a new arrival is an example.

Navigate

Why it matters

The core idea

Worked example: the dependency checker

Worked example: bounded progress proved and stuck

What the review looks for

Verify and debug

Related topics

Progress in a Handshake Chain

Why it matters

The core idea

Worked example: the dependency checker

Worked example: bounded progress proved and stuck

What the review looks for

Verify and debug

Related topics

Why it matters

The core idea

Worked example: the dependency checker

Worked example: bounded progress proved and stuck

What the review looks for

Verify and debug

Related topics

Up next

Why it matters

The core idea

Worked example: the dependency checker

Worked example: bounded progress proved and stuck

What the review looks for

Verify and debug

Related topics

Up next