Docs: some restructure of advanced section

- Filling out index descriptions for `using_yosys` and `using_yosys/synthesis`.
- To discourage skipping over these index pages, the toctree in
  `using_yosys/index` is hidden and instead has inline links to the two
  subsections.
- Tidying todos.
- Moves technology mapping to `techmap_synth`, leaving the techmap by example in
  the internals section. `yosys_flows` gets split up, with the coarse-grain
  intro replaced by `synthesis/index`, the extract pass moving to
  `synthesis/extract` and model checking to `more_scripting/model_checking`.

docs/source/index.rst

@@ -34,6 +34,7 @@ available, go to :ref:`commandindex`.
 
 .. toctree::
    :maxdepth: 3
+   :includehidden:
 
    introduction
    getting_started/index

docs/source/using_yosys/index.rst

@@ -1,11 +1,17 @@
 Using Yosys (advanced)
 ======================
 
-.. todo:: brief overview for the using Yosys index
+While much of Yosys is focused around synthesis, there are also a number of
+other useful things that can be accomplished with Yosys scripts or in an
+interactive shell.  As such this section is broken into two parts:
+:doc:`/using_yosys/synthesis/index` expands on the
+:doc:`/getting_started/example_synth` and goes into further detail on the major
+commands used in synthesis; :doc:`/using_yosys/more_scripting/index` covers the
+ways Yosys can interact with designs for a deeper investigation.
 
 .. toctree::
    :maxdepth: 2
+   :hidden:
 
    synthesis/index
    more_scripting/index
-	yosys_flows

docs/source/using_yosys/more_scripting/index.rst

@@ -9,5 +9,6 @@ More scripting
    load_design
    selections
    interactive_investigation
+   model_checking
 
 .. troubleshooting

docs/source/using_yosys/more_scripting/model_checking.rst

@@ -0,0 +1,108 @@
+Symbolic model checking
+-----------------------
+
+.. todo:: check text context
+
+.. note:: 
+    
+    While it is possible to perform model checking directly in Yosys, it 
+    is highly recommended to use SBY or EQY for formal hardware verification.
+
+Symbolic Model Checking (SMC) is used to formally prove that a circuit has (or
+has not) a given property.
+
+One application is Formal Equivalence Checking: Proving that two circuits are
+identical. For example this is a very useful feature when debugging custom
+passes in Yosys.
+
+Other applications include checking if a module conforms to interface standards.
+
+The :cmd:ref:`sat` command in Yosys can be used to perform Symbolic Model
+Checking.
+
+Checking techmap
+~~~~~~~~~~~~~~~~
+
+.. todo:: add/expand supporting text
+
+Let's look at the following example:
+
+.. literalinclude:: /code_examples/synth_flow/techmap_01_map.v
+   :language: verilog
+   :caption: ``docs/source/code_examples/synth_flow/techmap_01_map.v``
+
+.. literalinclude:: /code_examples/synth_flow/techmap_01.v
+   :language: verilog
+   :caption: ``docs/source/code_examples/synth_flow/techmap_01.v``
+
+.. literalinclude:: /code_examples/synth_flow/techmap_01.ys
+   :language: yoscrypt
+   :caption: ``docs/source/code_examples/synth_flow/techmap_01.ys``
+
+To see if it is correct we can use the following code:
+
+.. todo:: replace inline yosys script code
+
+.. code:: yoscrypt
+
+    # read test design
+    read_verilog techmap_01.v
+    hierarchy -top test
+
+    # create two version of the design: test_orig and test_mapped
+    copy test test_orig
+    rename test test_mapped
+
+    # apply the techmap only to test_mapped
+    techmap -map techmap_01_map.v test_mapped
+
+    # create a miter circuit to test equivalence
+    miter -equiv -make_assert -make_outputs test_orig test_mapped miter
+    flatten miter
+
+    # run equivalence check
+    sat -verify -prove-asserts -show-inputs -show-outputs miter
+
+Result:
+
+.. code::
+
+    Solving problem with 945 variables and 2505 clauses..
+    SAT proof finished - no model found: SUCCESS!
+
+AXI4 Stream Master
+~~~~~~~~~~~~~~~~~~
+
+The following AXI4 Stream Master has a bug. But the bug is not exposed if the
+slave keeps ``tready`` asserted all the time. (Something a test bench might do.)
+
+Symbolic Model Checking can be used to expose the bug and find a sequence of
+values for ``tready`` that yield the incorrect behavior.
+
+.. todo:: add/expand supporting text
+
+.. literalinclude:: /code_examples/axis/axis_master.v
+   :language: verilog
+   :caption: ``docs/source/code_examples/axis/axis_master.v``
+
+.. literalinclude:: /code_examples/axis/axis_test.v
+   :language: verilog
+   :caption: ``docs/source/code_examples/axis/axis_test.v``
+
+.. literalinclude:: /code_examples/axis/axis_test.ys
+   :language: yoscrypt
+   :caption: ``docs/source/code_examples/axis/test.ys``
+
+Result with unmodified ``axis_master.v``:
+
+.. code::
+
+    Solving problem with 159344 variables and 442126 clauses..
+    SAT proof finished - model found: FAIL!
+
+Result with fixed ``axis_master.v``:
+
+.. code::
+
+    Solving problem with 159144 variables and 441626 clauses..
+    SAT proof finished - no model found: SUCCESS!

