diff --git a/docs/source/code_examples/intro/Makefile b/docs/source/code_examples/intro/Makefile
index c7507e934..90b91d7a5 100644
--- a/docs/source/code_examples/intro/Makefile
+++ b/docs/source/code_examples/intro/Makefile
@@ -2,7 +2,7 @@ PROGRAM_PREFIX :=
 
 YOSYS ?= ../../../../$(PROGRAM_PREFIX)yosys
 
-DOTS = counter_00.dot counter_01.dot counter_02.dot counter_03.dot
+DOTS = counter_00.dot counter_proc.dot counter_01.dot counter_02.dot counter_03.dot
 
 dots: $(DOTS)
 
diff --git a/docs/source/code_examples/intro/counter_outputs.ys b/docs/source/code_examples/intro/counter_outputs.ys
index a35c83d6f..d52934b3f 100644
--- a/docs/source/code_examples/intro/counter_outputs.ys
+++ b/docs/source/code_examples/intro/counter_outputs.ys
@@ -1,12 +1,13 @@
-# read design
+# read
 read_verilog counter.v
 hierarchy -check -top counter
-
 show -notitle -format dot -prefix counter_00
 
-# the high-level stuff
-proc; opt; memory; opt; fsm; opt
+# elaborate
+proc
+show -notitle -format dot -prefix counter_proc
 
+opt
 show -notitle -format dot -prefix counter_01
 
 # mapping to internal cell library
