doc: add 'Convert (V)HDL to other formats'

1 files changed, 72 insertions, 21 deletions

diff --git a/doc/using/Synthesis.rst b/doc/using/Synthesis.rst
index 65e206274..582c7b425 100644
--- a/doc/using/Synthesis.rst
+++ b/doc/using/Synthesis.rst
@@ -7,29 +7,16 @@ Synthesis
 .. WARNING::
    This is experimental and work in progress! If you find crashes or unsupported features, please :ref:`report them <reporting_bugs>`!
 
-Since ``v0.37``, GHDL features a built-in (experimental) synthesis kernel with two backends: ``synth`` and ``yosys-plugin``. Currently, synthesis is supported as a front-end of other synthesis and technology mapping tools.
+Since ``v0.37``, GHDL features a built-in (experimental) synthesis kernel with two backends: ``synth`` and ``yosys-plugin``.
+Currently, synthesis is supported as a front-end of other synthesis and technology mapping tools.
 Hence, the netlists generated by GHDL are not optimised.
 
-.. NOTE::
-   Due to GHDL's modular architecture (see :ref:`INT:Overview`), the synthesis kernel shares the VHDL parsing front-end with the simulation back-ends. Hence, available options for synthesis are the same as for analysis and/or simulation elaboration (see :ref:`GHDL:options`).
-
-.. HINT::
-   Multiple pragmas are supported for preventing blocks of code from being synthesized:
-
-   ``-- pragma|synopsys|synthesis (synthesis|translate)( |_)(on|off)``
-
-   For example:
-
-   - ``-- pragma translate off``
-   - ``-- synthesis translate_on``
-   - ``-- synopsys synthesis_off``
-
 .. index:: synthesis command
 
 .. _Synth:command:
 
 Synthesis [``--synth``]
-=======================
+***********************
 
 .. HINT::
    This command is useful for checking that a design can be synthesized, before actually running a complete synthesis
@@ -61,9 +48,22 @@ See :ghdlsharp:`1174` for on-going discussion about other output formats.
 .. _synthesis_options:
 
 Synthesis options
-==================
+*****************
+
+.. HINT::
+   Multiple pragmas are supported for preventing blocks of code from being synthesized:
+
+   ``-- pragma|synopsys|synthesis (synthesis|translate)( |_)(on|off)``
 
-In addition to analyze options, there are some synthesis specific options.
+   For example:
+
+   - ``-- pragma translate off``
+   - ``-- synthesis translate_on``
+   - ``-- synopsys synthesis_off``
+
+Due to GHDL's modular architecture (see :ref:`INT:Overview`), the synthesis kernel shares the VHDL parsing front-end with the
+simulation back-ends. Hence, available options for synthesis are the same as for analysis and/or simulation elaboration
+(see :ref:`GHDL:options`). In addition to those options, there are some synthesis specific options.
 
 .. option:: -gNAME=VALUE
 
@@ -101,12 +101,12 @@ In addition to analyze options, there are some synthesis specific options.
 .. TIP::
   Furthermore there are lot of debug options available. Beware: these debug options should only used
   for debugging purposes as they aren't guaranteed to be stable during development of GHDL's synthesis feature.
-  You can find them in the file :ghdlsrc:`ghdlsynth.adb <src/ghdldrv/ghdlsynth.adb>` in the procedure ``Decode_Option()``.
+  You can find them in the file :ghdlsrc:`ghdlsynth.adb <ghdldrv/ghdlsynth.adb>` in the procedure ``Decode_Option()``.
 
 .. _Synth:plugin:
 
 Yosys plugin
-============
+************
 
 `ghdl-yosys-plugin <https://github.com/ghdl/ghdl-yosys-plugin>`_ is a module to use GHDL as a VHDL front-end for `Yosys
 Open Synthesis Suite <http://www.clifford.at/yosys/>`_, a framework for optimised synthesis and technology mapping.
@@ -120,4 +120,55 @@ depending of how is the plugin built. See `README <https://github.com/ghdl/ghdl-
 guidelines.
 
 .. HINT::
-   ghdl-yosys-plugin is a thin layer that converts the internal representation of :option:`--synth` to Yosys' C API. Hence, it is suggested to check the designs with :option:`--synth` before running synthesis with Yosys.
+   ghdl-yosys-plugin is a thin layer that converts the internal representation of :option:`--synth` to Yosys' C API. Hence,
+   it is suggested to check the designs with :option:`--synth` before running synthesis with Yosys.
+
+Convert (V)HDL to other formats
+===============================
+
+Yosys provides ``write_*`` commands for generating output netlists in different formats. Therefore, VHDL and/or Verilog
+sources can be converted to EDIF, SMT, BTOR2, etc.
+
+.. HINT:: For a comprehensive list of supported output formats (AIGER, BLIF, ILANG, JSON...), check out the
+  `Yosys documentation <http://www.clifford.at/yosys/documentation.html>`_.
+
+To Verilog
+----------
+
+.. code-block:: shell
+
+    yosys -m ghdl -p 'ghdl filename.vhdl -e unit_name; write_verilog filename.v'
+
+To EDIF
+-------
+
+.. code-block:: shell
+
+    yosys -m ghdl -p 'ghdl filename.vhdl -e unit_name; write_edif filename.edif'
+
+To SMT
+------
+
+.. code-block:: shell
+
+    yosys -m ghdl -p 'ghdl filename.vhdl -e unit_name; write_smt2 filename.smt2'
+
+To BTOR2
+--------
+
+.. code-block:: shell
+
+    yosys -m ghdl -p 'ghdl filename.vhdl -e unit_name; write_btor filename.btor'
+
+To FIRRTL
+---------
+
+.. code-block:: shell
+
+    yosys -m ghdl -p 'ghdl filename.vhdl -e unit_name; write_firrtl filename.firrtl'
+
+To VHDL
+-------
+
+There is work in progress in `ghdl/ghdl-yosys-plugin#122 <https://github.com/ghdl/ghdl-yosys-plugin/pull/122>`_ for adding
+a ``write_vhdl`` command to Yosys. That is the complement of what ghdl-yosys-plugin provides.