docs/source/using_yosys/synthesis/cell_libs.rst

@@ -73,8 +73,6 @@ Coarse-grain representation
 Logic gate mapping
 ~~~~~~~~~~~~~~~~~~
 
-.. TODO:: comment on similarities and/or differences with example_synth
-
 .. literalinclude:: /code_examples/intro/counter.ys
    :language: yoscrypt
    :lines: 14-15
@@ -89,8 +87,6 @@ Logic gate mapping
 Mapping to hardware
 ~~~~~~~~~~~~~~~~~~~
 
-.. todo:: are we recalling or is this new information
-
 For this example, we are using a Liberty file to describe a cell library which
 our internal cell library will be mapped to:
 

docs/source/using_yosys/synthesis/extract.rst

@@ -1,35 +1,5 @@
-Flows, command types, and order
-===============================
-
-Command order
--------------
-
-.. todo:: More surrounding text (esp as it relates to command order)
-
-Intro to coarse-grain synthesis
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-In coarse-grain synthesis the target architecture has cells of the same
-complexity or larger complexity than the internal RTL representation.
-
-For example:
-
-.. code:: verilog
-
-	wire [15:0] a, b;
-	wire [31:0] c, y;
-	assign y = a * b + c;
-
-This circuit contains two cells in the RTL representation: one multiplier and
-one adder. In some architectures this circuit can be implemented using
-a single circuit element, for example an FPGA DSP core. Coarse grain synthesis
-is this mapping of groups of circuit elements to larger components.
-
-Fine-grain synthesis would be matching the circuit elements to smaller
-components, such as LUTs, gates, or half- and full-adders.
-
 The extract pass
-~~~~~~~~~~~~~~~~
+----------------
 
 - Like the :cmd:ref:`techmap` pass, the :cmd:ref:`extract` pass is called with a
   map file. It compares the circuits inside the modules of the map file with the
@@ -256,112 +226,3 @@ Unwrap in ``test2``:
 
 .. figure:: /_images/code_examples/macc/macc_xilinx_test2e.*
     :class: width-helper
