Components

Yosys

Yosys is an open-source RTL synthesis framework. It supports Verilog and SystemVerilog (via plugins), and can target a wide range of FPGAs and ASICs through its standard cell technology mapping flow.

The bundled yosys binary is built from the latest tagged upstream release at the time the yosys-bin CI run executes.

Key binaries installed to bin/:

yosys         – main synthesis tool
yosys-abc     – ABC logic synthesis engine (called by Yosys internally)
yosys-config  – build-time configuration query tool

Standard cell libraries and scripts are installed under share/yosys/.

pyosys — Python Bindings

pyosys exposes the Yosys C++ API to Python using pybind11 bindings that are compiled against the Yosys source tree.

yosys-bin provides separate .so files for each supported Python version (3.10 – 3.13) so a single installation works with multiple interpreter versions without recompilation:

pyosys/libyosys.cpython-310-x86_64-linux-gnu.so
pyosys/libyosys.cpython-311-x86_64-linux-gnu.so
pyosys/libyosys.cpython-312-x86_64-linux-gnu.so
pyosys/libyosys.cpython-313-x86_64-linux-gnu.so

The correct variant is selected automatically by the Python import machinery.

Basic usage:

import pyosys

d = pyosys.Design()
d.run_pass("read_verilog -sv my_design.sv")
d.run_pass("synth -top my_top")
d.run_pass("write_json netlist.json")

yosys-slang Plugin

yosys-slang is a Yosys frontend plugin that uses the slang SystemVerilog compiler library to elaborate SystemVerilog designs. It provides the read_slang Yosys command, which supports a broader subset of the SystemVerilog standard than the built-in read_verilog -sv parser.

The plugin is installed as:

share/yosys/plugins/slang.so
pyosys/share/yosys/plugins/slang.so   (for pip-installed paths)

Loading the plugin:

# On the command line
yosys -m slang

# Inside a .ys script
plugin -i slang
read_slang top.sv
synth -top top
write_json netlist.json

The plugin is built from source during the yosys-bin CI run. It statically links slang and {fmt} so it has no additional runtime dependencies.

Boolector SMT Solver

Boolector is an SMT solver for the theories of fixed-size bit-vectors, arrays, and uninterpreted functions. It is used by Yosys formal verification flows to discharge proof obligations produced by write_smt2.

The boolector binary is installed to bin/boolector.

Typical usage with SymbiYosys / smtbmc:

yosys -p "read_verilog -formal my_design.sv; \
           prep -top my_top; \
           write_smt2 -wires model.smt2"

smtbmc --solver boolector model.smt2

Or use the DV Flow FormalPrepare task to drive the full flow from a flow.dv description.

sby — SymbiYosys

SymbiYosys (sby) is a front-end driver for Yosys-based formal hardware verification flows. It reads a .sby configuration file that describes the design sources, the verification engine to use (e.g. smtbmc, aiger, abc), and the properties to check (BMC, k-induction, cover), then orchestrates Yosys and the chosen solver.

Installed files:

bin/sby
share/yosys/python3/sby_*.py   – sby support library

Example .sby file:

[options]
mode bmc
depth 20

[engines]
smtbmc boolector

[script]
read -formal my_design.sv
prep -top my_top

[files]
my_design.sv

Run with:

sby -f my_design.sby

mcy — Mutation Cover with Yosys

mcy measures the quality of a formal verification test suite by injecting mutations into a design and checking how many are caught by the existing properties. It produces a coverage report showing which parts of the design are exercised by the formal tests.

Installed files:

bin/mcy
bin/mcy-dash
share/mcy/scripts/   – helper scripts used internally by mcy
share/mcy/dash/      – web dashboard assets for mcy-dash

Basic usage:

mcy init          # create mcy.cfg template
mcy run -j4       # run mutation checks with 4 parallel workers
mcy dash          # start web dashboard on http://localhost:5000

eqy — Equivalence Check with Yosys

eqy performs combinational and sequential equivalence checking between two netlists using Yosys. It is useful for verifying that synthesis, retiming, or other transformations preserve circuit behaviour.

Installed files:

bin/eqy
share/yosys/python3/eqy_job.py
share/yosys/plugins/eqy_combine.so
share/yosys/plugins/eqy_partition.so
share/yosys/plugins/eqy_recode.so

Example .eqy file:

[gold]
read -sv gold.sv
prep -top top

[gate]
read -sv gate.sv
prep -top top

[strategy simple]
use sat
depth 10

Run with:

eqy -f my_check.eqy

dv-flow-libyosys

dv-flow-libyosys (Python package dv_flow.libyosys) integrates Yosys with the DV Flow task framework. It provides ready-made synthesis and formal-preparation tasks that can be wired into a larger EDA pipeline described in a flow.dv file.

See DV Flow Task Reference for the full task reference.