Why it matters

A carry-lookahead adder replaces a ripple-carry adder to close timing. The netlist changes in hundreds of gates and every simulation vector still matches. The question on the review table is simple: do they agree on all 512 input combinations, including the carry corner nobody simulated? The miter answers exactly that, and its counterexample names the corner when they disagree.

This lesson has one job: show that equivalence of two combinational blocks is a safety property on a miter, and prove it both ways.

The core idea

A miter drives both implementations from the same primary inputs, XORs each pair of outputs, and ORs the results into one wire. The property asserts that wire is never 1. If it is proven, the blocks agree on every input. If it fails, the trace is one input assignment plus both outputs: the smallest possible disagreement, directly simulatable.

In textbook form the property is one line: the outputs are equal whenever the block is out of reset. Because the open front end rejects implication operators, the runnable form below states the same check as a Boolean comparison guarded by the reset history:

1
2
3
4
5

// not-run: implication operators are not accepted by this front end
// property p_equiv;
//   @(posedge clk) disable iff (rst) (a_out == b_out);
// endproperty
// assert property (p_equiv);

The runnable equivalent checks the same cycle with a Boolean comparison: same is combinational equality of the two sums, asserted once the reset cycle has passed. One cycle, one comparison, no sequences.

Worked example: ripple-carry against carry-lookahead

Two 4-bit adders sit in one miter with a shared 9-bit input (two nibbles and a carry in, 512 combinations). The reference is ripple-carry. The challenger computes group generates and propagates directly. The good pair is proven. The miter holds no design state, so a single checked step already presents every input assignment to the comparator, and the depth of 3 only skips the reset step: this is a complete result, not a bound.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

// formal: prove 3 expect pass slang top adder_miter
`define FORMAL
module ripple4 (
  input  wire [3:0] a, b,
  input  wire       cin,
  output wire [4:0] sum
);
  wire [4:0] c;
  assign c[0] = cin;
  genvar i;
  generate for (i = 0; i < 4; i = i + 1) begin : gb
    assign sum[i] = a[i] ^ b[i] ^ c[i];
    assign c[i+1] = (a[i] & b[i]) | (a[i] & c[i]) | (b[i] & c[i]);
  end endgenerate
  assign sum[4] = c[4];
endmodule
module lookahead4 #(parameter BUG = 0) (
  input  wire [3:0] a, b,
  input  wire       cin,
  output wire [4:0] sum
);
  wire [3:0] g = a & b;
  wire [3:0] p = a ^ b;
  wire [4:0] c;
  assign c[0] = cin;
  assign c[1] = g[0] | (p[0] & c[0]);
  assign c[2] = g[1] | (p[1] & g[0]) | (p[1] & p[0] & c[0]);
  assign c[3] = g[2] | (p[2] & g[1]) | (p[2] & p[1] & g[0]) |
                (p[2] & p[1] & p[0] & c[0]);
  assign c[4] = g[3] | (p[3] & g[2]) | (p[3] & p[2] & g[1]) |
                (p[3] & p[2] & p[1] & g[0]) |
                ((BUG == 1) ? 1'b0 : (p[3] & p[2] & p[1] & p[0] & c[0]));
  wire [3:0] s = p ^ c[3:0];
  assign sum = {c[4], s};
endmodule
module adder_miter #(parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] a, b,
  input  wire       cin,
  output wire       same
);
  wire [4:0] s_ref, s_dut;
  ripple4 u_ref (.a(a), .b(b), .cin(cin), .sum(s_ref));
  lookahead4 #(.BUG(BUG)) u_dut (.a(a), .b(b), .cin(cin), .sum(s_dut));
  assign same = (s_ref == s_dut);
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_equiv: assert (same);
`endif
endmodule

The injected bug drops the longest carry term: the carry out of bit 3 ignores a carry-in that propagates through all four bits. The mismatch needs every propagate true, every generate false and carry in high, which means a and b bitwise complementary with cin set: 16 assignments (any a, with b its complement). The failing run reports one of them, for example a 0101, b 1010, cin 1. Working it by hand: every propagate is 1 and no generate is 1, so the carries into bits 1 to 3 are still 1 and the low four sum bits are 1111 xor 1111 = 0000, while the carry out is now 0. The buggy lookahead answers 00000 (0) where the ripple answers 10000 (16), and only bit 4 differs:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

