Merge pull request #4396 from YosysHQ/krys/docs_verific

Clarify Verific support where the `verific` front end is mentioned
Add page on building yosys+verific

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

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

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`

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.
+

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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 

docs/source/yosys_internals/extending_yosys/abc_flow.rst

@@ -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.

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.

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