And appnotes

33 files changed, 0 insertions, 2721 deletions

diff --git a/manual/APPNOTE_010_Verilog_to_BLIF.tex b/manual/APPNOTE_010_Verilog_to_BLIF.tex
deleted file mode 100644
index 16254d593..000000000
--- a/manual/APPNOTE_010_Verilog_to_BLIF.tex
+++ /dev/null
@@ -1,466 +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}
-
-\lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=2em,xrightmargin=1em,numbers=left}
-
-\begin{document}
-
-\title{Yosys Application Note 010: \\ Converting Verilog to BLIF}
-\author{Claire Xenia Wolf \\ November 2013}
-\maketitle
-
-\begin{abstract}
-Verilog-2005 is a powerful Hardware Description Language (HDL) that can be used
-to easily create complex designs from small HDL code. It is the preferred
-method of design entry for many designers\footnote{The other half prefers VHDL,
-a very different but -- of course -- equally powerful language.}.
-
-The Berkeley Logic Interchange Format (BLIF) \cite{blif} is a simple file format for
-exchanging sequential logic between programs. It is easy to generate and
-easy to parse and is therefore the preferred method of design entry for
-many authors of logic synthesis tools.
-
-Yosys \cite{yosys} is a feature-rich
-Open-Source Verilog synthesis tool that can be used to bridge the gap between
-the two file formats. It implements most of Verilog-2005 and thus can be used
-to import modern behavioral Verilog designs into BLIF-based design flows
-without dependencies on proprietary synthesis tools.
-
-The scope of Yosys goes of course far beyond Verilog logic synthesis. But
-it is a useful and important feature and this Application Note will focus
-on this aspect of Yosys.
-\end{abstract}
-
-\section{Installation}
-
-Yosys written in C++ (using features from C++11) and is tested on modern Linux.
-It should compile fine on most UNIX systems with a C++11 compiler. The README
-file contains useful information on building Yosys and its prerequisites.
-
-Yosys is a large and feature-rich program with a couple of dependencies. It is,
-however, possible to deactivate some of the dependencies in the Makefile,
-resulting in features in Yosys becoming unavailable. When problems with building
-Yosys are encountered, a user who is only interested in the features of Yosys
-that are discussed in this Application Note may deactivate {\tt TCL}, {\tt Qt}
-and {\tt MiniSAT} support in the {\tt Makefile} and may opt against building
-{\tt yosys-abc}.
-
-\bigskip
-
-This Application Note is based on GIT Rev. {\tt e216e0e} from 2013-11-23 of
-Yosys \cite{yosys}. The Verilog sources used for the examples are taken from
-yosys-bigsim \cite{bigsim}, a collection of real-world designs used for
-regression testing Yosys.
-
-\section{Getting Started}
-
-We start our tour with the Navr\'e processor from yosys-bigsim. The Navr\'e
-processor \cite{navre} is an Open Source AVR clone. It is a single module ({\tt
-softusb\_navre}) in a single design file ({\tt softusb\_navre.v}). It also is
-using only features that map nicely to the BLIF format, for example it only
-uses synchronous resets.
-
-Converting {\tt softusb\_navre.v} to {\tt softusb\_navre.blif} could not be
-easier:
-
-\begin{figure}[H]
-\begin{lstlisting}[language=sh]
-yosys -o softusb_navre.blif -S softusb_navre.v
-\end{lstlisting}
- \renewcommand{\figurename}{Listing}
-\caption{Calling Yosys without script file}
-\end{figure}
-
-Behind the scenes Yosys is controlled by synthesis scripts that execute
-commands that operate on Yosys' internal state. For example, the {\tt -o
-softusb\_navre.blif} option just adds the command {\tt write\_blif
-softusb\_navre.blif} to the end of the script. Likewise a file on the
-command line -- {\tt softusb\_navre.v} in this case -- adds the command
-{\tt read\_verilog softusb\_navre.v} to the beginning of the
-synthesis script. In both cases the file type is detected from the
-file extension.
-
-Finally the option {\tt -S} instantiates a built-in default synthesis script.
-Instead of using {\tt -S} one could also specify the synthesis commands
-for the script on the command line using the {\tt -p} option, either using
-individual options for each command or by passing one big command string
-with a semicolon-separated list of commands. But in most cases it is more
-convenient to use an actual script file.
-
-\section{Using a Synthesis Script}
-
-With a script file we have better control over Yosys. The following script
-file replicates what the command from the last section did:
-
-\begin{figure}[H]
-\begin{lstlisting}[language=sh]
-read_verilog softusb_navre.v
-hierarchy
-proc; opt; memory; opt; techmap; opt
-write_blif softusb_navre.blif
-\end{lstlisting}
- \renewcommand{\figurename}{Listing}
-\caption{\tt softusb\_navre.ys}
-\end{figure}
-
-The first and last line obviously read the Verilog file and write the BLIF
-file.
-
-\medskip
-
-The 2nd line checks the design hierarchy and instantiates parametrized
-versions of the modules in the design, if necessary. In the case of this
-simple design this is a no-op. However, as a general rule a synthesis script
-should always contain this command as first command after reading the input
-files.
-
-\medskip
-
-The 3rd line does most of the actual work:
-
-\begin{itemize}
-\item The command {\tt opt} is the Yosys' built-in optimizer. It can perform
-some simple optimizations such as const-folding and removing unconnected parts
-of the design. It is common practice to call opt after each major step in the
-synthesis procedure. In cases where too much optimization is not appreciated
-(for example when analyzing a design), it is recommended to call {\tt clean}
-instead of {\tt opt}.
-\item The command {\tt proc} converts {\it processes} (Yosys' internal
-representation of Verilog {\tt always}- and {\tt initial}-blocks) to circuits
-of multiplexers and storage elements (various types of flip-flops).
-\item The command {\tt memory} converts Yosys' internal representations of
-arrays and array accesses to multi-port block memories, and then maps this
-block memories to address decoders and flip-flops, unless the option {\tt -nomap}
-is used, in which case the multi-port block memories stay in the design
-and can then be mapped to architecture-specific memory primitives using
-other commands.
-\item The command {\tt techmap} turns a high-level circuit with coarse grain
-cells such as wide adders and multipliers to a fine-grain circuit of simple
-logic primitives and single-bit storage elements. The command does that by
-substituting the complex cells by circuits of simpler cells. It is possible
-to provide a custom set of rules for this process in the form of a Verilog
-source file, as we will see in the next section.
-\end{itemize}
-
-Now Yosys can be run with the filename of the synthesis script as argument:
-
-\begin{figure}[H]
-\begin{lstlisting}[language=sh]
-yosys softusb_navre.ys
-\end{lstlisting}
- \renewcommand{\figurename}{Listing}
-\caption{Calling Yosys with script file}
-\end{figure}
-
-\medskip
-
-Now that we are using a synthesis script we can easily modify how Yosys
-synthesizes the design. The first thing we should customize is the
-call to the {\tt hierarchy} command:
-
-Whenever it is known that there are no implicit blackboxes in the design, i.e.
-modules that are referenced but are not defined, the {\tt hierarchy} command
-should be called with the {\tt -check} option. This will then cause synthesis
-to fail when implicit blackboxes are found in the design.
-
-The 2nd thing we can improve regarding the {\tt hierarchy} command is that we
-can tell it the name of the top level module of the design hierarchy. It will
-then automatically remove all modules that are not referenced from this top
-level module.
-
-\medskip
-
-For many designs it is also desired to optimize the encodings for the finite
-state machines (FSMs) in the design. The {\tt fsm} command finds FSMs, extracts
-them, performs some basic optimizations and then generate a circuit from
-the extracted and optimized description. It would also be possible to tell
-the {\tt fsm} command to leave the FSMs in their extracted form, so they can be
-further processed using custom commands. But in this case we don't want that.
-
-\medskip
-
-So now we have the final synthesis script for generating a BLIF file
-for the Navr\'e CPU:
-
-\begin{figure}[H]
-\begin{lstlisting}[language=sh]
-read_verilog softusb_navre.v
-hierarchy -check -top softusb_navre
-proc; opt; memory; opt; fsm; opt; techmap; opt
-write_blif softusb_navre.blif
-\end{lstlisting}
- \renewcommand{\figurename}{Listing}
-\caption{{\tt softusb\_navre.ys} (improved)}
-\end{figure}
-
-\section{Advanced Example: The Amber23 ARMv2a CPU}
-
-Our 2nd example is the Amber23 \cite{amber}
-ARMv2a CPU. Once again we base our example on the Verilog code that is included
-in yosys-bigsim \cite{bigsim}.
-
-\begin{figure}[b!]
-\begin{lstlisting}[language=sh]
-read_verilog a23_alu.v
-read_verilog a23_barrel_shift_fpga.v
-read_verilog a23_barrel_shift.v
-read_verilog a23_cache.v
-read_verilog a23_coprocessor.v
-read_verilog a23_core.v
-read_verilog a23_decode.v
-read_verilog a23_execute.v
-read_verilog a23_fetch.v
-read_verilog a23_multiply.v
-read_verilog a23_ram_register_bank.v
-read_verilog a23_register_bank.v
-read_verilog a23_wishbone.v
-read_verilog generic_sram_byte_en.v
-read_verilog generic_sram_line_en.v
-hierarchy -check -top a23_core
-add -global_input globrst 1
-proc -global_arst globrst
-techmap -map adff2dff.v
-opt; memory; opt; fsm; opt; techmap
-write_blif amber23.blif
-\end{lstlisting}
- \renewcommand{\figurename}{Listing}
-\caption{\tt amber23.ys}
-\label{aber23.ys}
-\end{figure}
-
-The problem with this core is that it contains no dedicated reset logic.
-Instead the coding techniques shown in Listing~\ref{glob_arst} are used to
-define reset values for the global asynchronous reset in an FPGA
-implementation. This design can not be expressed in BLIF as it is. Instead we
-need to use a synthesis script that transforms this form to synchronous resets that
-can be expressed in BLIF.
-
-(Note that there is no problem if this coding techniques are used to model
-ROM, where the register is initialized using this syntax but is never updated
-otherwise.)
-
-\medskip
-
-Listing~\ref{aber23.ys} shows the synthesis script for the Amber23 core. In
-line 17 the {\tt add} command is used to add a 1-bit wide global input signal
-with the name {\tt globrst}. That means that an input with that name is added
-to each module in the design hierarchy and then all module instantiations are
-altered so that this new signal is connected throughout the whole design
-hierarchy.
-
-\begin{figure}[t!]
-\begin{lstlisting}[language=Verilog]
-reg [7:0] a = 13, b;
-initial b = 37;
-\end{lstlisting}
- \renewcommand{\figurename}{Listing}
-\caption{Implicit coding of global asynchronous resets}
-\label{glob_arst}
-\end{figure}
-
-\begin{figure}[b!]
-\begin{lstlisting}[language=Verilog]
-(* techmap_celltype = "$adff" *)
-module adff2dff (CLK, ARST, D, Q);
-
-parameter WIDTH = 1;
-parameter CLK_POLARITY = 1;
-parameter ARST_POLARITY = 1;
-parameter ARST_VALUE = 0;
-
-input CLK, ARST;
-input [WIDTH-1:0] D;
-output reg [WIDTH-1:0] Q;
-
-wire [1023:0] _TECHMAP_DO_ = "proc";
-
-wire _TECHMAP_FAIL_ =
-    !CLK_POLARITY || !ARST_POLARITY;
-
-always @(posedge CLK)
-        if (ARST)
-                Q <= ARST_VALUE;
-        else
-                Q <= D;
-
-endmodule
-\end{lstlisting}
-\renewcommand{\figurename}{Listing}
-\caption{\tt adff2dff.v}
-\label{adff2dff.v}
-\end{figure}
-
-In line 18 the {\tt proc} command is called. But in this script the signal name
-{\tt globrst} is passed to the command as a global reset signal for resetting
-the registers to their assigned initial values.
-
-Finally in line 19 the {\tt techmap} command is used to replace all instances
-of flip-flops with asynchronous resets with flip-flops with synchronous resets.
-The map file used for this is shown in Listing~\ref{adff2dff.v}. Note how the
-{\tt techmap\_celltype} attribute is used in line 1 to tell the techmap command
-which cells to replace in the design, how the {\tt \_TECHMAP\_FAIL\_} wire in
-lines 15 and 16 (which evaluates to a constant value) determines if the
-parameter set is compatible with this replacement circuit, and how the {\tt
-\_TECHMAP\_DO\_} wire in line 13 provides a mini synthesis-script to be used to
-process this cell.
-
-\begin{figure*}
-\begin{lstlisting}[language=C]
-#include <stdint.h>
-#include <stdbool.h>
-
-#define BITMAP_SIZE 64
-#define OUTPORT 0x10000000
-
-static uint32_t bitmap[BITMAP_SIZE/32];
-
-static void bitmap_set(uint32_t idx) { bitmap[idx/32] |= 1 << (idx % 32); }
-static bool bitmap_get(uint32_t idx) { return (bitmap[idx/32] & (1 << (idx % 32))) != 0; }
-static void output(uint32_t val) { *((volatile uint32_t*)OUTPORT) = val; }
-
-int main() {
-	uint32_t i, j, k;
-	output(2);
-	for (i = 0; i < BITMAP_SIZE; i++) {
-		if (bitmap_get(i)) continue;
-		output(3+2*i);
-		for (j = 2*(3+2*i);; j += 3+2*i) {
-			if (j%2 == 0) continue;
-			k = (j-3)/2;
-			if (k >= BITMAP_SIZE) break;
-			bitmap_set(k);
-		}
-	}
-	output(0);
-	return 0;
-}
-\end{lstlisting}
-\renewcommand{\figurename}{Listing}
-\caption{Test program for the Amber23 CPU (Sieve of Eratosthenes). Compiled using
-GCC 4.6.3 for ARM with {\tt -Os -marm -march=armv2a -mno-thumb-interwork
--ffreestanding}, linked with {\tt -{}-fix-v4bx} set and booted with a custom
-setup routine written in ARM assembler.}
-\label{sieve}
-\end{figure*}
-
-\section{Verification of the Amber23 CPU}
-
-The BLIF file for the Amber23 core, generated using Listings~\ref{aber23.ys}
-and \ref{adff2dff.v} and the version of the Amber23 RTL source that is bundled
-with yosys-bigsim, was verified using the test-bench from yosys-bigsim.
-It successfully executed the program shown in Listing~\ref{sieve} in the
-test-bench.
-
-For simulation the BLIF file was converted back to Verilog using ABC
-\cite{ABC}. So this test includes the successful transformation of the BLIF
-file into ABC's internal format as well.
-
-The only thing left to write about the simulation itself is that it probably
-was one of the most energy inefficient and time consuming ways of successfully
-calculating the first 31 primes the author has ever conducted.
-
-\section{Limitations}
-
-At the time of this writing Yosys does not support multi-dimensional memories,
-does not support writing to individual bits of array elements, does not
-support initialization of arrays with {\tt \$readmemb} and {\tt \$readmemh},
-and has only limited support for tristate logic, to name just a few
-limitations.
-
-That being said, Yosys can synthesize an overwhelming majority of real-world
-Verilog RTL code. The remaining cases can usually be modified to be compatible
-with Yosys quite easily.
-
-The various designs in yosys-bigsim are a good place to look for examples
-of what is within the capabilities of Yosys.
-
-\section{Conclusion}
-
-Yosys is a feature-rich Verilog-2005 synthesis tool. It has many uses, but
-one is to provide an easy gateway from high-level Verilog code to low-level
-logic circuits.
-
-The command line option {\tt -S} can be used to quickly synthesize Verilog
-code to BLIF files without a hassle.
-
-With custom synthesis scripts it becomes possible to easily perform high-level
-optimizations, such as re-encoding FSMs. In some extreme cases, such as the
-Amber23 ARMv2 CPU, the more advanced Yosys features can be used to change a
-design to fit a certain need without actually touching the RTL code.
-
-\begin{thebibliography}{9}
-
-\bibitem{yosys}
-Claire Xenia Wolf. The Yosys Open SYnthesis Suite. \\
-\url{https://yosyshq.net/yosys/}
-
-\bibitem{bigsim}
-yosys-bigsim, a collection of real-world Verilog designs for regression testing purposes. \\
-\url{https://github.com/YosysHQ/yosys-bigsim}
-
-\bibitem{navre}
-Sebastien Bourdeauducq. Navr\'e AVR clone (8-bit RISC). \\
-\url{http://opencores.org/project,navre}
-
-\bibitem{amber}
-Conor Santifort. Amber ARM-compatible core. \\
-\url{http://opencores.org/project,amber}
-
-\bibitem{ABC}
-Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. \\
-\url{http://www.eecs.berkeley.edu/~alanmi/abc/}
-
-\bibitem{blif}
-Berkeley Logic Interchange Format (BLIF) \\
-\url{http://vlsi.colorado.edu/~vis/blif.ps}
-
-\end{thebibliography}
-
-
-\end{document}
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}
diff --git a/manual/APPNOTE_011_Design_Investigation/cmos.v b/manual/APPNOTE_011_Design_Investigation/cmos.v
deleted file mode 100644
index 2912c760a..000000000
--- a/manual/APPNOTE_011_Design_Investigation/cmos.v
+++ /dev/null
@@ -1,3 +0,0 @@
-module cmos_demo(input a, b, output [1:0] y);
-assign y = a + b;
-endmodule
diff --git a/manual/APPNOTE_011_Design_Investigation/cmos_00.dot b/manual/APPNOTE_011_Design_Investigation/cmos_00.dot
deleted file mode 100644
index 49c630080..000000000
--- a/manual/APPNOTE_011_Design_Investigation/cmos_00.dot
+++ /dev/null
@@ -1,34 +0,0 @@
-digraph "cmos_demo" {
-rankdir="LR";
-remincross=true;
-n4 [ shape=octagon, label="a", color="black", fontcolor="black" ];
-n5 [ shape=octagon, label="b", color="black", fontcolor="black" ];
-n6 [ shape=octagon, label="y", color="black", fontcolor="black" ];
-c10 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g0\nNOR|{}}" ];
-c11 [ shape=record, label="{{<p7> A|<p9> Y}|$g1\nNOT|{}}" ];
-c12 [ shape=record, label="{{<p7> A|<p9> Y}|$g2\nNOT|{}}" ];
-c13 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g3\nNOR|{}}" ];
-x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
-x0:e -> c13:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
-c14 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g4\nNOR|{}}" ];
-x1 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
-x1:e -> c14:p8:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
-x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
-x2:e -> c14:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
-n1 [ shape=diamond, label="$n4" ];
-n1:e -> c10:p9:w [color="black", label=""];
-n1:e -> c14:p7:w [color="black", label=""];
-n2 [ shape=diamond, label="$n5" ];
-n2:e -> c11:p9:w [color="black", label=""];
-n2:e -> c13:p7:w [color="black", label=""];
-n3 [ shape=diamond, label="$n6_1" ];
-n3:e -> c12:p9:w [color="black", label=""];
-n3:e -> c13:p8:w [color="black", label=""];
-n4:e -> c10:p8:w [color="black", label=""];
-n4:e -> c12:p7:w [color="black", label=""];
-n5:e -> c10:p7:w [color="black", label=""];
-n5:e -> c11:p7:w [color="black", label=""];
-n6:e -> x0:s0:w [color="black", label=""];
-n6:e -> x1:s0:w [color="black", label=""];
-n6:e -> x2:s0:w [color="black", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/cmos_01.dot b/manual/APPNOTE_011_Design_Investigation/cmos_01.dot
deleted file mode 100644
index ea6f4403c..000000000
--- a/manual/APPNOTE_011_Design_Investigation/cmos_01.dot
+++ /dev/null
@@ -1,23 +0,0 @@
-digraph "cmos_demo" {
-rankdir="LR";
-remincross=true;
-n4 [ shape=octagon, label="a", color="black", fontcolor="black" ];
-n5 [ shape=octagon, label="b", color="black", fontcolor="black" ];
-n6 [ shape=octagon, label="y[0]", color="black", fontcolor="black" ];
-n7 [ shape=octagon, label="y[1]", color="black", fontcolor="black" ];
-c11 [ shape=record, label="{{<p8> A|<p9> B}|$g0\nNOR|{<p10> Y}}" ];
-c12 [ shape=record, label="{{<p8> A}|$g1\nNOT|{<p10> Y}}" ];
-c13 [ shape=record, label="{{<p8> A}|$g2\nNOT|{<p10> Y}}" ];
-c14 [ shape=record, label="{{<p8> A|<p9> B}|$g3\nNOR|{<p10> Y}}" ];
-c15 [ shape=record, label="{{<p8> A|<p9> B}|$g4\nNOR|{<p10> Y}}" ];
-c11:p10:e -> c15:p8:w [color="black", label=""];
-c12:p10:e -> c14:p8:w [color="black", label=""];
-c13:p10:e -> c14:p9:w [color="black", label=""];
-n4:e -> c11:p9:w [color="black", label=""];
-n4:e -> c13:p8:w [color="black", label=""];
-n5:e -> c11:p8:w [color="black", label=""];
-n5:e -> c12:p8:w [color="black", label=""];
-c15:p10:e -> n6:w [color="black", label=""];
-c14:p10:e -> n7:w [color="black", label=""];
-n7:e -> c15:p9:w [color="black", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/example.v b/manual/APPNOTE_011_Design_Investigation/example.v
deleted file mode 100644
index 8c71989b3..000000000
--- a/manual/APPNOTE_011_Design_Investigation/example.v
+++ /dev/null
@@ -1,6 +0,0 @@
-module example(input clk, a, b, c,
-               output reg [1:0] y);
-    always @(posedge clk)
-        if (c)
-            y <= c ? a + b : 2'd0;
-endmodule
diff --git a/manual/APPNOTE_011_Design_Investigation/example.ys b/manual/APPNOTE_011_Design_Investigation/example.ys
deleted file mode 100644
index b1e956088..000000000
--- a/manual/APPNOTE_011_Design_Investigation/example.ys
+++ /dev/null
@@ -1,11 +0,0 @@
-read_verilog example.v
-show -format dot -prefix example_00
-proc
-show -format dot -prefix example_01
-opt
-show -format dot -prefix example_02
-
-cd example
-select t:$add
-show -format dot -prefix example_03
-
diff --git a/manual/APPNOTE_011_Design_Investigation/example_00.dot b/manual/APPNOTE_011_Design_Investigation/example_00.dot
deleted file mode 100644
index 1e23ed0ea..000000000
--- a/manual/APPNOTE_011_Design_Investigation/example_00.dot
+++ /dev/null
@@ -1,23 +0,0 @@
-digraph "example" {
-rankdir="LR";
-remincross=true;
-n4 [ shape=octagon, label="a", color="black", fontcolor="black" ];
-n5 [ shape=octagon, label="b", color="black", fontcolor="black" ];
-n6 [ shape=octagon, label="c", color="black", fontcolor="black" ];
-n7 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
-n8 [ shape=octagon, label="y", color="black", fontcolor="black" ];
-c12 [ shape=record, label="{{<p9> A|<p10> B}|$2\n$add|{<p11> Y}}" ];
-v0 [ label="2'00" ];
-c14 [ shape=record, label="{{<p9> A|<p10> B|<p13> S}|$3\n$mux|{<p11> Y}}" ];
-p1 [shape=box, style=rounded, label="PROC $1\nexample.v:3"];
-c12:p11:e -> c14:p10:w [color="black", style="setlinewidth(3)", label=""];
-c14:p11:e -> p1:w [color="black", style="setlinewidth(3)", label=""];
-n4:e -> c12:p9:w [color="black", label=""];
-n5:e -> c12:p10:w [color="black", label=""];
-n6:e -> c14:p13:w [color="black", label=""];
-n6:e -> p1:w [color="black", label=""];
-n7:e -> p1:w [color="black", label=""];
-p1:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
-n8:e -> p1:w [color="black", style="setlinewidth(3)", label=""];
-v0:e -> c14:p9:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/example_01.dot b/manual/APPNOTE_011_Design_Investigation/example_01.dot
deleted file mode 100644
index e89292b51..000000000
--- a/manual/APPNOTE_011_Design_Investigation/example_01.dot
+++ /dev/null
@@ -1,33 +0,0 @@
-digraph "example" {
-rankdir="LR";
-remincross=true;
-n6 [ shape=octagon, label="a", color="black", fontcolor="black" ];
-n7 [ shape=octagon, label="b", color="black", fontcolor="black" ];
-n8 [ shape=octagon, label="c", color="black", fontcolor="black" ];
-n9 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
-n10 [ shape=octagon, label="y", color="black", fontcolor="black" ];
-c14 [ shape=record, label="{{<p11> A|<p12> B}|$2\n$add|{<p13> Y}}" ];
-c18 [ shape=record, label="{{<p15> CLK|<p16> D}|$7\n$dff|{<p17> Q}}" ];
-c20 [ shape=record, label="{{<p11> A|<p12> B|<p19> S}|$5\n$mux|{<p13> Y}}" ];
-v0 [ label="2'00" ];
-c21 [ shape=record, label="{{<p11> A|<p12> B|<p19> S}|$3\n$mux|{<p13> Y}}" ];
-x1 [shape=box, style=rounded, label="BUF"];
-x2 [shape=box, style=rounded, label="BUF"];
-n1 [ shape=diamond, label="$0\\y[1:0]" ];
-x2:e:e -> n1:w [color="black", style="setlinewidth(3)", label=""];
-c18:p17:e -> n10:w [color="black", style="setlinewidth(3)", label=""];
-n10:e -> c20:p11:w [color="black", style="setlinewidth(3)", label=""];
-c14:p13:e -> c21:p12:w [color="black", style="setlinewidth(3)", label=""];
-n3 [ shape=point ];
-c20:p13:e -> n3:w [color="black", style="setlinewidth(3)", label=""];
-n3:e -> c18:p16:w [color="black", style="setlinewidth(3)", label=""];
-n3:e -> x2:w:w [color="black", style="setlinewidth(3)", label=""];
-x1:e:e -> c20:p19:w [color="black", label=""];
-c21:p13:e -> c20:p12:w [color="black", style="setlinewidth(3)", label=""];
-n6:e -> c14:p11:w [color="black", label=""];
-n7:e -> c14:p12:w [color="black", label=""];
-n8:e -> c21:p19:w [color="black", label=""];
-n8:e -> x1:w:w [color="black", label=""];
-n9:e -> c18:p15:w [color="black", label=""];
-v0:e -> c21:p11:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/example_02.dot b/manual/APPNOTE_011_Design_Investigation/example_02.dot
deleted file mode 100644
index f950ed2ed..000000000
--- a/manual/APPNOTE_011_Design_Investigation/example_02.dot
+++ /dev/null
@@ -1,20 +0,0 @@
-digraph "example" {
-rankdir="LR";
-remincross=true;
-n3 [ shape=octagon, label="a", color="black", fontcolor="black" ];
-n4 [ shape=octagon, label="b", color="black", fontcolor="black" ];
-n5 [ shape=octagon, label="c", color="black", fontcolor="black" ];
-n6 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
-n7 [ shape=octagon, label="y", color="black", fontcolor="black" ];
-c11 [ shape=record, label="{{<p8> A|<p9> B}|$2\n$add|{<p10> Y}}" ];
-c15 [ shape=record, label="{{<p12> CLK|<p13> D}|$7\n$dff|{<p14> Q}}" ];
-c17 [ shape=record, label="{{<p8> A|<p9> B|<p16> S}|$5\n$mux|{<p10> Y}}" ];
-c17:p10:e -> c15:p13:w [color="black", style="setlinewidth(3)", label=""];
-c11:p10:e -> c17:p9:w [color="black", style="setlinewidth(3)", label=""];
-n3:e -> c11:p8:w [color="black", label=""];
-n4:e -> c11:p9:w [color="black", label=""];
-n5:e -> c17:p16:w [color="black", label=""];
-n6:e -> c15:p12:w [color="black", label=""];
-c15:p14:e -> n7:w [color="black", style="setlinewidth(3)", label=""];
-n7:e -> c17:p8:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/example_03.dot b/manual/APPNOTE_011_Design_Investigation/example_03.dot
deleted file mode 100644
index e19d24af7..000000000
--- a/manual/APPNOTE_011_Design_Investigation/example_03.dot
+++ /dev/null
@@ -1,11 +0,0 @@
-digraph "example" {
-rankdir="LR";
-remincross=true;
-v0 [ label="a" ];
-v1 [ label="b" ];
-v2 [ label="$2_Y" ];
-c4 [ shape=record, label="{{<p1> A|<p2> B}|$2\n$add|{<p3> Y}}" ];
-v0:e -> c4:p1:w [color="black", label=""];
-v1:e -> c4:p2:w [color="black", label=""];
-c4:p3:e -> v2:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/foobaraddsub.v b/manual/APPNOTE_011_Design_Investigation/foobaraddsub.v
deleted file mode 100644
index 0f277211d..000000000
--- a/manual/APPNOTE_011_Design_Investigation/foobaraddsub.v
+++ /dev/null
@@ -1,8 +0,0 @@
-module foobaraddsub(a, b, c, d, fa, fs, ba, bs);
-  input [7:0] a, b, c, d;
-  output [7:0] fa, fs, ba, bs;
-  assign fa = a + (* foo *) b;
-  assign fs = a - (* foo *) b;
-  assign ba = c + (* bar *) d;
-  assign bs = c - (* bar *) d;
-endmodule
diff --git a/manual/APPNOTE_011_Design_Investigation/make.sh b/manual/APPNOTE_011_Design_Investigation/make.sh
deleted file mode 100644
index 3845dac6b..000000000
--- a/manual/APPNOTE_011_Design_Investigation/make.sh
+++ /dev/null
@@ -1,23 +0,0 @@
-#!/bin/bash
-set -ex
-if false; then
-	rm -f *.dot
-	../../yosys example.ys
-	../../yosys -p 'proc; opt; show -format dot -prefix splice' splice.v
-	../../yosys -p 'techmap; abc -liberty ../../techlibs/cmos/cmos_cells.lib;; show -format dot -prefix cmos_00' cmos.v
-	../../yosys -p 'techmap; splitnets -ports; abc -liberty ../../techlibs/cmos/cmos_cells.lib;; show -lib ../../techlibs/cmos/cmos_cells.v -format dot -prefix cmos_01' cmos.v
-	../../yosys -p 'opt; cd sumprod; select a:sumstuff; show -format dot -prefix sumprod_00' sumprod.v
-	../../yosys -p 'opt; cd sumprod; select a:sumstuff %x; show -format dot -prefix sumprod_01' sumprod.v
-	../../yosys -p 'opt; cd sumprod; select prod; show -format dot -prefix sumprod_02' sumprod.v
-	../../yosys -p 'opt; cd sumprod; select prod %ci; show -format dot -prefix sumprod_03' sumprod.v
-	../../yosys -p 'opt; cd sumprod; select prod %ci2; show -format dot -prefix sumprod_04' sumprod.v
-	../../yosys -p 'opt; cd sumprod; select prod %ci3; show -format dot -prefix sumprod_05' sumprod.v
-	../../yosys -p 'proc; opt; memory; opt; cd memdemo; show -format dot -prefix memdemo_00' memdemo.v
-	../../yosys -p 'proc; opt; memory; opt; cd memdemo; show -format dot -prefix memdemo_01 y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff' memdemo.v
-	../../yosys submod.ys
-	sed -i '/^label=/ d;' *.dot
-fi
-for dot_file in *.dot; do
-	pdf_file=${dot_file%.dot}.pdf
-	dot -Tpdf -o $pdf_file $dot_file
-done
diff --git a/manual/APPNOTE_011_Design_Investigation/memdemo.v b/manual/APPNOTE_011_Design_Investigation/memdemo.v
deleted file mode 100644
index b39564ddc..000000000
--- a/manual/APPNOTE_011_Design_Investigation/memdemo.v
+++ /dev/null
@@ -1,19 +0,0 @@
-module memdemo(clk, d, y);
-
-input clk;
-input [3:0] d;
-output reg [3:0] y;
-
-integer i;
-reg [1:0] s1, s2;
-reg [3:0] mem [0:3];
-
-always @(posedge clk) begin
-    for (i = 0; i < 4; i = i+1)
-        mem[i] <= mem[(i+1) % 4] + mem[(i+2) % 4];
-    { s2, s1 } = d ? { s1, s2 } ^ d : 4'b0;
-    mem[s1] <= d;
-    y <= mem[s2];
-end
-
-endmodule
diff --git a/manual/APPNOTE_011_Design_Investigation/memdemo_00.dot b/manual/APPNOTE_011_Design_Investigation/memdemo_00.dot
deleted file mode 100644
index 0336a9aac..000000000
--- a/manual/APPNOTE_011_Design_Investigation/memdemo_00.dot
+++ /dev/null
@@ -1,138 +0,0 @@
-digraph "memdemo" {
-rankdir="LR";
-remincross=true;
-n24 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
-n25 [ shape=octagon, label="d", color="black", fontcolor="black" ];
-n26 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ];
-n27 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ];
-n28 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ];
-n29 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ];
-n30 [ shape=diamond, label="s1", color="black", fontcolor="black" ];
-n31 [ shape=diamond, label="s2", color="black", fontcolor="black" ];
-n32 [ shape=octagon, label="y", color="black", fontcolor="black" ];
-c36 [ shape=record, label="{{<p33> A|<p34> B}|$28\n$add|{<p35> Y}}" ];
-c37 [ shape=record, label="{{<p33> A|<p34> B}|$31\n$add|{<p35> Y}}" ];
-c38 [ shape=record, label="{{<p33> A|<p34> B}|$34\n$add|{<p35> Y}}" ];
-c39 [ shape=record, label="{{<p33> A|<p34> B}|$37\n$add|{<p35> Y}}" ];
-c41 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$110\n$mux|{<p35> Y}}" ];
-x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
-x0:e -> c41:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
-c42 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$113\n$mux|{<p35> Y}}" ];
-x1 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
-x1:e -> c42:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
-c43 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$116\n$mux|{<p35> Y}}" ];
-x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
-x2:e -> c43:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
-v3 [ label="1'1" ];
-c44 [ shape=record, label="{{<p33> A|<p34> B}|$145\n$and|{<p35> Y}}" ];
-v4 [ label="1'1" ];
-c45 [ shape=record, label="{{<p33> A|<p34> B}|$175\n$and|{<p35> Y}}" ];
-v5 [ label="1'1" ];
-c46 [ shape=record, label="{{<p33> A|<p34> B}|$205\n$and|{<p35> Y}}" ];
-v6 [ label="1'1" ];
-c47 [ shape=record, label="{{<p33> A|<p34> B}|$235\n$and|{<p35> Y}}" ];
-v7 [ label="2'00" ];
-c48 [ shape=record, label="{{<p33> A|<p34> B}|$143\n$eq|{<p35> Y}}" ];
-v8 [ label="2'01" ];
-c49 [ shape=record, label="{{<p33> A|<p34> B}|$173\n$eq|{<p35> Y}}" ];
-v9 [ label="2'10" ];
-c50 [ shape=record, label="{{<p33> A|<p34> B}|$203\n$eq|{<p35> Y}}" ];
-v10 [ label="2'11" ];
-c51 [ shape=record, label="{{<p33> A|<p34> B}|$233\n$eq|{<p35> Y}}" ];
-c52 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$147\n$mux|{<p35> Y}}" ];
-c53 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$177\n$mux|{<p35> Y}}" ];
-c54 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$207\n$mux|{<p35> Y}}" ];
-c55 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$237\n$mux|{<p35> Y}}" ];
-c59 [ shape=record, label="{{<p56> CLK|<p57> D}|$66\n$dff|{<p58> Q}}" ];
-c60 [ shape=record, label="{{<p56> CLK|<p57> D}|$68\n$dff|{<p58> Q}}" ];
-c61 [ shape=record, label="{{<p56> CLK|<p57> D}|$70\n$dff|{<p58> Q}}" ];
-c62 [ shape=record, label="{{<p56> CLK|<p57> D}|$72\n$dff|{<p58> Q}}" ];
-c63 [ shape=record, label="{{<p56> CLK|<p57> D}|$59\n$dff|{<p58> Q}}" ];
-c64 [ shape=record, label="{{<p56> CLK|<p57> D}|$63\n$dff|{<p58> Q}}" ];
-c65 [ shape=record, label="{{<p56> CLK|<p57> D}|$64\n$dff|{<p58> Q}}" ];
-c66 [ shape=record, label="{{<p33> A}|$39\n$reduce_bool|{<p35> Y}}" ];
-v11 [ label="4'0000" ];
-c67 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$40\n$mux|{<p35> Y}}" ];
-x12 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 1:0 " ];
-c67:p35:e -> x12:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
-c68 [ shape=record, label="{{<p33> A|<p34> B}|$38\n$xor|{<p35> Y}}" ];
-x13 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
-x13:e -> c68:p33:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
-c36:p35:e -> c52:p33:w [color="black", style="setlinewidth(3)", label=""];
-c44:p35:e -> c52:p40:w [color="black", label=""];
-c45:p35:e -> c53:p40:w [color="black", label=""];
-c46:p35:e -> c54:p40:w [color="black", label=""];
-c47:p35:e -> c55:p40:w [color="black", label=""];
-c48:p35:e -> c44:p33:w [color="black", label=""];
-c49:p35:e -> c45:p33:w [color="black", label=""];
-c50:p35:e -> c46:p33:w [color="black", label=""];
-c51:p35:e -> c47:p33:w [color="black", label=""];
-c52:p35:e -> c59:p57:w [color="black", style="setlinewidth(3)", label=""];
-c53:p35:e -> c60:p57:w [color="black", style="setlinewidth(3)", label=""];
-c37:p35:e -> c53:p33:w [color="black", style="setlinewidth(3)", label=""];
-c54:p35:e -> c61:p57:w [color="black", style="setlinewidth(3)", label=""];
-c55:p35:e -> c62:p57:w [color="black", style="setlinewidth(3)", label=""];
-c66:p35:e -> c67:p40:w [color="black", label=""];
-c68:p35:e -> c67:p34:w [color="black", style="setlinewidth(3)", label=""];
-n24:e -> c59:p56:w [color="black", label=""];
-n24:e -> c60:p56:w [color="black", label=""];
-n24:e -> c61:p56:w [color="black", label=""];
-n24:e -> c62:p56:w [color="black", label=""];
-n24:e -> c63:p56:w [color="black", label=""];
-n24:e -> c64:p56:w [color="black", label=""];
-n24:e -> c65:p56:w [color="black", label=""];
-n25:e -> c52:p34:w [color="black", style="setlinewidth(3)", label=""];
-n25:e -> c53:p34:w [color="black", style="setlinewidth(3)", label=""];
-n25:e -> c54:p34:w [color="black", style="setlinewidth(3)", label=""];
-n25:e -> c55:p34:w [color="black", style="setlinewidth(3)", label=""];
-n25:e -> c66:p33:w [color="black", style="setlinewidth(3)", label=""];
-n25:e -> c68:p34:w [color="black", style="setlinewidth(3)", label=""];
-c59:p58:e -> n26:w [color="black", style="setlinewidth(3)", label=""];
-n26:e -> c38:p34:w [color="black", style="setlinewidth(3)", label=""];
-n26:e -> c39:p33:w [color="black", style="setlinewidth(3)", label=""];
-n26:e -> c42:p33:w [color="black", style="setlinewidth(3)", label=""];
-c60:p58:e -> n27:w [color="black", style="setlinewidth(3)", label=""];
-n27:e -> c36:p33:w [color="black", style="setlinewidth(3)", label=""];
-n27:e -> c39:p34:w [color="black", style="setlinewidth(3)", label=""];
-n27:e -> c42:p34:w [color="black", style="setlinewidth(3)", label=""];
-c61:p58:e -> n28:w [color="black", style="setlinewidth(3)", label=""];
-n28:e -> c36:p34:w [color="black", style="setlinewidth(3)", label=""];
-n28:e -> c37:p33:w [color="black", style="setlinewidth(3)", label=""];
-n28:e -> c43:p33:w [color="black", style="setlinewidth(3)", label=""];
-c62:p58:e -> n29:w [color="black", style="setlinewidth(3)", label=""];
-n29:e -> c37:p34:w [color="black", style="setlinewidth(3)", label=""];
-n29:e -> c38:p33:w [color="black", style="setlinewidth(3)", label=""];
-n29:e -> c43:p34:w [color="black", style="setlinewidth(3)", label=""];
-c38:p35:e -> c54:p33:w [color="black", style="setlinewidth(3)", label=""];
-c63:p58:e -> n30:w [color="black", style="setlinewidth(3)", label=""];
-n30:e -> x13:s1:w [color="black", style="setlinewidth(3)", label=""];
-c64:p58:e -> n31:w [color="black", style="setlinewidth(3)", label=""];
-n31:e -> x13:s0:w [color="black", style="setlinewidth(3)", label=""];
-c65:p58:e -> n32:w [color="black", style="setlinewidth(3)", label=""];
-c39:p35:e -> c55:p33:w [color="black", style="setlinewidth(3)", label=""];
-n5 [ shape=point ];
-x12:s0:e -> n5:w [color="black", style="setlinewidth(3)", label=""];
-n5:e -> c48:p34:w [color="black", style="setlinewidth(3)", label=""];
-n5:e -> c49:p34:w [color="black", style="setlinewidth(3)", label=""];
-n5:e -> c50:p34:w [color="black", style="setlinewidth(3)", label=""];
-n5:e -> c51:p34:w [color="black", style="setlinewidth(3)", label=""];
-n5:e -> c63:p57:w [color="black", style="setlinewidth(3)", label=""];
-n6 [ shape=point ];
-x12:s1:e -> n6:w [color="black", style="setlinewidth(3)", label=""];
-n6:e -> c64:p57:w [color="black", style="setlinewidth(3)", label=""];
-n6:e -> x0:s0:w [color="black", style="setlinewidth(3)", label=""];
-n6:e -> x1:s0:w [color="black", style="setlinewidth(3)", label=""];
-n6:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""];
-c41:p35:e -> c65:p57:w [color="black", style="setlinewidth(3)", label=""];
-c42:p35:e -> c41:p33:w [color="black", style="setlinewidth(3)", label=""];
-c43:p35:e -> c41:p34:w [color="black", style="setlinewidth(3)", label=""];
-v10:e -> c51:p33:w [color="black", style="setlinewidth(3)", label=""];
-v11:e -> c67:p33:w [color="black", style="setlinewidth(3)", label=""];
-v3:e -> c44:p34:w [color="black", label=""];
-v4:e -> c45:p34:w [color="black", label=""];
-v5:e -> c46:p34:w [color="black", label=""];
-v6:e -> c47:p34:w [color="black", label=""];
-v7:e -> c48:p33:w [color="black", style="setlinewidth(3)", label=""];
-v8:e -> c49:p33:w [color="black", style="setlinewidth(3)", label=""];
-v9:e -> c50:p33:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/memdemo_01.dot b/manual/APPNOTE_011_Design_Investigation/memdemo_01.dot
deleted file mode 100644
index 2ad92c78b..000000000
--- a/manual/APPNOTE_011_Design_Investigation/memdemo_01.dot
+++ /dev/null
@@ -1,29 +0,0 @@
-digraph "memdemo" {
-rankdir="LR";
-remincross=true;
-n4 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ];
-n5 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ];
-n6 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ];
-n7 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ];
-n8 [ shape=octagon, label="y", color="black", fontcolor="black" ];
-v0 [ label="$0\\s2[1:0] [1]" ];
-c13 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$110\n$mux|{<p12> Y}}" ];
-v1 [ label="$0\\s2[1:0] [0]" ];
-c14 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$113\n$mux|{<p12> Y}}" ];
-v2 [ label="$0\\s2[1:0] [0]" ];
-c15 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$116\n$mux|{<p12> Y}}" ];
-v3 [ label="clk" ];
-c19 [ shape=record, label="{{<p16> CLK|<p17> D}|$64\n$dff|{<p18> Q}}" ];
-c13:p12:e -> c19:p17:w [color="black", style="setlinewidth(3)", label=""];
-c14:p12:e -> c13:p9:w [color="black", style="setlinewidth(3)", label=""];
-c15:p12:e -> c13:p10:w [color="black", style="setlinewidth(3)", label=""];
-n4:e -> c14:p9:w [color="black", style="setlinewidth(3)", label=""];
-n5:e -> c14:p10:w [color="black", style="setlinewidth(3)", label=""];
-n6:e -> c15:p9:w [color="black", style="setlinewidth(3)", label=""];
-n7:e -> c15:p10:w [color="black", style="setlinewidth(3)", label=""];
-c19:p18:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
-v0:e -> c13:p11:w [color="black", label=""];
-v1:e -> c14:p11:w [color="black", label=""];
-v2:e -> c15:p11:w [color="black", label=""];
-v3:e -> c19:p16:w [color="black", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/primetest.v b/manual/APPNOTE_011_Design_Investigation/primetest.v
deleted file mode 100644
index 6cb766b73..000000000
--- a/manual/APPNOTE_011_Design_Investigation/primetest.v
+++ /dev/null
@@ -1,4 +0,0 @@
-module primetest(p, a, b, ok);
-input [15:0] p, a, b;
-output ok = p != a*b || a == 1 || b == 1;
-endmodule
diff --git a/manual/APPNOTE_011_Design_Investigation/splice.dot b/manual/APPNOTE_011_Design_Investigation/splice.dot
deleted file mode 100644
index 4657feed1..000000000
--- a/manual/APPNOTE_011_Design_Investigation/splice.dot
+++ /dev/null
@@ -1,39 +0,0 @@
-digraph "splice_demo" {
-rankdir="LR";
-remincross=true;
-n1 [ shape=octagon, label="a", color="black", fontcolor="black" ];
-n2 [ shape=octagon, label="b", color="black", fontcolor="black" ];
-n3 [ shape=octagon, label="c", color="black", fontcolor="black" ];
-n4 [ shape=octagon, label="d", color="black", fontcolor="black" ];
-n5 [ shape=octagon, label="e", color="black", fontcolor="black" ];
-n6 [ shape=octagon, label="f", color="black", fontcolor="black" ];
-n7 [ shape=octagon, label="x", color="black", fontcolor="black" ];
-n8 [ shape=octagon, label="y", color="black", fontcolor="black" ];
-c11 [ shape=record, label="{{<p9> A}|$2\n$neg|{<p10> Y}}" ];
-x0 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
-x0:e -> c11:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
-x1 [ shape=record, style=rounded, label="<s0> 3:0 - 7:4 " ];
-c11:p10:e -> x1:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
-c12 [ shape=record, label="{{<p9> A}|$1\n$not|{<p10> Y}}" ];
-x2 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
-x2:e -> c12:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
-x3 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 3:2 " ];
-c12:p10:e -> x3:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
-x4 [ shape=record, style=rounded, label="<s1> 0:0 - 1:1 |<s0> 1:1 - 0:0 " ];
-x5 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
-x6 [ shape=record, style=rounded, label="<s0> 3:0 - 11:8 " ];
-x5:e -> x6:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
-n1:e -> x4:s0:w [color="black", style="setlinewidth(3)", label=""];
-n1:e -> x4:s1:w [color="black", style="setlinewidth(3)", label=""];
-n1:e -> x5:s1:w [color="black", style="setlinewidth(3)", label=""];
-n2:e -> x5:s0:w [color="black", style="setlinewidth(3)", label=""];
-n3:e -> x0:s1:w [color="black", style="setlinewidth(3)", label=""];
-n4:e -> x0:s0:w [color="black", style="setlinewidth(3)", label=""];
-n5:e -> x2:s1:w [color="black", style="setlinewidth(3)", label=""];
-n6:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""];
-x4:e -> n7:w [color="black", style="setlinewidth(3)", label=""];
-x1:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
-x3:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
-x3:s1:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
-x6:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/splice.v b/manual/APPNOTE_011_Design_Investigation/splice.v
deleted file mode 100644
index 1cf7274c0..000000000
--- a/manual/APPNOTE_011_Design_Investigation/splice.v
+++ /dev/null
@@ -1,10 +0,0 @@
-module splice_demo(a, b, c, d, e, f, x, y);
-
-input [1:0] a, b, c, d, e, f;
-output [1:0] x = {a[0], a[1]};
-
-output [11:0] y;
-assign {y[11:4], y[1:0], y[3:2]} =
-                {a, b, -{c, d}, ~{e, f}};
-
-endmodule
diff --git a/manual/APPNOTE_011_Design_Investigation/submod.ys b/manual/APPNOTE_011_Design_Investigation/submod.ys
deleted file mode 100644
index 29ad61076..000000000
--- a/manual/APPNOTE_011_Design_Investigation/submod.ys
+++ /dev/null
@@ -1,16 +0,0 @@
-read_verilog memdemo.v
-proc; opt; memory; opt
-
-cd memdemo
-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
-
-cd ..
-show -format dot -prefix submod_00 memdemo
-show -format dot -prefix submod_01 scramble
-show -format dot -prefix submod_02 outstage
-show -format dot -prefix submod_03 selstage
diff --git a/manual/APPNOTE_011_Design_Investigation/submod_00.dot b/manual/APPNOTE_011_Design_Investigation/submod_00.dot
deleted file mode 100644
index 2e55268ee..000000000
--- a/manual/APPNOTE_011_Design_Investigation/submod_00.dot
+++ /dev/null
@@ -1,45 +0,0 @@
-digraph "memdemo" {
-rankdir="LR";
-remincross=true;
-n5 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
-n6 [ shape=octagon, label="d", color="black", fontcolor="black" ];
-n7 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ];
-n8 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ];
-n9 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ];
-n10 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ];
-n11 [ shape=diamond, label="s1", color="black", fontcolor="black" ];
-n12 [ shape=diamond, label="s2", color="black", fontcolor="black" ];
-n13 [ shape=octagon, label="y", color="black", fontcolor="black" ];
-c17 [ shape=record, label="{{<p14> CLK|<p15> D}|$59\n$dff|{<p16> Q}}" ];
-c18 [ shape=record, label="{{<p14> CLK|<p15> D}|$63\n$dff|{<p16> Q}}" ];
-c20 [ shape=record, label="{{<p5> clk|<p7> mem[0]|<p8> mem[1]|<p9> mem[2]|<p10> mem[3]|<p19> n1}|outstage\noutstage|{<p13> y}}" ];
-c21 [ shape=record, label="{{<p5> clk|<p6> d|<p19> n1}|scramble\nscramble|{<p7> mem[0]|<p8> mem[1]|<p9> mem[2]|<p10> mem[3]}}" ];
-c23 [ shape=record, label="{{<p6> d|<p11> s1|<p12> s2}|selstage\nselstage|{<p19> n1|<p22> n2}}" ];
-n1 [ shape=point ];
-c23:p19:e -> n1:w [color="black", style="setlinewidth(3)", label=""];
-n1:e -> c17:p15:w [color="black", style="setlinewidth(3)", label=""];
-n1:e -> c21:p19:w [color="black", style="setlinewidth(3)", label=""];
-c21:p10:e -> n10:w [color="black", style="setlinewidth(3)", label=""];
-n10:e -> c20:p10:w [color="black", style="setlinewidth(3)", label=""];
-c17:p16:e -> n11:w [color="black", style="setlinewidth(3)", label=""];
-n11:e -> c23:p11:w [color="black", style="setlinewidth(3)", label=""];
-c18:p16:e -> n12:w [color="black", style="setlinewidth(3)", label=""];
-n12:e -> c23:p12:w [color="black", style="setlinewidth(3)", label=""];
-c20:p13:e -> n13:w [color="black", style="setlinewidth(3)", label=""];
-n2 [ shape=point ];
-c23:p22:e -> n2:w [color="black", style="setlinewidth(3)", label=""];
-n2:e -> c18:p15:w [color="black", style="setlinewidth(3)", label=""];
-n2:e -> c20:p19:w [color="black", style="setlinewidth(3)", label=""];
-n5:e -> c17:p14:w [color="black", label=""];
-n5:e -> c18:p14:w [color="black", label=""];
-n5:e -> c20:p5:w [color="black", label=""];
-n5:e -> c21:p5:w [color="black", label=""];
-n6:e -> c21:p6:w [color="black", style="setlinewidth(3)", label=""];
-n6:e -> c23:p6:w [color="black", style="setlinewidth(3)", label=""];
-c21:p7:e -> n7:w [color="black", style="setlinewidth(3)", label=""];
-n7:e -> c20:p7:w [color="black", style="setlinewidth(3)", label=""];
-c21:p8:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
-n8:e -> c20:p8:w [color="black", style="setlinewidth(3)", label=""];
-c21:p9:e -> n9:w [color="black", style="setlinewidth(3)", label=""];
-n9:e -> c20:p9:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/submod_01.dot b/manual/APPNOTE_011_Design_Investigation/submod_01.dot
deleted file mode 100644
index f8f8c008a..000000000
--- a/manual/APPNOTE_011_Design_Investigation/submod_01.dot
+++ /dev/null
@@ -1,87 +0,0 @@
-digraph "scramble" {
-rankdir="LR";
-remincross=true;
-n17 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
-n18 [ shape=octagon, label="d", color="black", fontcolor="black" ];
-n19 [ shape=octagon, label="mem[0]", color="black", fontcolor="black" ];
-n20 [ shape=octagon, label="mem[1]", color="black", fontcolor="black" ];
-n21 [ shape=octagon, label="mem[2]", color="black", fontcolor="black" ];
-n22 [ shape=octagon, label="mem[3]", color="black", fontcolor="black" ];
-n23 [ shape=octagon, label="n1", color="black", fontcolor="black" ];
-c27 [ shape=record, label="{{<p24> A|<p25> B}|$28\n$add|{<p26> Y}}" ];
-c28 [ shape=record, label="{{<p24> A|<p25> B}|$31\n$add|{<p26> Y}}" ];
-c29 [ shape=record, label="{{<p24> A|<p25> B}|$34\n$add|{<p26> Y}}" ];
-c30 [ shape=record, label="{{<p24> A|<p25> B}|$37\n$add|{<p26> Y}}" ];
-v0 [ label="1'1" ];
-c31 [ shape=record, label="{{<p24> A|<p25> B}|$145\n$and|{<p26> Y}}" ];
-v1 [ label="1'1" ];
-c32 [ shape=record, label="{{<p24> A|<p25> B}|$175\n$and|{<p26> Y}}" ];
-v2 [ label="1'1" ];
-c33 [ shape=record, label="{{<p24> A|<p25> B}|$205\n$and|{<p26> Y}}" ];
-v3 [ label="1'1" ];
-c34 [ shape=record, label="{{<p24> A|<p25> B}|$235\n$and|{<p26> Y}}" ];
-v4 [ label="2'00" ];
-c35 [ shape=record, label="{{<p24> A|<p25> B}|$143\n$eq|{<p26> Y}}" ];
-v5 [ label="2'01" ];
-c36 [ shape=record, label="{{<p24> A|<p25> B}|$173\n$eq|{<p26> Y}}" ];
-v6 [ label="2'10" ];
-c37 [ shape=record, label="{{<p24> A|<p25> B}|$203\n$eq|{<p26> Y}}" ];
-v7 [ label="2'11" ];
-c38 [ shape=record, label="{{<p24> A|<p25> B}|$233\n$eq|{<p26> Y}}" ];
-c40 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$147\n$mux|{<p26> Y}}" ];
-c41 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$177\n$mux|{<p26> Y}}" ];
-c42 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$207\n$mux|{<p26> Y}}" ];
-c43 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$237\n$mux|{<p26> Y}}" ];
-c47 [ shape=record, label="{{<p44> CLK|<p45> D}|$66\n$dff|{<p46> Q}}" ];
-c48 [ shape=record, label="{{<p44> CLK|<p45> D}|$68\n$dff|{<p46> Q}}" ];
-c49 [ shape=record, label="{{<p44> CLK|<p45> D}|$70\n$dff|{<p46> Q}}" ];
-c50 [ shape=record, label="{{<p44> CLK|<p45> D}|$72\n$dff|{<p46> Q}}" ];
-c27:p26:e -> c40:p24:w [color="black", style="setlinewidth(3)", label=""];
-c36:p26:e -> c32:p24:w [color="black", label=""];
-c37:p26:e -> c33:p24:w [color="black", label=""];
-c38:p26:e -> c34:p24:w [color="black", label=""];
-c40:p26:e -> c47:p45:w [color="black", style="setlinewidth(3)", label=""];
-c41:p26:e -> c48:p45:w [color="black", style="setlinewidth(3)", label=""];
-c42:p26:e -> c49:p45:w [color="black", style="setlinewidth(3)", label=""];
-c43:p26:e -> c50:p45:w [color="black", style="setlinewidth(3)", label=""];
-n17:e -> c47:p44:w [color="black", label=""];
-n17:e -> c48:p44:w [color="black", label=""];
-n17:e -> c49:p44:w [color="black", label=""];
-n17:e -> c50:p44:w [color="black", label=""];
-n18:e -> c40:p25:w [color="black", style="setlinewidth(3)", label=""];
-n18:e -> c41:p25:w [color="black", style="setlinewidth(3)", label=""];
-n18:e -> c42:p25:w [color="black", style="setlinewidth(3)", label=""];
-n18:e -> c43:p25:w [color="black", style="setlinewidth(3)", label=""];
-c47:p46:e -> n19:w [color="black", style="setlinewidth(3)", label=""];
-n19:e -> c29:p25:w [color="black", style="setlinewidth(3)", label=""];
-n19:e -> c30:p24:w [color="black", style="setlinewidth(3)", label=""];
-c28:p26:e -> c41:p24:w [color="black", style="setlinewidth(3)", label=""];
-c48:p46:e -> n20:w [color="black", style="setlinewidth(3)", label=""];
-n20:e -> c27:p24:w [color="black", style="setlinewidth(3)", label=""];
-n20:e -> c30:p25:w [color="black", style="setlinewidth(3)", label=""];
-c49:p46:e -> n21:w [color="black", style="setlinewidth(3)", label=""];
-n21:e -> c27:p25:w [color="black", style="setlinewidth(3)", label=""];
-n21:e -> c28:p24:w [color="black", style="setlinewidth(3)", label=""];
-c50:p46:e -> n22:w [color="black", style="setlinewidth(3)", label=""];
-n22:e -> c28:p25:w [color="black", style="setlinewidth(3)", label=""];
-n22:e -> c29:p24:w [color="black", style="setlinewidth(3)", label=""];
-n23:e -> c35:p25:w [color="black", style="setlinewidth(3)", label=""];
-n23:e -> c36:p25:w [color="black", style="setlinewidth(3)", label=""];
-n23:e -> c37:p25:w [color="black", style="setlinewidth(3)", label=""];
-n23:e -> c38:p25:w [color="black", style="setlinewidth(3)", label=""];
-c29:p26:e -> c42:p24:w [color="black", style="setlinewidth(3)", label=""];
-c30:p26:e -> c43:p24:w [color="black", style="setlinewidth(3)", label=""];
-c31:p26:e -> c40:p39:w [color="black", label=""];
-c32:p26:e -> c41:p39:w [color="black", label=""];
-c33:p26:e -> c42:p39:w [color="black", label=""];
-c34:p26:e -> c43:p39:w [color="black", label=""];
-c35:p26:e -> c31:p24:w [color="black", label=""];
-v0:e -> c31:p25:w [color="black", label=""];
-v1:e -> c32:p25:w [color="black", label=""];
-v2:e -> c33:p25:w [color="black", label=""];
-v3:e -> c34:p25:w [color="black", label=""];
-v4:e -> c35:p24:w [color="black", style="setlinewidth(3)", label=""];
-v5:e -> c36:p24:w [color="black", style="setlinewidth(3)", label=""];
-v6:e -> c37:p24:w [color="black", style="setlinewidth(3)", label=""];
-v7:e -> c38:p24:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/submod_02.dot b/manual/APPNOTE_011_Design_Investigation/submod_02.dot
deleted file mode 100644
index 1a672c484..000000000
--- a/manual/APPNOTE_011_Design_Investigation/submod_02.dot
+++ /dev/null
@@ -1,33 +0,0 @@
-digraph "outstage" {
-rankdir="LR";
-remincross=true;
-n4 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
-n5 [ shape=octagon, label="mem[0]", color="black", fontcolor="black" ];
-n6 [ shape=octagon, label="mem[1]", color="black", fontcolor="black" ];
-n7 [ shape=octagon, label="mem[2]", color="black", fontcolor="black" ];
-n8 [ shape=octagon, label="mem[3]", color="black", fontcolor="black" ];
-n9 [ shape=octagon, label="n1", color="black", fontcolor="black" ];
-n10 [ shape=octagon, label="y", color="black", fontcolor="black" ];
-c15 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$110\n$mux|{<p14> Y}}" ];
-x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
-x0:e -> c15:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
-c16 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$113\n$mux|{<p14> Y}}" ];
-x1 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
-x1:e -> c16:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
-c17 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$116\n$mux|{<p14> Y}}" ];
-x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
-x2:e -> c17:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
-c21 [ shape=record, label="{{<p18> CLK|<p19> D}|$64\n$dff|{<p20> Q}}" ];
-c15:p14:e -> c21:p19:w [color="black", style="setlinewidth(3)", label=""];
-c21:p20:e -> n10:w [color="black", style="setlinewidth(3)", label=""];
-c16:p14:e -> c15:p11:w [color="black", style="setlinewidth(3)", label=""];
-c17:p14:e -> c15:p12:w [color="black", style="setlinewidth(3)", label=""];
-n4:e -> c21:p18:w [color="black", label=""];
-n5:e -> c16:p11:w [color="black", style="setlinewidth(3)", label=""];
-n6:e -> c16:p12:w [color="black", style="setlinewidth(3)", label=""];
-n7:e -> c17:p11:w [color="black", style="setlinewidth(3)", label=""];
-n8:e -> c17:p12:w [color="black", style="setlinewidth(3)", label=""];
-n9:e -> x0:s0:w [color="black", label=""];
-n9:e -> x1:s0:w [color="black", label=""];
-n9:e -> x2:s0:w [color="black", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/submod_03.dot b/manual/APPNOTE_011_Design_Investigation/submod_03.dot
deleted file mode 100644
index 0dbbe3baa..000000000
--- a/manual/APPNOTE_011_Design_Investigation/submod_03.dot
+++ /dev/null
@@ -1,26 +0,0 @@
-digraph "selstage" {
-rankdir="LR";
-remincross=true;
-n3 [ shape=octagon, label="d", color="black", fontcolor="black" ];
-n4 [ shape=octagon, label="n1", color="black", fontcolor="black" ];
-n5 [ shape=octagon, label="n2", color="black", fontcolor="black" ];
-n6 [ shape=octagon, label="s1", color="black", fontcolor="black" ];
-n7 [ shape=octagon, label="s2", color="black", fontcolor="black" ];
-c10 [ shape=record, label="{{<p8> A}|$39\n$reduce_bool|{<p9> Y}}" ];
-v0 [ label="4'0000" ];
-c13 [ shape=record, label="{{<p8> A|<p11> B|<p12> S}|$40\n$mux|{<p9> Y}}" ];
-x1 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 1:0 " ];
-c13:p9:e -> x1:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
-c14 [ shape=record, label="{{<p8> A|<p11> B}|$38\n$xor|{<p9> Y}}" ];
-x2 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
-x2:e -> c14:p8:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
-c10:p9:e -> c13:p12:w [color="black", label=""];
-c14:p9:e -> c13:p11:w [color="black", style="setlinewidth(3)", label=""];
-n3:e -> c10:p8:w [color="black", style="setlinewidth(3)", label=""];
-n3:e -> c14:p11:w [color="black", style="setlinewidth(3)", label=""];
-x1:s0:e -> n4:w [color="black", style="setlinewidth(3)", label=""];
-x1:s1:e -> n5:w [color="black", style="setlinewidth(3)", label=""];
-n6:e -> x2:s1:w [color="black", style="setlinewidth(3)", label=""];
-n7:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""];
-v0:e -> c13:p8:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod.v b/manual/APPNOTE_011_Design_Investigation/sumprod.v
deleted file mode 100644
index 4091bf0a1..000000000
--- a/manual/APPNOTE_011_Design_Investigation/sumprod.v
+++ /dev/null
@@ -1,12 +0,0 @@
-module sumprod(a, b, c, sum, prod);
-
-  input [7:0] a, b, c;
-  output [7:0] sum, prod;
-
-  {* sumstuff *}
-  assign sum = a + b + c;
-  {* *}
-
-  assign prod = a * b * c;
-
-endmodule
diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_00.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_00.dot
deleted file mode 100644
index 06522dcc9..000000000
--- a/manual/APPNOTE_011_Design_Investigation/sumprod_00.dot
+++ /dev/null
@@ -1,18 +0,0 @@
-digraph "sumprod" {
-rankdir="LR";
-remincross=true;
-v0 [ label="a" ];
-v1 [ label="b" ];
-v2 [ label="$1_Y" ];
-c4 [ shape=record, label="{{<p1> A|<p2> B}|$1\n$add|{<p3> Y}}" ];
-v3 [ label="$1_Y" ];
-v4 [ label="c" ];
-v5 [ label="sum" ];
-c5 [ shape=record, label="{{<p1> A|<p2> B}|$2\n$add|{<p3> Y}}" ];
-v0:e -> c4:p1:w [color="black", style="setlinewidth(3)", label=""];
-v1:e -> c4:p2:w [color="black", style="setlinewidth(3)", label=""];
-c4:p3:e -> v2:w [color="black", style="setlinewidth(3)", label=""];
-v3:e -> c5:p1:w [color="black", style="setlinewidth(3)", label=""];
-v4:e -> c5:p2:w [color="black", style="setlinewidth(3)", label=""];
-c5:p3:e -> v5:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_01.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_01.dot
deleted file mode 100644
index aefe7a6da..000000000
--- a/manual/APPNOTE_011_Design_Investigation/sumprod_01.dot
+++ /dev/null
@@ -1,15 +0,0 @@
-digraph "sumprod" {
-rankdir="LR";
-remincross=true;
-n2 [ shape=octagon, label="a", color="black", fontcolor="black" ];
-n3 [ shape=octagon, label="b", color="black", fontcolor="black" ];
-n4 [ shape=octagon, label="c", color="black", fontcolor="black" ];
-n5 [ shape=octagon, label="sum", color="black", fontcolor="black" ];
-c9 [ shape=record, label="{{<p6> A|<p7> B}|$1\n$add|{<p8> Y}}" ];
-c10 [ shape=record, label="{{<p6> A|<p7> B}|$2\n$add|{<p8> Y}}" ];
-c9:p8:e -> c10:p6:w [color="black", style="setlinewidth(3)", label=""];
-n2:e -> c9:p6:w [color="black", style="setlinewidth(3)", label=""];
-n3:e -> c9:p7:w [color="black", style="setlinewidth(3)", label=""];
-n4:e -> c10:p7:w [color="black", style="setlinewidth(3)", label=""];
-c10:p8:e -> n5:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_02.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_02.dot
deleted file mode 100644
index 4646c9947..000000000
--- a/manual/APPNOTE_011_Design_Investigation/sumprod_02.dot
+++ /dev/null
@@ -1,5 +0,0 @@
-digraph "sumprod" {
-rankdir="LR";
-remincross=true;
-n1 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_03.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_03.dot
deleted file mode 100644
index dcfea2b56..000000000
--- a/manual/APPNOTE_011_Design_Investigation/sumprod_03.dot
+++ /dev/null
@@ -1,11 +0,0 @@
-digraph "sumprod" {
-rankdir="LR";
-remincross=true;
-n1 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
-v0 [ label="$3_Y" ];
-v1 [ label="c" ];
-c5 [ shape=record, label="{{<p2> A|<p3> B}|$4\n$mul|{<p4> Y}}" ];
-c5:p4:e -> n1:w [color="black", style="setlinewidth(3)", label=""];
-v0:e -> c5:p2:w [color="black", style="setlinewidth(3)", label=""];
-v1:e -> c5:p3:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_04.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_04.dot
deleted file mode 100644
index e77c41aa2..000000000
--- a/manual/APPNOTE_011_Design_Investigation/sumprod_04.dot
+++ /dev/null
@@ -1,11 +0,0 @@
-digraph "sumprod" {
-rankdir="LR";
-remincross=true;
-n2 [ shape=octagon, label="c", color="black", fontcolor="black" ];
-n3 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
-c7 [ shape=record, label="{{<p4> A|<p5> B}|$4\n$mul|{<p6> Y}}" ];
-n1 [ shape=diamond, label="$3_Y" ];
-n1:e -> c7:p4:w [color="black", style="setlinewidth(3)", label=""];
-n2:e -> c7:p5:w [color="black", style="setlinewidth(3)", label=""];
-c7:p6:e -> n3:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_05.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_05.dot
deleted file mode 100644
index b54441290..000000000
--- a/manual/APPNOTE_011_Design_Investigation/sumprod_05.dot
+++ /dev/null
@@ -1,15 +0,0 @@
-digraph "sumprod" {
-rankdir="LR";
-remincross=true;
-n2 [ shape=octagon, label="c", color="black", fontcolor="black" ];
-n3 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
-v0 [ label="a" ];
-v1 [ label="b" ];
-c7 [ shape=record, label="{{<p4> A|<p5> B}|$3\n$mul|{<p6> Y}}" ];
-c8 [ shape=record, label="{{<p4> A|<p5> B}|$4\n$mul|{<p6> Y}}" ];
-c7:p6:e -> c8:p4:w [color="black", style="setlinewidth(3)", label=""];
-n2:e -> c8:p5:w [color="black", style="setlinewidth(3)", label=""];
-c8:p6:e -> n3:w [color="black", style="setlinewidth(3)", label=""];
-v0:e -> c7:p4:w [color="black", style="setlinewidth(3)", label=""];
-v1:e -> c7:p5:w [color="black", style="setlinewidth(3)", label=""];
-}
diff --git a/manual/APPNOTE_012_Verilog_to_BTOR.tex b/manual/APPNOTE_012_Verilog_to_BTOR.tex
deleted file mode 100644
index aabdc63c4..000000000
--- a/manual/APPNOTE_012_Verilog_to_BTOR.tex
+++ /dev/null
@@ -1,435 +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}
-
-\lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=2em,xrightmargin=1em,numbers=left}
-
-\begin{document}
-
-\title{Yosys Application Note 012: \\ Converting Verilog to BTOR}
-\author{Ahmed Irfan and Claire Xenia Wolf \\ April 2015}
-\maketitle
-
-\begin{abstract}
-Verilog-2005 is a powerful Hardware Description Language (HDL) that
-can be used to easily create complex designs from small HDL code.
-BTOR~\cite{btor} is a bit-precise word-level format for model
-checking.  It is a simple format and easy to parse. It allows to model
-the model checking problem over the theory of bit-vectors with
-one-dimensional arrays, thus enabling to model Verilog designs with
-registers and memories.  Yosys~\cite{yosys} is an Open-Source Verilog
-synthesis tool that can be used to convert Verilog designs with simple
-assertions to BTOR format.
-
-\end{abstract}
-
-\section{Installation}
-
-Yosys written in C++ (using features from C++11) and is tested on
-modern Linux.  It should compile fine on most UNIX systems with a
-C++11 compiler. The README file contains useful information on
-building Yosys and its prerequisites.
-
-Yosys is a large and feature-rich program with some dependencies. For
-this work, we may deactivate other extra features such as {\tt TCL}
-and {\tt ABC} support in the {\tt Makefile}.
-
-\bigskip
-
-This Application Note is based on GIT Rev. {\tt 082550f} from
-2015-04-04 of Yosys~\cite{yosys}.
-
-\section{Quick Start}
-
-We assume that the Verilog design is synthesizable and we also assume
-that the design does not have multi-dimensional memories.  As BTOR
-implicitly initializes registers to zero value and memories stay
-uninitialized, we assume that the Verilog design does
-not contain initial blocks. For more details about the BTOR format,
-please refer to~\cite{btor}.
-
-We provide a shell script {\tt verilog2btor.sh} which can be used to
-convert a Verilog design to BTOR. The script can be found in the
-{\tt backends/btor} directory. The following example shows its usage:
-
-\begin{figure}[H]
-\begin{lstlisting}[language=sh,numbers=none]
-verilog2btor.sh fsm.v fsm.btor test
-\end{lstlisting}
- \renewcommand{\figurename}{Listing}
-\caption{Using verilog2btor script}
-\end{figure}
-
-The script {\tt verilog2btor.sh} takes three parameters.  In the above
-example, the first parameter {\tt fsm.v} is the input design, the second
-parameter {\tt fsm.btor} is the file name of BTOR output, and the third
-parameter {\tt test} is the name of top module in the design.
-
-To specify the properties (that need to be checked), we have two
-options:
-\begin{itemize}
-\item We can use the Verilog {\tt assert} statement in the procedural block
-  or module body of the Verilog design, as shown in
-  Listing~\ref{specifying_property_assert}. This is the preferred option.
-\item We can use a single-bit output wire, whose name starts with
-  {\tt safety}.  The value of this output wire needs to be driven low
-  when the property is met, i.e. the solver will try to find a model
-  that makes the safety pin go high. This is demonstrated in
-  Listing~\ref{specifying_property_output}.
-\end{itemize}
-
-\begin{figure}[H]
-\begin{lstlisting}[language=Verilog,numbers=none]
-module test(input clk, input rst, output y);
-
-  reg [2:0] state;
-
-  always @(posedge clk) begin
-    if (rst || state == 3) begin
-      state <= 0;
-    end else begin
-      assert(state < 3);
-      state <= state + 1;
-    end
-  end
-
-  assign y = state[2];
-
-  assert property (y !== 1'b1);
-
-endmodule
-\end{lstlisting}
-\renewcommand{\figurename}{Listing}
-\caption{Specifying property in Verilog design with {\tt assert}}
-\label{specifying_property_assert}
-\end{figure}
-
-\begin{figure}[H]
-\begin{lstlisting}[language=Verilog,numbers=none]
-module test(input clk, input rst,
-    output y, output safety1);
-
-  reg [2:0] state;
-
-  always @(posedge clk) begin
-    if (rst || state == 3)
-      state <= 0;
-    else
-      state <= state + 1;
-  end
-
-  assign y = state[2];
-
-  assign safety1 = !(y !== 1'b1);
-
-endmodule
-\end{lstlisting}
-\renewcommand{\figurename}{Listing}
-\caption{Specifying property in Verilog design with output wire}
-\label{specifying_property_output}
-\end{figure}
-
-We can run Boolector~\cite{boolector}~$1.4.1$\footnote{
-Newer version of Boolector do not support sequential models.
-Boolector 1.4.1 can be built with picosat-951. Newer versions
-of picosat have an incompatible API.} on the generated BTOR
-file:
-
-\begin{figure}[H]
-\begin{lstlisting}[language=sh,numbers=none]
-$ boolector fsm.btor
-unsat
-\end{lstlisting}
- \renewcommand{\figurename}{Listing}
-\caption{Running boolector on BTOR file}
-\end{figure}
-
-We can also use nuXmv~\cite{nuxmv}, but on BTOR designs it does not
-support memories yet. With the next release of nuXmv, we will be also
-able to verify designs with memories.
-
-\section{Detailed Flow}
-
-Yosys is able to synthesize Verilog designs up to the gate level.
-We are interested in keeping registers and memories when synthesizing
-the design. For this purpose, we describe a customized Yosys synthesis
-flow, that is also provided by the {\tt verilog2btor.sh} script.
-Listing~\ref{btor_script_memory} shows the Yosys commands that are
-executed by {\tt verilog2btor.sh}.
-
-\begin{figure}[H]
-\begin{lstlisting}[language=sh]
-read_verilog -sv $1;
-hierarchy -top $3; hierarchy -libdir $DIR;
-hierarchy -check;
-proc; opt;
-opt_expr -mux_undef; opt;
-rename -hide;;;
-splice; opt;
-memory_dff -wr_only; memory_collect;;
-flatten;;
-memory_unpack;
-splitnets -driver;
-setundef -zero -undriven;
-opt;;;
-write_btor $2;
-\end{lstlisting}
- \renewcommand{\figurename}{Listing}
-\caption{Synthesis Flow for BTOR with memories}
-\label{btor_script_memory}
-\end{figure}
-
-Here is short description of what is happening in the script line by
-line:
-
-\begin{enumerate}
-\item Reading the input file.
-\item Setting the top module in the hierarchy and trying to read
-  automatically the files which are given as {\tt include} in the file
-  read in first line.
-\item Checking the design hierarchy.
-\item Converting processes to multiplexers (muxs) and flip-flops.
-\item Removing undef signals from muxs.
-\item Hiding all signal names that are not used as module ports.
-\item Explicit type conversion, by introducing slice and concat cells
-  in the circuit.
-\item Converting write memories to synchronous memories, and
-  collecting the memories to multi-port memories.
-\item Flattening the design to get only one module.
-\item Separating read and write memories.
-\item Splitting the signals that are partially assigned
-\item Setting undef to zero value.
-\item Final optimization pass.
-\item Writing BTOR file.
-\end{enumerate}
-
-For detailed description of the commands mentioned above, please refer
-to the Yosys documentation, or run {\tt yosys -h \it command\_name}.
-
-The script presented earlier can be easily modified to have a BTOR
-file that does not contain memories. This is done by removing the line
-number~8 and 10, and introduces a new command {\tt memory} at line
-number~8. Listing~\ref{btor_script_without_memory} shows the
-modified Yosys script file:
-
-\begin{figure}[H]
-\begin{lstlisting}[language=sh,numbers=none]
-read_verilog -sv $1;
-hierarchy -top $3; hierarchy -libdir $DIR;
-hierarchy -check;
-proc; opt;
-opt_expr -mux_undef; opt;
-rename -hide;;;
-splice; opt;
-memory;;
-flatten;;
-splitnets -driver;
-setundef -zero -undriven;
-opt;;;
-write_btor $2;
-\end{lstlisting}
- \renewcommand{\figurename}{Listing}
-\caption{Synthesis Flow for BTOR without memories}
-\label{btor_script_without_memory}
-\end{figure}
-
-\section{Example}
-
-Here is an example Verilog design that we want to convert to BTOR:
-
-\begin{figure}[H]
-\begin{lstlisting}[language=Verilog,numbers=none]
-module array(input clk);
-
-  reg [7:0] counter;
-  reg [7:0] mem [7:0];
-
-  always @(posedge clk) begin
-    counter <= counter + 8'd1;
-    mem[counter] <= counter;
-  end
-
-  assert property (!(counter > 8'd0) ||
-    mem[counter - 8'd1] == counter - 8'd1);
-
-endmodule
-\end{lstlisting}
-\renewcommand{\figurename}{Listing}
-\caption{Example - Verilog Design}
-\label{example_verilog}
-\end{figure}
-
-The generated BTOR file that contain memories, using the script shown
-in Listing~\ref{btor_script_memory}:
-\begin{figure}[H]
-\begin{lstlisting}[numbers=none]
-1 var 1 clk
-2 array 8 3
-3 var 8 $auto$rename.cc:150:execute$20
-4 const 8 00000001
-5 sub 8 3 4
-6 slice 3 5 2 0
-7 read 8 2 6
-8 slice 3 3 2 0
-9 add 8 3 4
-10 const 8 00000000
-11 ugt 1 3 10
-12 not 1 11
-13 const 8 11111111
-14 slice 1 13 0 0
-15 one 1
-16 eq 1 1 15
-17 and 1 16 14
-18 write 8 3 2 8 3
-19 acond 8 3 17 18 2
-20 anext 8 3 2 19
-21 eq 1 7 5
-22 or 1 12 21
-23 const 1 1
-24 one 1
-25 eq 1 23 24
-26 cond 1 25 22 24
-27 root 1 -26
-28 cond 8 1 9 3
-29 next 8 3 28
-\end{lstlisting}
-\renewcommand{\figurename}{Listing}
-\caption{Example - Converted BTOR with memory}
-\label{example_btor}
-\end{figure}
-
-And the BTOR file obtained by the script shown in
-Listing~\ref{btor_script_without_memory}, which expands the memory
-into individual elements:
-\begin{figure}[H]
-\begin{lstlisting}[numbers=none,escapechar=@]
-1 var 1 clk
-2 var 8 mem[0]
-3 var 8 $auto$rename.cc:150:execute$20
-4 slice 3 3 2 0
-5 slice 1 4 0 0
-6 not 1 5
-7 slice 1 4 1 1
-8 not 1 7
-9 slice 1 4 2 2
-10 not 1 9
-11 and 1 8 10
-12 and 1 6 11
-13 cond 8 12 3 2
-14 cond 8 1 13 2
-15 next 8 2 14
-16 const 8 00000001
-17 add 8 3 16
-18 const 8 00000000
-19 ugt 1 3 18
-20 not 1 19
-21 var 8 mem[2]
-22 and 1 7 10
-23 and 1 6 22
-24 cond 8 23 3 21
-25 cond 8 1 24 21
-26 next 8 21 25
-27 sub 8 3 16
-
-@\vbox to 0pt{\vss\vdots\vskip3pt}@
-54 cond 1 53 50 52
-55 root 1 -54
-
-@\vbox to 0pt{\vss\vdots\vskip3pt}@
-77 cond 8 76 3 44
-78 cond 8 1 77 44
-79 next 8 44 78
-\end{lstlisting}
-\renewcommand{\figurename}{Listing}
-\caption{Example - Converted BTOR without memory}
-\label{example_btor}
-\end{figure}
-
-\section{Limitations}
-
-BTOR does not support initialization of memories and registers, i.e. they are
-implicitly initialized to value zero, so the initial block for
-memories need to be removed when converting to BTOR. It should
-also be kept in consideration that BTOR does not support the {\tt x} or {\tt z}
-values of Verilog.
-
-Another thing to bear in mind is that Yosys will convert multi-dimensional
-memories to one-dimensional memories and address decoders. Therefore
-out-of-bounds memory accesses can yield unexpected results.
-
-\section{Conclusion}
-
-Using the described flow, we can use Yosys to generate word-level
-verification benchmarks with or without memories from Verilog designs.
-
-\begin{thebibliography}{9}
-
-\bibitem{yosys}
-Claire Xenia Wolf. The Yosys Open SYnthesis Suite. \\
-\url{https://yosyshq.net/yosys/}
-
-\bibitem{boolector}
-Robert Brummayer and Armin Biere, Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays\\
-\url{http://fmv.jku.at/boolector/}
-
-\bibitem{btor}
-Robert Brummayer and Armin Biere and Florian Lonsing, BTOR:
-Bit-Precise Modelling of Word-Level Problems for Model Checking\\
-\url{http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf}
-
-\bibitem{nuxmv}
-Roberto Cavada and Alessandro Cimatti and Michele Dorigatti and
-Alberto Griggio and Alessandro Mariotti and Andrea Micheli and Sergio
-Mover and Marco Roveri and Stefano Tonetta, The nuXmv Symbolic Model
-Checker\\
-\url{https://es-static.fbk.eu/tools/nuxmv/index.php}
-
-\end{thebibliography}
-
-
-\end{document}
diff --git a/manual/appnotes.sh b/manual/appnotes.sh
deleted file mode 100755
index 0ae52862e..000000000
--- a/manual/appnotes.sh
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/bin/bash
-
-set -ex
-for job in APPNOTE_010_Verilog_to_BLIF APPNOTE_011_Design_Investigation APPNOTE_012_Verilog_to_BTOR
-do
-	[ -f $job.ok -a $job.ok -nt $job.tex ] && continue
-	if [ -f $job/make.sh ]; then
-		cd $job
-		bash make.sh
-		cd ..
-	fi
-	old_md5=$([ -f $job.aux ] && md5sum < $job.aux || true)
-	while
-		pdflatex -shell-escape -halt-on-error $job.tex || exit
-		new_md5=$(md5sum < $job.aux)
-		[ "$old_md5" != "$new_md5" ]
-	do
-		old_md5="$new_md5"
-	done
-	touch $job.ok
-done
-