mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-06-06 09:00:54 +00:00
Code Activity

WIP docs

Browse source
This commit is contained in:
Krystine Sherwin 2026-06-02 15:45:00 +12:00
parent 693d5a7eb0
commit 776995c74d
No known key found for this signature in database
8 changed files with 227 additions and 182 deletions
Download patch file Download diff file Expand all files Collapse all files

102
docs/source/yosys_internals/extending_yosys/build_verific.rst
View file

@ -39,36 +39,36 @@ incorrect results.
Compile options
---------------
To enable Verific support ``ENABLE_VERIFIC`` has to be set to ``1`` and
``VERIFIC_DIR`` needs to point to the location where the library is located.
To enable Verific support, set the :makevar:`YOSYS_VERIFIC_DIR` CMake variable
to point to the location where the library is located, e.g.
============== ========================== ===============================
Parameter Default Description
============== ========================== ===============================
ENABLE_VERIFIC 0 Enable compilation with Verific
VERIFIC_DIR /usr/local/src/verific_lib Library and headers location
============== ========================== ===============================
.. code-block:: console
Since there are multiple Verific library builds and they can have different
features, there are compile options to select them.
cmake -B build . -DYOSYS_VERIFIC_DIR="/usr/local/src/verific_lib"
================================= ======= ===================================
Parameter Default Description
================================= ======= ===================================
ENABLE_VERIFIC_SYSTEMVERILOG 1 SystemVerilog support
ENABLE_VERIFIC_VHDL 1 VHDL support
ENABLE_VERIFIC_HIER_TREE 1 Hierarchy tree support
ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 YosysHQ specific extensions support
ENABLE_VERIFIC_EDIF 0 EDIF support
ENABLE_VERIFIC_LIBERTY 0 Liberty file support
================================= ======= ===================================
During building, CMake will attempt to automatically detect available Verific
library components to enable the corresponding compile-time option in Yosys.
This can be overridden by manually setting the :makevar:`YOSYS_VERIFIC_FEATURES`
CMake variable. This variable should contain a semi-colon separated list, e.g.
``-DYOSYS_VERIFIC_FEATURES="systemverilog;hier_tree"``. The table below lists
the features available to Yosys.
To find the compile options used for a given Yosys build, call ``yosys-config
--cxxflags``. This documentation was built with the following compile options:
============== =========== ===================================
Feature Directory Description
============== =========== ===================================
systemverilog verilog SystemVerilog support
vhdl vhdl VHDL support
hier_tree hier_tree Hierarchy tree support
extensions extensions YosysHQ specific extensions support
edif edif EDIF support
liberty synlib Liberty file support
============== =========== ===================================
.. literalinclude:: /generated/yosys-config
:start-at: --cxxflags
:end-before: --linkflags
.. TODO:: CMAKE_TODO
``yosys-config --cxxflags`` no longer includes the verific features, and the
CMakeCache.txt doesn't report auto detected :makevar:`YOSYS_VERIFIC_FEATURES`
- can we export these somehow?
.. note::
@ -82,11 +82,10 @@ are required for the Yosys-Verific patch:
* RTL elaboration with
* SystemVerilog with ``ENABLE_VERIFIC_SYSTEMVERILOG``, and/or
* VHDL support with ``ENABLE_VERIFIC_VHDL``.
* SystemVerilog with ``systemverilog``, and/or
* VHDL support with ``vhdl``.
* Hierarchy tree support and static elaboration with
``ENABLE_VERIFIC_HIER_TREE``.
* Hierarchy tree support and static elaboration with ``hier_tree``.
Please be aware that the following Verific configuration build parameter needs
to be enabled in order to create the fully supported build:
@ -105,11 +104,12 @@ to be enabled in order to create the fully supported build:
Optional Verific features
~~~~~~~~~~~~~~~~~~~~~~~~~
The following Verific features are available with TabbyCAD and can be enabled in
Yosys builds:
The following Verific features are available with TabbyCAD and will be
automatically enabled in Yosys builds if the listed directory is included in the
:makevar:`YOSYS_VERIFIC_DIR`:
* EDIF support with ``ENABLE_VERIFIC_EDIF``, and
* Liberty file support with ``ENABLE_VERIFIC_LIBERTY``.
* EDIF support with ``edif`` directory, and
* Liberty file support with ``synlib`` directory.
Partially supported builds
~~~~~~~~~~~~~~~~~~~~~~~~~~
@ -124,32 +124,18 @@ lists a series of build configurations which are possible, but only provide a
limited subset of features. Please note that support is limited without YosysHQ
specific extensions of Verific library.
Configuration values:
a. ``ENABLE_VERIFIC_SYSTEMVERILOG``
b. ``ENABLE_VERIFIC_VHDL``
c. ``ENABLE_VERIFIC_HIER_TREE``
d. ``ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS``
+--------------------------------------------------------------------------+-----+-----+-----+-----+
| | Configuration values |
+--------------------------------------------------------------------------+-----+-----+-----+-----+
| Features | a | b | c | d |
+==========================================================================+=====+=====+=====+=====+
| SystemVerilog + RTL elaboration | 1 | 0 | 0 | 0 |
+--------------------------------------------------------------------------+-----+-----+-----+-----+
| VHDL + RTL elaboration | 0 | 1 | 0 | 0 |
+--------------------------------------------------------------------------+-----+-----+-----+-----+
| SystemVerilog + VHDL + RTL elaboration | 1 | 1 | 0 | 0 |
+--------------------------------------------------------------------------+-----+-----+-----+-----+
| SystemVerilog + RTL elaboration + Static elaboration + Hier tree | 1 | 0 | 1 | 0 |
+--------------------------------------------------------------------------+-----+-----+-----+-----+
| VHDL + RTL elaboration + Static elaboration + Hier tree | 0 | 1 | 1 | 0 |
+--------------------------------------------------------------------------+-----+-----+-----+-----+
| SystemVerilog + VHDL + RTL elaboration + Static elaboration + Hier tree | 1 | 1 | 1 | 0 |
+--------------------------------------------------------------------------+-----+-----+-----+-----+
======================================================================= =================================
Features :makevar:`YOSYS_VERIFIC_FEATURES`
======================================================================= =================================
SystemVerilog + RTL elaboration systemverilog
VHDL + RTL elaboration vhdl
SystemVerilog + VHDL + RTL elaboration systemverilog;vhdl
SystemVerilog + RTL elaboration + Static elaboration + Hier tree systemverilog;vhdl;hier_tree
VHDL + RTL elaboration + Static elaboration + Hier tree vhdl;hier_tree
SystemVerilog + VHDL + RTL elaboration + Static elaboration + Hier tree systemverilog;vhdl;hier_tree
======================================================================= =================================
.. note::
In case your Verific build has EDIF and/or Liberty support, you can enable
those options. These are not mentioned above for simplification and since
they are disabled by default.
those options. These are not mentioned above for simplification.

