Inference produces coarse cells such as $dff and $adff. Synthesis lowers them to generic flops, which mapping exchanges for library cells with known area and timing, adding logic where the library lacks the cell.
The dfflibmap pass performs that exchange for flops. Combinational mapping around them is a separate step covered with technology mapping.
Each script runs synth to reach generic flops, then dfflegalize, then dfflibmap. Mapping directly from coarse $dff-family cells fails, so the lowering step is required.
The first script maps a plain flop to the teaching library. It asserts one DFF cell and no remaining generic flop cells.
read_verilog <<EOV
module top(input clk, input d, output reg q);
always @(posedge clk) q <= d;
endmodule
EOV
read_liberty -lib course.lib
hierarchy -check -top top
synth -top top
dfflegalize -cell $_DFF_P_ 01 -cell $_DFF_PN0_ 01
dfflibmap -liberty course.lib
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 cellThe second script maps a module with an enable flop, a sync-reset flop and an async-reset flop. It asserts at least one DFF and one DFFR cell, with no generic flop cells left behind.
read_verilog <<EOV
module top(input clk, input en, input srst, input arst, input [2:0] d, output reg [2:0] q);
always @(posedge clk) if (en) q[0] <= d[0];
always @(posedge clk) if (srst) q[1] <= 1'b0; else q[1] <= d[1];
always @(posedge clk or posedge arst) if (arst) q[2] <= 1'b0; else q[2] <= d[2];
endmodule
EOV
read_liberty -lib course.lib
hierarchy -check -top top
synth -top top
dfflegalize -cell $_DFF_P_ 01 -cell $_DFF_PN0_ 01
dfflibmap -liberty course.lib
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 cellscourse.lib EXAMPLE areas: DFF = 8 units, DFFR = 10 units
8-bit plain register post-map: 8 x 8 = 64 units
8-bit async-reset register post-map: 8 x 10 = 80 unitsNot every generic cell has a library twin. A synchronous-reset flop maps to dedicated cells only where the library offers them, and to a flop plus feedback logic elsewhere.
Enabled flops behave the same way in this library, which has no clock-enable cell. The mapping therefore varies by library, and the generic family stays the stable thing to check first.
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 that inferred flops must stay mappable to whatever the scan flow substitutes.
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.
A plain flop plus feedback mux logic implementing the reset. The behaviour is unchanged; the area grows.