diff --git a/docs/source/getting_started/installation.rst b/docs/source/getting_started/installation.rst index aea8b6a2dd2..4d1a2f36a58 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_internals/extending_yosys/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_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 582551f7486..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 - test_suites appendix diff --git a/docs/source/using_yosys/more_scripting/load_design.rst b/docs/source/using_yosys/more_scripting/load_design.rst index d64c50959bd..bbc55a36bd2 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 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: - :doc:`/cmd/read` 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/using_yosys/synthesis/memory.rst b/docs/source/using_yosys/synthesis/memory.rst index 0f5e1bd3010..e95a648757a 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 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/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_internals/extending_yosys/build_verific.rst b/docs/source/yosys_internals/extending_yosys/build_verific.rst new file mode 100644 index 00000000000..b20517bd3dd --- /dev/null +++ b/docs/source/yosys_internals/extending_yosys/build_verific.rst @@ -0,0 +1,153 @@ +Compiling with Verific library +============================== + +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 +----------------------- + +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. 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 want to use these tools, including + SBY, make sure to ask us if the Yosys-Verific patch is right for you. + +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. + +============== ========================== =============================== +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 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 + +.. note:: + + The YosysHQ specific extensions are only available with the TabbyCAD suite. + +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 + +.. 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. + +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``. + +Partially supported builds +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +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 +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 | ++--------------------------------------------------------------------------+-----+-----+-----+-----+ + +.. 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. 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/test_suites.rst b/docs/source/yosys_internals/extending_yosys/test_suites.rst similarity index 100% rename from docs/source/test_suites.rst rename to docs/source/yosys_internals/extending_yosys/test_suites.rst