Progress on AppNote 011

4 files changed, 143 insertions, 58 deletions

diff --git a/manual/APPNOTE_011_Design_Investigation.tex b/manual/APPNOTE_011_Design_Investigation.tex
index 9791ef79..c5947922 100644
--- a/manual/APPNOTE_011_Design_Investigation.tex
+++ b/manual/APPNOTE_011_Design_Investigation.tex
@@ -61,11 +61,12 @@
 Yosys \cite{yosys} can be a great environment for building custom synthesis
 flows \cite{glaserwolf}. It can also be an excellent tool for teaching and
 learning Verilog based RTL synthesis. In both applications it is of great
-importance to be able to analyze the designs produces easily.
+importance to be able to analyze the designs it produces easily.
 
 This Yosys application note covers the generation of circuit diagrams with the
-Yosys {\tt show} command and the selection of interesting parts of the circuit
-using the {\tt select} command.
+Yosys {\tt show} command, the selection of interesting parts of the circuit
+using the {\tt select} command, and briefly discusses advanced commands for
+investigating the actual behavior of circuits.
 \end{abstract}
 
 \section{Installation and Prerequisites}
@@ -77,22 +78,24 @@ for generating the actual circuit diagrams. Yosys must be build with Qt
 support in order to activate the built-in SVG viewer. Alternatively an
 external viewer can be used.
 
-\section{Introduction to the {\tt show} command}
+\section{Overview}
 
-The {\tt show} command generates a circuit diagram for the design in its
-current state. Various options can be used to change the appearance of the
-circuit diagram, set the name and format for the output file, and so forth.
-When called without any special options, it saves the circuit diagram in
-a temporary file and launches {\tt yosys-svgviewer} to display the diagram.
-Subsequent calls to {\tt show} re-use the {\tt yosys-svgviewer} instance
-(if still running).
+This application note is structured as follows:
 
-Fig.~\ref{example_src} shows a simple synthesis script and Verilog file that
-demonstrates the usage of {\tt show} in a simple setting. Note that {\tt show}
-is called with the {\tt -pause} option, that halts execution of the Yosys
-script until the user presses the Enter key. The {\tt show -pause} command
-also allows the user to enter an interactive shell to further investigate the
-circuit before continuing synthesis.
+Sec.~\ref{intro_show} introduces the {\tt show} command and explains the
+symbols used in the circuit diagrams generated by it.
+
+Sec.~\ref{navigate} introduces additional commands used to navigate in the
+design and select portions of the design and print additional information on
+the elements in the design that are not contained in the circuit diagrams.
+
+Sec.~\ref{poke} introduces commands to evaluate the design and solve SAT
+problems within the design.
+
+Sec.~\ref{conclusion} concludes the document and summarizes the key points.
+
+\section{Introduction to the {\tt show} command}
+\label{intro_show}
 
 \begin{figure}[b]
 \begin{lstlisting}
@@ -116,6 +119,29 @@ endmodule
 \label{example_src}
 \end{figure}
 
+\begin{figure}[b!]
+\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_00.pdf}
+\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_01.pdf}
+\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_02.pdf}
+\caption{Output of the three {\tt show} commands from Fig.~\ref{example_src}}
+\label{example_out}
+\end{figure}
+
+The {\tt show} command generates a circuit diagram for the design in its
+current state. Various options can be used to change the appearance of the
+circuit diagram, set the name and format for the output file, and so forth.
+When called without any special options, it saves the circuit diagram in
+a temporary file and launches {\tt yosys-svgviewer} to display the diagram.
+Subsequent calls to {\tt show} re-use the {\tt yosys-svgviewer} instance
+(if still running).
+
+Fig.~\ref{example_src} shows a simple synthesis script and Verilog file that
+demonstrates the usage of {\tt show} in a simple setting. Note that {\tt show}
+is called with the {\tt -pause} option, that halts execution of the Yosys
+script until the user presses the Enter key. The {\tt show -pause} command
+also allows the user to enter an interactive shell to further investigate the
+circuit before continuing synthesis.
+
 So this script, when executed, will show the design after each of the three
 synthesis commands. The generated circuit diagrams are shown in Fig.~\ref{example_out}.
 
@@ -123,11 +149,9 @@ The first diagram (from top to bottom) shows the design directly after being
 read by the Verilog front-end. Input and output ports are visualized using
 octagonal shapes. Cells are visualized as rectangles with inputs on the left
 and outputs on the right side. The cell labels are two lines long: The first line
