From 091222b87febb10fad87fcbe98a57599a54c5fd3 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 23 Oct 2020 14:03:55 +0200 Subject: [PATCH] Extract installation procedure to separate file --- docs/source/index.rst | 1 + docs/source/install.rst | 122 +++++++++++++++++++++++++++++++++++++ docs/source/quickstart.rst | 122 ------------------------------------- 3 files changed, 123 insertions(+), 122 deletions(-) create mode 100644 docs/source/install.rst diff --git a/docs/source/index.rst b/docs/source/index.rst index 825cd85..0527fb4 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -19,6 +19,7 @@ at the moment.) .. toctree:: :maxdepth: 3 + install.rst quickstart.rst reference.rst verilog.rst diff --git a/docs/source/install.rst b/docs/source/install.rst new file mode 100644 index 0000000..db8ba14 --- /dev/null +++ b/docs/source/install.rst @@ -0,0 +1,122 @@ +Installing +========== + +Follow the instructions below to install SymbiYosys and its dependencies. +Yosys, SymbiYosys, and Z3 are non-optional. The other packages are only +required for some engine configurations. + +Prerequisites +------------- + +Installing prerequisites (this command is for Ubuntu 16.04): + +.. code-block:: text + + sudo apt-get install build-essential clang bison flex libreadline-dev \ + gawk tcl-dev libffi-dev git mercurial graphviz \ + xdot pkg-config python python3 libftdi-dev gperf \ + libboost-program-options-dev autoconf libgmp-dev \ + cmake + +Yosys, Yosys-SMTBMC and ABC +--------------------------- + +http://www.clifford.at/yosys/ + +https://people.eecs.berkeley.edu/~alanmi/abc/ + +Next install Yosys, Yosys-SMTBMC and ABC (``yosys-abc``): + +.. code-block:: text + + git clone https://github.com/YosysHQ/yosys.git yosys + cd yosys + make -j$(nproc) + sudo make install + +SymbiYosys +---------- + +https://github.com/YosysHQ/SymbiYosys + +.. code-block:: text + + git clone https://github.com/YosysHQ/SymbiYosys.git SymbiYosys + cd SymbiYosys + sudo make install + +Yices 2 +------- + +http://yices.csl.sri.com/ + +.. code-block:: text + + git clone https://github.com/SRI-CSL/yices2.git yices2 + cd yices2 + autoconf + ./configure + make -j$(nproc) + sudo make install + +Z3 +-- + +https://github.com/Z3Prover/z3/wiki + +.. code-block:: text + + git clone https://github.com/Z3Prover/z3.git z3 + cd z3 + python scripts/mk_make.py + cd build + make -j$(nproc) + sudo make install + +super_prove +----------- + +https://bitbucket.org/sterin/super_prove_build + +Download the right binary .tar.gz for your system from http://downloads.bvsrc.org/super_prove/ +and extract it to ``/usr/local/super_prove``. + +Then create a wrapper script ``/usr/local/bin/suprove`` with the following contents: + +.. code-block:: text + + #!/bin/bash + tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi + exec /usr/local/super_prove/bin/${tool}.sh "$@" + +Avy +--- + +https://arieg.bitbucket.io/avy/ + +.. code-block:: text + + git clone https://bitbucket.org/arieg/extavy.git + cd extavy + git submodule update --init + mkdir build; cd build + cmake -DCMAKE_BUILD_TYPE=Release .. + make -j$(nproc) + sudo cp avy/src/{avy,avybmc} /usr/local/bin/ + +Boolector +--------- + +http://fmv.jku.at/boolector/ + +.. code-block:: text + + git clone https://github.com/boolector/boolector + cd boolector + ./contrib/setup-btor2tools.sh + ./contrib/setup-lingeling.sh + ./configure.sh + make -C build -j$(nproc) + sudo cp build/bin/{boolector,btor*} /usr/local/bin/ + sudo cp deps/btor2tools/bin/btorsim /usr/local/bin/ + diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst index 517f464..1e66039 100644 --- a/docs/source/quickstart.rst +++ b/docs/source/quickstart.rst @@ -5,128 +5,6 @@ Getting Started The example files used in this chapter can be downloaded from `here `_. -Installing ----------- - -Follow the instructions below to install SymbiYosys and its dependencies. -Yosys, SymbiYosys, and Z3 are non-optional. The other packages are only -required for some engine configurations. - -Prerequisites -~~~~~~~~~~~~~ - -Installing prerequisites (this command is for Ubuntu 16.04): - -.. code-block:: text - - sudo apt-get install build-essential clang bison flex libreadline-dev \ - gawk tcl-dev libffi-dev git mercurial graphviz \ - xdot pkg-config python python3 libftdi-dev gperf \ - libboost-program-options-dev autoconf libgmp-dev \ - cmake - -Yosys, Yosys-SMTBMC and ABC -~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -http://www.clifford.at/yosys/ - -https://people.eecs.berkeley.edu/~alanmi/abc/ - -Next install Yosys, Yosys-SMTBMC and ABC (``yosys-abc``): - -.. code-block:: text - - git clone https://github.com/YosysHQ/yosys.git yosys - cd yosys - make -j$(nproc) - sudo make install - -SymbiYosys -~~~~~~~~~~ - -https://github.com/YosysHQ/SymbiYosys - -.. code-block:: text - - git clone https://github.com/YosysHQ/SymbiYosys.git SymbiYosys - cd SymbiYosys - sudo make install - -Yices 2 -~~~~~~~ - -http://yices.csl.sri.com/ - -.. code-block:: text - - git clone https://github.com/SRI-CSL/yices2.git yices2 - cd yices2 - autoconf - ./configure - make -j$(nproc) - sudo make install - -Z3 -~~ - -https://github.com/Z3Prover/z3/wiki - -.. code-block:: text - - git clone https://github.com/Z3Prover/z3.git z3 - cd z3 - python scripts/mk_make.py - cd build - make -j$(nproc) - sudo make install - -super_prove -~~~~~~~~~~~ - -https://bitbucket.org/sterin/super_prove_build - -Download the right binary .tar.gz for your system from http://downloads.bvsrc.org/super_prove/ -and extract it to ``/usr/local/super_prove``. - -Then create a wrapper script ``/usr/local/bin/suprove`` with the following contents: - -.. code-block:: text - - #!/bin/bash - tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi - exec /usr/local/super_prove/bin/${tool}.sh "$@" - -Avy -~~~ - -https://arieg.bitbucket.io/avy/ - -.. code-block:: text - - git clone https://bitbucket.org/arieg/extavy.git - cd extavy - git submodule update --init - mkdir build; cd build - cmake -DCMAKE_BUILD_TYPE=Release .. - make -j$(nproc) - sudo cp avy/src/{avy,avybmc} /usr/local/bin/ - -Boolector -~~~~~~~~~ - -http://fmv.jku.at/boolector/ - -.. code-block:: text - - git clone https://github.com/boolector/boolector - cd boolector - ./contrib/setup-btor2tools.sh - ./contrib/setup-lingeling.sh - ./configure.sh - make -C build -j$(nproc) - sudo cp build/bin/{boolector,btor*} /usr/local/bin/ - sudo cp deps/btor2tools/bin/btorsim /usr/local/bin/ - First step: A simple BMC example -------------------------------- -- 2.30.2