Case Splitting and Assume-Guarantee

Split a proof into cases that finish, show that the cases cover everything, avoid the split that hides interleavings, and compose two blocks without circular logic.

Lesson: F4.3
Time: 25 min
Runs on: SymbiYosys
Check: 6 questions

Three proofs, one per burst type, all passed. In silicon an INCR burst right after a WRAP crossed a 4 KB page, because the INCR reused the WRAP’s beat size. Each proof had restricted the whole run to one burst type, so no proof ever saw one type follow another.

Split by Burst Type

One Proof Becomes ThreeThe assertion is proved once per burst type. The three cases together are every legal burst, because the request never carries burst type 3.

Read the diagram as text

every legal burst: FIXED, INCR or WRAP, any order
case FIXED: busy && burst_q == FIXED |-> in page
case INCR: busy && burst_q == INCR |-> in page
case WRAP: busy && burst_q == WRAP |-> in page
union: the three conditions cover every busy cycle

every legal burst → case FIXED
every legal burst → case INCR
every legal burst → case WRAP
case FIXED → union
case INCR → union
case WRAP → union

Soft split: the case is the assertion’s condition, so each run still allows any sequence of bursts.

Proof (`abc pdr` unless noted)	len 4 bits (16 beats)	len 8 bits (256 beats)
all types together	Prove PASS, 6.0 s	time limit (20 s), no verdict
case FIXED	Prove PASS, 0.6 s	Prove PASS, 0.6 s
case INCR	Prove PASS, 0.8 s	time limit (20 s), no verdict
case INCR, one helper, `smtbmc yices` prove 2	–	Prove PASS, 0.5 s
case WRAP	Prove PASS, 5.7 s	Prove PASS, 10.1 s

The property: every beat stays in the 4 KB page of its start address. WRAP lengths are 2, 4, 8 or 16 beats in both columns.

With 16-beat bursts the split costs about what the whole proof costs. With AXI4’s 256-beat INCR the whole proof runs out of time, and the split shows where: FIXED and WRAP finish, INCR does not. The hard case is now small enough to think about.

One helper for INCR, "the beats still to come fit below the page end", closes it at depth 2 (F4.6 shows how to find such helpers). The three cases together are every busy cycle, since the master never sends burst type 3.

The INCR helper, asserted (so it is proven too). Without it, k-induction at depth 8 is still UNKNOWN.

