% 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=2em,xrightmargin=1em,numbers=left}

\begin{document}

\title{Yosys Application Note 011: \\ Interactive Design Investigation}
\author{Clifford Wolf \\ November 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 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 commands for
investigating the actual behavior of circuits.
\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
{\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.

\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 and select portions of the design and print additional information on
the elements in the design that are not contained in the circuit diagrams.

Sec.~\ref{poke} introduces commands to evaluate the design and solve SAT
problems within the design.

Sec.~\ref{conclusion} concludes the document and summarizes the key points.

\section{Introduction to the {\tt show} command}
\label{intro_show}

\begin{figure}[b]
\begin{lstlisting}
$ 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 yosys-svgviewer} to display the diagram.
Subsequent calls to {\tt show} re-use the {\tt yosys-svgviewer} instance
(if still running).

\subsection{A simple circuit}

Fig.~\ref{example_src} shows a simple synthesis script and Verilog file that
demonstrates the usage of {\tt show} in a simple setting. Note that {\tt show}
is called with the {\tt -pause} option, that halts execution of the Yosys
script until the user presses the Enter key. The {\tt show -pause} command
also allows the user to enter an interactive shell to further investigate the
circuit before continuing synthesis.

So this script, when executed, will show the design after each of the three
synthesis commands. The generated circuit diagrams are shown in Fig.~\ref{example_out}.

The first diagram (from top to bottom) shows the design directly after being
read by the Verilog front-end. Input and output ports are visualized using
octagonal shapes. Cells are visualized as rectangles with inputs on the left
and outputs on the right side. The cell labels are two lines long: The first line
contains 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
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 by using the {\tt ;;} token, which doubles as
separator for commands. Unless one wants to specifically analyze this artefacts
left behind some operations, it is therefore recommended to call {\tt clean}
before calling {\tt show}.

\medskip

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 need
to be accessed. The example show in Fig.~\ref{splice_dia} and \ref{splice_src}
demonstrates how such circuits are visualized by the {\tt show} command.

The key elements in understanding this circuit diagram are of course the boxes
with round corners and rows labeled {\tt <MSB\_LEFT>:<LSB\_LEFT> -- <MSB\_RIGHT>:<LSB\_RIGHT>}.
Each of this boxes has one signal per row on one side and a common signal for all rows on the
other side. The {\tt <MSB>:<LSB>} tuples specify which bits are broken out from the signals
and are connected. So The top row of the box connecting the signals {\tt a} and {\tt b} indicates
that the bit 0 (i.e. the range 0:0) from signal {\tt a} is connected to bit 1 (i.e. the range
1:1) of signal {\tt x}.

Lines connecting such boxes together and lines connecting such boxes to cell
ports have slightly different look to emphasise that they are not actual signal
wires but a necessity of the graphical representation. This distinction seems
like a technicality, until one wants to debug a problem related to the way
Yosys internally represents signal vectors, for example when writing custom
Yosys commands.

\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 later option has the great 
advantage that the library only needs to be loaded once and can then be used
in all subsequent calls to the {\tt show} command.

In addition to that the 2nd diagram was generated after {\tt splitnet -ports}
was run on the design. This command splits all signal vectors into individual
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 SVG file and launches
{\tt yosys-svgviewer} 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 {\tt yosys-svgviewer} the left mouse button is per default bound to move the
diagram (and the mouse wheel can be used for zooming in and out). However, in
some cases one wants to copy text from the diagram. In this cases the
View->Interactive checkbox must be activated. This switch the rendering back-end
to one that supports interaction with the SVG file, such as selecting text.

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 number
generation. Sometimes it is necessary it try some values to find an assignment
of colors that works.

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 so
far. 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 only 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 where
a problem can be reproduces. So if for example 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 (see {\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 {\tt cd} command, all commands (with a few
exceptions, such as the {\tt read\_*} and {\tt write\_*} commands) operate
only on the selected module. So 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}.

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 performed by the last {\tt select} command.

The command {\tt select -clear} can be used to reset the selection.

\subsection{Operations on selections}

\begin{figure}[b]
\lstinputlisting{APPNOTE_011_Design_Investigation/foobaraddsub.v}
\caption{Test module for operations on selections}
\label{foobaraddsub}
\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 differently combine the elements on the stack.
For example the {\tt \%i} arguments intersects the last two elements 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}

\begin{figure}[t]
\lstinputlisting{APPNOTE_011_Design_Investigation/sumprod.v}
\caption{Another test module for operations on selections}
\label{sumprod}
\end{figure}

The listing in Fig.~\ref{sumprod} used 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.)

\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}

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 signal 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 schon 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}

\FIXME{}

\subsection{Selecting logic cones}

\FIXME{}

\subsection{Storing and recalling selections}

\FIXME{}

\section{Advanced investigation techniques}
\label{poke}

\FIXME{} --- submod, eval, sat

\section{Conclusion}
\label{conclusion}

\FIXME

\begin{thebibliography}{9}

\bibitem{yosys}
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/}

\end{thebibliography}

\end{document}