Case Splitting and Helper Lemmas

On this page

Part 4 of 10, lesson 21 of 23Proof Engines and ConvergenceAll levels

Why it matters

One property that covers several behaviours is several easier proofs glued together: a mode input that selects a computation is easier to prove range by range than all at once. But a split is only sound with its coverage proof: the cases must exhaust the possibilities, or the missing case is an unproven hole wearing a proof's clothes. This lesson splits a property on a 4-bit mode into three cases, proves each, proves the cases cover every mode, and catches the split that forgets one range.

The core idea

A case split replaces prove P with prove P under case 1, prove P under case 2, and so on, plus prove that the cases cover everything. The module below scales a 4-bit mode by 5, and its specification is y equals 5 times m. The cases are three ranges of m: below 4, from 4 to 11, and 12 or more. A planted bug gives the wrong product for the single mode 12, which lies in the third range. Each case is a separate run with the same module text and a different parameter. The coverage lemma says the three predicates together hold for every m, and it is itself a run. Write only the first two cases and both prove, the report counts the property proven, and the bug survives; the coverage lemma of that incomplete split fails, which is how the missing case is caught.

Worked example: three cases, a coverage lemma, a missing case

First the good design: each case proves at depth 1, since the module has no state, and the coverage lemma for the three-case split proves. Then the buggy design, with the incomplete split: the two cases the author wrote prove together, which is the false pass. The third case catches the bug at once, and the coverage lemma of the incomplete split fails with a counterexample in the range that was never written: a mode of 12 or more.

scale5.sv

