Two kinds of don't-care

An external, or controllability, don't-care is an input combination the environment never produces, such as a one-hot bus with no all-zero code. (A satisfiability don't-care in the strict sense is an internal node condition that no input assignment can produce; the unreachable bus code is the external form of the same idea.) An observability don't-care is a combination nobody reads, such as an ALU flag during a move. Both let the optimiser pick whichever value gives the smaller cover, but both are claims about the outside world that need a specification source. A claim without a source is a guess, and the break-it section shows what a wrong guess costs.

The example on a map

Take a 3-input function with ON-set {110, 111} and don't-care set {100, 101}. Without the don't-cares the two ON minterms merge into ab. Treating the don't-cares as 1 doubles the group to all four cells where a is 1, and the term widens to the single literal a.

What the tool does with x

In Yosys the don't-care spelling is x: a casex item assigning 1'bx says either value is acceptable there. The script below writes the example function three times: all-zero-default, the don't-care rows answered 1 (the resolved cover y = a as a case statement), and the bare don't-care style assigning x on those rows. All three go through proc, opt and ABC.

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
54
55
56
57
58
59
60
61
62
63
64

read_verilog <<EOV
module nodefault(input wire a, input wire b, input wire c, output wire y);
assign y = (a & b & c) | (a & b & ~c);
endmodule
module withone(input wire a, input wire b, input wire c, output wire y);
reg yo;
always @* begin
casex ({a, b, c})
3'b11?: yo = 1'b1;
3'b10?: yo = 1'b1;
default: yo = 1'b0;
endcase
end
assign y = yo;
endmodule
module withx(input wire a, input wire b, input wire c, output wire y);
reg yo;
always @* begin
casex ({a, b, c})
3'b11?: yo = 1'b1;
3'b10?: yo = 1'bx;
default: yo = 1'b0;
endcase
end
assign y = yo;
endmodule
EOV
design -save raw
hierarchy -check -top nodefault
proc
opt
check
write_json net_plain_opt.json
select -assert-count 3 t:$and
select -assert-count 1 t:$or
techmap
tee -o abc_plain.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_plain.txt stat -liberty course.lib
write_json net_plain.json
select -assert-none t:$and t:$or t:$mux t:$pmux
design -load raw
hierarchy -check -top withone
proc
opt
check
write_json net_one_opt.json
techmap
tee -o abc_one.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_one.txt stat -liberty course.lib
write_json net_one.json
select -assert-none t:$and t:$or t:$mux t:$pmux
design -load raw
hierarchy -check -top withx
proc
opt
check
write_json net_x_opt.json
techmap
tee -o abc_x.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_x.txt stat -liberty course.lib
write_json net_x.json
select -assert-none t:$and t:$or t:$mux t:$pmux
check
log PASS: default-zero and resolved forms map apart while bare x maps like default-zero

The default-zero form cannot widen: every minterm it answers 1 is an ON minterm, while answering 1 on the don't-care rows widens the cover to the single literal a. The bare-x form maps exactly like the default-zero form: the Yosys abc pass replaces the undef bits with constant zero bits before ABC itself starts, as its recorded log line says, so the offer never reaches the cover.

recorded abc pass note on the bare-x form
Replacing 1 occurrences of constant undef bits with constant zero bits

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

read_verilog <<EOV
module withx(input wire a, input wire b, input wire c, output wire y);
reg yo;
always @* begin
casex ({a, b, c})
3'b11?: yo = 1'b1;
3'b10?: yo = 1'bx;
default: yo = 1'b0;
endcase
end
assign y = yo;
endmodule
EOV
hierarchy -check -top withx
proc
opt -mux_undef
check
write_json net_xu_opt.json
select -assert-none t:$pmux t:$mux
techmap
tee -o abc_xu.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_xu.txt stat -liberty course.lib
write_json net_xu.json
select -assert-none t:$and t:$or t:$mux t:$pmux
check
log PASS: asking for undef-aware folding still resolves x to zero

The switch that asks for undef-aware folding is opt -mux_undef: it drops the x branch, which then falls to the default. The default here is 0, so the generic netlist holds 1 comparator cell and the mapped cover stays 1 x AND2 at area 3, exactly the default-zero cover. With a different default the same switch resolves differently. Yosys never passes don't-cares to ABC; only resolving the entries by hand moves the mapped result.

