mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 16:28:17 +00:00
Code Activity

Update quickstart.rst

Browse source
This commit is contained in:
Clifford Wolf 2017-09-14 03:29:12 +02:00
parent 68d90a5510
commit 3f1cbb0706
1 changed files with 27 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
docs/source/quickstart.rst
View file

@ -26,6 +26,10 @@ Installing prerequisites (this command is for Ubuntu 16.04):
Yosys, Yosys-SMTBMC and ABC 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``): Next install Yosys, Yosys-SMTBMC and ABC (``yosys-abc``):
.. code-block:: text .. code-block:: text
@ -38,6 +42,8 @@ Next install Yosys, Yosys-SMTBMC and ABC (``yosys-abc``):
SymbiYosys SymbiYosys
~~~~~~~~~~ ~~~~~~~~~~
https://github.com/cliffordwolf/SymbiYosys
.. code-block:: text .. code-block:: text
git clone https://github.com/cliffordwolf/SymbiYosys.git SymbiYosys git clone https://github.com/cliffordwolf/SymbiYosys.git SymbiYosys
@ -47,6 +53,8 @@ SymbiYosys
Yices 2 Yices 2
~~~~~~~ ~~~~~~~
http://yices.csl.sri.com/
.. code-block:: text .. code-block:: text
git clone https://github.com/SRI-CSL/yices2.git yices2 git clone https://github.com/SRI-CSL/yices2.git yices2
@ -59,6 +67,8 @@ Yices 2
Z3 Z3
~~ ~~
https://github.com/Z3Prover/z3/wiki
.. code-block:: text .. code-block:: text
git clone https://github.com/Z3Prover/z3.git z3 git clone https://github.com/Z3Prover/z3.git z3
@ -71,6 +81,8 @@ Z3
super_prove 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/ Download the right binary .tar.gz for your system from http://downloads.bvsrc.org/super_prove/
and extract it to ``/usr/local/super_prove``. and extract it to ``/usr/local/super_prove``.
@ -85,6 +97,8 @@ Then create a wrapper script ``/usr/local/bin/suprove`` with the following conte
Avy Avy
~~~ ~~~
https://arieg.bitbucket.io/avy/
.. code-block:: text .. code-block:: text
git clone https://bitbucket.org/arieg/extavy.git git clone https://bitbucket.org/arieg/extavy.git
@ -95,13 +109,25 @@ Avy
make -j$(nproc) make -j$(nproc)
sudo cp avy/src/{avy,avybmc} /usr/local/bin/ sudo cp avy/src/{avy,avybmc} /usr/local/bin/
Boolector
~~~~~~~~~
http://fmv.jku.at/boolector/
.. code-block:: text
wget http://fmv.jku.at/boolector/boolector-2.4.1-with-lingeling-bbc.tar.bz2
tar xvjf boolector-2.4.1-with-lingeling-bbc.tar.bz2
cd boolector-2.4.1-with-lingeling-bbc/
make
sudo cp boolector/bin/boolector /usr/local/bin/boolector
Other packages Other packages
~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~
Until I find the time to write install guides for the following packages, this Until I find the time to write install guides for the following packages, this
links must suffice: links must suffice:
* Boolector: http://fmv.jku.at/boolector/
* AIGER: http://fmv.jku.at/aiger/ * AIGER: http://fmv.jku.at/aiger/
First step: A simple BMC example First step: A simple BMC example