Why it matters

Two datapaths agree whenever the mode input is 0 and disagree on the odd nibbles when it is 1, where mode 1 is a debug path that bypasses the rounding. The unconstrained miter fails, correctly. The team constrains the miter to mode 0 and it passes. Both results are true and only one of them is the signoff statement. This lesson teaches how to state the weaker claim without letting it hide the missing mode.

This lesson has one job: show that a constrained proof passes exactly where the constraint holds, and that every other mode still owes a proof.

The core idea

Constrained equivalence assumes a condition on the inputs, for example mode tied to one value, and proves the outputs agree under it. The result is conditional: it says nothing about the excluded inputs. The report must therefore list every constraint alongside the verdict, and every excluded mode needs its own proof or its own documented owner.

Constants and don't-cares belong to the same discipline. A constant tied differently on the two sides is a setup difference, not a design difference, and must be aligned before comparison. A don't-care output may legally differ: the two implementations chose different values for an unspecified case, and the proof must exclude exactly those outputs rather than loosen the whole comparison.

Worked example: equal in mode 0 only

Two 4-bit datapaths share an input nibble and a mode bit. In mode 0 both round the nibble down to an even value. In mode 1 the reference still rounds but the revised block passes the nibble through. The script enumerates all 32 combinations: unconstrained comparison finds the eight mode-1 mismatches, the mode-0-constrained comparison is clean, and a second run with the mode-1 constraint correctly reports disagreement. An injected variant that also differs in mode 0 is caught by the constrained check, proving the check can fail:

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

import itertools

def ref(nib, mode):
    return nib & 0xE

def dut(nib, mode):
    return nib if mode == 1 else nib & 0xE

def dut_bug(nib, mode):
    return nib if mode == 1 else (nib & 0xE) ^ 0x2

def mismatches(fn1, fn2, modes):
    bad = []
    for nib in range(16):
        for mode in modes:
            if fn1(nib, mode) != fn2(nib, mode):
                bad.append((nib, mode))
    return bad

free = mismatches(ref, dut, [0, 1])
constrained = mismatches(ref, dut, [0])
other_mode = mismatches(ref, dut, [1])
assert len(free) == 8 and all(m == 1 for _, m in free)
assert constrained == []
assert len(other_mode) == 8
hidden = mismatches(ref, dut_bug, [0])
assert len(hidden) == 16
print("PASS: 8 mode-1 mismatches; mode-0 clean; hidden mode-0 bug caught")

The signoff statement for this block therefore reads: equivalent in mode 0 over all 16 nibbles; mode 1 intentionally different and covered by its own debug-path check. Either half alone would be a false claim.

The same pair runs as a miter below, so the statement is a proof and not an enumeration. The file holds one miter with three cases chosen by a parameter: case 0 leaves the mode input free, case 1 assumes mode 0 and compares, case 2 assumes mode 1 and checks the revised block against its own specification of the debug path (the nibble passes straight through). The miter has no design state, so one checked step presents every input assignment and each result below is complete, 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

// formal: prove 3 expect fail slang top mode_eq define CASE=0
`define FORMAL
module rnd_ref (
  input  wire [3:0] nib,
  input  wire       mode,
  output wire [3:0] out
);
  assign out = nib & 4'b1110;
endmodule
module rnd_dut (
  input  wire [3:0] nib,
  input  wire       mode,
  output wire [3:0] out
);
  assign out = mode ? nib : (nib & 4'b1110);
endmodule
module mode_eq #(parameter CASE = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] nib,
  input  wire       mode,
  output wire       same
);
  wire [3:0] o_ref, o_dut;
  rnd_ref u_r (.nib(nib), .mode(mode), .out(o_ref));
  rnd_dut u_d (.nib(nib), .mode(mode), .out(o_dut));
  assign same = (o_ref == o_dut);
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (CASE == 1) assume (mode == 1'b0);
  always @(*) if (CASE == 2) assume (mode == 1'b1);
  always @(*) if (!init && CASE != 2) a_equiv: assert (same);
  always @(*) if (!init && CASE == 2) a_debug_path: assert (o_dut == nib);
`endif
endmodule

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

