Boolean optimisation rewrites a logic network into a cheaper equivalent without changing what it computes. Every rewrite in this topic answers the same two questions: which gates can go, and how do you know the function survived? The five lessons below run real Yosys and ABC scripts, so each answer comes with a recorded report instead of a sketch.
The rewrites run in a typical order, iterated to a fixed point: Yosys opt repeats its passes until nothing changes, so each pass cleans up after the last. Constants fold first, since a tied input can delete a whole cone and expose new duplicates. Redundancy removal merges what the folding exposed. Sharing and factoring then trade literals against depth, the depth-area step rebalances the result, and AIG rewriting works the whole cone at once. Don't-care simplification runs last, because it changes the function on purpose and needs the care set written down before anything else moves.
Rewrite | What it removes | Risk |
|---|---|---|
Constant propagation | Gates with a tied input and everything they imply | None: the function is unchanged on every input. |
Redundancy removal | Duplicate gates and dead logic | None: the function is unchanged on every input. |
Sharing and factoring | Repeated sub-expressions and excess literals | Depth can grow while area shrinks. |
AIG rewriting and balancing | Depth and redundant structure across the whole cone | Generic depth only hints at the mapped delay. |
Don't-care simplification | Minterms the environment never produces or never observes | Wrong care-set claims change the function. |
Read the flowchart as a typical round, not a rigid script. Each box consumes the netlist the previous box wrote: folding turns gates into wires and constants, the four opt passes simplify those expressions, merge the duplicates they expose, prune dead mux branches and delete what is left unused, sharing reuses repeated cones, the depth step rebalances slow paths, and the don't-care step is allowed to change answers only where the care set says nobody looks. Iteration repeats the round until nothing changes. Mapping then covers whatever survives with library cells.
Lesson | What it covers |
|---|---|
Folding tied inputs through gates, masks and flops, with recorded before and after reports. | |
Duplicate, dead and self-cancelling logic, with a solver proof that the function survived. | |
Literal counts and sub-expression reuse, priced by hand and mapped by ABC. | |
And-Inverter Graphs and the depth-area trade-off on chains, trees and an adder. | |
External and observability don't-cares, with a Karnaugh map and a proof. |
You can read an optimisation log and say which pass did what: which lines folded constants, which merged duplicates, which deleted dead logic. You can predict what a tied input does to its cone before running the tool, and you can set up the solver proof that checks a rewrite kept the function. You can price a factored form by hand, read the mapped area ABC reports for the same function, and explain any gap between the two without guessing.
You can also say when to stop. A rewrite that deletes gates but adds a level of depth is only a win if the path had slack. A don't-care claim is only safe with a source in the specification. Those two judgements, plus the habit of proving each rewrite instead of eyeballing it, are what this topic is for. The next topic spends them on library cells.
The sharing and factoring row. Depth can grow while area shrinks, and the function must stay identical on every input combination.
The delay target with its constraint file, and the cell library. The Area Against Delay lesson in technology-mapping varies the target against sized.lib, and the sharing lesson maps one function against course.lib and nand_only.lib.
This hub runs no tool itself. Its numbers and pictures live in the five lessons below, each recorded from Yosys 0.69+post with ABC by the course checker (scripts/tools/run-rtl-testbenches.mjs with COURSE=synth). The teaching libraries course.lib and nand_only.lib are fictional, so absolute areas are teaching units; the shapes of the trade-offs are the point.