// formal: bmc 3 expect fail slang top adder_miter define BUG=1
`define FORMAL
module ripple4 (
  input  wire [3:0] a, b,
  input  wire       cin,
  output wire [4:0] sum
);
  wire [4:0] c;
  assign c[0] = cin;
  genvar i;
  generate for (i = 0; i < 4; i = i + 1) begin : gb
    assign sum[i] = a[i] ^ b[i] ^ c[i];
    assign c[i+1] = (a[i] & b[i]) | (a[i] & c[i]) | (b[i] & c[i]);
  end endgenerate
  assign sum[4] = c[4];
endmodule
module lookahead4 #(parameter BUG = 0) (
  input  wire [3:0] a, b,
  input  wire       cin,
  output wire [4:0] sum
);
  wire [3:0] g = a & b;
  wire [3:0] p = a ^ b;
  wire [4:0] c;
  assign c[0] = cin;
  assign c[1] = g[0] | (p[0] & c[0]);
  assign c[2] = g[1] | (p[1] & g[0]) | (p[1] & p[0] & c[0]);
  assign c[3] = g[2] | (p[2] & g[1]) | (p[2] & p[1] & g[0]) |
                (p[2] & p[1] & p[0] & c[0]);
  assign c[4] = g[3] | (p[3] & g[2]) | (p[3] & p[2] & g[1]) |
                (p[3] & p[2] & p[1] & g[0]) |
                ((BUG == 1) ? 1'b0 : (p[3] & p[2] & p[1] & p[0] & c[0]));
  wire [3:0] s = p ^ c[3:0];
  assign sum = {c[4], s};
endmodule
module adder_miter #(parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] a, b,
  input  wire       cin,
  output wire       same
);
  wire [4:0] s_ref, s_dut;
  ripple4 u_ref (.a(a), .b(b), .cin(cin), .sum(s_ref));
  lookahead4 #(.BUG(BUG)) u_dut (.a(a), .b(b), .cin(cin), .sum(s_dut));
  assign same = (s_ref == s_dut);
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_equiv: assert (same);
`endif
endmodule

# not-run: illustrative trace, not executable here
inputs:  a = 0101, b = 1010, cin = 1   (every bit propagates, none generates)
ripple:  carries 1,1,1,1 -> low bits 0000, c4 = 1  -> sum 10000 (16)
buggy:   c4 term p3&p2&p1&p0&cin dropped -> c4 = 0, low bits still 0000 -> sum 00000 (0)
broken bit: 4 (the carry out) | root cause: missing product term | fix: restore it

The script below repeats the comparison over all 512 input combinations in Python: the good lookahead agrees everywhere, the buggy one disagrees on exactly the 16 complementary assignments with carry in set, and the check is able to fail because the buggy variant is run through the same comparison:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

def lookahead(a, b, cin, bug):
    g = [((a >> i) & (b >> i)) & 1 for i in range(4)]
    p = [((a ^ b) >> i) & 1 for i in range(4)]
    c1 = g[0] | (p[0] & cin)
    c2 = g[1] | (p[1] & g[0]) | (p[1] & p[0] & cin)
    c3 = g[2] | (p[2] & g[1]) | (p[2] & p[1] & g[0]) | (p[2] & p[1] & p[0] & cin)
    c4 = g[3] | (p[3] & g[2]) | (p[3] & p[2] & g[1]) | (p[3] & p[2] & p[1] & g[0])
    if not bug:
        c4 |= p[3] & p[2] & p[1] & p[0] & cin
    c = [cin, c1, c2, c3]
    s = sum((p[i] ^ c[i]) << i for i in range(4))
    return (c4 << 4) | s

def mismatches(bug):
    return [(a, b, cin) for a in range(16) for b in range(16) for cin in (0, 1)
            if lookahead(a, b, cin, bug) != a + b + cin]

assert mismatches(False) == []
bad = mismatches(True)
assert len(bad) == 16
assert all((a ^ b) == 15 and cin == 1 for a, b, cin in bad)
assert lookahead(0b0101, 0b1010, 1, True) == 0
assert 0b0101 + 0b1010 + 1 == 16
print("PASS: 512 agree on the good adder; the bug differs on exactly 16 assignments")

How to read it: the sums are shown in hexadecimal, so 10 is binary 10000, sixteen. At step 0 the operands are 0101 and 1010 with cin low: both sums read f (01111) and same is high. At step 1 only cin changes to high: s_ref reads 10 (10000) and s_dut reads 0 (00000), diff reads 10, so only bit 4 differs, and same is low. At step 2 the operands change to 0011 and 1100 with cin low: both sums read f again. At step 3 cin goes high: the same pair of sums, 10 against 0, appears, and same is low. The assignment at step 3 is the one the proof run reported; the one at step 1 is the lesson's worked example.

What the review looks for

• The miter shares every input wire, including reset and mode selects: no copy driven separately.

• The comparator covers every output bit; the property asserts the OR of all XORs, not a sampled subset.

• A passing result names the bound, or the induction that completed it; a bounded pass says bounded to N.

Verify and debug

Replay the counterexample inputs in simulation on both blocks and confirm the same two sums. Then mutate the reference deliberately and confirm the miter fails: a miter that passes on a mutated reference is not comparing what you think. Check the cone report covers both cones; a silently empty cone proves in seconds and means nothing.

Related topics

• Next: SAT Sweeping and Structural Hashing

• Synthesis: Combinational Equivalence (flow)

• Formal glossary