-
-Symbolic model checking
------------------------
-
-.. todo:: check text context
-
-.. note:: 
-    
-    While it is possible to perform model checking directly in Yosys, it 
-    is highly recommended to use SBY or EQY for formal hardware verification.
-
-Symbolic Model Checking (SMC) is used to formally prove that a circuit has (or
-has not) a given property.
-
-One application is Formal Equivalence Checking: Proving that two circuits are
-identical. For example this is a very useful feature when debugging custom
-passes in Yosys.
-
-Other applications include checking if a module conforms to interface standards.
-
-The :cmd:ref:`sat` command in Yosys can be used to perform Symbolic Model
-Checking.
-
-Checking techmap
-~~~~~~~~~~~~~~~~
-
-.. todo:: add/expand supporting text
-
-Let's look at the following example:
-
-.. literalinclude:: /code_examples/synth_flow/techmap_01_map.v
-   :language: verilog
-   :caption: ``docs/source/code_examples/synth_flow/techmap_01_map.v``
-
-.. literalinclude:: /code_examples/synth_flow/techmap_01.v
-   :language: verilog
-   :caption: ``docs/source/code_examples/synth_flow/techmap_01.v``
-
-.. literalinclude:: /code_examples/synth_flow/techmap_01.ys
-   :language: yoscrypt
-   :caption: ``docs/source/code_examples/synth_flow/techmap_01.ys``
-
-To see if it is correct we can use the following code:
-
-.. todo:: replace inline yosys script code
-
-.. code:: yoscrypt
-
-    # read test design
-    read_verilog techmap_01.v
-    hierarchy -top test
-
-    # create two version of the design: test_orig and test_mapped
-    copy test test_orig
-    rename test test_mapped
-
-    # apply the techmap only to test_mapped
-    techmap -map techmap_01_map.v test_mapped
-
-    # create a miter circuit to test equivalence
-    miter -equiv -make_assert -make_outputs test_orig test_mapped miter
-    flatten miter
-
-    # run equivalence check
-    sat -verify -prove-asserts -show-inputs -show-outputs miter
-
-Result:
-
-.. code::
-
-    Solving problem with 945 variables and 2505 clauses..
-    SAT proof finished - no model found: SUCCESS!
-
-AXI4 Stream Master
-~~~~~~~~~~~~~~~~~~
-
-The following AXI4 Stream Master has a bug. But the bug is not exposed if the
-slave keeps ``tready`` asserted all the time. (Something a test bench might do.)
-
-Symbolic Model Checking can be used to expose the bug and find a sequence of
-values for ``tready`` that yield the incorrect behavior.
-
-.. todo:: add/expand supporting text
-
-.. literalinclude:: /code_examples/axis/axis_master.v
-   :language: verilog
-   :caption: ``docs/source/code_examples/axis/axis_master.v``
-
-.. literalinclude:: /code_examples/axis/axis_test.v
-   :language: verilog
-   :caption: ``docs/source/code_examples/axis/axis_test.v``
-
-.. literalinclude:: /code_examples/axis/axis_test.ys
-   :language: yoscrypt
-   :caption: ``docs/source/code_examples/axis/test.ys``
-
-Result with unmodified ``axis_master.v``:
-
-.. code::
-
-    Solving problem with 159344 variables and 442126 clauses..
-    SAT proof finished - model found: FAIL!
-
-Result with fixed ``axis_master.v``:
-
-.. code::
-
-    Solving problem with 159144 variables and 441626 clauses..
-    SAT proof finished - no model found: SUCCESS!

docs/source/using_yosys/synthesis/index.rst

@@ -1,7 +1,24 @@
 Synthesis in detail
 -------------------
 
-.. todo:: brief overview for the synthesis index
+Synthesis can generally be broken down into coarse-grain synthesis, and
+fine-grain synthesis.  We saw this in :doc:`/getting_started/example_synth`
+where a design was loaded and elaborated and then went through a series of
+coarse-grain optimizations before being mapped to hard blocks and fine-grain
+cells.  Most commands in Yosys will target either coarse-grain representation or
+fine-grain representation, with only a select few compatible with both states.
+
+Commands such as :cmd:ref:`proc`, :cmd:ref:`fsm`, and :cmd:ref:`memory` rely on
+the additional information in the coarse-grain representation, along with a
+number of optimizations such as :cmd:ref:`wreduce`, :cmd:ref:`share`, and
+:cmd:ref:`alumacc`.  :cmd:ref:`opt` provides optimizations which are useful in
+both states, while :cmd:ref:`techmap` is used to convert coarse-grain cells
+to the corresponding fine-grain representation.
+
+Single-bit cells (logic gates, FFs) as well as LUTs, half-adders, and
+full-adders make up the bulk of the fine-grain representation and are necessary
+for commands such as :cmd:ref:`abc`\ /:cmd:ref:`abc9`, :cmd:ref:`simplemap`,
+:cmd:ref:`dfflegalize`, and :cmd:ref:`memory_map`.
 
 .. toctree::
    :maxdepth: 3
@@ -12,6 +29,7 @@ Synthesis in detail
    memory
    opt
    techmap_synth
+   extract
    abc
    cell_libs
 

docs/source/using_yosys/synthesis/synth.rst

@@ -1,6 +1,8 @@
 Synth commands
 --------------
 
+.. todo:: comment on common ``synth_*`` options, like ``-run``
+
 Packaged ``synth_*`` commands
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 

docs/source/using_yosys/synthesis/techmap_synth.rst

@@ -1,4 +1,107 @@
-techmap_synth
+Technology mapping 
--------------
+==================
 
