Inference produces coarse generic cells such as $dff, $dffe, $sdff, and $adff, but no chip is built from them. Something must exchange each one for a library cell with known area and timing, adding logic wherever the library lacks the exact flop. This lesson runs that exchange on three designs: a lone plain flop, a mixed 6-bit register with an enabled pair, a sync-reset pair, and an async-reset pair, and a combined reset-plus-enable break-it. Every histogram and area below is read back from the recorded stat reports.
Inference produces the coarse families; synth lowers them to fine generic flops; dfflegalize restricts the fine set to cells the library can absorb; and dfflibmap performs the exchange against the liberty file, emitting DFF or DFFR cells. Combinational mapping around the flops is a separate step covered with technology mapping. Mapping directly from the coarse $dff-family cells fails, so the lowering order in the scripts is load-bearing, not stylistic.
The first script maps a lone plain flop to the teaching library and asserts the exchange exactly: one DFF cell and no remaining generic flop. The recorded chip area is 8, which is the per-bit storage price the whole topic leans on. The second script maps the mixed 6-bit register and asserts at least one DFF and one DFFR, with no generic flop cells left behind. Its recorded histogram reads DFF x4, DFFR x2, INV x4, MUX2 x2, NOR2 x2; the per-type table below breaks the mix down.
read_verilog <<EOV
module lone(input clk, input d, output reg q);
always @(posedge clk) q <= d;
endmodule
EOV
read_liberty -lib course.lib
hierarchy -check -top lone
synth -top lone
dfflegalize -cell $_DFF_P_ 01 -cell $_DFF_PN0_ 01
dfflibmap -liberty course.lib
tee -o abc_lone.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_lone.txt stat -liberty course.lib
write_json net_lone.json
select -assert-count 1 t:DFF
select -assert-none t:$_DFF_P_
select -assert-none t:$_DFF_PN0_
log PASS: plain flop maps to one DFF library cellread_verilog <<EOV
module trio2(input clk, input en, input srst, input arst, input [5:0] d, output reg [5:0] q);
always @(posedge clk) if (en) q[1:0] <= d[1:0];
always @(posedge clk) if (srst) q[3:2] <= 2'd0; else q[3:2] <= d[3:2];
always @(posedge clk or posedge arst) if (arst) q[5:4] <= 2'd0; else q[5:4] <= d[5:4];
endmodule
EOV
read_liberty -lib course.lib
hierarchy -check -top trio2
synth -top trio2 -flatten
dfflegalize -cell $_DFF_P_ 01 -cell $_DFF_PN0_ 01
dfflibmap -liberty course.lib
tee -o abc_trio2.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_trio2.txt stat -liberty course.lib
write_json net_trio2.json
select -assert-min 1 t:DFF
select -assert-min 1 t:DFFR
select -assert-none t:$_DFF_P_
select -assert-none t:$_DFF_PN0_
log PASS: enable and reset flops map to DFF and DFFR cellsThe enabled pair becomes 2 DFFs plus 2 MUX2s; the sync pair becomes the other two DFFs plus gating; the async pair becomes 2 DFFRs. No family maps to a cell the library does not have, as the per-type table below confirms.
Mixed-register pair | Library cells (recorded) | Reading |
|---|---|---|
2 enabled bits | 2 DFF + 2 MUX2 | Hold needs a mux per bit here. |
2 sync-reset bits | 2 DFF + 2 NOR2 + share of INV | Reset is gates on D, as the reset lesson shows. |
2 async-reset bits | 2 DFFR | Dedicated reset pins absorb the reset. |
Library cell | Count (recorded) | Area (recorded) |
|---|---|---|
DFF | 4 | 32 |
DFFR | 2 | 20 |
INV | 4 | 4 |
MUX2 | 2 | 10 |
NOR2 | 2 | 4 |
Read the table as the whole mapping story: 70 units of chip area. The enabled bits pay 10 in feedback muxes, the sync bits pay gating around plain flops, and only the async bits land on dedicated reset cells. No generic flop survives, which the absence assertions prove rather than the prose.
Not every generic cell has a library twin. A synchronous-reset flop maps to dedicated cells only where the library offers them, and to a plain flop plus gating on D elsewhere; the enabled flop behaves the same way in this library, which has no clock-enable cell. What the fallback can build depends on the cell: the recorded fallback on this page is the reset-plus-enable split below, where each half of the behaviour lands on a structure the library has. The mapping therefore varies by library, and the generic family stays the stable thing to check first.
The third script gives a 2-bit register an asynchronous reset AND an enable, which infers the combined $adffe family, a family the script asserts right after proc. The teaching library holds no flop with both pins, so the legalization step splits the behaviour before the exchange: dfflegalize -cell $_DFF_P_ 01 -cell $_DFF_PN0_ 01 forbids enable cells, leaving the reset to ride the DFFR pin while the enable becomes a feedback mux. The recorded histogram reads DFFR x2, INV x2, MUX2 x2 at chip area 32, with no generic flop left behind. Against 22 hand-derived units for the async-only pair (2 DFFR at 10 each plus 2 INV at 1 each, from the recorded per-cell areas), the enable's two muxes read off as 10 on top, at 32.
read_verilog <<EOV
module aer2(input clk, input en, input arst, input [1:0] d, output reg [1:0] q);
always @(posedge clk or posedge arst) if (arst) q <= 2'd0; else if (en) q <= d;
endmodule
EOV
hierarchy -check -top aer2
proc
opt
select -assert-count 1 t:$adffe
select -clear
read_liberty -lib course.lib
hierarchy -check -top aer2
synth -top aer2 -flatten
dfflegalize -cell $_DFF_P_ 01 -cell $_DFF_PN0_ 01
dfflibmap -liberty course.lib
tee -o abc_aer2.txt abc -liberty course.lib -constr typical.constr -D 1000
tee -o stat_aer2.txt stat -liberty course.lib
write_json net_aer2.json
select -assert-none t:$_DFF_P_
select -assert-none t:$_DFF_PN0_
select -assert-none t:$_DFFE_PP_
select -assert-none t:$_DFFE_PN0_
log PASS: combined reset and enable maps with recorded cells2-bit register | Library cells (recorded) | Chip area (stat -liberty) |
|---|---|---|
Async reset only (same two bits, no enable) | 2 DFFR + 2 INV | 22 by hand from the recorded cell areas |
Async reset plus enable | DFFR x2, INV x2, MUX2 x2 | 32 |
Test mapping later swaps library flops for scan cells with a shift path. That step belongs to design-for-test, so this topic only notes the contract it relies on: in test mode every async set and reset must be controllable from a primary input, normally through a test-mode bypass mux around any synchronizer or generated reset logic. A synchronizer-driven reset without that bypass leaves its flops uncontrollable, so scan excludes them and coverage drops; the failure is a scan DRC exclusion, not a stitching failure. The reset lesson's synchronized release stays the functional requirement, and the bypass mux is the test requirement on top of it.
dfflibmap, one DFF is present and no generic flop cell remains. What do the assertions prove together?The count proves the flop mapped to the expected library cell. The absence checks prove no generic flop was left unmapped, so the exchange is complete.
A plain flop plus combinational gating on D, NOR2 plus INV per bit here, exactly as the mixed register records for its sync pair. The behaviour is unchanged; the area moves into the gating.
Every number and picture on this page comes from three Yosys 0.70 runs recorded by the course checker (scripts/tools/run-rtl-testbenches.mjs with COURSE=synth): a lone flop, a mixed 6-bit register, and a reset-plus-enable register through synth, dfflegalize, dfflibmap -liberty course.lib, abc -liberty course.lib -constr typical.constr -D 1000 and stat -liberty course.lib with the asserted cell sets, including a proc-level $adffe assertion on the combined register. The library is fictional, so absolute areas are teaching units.