Circular Assume-Guarantee and the False Pass

On this page

Part 3 of 10, lesson 14 of 19Property Development and ConstraintsAll levels

Why it matters

Block A is proved on the assumption that B's output is good. Block B is proved on the assumption that A's output is good. Both proofs pass. The system holds a bad flag that circulates for ever. Job of this lesson: run the circle, see it pass falsely, and repair it by assuming the guarantee only up to the previous cycle.

The core idea

Each block copies the other's output into a flag one cycle later. In the faulty version nothing clears a flag at reset. Proved alone, block A with the assumption "the other flag is always low" keeps its own flag low from step 1, so the proof passes. The same two blocks in a ring start with arbitrary flags, swap them for ever, and fail the claim "both low" at step 1. The circle has no base case.

Top-down diagram: after reset both flags are arbitrary; block A copies B's flag and B copies A's, with an arrow from B back to A. From B a second arrow leads to a high flag that circulates for ever, and from that a repair box: assume the other flag was low in the previous cycle, or reset has just happened.

Each block's proof assumes the other's flag is good, so neither proof checks the start. A flag that is high after reset is copied round the ring for ever. The repair assumes the guarantee only in the previous cycle and asserts it now, so the first cycle after reset is checked.

The repair is induction on time. Assume the other block's output was good in the previous cycle (and make the assumption vacuous right after a reset cycle), and assert it now. The reset term matters: written without it the assumption silently removes the reset gap.

Worked example

MODE=0 is the same-cycle assumption, MODE=1 the time-indexed one, FIX=1 the reset that clears the flag. The first run is the false pass, the second the failing ring:

blk.sv

// formal: prove 4 expect pass slang top unit define FIX=0 define MODE=0
`define FORMAL
module blk #(parameter FIX = 0) (input wire clk, input wire rst, input wire other, output reg f);
  always @(posedge clk) begin
    if (FIX == 1 && rst) f <= 1'b0; else f <= other;
  end
endmodule
module unit #(parameter FIX = 0, parameter MODE = 0) (input wire clk, input wire rst, input wire other);
  wire f; blk #(.FIX(FIX)) u (.clk(clk), .rst(rst), .other(other), .f(f));
  reg init = 1'b1; reg pother = 1'b0, prst = 1'b1; always @(posedge clk) begin init <= 1'b0; pother <= other; prst <= rst; end
  always @(*) if (init) assume (rst);
  generate if (MODE == 0) begin : g0
    always @(*) assume (!other);
  end else begin : g1
    always @(*) if (!init) assume (!pother || prst);
  end endgenerate
  always @(*) if (!init) a_good: assert (!f);
endmodule
module ring #(parameter FIX = 0) (input wire clk, input wire rst);
  wire fa, fb;
  blk #(.FIX(FIX)) ua (.clk(clk), .rst(rst), .other(fb), .f(fa));
  blk #(.FIX(FIX)) ub (.clk(clk), .rst(rst), .other(fa), .f(fb));
  reg init = 1'b1; always @(posedge clk) init <= 1'b0; always @(*) if (init) assume (rst);
  always @(*) if (!init) a_good: assert (!fa && !fb);
endmodule

blk.sv

// formal: bmc 4 expect fail slang top ring define FIX=0
`define FORMAL
module blk #(parameter FIX = 0) (input wire clk, input wire rst, input wire other, output reg f);
  always @(posedge clk) begin
    if (FIX == 1 && rst) f <= 1'b0; else f <= other;
  end
endmodule
module unit #(parameter FIX = 0, parameter MODE = 0) (input wire clk, input wire rst, input wire other);
  wire f; blk #(.FIX(FIX)) u (.clk(clk), .rst(rst), .other(other), .f(f));
  reg init = 1'b1; reg pother = 1'b0, prst = 1'b1; always @(posedge clk) begin init <= 1'b0; pother <= other; prst <= rst; end
  always @(*) if (init) assume (rst);
  generate if (MODE == 0) begin : g0
    always @(*) assume (!other);
  end else begin : g1
    always @(*) if (!init) assume (!pother || prst);
  end endgenerate
  always @(*) if (!init) a_good: assert (!f);
