Update docs

diff --git a/docs/source/index.rst b/docs/source/index.rst
index fb5489c2434279e03f22fd38bacdb874c91f441b..b6de19a13e9c8df057980217b840617e8f842816 100644 (file)
--- a/docs/source/index.rst
+++ b/docs/source/index.rst
@@ -22,10 +22,3 @@ at the moment.)
    reference.rst
    license.rst
 
-
-Indices and tables
-==================
-
-* :ref:`genindex`
-* :ref:`search`
-

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 5ff0644ccdee774299861ce4a0c8d90abfd1cf63..cc2bf53529b0c30fd1db9ef1a0852642f66a1c12 100644 (file)
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -2,43 +2,58 @@
 Reference for .sby file format
 ==============================
 
-Yosys Script
-------------
-
-TBD
-
-File and files sections
------------------------
-
-TBD
-
-Modes, options, and engines
----------------------------
-
-TBD
-
-Options and engines for bounded model checks
---------------------------------------------
-
-TBD
-
-Options and engines for unbounded model checks
-----------------------------------------------
-
-TBD
-
-Options and engines for coverage analysis
------------------------------------------
-
-TBD
-
-Options and engines for liveness properties
--------------------------------------------
-
-TBD
-
-Options and engines for formal equivalence
-------------------------------------------
+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)
+``cover`` Generate set of shortest trace required to reach all cover() statements
+========= ===========
+
+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) |
++-------------+-----------+---------------------------------------------------------+
+| ``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``                                   |
++-------------+-----------+---------------------------------------------------------+
+
+Engines section
+---------------
+
+TBD
+
+Script section
+--------------
+
+TBD
+
+Files section
+-------------
 
 TBD