Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Use furo-ys #276

Merged
merged 3 commits into from
Sep 27, 2024
Merged

Use furo-ys #276

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5426bee
Use furo-ys
KrystalDelusion May 9, 2024
a3844d4
Docs: Use sby lexer
KrystalDelusion Jun 10, 2024
0fab912
Docs: Use sby role shortcut
KrystalDelusion Jun 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
43 changes: 0 additions & 43 deletions docs/source/_templates/page.html
View file
Open in desktop

This file was deleted.

4 changes: 2 additions & 2 deletions docs/source/autotune.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ directory.

The ``divider.sby`` file contains the following ``[engines]`` section:

.. code-block:: text
.. code-block:: sby

[engines]
smtbmc
Expand All @@ -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
Expand Down
35 changes: 7 additions & 28 deletions docs/source/conf.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand All @@ -10,38 +12,15 @@

# 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)
2 changes: 1 addition & 1 deletion docs/source/quickstart.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
54 changes: 29 additions & 25 deletions docs/source/reference.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
Expand All @@ -45,7 +49,7 @@ tasks or task groups:
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.

.. code-block:: text
.. code-block:: sby

[options]
task_1_or_2:
Expand All @@ -59,7 +63,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 given task is active:

.. code-block:: text
.. code-block:: sby

[options]
~task3:
Expand All @@ -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
Expand Down Expand Up @@ -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
``<taskname>:`` or ``~<taskname>:`` tag.

The command ``sby --dumptasks <sby_file>`` prints the list of all tasks defined in
Expand All @@ -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:

========= ===========
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -436,7 +440,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
the source file name. For example:

.. code-block:: text
.. code-block:: sby

[files]
top.sv
Expand All @@ -447,10 +451,10 @@ File sections
-------------

File sections can be used to create additional files in ``<outdir>/src/`` from
the literal content of the ``[file <filename>]`` section ("here document"). For
example:
the literal content of the :sby:`[file <filename>]` section ("here document").
For example:

.. code-block:: text
.. code-block:: sby

[file params.vh]
`define RESET_LEN 42
Expand All @@ -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--
Expand Down
2 changes: 1 addition & 1 deletion docs/source/requirements.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
furo
furo-ys @ git+https://github.com/YosysHQ/furo-ys
sphinx-argparse
19 changes: 1 addition & 18 deletions docs/static/custom.css
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 */
Binary file removed docs/static/favico.png
View file
Open in desktop
Binary file not shown.
Binary file removed docs/static/logo.png
View file
Open in desktop
Binary file not shown.