And appnotes

1 files changed, 0 insertions, 1070 deletions

diff --git a/manual/APPNOTE_011_Design_Investigation.tex b/manual/APPNOTE_011_Design_Investigation.tex
deleted file mode 100644
index 881212fe9..000000000
--- a/manual/APPNOTE_011_Design_Investigation.tex
+++ /dev/null
@@ -1,1070 +0,0 @@
-
-% IEEEtran howto:
-% http://ftp.univie.ac.at/packages/tex/macros/latex/contrib/IEEEtran/IEEEtran_HOWTO.pdf
-\documentclass[9pt,technote,a4paper]{IEEEtran}
-
-\usepackage[T1]{fontenc}   % required for luximono!
-\usepackage[scaled=0.8]{luximono}  % typewriter font with bold face
-
-% To install the luximono font files:
-% getnonfreefonts-sys --all        or
-% getnonfreefonts-sys luximono
-%
-% when there are trouble you might need to:
-% - Create /etc/texmf/updmap.d/99local-luximono.cfg
-%   containing the single line: Map ul9.map
-% - Run update-updmap followed by mktexlsr and updmap-sys
-%
-% This commands must be executed as root with a root environment
-% (i.e. run "sudo su" and then execute the commands in the root
-% shell, don't just prefix the commands with "sudo").
-
-\usepackage[unicode,bookmarks=false]{hyperref}
-\usepackage[english]{babel}
-\usepackage[utf8]{inputenc}
-\usepackage{amssymb}
-\usepackage{amsmath}
-\usepackage{amsfonts}
-\usepackage{units}
-\usepackage{nicefrac}
-\usepackage{eurosym}
-\usepackage{graphicx}
-\usepackage{verbatim}
-\usepackage{algpseudocode}
-\usepackage{scalefnt}
-\usepackage{xspace}
-\usepackage{color}
-\usepackage{colortbl}
-\usepackage{multirow}
-\usepackage{hhline}
-\usepackage{listings}
-\usepackage{float}
-
-\usepackage{tikz}
-\usetikzlibrary{calc}
-\usetikzlibrary{arrows}
-\usetikzlibrary{scopes}
-\usetikzlibrary{through}
-\usetikzlibrary{shapes.geometric}
-
-\def\FIXME{{\color{red}\bf FIXME}}
-
-\lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=0.7cm,xrightmargin=0.2cm,numbers=left}
-
-\begin{document}
-
-\title{Yosys Application Note 011: \\ Interactive Design Investigation}
-\author{Claire Xenia Wolf \\ Original Version December 2013}
-\maketitle
-
-\begin{abstract}
-Yosys \cite{yosys} can be a great environment for building custom synthesis
-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, 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 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}
-and \cite{xdot} for generating the actual circuit diagrams.
-
-\section{Overview}
-
-This application note is structured as follows:
-
-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}
-$ cat example.ys
-read_verilog example.v
-show -pause
-proc
-show -pause
-opt
-show -pause
-
-$ cat example.v
-module example(input clk, a, b, c,
-               output reg [1:0] y);
-    always @(posedge clk)
-        if (c)
-            y <= c ? a + b : 2'd0;
-endmodule
-\end{lstlisting}
-\caption{Yosys script with {\tt show} commands and example design}
-\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 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 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 (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
-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}
-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.
-
-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
-
-In this script we directly call {\tt opt} as next step, which finally leads us to
-the 3rd diagram in Fig.~\ref{example_out}. Here we see that the {\tt opt} command
-not only has removed the artifacts left behind by {\tt proc}, but also determined
-correctly that it can remove the first {\tt \$mux} cell without changing the behavior
-of the circuit.
-
-\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{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}
-yosys> ls
-
-1 modules:
-  example
-
-yosys> cd example
-
-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{Demonstration of {\tt ls} and {\tt cd} using {\tt example.v} from Fig.~\ref{example_src}}
-\label{lscd}
-\end{figure}
-
-\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}
-
-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}
-
-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}
-
-\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}
-
-\bibitem{yosys}
-Claire Xenia Wolf. The Yosys Open SYnthesis Suite.
-\url{https://yosyshq.net/yosys/}
-
-\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}