docs/source/install.rst

   1 Installing
   2 ==========
   3
   4 Follow the instructions below to install SymbiYosys and its dependencies.
   5 Yosys, SymbiYosys, and Z3 are non-optional. The other packages are only
   6 required for some engine configurations.
   7
   8 Prerequisites
   9 -------------
  10
  11 Installing prerequisites (this command is for Ubuntu 16.04):
  12
  13 .. code-block:: text
  14
  15    sudo apt-get install build-essential clang bison flex libreadline-dev \
  16                         gawk tcl-dev libffi-dev git mercurial graphviz   \
  17                         xdot pkg-config python python3 libftdi-dev gperf \
  18                         libboost-program-options-dev autoconf libgmp-dev \
  19                         cmake curl
  20
  21 Yosys, Yosys-SMTBMC and ABC
  22 ---------------------------
  23
  24 https://yosyshq.net/yosys/
  25
  26 https://people.eecs.berkeley.edu/~alanmi/abc/
  27
  28 Next install Yosys, Yosys-SMTBMC and ABC (``yosys-abc``):
  29
  30 .. code-block:: text
  31
  32    git clone https://github.com/YosysHQ/yosys.git yosys
  33    cd yosys
  34    make -j$(nproc)
  35    sudo make install
  36
  37 SymbiYosys
  38 ----------
  39
  40 https://github.com/YosysHQ/SymbiYosys
  41
  42 .. code-block:: text
  43
  44    git clone https://github.com/YosysHQ/SymbiYosys.git SymbiYosys
  45    cd SymbiYosys
  46    sudo make install
  47
  48 Yices 2
  49 -------
  50
  51 http://yices.csl.sri.com/
  52
  53 .. code-block:: text
  54
  55    git clone https://github.com/SRI-CSL/yices2.git yices2
  56    cd yices2
  57    autoconf
  58    ./configure
  59    make -j$(nproc)
  60    sudo make install
  61
  62 Z3
  63 --
  64
  65 https://github.com/Z3Prover/z3/wiki
  66
  67 .. code-block:: text
  68
  69    git clone https://github.com/Z3Prover/z3.git z3
  70    cd z3
  71    python scripts/mk_make.py
  72    cd build
  73    make -j$(nproc)
  74    sudo make install
  75
  76 super_prove
  77 -----------
  78
  79 https://github.com/sterin/super-prove-build
  80
  81 .. code-block:: text
  82
  83    sudo apt-get install cmake ninja-build g++ python-dev python-setuptools \
  84                         python-pip git
  85    git clone --recursive https://github.com/sterin/super-prove-build
  86    cd super-prove-build
  87    mkdir build
  88    cd build
  89    cmake -DCMAKE_BUILD_TYPE=Release -G Ninja ..
  90    ninja
  91    ninja package
  92
  93 This creates a .tar.gz archive for the target system. Extract it to
  94 ``/usr/local/super_prove``
  95
  96 .. code-block:: text
  97
  98    sudo tar -C /usr/local -x super_prove-X-Y-Release.tar.gz
  99
 100 Then create a wrapper script ``/usr/local/bin/suprove`` with the following contents:
 101
 102 .. code-block:: text
 103
 104    #!/bin/bash
 105    tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi
 106    exec /usr/local/super_prove/bin/${tool}.sh "$@"
 107
 108 And make this wrapper script executable:
 109
 110 .. code-block:: text
 111
 112    sudo chmod +x /usr/local/bin/suprove
 113
 114 Avy
 115 ---
 116
 117 https://arieg.bitbucket.io/avy/
 118
 119 .. code-block:: text
 120
 121    git clone https://bitbucket.org/arieg/extavy.git
 122    cd extavy
 123    git submodule update --init
 124    mkdir build; cd build
 125    cmake -DCMAKE_BUILD_TYPE=Release ..
 126    make -j$(nproc)
 127    sudo cp avy/src/{avy,avybmc} /usr/local/bin/
 128
 129 Boolector
 130 ---------
 131
 132 http://fmv.jku.at/boolector/
 133
 134 .. code-block:: text
 135
 136    git clone https://github.com/boolector/boolector
 137    cd boolector
 138    ./contrib/setup-btor2tools.sh
 139    ./contrib/setup-lingeling.sh
 140    ./configure.sh
 141    make -C build -j$(nproc)
 142    sudo cp build/bin/{boolector,btor*} /usr/local/bin/
 143    sudo cp deps/btor2tools/bin/btorsim /usr/local/bin/
 144
 145 To use the ``btor`` engine you additionally need a newer version of btorsim than the boolector setup script builds:
 146
 147 .. code-block:: text
 148
 149    git clone https://github.com/boolector/btor2tools
 150    ./configure.sh
 151    cmake .
 152    make install