-contains the cell name (or a {\tt \_<number\_} placeholder for cells without
-a name from the original Verilog, such as cells created from Verilog
-expressions) and the second line contains the cell type. Internal cell types
-are prefixed with a dollar sign. The Yosys manual contains a chapter on the
-internal cell library used in Yosys.
+contains a unique identifier for the cell and the second line contains the cell
+type. Internal cell types are prefixed with a dollar sign. The Yosys manual
+contains a chapter on the internal cell library used in Yosys.
 
 Constants are shown as ellipses with the constant value as label. The syntax
 {\tt <bit\_width>'<bits>} is used for for constants that are not 32-bit wide
@@ -139,42 +163,31 @@ load. Signals that are multiple bits wide are shown as think arrows.
 
 Finally {\it processes\/} are shown in boxes with round corners. Processes
 are Yosys' internal representation of the decision-trees and synchronization
-events modelled in a Verilog {\tt always}-block. The label reads {\tt PROC} in the
-first line and contains the source code location of the original {\tt
-always}-block in the 2nd line. Not how the multiplexer from the {\tt ?:}-expression
-is represented as a {\tt \$mux} cell but the multiplexer from the {\tt if}-statement
-is yet still hidden within the process.
+events modelled in a Verilog {\tt always}-block. The label reads {\tt PROC}
+followed by a unique identifier in the first line and contains the source code
+location of the original {\tt always}-block in the 2nd line. Note how the
+multiplexer from the {\tt ?:}-expression is represented as a {\tt \$mux} cell
+but the multiplexer from the {\tt if}-statement is yet still hidden within the
+process.
 
 \medskip
 
 The {\tt proc} command transforms the process from the first diagram into a
 multiplexer and a d-type flip-flip, which brings us to the 2nd diagram.
 
-Note that the auto-generated numbers for the cells have changed since the first
-diagram, because they are just placeholders . We will cover how to avoid this
-later in this document.
-
-
-\begin{figure}[b!]
-\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_00.pdf}
-\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_01.pdf}
-\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_02.pdf}
-\caption{Output of the three {\tt show} commands from Fig.~\ref{example_src}}
-\label{example_out}
-\end{figure}
-
-Also note that the design now contains two instances of a {\tt BUF}-node. The
-Rhombus shape to the right is a dangling wire. (Wire nodes are only shown if
-they are dangling or have names assigned from the Verilog input.) This are
-artefacts left behind by the {\tt proc}-command. It is quite usual to see such
-artefacts after calling commands that perform changes in the design, as most
-commands only care about doing the transformation in a foolproof way, not about
-cleaning up after them. The next call to {\tt clean} (or {\tt opt}, which
-includes {\tt clean} as one of its operations) will clean up this artefacts.
-This operation is so common in Yosys scripts that it can simply be abbreviated
-by using the {\tt ;;} token, which doubles as separator for commands. Unless
-one wants to specifically analyze this artefacts left behind some operations,
-it is therefore recommended to call {\tt clean} before calling {\tt show}.
+The Rhombus shape to the right is a dangling wire. (Wire nodes are only shown
+if they are dangling or have "`public"' names, for example names assigned from
+the Verilog input.) Also note that the design now contains two instances of a
+{\tt BUF}-node. This are artefacts left behind by the {\tt proc}-command. It is
+quite usual to see such artefacts after calling commands that perform changes
+in the design, as most commands only care about doing the transformation in the
+least complicated way, not about cleaning up after them. The next call to {\tt
+clean} (or {\tt opt}, which includes {\tt clean} as one of its operations) will
+clean up this artefacts.  This operation is so common in Yosys scripts that it
+can simply be abbreviated by using the {\tt ;;} token, which doubles as
+separator for commands. Unless one wants to specifically analyze this artefacts
+left behind some operations, it is therefore recommended to call {\tt clean}
+before calling {\tt show}.
 
 \medskip
 
@@ -184,10 +197,12 @@ not only has removed the artifacts left behind by {\tt proc}, but also determine
 correctly that it can remove the first {\tt \$mux} cell without changing the behavior
 of the circuit.
 
+\medskip
+
 \begin{figure}[b!]
 \includegraphics[width=\linewidth,trim=0 2cm 0 0]{APPNOTE_011_Design_Investigation/splice.pdf}
 \caption{Output of {\tt yosys -p 'proc; opt; show' splice.v}}
-\label{example_src}
+\label{splice_dia}
 \end{figure}
 
 \begin{figure}[b!]
@@ -204,18 +219,79 @@ assign {y[11:4], y[1:0], y[3:2]} =
 endmodule
 \end{lstlisting}
 \caption{\tt splice.v}
-\label{example_src}
+\label{splice_src}
 \end{figure}
 