-.. TODO:: techmap_synth
+.. todo:: less academic, check text is coherent
+
+Previous chapters outlined how HDL code is transformed into an RTL netlist. The
+RTL netlist is still based on abstract coarse-grain cell types like arbitrary
+width adders and even multipliers. This chapter covers how an RTL netlist is
+transformed into a functionally equivalent netlist utilizing the cell types
+available in the target architecture.
+
+Technology mapping is often performed in two phases. In the first phase RTL
+cells are mapped to an internal library of single-bit cells (see
+:ref:`sec:celllib_gates`). In the second phase this netlist of internal gate
+types is transformed to a netlist of gates from the target technology library.
+
+When the target architecture provides coarse-grain cells (such as block ram or
+ALUs), these must be mapped to directly form the RTL netlist, as information on
+the coarse-grain structure of the design is lost when it is mapped to bit-width
+gate types.
+
+Cell substitution
+-----------------
+
+The simplest form of technology mapping is cell substitution, as performed by
+the techmap pass. This pass, when provided with a Verilog file that implements
+the RTL cell types using simpler cells, simply replaces the RTL cells with the
+provided implementation.
+
+When no map file is provided, techmap uses a built-in map file that maps the
+Yosys RTL cell types to the internal gate library used by Yosys. The curious
+reader may find this map file as `techlibs/common/techmap.v` in the Yosys source
+tree.
+
+Additional features have been added to techmap to allow for conditional mapping
+of cells (see :doc:`/cmd/techmap`). This can for example be useful if the target
+architecture supports hardware multipliers for certain bit-widths but not for
+others.
+
+A usual synthesis flow would first use the techmap pass to directly map some RTL
+cells to coarse-grain cells provided by the target architecture (if any) and
+then use techmap with the built-in default file to map the remaining RTL cells
+to gate logic.
+
+Subcircuit substitution
+-----------------------
+
+Sometimes the target architecture provides cells that are more powerful than the
+RTL cells used by Yosys. For example a cell in the target architecture that can
+calculate the absolute-difference of two numbers does not match any single RTL
+cell type but only combinations of cells.
+
+For these cases Yosys provides the extract pass that can match a given set of
+modules against a design and identify the portions of the design that are
+identical (i.e. isomorphic subcircuits) to any of the given modules. These
+matched subcircuits are then replaced by instances of the given modules.
+
+The extract pass also finds basic variations of the given modules, such as
+swapped inputs on commutative cell types.
+
+In addition to this the extract pass also has limited support for frequent
+subcircuit mining, i.e. the process of finding recurring subcircuits in the
+design. This has a few applications, including the design of new coarse-grain
+architectures :cite:p:`intersynthFdlBookChapter`.
+
+The hard algorithmic work done by the extract pass (solving the isomorphic
+subcircuit problem and frequent subcircuit mining) is performed using the
+SubCircuit library that can also be used stand-alone without Yosys (see
+:ref:`sec:SubCircuit`).
+
+.. _sec:techmap_extern:
+
+Gate-level technology mapping
+-----------------------------
+
+.. todo:: newer techmap libraries appear to be largely ``.v`` instead of ``.lib``
+
+On the gate-level the target architecture is usually described by a "Liberty
+file". The Liberty file format is an industry standard format that can be used
+to describe the behaviour and other properties of standard library cells .
+
+Mapping a design utilizing the Yosys internal gate library (e.g. as a result of
+mapping it to this representation using the techmap pass) is performed in two
+phases.
+
+First the register cells must be mapped to the registers that are available on
+the target architectures. The target architecture might not provide all
+variations of d-type flip-flops with positive and negative clock edge,
+high-active and low-active asynchronous set and/or reset, etc. Therefore the
+process of mapping the registers might add additional inverters to the design
+and thus it is important to map the register cells first.
+
+Mapping of the register cells may be performed by using the dfflibmap pass. This
+pass expects a Liberty file as argument (using the -liberty option) and only
+uses the register cells from the Liberty file.
+
+Secondly the combinational logic must be mapped to the target architecture. This
+is done using the external program ABC via the abc pass by using the -liberty
+option to the pass. Note that in this case only the combinatorial cells are used
+from the cell library.
+
+Occasionally Liberty files contain trade secrets (such as sensitive timing
+information) that cannot be shared freely. This complicates processes such as
+reporting bugs in the tools involved. When the information in the Liberty file
+used by Yosys and ABC are not part of the sensitive information, the additional
+tool yosys-filterlib (see :ref:`sec:filterlib`) can be used to strip the
+sensitive information from the Liberty file.

docs/source/yosys_internals/techmap.rst

