Assume-Guarantee

A property that spans several blocks pulls all of them into its cone. Assume-guarantee reasoning splits it: each block is checked on its own, assuming what its neighbors promise and proving what it promises in return. If every promise that is assumed somewhere is proven somewhere else, the separate checks together cover the whole design. This article splits the source-and-sink example into two checks, and shows how the split forces the interface contract to be complete.

9 min read | Intermediate

What You'll Learn

• Explain assume-guarantee reasoning and when the split is sound
• Write the guarantees of a block as assertions and the same rules as assumptions on its neighbor
• Find a gap in an interface contract from a false failure
• Check a two-block design as two independent, smaller runs

The Idea

Block A guarantees some rules on its outputs; block B assumes those rules on its inputs. Check A with its guarantees as assertions. Check B with them as assumptions, plus B's own properties. If both checks pass, B's properties hold in the combined design, because the inputs B really receives satisfy the rules A was proven to keep.

The two checks are smaller than one combined check, and each block can be changed and rechecked without the other. That is how formal scales to subsystems: not with one huge run, but with many small ones connected by contracts.

Two conditions keep the method sound. Every assumption of one block must be proven as an assertion of the block that drives those signals. And the reasoning must not be circular: A's guarantees must not depend on assuming B's guarantees, which in turn depend on A's.

The Example: Source and Sink

The debugging article checked a source that sends 1, 2, 3 and so on, and a sink that adds them up, with one end-to-end property: after n words, the sum is n(n+1)/2. Here the two blocks are checked separately.

The Source and Its Guarantees

module src (input clk, input rst, input ready, output reg valid, output reg [7:0] data);
  always @(posedge clk)
    if (rst) begin
      valid <= 1'b0; data <= 8'd1;
    end else begin
      valid <= 1'b1;
      if (valid && ready) data <= data + 8'd1;
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // GUARANTEES of the source, proven here
  always @(posedge clk) if (!init && !$past(rst) && $past(valid) && !$past(ready)) assert (valid && data == $past(data));
  always @(posedge clk) if (!init && !$past(rst) && $past(valid && ready)) assert (data == $past(data) + 8'd1);
  always @(posedge clk) if (!init && !$past(rst) && !$past(valid && ready)) assert (data == $past(data));
  always @(posedge clk) if (!init && !$past(rst) && valid && !$past(valid)) assert (data == 8'd1);
`endif
endmodule

The guarantees: valid is held while waiting, the data goes up by one after each handshake, the data does not change without a handshake, and the first word is 1. The check uses the source alone, with ready free.

The Sink and Its Assumptions

The sink check turns the same four rules into assumptions on valid and data, and asserts the sum:

`ifdef FORMAL
  // ... reset ...
  // ASSUMPTIONS: what the source guarantees
  always @(posedge clk) if (!init && !$past(rst) && $past(valid) && !$past(ready)) assume (valid && data == $past(data));
  always @(posedge clk) if (!init && !$past(rst) && $past(valid && ready)) assume (data == $past(data) + 8'd1);
  always @(posedge clk) if (!init && !$past(rst) && !$past(valid && ready)) assume (data == $past(data));
  always @(*) if (!init && n == 8'd0 && valid) assume (data == 8'd1);
  // the sink's own property
  always @(posedge clk) if (!init) assert (sum == ({8'd0, n} * ({8'd0, n} + 16'd1)) / 16'd2);
`endif

Both checks pass on the lab engine. Together they prove the end-to-end property, without ever putting both blocks in one run.

The Contract Must Be Complete

The first version of this split left out the third rule, "the data does not change without a handshake". The source check passed, but the sink check failed at step 5. In the trace, valid drops for a cycle and the data jumps from 2 to 66 while it is low. The real source never does that, but nothing in the assumptions forbade it, because the rules only talked about cycles with valid high.

That false failure was useful: it showed a gap in the interface contract. Adding the missing rule as a guarantee of the source, proven there, and as an assumption of the sink closed it. Writing contracts precisely enough for assume-guarantee is one of the main benefits of the method, because the same contract documents the interface for everyone who uses it.

Catching a Bug in the Source

Put back the bug from the debugging article: the source advances its data on valid alone. The source check fails at step 4 on its guarantees: data changes while waiting. The sink check is unaffected, because it relies only on the contract. The bug is found in the block where it lives, with a short trace, which is the second benefit of the method.

Running It in ChipVerify Lab

The example contains the source with its guarantees, and a second file with the sink and its assumptions. Each module is checked on its own: set the top module to src and run, then to sink and run.

Common Mistakes