The 5-against-3 generic gap between the default-zero and bare-x rows is bit-level against word-level representation: AND, OR and NOT cells versus comparators plus a multiplexer. It is not a saving, because both rows map to the same cover.

One caution: casex also treats x in the selector as a wildcard, so an unknown selector can match an unintended item. Here x appears only in the assigned value, never in a live selector, which is the narrow safe use.

Proof: the minimised form on the care set

A plain equivalence check would be the wrong proof here: the minimised form y = a answers 1 at 100 and 101 where the default-zero form answers 0, by design. The right claim is narrower: equal on every cared input.

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

read_verilog <<EOV
module gold(input wire a, input wire b, input wire c, output wire y);
assign y = (a & b & c) | (a & b & ~c);
endmodule
module gate(input wire a, input wire b, input wire c, output wire y);
assign y = a;
endmodule
module m(input wire a, input wire b, input wire c, output wire trigger);
wire yg, yo;
gold g(.a(a), .b(b), .c(c), .y(yg));
gate o(.a(a), .b(b), .c(c), .y(yo));
wire care = ~(a & ~b);
assign trigger = (yg ^ yo) & care;
endmodule
EOV
hierarchy -check
proc
opt
hierarchy -top m
flatten
sat -prove trigger 0 -verify m
log PASS: minimized form matches the spec on every cared input

The checker module fires its trigger only where the outputs differ AND the input is cared about, with care = ~(a & ~b) masking exactly the two don't-care minterms. The solver proves the trigger can never fire: 6 of the 8 input combinations, with the remaining two your promise.

Break it: lie about the care set

Now write the lie into the mask itself: claim 010 never arrives either, excluding it alongside 100 and 101. The minimiser answers 1 there. The variant below runs the identical proof under the lying mask, and it passes: the mask is the one input the solver never checks.

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

read_verilog <<EOV
module gold(input wire a, input wire b, input wire c, output wire y);
assign y = (a & b & c) | (a & b & ~c);
endmodule
module gate_bad(input wire a, input wire b, input wire c, output wire y);
assign y = a | (b & ~c);
endmodule
module m(input wire a, input wire b, input wire c, output wire trigger);
wire yg, yo;
gold g(.a(a), .b(b), .c(c), .y(yg));
gate_bad o(.a(a), .b(b), .c(c), .y(yo));
wire care = ~(a & ~b) & (a | ~b | c);
assign trigger = (yg ^ yo) & care;
endmodule
EOV
hierarchy -check
proc
opt
hierarchy -top m
flatten
sat -prove trigger 0 -verify m
log PASS: proof under the lying mask passes while input 010 differs in service

That PASS says nothing about 010. In service the environment still produces 010, and the circuit answers 1 where the specification answers 0. Under the honest mask the same implementation is refuted, and the recorded model below names 010.

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

read_verilog <<EOV
module gold(input wire a, input wire b, input wire c, output wire y);
assign y = (a & b & c) | (a & b & ~c);
endmodule
module gate_bad(input wire a, input wire b, input wire c, output wire y);
assign y = a | (b & ~c);
endmodule
module m(input wire a, input wire b, input wire c, output wire trigger);
wire yg, yo;
gold g(.a(a), .b(b), .c(c), .y(yg));
gate_bad o(.a(a), .b(b), .c(c), .y(yo));
wire care = ~(a & ~b);
assign trigger = (yg ^ yo) & care;
endmodule
EOV
hierarchy -check
proc
opt
hierarchy -top m
flatten
tee -o cex_bad.txt sat -show-inputs -show-outputs -prove trigger 0 -falsify m
log PASS: solver refutes the wrong implementation with input 010

recorded counterexample under the honest mask
  Signal Name             Dec       Hex           Bin
  \a                        0         0             0
  \b                        1         1             1
  \c                        0         0             0
  \trigger                  1         1             1

Read the two variants as a pair. The lying mask passes and the honest mask fails with a counterexample at 010, so the lie is only caught when the mask itself is checked against the specification or the environment, with assertions or simulation. The solver proves the implementation under the mask; reviewing the mask is your job.

Common mistakes

Full equivalence must fail here: the resolved form answers 1 on the don't-care rows where the specification answers 0, by design. Prove under the care mask instead, and review the mask itself: the mask is the one input the solver never checks.

Related topics

• Previous: AIGs, depth and area

• Next: Technology Mapping