# SymbiYosys is the driver that turns a Yosys flow into a proof run > SymbiYosys, or sby, is a front-end driver program for Yosys based formal hardware verification flows, which means it orchestrates the synthesis and the solver rather than doing the verification itself. It is ISC licensed, it is part of both the Tabby CAD Suite and the free OSS CAD Suite, and the easiest way to get it is to install one of those bundles rather than sby alone. **YosysHQ/sby** — SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows - Repository: https://github.com/YosysHQ/sby - Stars: 559 · Forks: 108 - Language: Python - License: NOASSERTION - Published: 2026-10-22 · Updated: 2026-10-22 · Language: en - Canonical page: https://hysenlabs.com/projects/yosyshq-sby ## A driver, not a verifier SymbiYosys, or sby, is a front-end driver program for Yosys based formal hardware verification flows. The full documentation lives at yosyshq.readthedocs.io under the sby project. The word driver does a lot of work there. sby is not itself a formal verification engine. It is the program that sets up a flow, invokes Yosys to build the model, drives a solver on the result and reports the outcome, which is why the tool's job is orchestration rather than proof. That distinction matters for how you should judge the project. A verification engine's quality is a matter of how much it can prove and how fast. sby's quality is a matter of how well it expresses the flows, how clearly it reports what happened and how portable it is across the solvers you might want to use later. The engine choice is deliberately open, which is why the documentation has a section on selecting the right engine. The two halves of the name come from that arrangement. Symbi, as in symbiosis, is the collaboration between the synthesis side and the solver side, and Yosys is the tool at the centre of it. ## The licence split, and what the solvers bring SymbiYosys itself is licensed under the ISC licence, with the COPYING file at the top of the repository. The documentation is careful to add that the solvers and other components used by SymbiYosys come with their own licence terms, and points at the selecting the right engine section of the documentation for more detail. That sentence is doing real work. In a formal verification setup the solver is usually the heavyweight component, and it is frequently licensed separately, sometimes under terms that restrict use in a commercial flow. A permissive front end over a restricted engine gives you the wrong impression of what you can ship. So the correct way to evaluate a setup that uses sby is to evaluate the whole stack, engine included, and to read the terms of every piece rather than the terms of the driver. The engine documentation section is where that discussion belongs, and the fact that the project points you there rather than summarising it is a sign the maintainers consider it part of the decision. The ISC licence itself is short and permissive, with the usual disclaimer of warranty, which suits a tool that is meant to be dropped into whatever flow you already have. ## Install the suite, not the tool The installation guidance is unusually direct about this. SymbiYosys is part of the Tabby CAD Suite and the OSS CAD Suite, and the easiest way to use sby is to install the binary software suite, which contains all required dependencies, including all supported solvers. There are two routes. You can contact YosysHQ for a Tabby CAD Suite evaluation license and download link, or you can go to the OSS CAD Suite build releases to download the free OSS CAD Suite, then follow the install instructions on GitHub. The difference between them is stated in the same section, and it is not a price difference. The documentation says to make sure to get a Tabby CAD Suite evaluation license for extensive SystemVerilog Assertion support, as well as industry grade SystemVerilog and VHDL parsers. So the free suite gives you sby and the solvers, and the commercial suite adds the parts of the toolchain that deal with the languages people actually write assertions in. If your verification work is in SystemVerilog with assertions, or in VHDL, that gap is the deciding factor rather than the cost of the licences. The project also links a datasheet page for the difference between the two suites, and a contact page for the evaluation licence. ## What the Makefile actually installs The Makefile is short and its install target tells you how sby is laid out on disk, which is worth understanding because the installation is not a single script. The install target creates the bin directory and a share/yosys/python3 directory under the prefix, copies the sbysrc/sby_*.py files into that python3 directory, and then runs sed over sby_core.py to substitute a program prefix placeholder with the value of PROGRAM_PREFIX. The reason for the sed step is visible in the target itself. sby_core.py contains placeholders such as ##yosys-program-prefix##, and the sed expression rewrites that into the actual quoted prefix. The same pattern appears for the sys.path and the release version, and on Windows the shebang line is rewritten to the Windows path of the Python interpreter, which is computed with cygpath, since the launcher executable needs an absolute path to Python to work. The Windows branch also compiles a separate binary. It runs gcc with -DGUI=0 -O -s over extern/launcher.c to produce sby.exe in the bin directory, while the non-Windows branch substitutes the sys.path and the shebang into sby.py to produce sby-script.py. So on Windows the entry point is a native launcher, and elsewhere it is a Python script with a patched shebang. ## Version stamping, and the difference between the two test targets There is a small piece of build logic that is worth reading, because it explains how a tool with no releases on GitHub still knows what version it is. The Makefile checks whether the .gittag file still contains an unexpanded git describe placeholder. If it does, the release version is taken from git describe --dirty, which means a local build reports the commit it came from and marks itself dirty if the working tree has changes. If the file has been expanded at release time, the version is read from it instead. The YOSYS_RELEASE_VERSION is then substituted into the source as the release_version value, so the version a user sees in sby matches the tag the build was made from. The two test targets differ in exactly one way, and the help text spells it out. The test target runs the tests, skipping tests with missing dependencies, while the ci target runs all tests, failing tests with missing dependencies. The ci target also notes that it requires a full Tabby CAD Suite or OSS CAD Suite install. So a developer without every solver installed still gets a useful signal from the test suite, and the CI configuration is strict about it. The other targets are html to build the documentation into docs/build/html, and clean for cleanup. ## The repository layout, and a project that is still moving The top level of the repository shows what the project is made of. There is a sbysrc directory holding the Python source, a docs directory, a tests directory, a tools directory and an extern directory, which is where the launcher.c for the Windows build lives. There is a Makefile, a COPYING file, a .gittag, a .pre-commit-config.yaml and a .readthedocs.yaml, the last of which is what builds the documentation site on Read the Docs. The documentation configuration is a small signal about the project's priorities. Formal verification tooling has a steep learning curve, and the difference between a flow that works and one that silently does not is usually a detail in the documentation. A repository that treats the docs as a build artifact with its own pipeline is taking that seriously. The maintenance record is current. The last push was on 2026-10-15, and the repository publishes no GitHub releases, which is consistent with the .gittag mechanism: the version is derived from git describe rather than from a release artefact, and the binary distributions are the CAD suites rather than this repository. So the shape of the project is a driver that travels with the suite. The repository is where the driver lives and where its documentation is written, and the thing you install is the bundle. ## Conclusion Adopt SymbiYosys if you are running formal verification on hardware designs and want a driver that orchestrates the Yosys flow and the solver for you, and if you are willing to install a CAD suite to get it. Do not expect sby alone to give you a working verification setup, because the solvers and the other components come with their own licence terms and their own installation. Before you start, check two things: which suite you are installing, since the free OSS CAD Suite lacks the extensive SystemVerilog Assertion support and the industry grade SystemVerilog and VHDL parsers that the Tabby suite provides, and which engine you want to drive, since the documentation has a section on selecting the right engine and the choice determines what your flow can prove. ## FAQ ### What is SymbiYosys used for? It is a front-end driver program for Yosys based formal hardware verification flows. It orchestrates the synthesis and the solver steps and reports the outcome, rather than being a verification engine itself. ### What licence is SymbiYosys released under? SymbiYosys itself is licensed under the ISC licence, with the COPYING file in the repository. The documentation notes that the solvers and other components it uses come with their own licence terms, and points at the selecting the right engine section for details. ### How do I install SymbiYosys? The easiest way is to install a binary suite that contains all required dependencies and solvers, either the free OSS CAD Suite from its GitHub releases or the Tabby CAD Suite with an evaluation license from YosysHQ. The suite matters because the Tabby version adds extensive SystemVerilog Assertion support and industry grade SystemVerilog and VHDL parsers. ### How does sby know its own version? The Makefile reads a .gittag file. If it still holds an unexpanded git describe placeholder, the version comes from git describe --dirty, otherwise the value stored in the file is used, and that version is substituted into the source as the release_version. ### What is the difference between the make test and make ci targets? The test target runs the tests and skips tests whose dependencies are missing, while the ci target runs all tests and fails on those with missing dependencies. The ci target needs a full Tabby CAD Suite or OSS CAD Suite install. ## Sources - [Issues](https://github.com/YosysHQ/sby/issues) - [README](https://github.com/YosysHQ/sby/blob/main/README.md) - [YosysHQ/sby on GitHub](https://github.com/YosysHQ/sby) --- Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/yosyshq-sby