Synthesis and equivalence
xl_synth: smaller, shallower netlists, many times faster
xl_synth is Xerolane's synthesis tool, built on Yosys 0.69, the open-source synthesis tool. It reads SystemVerilog through the slang frontend and writes a gate netlist, or a netlist of a standard-cell library's own cells. Against standard Yosys 0.69 with ABC on the same RTL, its netlists are smaller and about half as deep, and it makes them many times faster, on one laptop. The mapping of every netlist it writes to gates is proven equivalent before the netlist is written. What is proven, and what is checked.
faster: Vortex with 1 core from SystemVerilog into the sky130 cell library in 27 s, against 3,943 s for standard Yosys 0.69 with ABC.
less cell area on Vortex than standard Yosys with ABC, with 15% fewer cells, at half the logic depth.
less cell area on picorv32, with 19% fewer cells, 23 cells deep against 62.
peak memory for Vortex into sky130, against 2.1 GB for standard Yosys.
Mapped into a standard-cell library
Both sides map into the SkyWater sky130 high-density library: standard Yosys with dfflibmap and abc -liberty, xl_synth with its own mapping over the same library's cells. Vortex keeps its memories as the same RAM macros on both sides; picorv32 builds its register file from flip-flops. Area and cells are the logic's (the flip-flops are the same cells on both sides); depth is in cells on the longest path between flip-flops.
| Standard Yosys 0.69 with ABC | xl_synth | Difference | |
|---|---|---|---|
| Vortex, 1 core, memories as RAM macros | |||
| Logic area (µm²) | 1,457,330 | 1,360,861 | 6.6% smaller |
| Logic cells | 256,471 | 218,553 | 15% fewer |
| Logic depth (cells) | 64 | 33 | 48% less |
| RTL to netlist | 3,943 s | 27 s | 146× faster |
| Peak memory | 2.1 GB | 1.5 GB | 29% less |
| picorv32, register file as flip-flops | |||
| Logic area (µm²) | 89,146 | 79,262 | 11% smaller |
| Logic cells | 15,138 | 12,309 | 19% fewer |
| Logic depth (cells) | 62 | 23 | 63% less |
| RTL to netlist | 5.0 s | 3.9 s | 1.3× faster |
Vortex with 2 and 4 cores: xl_synth takes 2,825,505 µm² (34 cells deep) and 5,670,362 µm² (35 cells deep); standard Yosys's runs on them are in progress.
Gate counts
Here both sides make their own generic gates. With memories kept as RAMs, both map Vortex's memories to the same RAM macro, and the counts are the logic and flip-flops around the RAMs. Both are counted the same way: each gate and each flip-flop once, a flip-flop with an enable once, RAM macros not counted, and depth in two-input AND levels.
| Standard Yosys 0.69 with ABC | xl_synth | Difference | |
|---|---|---|---|
| Vortex, 1 core, memories as RAMs | |||
| Gates and flip-flops | 277,753 | 264,850 | 4.6% fewer |
| Logic depth | 138 | 71 | 49% less |
| RTL to gate netlist | 221 s | 4.9 s | 45× faster |
| Vortex, 2 cores, memories as RAMs | |||
| Gates and flip-flops | 568,419 | 540,885 | 4.8% fewer |
| Logic depth | 136 | 71 | 48% less |
| RTL to gate netlist | 529 s | 8.8 s | 60× faster |
| Vortex, 4 cores, memories as RAMs | |||
| Gates and flip-flops | 1,407,781 | 1,350,385 | 4.1% fewer |
| Logic depth | 138 | 71 | 49% less |
| RTL to gate netlist | 1,854 s | 22.9 s | 81× faster |
| Vortex, 1 core, memories built from flip-flops | |||
| Gates and flip-flops | 1,807,014 | 1,233,158 | 32% fewer |
| Logic depth | 138 | 71 | 49% less |
| RTL to gate netlist | 507 s | 14.1 s | 36× faster |
Every figure on this page is from one laptop: an Intel Core i7-14650HX with 24 threads and 64 GB of memory. Standard Yosys 0.69 is built from its release tag; its synthesis is synth -flatten, which runs ABC.
Capacity: Vortex with 16 cores
Vortex is an open RISC-V GPGPU. With 16 cores in one cluster and a shared L2 cache it builds to 8,576,969 gates and 1,373,475 flip-flops, with its arrays kept as memories. Every figure is from one laptop: an NVIDIA RTX 4060 Laptop GPU and an Intel Core i7-14650HX with 24 threads and 64 GB of memory.
Yosys 0.69, the release xl_synth is built on, took 1,598 s and 35 GB to synthesise this design. xl_synth's front end takes 38 s and 1.11 GB: 42 times faster in 31 times less memory.
The proof of xl_synth's gate mapping against Yosys's techmap rules takes 15.5 s. From the SystemVerilog sources to a gate netlist ready to simulate, every step takes 72 s.
What is proven, and what is checked
Inside one xl_synth run, the RTL is elaborated, optimised and flattened into a word-level netlist of adders, multiplexers, registers and memories. That netlist is then mapped to gates twice: once by xl_synth, which gives the netlist we deliver, and once by Yosys's own techmap rules, applied cell by cell. The two gate netlists are proven equivalent: every flip-flop's next state, every memory port and every output is the same function on both sides, for every value of the inputs and the present state. A netlist mapped into a cell library is proven a second time: its cells are read back through the library's own functions and proven equal to the gates already proven.
That proof covers the step from words to gates. It does not cover the steps from the RTL to words; those are checked, not proven, by running the RTL in Verilator and the gate netlist in our GPU simulator on the same stimulus and comparing every output on every cycle.
- Proven: words to gatesOn Vortex with 16 cores, 1,669,271 of the 1,768,373 points match by structure, and the remaining 99,102 are proven with a SAT solver, in parallel, with a result that does not depend on how many run at once. Memory ports, start values and the clock edge of every flip-flop are compared, not only the logic between them.
- Checked: RTL to gates, by simulationVortex with 16 cores built this way matches Verilator running the RTL on 512 of 512 random stimulus sets of 2,000 clocks each. That is evidence, not a proof. RTL to gates →
- Checked: the passes we replacedEach pass we replaced gives a netlist byte for byte the same as the Yosys pass it replaces, on Vortex and on Yosys's own tests.
- Next: proven against an unmodified YosysA gold netlist built by standard Yosys 0.69 from its own elaboration of the RTL, without optimisation, proven equivalent to xl_synth's netlist. The proof then covers every step of xl_synth, from the RTL to gates.
What changed
- A compact netlistThe optimisation rounds and the memory passes run on a flat netlist of our own: nodes per wire bit and cells as records. It holds Vortex with 8 cores in 61 MB, where Yosys's own netlist takes 880 MB.
- Gates written, not heldThe gate mapping the check compares against is written cell by cell, from one template per kind of cell, instead of being built whole in memory first.
- Identical instances read onceA module used many times, such as a core, is elaborated once and shared.
- Without ABCxl_synth does not call ABC, Yosys's external logic optimiser. Its optimisation of the logic and its mapping into a cell library are its own, and every netlist they produce is proven.
Each pass we replaced gives a netlist byte for byte the same as the Yosys pass it replaces, on Vortex and on Yosys's own tests. xl_synth is built on Yosys 0.69, under Yosys's ISC licence. Our thanks to the Yosys and slang projects.