endmodule
module ring #(parameter FIX = 0) (input wire clk, input wire rst);
  wire fa, fb;
  blk #(.FIX(FIX)) ua (.clk(clk), .rst(rst), .other(fb), .f(fa));
  blk #(.FIX(FIX)) ub (.clk(clk), .rst(rst), .other(fa), .f(fb));
  reg init = 1'b1; always @(posedge clk) init <= 1'b0; always @(*) if (init) assume (rst);
  always @(*) if (!init) a_good: assert (!fa && !fb);
endmodule

The time-indexed assumption exposes the flaw at once: the unit proof now fails at step 1, because the flag has no value of its own after reset. With the reset fix, both the unit and the ring prove:

blk.sv

// formal: bmc 4 expect fail slang top unit define FIX=0 define MODE=1
`define FORMAL
module blk #(parameter FIX = 0) (input wire clk, input wire rst, input wire other, output reg f);
  always @(posedge clk) begin
    if (FIX == 1 && rst) f <= 1'b0; else f <= other;
  end
endmodule
module unit #(parameter FIX = 0, parameter MODE = 0) (input wire clk, input wire rst, input wire other);
  wire f; blk #(.FIX(FIX)) u (.clk(clk), .rst(rst), .other(other), .f(f));
  reg init = 1'b1; reg pother = 1'b0, prst = 1'b1; always @(posedge clk) begin init <= 1'b0; pother <= other; prst <= rst; end
  always @(*) if (init) assume (rst);
  generate if (MODE == 0) begin : g0
    always @(*) assume (!other);
  end else begin : g1
    always @(*) if (!init) assume (!pother || prst);
  end endgenerate
  always @(*) if (!init) a_good: assert (!f);
endmodule
module ring #(parameter FIX = 0) (input wire clk, input wire rst);
  wire fa, fb;
  blk #(.FIX(FIX)) ua (.clk(clk), .rst(rst), .other(fb), .f(fa));
  blk #(.FIX(FIX)) ub (.clk(clk), .rst(rst), .other(fa), .f(fb));
  reg init = 1'b1; always @(posedge clk) init <= 1'b0; always @(*) if (init) assume (rst);
  always @(*) if (!init) a_good: assert (!fa && !fb);
endmodule

blk.sv

// formal: prove 4 expect pass slang top unit define FIX=1 define MODE=1
`define FORMAL
module blk #(parameter FIX = 0) (input wire clk, input wire rst, input wire other, output reg f);
  always @(posedge clk) begin
    if (FIX == 1 && rst) f <= 1'b0; else f <= other;
  end
endmodule
module unit #(parameter FIX = 0, parameter MODE = 0) (input wire clk, input wire rst, input wire other);
  wire f; blk #(.FIX(FIX)) u (.clk(clk), .rst(rst), .other(other), .f(f));
  reg init = 1'b1; reg pother = 1'b0, prst = 1'b1; always @(posedge clk) begin init <= 1'b0; pother <= other; prst <= rst; end
  always @(*) if (init) assume (rst);
  generate if (MODE == 0) begin : g0
    always @(*) assume (!other);
  end else begin : g1
    always @(*) if (!init) assume (!pother || prst);
  end endgenerate
  always @(*) if (!init) a_good: assert (!f);
endmodule
module ring #(parameter FIX = 0) (input wire clk, input wire rst);
  wire fa, fb;
  blk #(.FIX(FIX)) ua (.clk(clk), .rst(rst), .other(fb), .f(fa));
  blk #(.FIX(FIX)) ub (.clk(clk), .rst(rst), .other(fa), .f(fb));
  reg init = 1'b1; always @(posedge clk) init <= 1'b0; always @(*) if (init) assume (rst);
  always @(*) if (!init) a_good: assert (!fa && !fb);
endmodule

blk.sv

