What counts as redundant

Redundant logic computes something already known, or something nobody reads. Two gates with identical inputs compute the same value twice. A gate whose output never reaches an output computes nothing at all. And some logic is redundant only in context: it looks useful gate by gate, but no input combination can observe it.

Removal is safe exactly when the visible function never changes, and safe is a claim that needs a proof, not a glance. This lesson runs three redundancies through the same passes. One falls to plain opt. Two survive it and fall only to ABC, which removes them through AIG structural hashing and truth-table rewriting over small cuts. That rewriting is itself local in scope; the real contrast is that Yosys opt_expr carries no absorption or reconvergence rule, while ABC compares the truth tables of small cuts.

Three redundancies, three fates

The first script builds the easy case: two identical AND gates feeding one OR. After elaboration the recorded netlist holds two AND cells and one OR cell. The script then runs the four small passes one by one, each with its log captured, before the blanket opt. The assertions pin the outcome: exactly one AND cell remains and no OR cell.

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

read_verilog <<EOV
module dupred(input wire a, input wire b, output wire y);
wire t1 = a & b;
wire t2 = a & b;
assign y = t1 | t2;
endmodule
EOV
hierarchy -check -top dupred
proc
write_json net_dup_proc.json
tee -o log_expr.txt opt_expr
tee -o log_merge.txt opt_merge
tee -o log_muxtree.txt opt_muxtree
tee -o log_clean.txt opt_clean
opt
check
write_json net_dup_opt.json
select -assert-count 1 t:$and
select -assert-none t:$or
log PASS: duplicate gates merge and the self-OR folds away

What each opt pass does

The table names each pass's job on this exact design; the recorded lines below are the passes reporting back, one action line per pass. Read both in run order.

recorded action lines, one per pass
opt_expr: Optimizing module dupred.
opt_merge: Removed a total of 1 cells.
opt_muxtree: Removed 0 multiplexer ports.
opt_clean: Removed 0 unused cells and 3 unused wires.

On the duplicate design the division of labour is visible in the recorded counts: elaboration gives 2 AND cells and 1 OR cell, and after the passes 1 AND cell remains with no OR cell. The merge pass unites the duplicates; the expression pass folds the OR of a signal with itself.

Where opt stops and ABC continues

The next two scripts run the harder pair. y = a | (a & b) is redundant by absorption: when a is 1 the answer is 1 whatever b says, and when a is 0 both terms are 0. y = (a & b) | (a & ~b) is redundant by reconvergence: a fans out to both AND gates and meets again at the OR, and case-splitting on a shows the output always equals a. Both arguments quantify over input combinations, and opt_expr carries no rule for either shape, so opt leaves both netlists untouched; ABC's hashing and rewriting, which compares truth tables of small cuts, removes them during mapping.

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 absred(input wire a, input wire b, output wire y);
assign y = a | (a & b);
endmodule
EOV
hierarchy -check -top absred
proc
tee -o stat_abs_proc.txt stat
write_json net_abs_proc.json
opt
check
tee -o stat_abs_opt.txt stat
write_json net_abs_opt.json
select -assert-count 1 t:$and
select -assert-count 1 t:$or
techmap
tee -o abc_abs.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_abs.txt stat -liberty course.lib
write_json net_abs_map.json
select -assert-none t:$and t:$or t:$not
check
log PASS: opt keeps the absorption term while abc maps it away

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 recreconv(input wire a, input wire b, output wire y);
assign y = (a & b) | (a & ~b);
endmodule
EOV
hierarchy -check -top recreconv
proc
tee -o stat_rec_proc.txt stat
write_json net_rec_proc.json
opt
check
tee -o stat_rec_opt.txt stat
write_json net_rec_opt.json
select -assert-count 2 t:$and
select -assert-count 1 t:$or
techmap
tee -o abc_rec.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_rec.txt stat -liberty course.lib
write_json net_rec_map.json
select -assert-none t:$and t:$or t:$not
check
log PASS: opt keeps the reconvergent redundancy while abc maps it away

Read the middle column first: it is the recorded evidence that generic optimisation changed nothing on either harder design. Then read the right column: mapping covers each output with a buffer, 1 x BUF in both recorded histograms, because once ABC sees that each output equals the wire a, a buffer carrying a to the output is the whole cover.

Proof in Yosys

Three simplifications that sound aggressive need one proof: the duplicate pair folded to one AND, and both harder outputs replaced by the wire a. The script below builds the original three-output design beside the simplified one, joins them with a miter, and asks the solver to prove the trigger can never fire. Proving happens before mapping on purpose: library cells carry no SAT model.

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, output wire y_dup, output wire y_abs, output wire y_rec);
wire t1 = a & b;
wire t2 = a & b;
assign y_dup = t1 | t2;
assign y_abs = a | (a & b);
assign y_rec = (a & b) | (a & ~b);
endmodule
module gate(input wire a, input wire b, output wire y_dup, output wire y_abs, output wire y_rec);
wire t = a & b;
assign y_dup = t;
assign y_abs = a;
assign y_rec = a;
endmodule
EOV
hierarchy -check
proc
opt
miter -equiv -flatten -make_outputs gold gate m
hierarchy -top m
sat -prove trigger 0 -verify m
log PASS: simplified outputs equal the originals on every input

The PASS line covers all four input pairs on all three outputs at once: the miter flags any input where any pair of outputs differs, and the solver proves no such input exists. Sampling a few vectors could miss the one that differs; the proof quantifies over all of them. That is the difference between testing a rewrite and knowing it.

Break it: skip the merge pass

Now change one thing about the setup: run the duplicate design through opt_expr and opt_clean but skip opt_merge. If merging were doing real work here, skipping it should leave gates behind. The script folds and cleans without merging and records the surviving netlist.

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

read_verilog <<EOV
module dupred(input wire a, input wire b, output wire y);
wire t1 = a & b;
wire t2 = a & b;
assign y = t1 | t2;
endmodule
EOV
hierarchy -check -top dupred
proc
tee -o stat_nomerge_proc.txt stat
write_json net_nomerge_proc.json
opt_expr
opt_clean
check
tee -o stat_nomerge.txt stat
write_json net_nomerge.json
select -assert-count 2 t:$and
select -assert-count 1 t:$or
log PASS: folding without merging leaves the duplicate pair in place

Without the merge pass the recorded netlist keeps 2 AND cells and 1 OR cell, against a single AND cell and no OR with the full pass. Expression folding alone cannot see that the two AND cells are identical; only the merge pass unites them so the self-OR can fold. The general lesson is that each redundancy belongs to the pass that can see it, and the recorded stage reports tell you which one did the work.

Common mistakes

Redundancy at RTL is not always redundancy at the gate level. Sub-expressions written twice in RTL merge only if every input matches exactly after elaboration; one width or signedness difference prevents the merge, and the duplicate survives to mapping. Check the proc-stage netlist before assuming the merge happened.

Related topics

• Previous: Constant propagation

• Next: Factoring, collapsing and sharing