Module netlist 

Verilog to and-inverter graphs, through yosys: the bridge that puts any RTL the compiler prints in front of the certified equivalence engine (logicaffeine_proof::sweep, logicaffeine_proof::seq_equiv).

synthesize elaborates one top module with its parameters set (script), flattens it, maps memories to flip-flops, and writes two views: the word-level netlist as yosys JSON, read here for its clock domains, and the bit-level circuit as ASCII AIGER, read by Aig::parse. Nothing in the script rewrites logic: no opt_expr, no abc; every multiplier is lowered by one fixed map (CANONICAL_MUL), so a product is the same circuit in every design that computes it; cells computing one thing from the same signals are merged first (opt_merge), once every undefined bit is a cell of its own, so a design computing a product many times lowers it once. An undefined bit ('x, an unassigned branch) becomes a free input (setundef -anyseq), so a proof holds for every value it could take and never for a value an optimizer chose; synthesize_reading with Undefined::Zero reads every one as 0 instead (setundef -zero), the source as a circuit that fixed them does; asynchronous resets become synchronous (async2sync), the cycle-level reading every flip-flop then has on the one global clock the AIGER latches tick on. That reading is exact only for a design with a single clock and no level-sensitive latches, so a design with several clocks or any latch is refused by name (NetlistError::Clocks, NetlistError::LevelLatches) rather than modeled wrongly; check such a design one clock domain at a time.

yosys is LOGOS_YOSYS when set, else yosys on PATH. Each run works in its own directory under the system temporary directory and removes it.

Structs

ClockSource

A net that clocks registers or memory ports: its name, what drives it, and the register bits it clocks.

CutNetlist

A design with its units cut out: its netlist and the instances, by name.

Domains

The sequential elements of a flattened module.

Graph

A module’s instances as a floorplan’s wires: every instance, each pair of them and the bits between them, and each instance and the bits between it and the module’s own ports, in name order, no wire of no bits.

Link

Two instances of a module and the bits between them.

Netlist

A synthesized module: its bit-level circuit, its word-level yosys JSON, and its clock domains.

UnitInstance

An instance of a unit cut out of a design (synthesize_cut): its flattened name, its module, the parameters it gives its module (by name, each value in one spelling, rtlil_value; every one it leaves is the module’s default), and its input and output ports with their widths, in the order the netlist lists them.

Enums

ClockDriver

What drives a net that clocks registers.

NetlistError

Why a module did not become an and-inverter graph.

Undefined

What an undefined bit of the source is in the circuit.

Functions

clock_sources

Every net that clocks a register or a memory port of top with its parameters set, flattened: what drives it and the register bits it clocks, the nets no port drives first, then by the bits they clock. A clock a register or logic makes inside a design reaches no global network unless the fitter gives it one, and a persona’s region cannot; it rides general routing, its skew paid for in the delay the router adds for hold, so a design is refused such a clock before it is fitted.

module_graph

The instances of module in verilog as a floorplan’s wires: each pair of its instances and the bits between them, and each instance and the bits between it and the module’s own ports. The modules through names are dissolved into it (flatten), so their instances are the module’s, named by path (fast|unit; a generate block’s lane_port[0].port); every other module is read by its ports alone (read_verilog -lib), so nothing under an instance is elaborated. The bits between two ends are the nets one drives and the other reads, and what each drives into the other through the module’s own logic (its registers, multiplexers and the rest, one cell or more): the fewer of the nets leaving the one and the nets arriving at the other, so a bus through a register stage counts its width and a select steering a bus one bit. A net two ends only read joins neither to the other: a broadcast is a star from its driver, not a wire between every two of its readers. A glue cell’s clock pins carry no bits: the clock network is no wire a floorplan shortens.

script

The yosys script that elaborates top with params and writes design.json and design.aag, every undefined bit a free input. The design is read deferred: a module is elaborated only as the hierarchy instantiates it, with its instance’s parameters, never at its defaults on the way in.

script_cut

script_reading with every instance of the units modules cut out: each module read from units.v as its ports alone (read_verilog -lib, its body never elaborated; a module no unit is named is an error), and once the design is flat and written, each instance turned into ports of the top (expose -evert) — its outputs inputs named <instance>.<port>[bit], its inputs outputs of the same names.

script_reading

script, each undefined bit read as undefined says.

synthesize

Synthesize top of verilog with params set into an and-inverter graph, every undefined bit a free input.

synthesize_cut

top with every instance of the units modules cut out (script_cut), each undefined bit read as undefined says: a composition whose units are proven apart, to be proven over its units as functions it knows nothing of.

synthesize_reading

synthesize, each undefined bit read as undefined says.