// formal: prove 4 expect pass slang top ring define FIX=1
`define FORMAL
module blk #(parameter FIX = 0) (input wire clk, input wire rst, input wire other, output reg f);
  always @(posedge clk) begin
    if (FIX == 1 && rst) f <= 1'b0; else f <= other;
  end
endmodule
module unit #(parameter FIX = 0, parameter MODE = 0) (input wire clk, input wire rst, input wire other);
  wire f; blk #(.FIX(FIX)) u (.clk(clk), .rst(rst), .other(other), .f(f));
  reg init = 1'b1; reg pother = 1'b0, prst = 1'b1; always @(posedge clk) begin init <= 1'b0; pother <= other; prst <= rst; end
  always @(*) if (init) assume (rst);
  generate if (MODE == 0) begin : g0
    always @(*) assume (!other);
  end else begin : g1
    always @(*) if (!init) assume (!pother || prst);
  end endgenerate
  always @(*) if (!init) a_good: assert (!f);
endmodule
module ring #(parameter FIX = 0) (input wire clk, input wire rst);
  wire fa, fb;
  blk #(.FIX(FIX)) ua (.clk(clk), .rst(rst), .other(fb), .f(fa));
  blk #(.FIX(FIX)) ub (.clk(clk), .rst(rst), .other(fa), .f(fb));
  reg init = 1'b1; always @(posedge clk) init <= 1'b0; always @(*) if (init) assume (rst);
  always @(*) if (!init) a_good: assert (!fa && !fb);
endmodule

Run	Result	Reading
Unit, same-cycle assumption, no reset fix	Proven	False pass: the assumption supplies the base case
Ring, no reset fix	Fails at step 1	The circle proves nothing
Unit, time-indexed, no reset fix	Fails at step 1	No base case: the flag has no reset value
Unit and ring, time-indexed, reset fix	Proven	Base case from reset, step from the previous cycle

example.py

from itertools import product
# One flag per block. A flag copies the other block's output; with the fix a reset clears it.
def nxt(other, rst, fix):
    return 0 if (fix and rst) else other

def unit_ok(mode, fix, n=5):
    # block alone: 'other' is a free input; step 0 is a reset; f must be 0 from step 1
    for f0, other, later in product((0, 1), product((0, 1), repeat=n), product((0, 1), repeat=n - 1)):
        rst = (1,) + later
        if mode == 0 and any(other): continue                                # assume (!other) in every step
        if mode == 1 and any(other[t - 1] and not rst[t - 1] for t in range(1, n)): continue   # assume (!pother || prst)
        f = f0
        for t in range(n):
            if t >= 1 and f != 0: return False
            f = nxt(other[t], rst[t], fix)
    return True

def ring_ok(fix, n=5):
    for fa, fb, later in product((0, 1), (0, 1), product((0, 1), repeat=n - 1)):
        rst = (1,) + later
        for t in range(n):
            if t >= 1 and (fa or fb): return False
            fa, fb = nxt(fb, rst[t], fix), nxt(fa, rst[t], fix)
    return True

assert unit_ok(0, 0) is True and ring_ok(0) is False        # the circle: the unit passes, the ring fails
assert unit_ok(1, 0) is False                                # time-indexed assumption: no base case, caught
assert unit_ok(1, 1) is True and ring_ok(1) is True          # reset fix: both prove
print("PASS: same-cycle circle passes falsely; time-indexed assumption exposes it; the reset fix proves unit and ring")

What a reviewer looks for

Every assume-guarantee pair is drawn; a pair that points both ways is rejected or carries an induction-on-time argument.
A guarantee assumed about a neighbour is time-indexed: previous cycle in the assumption, current cycle in the assertion, vacuous after reset.
The two-direction test: delete one assumption at a time. If a proof that should depend on the other is unchanged in both directions, there is no real dependence; if each needs the other, there is a circle.

Verify and debug

Draw each assumption and the assertion that discharges it; a pair of arrows in both directions is the circle. Then run the ring with no assumptions between the blocks: here it fails within depth 4 while the units prove alone under the same-cycle assumption, which means the units lean on each other. Next make the assumption time-indexed and rerun the unit: it fails at step 1, because the flag has no value of its own after reset. That failure is the missing base case showing itself; the reset fix removes it and both the unit and the ring prove.

Check yourself Why does the time-indexed assumption need the || prst term?

Right after a reset cycle the previous output is not constrained by anything. Without the term the assumption removes that cycle and the base case disappears.

Navigate

Why it matters

The core idea

Worked example

What a reviewer looks for

Verify and debug

Related topics

Circular Assume-Guarantee and the False Pass

Why it matters

The core idea

Worked example

What a reviewer looks for

Verify and debug

Related topics

Why it matters

The core idea

Worked example

What a reviewer looks for

Verify and debug

Related topics

Up next

Why it matters

The core idea

Worked example

What a reviewer looks for

Verify and debug

Related topics

Up next