The design computes y from (a and b) or (c and d): an AND-OR cone over four inputs and one output. It is the smallest design that still exercises every stage boundary: coarse gates after elaboration, bit-level gates after lowering, and a handful of library cells after mapping. The full Verilog sits inside the runnable block below, one module only, finishing in a fraction of a second.
Two deliberate choices keep the assertions honest. First, the script pins exact counts only before mapping, where elaboration is deterministic: two $and cells and one $or cell. Second, after mapping it pins only absences plus a lower bound: no coarse cells, no generic gates, and at least one library cell without naming which family the mapper chose. Pin shape, not exact library cells: a minimum on one family such as NAND2 names a covering choice the mapper is free to change between builds, so that detail stays in the recording and out of the assertions.
Command | Stage | What it does here |
|---|---|---|
read_verilog | 1. Read | Loads the inline design through a here-document. |
hierarchy | 2. Elaborate | Checks the design and sets the top module. |
proc | 2. Elaborate | Resolves processes; a no-op on this purely continuous design. |
opt | 3. Optimise | Cleans up the generic graph; nothing to fold here. |
techmap | 3. Optimise | Lowers the coarse cells toward mappable bit-level gates. |
abc -liberty | 4. Map | Maps the logic to cells of course.lib. |
stat -liberty | 5. Report | Prints counts and area in library units. |
The script below records the generic netlist, freezes it, maps it, freezes the result, then reloads each frozen stage for assertions. A wrong claim fails the run instead of printing PASS, so every number quoted after this block was checked by the tool, not by the author.
read_verilog <<EOV
module and_or(input a, b, c, d, output y);
assign y = (a & b) | (c & d);
endmodule
EOV
hierarchy -check -top and_or
proc
opt
tee -o stat_generic.txt stat
write_json net_generic.json
design -save generic
techmap
tee -o abc_mapped.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_mapped.txt stat -liberty course.lib
write_json net_mapped.json
design -save mapped
design -load generic
select -assert-count 2 t:$and
select -assert-count 1 t:$or
select -assert-none t:$_AND_ t:$_OR_ t:$_NOT_ t:$_MUX_ t:$_XOR_ t:$fa %u
design -load mapped
select -assert-none t:$and t:$or t:$xor t:$mux t:$not t:$add t:$sub %u
select -assert-none t:$_AND_ t:$_OR_ t:$_NOT_ t:$_MUX_ t:$_XOR_ t:$_NAND_ t:$_NOR_ %u
select -assert-min 1 t:INV t:BUF t:NAND2 t:NOR2 t:AND2 t:OR2 t:NAND3 t:NOR3 t:XOR2 t:XNOR2 t:AOI21 t:OAI21 t:MUX2 %u
check
log PASS: and_or keeps two ands and one or until mapping, then uses library cells only$and or $_AND_ cell remain, and will the mapped netlist use NAND2 cells?No coarse or generic cell remains: the script asserts the absence of both families, and the recording honours it. NAND2 is likely but deliberately unasserted, because the exact covering is the mapper's choice and varies between builds. The mapped netlist holds 3 library cells at area 6 library units; which families those are is read from the recording below, never pinned in the script.
The generic census is exactly what the RTL wrote: two $and cells feeding one $or cell, three cells total, zero generic gates. Elaboration preserves structure here the way it preserved the adder's word cells in the flow-stages lesson; only the cell family differs.
Generic cell type | Cells |
|---|---|
| 2 |
| 1 |
Mapping covers those three coarse cells with the library cells the stat report totals below, reaching 178 ps against the loose 1000 ps target. The per-family split is read from that same report, and the union assertion guarantees at least one of these families is present without saying which one the mapper must pick.
Library cell | Cells |
|---|---|
NAND2 | 3 |
This comparison swaps the design rather than breaking the flow. Replace the cone with a single exclusive-or, y = a ^ b, and rerun the identical flow. The generic stage must change shape: one $xor cell instead of two $and cells plus one $or. The mapped stage must change with it, because different logic offers different coverings. The second script pins the new generic count and the same library-only shape after mapping.
read_verilog <<EOV
module xor_ab(input a, b, output y);
assign y = a ^ b;
endmodule
EOV
hierarchy -check -top xor_ab
proc
opt
tee -o stat_generic_xor.txt stat
write_json net_generic_xor.json
design -save generic_xor
techmap
tee -o abc_xor.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_xor.txt stat -liberty course.lib
write_json net_xor.json
design -save mapped_xor
design -load generic_xor
select -assert-count 1 t:$xor
design -load mapped_xor
select -assert-none t:$and t:$or t:$xor t:$mux t:$not t:$add t:$sub %u
select -assert-none t:$_AND_ t:$_OR_ t:$_NOT_ t:$_MUX_ t:$_XOR_ t:$_NAND_ t:$_NOR_ %u
select -assert-min 1 t:INV t:BUF t:NAND2 t:NOR2 t:AND2 t:OR2 t:NAND3 t:NOR3 t:XOR2 t:XNOR2 t:AOI21 t:OAI21 t:MUX2 %u
check
log PASS: xor variant maps to library cells with a different mix and areaThe xor variant elaborates to a single generic cell and maps to the library cells the comparison table totals below, at the area it totals there. Fewer inputs and a different operator, with the single output unchanged: every one of those changes is visible in the two recordings side by side.
Build | Generic cells | Mapped cells | Area (library units) |
|---|---|---|---|
AND-OR cone | 3 | 3 | 6 |
XOR (`a ^ b`) | 1 | 1 | 5 |
Two $and cells, one $or cell, and zero generic gates. Elaboration is deterministic from the RTL, so exact counts are stable; the mapped covering varies between builds, so only absences and a lower bound are pinned there.
The union assertion requiring at least one library cell, together with the absence of every coarse and generic family. It guarantees library-only cells without saying which families the mapper chose.
Every number and picture on this page comes from two Yosys 0.69 runs of the shown scripts, recorded by the course checker (scripts/tools/run-rtl-testbenches.mjs with COURSE=synth): an AND-OR cone elaborated, lowered, and mapped against course.lib with a loose 1000 ps target, plus an xor variant through the identical flow. The library is fictional, so absolute areas are teaching units.