diff --git a/docs/source/getting_started/example_synth.rst b/docs/source/getting_started/example_synth.rst
new file mode 100644
index 000000000..9f61e9180
--- /dev/null
+++ b/docs/source/getting_started/example_synth.rst
@@ -0,0 +1,217 @@
+Synthesis starter
+-----------------
+
+A simple counter
+~~~~~~~~~~~~~~~~
+
+.. role:: yoscrypt(code)
+   :language: yoscrypt
+
+This section covers an example project available in
+``docs/source/code_examples/intro/*``.  The project contains a simple ASIC
+synthesis script (``counter.ys``), a digital design written in Verilog
+(``counter.v``), and a simple CMOS cell library (``mycells.lib``).
+
+First, let's quickly look at the design:
+
+.. literalinclude:: /code_examples/intro/counter.v
+   :language: Verilog
+   :caption: ``docs/source/code_examples/intro/counter.v``
+   :linenos:
+   :name: counter-v
+
+This is a simple counter with reset and enable.  If the reset signal, ``rst``,
+is high then the counter will reset to 0.  Otherwise, if the enable signal,
+``en``, is high then the ``count`` register will increment by 1 each rising edge
+of the clock, ``clk``.  
+
+Loading the design
+~~~~~~~~~~~~~~~~~~
+
+Let's load the design into Yosys.  From the command line, we can call ``yosys
+counter.v``.  This will open an interactive Yosys shell session and immediately
+parse the code from ``counter.v`` and convert it into an Abstract Syntax Tree
+(AST).  If you are interested in how this happens, there is more information in
+the document, :doc:`/yosys_internals/flow/verilog_frontend`.  For now, suffice
+it to say that we do this to simplify further processing of the design.  You
+should see something like the following:
+
+.. code:: console
+
+   $ yosys counter.v
+
+   -- Parsing `counter.v' using frontend ` -vlog2k' --
+
+   1. Executing Verilog-2005 frontend: counter.v
+   Parsing Verilog input from `counter.v' to AST representation.
+   Storing AST representation for module `$abstract\counter'.
+   Successfully finished Verilog frontend.
+
+Now that we are in the interactive shell, we can call Yosys commands directly.
+Let's run :yoscrypt:`hierarchy -check -top counter`.  This command declares that
+the top level module is ``counter``, and that we want to expand it and any other
+modules it may use.  Any other modules which were loaded are then discarded,
+stopping the following commands from trying to work on them.  By passing the
+``-check`` option there we are also telling the :cmd:ref:`hierarchy` command
+that if the design includes any non-blackbox modules without an implementation
+it should return an error.
+
+.. todo:: more on why :cmd:ref:`hierarchy` is important
+
+.. note::
+
+   :cmd:ref:`hierarchy` should always be the first command after the design has
+   been read.
+
+.. use doscon for a console-like display that supports the `yosys> [command]` format.
+
+.. code:: doscon
+
+   yosys> hierarchy -check -top counter
+
+   2. Executing HIERARCHY pass (managing design hierarchy).
+
+   3. Executing AST frontend in derive mode using pre-parsed AST for module `\counter'.
+   Generating RTLIL representation for module `\counter'.
+
+   3.1. Analyzing design hierarchy..
+   Top module:  \counter
+
+   3.2. Analyzing design hierarchy..
+   Top module:  \counter
+   Removing unused module `$abstract\counter'.
+   Removed 1 unused modules.
+
+Our circuit now looks like this:
+
+.. figure:: /_images/code_examples/intro/counter_00.*
+   :class: width-helper
+   :name: counter-hierarchy
+
+   ``counter`` module after :cmd:ref:`hierarchy`
+
+Elaboration
+~~~~~~~~~~~
+
+Notice that block that says "PROC" in :ref:`counter-hierarchy`?  Simple
+operations like ``count + 2'd1`` can be extracted from our ``always @`` block in
+:ref:`counter-v`.  This gives us the ``$add`` cell we see.  But control logic,
+like the ``if .. else``; and memory elements, like the ``count <='2d0``; are not
+so straightforward. To handle these, let us now introduce a new command:
+:doc:`/cmd/proc`.
+
+:cmd:ref:`proc` is a macro command; running a series of other commands which
+work to convert the behavioral logic of processes into multiplexers and
+registers.  We go into more detail on :cmd:ref:`proc` later in
+:doc:`/using_yosys/synthesis/proc`, but for now let's see what happens when we
+run it.
+
+.. figure:: /_images/code_examples/intro/counter_proc.*
+   :class: width-helper
+
+   ``counter`` module after :cmd:ref:`proc`
+
+The ``if`` statements are now modeled with ``$mux`` cells, and the memory
+consists of a ``$dff`` cell.  That's getting a bit messy now, so let's chuck in
+a call to :cmd:ref:`opt`.
+
+.. figure:: /_images/code_examples/intro/counter_01.*
+   :class: width-helper
+
+   ``counter`` module after :cmd:ref:`opt`
+
+Much better.  We can now see that the ``$dff`` and ``$mux`` cells have been
+replaced with a single ``$sdffe``, using the built-in enable and reset ports
+instead.
+
+.. todo:: a bit more on :cmd:ref:`opt` here
+
+At this stage of a synthesis flow there are a few other commands we could run.
+First off is :cmd:ref:`flatten`.  If we had any modules within our ``counter``,
+this would replace them with their implementation.  Flattening the design like
+this can allow for optimizations between modules which would otherwise be
+missed.  Next is :doc:`/cmd/check`.
+
+Depending on the target architecture, we might also run commands such as
+:cmd:ref:`tribuf` with the ``-logic`` option and :cmd:ref:`deminout`.  These
+remove tristate and inout constructs respectively, replacing them with logic
+suitable for mapping to an FPGA.
+
+The coarse-grain representation
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+At this stage, the design is in coarse-grain representation.  It still looks
+recognizable, and cells are word-level operators with parametrizable width.
+There isn't much else we can do for our ``counter`` example, but this is the
+stage of synthesis where we do things like const propagation, expression
+rewriting, and trimming unused parts of wires.
+
+This is also where we convert our FSMs and hard blocks like DSPs or memories.
+Such elements have to be inferred from patterns in the design and there are
+special passes for each.  Detection of these patterns can also be affected by
+optimizations and other transformations done previously.
+
+.. todo:: talk more about DSPs (and their associated commands)
+
+Some of the commands we might use here are:
+
+- :doc:`/cmd/fsm`,
+- :doc:`/cmd/memory`,
+- :doc:`/cmd/wreduce`,
+- :doc:`/cmd/peepopt`,
+- :doc:`/cmd/alumacc`, and
+- :doc:`/cmd/share`.
+
+Techmap
+~~~~~~~
+
+:yoscrypt:`techmap` - Map coarse-grain RTL cells (adders, etc.) to fine-grain
+logic gates (AND, OR, NOT, etc.).
+
+.. literalinclude:: /code_examples/intro/counter.ys
+   :language: yoscrypt
+   :lines: 8-9
+
+Result:
+
+.. figure:: /_images/code_examples/intro/counter_02.*
+   :class: width-helper
+
+   ``counter`` after :cmd:ref:`techmap`
+
+Mapping to hardware
+~~~~~~~~~~~~~~~~~~~
+
+:ref:`cmos_lib`
+
+#. :yoscrypt:`dfflibmap -liberty mycells.lib` - Map registers to available
+   hardware flip-flops.
+#. :yoscrypt:`abc -liberty mycells.lib` - Map logic to available hardware gates.
+
+.. figure:: /_images/code_examples/intro/counter_03.*
+   :class: width-helper
+
+   ``counter`` after hardware cell mapping
+
+.. _cmos_lib:
+
+The CMOS cell library
+^^^^^^^^^^^^^^^^^^^^^
+
+.. literalinclude:: /code_examples/intro/mycells.lib
+   :language: Liberty
+   :caption: ``docs/source/code_examples/intro/mycells.lib``
+
+The script file
+~~~~~~~~~~~~~~~
+
+#. :yoscrypt:`read_verilog -defer counter.v`
+#. :yoscrypt:`clean` - Clean up the design (just the last step of
+   :cmd:ref:`opt`).
+#. :yoscrypt:`write_verilog synth.v` - Write final synthesis result to output
+   file.
+
+.. literalinclude:: /code_examples/intro/counter.ys
+   :language: yoscrypt
+   :caption: ``docs/source/code_examples/intro/counter.ys``
+
diff --git a/docs/source/getting_started/examples.rst b/docs/source/getting_started/examples.rst
deleted file mode 100644
index 5e1b0e429..000000000
--- a/docs/source/getting_started/examples.rst
+++ /dev/null
@@ -1,146 +0,0 @@
-Example(s)
-----------
-
-.. _sec:typusecase:
-
-Typical use case
-~~~~~~~~~~~~~~~~
-
-The following example script may be used in a synthesis flow to convert the
-behavioural Verilog code from the input file design.v to a gate-level netlist
-synth.v using the cell library described by the Liberty file :
-
-.. code:: yoscrypt
-   :number-lines:
-
-   #. read input file to internal representation
-   read_verilog design.v
-
-   #. convert high-level behavioral parts ("processes") to d-type flip-flops and muxes
-   proc
-
-   #. perform some simple optimizations
-   opt
-
-   #. convert high-level memory constructs to d-type flip-flops and multiplexers
-   memory
-
-   #. perform some simple optimizations
-   opt
-
-   #. convert design to (logical) gate-level netlists
-   techmap
-
-   #. perform some simple optimizations
-   opt
-
-   #. map internal register types to the ones from the cell library
-   dfflibmap -liberty cells.lib
-
-   #. use ABC to map remaining logic to cells from the cell library
-   abc -liberty cells.lib
-
-   #. cleanup
-   opt
-
-   #. write results to output file
-   write_verilog synth.v
-
-A detailed description of the commands available in Yosys can be found in
-:ref:`cmd_ref`.
-
-Simple synthesis script
-~~~~~~~~~~~~~~~~~~~~~~~
-
-This section covers an example project available in
-``docs/source/code_examples/intro/*``.  The project contains a simple ASIC
-synthesis script (``counter.ys``), a digital design written in Verilog
-(``counter.v``), and a simple CMOS cell library (``mycells.lib``).
-
-.. literalinclude:: /code_examples/intro/counter.ys
-   :language: yoscrypt
-   :caption: ``docs/source/code_examples/intro/counter.ys``
-
-.. role:: yoscrypt(code)
-   :language: yoscrypt
-
-#. :yoscrypt:`read_verilog counter.v` - Read Verilog source file and convert to
-   internal representation.
-#. :yoscrypt:`hierarchy -check -top counter` - Elaborate the design hierarchy.
-   Should always be the first command after reading the design. Can re-run AST front-end.
-#. :yoscrypt:`proc` - Convert ``processes`` (the internal representation of
-   behavioral Verilog code) into multiplexers and registers.
-#. :yoscrypt:`opt` - Perform some basic optimizations and cleanups.
-#. :yoscrypt:`fsm` - Analyze and optimize finite state machines.
-#. :yoscrypt:`opt` - Perform some basic optimizations and cleanups.
-#. :yoscrypt:`memory` - Analyze memories and create circuits to implement them.
-#. :yoscrypt:`opt` - Perform some basic optimizations and cleanups.
-#. :yoscrypt:`techmap` - Map coarse-grain RTL cells (adders, etc.) to fine-grain
-   logic gates (AND, OR, NOT, etc.).
-#. :yoscrypt:`opt` - Perform some basic optimizations and cleanups.
-#. :yoscrypt:`dfflibmap -liberty mycells.lib` - Map registers to available
-   hardware flip-flops.
-#. :yoscrypt:`abc -liberty mycells.lib` - Map logic to available hardware gates.
-#. :yoscrypt:`clean` - Clean up the design (just the last step of
-   :cmd:ref:`opt`).
-#. :yoscrypt:`write_verilog synth.v` - Write final synthesis result to output
-   file.
-
-Running the script
-^^^^^^^^^^^^^^^^^^
-
-.. literalinclude:: /code_examples/intro/counter.v
-   :language: Verilog
-   :caption: ``docs/source/code_examples/intro/counter.v``
-
-.. literalinclude:: /code_examples/intro/mycells.lib
-   :language: Liberty
-   :caption: ``docs/source/code_examples/intro/mycells.lib``
-
-Step 1
-""""""
-
-.. literalinclude:: /code_examples/intro/counter.ys
-   :language: yoscrypt
-   :lines: 1-3
-
-Result:
-
-.. figure:: /_images/code_examples/intro/counter_00.*
-    :class: width-helper
-
-Step 2
-""""""
-
-.. literalinclude:: /code_examples/intro/counter.ys
-   :language: yoscrypt
-   :lines: 5-6
-
-Result:
-
-.. figure:: /_images/code_examples/intro/counter_01.*
-    :class: width-helper
-
-Step 3
-""""""
-
-.. literalinclude:: /code_examples/intro/counter.ys
-   :language: yoscrypt
-   :lines: 8-9
-
-Result:
-
-.. figure:: /_images/code_examples/intro/counter_02.*
-    :class: width-helper
-
-Step 4
-""""""
-
-.. literalinclude:: /code_examples/intro/counter.ys
-   :language: yoscrypt
-   :lines: 11-18
-
-Result:
-
-.. figure:: /_images/code_examples/intro/counter_03.*
-    :class: width-helper
diff --git a/docs/source/getting_started/index.rst b/docs/source/getting_started/index.rst
index 0828adf39..2f89a71cd 100644
--- a/docs/source/getting_started/index.rst
+++ b/docs/source/getting_started/index.rst
@@ -2,9 +2,8 @@ Getting started with Yosys
 ==========================
 
 .. toctree::
-	:maxdepth: 3
+   :maxdepth: 3
 
-	installation
-	scripting_intro
-	typical_phases
-	examples
+   installation
+   scripting_intro
+   example_synth
diff --git a/docs/source/getting_started/scripting_intro.rst b/docs/source/getting_started/scripting_intro.rst
index d5877917c..fd2aeee88 100644
--- a/docs/source/getting_started/scripting_intro.rst
+++ b/docs/source/getting_started/scripting_intro.rst
@@ -7,8 +7,7 @@ Yosys reads and processes commands from synthesis scripts, command line
 arguments and an interactive command prompt. Yosys commands consist of a command
 name and an optional whitespace separated list of arguments. Commands are
 terminated using the newline character or a semicolon (;). Empty lines and lines
-starting with the hash sign (#) are ignored. See :ref:`sec:typusecase` for an
-example synthesis script.
+starting with the hash sign (#) are ignored. Also see :doc:`example_synth`.
 
 The command :cmd:ref:`help` can be used to access the command reference manual,
 with ``help <command>`` providing details for a specific command.  ``yosys -H``
diff --git a/docs/source/getting_started/typical_phases.rst b/docs/source/getting_started/typical_phases.rst
index 64f76cd4e..d6cf89be5 100644
--- a/docs/source/getting_started/typical_phases.rst
+++ b/docs/source/getting_started/typical_phases.rst
@@ -168,7 +168,7 @@ The command :cmd:ref:`clean` can be used as alias for :cmd:ref:`opt_clean`. And
     hierarchy; proc; opt; memory; opt_expr;; fsm;;
 
 Example
-"""""""
+^^^^^^^
 
 .. todo:: describe ``opt`` images
 
@@ -217,7 +217,7 @@ Example
    :caption: ``docs/source/code_examples/synth_flow/opt_04.ys``
 
 When to use :cmd:ref:`opt` or :cmd:ref:`clean`
-""""""""""""""""""""""""""""""""""""""""""""""
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 Usually it does not hurt to call :cmd:ref:`opt` after each regular command in
 the synthesis script. But it increases the synthesis time, so it is favourable
diff --git a/docs/source/using_yosys/index.rst b/docs/source/using_yosys/index.rst
index fd8b2171f..d254df76f 100644
--- a/docs/source/using_yosys/index.rst
+++ b/docs/source/using_yosys/index.rst
@@ -4,6 +4,6 @@ Using Yosys (advanced)
 .. toctree:: 
 	:maxdepth: 2
 
+	synthesis/index
 	more_scripting/index
-	memory_mapping
 	yosys_flows
diff --git a/docs/source/using_yosys/more_scripting/index.rst b/docs/source/using_yosys/more_scripting/index.rst
index 8fb460613..f16298ce0 100644
--- a/docs/source/using_yosys/more_scripting/index.rst
+++ b/docs/source/using_yosys/more_scripting/index.rst
@@ -4,8 +4,6 @@ More scripting
 .. toctree::
 	:maxdepth: 3
 
-	opt_passes
 	selections
 	interactive_investigation
-	synth
 	troubleshooting
diff --git a/docs/source/using_yosys/synthesis/index.rst b/docs/source/using_yosys/synthesis/index.rst
new file mode 100644
index 000000000..b8dba55e9
--- /dev/null
+++ b/docs/source/using_yosys/synthesis/index.rst
@@ -0,0 +1,10 @@
+Synthesis in detail
+-------------------
+
+.. toctree::
+   :maxdepth: 3
+
+   synth
+   opt_passes
+   proc
+   memory_mapping
diff --git a/docs/source/using_yosys/memory_mapping.rst b/docs/source/using_yosys/synthesis/memory_mapping.rst
similarity index 100%
rename from docs/source/using_yosys/memory_mapping.rst
rename to docs/source/using_yosys/synthesis/memory_mapping.rst
diff --git a/docs/source/using_yosys/more_scripting/opt_passes.rst b/docs/source/using_yosys/synthesis/opt_passes.rst
similarity index 100%
rename from docs/source/using_yosys/more_scripting/opt_passes.rst
rename to docs/source/using_yosys/synthesis/opt_passes.rst
diff --git a/docs/source/using_yosys/synthesis/proc.rst b/docs/source/using_yosys/synthesis/proc.rst
new file mode 100644
index 000000000..1d7b823be
--- /dev/null
+++ b/docs/source/using_yosys/synthesis/proc.rst
@@ -0,0 +1,4 @@
+The :cmd:ref:`proc` command
+---------------------------
+
+text
diff --git a/docs/source/using_yosys/more_scripting/synth.rst b/docs/source/using_yosys/synthesis/synth.rst
similarity index 100%
rename from docs/source/using_yosys/more_scripting/synth.rst
rename to docs/source/using_yosys/synthesis/synth.rst