3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 08:28:16 +00:00

Docs: Use sby lexer

This commit is contained in:
Krystine Sherwin 2024-06-10 18:41:15 +12:00
parent 5426bee107
commit a3844d4a30
No known key found for this signature in database
4 changed files with 22 additions and 16 deletions

View file

@ -29,7 +29,7 @@ directory.
The ``divider.sby`` file contains the following ``[engines]`` section: The ``divider.sby`` file contains the following ``[engines]`` section:
.. code-block:: text .. code-block:: sby
[engines] [engines]
smtbmc smtbmc
@ -51,7 +51,7 @@ This tells us that for the ``medium`` task, the best engine choice (#1) is
``smtbmc bitwuzla -- --noincr``. To use this engine by default we can change ``smtbmc bitwuzla -- --noincr``. To use this engine by default we can change
the ``[engines]`` section of ``divider.sby`` to: the ``[engines]`` section of ``divider.sby`` to:
.. code-block:: text .. code-block:: sby
[engines] [engines]
smtbmc bitwuzla -- --noincr smtbmc bitwuzla -- --noincr

View file

@ -2,6 +2,8 @@
import sys import sys
import os import os
from sphinx.application import Sphinx
sys.path.append(os.path.abspath(f"{__file__}/../../../sbysrc")) sys.path.append(os.path.abspath(f"{__file__}/../../../sbysrc"))
project = 'YosysHQ SBY' project = 'YosysHQ SBY'
@ -18,3 +20,7 @@ html_static_path = ['../static']
extensions = ['sphinx.ext.autosectionlabel'] extensions = ['sphinx.ext.autosectionlabel']
extensions += ['sphinxarg.ext'] extensions += ['sphinxarg.ext']
def setup(app: Sphinx) -> None:
from furo_ys.lexers.SBYLexer import SBYLexer
app.add_lexer("sby", SBYLexer)

View file

@ -215,7 +215,7 @@ Exercise
Adjust the ``[script]`` section of ``fifo.sby`` so that it looks like the below. Adjust the ``[script]`` section of ``fifo.sby`` so that it looks like the below.
.. code-block:: text .. code-block:: sby
[script] [script]
nofullskip: read -define NO_FULL_SKIP=1 nofullskip: read -define NO_FULL_SKIP=1

View file

@ -13,7 +13,7 @@ Tasks section
The optional ``[tasks]`` section can be used to configure multiple verification tasks in The optional ``[tasks]`` section can be used to configure multiple verification tasks in
a single ``.sby`` file. Each line in the ``[tasks]`` section configures one task. For example: a single ``.sby`` file. Each line in the ``[tasks]`` section configures one task. For example:
.. code-block:: text .. code-block:: sby
[tasks] [tasks]
task1 task_1_or_2 task_1_or_3 task1 task_1_or_2 task_1_or_3
@ -35,7 +35,7 @@ If no task is specified then all tasks in the ``[tasks]`` section are run.
After the ``[tasks]`` section individual lines can be specified for specific After the ``[tasks]`` section individual lines can be specified for specific
tasks or task groups: tasks or task groups:
.. code-block:: text .. code-block:: sby
[options] [options]
task_1_or_2: mode bmc task_1_or_2: mode bmc
@ -45,7 +45,7 @@ tasks or task groups:
If the tag ``<taskname>:`` is used on a line by itself then the conditional string If the tag ``<taskname>:`` is used on a line by itself then the conditional string
extends until the next conditional block or ``--`` on a line by itself. extends until the next conditional block or ``--`` on a line by itself.
.. code-block:: text .. code-block:: sby
[options] [options]
task_1_or_2: task_1_or_2:
@ -59,7 +59,7 @@ extends until the next conditional block or ``--`` on a line by itself.
The tag ``~<taskname>:`` can be used for a line or block that should not be used when The tag ``~<taskname>:`` can be used for a line or block that should not be used when
the given task is active: the given task is active:
.. code-block:: text .. code-block:: sby
[options] [options]
~task3: ~task3:
@ -73,7 +73,7 @@ the given task is active:
The following example demonstrates how to configure safety and liveness checks for all The following example demonstrates how to configure safety and liveness checks for all
combinations of some host implementations A and B and device implementations X and Y: combinations of some host implementations A and B and device implementations X and Y:
.. code-block:: text .. code-block:: sby
[tasks] [tasks]
prove_hAdX prove hostA deviceX prove_hAdX prove hostA deviceX
@ -208,7 +208,7 @@ usually followed by a solver name and solver options.
Example: Example:
.. code-block:: text .. code-block:: sby
[engines] [engines]
smtbmc --syn --nopresat z3 rewriter.cache_all=true opt.enable_sat=true smtbmc --syn --nopresat z3 rewriter.cache_all=true opt.enable_sat=true
@ -378,7 +378,7 @@ The ``[script]`` section contains the Yosys script that reads and elaborates
the design under test. For example, for a simple project contained in a single the design under test. For example, for a simple project contained in a single
design file ``mytest.sv`` with the top-module ``mytest``: design file ``mytest.sv`` with the top-module ``mytest``:
.. code-block:: text .. code-block:: sby
[script] [script]
read -sv mytest.sv read -sv mytest.sv
@ -387,7 +387,7 @@ design file ``mytest.sv`` with the top-module ``mytest``:
Or explicitly using the Verific SystemVerilog parser (default for ``read -sv`` Or explicitly using the Verific SystemVerilog parser (default for ``read -sv``
when Yosys is built with Verific support): when Yosys is built with Verific support):
.. code-block:: text .. code-block:: sby
[script] [script]
verific -sv mytest.sv verific -sv mytest.sv
@ -397,7 +397,7 @@ when Yosys is built with Verific support):
Or explicitly using the native Yosys Verilog parser (default for ``read -sv`` Or explicitly using the native Yosys Verilog parser (default for ``read -sv``
when Yosys is not built with Verific support): when Yosys is not built with Verific support):
.. code-block:: text .. code-block:: sby
[script] [script]
read_verilog -sv mytest.sv read_verilog -sv mytest.sv
@ -422,7 +422,7 @@ Yosys script for files not listed in the files section.)
For example: For example:
.. code-block:: text .. code-block:: sby
[files] [files]
top.sv top.sv
@ -436,7 +436,7 @@ If the name of the file in ``<outdir>/src/`` should be different from the
basename of the specified file, then the new file name can be specified before basename of the specified file, then the new file name can be specified before
the source file name. For example: the source file name. For example:
.. code-block:: text .. code-block:: sby
[files] [files]
top.sv top.sv
@ -450,7 +450,7 @@ File sections can be used to create additional files in ``<outdir>/src/`` from
the literal content of the ``[file <filename>]`` section ("here document"). For the literal content of the ``[file <filename>]`` section ("here document"). For
example: example:
.. code-block:: text .. code-block:: sby
[file params.vh] [file params.vh]
`define RESET_LEN 42 `define RESET_LEN 42
@ -465,7 +465,7 @@ file lines from the python code. The variable ``task`` contains the current task
if any, and ``None`` otherwise. The variable ``tags`` contains a set of all tags if any, and ``None`` otherwise. The variable ``tags`` contains a set of all tags
associated with the current task. associated with the current task.
.. code-block:: text .. code-block:: sby
[tasks] [tasks]
--pycode-begin-- --pycode-begin--