3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 14:04:07 +00:00
sby/docs/source/reference.rst
2017-07-01 18:33:36 +02:00

82 lines
4.4 KiB
ReStructuredText

Reference for .sby file format
==============================
A ``.sby`` file consists of sections. Each section start with a single-line
section header in square brackets. The order of sections in a ``.sby`` file
is irrelevant, but by convention the usual order is ``[options]``,
``[engines]``, ``[script]``, and ``[files]``.
Options section
---------------
The ``[options]`` section contains lines with key-value pairs. The ``mode``
option is mandatory. The possible values for the ``mode`` option are:
========= ===========
Mode Description
========= ===========
``bmc`` Bounded model check to verify safety properties (``assert(...)`` statements)
``prove`` Unbounded model check to verify safety properties (``assert(...)`` statements)
``live`` Unbounded model check to verify liveness properties (``assert(s_eventually ...)`` statements)
``cover`` Generate set of shortest traces required to reach all cover() statements
``equiv`` Formal equivalence checking (usually to verify pre- and post-synthesis equivalence)
``synth`` Reactive Synthesis (synthesis of circuit from safety properties)
========= ===========
All other options have default values and thus are optional. The available
options are:
+-------------+------------+---------------------------------------------------------+
| Option | Modes | Description |
+=============+============+=========================================================+
| ``expect`` | All | Expected result as comma-separated list of the tokens |
| | | ``pass``, ``fail``, ``unknown``, ``error``, and |
| | | ``timeout``. Unexpected results yield a nonzero return |
| | | code . Default: ``pass`` |
+-------------+------------+---------------------------------------------------------+
| ``timeout`` | All | Timeout in seconds. Default: ``none`` (i.e. no timeout) |
+-------------+------------+---------------------------------------------------------+
| ``wait`` | All | Instead of terminating when the first engine returns, |
| | | wait for all engines to return and check for |
| | | consistency. Values: ``on``, ``off``. Default: ``off`` |
+-------------+------------+---------------------------------------------------------+
| ``aigsmt`` | All | Which SMT2 solver to use for converting AIGER witnesses |
| | | to counter example traces. Use ``none`` to disable |
| | | conversion of AIGER witnesses. Default: ``yices`` |
+-------------+------------+---------------------------------------------------------+
| ``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. |
| | ``cover`` | Default: None |
+-------------+------------+---------------------------------------------------------+
| ``depth`` | ``bmc``, | Depth of the bounded model check. Only the specified |
| | ``cover`` | number of cycles are considered. Default: ``20`` |
| +------------+---------------------------------------------------------+
| | ``prove`` | Depth for the k-induction performed by the ``smtbmc`` |
| | | engine. Other engines ignore this option in ``prove`` |
| | | mode. Default: ``20`` |
+-------------+------------+---------------------------------------------------------+
| ``append`` | ``bmc``, | When generating a counter-example trace, add the |
| | ``prove``, | specified number of cycles at the end of the trace. |
| | ``cover`` | Default: ``0`` |
+-------------+------------+---------------------------------------------------------+
Engines section
---------------
TBD
Script section
--------------
TBD
Files section
-------------
TBD