The design computes y from (a and b) or (c and d): an AND-OR structure over four inputs. The assertions below pin only robust facts about the mapped result.
The full Verilog sits inside the runnable block, with one design only. It finishes in a fraction of a second.
Command | Stage | What it does here |
|---|---|---|
read_verilog | Read in | Loads the inline design through a here-document. |
hierarchy | Elaboration | Checks the design and sets the top module. |
proc, flatten | Elaboration | Resolves processes and flattens hierarchy. |
opt | Generic optimisation | Cleans up the generic graph before mapping. |
techmap | Mapping | Lowers generic cells toward mappable gates. |
abc -liberty | Mapping | Maps the logic to cells of course.lib. |
stat -liberty | Reporting | Prints counts and area in library units. |
The script below runs the whole flow and asserts only robust facts: no generic gates remain and mapped cells are present. A wrong claim fails the run instead of printing PASS.
read_verilog <<EOV
module and_or(
input wire a,
input wire b,
input wire c,
input wire d,
output wire y
);
assign y = (a & b) | (c & d);
endmodule
EOV
hierarchy -check -top and_or
proc
flatten
opt
techmap
abc -liberty course.lib
stat -liberty course.lib
select -assert-none t:$_AND_ t:$_OR_ %u
select -assert-min 1 t:NAND2
log PASS: and_or mapped to library cells with no generic gates leftThe PASS line proves the mapped design uses library cells, with at least one NAND2 present. Exact mapped counts depend on the tool build, so the lesson never quotes them.
That no generic AND or OR remains and at least one mapped NAND2 is present. Exact mapped counts depend on the tool build, so the script never pins them.
Before techmap the design still uses coarse cells, so a generic-gate assertion there fails. The script pins only post-mapping facts.