41
docs/source/yosys_internals/extending_yosys/test_suites.rst
View file

@ -7,19 +7,32 @@ Running the included test suite
-------------------------------
The Yosys source comes with a test suite to avoid regressions and keep
everything working as expected. Tests can be run by calling ``make test`` from
the root Yosys directory. By default, this runs vanilla and unit tests.
everything working as expected. Tests can be run by building the ``test``
target from the root Yosys directory. By default, this runs vanilla and unit
tests.
.. code:: console
cmake -B build .
cmake --build build --target test --parallel $(nproc)
.. TODO:: CMAKE_TODO
Using ``make -C <docs|tests>`` does work, but only if using default
:makevar:`BUILD_DIR` (``build``) and :makevar:`PROGRAM_PREFIX` (none).
Vanilla tests
~~~~~~~~~~~~~
These make up the majority of our testing coverage.
They can be run with ``make vanilla-test`` and are based on calls to
make subcommands (``make makefile-tests``) and shell scripts
(``make seed-tests`` and ``make abcopt-tests``). Both use ``run-test.sh``
files, but make-based tests only call ``tests/gen-tests-makefile.sh``
to generate a makefile appropriate for the given directory, so only
afterwards when make is invoked do the tests actually run.
.. TODO:: update for test infra changes
These make up the majority of our testing coverage. They can be run with the
``test-vanilla`` CMake target, or by calling ``make vanilla-test`` from the
``tests`` directory, and are based on calls to make subcommands (``make
makefile-tests``) and shell scripts (``make seed-tests`` and ``make
abcopt-tests``). Both use ``run-test.sh`` files, but make-based tests only call
``tests/gen-tests-makefile.sh`` to generate a makefile appropriate for the given
directory, so only afterwards when make is invoked do the tests actually run.
Usually their structure looks something like this:
you write a .ys file that gets automatically run,
@ -45,7 +58,7 @@ Running the unit tests requires the following additional packages:
No additional requirements.
Unit tests can be run with ``make unit-test``.
Unit tests can be run with the ``test-unit`` CMake target.
Functional tests
~~~~~~~~~~~~~~~~
@ -75,12 +88,20 @@ If you don't have one of the :ref:`getting_started/installation:CAD suite(s)`
installed, you should also install Z3 `following their
instructions <https://github.com/Z3Prover/z3>`_.
.. TODO:: CMAKE_TODO
How does this work under CMake? Is it only via ``make -C tests ENABLE_FUNCTIONAL_TESTS=1``
Then, set the :makevar:`ENABLE_FUNCTIONAL_TESTS` make variable when calling
``make test`` and the functional tests will be run as well.
Docs tests
~~~~~~~~~~
.. TODO:: CMAKE_TODO
Is this available via CMake?
There are some additional tests for checking examples included in the
documentation, which can be run by calling ``make test`` from the
:file:`yosys/docs` sub-directory (or ``make -C docs test`` from the root). This