mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-06 14:24:08 +00:00
Code Activity

Merge pull request #228 from jix/docs-updates

Browse source 
Docs updates
This commit is contained in:
Jannis Harder 2023-02-06 22:10:38 +01:00 committed by GitHub
parent 7d3f0d50a5 7a3b88ca67
commit 37d1234e38
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 79 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
docs/source/install.rst
View file

@ -102,6 +102,20 @@ To use the ``btor`` engine you will need to install btor2tools from
`commit c35cf1c <https://github.com/Boolector/btor2tools/commit/c35cf1c>`_ or `commit c35cf1c <https://github.com/Boolector/btor2tools/commit/c35cf1c>`_ or
newer. newer.
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
Optional components Optional components
------------------- -------------------
Additional solver engines can be installed as per their instructions, links are Additional solver engines can be installed as per their instructions, links are
@ -112,12 +126,6 @@ Z3
https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3
Yices 2
^^^^^^^
http://yices.csl.sri.com/
https://github.com/SRI-CSL/yices2
super_prove super_prove
^^^^^^^^^^^ ^^^^^^^^^^^
https://github.com/sterin/super-prove-build https://github.com/sterin/super-prove-build

117
docs/source/reference.rst
View file

@ -129,58 +129,71 @@ Mode Description
All other options have default values and thus are optional. The available All other options have default values and thus are optional. The available
options are: options are:
+------------------+------------+---------------------------------------------------------+ +-------------------+------------+---------------------------------------------------------+
| Option | Modes | Description | | Option | Modes | Description |
+==================+============+=========================================================+ +===================+============+=========================================================+
| ``expect`` | All | Expected result as comma-separated list of the tokens | | ``expect`` | All | Expected result as comma-separated list of the tokens |
| | | ``pass``, ``fail``, ``unknown``, ``error``, and | | | | ``pass``, ``fail``, ``unknown``, ``error``, and |
| | | ``timeout``. Unexpected results yield a nonzero return | | | | ``timeout``. Unexpected results yield a nonzero return |
| | | code . Default: ``pass`` | | | | code . Default: ``pass`` |
+------------------+------------+---------------------------------------------------------+ +-------------------+------------+---------------------------------------------------------+
| ``timeout`` | All | Timeout in seconds. Default: ``none`` (i.e. no timeout) | | ``timeout`` | All | Timeout in seconds. Default: ``none`` (i.e. no timeout) |
+------------------+------------+---------------------------------------------------------+ +-------------------+------------+---------------------------------------------------------+
| ``multiclock`` | All | Create a model with multiple clocks and/or asynchronous | | ``multiclock`` | All | Create a model with multiple clocks and/or asynchronous |
| | | logic. Values: ``on``, ``off``. Default: ``off`` | | | | logic. Values: ``on``, ``off``. Default: ``off`` |
+------------------+------------+---------------------------------------------------------+ +-------------------+------------+---------------------------------------------------------+
| ``wait`` | All | Instead of terminating when the first engine returns, | | ``wait`` | All | Instead of terminating when the first engine returns, |
| | | wait for all engines to return and check for | | | | wait for all engines to return and check for |
| | | consistency. Values: ``on``, ``off``. Default: ``off`` | | | | consistency. Values: ``on``, ``off``. Default: ``off`` |
+------------------+------------+---------------------------------------------------------+ +-------------------+------------+---------------------------------------------------------+
| ``vcd`` | All | Write VCD traces for counter-example or cover traces. | | ``vcd`` | All | Write VCD traces for counter-example or cover traces. |
| | | Values: ``on``, ``off``. Default: ``on`` | | | | Values: ``on``, ``off``. Default: ``on`` |
+------------------+------------+---------------------------------------------------------+ +-------------------+------------+---------------------------------------------------------+
| ``aigsmt`` | All | Which SMT2 solver to use for converting AIGER witnesses | | ``vcd_sim`` | All | When generating VCD traces, use Yosys's ``sim`` |
| | | to counter example traces. Use ``none`` to disable | | | | command. Replaces the engine native VCD output. |
| | | conversion of AIGER witnesses. Default: ``yices`` | | | | Values: ``on``, ``off``. Default: ``off`` |
+------------------+------------+---------------------------------------------------------+ +-------------------+------------+---------------------------------------------------------+
| ``tbtop`` | All | The top module for generated Verilog test benches, as | | ``fst`` | All | Generate FST traces using Yosys's sim command. |
| | | hierarchical path relative to the design top module. | | | | Values: ``on``, ``off``. Default: ``off`` |
+------------------+------------+---------------------------------------------------------+ +-------------------+------------+---------------------------------------------------------+
| ``make_model`` | All | Force generation of the named formal models. Takes a | | ``aigsmt`` | All | Which SMT2 solver to use for converting AIGER witnesses |
| | | comma-separated list of model names. For a model | | | | to counter example traces. Use ``none`` to disable |
| | | ``<name>`` this will generate the | | | | conversion of AIGER witnesses. Default: ``yices`` |
| | | ``model/design_<name>.*`` files within the working | +-------------------+------------+---------------------------------------------------------+
| | | directory, even when not required to run the task. | | ``tbtop`` | All | The top module for generated Verilog test benches, as |
+------------------+------------+---------------------------------------------------------+ | | | hierarchical path relative to the design top module. |
| ``smtc`` | ``bmc``, | Pass this ``.smtc`` file to the smtbmc engine. All | +-------------------+------------+---------------------------------------------------------+
| | ``prove``, | other engines are disabled when this option is used. | | ``make_model`` | All | Force generation of the named formal models. Takes a |
| | ``cover`` | Default: None | | | | comma-separated list of model names. For a model |
+------------------+------------+---------------------------------------------------------+ | | | ``<name>`` this will generate the |
| ``depth`` | ``bmc``, | Depth of the bounded model check. Only the specified | | | | ``model/design_<name>.*`` files within the working |
| | ``cover`` | number of cycles are considered. Default: ``20`` | | | | directory, even when not required to run the task. |
| +------------+---------------------------------------------------------+ +-------------------+------------+---------------------------------------------------------+
| | ``prove`` | Depth for the k-induction performed by the ``smtbmc`` | | ``smtc`` | ``bmc``, | Pass this ``.smtc`` file to the smtbmc engine. All |
| | | engine. Other engines ignore this option in ``prove`` | | | ``prove``, | other engines are disabled when this option is used. |
| | | mode. Default: ``20`` | | | ``cover`` | Default: None |
+------------------+------------+---------------------------------------------------------+ +-------------------+------------+---------------------------------------------------------+
| ``skip`` | ``bmc``, | Skip the specified number of time steps. Only valid | | ``depth`` | ``bmc``, | Depth of the bounded model check. Only the specified |
| | ``cover`` | with smtbmc engine. All other engines are disabled when | | | ``cover`` | number of cycles are considered. Default: ``20`` |
| | | this option is used. Default: None | | +------------+---------------------------------------------------------+
+------------------+------------+---------------------------------------------------------+ | | ``prove`` | Depth for the k-induction performed by the ``smtbmc`` |
| ``append`` | ``bmc``, | When generating a counter-example trace, add the | | | | engine. Other engines ignore this option in ``prove`` |
| | ``prove``, | specified number of cycles at the end of the trace. | | | | mode. Default: ``20`` |
| | ``cover`` | Default: ``0`` | +-------------------+------------+---------------------------------------------------------+
+------------------+------------+---------------------------------------------------------+ | ``skip`` | ``bmc``, | Skip the specified number of time steps. Only valid |
| | ``cover`` | with smtbmc engine. All other engines are disabled when |
| | | this option is used. Default: None |
+-------------------+------------+---------------------------------------------------------+
| ``append`` | ``bmc``, | When generating a counter-example trace, add the |
| | ``prove``, | specified number of cycles at the end of the trace. |
| | ``cover`` | Default: ``0`` |
+-------------------+------------+---------------------------------------------------------+
| ``append_assume`` | ``bmc``, | Uphold assumptions when appending cycles at the end of |
| | ``prove``, | the trace. Depending on the engine and options used |
| | ``cover`` | this may be implicitly on or not supported (as |
| | | indicated in SBY's log output). |
| | | Values: ``on``, ``off``. Default: ``off`` |
+-------------------+------------+---------------------------------------------------------+
Engines section Engines section
--------------- ---------------