-\FIXME{} --- Splicing, Cell libraries
+\begin{figure}[t!]
+\includegraphics[height=\linewidth]{APPNOTE_011_Design_Investigation/cmos_00.pdf}
+\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/cmos_01.pdf}
+\caption{Effects of {\tt splitnets} command and of providing a cell library. (The
+circuit is a half-adder built from simple CMOS gates.)}
+\label{splitnets_libfile}
+\end{figure}
+
+As has been indicated in this example, Yosys is can manage signal vectors (aka.
+multi-bit wires or buses) as native objects. This provides great advantages
+when analyzing circuits that operate on wide integers. But it also introduces
+some additional complexity when the individual bits of of a signal vector need
+to be accessed. The example show in Fig.~\ref{splice_dia} and \ref{splice_src}
+demonstrates how such circuits are visualized by the {\tt show} command.
+
+The key elements in understanding this circuit diagram are of course the boxes
+with round corners and rows labeled {\tt <MSB\_LEFT>:<LSB\_LEFT> -- <MSB\_RIGHT>:<LSB\_RIGHT>}.
+Each of this boxes has one signal per row on one side and a common signal for all rows on the
+other side. The {\tt <MSB>:<LSB>} tuples specify which bits are broken out from the signals
+and are connected. So The top row of the box connecting the signals {\tt a} and {\tt b} indicates
+that the bit 0 (i.e. the range 0:0) from signal {\tt a} is connected to bit 1 (i.e. the range
+1:1) of signal {\tt x}.
+
+Lines connecting such boxes together and lines connecting such boxes to cell
+ports have slightly different look to emphasise that they are not actual signal
+wires but a necessity of the graphical representation. This distinction seems
+like a technicality, until one wants to debug a problem related to the way
+Yosys internally represents signal vectors, for example when writing custom
+Yosys commands.
+
+\medskip
+
+Finally Fig.~\ref{splitnets_libfile} shows two common pitfalls when working
+with designs mapped to a cell library. The top figure has two problems: First
+Yosys did not have access to the cell library when this diagram was generated,
+resulting in all cell ports defaulting to being inputs. This is why all ports
+are drawn on the left side the cells are awkwardly arranged in a large column.
+Secondly the two-bit vector {\tt y} requires breakout-boxes for its individual
+bits, resulting in an unnecessary complex diagram.
+
+For the 2nd diagram Yosys has been given a description of the cell library as
+Verilog file containing blackbox modules. There are two ways to load cell
+descriptions into Yosys: First the Verilog file for the cell library can be
+passed directly to the {\tt show} command using the {\tt -lib <filename>}
+option. Secondly it is possible to load cell libraries into the design with
+the {\tt read\_verilog -lib <filename>} command. The later option has the great 
+advantage that the library only needs to be loaded once and can then be used
+in all subsequent calls to the {\tt show} command.
+
+In addition to that the 2nd diagram was generated after {\tt splitnet -ports}
+was run on the design. This command splits all signal vectors into individual
+signals, which is often desirable when looking at gate-level circuits. The
+{\tt -ports} option is required to also split module ports. Per default the
+command only operates on interior signals.
+
 
 \section{Navigating the design}
+\label{navigate}
 
-\FIXME{} --- cd and ls, multi-page diagrams, select, cones and boolean operations
+\FIXME{} --- cd and ls, dump,  multi-page diagrams, select, cones and boolean operations
 
 \section{Advanced investigation techniques}
+\label{poke}
+
+\FIXME{} --- eval, sat
+
+\section{Conclusion}
+\label{conclusion}
 
-\FIXME{} --- dump, eval, sat
+\FIXME
 
 \begin{thebibliography}{9}
 
diff --git a/manual/APPNOTE_011_Design_Investigation/.gitignore b/manual/APPNOTE_011_Design_Investigation/.gitignore
index b6fb3068..81422061 100644
--- a/manual/APPNOTE_011_Design_Investigation/.gitignore
+++ b/manual/APPNOTE_011_Design_Investigation/.gitignore
@@ -1,4 +1,6 @@
 example_00.dot
 example_01.dot
 example_02.dot
+cmos_00.dot
+cmos_01.dot
 splice.dot
diff --git a/manual/APPNOTE_011_Design_Investigation/cmos.v b/manual/APPNOTE_011_Design_Investigation/cmos.v
new file mode 100644
index 00000000..2912c760
--- /dev/null
+++ b/manual/APPNOTE_011_Design_Investigation/cmos.v
@@ -0,0 +1,3 @@
+module cmos_demo(input a, b, output [1:0] y);
+assign y = a + b;
+endmodule
diff --git a/manual/APPNOTE_011_Design_Investigation/make.sh b/manual/APPNOTE_011_Design_Investigation/make.sh
index 60c6c6be..c4697098 100644
--- a/manual/APPNOTE_011_Design_Investigation/make.sh
+++ b/manual/APPNOTE_011_Design_Investigation/make.sh
@@ -1,8 +1,12 @@
 #!/bin/bash
 ../../yosys example.ys
 ../../yosys -p 'proc; opt; show -format dot -prefix splice' splice.v
-sed -i '/^label=/ d;' example_*.dot splice.dot
+../../yosys -p 'techmap; abc -liberty ../../techlibs/cmos/cmos_cells.lib;; show -format dot -prefix cmos_00' cmos.v
+../../yosys -p 'techmap; splitnets -ports; abc -liberty ../../techlibs/cmos/cmos_cells.lib;; show -lib ../../techlibs/cmos/cmos_cells.v -format dot -prefix cmos_01' cmos.v
+sed -i '/^label=/ d;' example_*.dot splice.dot cmos_*.dot
 dot -Tpdf -o example_00.pdf example_00.dot
 dot -Tpdf -o example_01.pdf example_01.dot
 dot -Tpdf -o example_02.pdf example_02.dot
 dot -Tpdf -o splice.pdf splice.dot
+dot -Tpdf -o cmos_00.pdf cmos_00.dot
+dot -Tpdf -o cmos_01.pdf cmos_01.dot