From RTL to cells

The design below holds one inverter and one two-input NAND. Mapping must cover both from the course library.

The script reads the library, runs generic optimisation, maps with ABC, then asserts the result. Each assertion pins a claim the lesson makes.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

read_liberty -lib course.lib
read_verilog <<EOV
module top(input wire a, input wire b, input wire c, output wire y1, output wire y2);
assign y1 = ~a;
assign y2 = ~(b & c);
endmodule
EOV
hierarchy -check -top top
proc
opt
techmap
abc -liberty course.lib
stat -liberty course.lib
select -assert-count 1 t:INV
select -assert-min 1 t:NAND2
log PASS: inverter maps to INV and NAND maps to NAND2 from course.lib

Reading the result

The first assertion pins exactly one INV cell. The second pins at least one NAND2 cell, a bound that holds even if the mapper adds buffering.

The stat line reports area from the same library areas. No report text is quoted here, so every number below comes from asserted counts times table areas.

course.lib EXAMPLE areas (library units): INV = 1, NAND2 = 2
example covering: 1 INV cell and 1 NAND2 cell
area = 1 x 1 + 1 x 2 = 1 + 2 = 3 library units

What the library decides

The same RTL mapped against nand_only.lib can only use INV, BUF, and NAND2. A wider library offers cheaper coverings, such as AOI21 for and-or-invert cones.

Every mapping claim names its library. Cell counts and areas from one library never transfer to another.

Related topics

• Delay tables and interpolation

• Structuring and Buffering