\def\FIXME{{\color{red}\bf FIXME}}
-\lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=2em,xrightmargin=1em,numbers=left}
+\lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=0.7cm,xrightmargin=0.2cm,numbers=left}
\begin{document}
\title{Yosys Application Note 011: \\ Interactive Design Investigation}
-\author{Clifford Wolf \\ November 2013}
+\author{Clifford Wolf \\ Original Version December 2013}
\maketitle
\begin{abstract}
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.
+flows. 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 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 investigation
+commands for evaluating circuits and solving SAT problems.
\end{abstract}
\section{Installation and Prerequisites}
-This Application Note is based on GIT Rev. {\tt \FIXME} from \FIXME{} of
-Yosys \cite{yosys}. The {\tt README} file covers how to install Yosys. The
+This Application Note is based on the Yosys \cite{yosys} GIT Rev. {\tt 2b90ba1} from
+2013-12-08. The {\tt README} file covers how to install Yosys. The
{\tt show} command requires a working installation of GraphViz \cite{graphviz}
-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.
+and \cite{xdot} for generating the actual circuit diagrams.
-\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, 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}
\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 xdot} to display the diagram.
+Subsequent calls to {\tt show} re-use the {\tt xdot} instance
+(if still running).
+
+\subsection{A simple circuit}
+
+Fig.~\ref{example_src} shows a simple synthesis script and a Verilog file that
+demonstrate 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}.
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
+read by the Verilog front-end. Input and output ports are displayed as
+octagonal shapes. Cells are displayed 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
-and/or contain bits that are not 0 or 1 (but {\tt x} or {\tt z}). Ordinary
+and/or contain bits that are not 0 or 1 (i.e. {\tt x} or {\tt z}). Ordinary
32-bit constants are written using decimal numbers.
Single-bit signals are shown as thin arrows pointing from the driver to the
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 with 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 always call {\tt clean}
+before calling {\tt show}.
\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!]
+\lstinputlisting{APPNOTE_011_Design_Investigation/splice.v}
+\caption{\tt splice.v}
+\label{splice_src}
+\end{figure}
+
+\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}
+
+\subsection{Break-out boxes for signal vectors}
+
+As has been indicated by the last 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
+are 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 of the signals are broken out
+and connected. So the top row of the box connecting the signals {\tt a} and {\tt x} 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 a 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.
+
+\subsection{Gate level netlists}
+
+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 2nd method 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
+signal bits, 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.
+
+\subsection{Miscellaneous notes}
+
+Per default the {\tt show} command outputs a temporary {\tt dot} file and launches
+{\tt xdot} to display it. The options {\tt -format}, {\tt -viewer}
+and {\tt -prefix} can be used to change format, viewer and filename prefix.
+Note that the {\tt pdf} and {\tt ps} format are the only formats that support
+plotting multiple modules in one run.
+
+In densely connected circuits it is sometimes hard to keep track of the
+individual signal wires. For this cases it can be useful to call {\tt show}
+with the {\tt -colors <integer>} argument, which randomly assigns colors to the
+nets. The integer (> 0) is used as seed value for the random color
+assignments. Sometimes it is necessary it try some values to find an assignment
+of colors that looks good.
+
+The command {\tt help show} prints a complete listing of all options supported
+by the {\tt show} command.
+
+\section{Navigating the design}
+\label{navigate}
+
+Plotting circuit diagrams for entire modules in the design brings us only helps
+in simple cases. For complex modules the generated circuit diagrams are just stupidly big
+and are no help at all. In such cases one first has to select the relevant
+portions of the circuit.
+
+In addition to {\it what\/} to display one also needs to carefully decide
+{\it when\/} to display it, with respect to the synthesis flow. In general
+it is a good idea to troubleshoot a circuit in the earliest state in which
+a problem can be reproduced. So if, for example, the internal state before calling
+the {\tt techmap} command already fails to verify, it is better to troubleshoot
+the coarse-grain version of the circuit before {\tt techmap} than the gate-level
+circuit after {\tt techmap}.
+
+\medskip
+
+Note: It is generally recommended to verify the internal state of a design by
+writing it to a Verilog file using {\tt write\_verilog -noexpr} and using the
+simulation models from {\tt simlib.v} and {\tt simcells.v} from the Yosys data
+directory (as printed by {\tt yosys-config -{}-datdir}).
+
+\subsection{Interactive Navigation}
+
+\begin{figure}
\begin{lstlisting}
-module splice_demo(a, b, c, d, e, f, x, y);
+yosys> ls
-input [1:0] a, b, c, d, e, f;
-output [1:0] x = {a[0], a[1]};
+1 modules:
+ example
-output [11:0] y;
-assign {y[11:4], y[1:0], y[3:2]} =
- {a, b, -{c, d}, ~{e, f}};
+yosys> cd example
-endmodule
+yosys [example]> ls
+
+7 wires:
+ $0\y[1:0]
+ $add$example.v:5$2_Y
+ a
+ b
+ c
+ clk
+ y
+
+3 cells:
+ $add$example.v:5$2
+ $procdff$7
+ $procmux$5
\end{lstlisting}
-\caption{\tt splice.v}
-\label{example_src}
+\caption{Demonstration of {\tt ls} and {\tt cd} using {\tt example.v} from Fig.~\ref{example_src}}
+\label{lscd}
\end{figure}
-\FIXME{} --- Splicing, Cell libraries
+\begin{figure}[b]
+\begin{lstlisting}
+ attribute \src "example.v:5"
+ cell $add $add$example.v:5$2
+ parameter \A_SIGNED 0
+ parameter \A_WIDTH 1
+ parameter \B_SIGNED 0
+ parameter \B_WIDTH 1
+ parameter \Y_WIDTH 2
+ connect \A \a
+ connect \B \b
+ connect \Y $add$example.v:5$2_Y
+ end
+\end{lstlisting}
+\caption{Output of {\tt dump \$2} using the design from Fig.~\ref{example_src} and Fig.~\ref{example_out}}
+\label{dump2}
+\end{figure}
-\section{Navigating the design}
+Once the right state within the synthesis flow for debugging the circuit has
+been identified, it is recommended to simply add the {\tt shell} command
+to the matching place in the synthesis script. This command will stop the
+synthesis at the specified moment and go to shell mode, where the user can
+interactively enter commands.
+
+For most cases, the shell will start with the whole design selected (i.e. when
+the synthesis script does not already narrow the selection). The command {\tt
+ls} can now be used to create a list of all modules. The command {\tt cd} can
+be used to switch to one of the modules (type {\tt cd ..} to switch back). Now
+the {\tt ls} command lists the objects within that module. Fig.~\ref{lscd}
+demonstrates this using the design from Fig.~\ref{example_src}.
+
+There is a thing to note in Fig.~\ref{lscd}: We can see that the cell names
+from Fig.~\ref{example_out} are just abbreviations of the actual cell names,
+namely the part after the last dollar-sign. Most auto-generated names (the ones
+starting with a dollar sign) are rather long and contains some additional
+information on the origin of the named object. But in most cases those names
+can simply be abbreviated using the last part.
+
+Usually all interactive work is done with one module selected using the {\tt cd}
+command. But it is also possible to work from the design-context ({\tt cd ..}). In
+this case all object names must be prefixed with {\tt <module\_name>/}. For
+example {\tt a*/b*} would refer to all objects whose names start with {\tt b} from
+all modules whose names start with {\tt a}.
+
+The {\tt dump} command can be used to print all information about an object.
+For example {\tt dump \$2} will print Fig.~\ref{dump2}. This can for example
+be useful to determine the names of nets connected to cells, as the net-names
+are usually suppressed in the circuit diagram if they are auto-generated.
+
+For the remainder of this document we will assume that the commands are run from
+module-context and not design-context.
+
+\subsection{Working with selections}
+
+\begin{figure}[t]
+\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_03.pdf}
+\caption{Output of {\tt show} after {\tt select \$2} or {\tt select t:\$add}
+(see also Fig.~\ref{example_out})}
+\label{seladd}
+\end{figure}
+
+When a module is selected using the {\tt cd} command, all commands (with a few
+exceptions, such as the {\tt read\_*} and {\tt write\_*} commands) operate
+only on the selected module. This can also be useful for synthesis scripts
+where different synthesis strategies should be applied to different modules
+in the design.
+
+But for most interactive work we want to further narrow the set of selected
+objects. This can be done using the {\tt select} command.
+
+For example, if the command {\tt select \$2} is executed, a subsequent {\tt show}
+command will yield the diagram shown in Fig.~\ref{seladd}. Note that the nets are
+now displayed in ellipses. This indicates that they are not selected, but only
+shown because the diagram contains a cell that is connected to the net. This
+of course makes no difference for the circuit that is shown, but it can be a useful
+information when manipulating selections.
+
+Objects can not only be selected by their name but also by other properties.
+For example {\tt select t:\$add} will select all cells of type {\tt \$add}. In
+this case this is also yields the diagram shown in Fig.~\ref{seladd}.
+
+\begin{figure}[b]
+\lstinputlisting{APPNOTE_011_Design_Investigation/foobaraddsub.v}
+\caption{Test module for operations on selections}
+\label{foobaraddsub}
+\end{figure}
+
+The output of {\tt help select} contains a complete syntax reference for
+matching different properties.
+
+Many commands can operate on explicit selections. For example the command {\tt
+dump t:\$add} will print information on all {\tt \$add} cells in the active
+module. Whenever a command has {\tt [selection]} as last argument in its usage
+help, this means that it will use the engine behind the {\tt select} command
+to evaluate additional arguments and use the resulting selection instead of
+the selection created by the last {\tt select} command.
+
+Normally the {\tt select} command overwrites a previous selection. The
+commands {\tt select -add} and {\tt select -del} can be used to add
+or remove objects from the current selection.
+
+The command {\tt select -clear} can be used to reset the selection to the
+default, which is a complete selection of everything in the current module.
+
+\subsection{Operations on selections}
+
+\begin{figure}[t]
+\lstinputlisting{APPNOTE_011_Design_Investigation/sumprod.v}
+\caption{Another test module for operations on selections}
+\label{sumprod}
+\end{figure}
+
+\begin{figure}[b]
+\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/sumprod_00.pdf}
+\caption{Output of {\tt show a:sumstuff} on Fig.~\ref{sumprod}}
+\label{sumprod_00}
+\end{figure}
+
+The {\tt select} command is actually much more powerful than it might seem on
+the first glimpse. When it is called with multiple arguments, each argument is
+evaluated and pushed separately on a stack. After all arguments have been
+processed it simply creates the union of all elements on the stack. So the
+following command will select all {\tt \$add} cells and all objects with
+the {\tt foo} attribute set:
+
+\begin{verbatim}
+select t:$add a:foo
+\end{verbatim}
+
+(Try this with the design shown in Fig.~\ref{foobaraddsub}. Use the {\tt
+select -list} command to list the current selection.)
+
+In many cases simply adding more and more stuff to the selection is an
+ineffective way of selecting the interesting part of the design. Special
+arguments can be used to combine the elements on the stack.
+For example the {\tt \%i} arguments pops the last two elements from
+the stack, intersects them, and pushes the result back on the stack. So the
+following command will select all {\$add} cells that have the {\tt foo}
+attribute set:
+
+\begin{verbatim}
+select t:$add a:foo %i
+\end{verbatim}
+
+The listing in Fig.~\ref{sumprod} uses the Yosys non-standard {\tt \{* ... *\}}
+syntax to set the attribute {\tt sumstuff} on all cells generated by the first
+assign statement. (This works on arbitrary large blocks of Verilog code an
+can be used to mark portions of code for analysis.)
+
+Selecting {\tt a:sumstuff} in this module will yield the circuit diagram shown
+in Fig.~\ref{sumprod_00}. As only the cells themselves are selected, but not
+the temporary wire {\tt \$1\_Y}, the two adders are shown as two disjunct
+parts. This can be very useful for global signals like clock and reset signals: just
+unselect them using a command such as {\tt select -del clk rst} and each cell
+using them will get its own net label.
+
+In this case however we would like to see the cells connected properly. This
+can be achieved using the {\tt \%x} action, that broadens the selection, i.e.
+for each selected wire it selects all cells connected to the wire and vice
+versa. So {\tt show a:sumstuff \%x} yields the diagram shown in Fig.~\ref{sumprod_01}.
+
+\begin{figure}[t]
+\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/sumprod_01.pdf}
+\caption{Output of {\tt show a:sumstuff \%x} on Fig.~\ref{sumprod}}
+\label{sumprod_01}
+\end{figure}
+
+\subsection{Selecting logic cones}
+
+Fig.~\ref{sumprod_01} shows what is called the {\it input cone\/} of {\tt sum}, i.e.
+all cells and signals that are used to generate the signal {\tt sum}. The {\tt \%ci}
+action can be used to select the input cones of all object in the top selection
+in the stack maintained by the {\tt select} command.
+
+As the {\tt \%x} action, this commands broadens the selection by one ``step''. But
+this time the operation only works against the direction of data flow. That means,
+wires only select cells via output ports and cells only select wires via input ports.
+
+Fig.~\ref{select_prod} show the sequence of diagrams generated by the following
+commands:
+
+\begin{verbatim}
+show prod
+show prod %ci
+show prod %ci %ci
+show prod %ci %ci %ci
+\end{verbatim}
-\FIXME{} --- cd and ls, multi-page diagrams, select, cones and boolean operations
+When selecting many levels of logic, repeating {\tt \%ci} over and over again
+can be a bit dull. So there is a shortcut for that: the number of iterations
+can be appended to the action. So for example the action {\tt \%ci3} is
+identical to performing the {\tt \%ci} action three times.
+
+The action {\tt \%ci*} performs the {\tt \%ci} action over and over again until
+it has no effect anymore.
+
+\begin{figure}[t]
+\hfill \includegraphics[width=4cm,trim=0 1cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_02.pdf} \\
+\includegraphics[width=\linewidth,trim=0 0cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_03.pdf} \\
+\includegraphics[width=\linewidth,trim=0 0cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_04.pdf} \\
+\includegraphics[width=\linewidth,trim=0 2cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_05.pdf} \\
+\caption{Objects selected by {\tt select prod \%ci...}}
+\label{select_prod}
+\end{figure}
+
+\medskip
+
+In most cases there are certain cell types and/or ports that should not be considered for the {\tt \%ci}
+action, or we only want to follow certain cell types and/or ports. This can be achieved using additional
+patterns that can be appended to the {\tt \%ci} action.
+
+Lets consider the design from Fig.~\ref{memdemo_src}. It serves no purpose other than being a non-trivial
+circuit for demonstrating some of the advanced Yosys features. We synthesize the circuit using {\tt proc;
+opt; memory; opt} and change to the {\tt memdemo} module with {\tt cd memdemo}. If we type {\tt show}
+now we see the diagram shown in Fig.~\ref{memdemo_00}.
+
+\begin{figure}[b!]
+\lstinputlisting{APPNOTE_011_Design_Investigation/memdemo.v}
+\caption{Demo circuit for demonstrating some advanced Yosys features}
+\label{memdemo_src}
+\end{figure}
+
+\begin{figure*}[t]
+\includegraphics[width=\linewidth,trim=0 0cm 0 0cm]{APPNOTE_011_Design_Investigation/memdemo_00.pdf} \\
+\caption{Complete circuit diagram for the design shown in Fig.~\ref{memdemo_src}}
+\label{memdemo_00}
+\end{figure*}
+
+But maybe we are only interested in the tree of multiplexers that select the
+output value. In order to get there, we would start by just showing the output signal
+and its immediate predecessors:
+
+\begin{verbatim}
+show y %ci2
+\end{verbatim}
+
+From this we would learn that {\tt y} is driven by a {\tt \$dff cell}, that
+{\tt y} is connected to the output port {\tt Q}, that the {\tt clk} signal goes
+into the {\tt CLK} input port of the cell, and that the data comes from a
+auto-generated wire into the input {\tt D} of the flip-flop cell.
+
+As we are not interested in the clock signal we add an additional pattern to the {\tt \%ci}
+action, that tells it to only follow ports {\tt Q} and {\tt D} of {\tt \$dff} cells:
+
+\begin{verbatim}
+show y %ci2:+$dff[Q,D]
+\end{verbatim}
+
+To add a pattern we add a colon followed by the pattern to the {\tt \%ci}
+action. The pattern it self starts with {\tt -} or {\tt +}, indicating if it is
+an include or exclude pattern, followed by an optional comma separated list
+of cell types, followed by an optional comma separated list of port names in
+square brackets.
+
+Since we know that the only cell considered in this case is a {\tt \$dff} cell,
+we could as well only specify the port names:
+
+\begin{verbatim}
+show y %ci2:+[Q,D]
+\end{verbatim}
+
+Or we could decide to tell the {\tt \%ci} action to not follow the {\tt CLK} input:
+
+\begin{verbatim}
+show y %ci2:-[CLK]
+\end{verbatim}
+
+\begin{figure}[b]
+\includegraphics[width=\linewidth,trim=0 0cm 0 0cm]{APPNOTE_011_Design_Investigation/memdemo_01.pdf} \\
+\caption{Output of {\tt show y \%ci2:+\$dff[Q,D] \%ci*:-\$mux[S]:-\$dff}}
+\label{memdemo_01}
+\end{figure}
+
+Next we would investigate the next logic level by adding another {\tt \%ci2} to
+the command:
+
+\begin{verbatim}
+show y %ci2:-[CLK] %ci2
+\end{verbatim}
+
+From this we would learn that the next cell is a {\tt \$mux} cell and we would add additional
+pattern to narrow the selection on the path we are interested. In the end we would end up
+with a command such as
+
+\begin{verbatim}
+show y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff
+\end{verbatim}
+
+in which the first {\tt \%ci} jumps over the initial d-type flip-flop and the
+2nd action selects the entire input cone without going over multiplexer select
+inputs and flip-flop cells. The diagram produces by this command is shown in
+Fig.~\ref{memdemo_01}.
+
+\medskip
+
+Similar to {\tt \%ci} exists an action {\tt \%co} to select output cones that
+accepts the same syntax for pattern and repetition. The {\tt \%x} action mentioned
+previously also accepts this advanced syntax.
+
+This actions for traversing the circuit graph, combined with the actions for
+boolean operations such as intersection ({\tt \%i}) and difference ({\tt \%d})
+are powerful tools for extracting the relevant portions of the circuit under
+investigation.
+
+See {\tt help select} for a complete list of actions available in selections.
+
+\subsection{Storing and recalling selections}
+
+The current selection can be stored in memory with the command {\tt select -set
+<name>}. It can later be recalled using {\tt select @<name>}. In fact, the {\tt
+@<name>} expression pushes the stored selection on the stack maintained by the
+{\tt select} command. So for example
+
+\begin{verbatim}
+select @foo @bar %i
+\end{verbatim}
+
+will select the intersection between the stored selections {\tt foo} and {\tt bar}.
+
+\medskip
+
+In larger investigation efforts it is highly recommended to maintain a script that
+sets up relevant selections, so they can easily be recalled, for example when
+Yosys needs to be re-run after a design or source code change.
+
+The {\tt history} command can be used to list all recent interactive commands.
+This feature can be useful for creating such a script from the commands used in
+an interactive session.
\section{Advanced investigation techniques}
+\label{poke}
+
+When working with very large modules, it is often not enough to just select the
+interesting part of the module. Instead it can be useful to extract the
+interesting part of the circuit into a separate module. This can for example be
+useful if one wants to run a series of synthesis commands on the critical part
+of the module and wants to carefully read all the debug output created by the
+commands in order to spot a problem. This kind of troubleshooting is much easier
+if the circuit under investigation is encapsulated in a separate module.
+
+Fig.~\ref{submod} shows how the {\tt submod} command can be used to split the
+circuit from Fig.~\ref{memdemo_src} and \ref{memdemo_00} into its components.
+The {\tt -name} option is used to specify the name of the new module and
+also the name of the new cell in the current module.
+
+\begin{figure}[t]
+\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_00.pdf} \\ \centerline{\tt memdemo} \vskip1em\par
+\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_01.pdf} \\ \centerline{\tt scramble} \vskip1em\par
+\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_02.pdf} \\ \centerline{\tt outstage} \vskip1em\par
+\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_03.pdf} \\ \centerline{\tt selstage} \vskip1em\par
+\begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
+select -set outstage y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff
+select -set selstage y %ci2:+$dff[Q,D] %ci*:-$dff @outstage %d
+select -set scramble mem* %ci2 %ci*:-$dff mem* %d @selstage %d
+submod -name scramble @scramble
+submod -name outstage @outstage
+submod -name selstage @selstage
+\end{lstlisting}
+\caption{The circuit from Fig.~\ref{memdemo_src} and \ref{memdemo_00} broken up using {\tt submod}}
+\label{submod}
+\end{figure}
+
+\subsection{Evaluation of combinatorial circuits}
+
+The {\tt eval} command can be used to evaluate combinatorial circuits.
+For example (see Fig.~\ref{submod} for the circuit diagram of {\tt selstage}):
+
+{\scriptsize
+\begin{verbatim}
+ yosys [selstage]> eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1
+
+ 9. Executing EVAL pass (evaluate the circuit given an input).
+ Full command line: eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1
+ Eval result: \n2 = 2'10.
+ Eval result: \n1 = 2'10.
+\end{verbatim}
+\par}
+
+So the {\tt -set} option is used to set input values and the {\tt -show} option
+is used to specify the nets to evaluate. If no {\tt -show} option is specified,
+all selected output ports are used per default.
+
+If a necessary input value is not given, an error is produced. The option
+{\tt -set-undef} can be used to instead set all unspecified input nets to
+undef ({\tt x}).
+
+The {\tt -table} option can be used to create a truth table. For example:
+
+{\scriptsize
+\begin{verbatim}
+ yosys [selstage]> eval -set-undef -set d[3:1] 0 -table s1,d[0]
+
+ 10. Executing EVAL pass (evaluate the circuit given an input).
+ Full command line: eval -set-undef -set d[3:1] 0 -table s1,d[0]
+
+ \s1 \d [0] | \n1 \n2
+ ---- ------ | ---- ----
+ 2'00 1'0 | 2'00 2'00
+ 2'00 1'1 | 2'xx 2'00
+ 2'01 1'0 | 2'00 2'00
+ 2'01 1'1 | 2'xx 2'01
+ 2'10 1'0 | 2'00 2'00
+ 2'10 1'1 | 2'xx 2'10
+ 2'11 1'0 | 2'00 2'00
+ 2'11 1'1 | 2'xx 2'11
+
+ Assumed undef (x) value for the following signals: \s2
+\end{verbatim}
+}
+
+Note that the {\tt eval} command (as well as the {\tt sat} command discussed in
+the next sections) does only operate on flattened modules. It can not analyze
+signals that are passed through design hierarchy levels. So the {\tt flatten}
+command must be used on modules that instantiate other modules before this
+commands can be applied.
+
+\subsection{Solving combinatorial SAT problems}
-\FIXME{} --- dump, eval, sat
+\begin{figure}[b]
+\lstinputlisting{APPNOTE_011_Design_Investigation/primetest.v}
+\caption{A simple miter circuit for testing if a number is prime. But it has a
+problem (see main text and Fig.~\ref{primesat}).}
+\label{primetest}
+\end{figure}
+
+\begin{figure*}[!t]
+\begin{lstlisting}[basicstyle=\ttfamily\small]
+yosys [primetest]> sat -prove ok 1 -set p 31
+
+8. Executing SAT pass (solving SAT problems in the circuit).
+Full command line: sat -prove ok 1 -set p 31
+
+Setting up SAT problem:
+Import set-constraint: \p = 16'0000000000011111
+Final constraint equation: \p = 16'0000000000011111
+Imported 6 cells to SAT database.
+Import proof-constraint: \ok = 1'1
+Final proof equation: \ok = 1'1
+
+Solving problem with 2790 variables and 8241 clauses..
+SAT proof finished - model found: FAIL!
+
+ ______ ___ ___ _ _ _ _
+ (_____ \ / __) / __) (_) | | | |
+ _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |
+ | ____/ ___) _ \ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|
+ | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_
+ |_| |_| \___/ \___/ |_| |_| \_____|_|\_)_____)\____|_|
+
+
+ Signal Name Dec Hex Bin
+ -------------------- ---------- ---------- ---------------------
+ \a 15029 3ab5 0011101010110101
+ \b 4099 1003 0001000000000011
+ \ok 0 0 0
+ \p 31 1f 0000000000011111
+
+yosys [primetest]> sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0
+
+9. Executing SAT pass (solving SAT problems in the circuit).
+Full command line: sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0
+
+Setting up SAT problem:
+Import set-constraint: \p = 16'0000000000011111
+Import set-constraint: { \a [15:8] \b [15:8] } = 16'0000000000000000
+Final constraint equation: { \a [15:8] \b [15:8] \p } = { 16'0000000000000000 16'0000000000011111 }
+Imported 6 cells to SAT database.
+Import proof-constraint: \ok = 1'1
+Final proof equation: \ok = 1'1
+
+Solving problem with 2790 variables and 8257 clauses..
+SAT proof finished - no model found: SUCCESS!
+
+ /$$$$$$ /$$$$$$$$ /$$$$$$$
+ /$$__ $$ | $$_____/ | $$__ $$
+ | $$ \ $$ | $$ | $$ \ $$
+ | $$ | $$ | $$$$$ | $$ | $$
+ | $$ | $$ | $$__/ | $$ | $$
+ | $$/$$ $$ | $$ | $$ | $$
+ | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$
+ \____ $$$|__/|________/|__/|_______/|__/
+ \__/
+\end{lstlisting}
+\caption{Experiments with the miter circuit from Fig.~\ref{primetest}. The first attempt of proving that 31
+is prime failed because the SAT solver found a creative way of factorizing 31 using integer overflow.}
+\label{primesat}
+\end{figure*}
+
+Often the opposite of the {\tt eval} command is needed, i.e. the circuits
+output is given and we want to find the matching input signals. For small
+circuits with only a few input bits this can be accomplished by trying all
+possible input combinations, as it is done by the {\tt eval -table} command.
+For larger circuits however, Yosys provides the {\tt sat} command that uses
+a SAT \cite{CircuitSAT} solver \cite{MiniSAT} to solve this kind of problems.
+
+The {\tt sat} command works very similar to the {\tt eval} command. The main
+difference is that it is now also possible to set output values and find the
+corresponding input values. For Example:
+
+{\scriptsize
+\begin{verbatim}
+ yosys [selstage]> sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001
+
+ 11. Executing SAT pass (solving SAT problems in the circuit).
+ Full command line: sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001
+
+ Setting up SAT problem:
+ Import set-constraint: \s1 = \s2
+ Import set-constraint: { \n2 \n1 } = 4'1001
+ Final constraint equation: { \n2 \n1 \s1 } = { 4'1001 \s2 }
+ Imported 3 cells to SAT database.
+ Import show expression: { \s1 \s2 \d }
+
+ Solving problem with 81 variables and 207 clauses..
+ SAT solving finished - model found:
+
+ Signal Name Dec Hex Bin
+ -------------------- ---------- ---------- ---------------
+ \d 9 9 1001
+ \s1 0 0 00
+ \s2 0 0 00
+\end{verbatim}
+}
+
+Note that the {\tt sat} command supports signal names in both arguments
+to the {\tt -set} option. In the above example we used {\tt -set s1 s2}
+to constraint {\tt s1} and {\tt s2} to be equal. When more complex
+constraints are needed, a wrapper circuit must be constructed that
+checks the constraints and signals if the constraint was met using an
+extra output port, which then can be forced to a value using the {\tt
+-set} option. (Such a circuit that contains the circuit under test
+plus additional constraint checking circuitry is called a {\it miter\/}
+circuit.)
+
+Fig.~\ref{primetest} shows a miter circuit that is supposed to be used as a
+prime number test. If {\tt ok} is 1 for all input values {\tt a} and {\tt b}
+for a given {\tt p}, then {\tt p} is prime, or at least that is the idea.
+
+The Yosys shell session shown in Fig.~\ref{primesat} demonstrates that SAT
+solvers can even find the unexpected solutions to a problem: Using integer
+overflow there actually is a way of ``factorizing'' 31. The clean solution
+would of course be to perform the test in 32 bits, for example by replacing
+{\tt p != a*b} in the miter with {\tt p != \{16'd0,a\}*b}, or by using a
+temporary variable for the 32 bit product {\tt a*b}. But as 31 fits well into
+8 bits (and as the purpose of this document is to show off Yosys features)
+we can also simply force the upper 8 bits of {\tt a} and {\tt b} to zero for
+the {\tt sat} call, as is done in the second command in Fig.~\ref{primesat}
+(line 31).
+
+The {\tt -prove} option used in this example works similar to {\tt -set}, but
+tries to find a case in which the two arguments are not equal. If such a case is
+not found, the property is proven to hold for all inputs that satisfy the other
+constraints.
+
+It might be worth noting, that SAT solvers are not particularly efficient at
+factorizing large numbers. But if a small factorization problem occurs as
+part of a larger circuit problem, the Yosys SAT solver is perfectly capable
+of solving it.
+
+\subsection{Solving sequential SAT problems}
+
+\begin{figure}[t!]
+\begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
+yosys [memdemo]> sat -seq 6 -show y -show d -set-init-undef \
+ -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3
+
+6. Executing SAT pass (solving SAT problems in the circuit).
+Full command line: sat -seq 6 -show y -show d -set-init-undef
+ -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3
+
+Setting up time step 1:
+Final constraint equation: { } = { }
+Imported 29 cells to SAT database.
+
+Setting up time step 2:
+Final constraint equation: { } = { }
+Imported 29 cells to SAT database.
+
+Setting up time step 3:
+Final constraint equation: { } = { }
+Imported 29 cells to SAT database.
+
+Setting up time step 4:
+Import set-constraint for timestep: \y = 4'0001
+Final constraint equation: \y = 4'0001
+Imported 29 cells to SAT database.
+
+Setting up time step 5:
+Import set-constraint for timestep: \y = 4'0010
+Final constraint equation: \y = 4'0010
+Imported 29 cells to SAT database.
+
+Setting up time step 6:
+Import set-constraint for timestep: \y = 4'0011
+Final constraint equation: \y = 4'0011
+Imported 29 cells to SAT database.
+
+Setting up initial state:
+Final constraint equation: { \y \s2 \s1 \mem[3] \mem[2] \mem[1]
+ \mem[0] } = 24'xxxxxxxxxxxxxxxxxxxxxxxx
+
+Import show expression: \y
+Import show expression: \d
+
+Solving problem with 10322 variables and 27881 clauses..
+SAT model found. maximizing number of undefs.
+SAT solving finished - model found:
+
+ Time Signal Name Dec Hex Bin
+ ---- -------------------- ---------- ---------- ---------------
+ init \mem[0] -- -- xxxx
+ init \mem[1] -- -- xxxx
+ init \mem[2] -- -- xxxx
+ init \mem[3] -- -- xxxx
+ init \s1 -- -- xx
+ init \s2 -- -- xx
+ init \y -- -- xxxx
+ ---- -------------------- ---------- ---------- ---------------
+ 1 \d 0 0 0000
+ 1 \y -- -- xxxx
+ ---- -------------------- ---------- ---------- ---------------
+ 2 \d 1 1 0001
+ 2 \y -- -- xxxx
+ ---- -------------------- ---------- ---------- ---------------
+ 3 \d 2 2 0010
+ 3 \y 0 0 0000
+ ---- -------------------- ---------- ---------- ---------------
+ 4 \d 3 3 0011
+ 4 \y 1 1 0001
+ ---- -------------------- ---------- ---------- ---------------
+ 5 \d -- -- 001x
+ 5 \y 2 2 0010
+ ---- -------------------- ---------- ---------- ---------------
+ 6 \d -- -- xxxx
+ 6 \y 3 3 0011
+\end{lstlisting}
+\caption{Solving a sequential SAT problem in the {\tt memdemo} module from Fig.~\ref{memdemo_src}.}
+\label{memdemo_sat}
+\end{figure}
+
+The SAT solver functionality in Yosys can not only be used to solve
+combinatorial problems, but can also solve sequential problems. Let's consider
+the entire {\tt memdemo} module from Fig.~\ref{memdemo_src} and suppose we
+want to know which sequence of input values for {\tt d} will cause the output
+{\tt y} to produce the sequence 1, 2, 3 from any initial state.
+Fig.~\ref{memdemo_sat} show the solution to this question, as produced by
+the following command:
+
+\begin{verbatim}
+ sat -seq 6 -show y -show d -set-init-undef \
+ -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3
+\end{verbatim}
+
+The {\tt -seq 6} option instructs the {\tt sat} command to solve a sequential
+problem in 6 time steps. (Experiments with lower number of steps have show that
+at least 3 cycles are necessary to bring the circuit in a state from which
+the sequence 1, 2, 3 can be produced.)
+
+The {\tt -set-init-undef} option tells the {\tt sat} command to initialize
+all registers to the undef ({\tt x}) state. The way the {\tt x} state
+is treated in Verilog will ensure that the solution will work for any
+initial state.
+
+The {\tt -max\_undef} option instructs the {\tt sat} command to find a solution
+with a maximum number of undefs. This way we can see clearly which inputs bits
+are relevant to the solution.
+
+Finally the three {\tt -set-at} options add constraints for the {\tt y}
+signal to play the 1, 2, 3 sequence, starting with time step 4.
+
+It is not surprising that the solution sets {\tt d = 0} in the first step, as
+this is the only way of setting the {\tt s1} and {\tt s2} registers to a known
+value. The input values for the other steps are a bit harder to work out
+manually, but the SAT solver finds the correct solution in an instant.
+
+\medskip
+
+There is much more to write about the {\tt sat} command. For example, there is
+a set of options that can be used to performs sequential proofs using temporal
+induction \cite{tip}. The command {\tt help sat} can be used to print a list
+of all options with short descriptions of their functions.
+
+\section{Conclusion}
+\label{conclusion}
+
+Yosys provides a wide range of functions to analyze and investigate designs. For
+many cases it is sufficient to simply display circuit diagrams, maybe use some
+additional commands to narrow the scope of the circuit diagrams to the interesting
+parts of the circuit. But some cases require more than that. For this applications
+Yosys provides commands that can be used to further inspect the behavior of the
+circuit, either by evaluating which output values are generated from certain input values
+({\tt eval}) or by evaluation which input values and initial conditions can result
+in a certain behavior at the outputs ({\tt sat}). The SAT command can even be used
+to prove (or disprove) theorems regarding the circuit, in more advanced cases
+with the additional help of a miter circuit.
+
+This features can be powerful tools for the circuit designer using Yosys as a
+utility for building circuits and the software developer using Yosys as a
+framework for new algorithms alike.
\begin{thebibliography}{9}
Clifford Wolf. The Yosys Open SYnthesis Suite.
\url{http://www.clifford.at/yosys/}
-\bibitem{glaserwolf}
-Johann Glaser. Clifford Wolf. Methodology and Example-Driven Interconnect
-Synthesis for Designing Heterogeneous Coarse-Grain Reconfigurable
-Architectures. In: Jan Haase (Editor). {\it Models, Methods, and Tools for Complex Chip Design.
-Lecture Notes in Electrical Engineering. Volume 265, 2014, pp 201-221.\/}
-\href{http://dx.doi.org/10.1007/978-3-319-01418-0_12}{DOI 10.1007/978-3-319-01418-0\_12}
-
\bibitem{graphviz}
Graphviz - Graph Visualization Software.
\url{http://www.graphviz.org/}
+\bibitem{xdot}
+xdot.py - an interactive viewer for graphs written in Graphviz's dot language.
+\url{https://github.com/jrfonseca/xdot.py}
+
+\bibitem{CircuitSAT}
+{\it Circuit satisfiability problem} on Wikipedia
+\url{http://en.wikipedia.org/wiki/Circuit_satisfiability}
+
+\bibitem{MiniSAT}
+MiniSat: a minimalistic open-source SAT solver.
+\url{http://minisat.se/}
+
+\bibitem{tip}
+Niklas Een and Niklas S\"orensson (2003).
+Temporal Induction by Incremental SAT Solving.
+\url{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.8161}
+
\end{thebibliography}
\end{document}
projects / yosys.git / blobdiff