// formal: prove 3 expect pass slang top mode_eq define CASE=1
`define FORMAL
module rnd_ref (
  input  wire [3:0] nib,
  input  wire       mode,
  output wire [3:0] out
);
  assign out = nib & 4'b1110;
endmodule
module rnd_dut (
  input  wire [3:0] nib,
  input  wire       mode,
  output wire [3:0] out
);
  assign out = mode ? nib : (nib & 4'b1110);
endmodule
module mode_eq #(parameter CASE = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] nib,
  input  wire       mode,
  output wire       same
);
  wire [3:0] o_ref, o_dut;
  rnd_ref u_r (.nib(nib), .mode(mode), .out(o_ref));
  rnd_dut u_d (.nib(nib), .mode(mode), .out(o_dut));
  assign same = (o_ref == o_dut);
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (CASE == 1) assume (mode == 1'b0);
  always @(*) if (CASE == 2) assume (mode == 1'b1);
  always @(*) if (!init && CASE != 2) a_equiv: assert (same);
  always @(*) if (!init && CASE == 2) a_debug_path: assert (o_dut == nib);
`endif
endmodule

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

// formal: prove 3 expect pass slang top mode_eq define CASE=2
`define FORMAL
module rnd_ref (
  input  wire [3:0] nib,
  input  wire       mode,
  output wire [3:0] out
);
  assign out = nib & 4'b1110;
endmodule
module rnd_dut (
  input  wire [3:0] nib,
  input  wire       mode,
  output wire [3:0] out
);
  assign out = mode ? nib : (nib & 4'b1110);
endmodule
module mode_eq #(parameter CASE = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [3:0] nib,
  input  wire       mode,
  output wire       same
);
  wire [3:0] o_ref, o_dut;
  rnd_ref u_r (.nib(nib), .mode(mode), .out(o_ref));
  rnd_dut u_d (.nib(nib), .mode(mode), .out(o_dut));
  assign same = (o_ref == o_dut);
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (CASE == 1) assume (mode == 1'b0);
  always @(*) if (CASE == 2) assume (mode == 1'b1);
  always @(*) if (!init && CASE != 2) a_equiv: assert (same);
  always @(*) if (!init && CASE == 2) a_debug_path: assert (o_dut == nib);
`endif
endmodule

Case 0 fails with a mode-1 counterexample: an odd nibble with mode 1, where the reference rounds the low bit away and the revised block keeps it. Case 1 is proven under the stated constraint, and it would stay proven if the revised block were broken in mode 1, which is exactly why case 2 exists: the excluded mode owes its own proof. The signoff statement therefore lists three rows (unconstrained: fails; mode 0: equivalent; mode 1: intentionally different, debug path proven against its own specification).

Don't-cares: one default, two legal readings

A decoder specifies codes 0 to 3 and leaves codes 4 to 7 unspecified. Two implementations choose different values for the unspecified codes: the reference drives 00 in its default branch and the revised block drives 11. Both are legal. An unconstrained miter fails on code 4, which is a real difference that the specification allows. The right response is to exclude exactly the unspecified codes from the comparison, not to loosen the miter. The mutation shows the exclusion does not hide a real bug: the revised decoder with a wrong answer for code 2 still fails with the don't-care exclusion in place.

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

// formal: prove 3 expect fail slang top dc_eq define MASK=0 define BUG=0
`define FORMAL
module dec_ref (
  input  wire [2:0] code,
  output reg  [1:0] y
);
  always @(*) case (code)
    3'd0: y = 2'b00;
    3'd1: y = 2'b01;
    3'd2: y = 2'b10;
    3'd3: y = 2'b11;
    default: y = 2'b00;
  endcase
endmodule
module dec_alt #(parameter BUG = 0) (
  input  wire [2:0] code,
  output reg  [1:0] y
);
  always @(*) case (code)
    3'd0: y = 2'b00;
    3'd1: y = 2'b01;
    3'd2: y = (BUG == 1) ? 2'b11 : 2'b10;
    3'd3: y = 2'b11;
    default: y = 2'b11;
  endcase
endmodule
module dc_eq #(parameter MASK = 0, parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [2:0] code,
  output wire       same
);
  wire [1:0] y1, y2;
  dec_ref u_r (.code(code), .y(y1));
  dec_alt #(.BUG(BUG)) u_a (.code(code), .y(y2));
  wire specified = !code[2];
  assign same = (y1 == y2);
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_equiv: assert ((MASK == 1) ? (!specified || same) : same);
`endif
endmodule

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

