mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-22 21:05:30 +00:00
Code Activity

Add documentation for smtbmc engine --anybase option

Browse source
This commit is contained in:
George Rennie 2021-11-16 15:34:21 +00:00
parent 79634d5016
commit ba859012a9
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
docs/source/reference.rst
View file

@ -231,6 +231,14 @@ the following options:
+-----------------+---------------------------------------------------------+
| ``--progress`` | Enable Yosys-SMTBMC timer display. |
+-----------------+---------------------------------------------------------+
| ``--anybase`` | Generate an arbitrary basecase trace in ``prove`` mode, |
| | instead of one derived from the starting conditions. |
| | (This provides a weaker proof that there exists some |
| | basecase for which the assertions hold. |
| | This is powerful when combined with a separate proof |
| | that the assertions hold for ``depth`` cycles after |
| | reset). |
+-----------------+---------------------------------------------------------+
Any SMT2 solver that is compatible with ``yosys-smtbmc`` can be passed as
argument to the ``smtbmc`` engine. The solver options are passed to the solver