From 14f2208e47573c56e6478333f8df320ce44081cb Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Wed, 17 Jan 2024 08:32:14 +1300
Subject: [PATCH] Docs: opt_expr

---
 docs/source/getting_started/example_synth.rst | 20 ++++++-------------
 docs/source/using_yosys/synthesis/opt.rst     | 14 +++++++++----
 2 files changed, 16 insertions(+), 18 deletions(-)

diff --git a/docs/source/getting_started/example_synth.rst b/docs/source/getting_started/example_synth.rst
index 3317656a1..e1cc257db 100644
--- a/docs/source/getting_started/example_synth.rst
+++ b/docs/source/getting_started/example_synth.rst
@@ -155,13 +155,6 @@ the register uses an ``$adff`` cell.  If we look at the terminal output we can
 also see all of the different ``proc_*`` commands being called.  We will look at
 each of these in more detail in :doc:`/using_yosys/synthesis/proc`.
 
-.. TODO:: intro ``opt_expr``
-   :doc:`/cmd/opt_expr`
-
-   - by default called at the end of :cmd:ref:`proc`
-   - can be disabled with ``-noopt``
-   - done here for... reasons?
-
 Notice how in the top left of :ref:`addr_gen_proc` we have a floating wire,
 generated from the initial assignment of 0 to the ``addr`` wire.  However, this
 initial assignment is not synthesizable, so this will need to be cleaned up
@@ -176,15 +169,14 @@ at the same time by separating them with a colon: :yoscrypt:`opt_expr; clean`.
 
    ``addr_gen`` module after :yoscrypt:`opt_expr; clean`
 
-You may also notice that the highlighted ``$eq`` cell input of ``255`` has been
-converted to ``8'11111111``.  Constant values are presented in the format
+You may also notice that the highlighted ``$eq`` cell input of ``255`` has
+changed to ``8'11111111``.  Constant values are presented in the format
 ``<bit_width>'<bits>``, with 32-bit values instead using the decimal number.
 This indicates that the constant input has been reduced from 32-bit wide to
-8-bit wide.  :cmd:ref:`opt_expr` performs simple expression rewriting and
-constant folding, which we discuss in more detail in
-:doc:`/using_yosys/synthesis/opt`.
-
-.. TODO:: why doesn't the 32-bit value 1 get converted to 1'1?
+8-bit wide.  This is a side-effect of running :cmd:ref:`opt_expr`, which
+performs constant folding and simple expression rewriting.    For more on why
+this happens, refer to :doc:`/using_yosys/synthesis/opt` and the :ref:`section
+on opt_expr <adv_opt_expr>`.
 
 .. note::
 
diff --git a/docs/source/using_yosys/synthesis/opt.rst b/docs/source/using_yosys/synthesis/opt.rst
index d60e17a48..219a139c1 100644
--- a/docs/source/using_yosys/synthesis/opt.rst
+++ b/docs/source/using_yosys/synthesis/opt.rst
@@ -21,10 +21,12 @@ to run this pass after each major step in the synthesis script.  As listed in
    :dedent:
    :caption: Passes called by :cmd:ref:`opt`
 
-Const folding and simple expression rewriting - :cmd:ref:`opt_expr`
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+.. _adv_opt_expr:
 
-This pass performs const folding on the internal combinational cell types
+Constant folding and simple expression rewriting - :cmd:ref:`opt_expr`
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+This pass performs constant folding on the internal combinational cell types
 described in :doc:`/yosys_internals/formats/cell_library`. This means a cell
 with all constant inputs is replaced with the constant value this cell drives.
 In some cases this pass can also optimize cells with some constant inputs.
@@ -69,7 +71,11 @@ with a buffer.
 
 Besides this basic const folding the :cmd:ref:`opt_expr` pass can replace 1-bit
 wide ``$eq`` and ``$ne`` cells with buffers or not-gates if one input is
-constant.
+constant.  Equality checks may also be reduced in size if there are redundant
+bits in the arguments (i.e. bits which are constant on both inputs).  This can,
+for example, result in a 32-bit wide constant like ``255`` being reduced to the
+8-bit value of ``8'11111111`` if the signal being compared is only 8-bit as in
+:ref:`addr_gen_clean` of :doc:`/getting_started/example_synth`.
 
 The :cmd:ref:`opt_expr` pass is very conservative regarding optimizing ``$mux``
 cells, as these cells are often used to model decision-trees and breaking these