From a3844d4a30539843d7f2b07fe742cde95f3b37da Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 10 Jun 2024 18:41:15 +1200 Subject: [PATCH] Docs: Use sby lexer --- docs/source/autotune.rst | 4 ++-- docs/source/conf.py | 6 ++++++ docs/source/quickstart.rst | 2 +- docs/source/reference.rst | 26 +++++++++++++------------- 4 files changed, 22 insertions(+), 16 deletions(-) diff --git a/docs/source/autotune.rst b/docs/source/autotune.rst index 1943218..5204a7f 100644 --- a/docs/source/autotune.rst +++ b/docs/source/autotune.rst @@ -29,7 +29,7 @@ directory. The ``divider.sby`` file contains the following ``[engines]`` section: -.. code-block:: text +.. code-block:: sby [engines] 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 the ``[engines]`` section of ``divider.sby`` to: -.. code-block:: text +.. code-block:: sby [engines] smtbmc bitwuzla -- --noincr diff --git a/docs/source/conf.py b/docs/source/conf.py index 68831f1..99813a2 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -2,6 +2,8 @@ import sys import os +from sphinx.application import Sphinx + sys.path.append(os.path.abspath(f"{__file__}/../../../sbysrc")) project = 'YosysHQ SBY' @@ -18,3 +20,7 @@ html_static_path = ['../static'] extensions = ['sphinx.ext.autosectionlabel'] extensions += ['sphinxarg.ext'] + +def setup(app: Sphinx) -> None: + from furo_ys.lexers.SBYLexer import SBYLexer + app.add_lexer("sby", SBYLexer) diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst index 604d04c..63e72de 100644 --- a/docs/source/quickstart.rst +++ b/docs/source/quickstart.rst @@ -215,7 +215,7 @@ Exercise Adjust the ``[script]`` section of ``fifo.sby`` so that it looks like the below. -.. code-block:: text +.. code-block:: sby [script] nofullskip: read -define NO_FULL_SKIP=1 diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 083c7f0..68da65d 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -13,7 +13,7 @@ Tasks section 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: -.. code-block:: text +.. code-block:: sby [tasks] 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 tasks or task groups: -.. code-block:: text +.. code-block:: sby [options] task_1_or_2: mode bmc @@ -45,7 +45,7 @@ tasks or task groups: If the tag ``:`` is used on a line by itself then the conditional string extends until the next conditional block or ``--`` on a line by itself. -.. code-block:: text +.. code-block:: sby [options] task_1_or_2: @@ -59,7 +59,7 @@ extends until the next conditional block or ``--`` on a line by itself. The tag ``~:`` can be used for a line or block that should not be used when the given task is active: -.. code-block:: text +.. code-block:: sby [options] ~task3: @@ -73,7 +73,7 @@ the given task is active: 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: -.. code-block:: text +.. code-block:: sby [tasks] prove_hAdX prove hostA deviceX @@ -208,7 +208,7 @@ usually followed by a solver name and solver options. Example: -.. code-block:: text +.. code-block:: sby [engines] 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 design file ``mytest.sv`` with the top-module ``mytest``: -.. code-block:: text +.. code-block:: sby [script] 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`` when Yosys is built with Verific support): -.. code-block:: text +.. code-block:: sby [script] 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`` when Yosys is not built with Verific support): -.. code-block:: text +.. code-block:: sby [script] read_verilog -sv mytest.sv @@ -422,7 +422,7 @@ Yosys script for files not listed in the files section.) For example: -.. code-block:: text +.. code-block:: sby [files] top.sv @@ -436,7 +436,7 @@ If the name of the file in ``/src/`` should be different from the basename of the specified file, then the new file name can be specified before the source file name. For example: -.. code-block:: text +.. code-block:: sby [files] top.sv @@ -450,7 +450,7 @@ File sections can be used to create additional files in ``/src/`` from the literal content of the ``[file ]`` section ("here document"). For example: -.. code-block:: text +.. code-block:: sby [file params.vh] `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 associated with the current task. -.. code-block:: text +.. code-block:: sby [tasks] --pycode-begin--