// formal: prove 1 expect pass slang top scale5 define CASE=0
`define FORMAL
// scale5: a 4-bit mode m selects a scaled output; the specification is y = 5 * m (lesson-local module).
// BUG = 1: the product is wrong for the single mode m = 12.
// CASE picks the obligation of this run: 0, 1 and 2 are the three cases of the split, 3 is the pair of
// cases an incomplete split would contain, 8 is the coverage lemma of that incomplete split, 9 the
// coverage lemma of the full split.
module scale5 #(parameter BUG = 0, parameter CASE = 0) (
  input  wire [3:0] m,
  output wire [7:0] y
);
  assign y = (BUG == 1 && m == 4'd12) ? 8'd0 : ({4'b0, m} << 2) + {4'b0, m};

`ifdef FORMAL
  wire c0 = (m < 4'd4);                      // case 0: small modes
  wire c1 = (m >= 4'd4) && (m < 4'd12);      // case 1: middle modes
  wire c2 = (m >= 4'd12);                    // case 2: large modes
  wire ok = (y == {4'b0, m} * 8'd5);         // the specification
  always @(*) begin
    if (CASE == 0) a_case0: assert (!c0 || ok);
    if (CASE == 1) a_case1: assert (!c1 || ok);
    if (CASE == 2) a_case2: assert (!c2 || ok);
    if (CASE == 3) a_case01: assert ((!c0 || ok) && (!c1 || ok));
    if (CASE == 8) a_cover_two: assert (c0 || c1);
    if (CASE == 9) a_cover_three: assert (c0 || c1 || c2);
  end
`endif
endmodule

scale5.sv

// formal: prove 1 expect pass slang top scale5 define CASE=1
`define FORMAL
// scale5: a 4-bit mode m selects a scaled output; the specification is y = 5 * m (lesson-local module).
// BUG = 1: the product is wrong for the single mode m = 12.
// CASE picks the obligation of this run: 0, 1 and 2 are the three cases of the split, 3 is the pair of
// cases an incomplete split would contain, 8 is the coverage lemma of that incomplete split, 9 the
// coverage lemma of the full split.
module scale5 #(parameter BUG = 0, parameter CASE = 0) (
  input  wire [3:0] m,
  output wire [7:0] y
);
  assign y = (BUG == 1 && m == 4'd12) ? 8'd0 : ({4'b0, m} << 2) + {4'b0, m};

`ifdef FORMAL
  wire c0 = (m < 4'd4);                      // case 0: small modes
  wire c1 = (m >= 4'd4) && (m < 4'd12);      // case 1: middle modes
  wire c2 = (m >= 4'd12);                    // case 2: large modes
  wire ok = (y == {4'b0, m} * 8'd5);         // the specification
  always @(*) begin
    if (CASE == 0) a_case0: assert (!c0 || ok);
    if (CASE == 1) a_case1: assert (!c1 || ok);
    if (CASE == 2) a_case2: assert (!c2 || ok);
    if (CASE == 3) a_case01: assert ((!c0 || ok) && (!c1 || ok));
    if (CASE == 8) a_cover_two: assert (c0 || c1);
    if (CASE == 9) a_cover_three: assert (c0 || c1 || c2);
  end
`endif
endmodule

scale5.sv

// formal: prove 1 expect pass slang top scale5 define CASE=2
`define FORMAL
// scale5: a 4-bit mode m selects a scaled output; the specification is y = 5 * m (lesson-local module).
// BUG = 1: the product is wrong for the single mode m = 12.
// CASE picks the obligation of this run: 0, 1 and 2 are the three cases of the split, 3 is the pair of
// cases an incomplete split would contain, 8 is the coverage lemma of that incomplete split, 9 the
// coverage lemma of the full split.
module scale5 #(parameter BUG = 0, parameter CASE = 0) (
  input  wire [3:0] m,
  output wire [7:0] y
);
  assign y = (BUG == 1 && m == 4'd12) ? 8'd0 : ({4'b0, m} << 2) + {4'b0, m};

`ifdef FORMAL
  wire c0 = (m < 4'd4);                      // case 0: small modes
  wire c1 = (m >= 4'd4) && (m < 4'd12);      // case 1: middle modes
  wire c2 = (m >= 4'd12);                    // case 2: large modes
  wire ok = (y == {4'b0, m} * 8'd5);         // the specification
  always @(*) begin
    if (CASE == 0) a_case0: assert (!c0 || ok);
    if (CASE == 1) a_case1: assert (!c1 || ok);
    if (CASE == 2) a_case2: assert (!c2 || ok);
    if (CASE == 3) a_case01: assert ((!c0 || ok) && (!c1 || ok));
    if (CASE == 8) a_cover_two: assert (c0 || c1);
    if (CASE == 9) a_cover_three: assert (c0 || c1 || c2);
  end
`endif
endmodule

scale5.sv

// formal: prove 1 expect pass slang top scale5 define CASE=9
`define FORMAL
// scale5: a 4-bit mode m selects a scaled output; the specification is y = 5 * m (lesson-local module).
// BUG = 1: the product is wrong for the single mode m = 12.
// CASE picks the obligation of this run: 0, 1 and 2 are the three cases of the split, 3 is the pair of
// cases an incomplete split would contain, 8 is the coverage lemma of that incomplete split, 9 the
// coverage lemma of the full split.
module scale5 #(parameter BUG = 0, parameter CASE = 0) (
  input  wire [3:0] m,
  output wire [7:0] y
);
  assign y = (BUG == 1 && m == 4'd12) ? 8'd0 : ({4'b0, m} << 2) + {4'b0, m};

`ifdef FORMAL
  wire c0 = (m < 4'd4);                      // case 0: small modes
  wire c1 = (m >= 4'd4) && (m < 4'd12);      // case 1: middle modes
  wire c2 = (m >= 4'd12);                    // case 2: large modes
  wire ok = (y == {4'b0, m} * 8'd5);         // the specification
  always @(*) begin
    if (CASE == 0) a_case0: assert (!c0 || ok);
    if (CASE == 1) a_case1: assert (!c1 || ok);
    if (CASE == 2) a_case2: assert (!c2 || ok);
    if (CASE == 3) a_case01: assert ((!c0 || ok) && (!c1 || ok));
    if (CASE == 8) a_cover_two: assert (c0 || c1);
    if (CASE == 9) a_cover_three: assert (c0 || c1 || c2);
  end
`endif
endmodule

Good design: all three cases prove, and so does the coverage lemma of the full split. Together these are a proof of the whole property for every mode.

scale5.sv

// formal: prove 1 expect pass slang top scale5 define BUG=1 define CASE=3
`define FORMAL
// scale5: a 4-bit mode m selects a scaled output; the specification is y = 5 * m (lesson-local module).
// BUG = 1: the product is wrong for the single mode m = 12.
// CASE picks the obligation of this run: 0, 1 and 2 are the three cases of the split, 3 is the pair of
// cases an incomplete split would contain, 8 is the coverage lemma of that incomplete split, 9 the
// coverage lemma of the full split.
module scale5 #(parameter BUG = 0, parameter CASE = 0) (
  input  wire [3:0] m,
  output wire [7:0] y
);
  assign y = (BUG == 1 && m == 4'd12) ? 8'd0 : ({4'b0, m} << 2) + {4'b0, m};

`ifdef FORMAL
  wire c0 = (m < 4'd4);                      // case 0: small modes
  wire c1 = (m >= 4'd4) && (m < 4'd12);      // case 1: middle modes
  wire c2 = (m >= 4'd12);                    // case 2: large modes
  wire ok = (y == {4'b0, m} * 8'd5);         // the specification
  always @(*) begin
    if (CASE == 0) a_case0: assert (!c0 || ok);
    if (CASE == 1) a_case1: assert (!c1 || ok);
    if (CASE == 2) a_case2: assert (!c2 || ok);
    if (CASE == 3) a_case01: assert ((!c0 || ok) && (!c1 || ok));
    if (CASE == 8) a_cover_two: assert (c0 || c1);
    if (CASE == 9) a_cover_three: assert (c0 || c1 || c2);
  end
`endif
endmodule

The false pass: with the bug planted, the two cases written down, below 4 and from 4 to 11, both hold, because the faulty mode lies outside both.

scale5.sv

// formal: bmc 1 expect fail slang top scale5 define BUG=1 define CASE=2
`define FORMAL
// scale5: a 4-bit mode m selects a scaled output; the specification is y = 5 * m (lesson-local module).
// BUG = 1: the product is wrong for the single mode m = 12.
// CASE picks the obligation of this run: 0, 1 and 2 are the three cases of the split, 3 is the pair of
// cases an incomplete split would contain, 8 is the coverage lemma of that incomplete split, 9 the
// coverage lemma of the full split.
module scale5 #(parameter BUG = 0, parameter CASE = 0) (
  input  wire [3:0] m,
  output wire [7:0] y
);
  assign y = (BUG == 1 && m == 4'd12) ? 8'd0 : ({4'b0, m} << 2) + {4'b0, m};

`ifdef FORMAL
  wire c0 = (m < 4'd4);                      // case 0: small modes
  wire c1 = (m >= 4'd4) && (m < 4'd12);      // case 1: middle modes
  wire c2 = (m >= 4'd12);                    // case 2: large modes
  wire ok = (y == {4'b0, m} * 8'd5);         // the specification
  always @(*) begin
    if (CASE == 0) a_case0: assert (!c0 || ok);
    if (CASE == 1) a_case1: assert (!c1 || ok);
    if (CASE == 2) a_case2: assert (!c2 || ok);
    if (CASE == 3) a_case01: assert ((!c0 || ok) && (!c1 || ok));
    if (CASE == 8) a_cover_two: assert (c0 || c1);
    if (CASE == 9) a_cover_three: assert (c0 || c1 || c2);
  end
`endif
endmodule

The third case, written, finds it at once: mode 12 gives the wrong product.

scale5.sv

// formal: bmc 1 expect fail slang top scale5 define CASE=8
`define FORMAL
// scale5: a 4-bit mode m selects a scaled output; the specification is y = 5 * m (lesson-local module).
// BUG = 1: the product is wrong for the single mode m = 12.
// CASE picks the obligation of this run: 0, 1 and 2 are the three cases of the split, 3 is the pair of
// cases an incomplete split would contain, 8 is the coverage lemma of that incomplete split, 9 the
// coverage lemma of the full split.
module scale5 #(parameter BUG = 0, parameter CASE = 0) (
  input  wire [3:0] m,
  output wire [7:0] y
);
  assign y = (BUG == 1 && m == 4'd12) ? 8'd0 : ({4'b0, m} << 2) + {4'b0, m};

`ifdef FORMAL
  wire c0 = (m < 4'd4);                      // case 0: small modes
  wire c1 = (m >= 4'd4) && (m < 4'd12);      // case 1: middle modes
  wire c2 = (m >= 4'd12);                    // case 2: large modes
  wire ok = (y == {4'b0, m} * 8'd5);         // the specification
  always @(*) begin
    if (CASE == 0) a_case0: assert (!c0 || ok);
    if (CASE == 1) a_case1: assert (!c1 || ok);
    if (CASE == 2) a_case2: assert (!c2 || ok);
    if (CASE == 3) a_case01: assert ((!c0 || ok) && (!c1 || ok));
    if (CASE == 8) a_cover_two: assert (c0 || c1);
    if (CASE == 9) a_cover_three: assert (c0 || c1 || c2);
  end
`endif
endmodule

And the coverage lemma of the incomplete split fails on its own, on the good design, with a counterexample in the modes no case contains: the lemma checks the structure of the proof, not the design.

Run	Design	Obligation	Result
Case 0, case 1, case 2	Good	Property in each range	Each proven
Coverage, three cases	Good	The ranges cover every mode	Proven
Cases 0 and 1 together	Bug at mode 12	Property in the two ranges written	Proven: the false pass
Case 2	Bug at mode 12	Property in the range never written	Counterexample: the bug
Coverage, two cases	Either	The two ranges cover every mode	Counterexample: modes 12 and above uncovered

example.py

def c0(m):
    return m < 4

def c1(m):
    return 4 <= m < 12

def c2(m):
    return m >= 12

def uncovered(cases):
    return {m for m in range(16) if not any(c(m) for c in cases)}

assert uncovered([c0, c1, c2]) == set()                     # the three-case split covers every mode
gap = uncovered([c0, c1])                                  # the incomplete split
assert gap == {12, 13, 14, 15}, gap
assert 12 in gap                                           # exactly where the planted bug hides

# the same enumeration, applied to a split that overlaps: not a gap, but worth knowing
def overlapping(cases):
    return {m for m in range(16) if sum(c(m) for c in cases) > 1}
assert overlapping([c0, c1, c2]) == set()

# injected data: a split whose middle case stops one mode early leaves mode 11 uncovered
def c1_short(m):
    return 4 <= m < 11
assert uncovered([c0, c1_short, c2]) == {11}
caught = False
try:
    assert uncovered([c0, c1_short, c2]) == set()
except AssertionError:
    caught = True
assert caught, "coverage check missed the gap at mode 11"
print("PASS: three cases cover all 16 modes; two cases leave 12..15; an off-by-one gap at 11 is caught")

What the review looks for

Every split files its coverage proof next to the case proofs, with the uncovered set shown empty.
Cases are disjoint or the overlap is proven consistent, never accidentally overlapping.
Each case is tried against a mutant in its own range: a case no mutant exercises is a candidate for removal.

Verify and debug

Check a split by deleting one case at a time and rerunning the coverage proof: each deletion must fail loudly. If a deletion still passes, the coverage proof is weaker than the split and must be rewritten before the split is trusted. Write the coverage lemma from the same predicates as the cases, never from a second description.

Check yourself Your three-case split proves, but deleting the middle case still passes coverage. What is wrong?

The coverage proof does not actually enumerate the ranges: it passes without the middle case, so it cannot catch a missing case. Rewrite coverage from the case predicates themselves, then confirm each deletion fails.

Navigate

Why it matters

The core idea

Worked example: three cases, a coverage lemma, a missing case

What the review looks for

Verify and debug

Related topics

Case Splitting and Helper Lemmas

Why it matters

The core idea

Worked example: three cases, a coverage lemma, a missing case

What the review looks for

Verify and debug

Related topics

Why it matters

The core idea

Worked example: three cases, a coverage lemma, a missing case

What the review looks for

Verify and debug

Related topics

Up next

Why it matters

The core idea

Worked example: three cases, a coverage lemma, a missing case

What the review looks for

Verify and debug

Related topics

Up next