@@ -1,113 +1,3 @@
-.. _chapter:techmap:
-
-.. todo:: less academic, check text is coherent
-
-.. TODO:: can we split some of this into synthesis/techmap ?
-
-Technology mapping 
-==================
-
-Previous chapters outlined how HDL code is transformed into an RTL netlist. The
-RTL netlist is still based on abstract coarse-grain cell types like arbitrary
-width adders and even multipliers. This chapter covers how an RTL netlist is
-transformed into a functionally equivalent netlist utilizing the cell types
-available in the target architecture.
-
-Technology mapping is often performed in two phases. In the first phase RTL
-cells are mapped to an internal library of single-bit cells (see
-:ref:`sec:celllib_gates`). In the second phase this netlist of internal gate
-types is transformed to a netlist of gates from the target technology library.
-
-When the target architecture provides coarse-grain cells (such as block ram or
-ALUs), these must be mapped to directly form the RTL netlist, as information on
-the coarse-grain structure of the design is lost when it is mapped to bit-width
-gate types.
-
-Cell substitution
------------------
-
-The simplest form of technology mapping is cell substitution, as performed by
-the techmap pass. This pass, when provided with a Verilog file that implements
-the RTL cell types using simpler cells, simply replaces the RTL cells with the
-provided implementation.
-
-When no map file is provided, techmap uses a built-in map file that maps the
-Yosys RTL cell types to the internal gate library used by Yosys. The curious
-reader may find this map file as `techlibs/common/techmap.v` in the Yosys source
-tree.
-
-Additional features have been added to techmap to allow for conditional mapping
-of cells (see :doc:`/cmd/techmap`). This can for example be useful if the target
-architecture supports hardware multipliers for certain bit-widths but not for
-others.
-
-A usual synthesis flow would first use the techmap pass to directly map some RTL
-cells to coarse-grain cells provided by the target architecture (if any) and
-then use techmap with the built-in default file to map the remaining RTL cells
-to gate logic.
-
-Subcircuit substitution
------------------------
-
-Sometimes the target architecture provides cells that are more powerful than the
-RTL cells used by Yosys. For example a cell in the target architecture that can
-calculate the absolute-difference of two numbers does not match any single RTL
-cell type but only combinations of cells.
-
-For these cases Yosys provides the extract pass that can match a given set of
-modules against a design and identify the portions of the design that are
-identical (i.e. isomorphic subcircuits) to any of the given modules. These
-matched subcircuits are then replaced by instances of the given modules.
-
-The extract pass also finds basic variations of the given modules, such as
-swapped inputs on commutative cell types.
-
-In addition to this the extract pass also has limited support for frequent
-subcircuit mining, i.e. the process of finding recurring subcircuits in the
-design. This has a few applications, including the design of new coarse-grain
-architectures :cite:p:`intersynthFdlBookChapter`.
-
-The hard algorithmic work done by the extract pass (solving the isomorphic
-subcircuit problem and frequent subcircuit mining) is performed using the
-SubCircuit library that can also be used stand-alone without Yosys (see
-:ref:`sec:SubCircuit`).
-
-.. _sec:techmap_extern:
-
-Gate-level technology mapping
------------------------------
-
-On the gate-level the target architecture is usually described by a "Liberty
-file". The Liberty file format is an industry standard format that can be used
-to describe the behaviour and other properties of standard library cells .
-
-Mapping a design utilizing the Yosys internal gate library (e.g. as a result of
-mapping it to this representation using the techmap pass) is performed in two
-phases.
-
-First the register cells must be mapped to the registers that are available on
-the target architectures. The target architecture might not provide all
-variations of d-type flip-flops with positive and negative clock edge,
-high-active and low-active asynchronous set and/or reset, etc. Therefore the
-process of mapping the registers might add additional inverters to the design
-and thus it is important to map the register cells first.
-
-Mapping of the register cells may be performed by using the dfflibmap pass. This
-pass expects a Liberty file as argument (using the -liberty option) and only
-uses the register cells from the Liberty file.
-
-Secondly the combinational logic must be mapped to the target architecture. This
-is done using the external program ABC via the abc pass by using the -liberty
-option to the pass. Note that in this case only the combinatorial cells are used
-from the cell library.
-
-Occasionally Liberty files contain trade secrets (such as sensitive timing
-information) that cannot be shared freely. This complicates processes such as
-reporting bugs in the tools involved. When the information in the Liberty file
-used by Yosys and ABC are not part of the sensitive information, the additional
-tool yosys-filterlib (see :ref:`sec:filterlib`) can be used to strip the
-sensitive information from the Liberty file.
-
 Techmap by example
 ------------------