// formal: prove 3 expect pass slang top dc_eq define MASK=1 define BUG=0
`define FORMAL
module dec_ref (
  input  wire [2:0] code,
  output reg  [1:0] y
);
  always @(*) case (code)
    3'd0: y = 2'b00;
    3'd1: y = 2'b01;
    3'd2: y = 2'b10;
    3'd3: y = 2'b11;
    default: y = 2'b00;
  endcase
endmodule
module dec_alt #(parameter BUG = 0) (
  input  wire [2:0] code,
  output reg  [1:0] y
);
  always @(*) case (code)
    3'd0: y = 2'b00;
    3'd1: y = 2'b01;
    3'd2: y = (BUG == 1) ? 2'b11 : 2'b10;
    3'd3: y = 2'b11;
    default: y = 2'b11;
  endcase
endmodule
module dc_eq #(parameter MASK = 0, parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [2:0] code,
  output wire       same
);
  wire [1:0] y1, y2;
  dec_ref u_r (.code(code), .y(y1));
  dec_alt #(.BUG(BUG)) u_a (.code(code), .y(y2));
  wire specified = !code[2];
  assign same = (y1 == y2);
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_equiv: assert ((MASK == 1) ? (!specified || same) : same);
`endif
endmodule

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

// formal: prove 3 expect fail slang top dc_eq define MASK=1 define BUG=1
`define FORMAL
module dec_ref (
  input  wire [2:0] code,
  output reg  [1:0] y
);
  always @(*) case (code)
    3'd0: y = 2'b00;
    3'd1: y = 2'b01;
    3'd2: y = 2'b10;
    3'd3: y = 2'b11;
    default: y = 2'b00;
  endcase
endmodule
module dec_alt #(parameter BUG = 0) (
  input  wire [2:0] code,
  output reg  [1:0] y
);
  always @(*) case (code)
    3'd0: y = 2'b00;
    3'd1: y = 2'b01;
    3'd2: y = (BUG == 1) ? 2'b11 : 2'b10;
    3'd3: y = 2'b11;
    default: y = 2'b11;
  endcase
endmodule
module dc_eq #(parameter MASK = 0, parameter BUG = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [2:0] code,
  output wire       same
);
  wire [1:0] y1, y2;
  dec_ref u_r (.code(code), .y(y1));
  dec_alt #(.BUG(BUG)) u_a (.code(code), .y(y2));
  wire specified = !code[2];
  assign same = (y1 == y2);
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_equiv: assert ((MASK == 1) ? (!specified || same) : same);
`endif
endmodule

One caution belongs to the two-state model. The formal flow here has no unknown value: if the source wrote an unknown in the default branch, the formal model would treat it as an arbitrary 0 or 1, and simulation would show an x. Two-state equivalence can therefore show that two defined readings differ, and can exclude them by a stated condition, but it cannot show what an unknown would do downstream. That question is answered by a reset-determinism proof and a separate X-aware analysis, not by the miter.

1
2
3
4
5

// not-run: an unknown value is not modelled by the two-state formal flow
// reading A (reference): unspecified codes are a defined value
//   default: y = 2'b00;
// reading B (revised): unspecified codes are an explicit don't-care
//   default: y = 2'bx;   // simulation shows x; the formal model treats it as any 0 or 1

What the review looks for

• Every constraint appears next to the verdict: which inputs are tied, which modes are excluded, which outputs are don't-care.

• Each excluded mode has its own row: a proof, a separate check, or a named owner and a reason.

• Don't-care exclusions name exact outputs and exact conditions, never a blanket loosening.

Verify and debug

Re-run the miter once per mode with the constraint flipped, and confirm each run fails or passes as the table predicts. A mode that was never run is the classic escape: enumerate the mode values from the specification, not from the proof script. For don't-cares, mutate one excluded output and confirm the verdict does not change, then mutate one included output and confirm it fails.

Related topics

• SAT Sweeping and Structural Hashing

• Next: Reading a Failing Miter

• Synthesis: Constants and Don't-Cares