From 2ffafadf2244c31b994546aef5e87f542cf993ee Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:58 +1200 Subject: [PATCH 01/14] Docs: Add note on verific Having a verific license does not provide access to the verific frontend. --- docs/source/using_yosys/more_scripting/load_design.rst | 8 ++++++++ docs/source/using_yosys/synthesis/memory.rst | 3 +++ 2 files changed, 11 insertions(+) diff --git a/docs/source/using_yosys/more_scripting/load_design.rst b/docs/source/using_yosys/more_scripting/load_design.rst index d64c50959bd..07c2bd8e58e 100644 --- a/docs/source/using_yosys/more_scripting/load_design.rst +++ b/docs/source/using_yosys/more_scripting/load_design.rst @@ -27,6 +27,14 @@ keyword: Frontends .. todo:: more info on other ``read_*`` commands, also is this the first time we mention verific? +.. note:: + + The Verific frontend for Yosys, which provides the :cmd:ref:`verific` + command, requires the commercial `Tabby CAD Suite`_. This is not the same as + simply having a Verific license when using Yosys. + +.. _Tabby CAD Suite: https://www.yosyshq.com/tabby-cad-datasheet + Others: - :doc:`/cmd/read` diff --git a/docs/source/using_yosys/synthesis/memory.rst b/docs/source/using_yosys/synthesis/memory.rst index 0f5e1bd3010..8306c82b9fb 100644 --- a/docs/source/using_yosys/synthesis/memory.rst +++ b/docs/source/using_yosys/synthesis/memory.rst @@ -697,6 +697,9 @@ TDP with multiple read ports Patterns only supported with Verific ------------------------------------ +The following patterns are only supported when Yosys is built with the Verific +front-end. + Synchronous SDP with write-first behavior via blocking assignments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ From e18a2f1e27cb699c13556181e75d6d3c20683aa6 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:58 +1200 Subject: [PATCH 02/14] Docs: Section/folder for yosys source details Move test_suites page into said folder. Placeholder page for building with verific. --- docs/source/getting_started/installation.rst | 5 +++-- docs/source/index.rst | 2 +- docs/source/yosys_source/build_verific.rst | 2 ++ docs/source/yosys_source/index.rst | 7 +++++++ docs/source/{ => yosys_source}/test_suites.rst | 0 5 files changed, 13 insertions(+), 3 deletions(-) create mode 100644 docs/source/yosys_source/build_verific.rst create mode 100644 docs/source/yosys_source/index.rst rename docs/source/{ => yosys_source}/test_suites.rst (100%) diff --git a/docs/source/getting_started/installation.rst b/docs/source/getting_started/installation.rst index aea8b6a2dd2..76b5aa4faf6 100644 --- a/docs/source/getting_started/installation.rst +++ b/docs/source/getting_started/installation.rst @@ -138,7 +138,8 @@ To use a compiler different than the default, use: .. seealso:: - Refer to :doc:`/test_suites` for details on testing Yosys once compiled. + Refer to :doc:`/yosys_source/test_suites` for details on testing Yosys once + compiled. Source tree and build system ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -193,7 +194,7 @@ directories: ``tests/`` This directory contains the suite of unit tests and regression tests used by - Yosys. See :doc:`/test_suites`. + Yosys. See :doc:`/yosys_source/test_suites`. The top-level Makefile includes :file:`frontends/{*}/Makefile.inc`, :file:`passes/{*}/Makefile.inc` and :file:`backends/{*}/Makefile.inc`. So when diff --git a/docs/source/index.rst b/docs/source/index.rst index 582551f7486..dd8fc9e775c 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -40,6 +40,6 @@ available, go to :ref:`commandindex`. getting_started/index using_yosys/index yosys_internals/index - test_suites + yosys_source/index appendix diff --git a/docs/source/yosys_source/build_verific.rst b/docs/source/yosys_source/build_verific.rst new file mode 100644 index 00000000000..4cceb368ec1 --- /dev/null +++ b/docs/source/yosys_source/build_verific.rst @@ -0,0 +1,2 @@ +Compiling with Verific library +------------------------------ diff --git a/docs/source/yosys_source/index.rst b/docs/source/yosys_source/index.rst new file mode 100644 index 00000000000..e93b01d4f2c --- /dev/null +++ b/docs/source/yosys_source/index.rst @@ -0,0 +1,7 @@ +Yosys source details +-------------------- + +.. toctree:: + + build_verific + test_suites diff --git a/docs/source/test_suites.rst b/docs/source/yosys_source/test_suites.rst similarity index 100% rename from docs/source/test_suites.rst rename to docs/source/yosys_source/test_suites.rst From d97a243c22cd682e4e043bb50d45b4a7cde2ff15 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:59 +1200 Subject: [PATCH 03/14] Docs: Intro to Yosys source section --- docs/source/yosys_internals/extending_yosys/extensions.rst | 2 ++ docs/source/yosys_source/index.rst | 4 ++++ 2 files changed, 6 insertions(+) diff --git a/docs/source/yosys_internals/extending_yosys/extensions.rst b/docs/source/yosys_internals/extending_yosys/extensions.rst index f10c634b015..fa4ad51f8f4 100644 --- a/docs/source/yosys_internals/extending_yosys/extensions.rst +++ b/docs/source/yosys_internals/extending_yosys/extensions.rst @@ -8,6 +8,8 @@ Writing extensions .. todo:: update to use :file:`/code_examples/extensions/test*.log` +.. todo:: should this be moved to yosys_source section? + This chapter contains some bits and pieces of information about programming yosys extensions. Don't be afraid to ask questions on the YosysHQ Slack. diff --git a/docs/source/yosys_source/index.rst b/docs/source/yosys_source/index.rst index e93b01d4f2c..c1d8e3f18ba 100644 --- a/docs/source/yosys_source/index.rst +++ b/docs/source/yosys_source/index.rst @@ -1,6 +1,10 @@ Yosys source details -------------------- +This section goes into additional detail on the Yosys source code and git +repository. This information is not needed for simply using Yosys, but may be +of interest for developers looking to customise Yosys builds. + .. toctree:: build_verific From 53b223f0dfa6cb86aacbccf8f99814b5a551f55b Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:59 +1200 Subject: [PATCH 04/14] Docs: Initial build_verific.rst From verific.md Co-authored-by: Miodrag Milanovic --- docs/source/yosys_source/build_verific.rst | 158 ++++++++++++++++++++- 1 file changed, 157 insertions(+), 1 deletion(-) diff --git a/docs/source/yosys_source/build_verific.rst b/docs/source/yosys_source/build_verific.rst index 4cceb368ec1..f8870e0c13b 100644 --- a/docs/source/yosys_source/build_verific.rst +++ b/docs/source/yosys_source/build_verific.rst @@ -1,2 +1,158 @@ Compiling with Verific library ------------------------------- +============================== + +YosysHQ creates build for TabbyCAD Suite that includes Verific with additional +patches and our own extensions library. However, if you have licensed Verific +library in source or binary form you can still compile Yosys and have at least +partial support. + +Compile options +--------------- + +To enable Verific support ``ENABLE_VERIFIC`` has to be set to ``1`` and +``VERIFIC_DIR`` needs to point to location where library is located. + +============== ========================== =============================== +Parameter Default Description +============== ========================== =============================== +ENABLE_VERIFIC 0 Enable compilation with Verific +VERIFIC_DIR /usr/local/src/verific_lib Library and headers location +============== ========================== =============================== + +Since there are multiple Verific library builds and they can have different +features, there are compile options to select them. + +================================= ======= =================================== +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 1 YosysHQ specific extensions support +ENABLE_VERIFIC_EDIF 0 EDIF support +ENABLE_VERIFIC_LIBERTY 0 Liberty file support +================================= ======= =================================== + +Supported build +--------------- + +Default options values are created in such way to represent supported build. +This one includes SystemVerilog and VHDL support with RTL elaboration, hierarchy +tree and static elaboration for both languages. + +Fully supported build includes additional YosysHQ patch that can be bought for +**only** this Verific library configuration. + +NOTE: TabbyCAD builds also have additional EDIF and Liberty file support enabled +as well. YosysHQ extensions library is only part of TabbyCAD as a product. + +Partialy supported builds +------------------------- + +Note that these builds can be used with Yosys but will miss some of important +features. + +1. SystemVerilog + RTL elaboration + +================================= ======= +Parameter Default +================================= ======= +ENABLE_VERIFIC_SYSTEMVERILOG 1 +ENABLE_VERIFIC_VHDL 0 +ENABLE_VERIFIC_HIER_TREE 0 +ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 +================================= ======= + +2. VHDL + RTL elaboration + +================================= ======= +Parameter Default +================================= ======= +ENABLE_VERIFIC_SYSTEMVERILOG 0 +ENABLE_VERIFIC_VHDL 1 +ENABLE_VERIFIC_HIER_TREE 0 +ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 +================================= ======= + +3. SystemVerilog + VHDL + RTL elaboration + +================================= ======= +Parameter Default +================================= ======= +ENABLE_VERIFIC_SYSTEMVERILOG 1 +ENABLE_VERIFIC_VHDL 1 +ENABLE_VERIFIC_HIER_TREE 0 +ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 +================================= ======= + +3. SystemVerilog + RTL elaboration + Static elaboration + Hier tree + +================================= ======= +Parameter Default +================================= ======= +ENABLE_VERIFIC_SYSTEMVERILOG 1 +ENABLE_VERIFIC_VHDL 0 +ENABLE_VERIFIC_HIER_TREE 1 +ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 +================================= ======= + +3. VHDL + RTL elaboration + Static elaboration + Hier tree + +================================= ======= +Parameter Default +================================= ======= +ENABLE_VERIFIC_SYSTEMVERILOG 0 +ENABLE_VERIFIC_VHDL 1 +ENABLE_VERIFIC_HIER_TREE 1 +ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 +================================= ======= + +4. SystemVerilog + VHDL + RTL elaboration + Static elaboration + Hier + tree + +================================= ======= +Parameter Default +================================= ======= +ENABLE_VERIFIC_SYSTEMVERILOG 1 +ENABLE_VERIFIC_VHDL 1 +ENABLE_VERIFIC_HIER_TREE 1 +ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 +================================= ======= + +NOTE: + +In case your Verific build have EDIF and/or Liberty support, you can enable +those options, these are not mentioned above for simplification and since they +are disabled by default. + +NOTE: To be able to compile Yosys+Verific you need Verific library that have at +least one of HDL languages support with RTL elaboration enabled. Please note +that without YosysHQ specific extensions of Verific library, support is limited. + +Verific Features that should be enabled in your Verific library +=============================================================== + +Please be aware that next Verific configuration build parameter needs to be +enabled in order to create fully supported build. + +:: + + database/DBCompileFlags.h: + DB_PRESERVE_INITIAL_VALUE + +Additional features included with Yosys Verific patch +===================================================== + +New cells +--------- + +============== =========== +Cell Description +============== =========== +$initstate +$set_tag +$get_tag +$overwrite_tag +$original_tag +$future_ff +============== =========== From 8e618cac450ea9c9b0855ba8dba0b1ee1eb3534e Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:59 +1200 Subject: [PATCH 05/14] Docs: Update build_verific.rst Move patch section to top. Add todos for open questions. Reformat partially supported builds into a single table. General language tidy up/reflow. --- docs/source/yosys_source/build_verific.rst | 208 +++++++++------------ 1 file changed, 89 insertions(+), 119 deletions(-) diff --git a/docs/source/yosys_source/build_verific.rst b/docs/source/yosys_source/build_verific.rst index f8870e0c13b..626d045de13 100644 --- a/docs/source/yosys_source/build_verific.rst +++ b/docs/source/yosys_source/build_verific.rst @@ -1,16 +1,48 @@ Compiling with Verific library ============================== -YosysHQ creates build for TabbyCAD Suite that includes Verific with additional -patches and our own extensions library. However, if you have licensed Verific -library in source or binary form you can still compile Yosys and have at least -partial support. +The easiest way to get Yosys with Verific support is to `contact YosysHQ`_ for a +`Tabby CAD Suite`_ evaluation license and download link. The TabbyCAD Suite +includes additional patches and a custom extensions library in order to get the +most out of the Verific parser when using Yosys. + +If you already have a license for the Verific parser, in either source or binary +form, you may be able to compile Yosys with partial Verific support yourself. + +.. _contact YosysHQ : https://www.yosyshq.com/contact +.. _Tabby CAD Suite: https://www.yosyshq.com/tabby-cad-datasheet + +The Yosys-Verific patch +----------------------- + +.. todo:: Fill out section on Yosys-Verific patch + +* Yosys-Verific patch developed for best integration +* Needed for some of the formal verification front-end tools +* `contact YosysHQ`_ about licensing this patch for your own Yosys builds +* Unable to provide support for builds without this patch + +New cells +~~~~~~~~~ + +============== =========== +Cell Description +============== =========== +$initstate +$set_tag +$get_tag +$overwrite_tag +$original_tag +$future_ff +============== =========== + +.. todo:: (sub)section on features only available with TabbyCAD Compile options --------------- To enable Verific support ``ENABLE_VERIFIC`` has to be set to ``1`` and -``VERIFIC_DIR`` needs to point to location where library is located. +``VERIFIC_DIR`` needs to point to the location where the library is located. ============== ========================== =============================== Parameter Default Description @@ -34,125 +66,63 @@ ENABLE_VERIFIC_LIBERTY 0 Liberty file support ================================= ======= =================================== Supported build ---------------- - -Default options values are created in such way to represent supported build. -This one includes SystemVerilog and VHDL support with RTL elaboration, hierarchy -tree and static elaboration for both languages. - -Fully supported build includes additional YosysHQ patch that can be bought for -**only** this Verific library configuration. - -NOTE: TabbyCAD builds also have additional EDIF and Liberty file support enabled -as well. YosysHQ extensions library is only part of TabbyCAD as a product. - -Partialy supported builds -------------------------- - -Note that these builds can be used with Yosys but will miss some of important -features. - -1. SystemVerilog + RTL elaboration - -================================= ======= -Parameter Default -================================= ======= -ENABLE_VERIFIC_SYSTEMVERILOG 1 -ENABLE_VERIFIC_VHDL 0 -ENABLE_VERIFIC_HIER_TREE 0 -ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 -================================= ======= - -2. VHDL + RTL elaboration - -================================= ======= -Parameter Default -================================= ======= -ENABLE_VERIFIC_SYSTEMVERILOG 0 -ENABLE_VERIFIC_VHDL 1 -ENABLE_VERIFIC_HIER_TREE 0 -ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 -================================= ======= - -3. SystemVerilog + VHDL + RTL elaboration - -================================= ======= -Parameter Default -================================= ======= -ENABLE_VERIFIC_SYSTEMVERILOG 1 -ENABLE_VERIFIC_VHDL 1 -ENABLE_VERIFIC_HIER_TREE 0 -ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 -================================= ======= - -3. SystemVerilog + RTL elaboration + Static elaboration + Hier tree - -================================= ======= -Parameter Default -================================= ======= -ENABLE_VERIFIC_SYSTEMVERILOG 1 -ENABLE_VERIFIC_VHDL 0 -ENABLE_VERIFIC_HIER_TREE 1 -ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 -================================= ======= - -3. VHDL + RTL elaboration + Static elaboration + Hier tree - -================================= ======= -Parameter Default -================================= ======= -ENABLE_VERIFIC_SYSTEMVERILOG 0 -ENABLE_VERIFIC_VHDL 1 -ENABLE_VERIFIC_HIER_TREE 1 -ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 -================================= ======= - -4. SystemVerilog + VHDL + RTL elaboration + Static elaboration + Hier - tree - -================================= ======= -Parameter Default -================================= ======= -ENABLE_VERIFIC_SYSTEMVERILOG 1 -ENABLE_VERIFIC_VHDL 1 -ENABLE_VERIFIC_HIER_TREE 1 -ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 -================================= ======= - -NOTE: - -In case your Verific build have EDIF and/or Liberty support, you can enable -those options, these are not mentioned above for simplification and since they -are disabled by default. - -NOTE: To be able to compile Yosys+Verific you need Verific library that have at -least one of HDL languages support with RTL elaboration enabled. Please note -that without YosysHQ specific extensions of Verific library, support is limited. +~~~~~~~~~~~~~~~ + +The default values for options represent the only fully supported configuration +of Yosys with Verific. This build includes SystemVerilog and VHDL support with +RTL elaboration, hierarchy tree and static elaboration for both languages. This +is the only configuration for which the Yosys-Verific patch is available. + +.. note:: + + TabbyCAD builds also have additional EDIF and Liberty file support enabled. + YosysHQ extensions library is only part of TabbyCAD as a product. + +.. todo:: is "YosysHQ extensions library" == "YosysHQ specific extensions support" ? + + If not, they need to be better distinguished. If they are, then how is it + possible for someone to build the supported configuration? + +Partially supported builds +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +To be able to compile Yosys with Verific, the Verific library must have support +for at least one HDL language with RTL elaboration enabled. The following table +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 beginning with ENABLE_VERIFIC\_ | ++--------------------------------------------------------------------------+---------------+------+-----------+--------------------+ +| Features | SYSTEMVERILOG | VHDL | HIER_TREE | YOSYSHQ_EXTENSIONS | ++==========================================================================+===============+======+===========+====================+ +| 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 | ++--------------------------------------------------------------------------+---------------+------+-----------+--------------------+ + +.. 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. Verific Features that should be enabled in your Verific library -=============================================================== +--------------------------------------------------------------- -Please be aware that next Verific configuration build parameter needs to be -enabled in order to create fully supported build. +Please be aware that the following Verific configuration build parameter needs +to be enabled in order to create the fully supported build. :: database/DBCompileFlags.h: DB_PRESERVE_INITIAL_VALUE - -Additional features included with Yosys Verific patch -===================================================== - -New cells ---------- - -============== =========== -Cell Description -============== =========== -$initstate -$set_tag -$get_tag -$overwrite_tag -$original_tag -$future_ff -============== =========== From 00bb3b6fc2f903d7eb32ae978cff2abd11832cae Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:59 +1200 Subject: [PATCH 06/14] Docs: Merge yosys_source into extending_yosys Move abc_flow content into synthesis/abc document. --- docs/source/using_yosys/synthesis/abc.rst | 84 ++++++++++++++++++- .../extending_yosys/abc_flow.rst | 76 ----------------- .../extending_yosys}/build_verific.rst | 0 .../yosys_internals/extending_yosys/index.rst | 11 ++- .../extending_yosys}/test_suites.rst | 0 docs/source/yosys_source/index.rst | 11 --- 6 files changed, 88 insertions(+), 94 deletions(-) delete mode 100644 docs/source/yosys_internals/extending_yosys/abc_flow.rst rename docs/source/{yosys_source => yosys_internals/extending_yosys}/build_verific.rst (100%) rename docs/source/{yosys_source => yosys_internals/extending_yosys}/test_suites.rst (100%) delete mode 100644 docs/source/yosys_source/index.rst diff --git a/docs/source/using_yosys/synthesis/abc.rst b/docs/source/using_yosys/synthesis/abc.rst index 928b320186d..fca9ddec063 100644 --- a/docs/source/using_yosys/synthesis/abc.rst +++ b/docs/source/using_yosys/synthesis/abc.rst @@ -1,5 +1,5 @@ The ABC toolbox ---------------- +=============== .. role:: yoscrypt(code) :language: yoscrypt @@ -21,7 +21,7 @@ global view of the mapping problem. .. _ABC: https://github.com/berkeley-abc/abc ABC: the unit delay model, simple and efficient -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +----------------------------------------------- The :cmd:ref:`abc` pass uses a highly simplified view of an FPGA: @@ -66,7 +66,7 @@ But this approach has drawbacks, too: before clock edge) which affect the delay of a path. ABC9: the generalised delay model, realistic and flexible -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +--------------------------------------------------------- ABC9 uses a more detailed and accurate model of an FPGA: @@ -101,3 +101,81 @@ optimise better around those boxes, and also permute inputs to give the critical path the fastest inputs. .. todo:: more about logic minimization & register balancing et al with ABC + +Setting up a flow for ABC9 +-------------------------- + +Much of the configuration comes from attributes and ``specify`` blocks in +Verilog simulation models. + +``specify`` syntax +~~~~~~~~~~~~~~~~~~ + +Since ``specify`` is a relatively obscure part of the Verilog standard, a quick +guide to the syntax: + +.. code-block:: verilog + + specify // begins a specify block + (A => B) = 123; // simple combinational path from A to B with a delay of 123. + (A *> B) = 123; // simple combinational path from A to all bits of B with a delay of 123 for all. + if (FOO) (A => B) = 123; // paths may apply under specific conditions. + (posedge CLK => (Q : D)) = 123; // combinational path triggered on the positive edge of CLK; used for clock-to-Q arrival paths. + $setup(A, posedge CLK, 123); // setup constraint for an input relative to a clock. + endspecify // ends a specify block + +By convention, all delays in ``specify`` blocks are in integer picoseconds. +Files containing ``specify`` blocks should be read with the ``-specify`` option +to :cmd:ref:`read_verilog` so that they aren't skipped. + +LUTs +^^^^ + +LUTs need to be annotated with an ``(* abc9_lut=N *)`` attribute, where ``N`` is +the relative area of that LUT model. For example, if an architecture can combine +LUTs to produce larger LUTs, then the combined LUTs would have increasingly +larger ``N``. Conversely, if an architecture can split larger LUTs into smaller +LUTs, then the smaller LUTs would have smaller ``N``. + +LUTs are generally specified with simple combinational paths from the LUT inputs +to the LUT output. + +DFFs +^^^^ + +DFFs should be annotated with an ``(* abc9_flop *)`` attribute, however ABC9 has +some specific requirements for this to be valid: - the DFF must initialise to +zero (consider using :cmd:ref:`dfflegalize` to ensure this). - the DFF cannot +have any asynchronous resets/sets (see the simplification idiom and the Boxes +section for what to do here). + +It is worth noting that in pure ``abc9`` mode, only the setup and arrival times +are passed to ABC9 (specifically, they are modelled as buffers with the given +delay). In ``abc9 -dff``, the flop itself is passed to ABC9, permitting +sequential optimisations. + +Some vendors have universal DFF models which include async sets/resets even when +they're unused. Therefore *the simplification idiom* exists to handle this: by +using a ``techmap`` file to discover flops which have a constant driver to those +asynchronous controls, they can be mapped into an intermediate, simplified flop +which qualifies as an ``(* abc9_flop *)``, ran through :cmd:ref:`abc9`, and then +mapped back to the original flop. This is used in :cmd:ref:`synth_intel_alm` and +:cmd:ref:`synth_quicklogic` for the PolarPro3. + +DFFs are usually specified to have setup constraints against the clock on the +input signals, and an arrival time for the ``Q`` output. + +Boxes +^^^^^ + +A "box" is a purely-combinational piece of hard logic. If the logic is exposed +to ABC9, it's a "whitebox", otherwise it's a "blackbox". Carry chains would be +best implemented as whiteboxes, but a DSP would be best implemented as a +blackbox (multipliers are too complex to easily work with). LUT RAMs can be +implemented as whiteboxes too. + +Boxes are arguably the biggest advantage that ABC9 has over ABC: by being aware +of carry chains and DSPs, it avoids optimising for a path that isn't the actual +critical path, while the generally-longer paths result in ABC9 being able to +reduce design area by mapping other logic to larger-but-slower cells. + diff --git a/docs/source/yosys_internals/extending_yosys/abc_flow.rst b/docs/source/yosys_internals/extending_yosys/abc_flow.rst deleted file mode 100644 index 86afd3336f6..00000000000 --- a/docs/source/yosys_internals/extending_yosys/abc_flow.rst +++ /dev/null @@ -1,76 +0,0 @@ -Setting up a flow for ABC9 --------------------------- - -Much of the configuration comes from attributes and ``specify`` blocks in -Verilog simulation models. - -``specify`` syntax -~~~~~~~~~~~~~~~~~~ - -Since ``specify`` is a relatively obscure part of the Verilog standard, a quick -guide to the syntax: - -.. code-block:: verilog - - specify // begins a specify block - (A => B) = 123; // simple combinational path from A to B with a delay of 123. - (A *> B) = 123; // simple combinational path from A to all bits of B with a delay of 123 for all. - if (FOO) (A => B) = 123; // paths may apply under specific conditions. - (posedge CLK => (Q : D)) = 123; // combinational path triggered on the positive edge of CLK; used for clock-to-Q arrival paths. - $setup(A, posedge CLK, 123); // setup constraint for an input relative to a clock. - endspecify // ends a specify block - -By convention, all delays in ``specify`` blocks are in integer picoseconds. -Files containing ``specify`` blocks should be read with the ``-specify`` option -to :cmd:ref:`read_verilog` so that they aren't skipped. - -LUTs -^^^^ - -LUTs need to be annotated with an ``(* abc9_lut=N *)`` attribute, where ``N`` is -the relative area of that LUT model. For example, if an architecture can combine -LUTs to produce larger LUTs, then the combined LUTs would have increasingly -larger ``N``. Conversely, if an architecture can split larger LUTs into smaller -LUTs, then the smaller LUTs would have smaller ``N``. - -LUTs are generally specified with simple combinational paths from the LUT inputs -to the LUT output. - -DFFs -^^^^ - -DFFs should be annotated with an ``(* abc9_flop *)`` attribute, however ABC9 has -some specific requirements for this to be valid: - the DFF must initialise to -zero (consider using :cmd:ref:`dfflegalize` to ensure this). - the DFF cannot -have any asynchronous resets/sets (see the simplification idiom and the Boxes -section for what to do here). - -It is worth noting that in pure ``abc9`` mode, only the setup and arrival times -are passed to ABC9 (specifically, they are modelled as buffers with the given -delay). In ``abc9 -dff``, the flop itself is passed to ABC9, permitting -sequential optimisations. - -Some vendors have universal DFF models which include async sets/resets even when -they're unused. Therefore *the simplification idiom* exists to handle this: by -using a ``techmap`` file to discover flops which have a constant driver to those -asynchronous controls, they can be mapped into an intermediate, simplified flop -which qualifies as an ``(* abc9_flop *)``, ran through :cmd:ref:`abc9`, and then -mapped back to the original flop. This is used in :cmd:ref:`synth_intel_alm` and -:cmd:ref:`synth_quicklogic` for the PolarPro3. - -DFFs are usually specified to have setup constraints against the clock on the -input signals, and an arrival time for the ``Q`` output. - -Boxes -^^^^^ - -A "box" is a purely-combinational piece of hard logic. If the logic is exposed -to ABC9, it's a "whitebox", otherwise it's a "blackbox". Carry chains would be -best implemented as whiteboxes, but a DSP would be best implemented as a -blackbox (multipliers are too complex to easily work with). LUT RAMs can be -implemented as whiteboxes too. - -Boxes are arguably the biggest advantage that ABC9 has over ABC: by being aware -of carry chains and DSPs, it avoids optimising for a path that isn't the actual -critical path, while the generally-longer paths result in ABC9 being able to -reduce design area by mapping other logic to larger-but-slower cells. diff --git a/docs/source/yosys_source/build_verific.rst b/docs/source/yosys_internals/extending_yosys/build_verific.rst similarity index 100% rename from docs/source/yosys_source/build_verific.rst rename to docs/source/yosys_internals/extending_yosys/build_verific.rst diff --git a/docs/source/yosys_internals/extending_yosys/index.rst b/docs/source/yosys_internals/extending_yosys/index.rst index c2dc6cd2b8b..2a4d2dfef04 100644 --- a/docs/source/yosys_internals/extending_yosys/index.rst +++ b/docs/source/yosys_internals/extending_yosys/index.rst @@ -1,11 +1,14 @@ -Extending Yosys ---------------- +Working with the Yosys codebase +------------------------------- -.. todo:: brief overview for the extending Yosys index +This section goes into additional detail on the Yosys source code and git +repository. This information is not needed for simply using Yosys, but may be +of interest for developers looking to customise Yosys builds. .. toctree:: :maxdepth: 3 extensions - abc_flow + build_verific + test_suites diff --git a/docs/source/yosys_source/test_suites.rst b/docs/source/yosys_internals/extending_yosys/test_suites.rst similarity index 100% rename from docs/source/yosys_source/test_suites.rst rename to docs/source/yosys_internals/extending_yosys/test_suites.rst diff --git a/docs/source/yosys_source/index.rst b/docs/source/yosys_source/index.rst deleted file mode 100644 index c1d8e3f18ba..00000000000 --- a/docs/source/yosys_source/index.rst +++ /dev/null @@ -1,11 +0,0 @@ -Yosys source details --------------------- - -This section goes into additional detail on the Yosys source code and git -repository. This information is not needed for simply using Yosys, but may be -of interest for developers looking to customise Yosys builds. - -.. toctree:: - - build_verific - test_suites From cfba26ca8ba335ee3a66f69994ab008effd89ead Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:59 +1200 Subject: [PATCH 07/14] Docs: Verific progress --- .../extending_yosys/build_verific.rst | 80 +++++++++---------- 1 file changed, 38 insertions(+), 42 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/build_verific.rst b/docs/source/yosys_internals/extending_yosys/build_verific.rst index 626d045de13..3ae1925b632 100644 --- a/docs/source/yosys_internals/extending_yosys/build_verific.rst +++ b/docs/source/yosys_internals/extending_yosys/build_verific.rst @@ -15,28 +15,19 @@ form, you may be able to compile Yosys with partial Verific support yourself. The Yosys-Verific patch ----------------------- -.. todo:: Fill out section on Yosys-Verific patch - -* Yosys-Verific patch developed for best integration +* To provide the best integration between Yosys and Verific, some features are + required to be patched into the Verific library. +* Synthesis from RTL may be possible without this patch, however we are unable + to provide support for any Yosys+Verific builds without it. * Needed for some of the formal verification front-end tools -* `contact YosysHQ`_ about licensing this patch for your own Yosys builds -* Unable to provide support for builds without this patch - -New cells -~~~~~~~~~ +* `contact YosysHQ`_ about licensing this patch for your own Yosys builds. -============== =========== -Cell Description -============== =========== -$initstate -$set_tag -$get_tag -$overwrite_tag -$original_tag -$future_ff -============== =========== +.. warning:: -.. todo:: (sub)section on features only available with TabbyCAD + Some of the formal verification front-end tools may not be fully supported + without the full TabbyCAD suite. If you are wanting to use these tools, make + sure to `contact YosysHQ`_ and ask us if the Yosys-Verific patch is right for + you. Compile options --------------- @@ -65,23 +56,39 @@ ENABLE_VERIFIC_EDIF 0 EDIF support ENABLE_VERIFIC_LIBERTY 0 Liberty file support ================================= ======= =================================== -Supported build -~~~~~~~~~~~~~~~ +Required Verific features +~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following features, along with their corresponding Yosys build parameters, +are required for the Yosys-Verific patch: + +* RTL elaboration with + * SystemVerilog with ENABLE_VERIFIC_SYSTEMVERILOG, and/or + * VHDL support with ENABLE_VERIFIC_VHDL. +* Hierarchy tree support and static elaboration with ENABLE_VERIFIC_HIER_TREE. + +Please be aware that the following Verific configuration build parameter needs +to be enabled in order to create the fully supported build: + +:: + + database/DBCompileFlags.h: + DB_PRESERVE_INITIAL_VALUE -The default values for options represent the only fully supported configuration -of Yosys with Verific. This build includes SystemVerilog and VHDL support with -RTL elaboration, hierarchy tree and static elaboration for both languages. This -is the only configuration for which the Yosys-Verific patch is available. +.. note:: -.. note:: + Yosys+Verific builds may compile without these features, but we provide no + guarantees and cannot offer support if they are disabled or the Yosys-Verific + patch is not used. - TabbyCAD builds also have additional EDIF and Liberty file support enabled. - YosysHQ extensions library is only part of TabbyCAD as a product. +Optional Verific features +~~~~~~~~~~~~~~~~~~~~~~~~~ -.. todo:: is "YosysHQ extensions library" == "YosysHQ specific extensions support" ? +The following Verific features are available with TabbyCAD and can be enabled in +Yosys builds: - If not, they need to be better distinguished. If they are, then how is it - possible for someone to build the supported configuration? +* EDIF support with ENABLE_VERIFIC_EDIF, and +* Liberty file support with ENABLE_VERIFIC_LIBERTY. Partially supported builds ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -115,14 +122,3 @@ specific extensions of Verific library. 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. - -Verific Features that should be enabled in your Verific library ---------------------------------------------------------------- - -Please be aware that the following Verific configuration build parameter needs -to be enabled in order to create the fully supported build. - -:: - - database/DBCompileFlags.h: - DB_PRESERVE_INITIAL_VALUE From 88bb785dcd729b5df31fab4462269d86be72122d Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:59 +1200 Subject: [PATCH 08/14] Docs: Verific but with sentences --- .../extending_yosys/build_verific.rst | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/build_verific.rst b/docs/source/yosys_internals/extending_yosys/build_verific.rst index 3ae1925b632..ea21fda0868 100644 --- a/docs/source/yosys_internals/extending_yosys/build_verific.rst +++ b/docs/source/yosys_internals/extending_yosys/build_verific.rst @@ -15,18 +15,17 @@ form, you may be able to compile Yosys with partial Verific support yourself. The Yosys-Verific patch ----------------------- -* To provide the best integration between Yosys and Verific, some features are - required to be patched into the Verific library. -* Synthesis from RTL may be possible without this patch, however we are unable - to provide support for any Yosys+Verific builds without it. -* Needed for some of the formal verification front-end tools -* `contact YosysHQ`_ about licensing this patch for your own Yosys builds. +YosysHQ maintains and develops a patch for Verific in order to better integrate +with Yosys and to provide features required by some of the formal verification +front-end tools. Synthesis from RTL may be possible without this patch, however +we are unable to provide support for any Yosys+Verific builds without it. To +license this patch for your own Yosys builds, `contact YosysHQ`_. .. warning:: Some of the formal verification front-end tools may not be fully supported - without the full TabbyCAD suite. If you are wanting to use these tools, make - sure to `contact YosysHQ`_ and ask us if the Yosys-Verific patch is right for + without the full TabbyCAD suite. If you are wanting to use these tools, + including SBY, make sure to ask us if the Yosys-Verific patch is right for you. Compile options @@ -93,6 +92,10 @@ Yosys builds: Partially supported builds ~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. todo:: still unclear on the purpose of this section. + + Are these the configurations we have tested as being able to compile? + To be able to compile Yosys with Verific, the Verific library must have support for at least one HDL language with RTL elaboration enabled. The following table lists a series of build configurations which are possible, but only provide a From 36ad07e1d5bf1e4ca9759062555600182ae7f4b5 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:59 +1200 Subject: [PATCH 09/14] Docs: Update build_verific Clarify partially supported builds section. Update parameter defaults. Include note on finding compile options with `yosys-config`. Fix remaining references to `/yosys_source/`. --- docs/source/getting_started/installation.rst | 6 +++--- docs/source/index.rst | 1 - .../extending_yosys/build_verific.rst | 15 +++++++++++---- 3 files changed, 14 insertions(+), 8 deletions(-) diff --git a/docs/source/getting_started/installation.rst b/docs/source/getting_started/installation.rst index 76b5aa4faf6..4d1a2f36a58 100644 --- a/docs/source/getting_started/installation.rst +++ b/docs/source/getting_started/installation.rst @@ -138,8 +138,8 @@ To use a compiler different than the default, use: .. seealso:: - Refer to :doc:`/yosys_source/test_suites` for details on testing Yosys once - compiled. + Refer to :doc:`/yosys_internals/extending_yosys/test_suites` for details on + testing Yosys once compiled. Source tree and build system ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -194,7 +194,7 @@ directories: ``tests/`` This directory contains the suite of unit tests and regression tests used by - Yosys. See :doc:`/yosys_source/test_suites`. + Yosys. See :doc:`/yosys_internals/extending_yosys/test_suites`. The top-level Makefile includes :file:`frontends/{*}/Makefile.inc`, :file:`passes/{*}/Makefile.inc` and :file:`backends/{*}/Makefile.inc`. So when diff --git a/docs/source/index.rst b/docs/source/index.rst index dd8fc9e775c..106ddbab86b 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -40,6 +40,5 @@ available, go to :ref:`commandindex`. getting_started/index using_yosys/index yosys_internals/index - yosys_source/index appendix diff --git a/docs/source/yosys_internals/extending_yosys/build_verific.rst b/docs/source/yosys_internals/extending_yosys/build_verific.rst index ea21fda0868..d8502d7bb67 100644 --- a/docs/source/yosys_internals/extending_yosys/build_verific.rst +++ b/docs/source/yosys_internals/extending_yosys/build_verific.rst @@ -50,11 +50,18 @@ 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 1 YosysHQ specific extensions support +ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS 0 YosysHQ specific extensions support ENABLE_VERIFIC_EDIF 0 EDIF support ENABLE_VERIFIC_LIBERTY 0 Liberty file support ================================= ======= =================================== +To find the compile options used for a given Yosys build, call `yosys-config +--cxxflags`. This documentation was built with the following compile options: + +.. literalinclude:: /generated/yosys-config + :start-at: --cxxflags + :end-before: --linkflags + Required Verific features ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -92,9 +99,9 @@ Yosys builds: Partially supported builds ~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. todo:: still unclear on the purpose of this section. - - Are these the configurations we have tested as being able to compile? +This section describes Yosys+Verific configurations which we have confirmed as +working in the past, however they are not a part of our regular tests so we +cannot guarantee they are still functional. To be able to compile Yosys with Verific, the Verific library must have support for at least one HDL language with RTL elaboration enabled. The following table From 0327ad97f2e7ddeaa553c1fca768cd32ec29056e Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:59 +1200 Subject: [PATCH 10/14] Docs: Fix code formatting Gets me everytime --- .../extending_yosys/build_verific.rst | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/build_verific.rst b/docs/source/yosys_internals/extending_yosys/build_verific.rst index d8502d7bb67..16ec53645b2 100644 --- a/docs/source/yosys_internals/extending_yosys/build_verific.rst +++ b/docs/source/yosys_internals/extending_yosys/build_verific.rst @@ -55,8 +55,8 @@ ENABLE_VERIFIC_EDIF 0 EDIF support ENABLE_VERIFIC_LIBERTY 0 Liberty file support ================================= ======= =================================== -To find the compile options used for a given Yosys build, call `yosys-config ---cxxflags`. This documentation was built with the following compile options: +To find the compile options used for a given Yosys build, call ``yosys-config +--cxxflags``. This documentation was built with the following compile options: .. literalinclude:: /generated/yosys-config :start-at: --cxxflags @@ -69,9 +69,10 @@ The following features, along with their corresponding Yosys build parameters, are required for the Yosys-Verific patch: * RTL elaboration with - * SystemVerilog with ENABLE_VERIFIC_SYSTEMVERILOG, and/or - * VHDL support with ENABLE_VERIFIC_VHDL. -* Hierarchy tree support and static elaboration with ENABLE_VERIFIC_HIER_TREE. + * SystemVerilog with ``ENABLE_VERIFIC_SYSTEMVERILOG``, and/or + * VHDL support with ``ENABLE_VERIFIC_VHDL``. +* Hierarchy tree support and static elaboration with + ``ENABLE_VERIFIC_HIER_TREE``. Please be aware that the following Verific configuration build parameter needs to be enabled in order to create the fully supported build: @@ -93,8 +94,8 @@ Optional Verific features The following Verific features are available with TabbyCAD and can be enabled in Yosys builds: -* EDIF support with ENABLE_VERIFIC_EDIF, and -* Liberty file support with ENABLE_VERIFIC_LIBERTY. +* EDIF support with ``ENABLE_VERIFIC_EDIF``, and +* Liberty file support with ``ENABLE_VERIFIC_LIBERTY``. Partially supported builds ~~~~~~~~~~~~~~~~~~~~~~~~~~ From 8145461c7898754985595f84787f4058e0c9aa8d Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:59 +1200 Subject: [PATCH 11/14] Docs: Fix Verific builds table formatting PDF don't like the long headers, so instead use placeholders a-d with elaborations below. --- .../extending_yosys/build_verific.rst | 40 +++++++++++-------- 1 file changed, 23 insertions(+), 17 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/build_verific.rst b/docs/source/yosys_internals/extending_yosys/build_verific.rst index 16ec53645b2..ae453886f99 100644 --- a/docs/source/yosys_internals/extending_yosys/build_verific.rst +++ b/docs/source/yosys_internals/extending_yosys/build_verific.rst @@ -110,23 +110,29 @@ 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 beginning with ENABLE_VERIFIC\_ | -+--------------------------------------------------------------------------+---------------+------+-----------+--------------------+ -| Features | SYSTEMVERILOG | VHDL | HIER_TREE | YOSYSHQ_EXTENSIONS | -+==========================================================================+===============+======+===========+====================+ -| 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 | -+--------------------------------------------------------------------------+---------------+------+-----------+--------------------+ ++--------------------------------------------------------------------------+---+---+---+-----------+ +| | 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 | ++--------------------------------------------------------------------------+-----+-----+-----+-----+ + +Configuration values: + a. ``ENABLE_VERIFIC_SYSTEMVERILOG`` + b. ``ENABLE_VERIFIC_VHDL`` + c. ``ENABLE_VERIFIC_HIER_TREE`` + d. ``ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS`` .. note:: From 6431534c2455ffb091d70a510581cf00f73ca79e Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:03:59 +1200 Subject: [PATCH 12/14] Docs: Some other fixes --- docs/source/using_yosys/more_scripting/load_design.rst | 7 +++---- docs/source/yosys_internals/extending_yosys/extensions.rst | 2 -- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/docs/source/using_yosys/more_scripting/load_design.rst b/docs/source/using_yosys/more_scripting/load_design.rst index 07c2bd8e58e..cf6a1dc1f3f 100644 --- a/docs/source/using_yosys/more_scripting/load_design.rst +++ b/docs/source/using_yosys/more_scripting/load_design.rst @@ -30,10 +30,9 @@ keyword: Frontends .. note:: The Verific frontend for Yosys, which provides the :cmd:ref:`verific` - command, requires the commercial `Tabby CAD Suite`_. This is not the same as - simply having a Verific license when using Yosys. - -.. _Tabby CAD Suite: https://www.yosyshq.com/tabby-cad-datasheet + command, requires Yosys to be built with Verific. This is not the same as + simply having a Verific license when using Yosys. Check + :doc:`/yosys_internals/extending_yosys/build_verific` for more. Others: diff --git a/docs/source/yosys_internals/extending_yosys/extensions.rst b/docs/source/yosys_internals/extending_yosys/extensions.rst index fa4ad51f8f4..f10c634b015 100644 --- a/docs/source/yosys_internals/extending_yosys/extensions.rst +++ b/docs/source/yosys_internals/extending_yosys/extensions.rst @@ -8,8 +8,6 @@ Writing extensions .. todo:: update to use :file:`/code_examples/extensions/test*.log` -.. todo:: should this be moved to yosys_source section? - This chapter contains some bits and pieces of information about programming yosys extensions. Don't be afraid to ask questions on the YosysHQ Slack. From 3317d80480e98539d44d474d7f85cab6f83be168 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 22 Aug 2024 10:04:00 +1200 Subject: [PATCH 13/14] Docs: Clarify verific caveats --- .../extending_yosys/build_verific.rst | 21 +++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/docs/source/yosys_internals/extending_yosys/build_verific.rst b/docs/source/yosys_internals/extending_yosys/build_verific.rst index ae453886f99..ae9e4f1d44a 100644 --- a/docs/source/yosys_internals/extending_yosys/build_verific.rst +++ b/docs/source/yosys_internals/extending_yosys/build_verific.rst @@ -17,12 +17,21 @@ The Yosys-Verific patch YosysHQ maintains and develops a patch for Verific in order to better integrate with Yosys and to provide features required by some of the formal verification -front-end tools. Synthesis from RTL may be possible without this patch, however -we are unable to provide support for any Yosys+Verific builds without it. To -license this patch for your own Yosys builds, `contact YosysHQ`_. +front-end tools. To license this patch for your own Yosys builds, `contact +YosysHQ`_. .. warning:: + While synthesis from RTL may be possible without this patch, YosysHQ provides + no guarantees of correctness and is unable to provide support. + +We recommend against using unpatched Yosys+Verific builds in conjunction with +the formal verification front-end tools unless you are familiar with their inner +workings. There are cases where the tools will appear to work, while producing +incorrect results. + +.. note:: + Some of the formal verification front-end tools may not be fully supported without the full TabbyCAD suite. If you are wanting to use these tools, including SBY, make sure to ask us if the Yosys-Verific patch is right for @@ -62,6 +71,10 @@ To find the compile options used for a given Yosys build, call ``yosys-config :start-at: --cxxflags :end-before: --linkflags +.. note:: + + The YosysHQ specific extensions are only available with the TabbyCAD suite. + Required Verific features ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -110,7 +123,7 @@ 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 | +--------------------------------------------------------------------------+-----+-----+-----+-----+ | Features | a | b | c | d | From 583d820dc2cd1ef9e385145452550ab71be9115f Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 23 Aug 2024 09:23:57 +1200 Subject: [PATCH 14/14] Docs: Apply verific docs suggestions --- .../using_yosys/more_scripting/load_design.rst | 5 +++-- docs/source/using_yosys/synthesis/memory.rst | 4 ++-- .../extending_yosys/build_verific.rst | 17 ++++++++--------- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/docs/source/using_yosys/more_scripting/load_design.rst b/docs/source/using_yosys/more_scripting/load_design.rst index cf6a1dc1f3f..bbc55a36bd2 100644 --- a/docs/source/using_yosys/more_scripting/load_design.rst +++ b/docs/source/using_yosys/more_scripting/load_design.rst @@ -30,8 +30,9 @@ keyword: Frontends .. note:: The Verific frontend for Yosys, which provides the :cmd:ref:`verific` - command, requires Yosys to be built with Verific. This is not the same as - simply having a Verific license when using Yosys. Check + command, requires Yosys to be built with Verific. For full functionality, + custom modifications to the Verific source code from YosysHQ are required, + but limited useability can be achieved with some stock Verific builds. Check :doc:`/yosys_internals/extending_yosys/build_verific` for more. Others: diff --git a/docs/source/using_yosys/synthesis/memory.rst b/docs/source/using_yosys/synthesis/memory.rst index 8306c82b9fb..e95a648757a 100644 --- a/docs/source/using_yosys/synthesis/memory.rst +++ b/docs/source/using_yosys/synthesis/memory.rst @@ -697,8 +697,8 @@ TDP with multiple read ports Patterns only supported with Verific ------------------------------------ -The following patterns are only supported when Yosys is built with the Verific -front-end. +The following patterns are only supported when the design is read in using the +Verific front-end. Synchronous SDP with write-first behavior via blocking assignments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/docs/source/yosys_internals/extending_yosys/build_verific.rst b/docs/source/yosys_internals/extending_yosys/build_verific.rst index ae9e4f1d44a..b20517bd3dd 100644 --- a/docs/source/yosys_internals/extending_yosys/build_verific.rst +++ b/docs/source/yosys_internals/extending_yosys/build_verific.rst @@ -33,9 +33,8 @@ incorrect results. .. note:: Some of the formal verification front-end tools may not be fully supported - without the full TabbyCAD suite. If you are wanting to use these tools, - including SBY, make sure to ask us if the Yosys-Verific patch is right for - you. + without the full TabbyCAD suite. If you want to use these tools, including + SBY, make sure to ask us if the Yosys-Verific patch is right for you. Compile options --------------- @@ -123,6 +122,12 @@ 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 | +--------------------------------------------------------------------------+-----+-----+-----+-----+ @@ -141,12 +146,6 @@ specific extensions of Verific library. | SystemVerilog + VHDL + RTL elaboration + Static elaboration + Hier tree | 1 | 1 | 1 | 0 | +--------------------------------------------------------------------------+-----+-----+-----+-----+ -Configuration values: - a. ``ENABLE_VERIFIC_SYSTEMVERILOG`` - b. ``ENABLE_VERIFIC_VHDL`` - c. ``ENABLE_VERIFIC_HIER_TREE`` - d. ``ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS`` - .. note:: In case your Verific build has EDIF and/or Liberty support, you can enable