Installation guide#

This document will guide you through the process of installing sby.

CAD suite(s)#

Sby (SymbiYosys) is part of the Tabby CAD Suite and the OSS CAD Suite! The easiest way to use sby is to install the binary software suite, which contains all required dependencies, including all supported solvers.

Make sure to get a Tabby CAD Suite Evaluation License for extensive SystemVerilog Assertion (SVA) support, as well as industry-grade SystemVerilog and VHDL parsers!

For more information about the difference between Tabby CAD Suite and the OSS CAD Suite, please visit https://www.yosyshq.com/tabby-cad-datasheet.

Installing from source#

Follow the instructions below to install sby and its dependencies. Yosys and sby are non-optional. Boolector is recommended to install but not required. The other packages are only required for some engine configurations.

Prerequisites#

Installing prerequisites (this command is for Ubuntu 20.04):

sudo apt-get install build-essential clang bison flex \
                     libreadline-dev gawk tcl-dev libffi-dev git \
                     graphviz xdot pkg-config python3 zlib1g-dev

python3 -m pip install click

Required components#

Yosys, Yosys-SMTBMC and ABC#

https://yosyshq.net/yosys/

https://people.eecs.berkeley.edu/~alanmi/abc/

Note that this will install Yosys, Yosys-SMTBMC and ABC (as yosys-abc):

git clone https://github.com/YosysHQ/yosys
cd yosys
make -j$(nproc)
sudo make install

sby#

https://github.com/YosysHQ/sby

git clone https://github.com/YosysHQ/sby
cd sby
sudo make install

Yices 2#

http://yices.csl.sri.com/

git clone https://github.com/SRI-CSL/yices2.git yices2
cd yices2
autoconf
./configure
make -j$(nproc)
sudo make install

Optional components#

Additional solver engines can be installed as per their instructions, links are provided below.

Z3#

super_prove#

Avy#