A 4-bit adder, s = a + b, is synthesised once and mapped three times with ABC: full teaching library, NAND-only variant, and full library with XOR2 banned. Every area below comes from the recorded stat reports, in library units of the fictional teaching library, never silicon. The libraries are fixed data: course.lib holds 15 cells and nand_only.lib 3.
Cell | Area | Cell | Area |
|---|---|---|---|
INV | 1 | XNOR2 | 5 |
BUF | 2 | AOI21 | 3 |
NAND2 | 2 | OAI21 | 3 |
NOR2 | 2 | MUX2 | 5 |
AND2 | 3 | DFF | 8 |
OR2 | 3 | DFFR | 10 |
NAND3 | 3 | ||
NOR3 | 3 | ||
XOR2 | 5 |
The restricted nand_only.lib holds only INV, BUF, and NAND2 at the same areas; every other function must be built from those three.
The script synthesises the adder once, saves the generic gates, and maps the same gates three ways — all against typical.constr with a very loose 100000 ps target, so every ABC report carries its Gates, Area, and Delay line. Each run writes its report and histogram; the first and third also write netlists. The assertions are the lesson's spine: no generic gate may remain after any mapping, the NAND-only run must hold no AND2, OR2, XOR2, XNOR2, AOI21, OAI21, or MUX2 and at least one NAND2, and the third run no XOR2. Every figure is read back from the files this script writes.
read_verilog <<EOV
module adder4(input [3:0] a, b, output [4:0] s);
assign s = a + b;
endmodule
EOV
synth -top adder4
design -save generic
tee -o abc_full.txt abc -liberty course.lib -constr typical.constr -D 100000
tee -o stat_full.txt stat -liberty course.lib
write_json net_full.json
select -assert-none t:$and t:$or t:$xor t:$xnor t:$mux t:$not
select -assert-none t:$_AND_ t:$_OR_ t:$_XOR_ t:$_XNOR_ t:$_MUX_ t:$_NOT_ t:$_NAND_ t:$_NOR_
check
design -load generic
tee -o abc_nand.txt abc -liberty nand_only.lib -constr typical.constr -D 100000
tee -o stat_nand.txt stat -liberty nand_only.lib
select -assert-none t:$and t:$or t:$xor t:$xnor t:$mux t:$not
select -assert-none t:$_AND_ t:$_OR_ t:$_XOR_ t:$_XNOR_ t:$_MUX_ t:$_NOT_ t:$_NAND_ t:$_NOR_
select -assert-none t:AND2 t:OR2 t:XOR2 t:XNOR2 t:AOI21 t:OAI21 t:MUX2
select -assert-min 1 t:NAND2
check
design -load generic
tee -o abc_noxor.txt abc -liberty course.lib -dont_use XOR2 -constr typical.constr -D 100000
tee -o stat_noxor.txt stat -liberty course.lib
write_json net_noxor.json
select -assert-none t:$and t:$or t:$xor t:$xnor t:$mux t:$not
select -assert-none t:$_AND_ t:$_OR_ t:$_XOR_ t:$_XNOR_ t:$_MUX_ t:$_NOT_ t:$_NAND_ t:$_NOR_
select -assert-none t:XOR2
check
log PASS: adder maps to three libraries with asserted cell setsThe recorded full-library histogram holds 3 XOR2 cells alongside 3 XNOR2 cells. Both cost 5 units, so no bit saves area by switching polarity — each sum takes the polarity its neighbouring carry logic absorbs most cheaply, the same bubble-pushing from the previous lesson. The NAND-only histogram holds neither by construction, and the XOR2-banned run holds 0 XOR2, exactly as its assertion demands.
Library | Cells | Area (library units) | Delay (ps, ABC report) | XOR2 cells |
|---|---|---|---|---|
course.lib | 18 | 59 | 510 | 3 |
nand_only.lib | 42 | 66 | 922 | 0 |
course.lib, XOR2 banned | 20 | 59 | 600 | 0 |
Read the table as three answers to one RTL. The full library reports 18 cells at area 59 with arrival 510 ps: the mapper's free choice, undisturbed. The NAND-only library reports 42 cells at area 66 with arrival 922 ps, a rise of 7 units, because every sum that wanted one XOR2 is rebuilt from several NAND2 cells and the extra gates outweigh the saving per cell. The XOR2 ban reports 20 cells at area 59 with arrival 600 ps: the same area as the free run across two more cells, with the delay up about 90 ps. Set that reroute beside the NAND-only rebuild in the table, and price each restriction separately.
The figure is the cover made visible: sums in XOR2 and XNOR2 cells, carries in the AND, NAND, NOR, and AOI/OAI cells beside them — all proven present by the histogram and generic-free by the assertions. The library is fictional, so absolute areas are classroom units; the shape of the trade is the point that transfers.
The third run in the script is the break-it: the full library minus XOR2, the exact cell a ripple adder reaches for first. The recorded fallback is not NAND-based: NAND2 holds at 5 in both histograms, while XOR2 goes to 0 and XNOR2 rises from 3 to 4, AND2 from 1 to 3, and NOR2 from 2 to 4. The swap to XNOR2 carries the sums at the same 5-unit price, and the AND2 and NOR2 growth absorbs the polarity the XOR2 used to provide. The area holds level with the free run across 20 cells, with the arrival slipping from 510 ps to 600 ps. Compare that reroute with the NAND-only rebuild in the table: removing one cell kind where polarity and AND/NOR fallbacks exist is a reroute, while removing the whole library down to three cells is a rebuild. Bans are priced per option removed, not per ban issued, in these runs.
Sums need XOR behaviour. The full library covers the four sum bits with 3 XOR2 cells and 3 XNOR2 cells: six XOR-family cells at 5 units each, so no bit saves area by switching polarity and each sum takes the polarity the neighbouring carry logic absorbs most cheaply. The restricted library builds each sum from several NAND2 cells instead. The table shows the bill: area 59 against 66, a rise of 7 units for the same addition.
Each assert-none line proves the named generic gate kind is gone from the mapped netlist; together they prove the mapping reached library cells. A silent area quote proves nothing by itself, which is why this lesson's table is read back from the recorded stat files the asserted script wrote.
Every number and picture on this page comes from one Yosys 0.69 run of the script shown, recorded by the course checker (scripts/tools/run-rtl-testbenches.mjs with COURSE=synth): ABC maps a behavioural 4-bit adder against course.lib, against nand_only.lib, and against course.lib with XOR2 banned. The libraries are fictional, so absolute areas are teaching units; the ordering of the three results is the point.