diff --git a/docs/source/_templates/page.html b/docs/source/_templates/page.html
deleted file mode 100644
index de334e7..0000000
--- a/docs/source/_templates/page.html
+++ /dev/null
@@ -1,43 +0,0 @@
-{#
-
-See https://github.com/pradyunsg/furo/blob/main/src/furo/theme/furo/page.html for the original
-block this is overwriting.
-
-The part that is customized is between the "begin of custom part" and "end of custom part"
-comments below. It uses the same styles as the existing right sidebar code.
-
-#}
-{% extends "furo/page.html" %}
-{% block right_sidebar %}
-
-{% endblock %}
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 e18817c..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'
@@ -10,38 +12,15 @@ copyright = '2023 YosysHQ GmbH'
# select HTML theme
-templates_path = ["_templates"]
-html_theme = "furo"
-html_logo = '../static/logo.png'
-html_favicon = '../static/favico.png'
+html_theme = "furo-ys"
html_css_files = ['custom.css']
# These folders are copied to the documentation's HTML output
html_static_path = ['../static']
-# code blocks style
-pygments_style = 'colorful'
-highlight_language = 'systemverilog'
-
-html_theme_options = {
- "sidebar_hide_name": True,
-
- "light_css_variables": {
- "color-brand-primary": "#d6368f",
- "color-brand-content": "#4b72b8",
- "color-api-name": "#8857a3",
- "color-api-pre-name": "#4b72b8",
- "color-link": "#8857a3",
- },
-
- "dark_css_variables": {
- "color-brand-primary": "#e488bb",
- "color-brand-content": "#98bdff",
- "color-api-name": "#8857a3",
- "color-api-pre-name": "#4b72b8",
- "color-link": "#be95d5",
- },
-}
-
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 61fd7a9..7b92d7c 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -1,19 +1,23 @@
+.. role:: sby(code)
+ :language: sby
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 for the most part irrelevant, but by convention the usual order is
-``[tasks]``, ``[options]``, ``[engines]``, ``[script]``, and ``[files]``.
+section header in square brackets. The order of sections in a ``.sby`` file is
+for the most part irrelevant, but by convention the usual order is
+:sby:`[tasks]`, :sby:`[options]`, :sby:`[engines]`, :sby:`[script]`, and
+:sby:`[files]`.
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:
+The optional :sby:`[tasks]` section can be used to configure multiple
+verification tasks in a single ``.sby`` file. Each line in the :sby:`[tasks]`
+section configures one task. For example:
-.. code-block:: text
+.. code-block:: sby
[tasks]
task1 task_1_or_2 task_1_or_3
@@ -30,12 +34,12 @@ calling ``sby`` on a ``.sby`` file:
sby example.sby task2
-If no task is specified then all tasks in the ``[tasks]`` section are run.
+If no task is specified then all tasks in the :sby:`[tasks]` section are run.
-After the ``[tasks]`` section individual lines can be specified for specific
+After the :sby:`[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 +49,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 +63,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 +77,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
@@ -101,7 +105,7 @@ combinations of some host implementations A and B and device implementations X a
deviceY: read -sv deviceY.v
...
-The ``[tasks]`` section must appear in the ``.sby`` file before the first
+The :sby:`[tasks]` section must appear in the ``.sby`` file before the first
``:`` or ``~:`` tag.
The command ``sby --dumptasks `` prints the list of all tasks defined in
@@ -110,7 +114,7 @@ a given ``.sby`` file.
Options section
---------------
-The ``[options]`` section contains lines with key-value pairs. The ``mode``
+The :sby:`[options]` section contains lines with key-value pairs. The ``mode``
option is mandatory. The possible values for the ``mode`` option are:
========= ===========
@@ -208,7 +212,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
@@ -374,11 +378,11 @@ other engines. This makes it easier to use the same models outside of sby.
Script section
--------------
-The ``[script]`` section contains the Yosys script that reads and elaborates
+The :sby:`[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 +391,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 +401,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 +426,7 @@ Yosys script for files not listed in the files section.)
For example:
-.. code-block:: text
+.. code-block:: sby
[files]
top.sv
@@ -436,7 +440,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
@@ -447,10 +451,10 @@ File sections
-------------
File sections can be used to create additional files in ``/src/`` from
-the literal content of the ``[file ]`` section ("here document"). For
-example:
+the literal content of the :sby:`[file ]` section ("here document").
+For example:
-.. code-block:: text
+.. code-block:: sby
[file params.vh]
`define RESET_LEN 42
@@ -465,7 +469,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--
diff --git a/docs/source/requirements.txt b/docs/source/requirements.txt
index 0e4756e..9b32c0a 100644
--- a/docs/source/requirements.txt
+++ b/docs/source/requirements.txt
@@ -1,2 +1,2 @@
-furo
+furo-ys @ git+https://github.com/YosysHQ/furo-ys
sphinx-argparse
diff --git a/docs/static/custom.css b/docs/static/custom.css
index b23ce2d..40a8c17 100644
--- a/docs/static/custom.css
+++ b/docs/static/custom.css
@@ -1,18 +1 @@
-/* Don't hide the right sidebar as we're placing our fixed links there */
-aside.no-toc {
- display: block !important;
-}
-
-/* Colorful headings */
-h1 {
- color: var(--color-brand-primary);
-}
-
-h2, h3, h4, h5, h6 {
- color: var(--color-brand-content);
-}
-
-/* Use a different color for external links */
-a.external {
- color: var(--color-brand-primary) !important;
-}
+/* empty */
diff --git a/docs/static/favico.png b/docs/static/favico.png
deleted file mode 100644
index 3f5afba..0000000
Binary files a/docs/static/favico.png and /dev/null differ
diff --git a/docs/static/logo.png b/docs/static/logo.png
deleted file mode 100644
index 8e5a507..0000000
Binary files a/docs/static/logo.png and /dev/null differ