From: Clifford Wolf Date: Mon, 6 Feb 2017 16:49:20 +0000 (+0100) Subject: Update docs X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=24e19e3cda1d83ba7ea14058135a0d62f00e68ca;p=SymbiYosys.git Update docs --- diff --git a/docs/source/index.rst b/docs/source/index.rst index fb5489c..b6de19a 100644 --- 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 5ff0644..cc2bf53 100644 --- 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