wire [15:0] f_off = {4'd0, addr[11:0]} & ~(step - 16'd1);
wire [16:0] f_end = {1'b0, f_off} + {1'b0, step} * ({9'd0, left} + 17'd1);
always @(posedge clk) if (!rst && busy && burst_q == INCR) assert(f_end <= 17'd4096);

Soft Split and Hard Split

Soft split: the case is a condition

if (!rst && busy && burst_q == INCR)
  assert(addr[15:12] == page[15:12]);

Faulty design: FAIL at step 7, 0.6 s (bmc 20).

Hard split: the inputs are restricted

if (!busy && start) restrict(burst == INCR);

Faulty design: Prove PASS, 0.8 s (abc pdr).

Faulty design: INCR keeps an old beat size	Measured result
hard split, FIXED only, `abc pdr`	Prove PASS, 0.6 s
hard split, INCR only, `abc pdr`	Prove PASS, 0.8 s
hard split, WRAP only, `abc pdr`	Prove PASS, 5.3 s
soft split, case INCR, `bmc` 20	FAIL at step 7, 0.6 s
no split, `bmc` 20	FAIL at step 7, 0.6 s

Three hard-split passes on a design with a real bug.

A soft split keeps every input sequence; only the assertion narrows. A hard split restricts the inputs themselves: here, every burst of the run has one type. That deletes every interleaving, and the faulty design passes all three runs.

Measured counterexample of the faulty design with no split (bmc, depth 20): FAIL at step 7, 0.6 s.

The escape is a WRAP followed by an INCR. A split proves the whole only under two conditions. The cases are exhaustive, and the case variable is fixed for the run, like a strap or a configuration written once. restrict is the IEEE statement for such constraints; simulation ignores it.

Faulty design, burst type a static configuration (`$anyconst`)	Measured result (`abc pdr`)
split: `restrict(f_cfg == FIXED)`	Prove PASS, 0.6 s
split: `restrict(f_cfg == INCR)`	Prove PASS, 0.7 s
split: `restrict(f_cfg == WRAP)`	Prove PASS, 4.7 s
no split	Prove PASS, 4.3 s

With the type fixed for the run, the three slices are exhaustive and sound, and they agree with the unsplit run.

Here the same faulty RTL is correct, because a WRAP can never be followed by an INCR. Whether a hard split is sound is a fact about the environment: write it as an assumption and cite the specification row that justifies it.

Assume-Guarantee

Two Blocks, Two Guarantees, CrossedThe sender spends credits; the receiver returns one per freed slot. Each block is proved alone, assuming the other block’s guarantee on its inputs.

Read the diagram as text

snd: two credits; sends only with a credit
rcv: two buffer slots; registered credit return
G_A: no send while two words are outstanding
G_B: no credit while nothing is outstanding
out_cnt: interface monitor: sends minus credits

snd → rcv: send
rcv → snd: ret
G_A → rcv: assumed by
G_B → snd: assumed by
out_cnt → G_A
out_cnt → G_B

G_A is proved on snd under G_B; G_B is proved on rcv under G_A.

Run (`abc pdr`)	Correct receiver	Faulty receiver
snd alone, G_B assumed	Prove PASS, 0.5 s	not involved
rcv alone, G_A assumed	Prove PASS, 0.5 s	FAIL at step 3, 0.6 s
both, nothing assumed	Prove PASS, 0.5 s	FAIL at step 3, 0.6 s
both, G_A and G_B assumed and asserted in one run	Prove PASS, 0.5 s	Prove PASS, 0.5 s
both, G_A and G_B assumed one cycle late	Prove PASS, 0.5 s	FAIL at step 3, 0.6 s

The faulty receiver returns a credit when asked to pop an empty buffer.

Each block is proved alone, with the other block’s guarantee assumed on its inputs. It looks circular: G_A needs G_B and G_B needs G_A. It is sound here because ret is a register, so G_B at cycle t uses G_A only up to t − 1. Neither guarantee can be the first to break.

The trap is the shortcut of one run that assumes both guarantees in the same cycle it asserts them. The faulty receiver passes, because the assumption deletes the cycle where it breaks. Assuming them one cycle late restores the induction over time, and the bug is found again.

Asked in Interviews

Question	Answer
What is case splitting?	Proving a property once per case of the inputs or modes, so each run has a smaller cone. Prove that the cases cover everything, prefer the soft split, and use a hard split only on values that cannot change during a run.
What is assume-guarantee reasoning?	Proving each block alone, assuming its neighbours’ guarantees on its inputs, then composing. Each guarantee must be proved somewhere.
When is it circular?	When a guarantee at cycle t needs the other guarantee at the same cycle t, for example through a combinational path, or when both are assumed and asserted in one run. A one-cycle delay on every dependency makes the argument an induction over time.

Try It

The lab is the INCR case of the soft split, 16-beat lengths, abc pdr. Measured: Prove PASS, 0.8 s.

The rule in concurrent SVA. Each case adds its condition to the antecedent.

assert property (@(posedge clk) disable iff (rst)
  busy |-> addr[15:12] == page[15:12]);

Write the other cases
Change the case condition to FIXED, then WRAP, and record the three times.
Hard split the faulty design
Capture size_q only on WRAP bursts (the faulty line), drop the case condition, and add restrict(burst == INCR); under if (!busy && start). Run, then remove the restrict and run bmc at depth 20.
Read the escape
In the bmc trace, find the burst types of the two starts before the failure.

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module agen(input clk, rst, start, input [15:0] a, input [1:0] size, input [3:0] len,
  input [1:0] burst, output reg busy = 0, output reg [15:0] addr = 0);
  localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2;
  reg [1:0] size_q = 0, burst_q = 0;
  reg [3:0] left = 0, len_q = 0;
  reg [15:0] lo = 0, page = 0;
  wire [15:0] step = 16'd1 << size_q;
  wire [15:0] total = step * ({12'd0, len_q} + 16'd1);
  wire [15:0] nxt = (addr & ~(step - 16'd1)) + step;
  always @(posedge clk)
    if (rst) begin busy <= 0; left <= 0; end
    else if (!busy) begin
      if (start) begin
        busy <= 1; addr <= a; size_q <= size;
        burst_q <= burst; left <= len; len_q <= len; page <= a;
        lo <= a & ~((16'd1 << size) * ({12'd0, len} + 16'd1) - 16'd1);
      end
    end else begin
      if (left == 0) busy <= 0; else left <= left - 1'b1;
      case (burst_q)
        FIXED: addr <= addr;
        WRAP: addr <= (nxt == lo + total) ? lo : nxt;
        default: addr <= nxt;
      endcase
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // the master obeys the AXI burst rules
  always @(*) if (!busy && start) begin
    assume(burst != 2'd3);
    assume(burst != INCR || {4'd0, a[11:0]} + (16'd1 << size) * ({12'd0, len} + 16'd1) <= 16'd4096);
    if (burst == WRAP) assume((len == 1 || len == 3 || len == 7 || len == 15) && (a & ((16'd1 << size) - 16'd1)) == 0);
  end
  always @(posedge clk) if (!rst && busy && burst_q == INCR) assert(addr[15:12] == page[15:12]);
endmodule

Check Yourself

Predict the outputThe faulty address generator with restrict(burst == INCR) on every request, mode prove, abc pdr, reset assumed in step 0. The verdict is:

module agen(input clk, rst, start, input [15:0] a, input [1:0] size, input [3:0] len,
  input [1:0] burst, output reg busy = 0, output reg [15:0] addr = 0);
  localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2;
  reg [1:0] size_q = 0, burst_q = 0;
  reg [3:0] left = 0, len_q = 0;
  reg [15:0] lo = 0, page = 0;
  wire [15:0] step = 16'd1 << size_q;
  wire [15:0] total = step * ({12'd0, len_q} + 16'd1);
  wire [15:0] nxt = (addr & ~(step - 16'd1)) + step;
  always @(posedge clk)
    if (rst) begin busy <= 0; left <= 0; end
    else if (!busy) begin
      if (start) begin
        busy <= 1; addr <= a; if (burst == WRAP) size_q <= size;   /* bug: INCR keeps an old size */
        burst_q <= burst; left <= len; len_q <= len; page <= a;
        lo <= a & ~((16'd1 << size) * ({12'd0, len} + 16'd1) - 16'd1);
      end
    end else begin
      if (left == 0) busy <= 0; else left <= left - 1'b1;
      case (burst_q)
        FIXED: addr <= addr;
        WRAP: addr <= (nxt == lo + total) ? lo : nxt;
        default: addr <= nxt;
      endcase
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // the master obeys the AXI burst rules
  always @(*) if (!busy && start) begin
    assume(burst != 2'd3);
    assume(burst != INCR || {4'd0, a[11:0]} + (16'd1 << size) * ({12'd0, len} + 16'd1) <= 16'd4096);
    if (burst == WRAP) assume((len == 1 || len == 3 || len == 7 || len == 15) && (a & ((16'd1 << size) - 16'd1)) == 0);
    restrict(burst == INCR);            // hard split
  end
  always @(posedge clk) if (!rst && busy) assert(addr[15:12] == page[15:12]);
endmodule

Predict the outputThe faulty receiver composed with the sender, both guarantees assumed and asserted in the same run, mode prove, abc pdr, reset assumed in step 0. The verdict is:

module snd(input clk, rst, want, ret, output send);
  reg [1:0] cred = 2'd2;
  assign send = want && cred != 2'd0;
  always @(posedge clk) if (rst) cred <= 2'd2; else cred <= cred - send + ret;
endmodule
module rcv(input clk, rst, send, drain, output reg ret = 0);
  reg [1:0] fill = 2'd0;
  wire pop = drain;                      // bug: pops an empty buffer
  always @(posedge clk)
    if (rst) begin fill <= 0; ret <= 0; end
    else begin fill <= fill + send - pop; ret <= pop; end
endmodule
module link(input clk, rst, want, drain);
  wire send, ret;
  snd a(.clk(clk), .rst(rst), .want(want), .ret(ret), .send(send));
  rcv b(.clk(clk), .rst(rst), .send(send), .drain(drain), .ret(ret));
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg [2:0] out_cnt = 3'd0;   // words sent minus credits returned
  reg ok_q = 1'b1;
  always @(posedge clk) begin
    out_cnt <= rst ? 3'd0 : out_cnt + send - ret;
    ok_q <= rst || (!(send && out_cnt == 3'd2) && !(ret && out_cnt == 3'd0));
  end
  always @(posedge clk) if (!rst) begin
    assume(!(send && out_cnt == 3'd2));
    assume(!(ret && out_cnt == 3'd0));
    assert(!(send && out_cnt == 3'd2));
    assert(!(ret && out_cnt == 3'd0));
  end
endmodule

Predict the outputThe same faulty pair, with both guarantees assumed only for the previous cycle (assume(ok_q)), mode prove, abc pdr. The verdict is:

module snd(input clk, rst, want, ret, output send);
  reg [1:0] cred = 2'd2;
  assign send = want && cred != 2'd0;
  always @(posedge clk) if (rst) cred <= 2'd2; else cred <= cred - send + ret;
endmodule
module rcv(input clk, rst, send, drain, output reg ret = 0);
  reg [1:0] fill = 2'd0;
  wire pop = drain;                      // bug: pops an empty buffer
  always @(posedge clk)
    if (rst) begin fill <= 0; ret <= 0; end
    else begin fill <= fill + send - pop; ret <= pop; end
endmodule
module link(input clk, rst, want, drain);
  wire send, ret;
  snd a(.clk(clk), .rst(rst), .want(want), .ret(ret), .send(send));
  rcv b(.clk(clk), .rst(rst), .send(send), .drain(drain), .ret(ret));
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg [2:0] out_cnt = 3'd0;   // words sent minus credits returned
  reg ok_q = 1'b1;
  always @(posedge clk) begin
    out_cnt <= rst ? 3'd0 : out_cnt + send - ret;
    ok_q <= rst || (!(send && out_cnt == 3'd2) && !(ret && out_cnt == 3'd0));
  end
  always @(posedge clk) if (!rst) begin
    assume(ok_q);     // both held in the previous cycle
    assert(!(send && out_cnt == 3'd2));
    assert(!(ret && out_cnt == 3'd0));
  end
endmodule

ConceptWhich case split is unsound?

A split on an $anyconst tag that the solver fixes once at step 0A FIFO proof split on push = 0 or 1, restricted for the whole runA split on a configuration register written once before the block is usedA split on a parameter, fixed when the design is elaborated

ConceptWhich check makes a case split a proof of the whole?

Running the three cases on separate machines at the same timeA cover that reaches each of the three cases at least onceA proof that the OR of the case conditions always holdsA larger depth or time limit in the hardest of the three cases

Read the waveformWhich burst types start before the failure in the measured trace?

Measured counterexample of the faulty design with no split (bmc, depth 20): FAIL at step 7, 0.6 s.

Only INCR burstsA FIXED, then a WRAPOnly WRAP burstsA WRAP, then an INCR

Remember

A case split shrinks each run’s cone and shows which case is hard.
Prove that the cases cover everything.
Soft split keeps every input sequence; a hard split hides interleavings unless the case variable is fixed for the run.
Assume-guarantee is sound when each guarantee depends on the other only through earlier cycles.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.