Various documentation updates

13 files changed, 1277 insertions, 108 deletions

diff --git a/CodingReadme b/CodingReadme
index 88f16ff0..03de3fc1 100644
--- a/CodingReadme
+++ b/CodingReadme
@@ -159,6 +159,7 @@ Then with default config setting:
 	cd ~yosys
 	./yosys -p 'proc; show' tests/simple/fiedler-cooley.v
 	./yosys -p 'proc; opt; show' tests/simple/fiedler-cooley.v
+	./yosys -p 'synth; show' tests/simple/fiedler-cooley.v
 
 	cd ~yosys
 	make manual
diff --git a/manual/CHAPTER_Appnotes.tex b/manual/CHAPTER_Appnotes.tex
index 959aabd2..2abfa85d 100644
--- a/manual/CHAPTER_Appnotes.tex
+++ b/manual/CHAPTER_Appnotes.tex
@@ -2,11 +2,24 @@
 \chapter{Application Notes}
 \label{chapter:appnotes}
 
-\begin{fixme}
-This appendix will cover some typical use-cases of Yosys in the form of application notes.
-\end{fixme}
+% \begin{fixme}
+% This appendix will cover some typical use-cases of Yosys in the form of application notes.
+% \end{fixme}
+% 
+% \section{Synthesizing using a Cell Library in Liberty Format}
+% \section{Reverse Engeneering the MOS6502 from an NMOS Transistor Netlist}
+% \section{Reconfigurable Coarse-Grain Synthesis using Intersynth}
 
-\section{Synthesizing using a Cell Library in Liberty Format}
-\section{Reverse Engeneering the MOS6502 from an NMOS Transistor Netlist}
-\section{Reconfigurable Coarse-Grain Synthesis using Intersynth}
+This appendix contains copies of the Yosys application notes.
+
+\begin{itemize}
+\item Yosys AppNote 010: Converting Verilog to BLIF \dotfill Page \pageref{app:010} \hskip2cm\null
+\item Yosys AppNote 011: Interactive Design Investigation \dotfill Page \pageref{app:011} \hskip2cm\null
+\end{itemize}
+
+\eject\label{app:010}
+\includepdf[pages=-,pagecommand=\thispagestyle{plain}]{APPNOTE_010_Verilog_to_BLIF.pdf}
+
+\eject\label{app:011}
+\includepdf[pages=-,pagecommand=\thispagestyle{plain}]{APPNOTE_011_Design_Investigation.pdf}
 
diff --git a/manual/CHAPTER_Auxprogs.tex b/manual/CHAPTER_Auxprogs.tex
index cce3741c..a0089382 100644
--- a/manual/CHAPTER_Auxprogs.tex
+++ b/manual/CHAPTER_Auxprogs.tex
@@ -17,3 +17,9 @@ The {\tt yosys-filterlib} tool is a small utility that can be used to strip
 or extract information from a Liberty file. See Sec.~\ref{sec:techmap_extern}
 for details.
 
+\section{yosys-abc}
+
+This is a unmodified copy of ABC \citeweblink{ABC}. Not all versions of Yosys
+work with all versions of ABC. So Yosys comes with its own yosys-abc to avoid
+compatibility issues between the two.
+
diff --git a/manual/PRESENTATION_ExAdv.tex b/manual/PRESENTATION_ExAdv.tex
index 471516b4..74350091 100644
--- a/manual/PRESENTATION_ExAdv.tex
+++ b/manual/PRESENTATION_ExAdv.tex
@@ -790,7 +790,7 @@ Unwrap in {\tt test2}:
 
 \hfil\begin{tikzpicture}
 \node at (0,0) {\includegraphics[width=11cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2d.pdf}};
-\node at (0,-4) {\includegraphics[width=11cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2e.pdf}};
+\node at (0,-4) {\includegraphics[width=8cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2e.pdf}};
 \node at (1,-1.7) {\begin{lstlisting}[linewidth=5.5cm, frame=single, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys]
 techmap -map macc_xilinx_unwrap_map.v ;;
 \end{lstlisting}};
diff --git a/manual/PRESENTATION_ExOth/axis_master.v b/manual/PRESENTATION_ExOth/axis_master.v
index 25a1feee..fe9008ad 100644
--- a/manual/PRESENTATION_ExOth/axis_master.v
+++ b/manual/PRESENTATION_ExOth/axis_master.v
@@ -13,7 +13,7 @@ module axis_master(aclk, aresetn, tvalid, tready, tdata);
 	    if (tvalid && tready)
 	    	tvalid <= 0;
 	    if (!tvalid || !tready) begin
-	    //             ^- should be not inverted!
+	    //             ^- should not be inverted!
                 state = state ^ state << 13;
                 state = state ^ state >> 7;
                 state = state ^ state << 17;
diff --git a/manual/PRESENTATION_ExSyn.tex b/manual/PRESENTATION_ExSyn.tex
index 80398229..f0dd96e3 100644
--- a/manual/PRESENTATION_ExSyn.tex
+++ b/manual/PRESENTATION_ExSyn.tex
@@ -268,7 +268,7 @@ memory -nomap; techmap -map my_memory_map.v; memory_map
 \end{frame}
 
 \begin{frame}[t, fragile]{\subsecname{} -- Example 1/2}
-\vbox to 0cm{\includegraphics[width=\linewidth,trim=0cm 0cm 0cm -10cm]{PRESENTATION_ExSyn/memory_01.pdf}\vss}
+\vbox to 0cm{\includegraphics[width=\linewidth,trim=0cm 0cm 0cm -6cm]{PRESENTATION_ExSyn/memory_01.pdf}\vss}
 \vskip-1cm
 \begin{columns}
 \column[t]{5cm}
@@ -455,7 +455,7 @@ read_verilog -D WITH_MULT cpu_alu.v
 hierarchy -check -top cpu_top
 
 # high-level synthesis
-proc; opt; memory -nomap;; fsm; opt
+proc; opt; fsm;; memory -nomap; opt
 
 # substitute block rams
 techmap -map map_rams.v
@@ -497,7 +497,7 @@ the next part (Section 3, ``Advanced Synthesis'') of this presentation.}
 \item Yosys provides commands for each phase of the synthesis.
 \item Each command solves a (more or less) simple problem.
 \item Complex commands are often only front-ends to simple commands.
-\item {\tt proc; opt; memory; opt; fsm; opt; techmap; opt; abc;;}
+\item {\tt proc; opt; fsm; opt; memory; opt; techmap; opt; abc;;}
 \end{itemize}
 
 \bigskip
diff --git a/manual/PRESENTATION_Intro.tex b/manual/PRESENTATION_Intro.tex
index 7697266d..ed600a3e 100644
--- a/manual/PRESENTATION_Intro.tex
+++ b/manual/PRESENTATION_Intro.tex
@@ -277,7 +277,7 @@ Direct link to the files: \\ \footnotesize
 
 \medskip
 {\color{YosysGreen}\# the high-level stuff}\\
-\boxalert<3>{proc}; \boxalert<4>{opt}; \boxalert<5>{memory}; \boxalert<6>{opt}; \boxalert<7>{fsm}; \boxalert<8>{opt}
+\boxalert<3>{proc}; \boxalert<4>{opt}; \boxalert<5>{fsm}; \boxalert<6>{opt}; \boxalert<7>{memory}; \boxalert<8>{opt}
 
 \medskip
 {\color{YosysGreen}\# mapping to internal cell library}\\
@@ -308,9 +308,9 @@ Direct link to the files: \\ \footnotesize
 \only<2>{hierarchy -check -top counter}%
 \only<3>{proc}%
 \only<4>{opt}%
-\only<5>{memory}%
+\only<5>{fsm}%
 \only<6>{opt}%
-\only<7>{fsm}%
+\only<7>{memory}%
 \only<8>{opt}%
 \only<9>{techmap}%
 \only<10>{opt}%
@@ -333,13 +333,13 @@ Direct link to the files: \\ \footnotesize
 	Perform some basic optimizations and cleanups.
 }%
 \only<5>{
-	Analyze memories and create circuits to implement them.
+	Analyze and optimize finite state machines.
 }%
 \only<6>{
 	Perform some basic optimizations and cleanups.
 }%
 \only<7>{
-	Analyze and optimize finite state machines.
+	Analyze memories and create circuits to implement them.
 }%
 \only<8>{
 	Perform some basic optimizations and cleanups.
@@ -398,7 +398,7 @@ hierarchy -check -top counter
 
 \begin{frame}[t, fragile]{\subsecname{} -- Step 2/4}
 \begin{verbatim}
-proc; opt; memory; opt; fsm; opt
+proc; opt; fsm; opt; memory; opt
 \end{verbatim}
 
 \vfill
@@ -427,6 +427,48 @@ clean
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\subsection{The synth command}
+
+\begin{frame}[fragile]{\subsecname{}}
+Yosys contains a default (recommended example) synthesis script in form of the
+{\tt synth} command. The following commands are executed by this synthesis command:
+
+\begin{columns}
+\column[t]{5cm}
+\begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys]
+begin:
+    hierarchy -check [-top <top>]
+
+coarse:
+    proc
+    opt
+    wreduce
+    alumacc
+    share
+    opt
+    fsm
+    opt -fast
+    memory -nomap
+    opt_clean
+\end{lstlisting}
+\column[t]{5cm}
+\begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys]
+fine:
+    opt -fast -full
+    memory_map
+    opt -full
+    techmap
+    opt -fast
+
+abc:
+    abc -fast
+    opt -fast
+\end{lstlisting}
+\end{columns}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \subsection{Yosys Commands}
 
 \begin{frame}[fragile]{\subsecname{} 1/3 \hspace{0pt plus 1 filll} (excerpt)}
@@ -500,6 +542,7 @@ Commands for writing the results:
 \bigskip
 Script-Commands for standard synthesis tasks:
 \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys]
+    synth                # generic synthesis script
     synth_xilinx         # synthesis for Xilinx FPGAs
 \end{lstlisting}
 
@@ -603,12 +646,8 @@ endmodule
 
 \begin{frame}{\subsecname}
 \begin{itemize}
-\item Multi-dimensional arrays (memories)
-\item Writing to arrays using bit- and part-selects (todo for 0.4.0)
-\item The wor/wand wire types (maybe for 0.4.0)
 \item Tri-state logic
-
-\bigskip
+\item The wor/wand wire types (maybe for 0.5)
 \item Latched logic (is synthesized as logic with feedback loops)
 \item Some non-synthesizable features that should be ignored in synthesis are not supported by the parser and cause a parser error (file a bug report if you encounter this problem)
 \end{itemize}
@@ -813,10 +852,12 @@ control logic because it is simpler than setting up a commercial flow.
 \item When building on other Linux distributions:
 \begin{itemize}
 \item Needs compiler with some C++11 support
+\item See README file for build instructions
 \item Post to the subreddit if you get stuck
 \end{itemize}
 \item Ported to OS X (Darwin) and OpenBSD
-\item No win32 support (yet)
+\item Native win32 build with VisualStudio
+\item Cross win32 build with MXE
 \end{itemize}
 \end{frame}
 
diff --git a/manual/PRESENTATION_Prog.tex b/manual/PRESENTATION_Prog.tex
index 590451be..d4002458 100644
--- a/manual/PRESENTATION_Prog.tex
+++ b/manual/PRESENTATION_Prog.tex
@@ -89,12 +89,13 @@ left with a much simpler version of RTLIL:
 \bigskip
 Many commands simply choose to only work on this simpler version:
 \begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont]
-if (module->processes.size() != 0 || module->memories.size() != 0)
-    log_error("This command does not operate on modules with processes "
-              "and/or memories! Run 'proc' and 'memory' first.\n");
+for (RTLIL::Module *module : design->selected_modules() {
+    if (module->has_memories_warn() || module->has_processes_warn())
+        continue;
+    ....
+}
 \end{lstlisting}
 
-\bigskip
 For simplicity we only discuss this version of RTLIL in this presentation.
 \end{frame}
 
@@ -145,7 +146,9 @@ See {\tt yosys/kernel/rtlil.h} for details.
 \subsubsection{RTLIL::IdString}
 
 \begin{frame}{\subsubsecname}{}
-{\tt RTLIL::IdString} is a simple wrapper for {\tt std::string}. It is used for names of RTLIL objects.
+{\tt RTLIL::IdString} in many ways behave like a {\tt std::string}. It is used
+for names of RTLIL objects. Internally a RTLIL::IdString object is only a
+single integer.
 
 \medskip
 The first character of a {\tt RTLIL::IdString} specifies if the name is {\it public\/} or {\it private\/}:
@@ -168,25 +171,25 @@ Use the {\tt NEW\_ID} macro to create a new unique private name.
 
 \begin{frame}[t, fragile]{\subsubsecname}
 The {\tt RTLIL::Design} and {\tt RTLIL::Module} structs are the top-level RTLIL
-data structures.
-
-Yosys always operates on one active design, but can hold many designs in memory.
+data structures. Yosys always operates on one active design, but can hold many designs in memory.
 
 \bigskip
 \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++]
 struct RTLIL::Design {
-    std::map<RTLIL::IdString, RTLIL::Module*> modules;
+    std::map<RTLIL::IdString, RTLIL::Module*> modules_;
     ...
 };
 
 struct RTLIL::Module {
     RTLIL::IdString name;
-    std::map<RTLIL::IdString, RTLIL::Wire*> wires;
-    std::map<RTLIL::IdString, RTLIL::Cell*> cells;
-    std::vector<RTLIL::SigSig> connections;
+    std::map<RTLIL::IdString, RTLIL::Wire*> wires_;
+    std::map<RTLIL::IdString, RTLIL::Cell*> cells_;
+    std::vector<RTLIL::SigSig> connections_;
     ...
 };
 \end{lstlisting}
+
+(Use the various accessor functions instead of directly working with the {\tt *\_} members.)
 \end{frame}
 
 \subsubsection{The RTLIL::Wire Structure}
@@ -251,21 +254,22 @@ constants are part of the RTLIL representation itself.
 
 \begin{frame}[t, fragile]{\subsubsecname}
 The {\tt RTLIL::SigSpec} struct represents a signal vector. Each bit can either be a bit from a wire
-or a constant value. Consecutive bits from a wire or consecutive constant bits are consolidated into
-a {\tt RTLIL::SigChunk}:
+or a constant value.
 
 \bigskip
 \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++]
-struct RTLIL::SigChunk {
+struct RTLIL::SigBit
+{
     RTLIL::Wire *wire;
-    RTLIL::Const data; // only used if wire == NULL
-    int width, offset;
+    union {
+        RTLIL::State data; // used if wire == NULL
+        int offset;        // used if wire != NULL
+    };
     ...
 };
 
 struct RTLIL::SigSpec {
-    std::vector<RTLIL::SigChunk> chunks; // LSB at index 0
-    int width;
+    std::vector<RTLIL::SigBit> bits_; // LSB at index 0
     ...
 };
 \end{lstlisting}
@@ -289,7 +293,7 @@ instances:
 \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++]
 struct RTLIL::Cell {
     RTLIL::IdString name, type;
-    std::map<RTLIL::IdString, RTLIL::SigSpec> connections;
+    std::map<RTLIL::IdString, RTLIL::SigSpec> connections_;
     std::map<RTLIL::IdString, RTLIL::Const> parameters;
     ...
 };
@@ -345,7 +349,7 @@ typedef std::pair<RTLIL::SigSpec, RTLIL::SigSpec> RTLIL::SigSig;
 
 struct RTLIL::Module {
     ...
-    std::vector<RTLIL::SigSig> connections;
+    std::vector<RTLIL::SigSig> connections_;
     ...
 };
 \end{lstlisting}
@@ -354,8 +358,8 @@ struct RTLIL::Module {
 {\tt RTLIL::SigSig::first} is the driven signal and {\tt RTLIL::SigSig::second} is the driving signal.
 Example usage (setting wire {\tt foo} to value {\tt 42}):
 \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++]
-module->connections.push_back(RTLIL::SigSig(module->wires.at("\\foo"),
-        RTLIL::SigSpec(42, module->wires.at("\\foo")->width)));
+module->connect(module->wire("\\foo"),
+                RTLIL::SigSpec(42, module->wire("\\foo")->width));
 \end{lstlisting}
 \end{frame}
 
@@ -378,17 +382,19 @@ endmodule
 RTLIL::Module *module = new RTLIL::Module;
 module->name = "\\absval";
 
-RTLIL::Wire *a = module->new_wire(4, "\\a");
+RTLIL::Wire *a = module->addWire("\\a", 4);
 a->port_input = true;
 a->port_id = 1;
 
-RTLIL::Wire *y = module->new_wire(4, "\\y");
+RTLIL::Wire *y = module->addWire("\\y", 4);
 y->port_output = true;
 y->port_id = 2;
 
-RTLIL::Wire *a_inv = module->new_wire(4, NEW_ID);
+RTLIL::Wire *a_inv = module->addWire(NEW_ID, 4);
 module->addNeg(NEW_ID, a, a_inv, true);
 module->addMux(NEW_ID, a, a_inv, RTLIL::SigSpec(a, 1, 3), y);
+
+module->fixup_ports();
 \end{lstlisting}
 \end{frame}
 
@@ -431,8 +437,8 @@ In this case {\tt a}, {\tt x}, and {\tt y} are all different names for the same
 
 \smallskip
 \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++]
-RTLIL::SigSpec a(module->wires.at("\\a")), x(module->wires.at("\\x")),
-                                           y(module->wires.at("\\y"));
+RTLIL::SigSpec a(module->wire("\\a")), x(module->wire("\\x")),
+                                       y(module->wire("\\y"));
 log("%d %d %d\n", a == x, x == y, y == a); // will print "0 0 0"
 \end{lstlisting}
 
@@ -462,9 +468,9 @@ log("Mapped signal x: %s\n", log_signal(sigmap(x)));
 \end{lstlisting}
 
 \medskip
-Use {\tt RTLIL::id2cstr()} to create a C-string for an {\tt RTLIL::IdString}:
+Use {\tt log\_id()} to create a C-string for an {\tt RTLIL::IdString}:
 \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++]
-log("Name of this module: %s\n", RTLIL::id2cstr(module->name));
+log("Name of this module: %s\n", log_id(module->name));
 \end{lstlisting}
 
 \medskip
@@ -513,9 +519,8 @@ a new yosys command:
 
 \bigskip
 \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++]
-#include "kernel/rtlil.h"
-#include "kernel/register.h"
-#include "kernel/log.h"
+#include "kernel/yosys.h"
+USING_YOSYS_NAMESPACE
 
 struct MyPass : public Pass {
     MyPass() : Pass("my_cmd", "just a simple test") { }
@@ -526,9 +531,9 @@ struct MyPass : public Pass {
             log("  %s\n", arg.c_str());
 
         log("Modules in current design:\n");
-        for (auto &mod : design->modules)
-            log("  %s (%zd wires, %zd cells)\n", RTLIL::id2cstr(mod.first),
-                    mod.second->wires.size(), mod.second->cells.size());
+        for (auto mod : design->modules())
+            log("  %s (%d wires, %d cells)\n", log_id(mod),
+                    GetSize(mod->wires), GetSize(mod->cells));
     }
 } MyPass;
 \end{lstlisting}
@@ -566,7 +571,7 @@ yosys -m ./my_cmd.so -p 'my_cmd foo bar'
 \item \dots and even simpler if you don't need RTLIL::Memory or RTLIL::Process objects.
 
 \bigskip
-\item Writing synthesis software? Consider learning the Yosys API and make your stuff
+\item Writing synthesis software? Consider learning the Yosys API and make your work
 part of the Yosys framework.
 \end{itemize}
 
diff --git a/manual/PRESENTATION_Prog/my_cmd.cc b/manual/PRESENTATION_Prog/my_cmd.cc
index 3e3cf13a..1d28ce97 100644
--- a/manual/PRESENTATION_Prog/my_cmd.cc
+++ b/manual/PRESENTATION_Prog/my_cmd.cc
@@ -1,6 +1,9 @@
 #include "kernel/yosys.h"
 #include "kernel/sigtools.h"
 
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
 struct MyPass : public Pass {
     MyPass() : Pass("my_cmd", "just a simple test") { }
     virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
@@ -25,6 +28,7 @@ struct Test1Pass : public Pass {
             log_error("A module with the name absval already exists!\n");
 
         RTLIL::Module *module = design->addModule("\\absval");
+        log("Name of this module: %s\n", log_id(module));
 
         RTLIL::Wire *a = module->addWire("\\a", 4);
         a->port_input = true;
@@ -38,7 +42,7 @@ struct Test1Pass : public Pass {
         module->addNeg(NEW_ID, a, a_inv, true);
         module->addMux(NEW_ID, a, a_inv, RTLIL::SigSpec(a, 3), y);
 
-        log("Name of this module: %s\n", log_id(module));
+	module->fixup_ports();
     }
 } Test1Pass;
 
@@ -69,3 +73,4 @@ struct Test2Pass : public Pass {
     }
 } Test2Pass;
 
+PRIVATE_NAMESPACE_END
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex
index 35249ed8..697add15 100644
--- a/manual/command-reference-manual.tex
+++ b/manual/command-reference-manual.tex
@@ -15,22 +15,88 @@ library to a target architecture.
     -script <file>
         use the specified ABC script file instead of the default script.
 
+        if <file> starts with a plus sign (+), then the rest of the filename
+        string is interprated as the command string to be passed to ABC. the
+        leading plus sign is removed and all commas (,) in the string are
+        replaced with blanks before the string is passed to ABC.
+
+        if no -script parameter is given, the following scripts are used:
+
+        for -liberty without -constr:
+          strash; scorr -v; ifraig -v; retime -v {D}; strash; dch -vf;
+               map -v {D}
+
+        for -liberty with -constr:
+          strash; scorr -v; ifraig -v; retime -v {D}; strash; dch -vf;
+               map -v {D}; buffer -v; upsize -v {D}; dnsize -v {D};
+               stime -p
+
+        for -lut:
+          strash; scorr -v; ifraig -v; retime -v; strash; dch -vf; if -v
+
+        otherwise:
+          strash; scorr -v; ifraig -v; retime -v; strash; dch -vf; map -v
+
+    -fast
+        use different default scripts that are slightly faster (at the cost
+        of output quality):
+
+        for -liberty without -constr:
+          retime -v {D}; map -v {D}
+
+        for -liberty with -constr:
+          retime -v {D}; map -v {D}; buffer -v; upsize -v {D};
+               dnsize -v {D}; stime -p
+
+        for -lut:
+          retime -v; if -v
+
+        otherwise:
+          retime -v; map -v
+
     -liberty <file>
         generate netlists for the specified cell library (using the liberty
-        file format). Without this option, ABC is used to optimize the netlist
-        but keeps using yosys's internal gate library. This option is ignored if
-        the -script option is also used.
+        file format).
 
     -constr <file>
-        pass this file with timing constraints to ABC
+        pass this file with timing constraints to ABC. use with -liberty.
+
+        a constr file contains two lines:
+            set_driving_cell <cell_name>
+            set_load <floating_point_number>
+
+        the set_driving_cell statement defines which cell type is assumed to
+        drive the primary inputs and the set_load statement sets the load in
+        femtofarads for each primary output.
+
+    -D <picoseconds>
+        set delay target. the string {D} in the default scripts above is
+        replaced by this option when used, and an empty string otherwise.
 
     -lut <width>
         generate netlist using luts of (max) the specified width.
 
+    -dff
+        also pass $_DFF_?_ cells through ABC (only one clock domain, if many
+        clock domains are present in a module, the one with the largest number
+        of $_DFF_?_ cells in it is used)
+
+    -clk [!]<signal-name>
+        use the specified clock domain. (when this option is used in combination
+        with -dff, then it falls back to the automatic dection of clock domain
+        if the specified clock is not found in a module.)
+
+    -keepff
+        set the "keep" attribute on flip-flop output wires. (and thus preserve
+        them, for example for equivialence checking.)
+
     -nocleanup
         when this option is used, the temporary files created by this pass
         are not removed. this is useful for debugging.
 
+When neither -liberty nor -lut is used, the Yosys standard cell library is
+loaded into ABC before the ABC script is executed.
+
 This pass does not operate on modules with unprocessed processes in it.
 (I.e. the 'proc' pass should be used first to convert processes to netlists.)
 
@@ -59,6 +125,15 @@ Like 'add -input', but also connect the signal between instances of the
 selected modules.
 \end{lstlisting}
 
+\section{alumacc -- extract ALU and MACC cells}
+\label{cmd:alumacc}
+\begin{lstlisting}[numbers=left,frame=single]
+    alumacc [selection]
+
+This pass translates arithmetic operations $add, $mul, $lt, etc. to $alu and
+$macc cells.
+\end{lstlisting}
+
 \section{cd -- a shortcut for 'select -module <name>'}
 \label{cmd:cd}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -92,6 +167,129 @@ When commands are separated using the ';;;' token, this command will be executed
 in -purge mode between the commands.
 \end{lstlisting}
 
+\section{connect -- create or remove connections}
+\label{cmd:connect}
+\begin{lstlisting}[numbers=left,frame=single]
+    connect [-nomap] [-nounset] -set <lhs-expr> <rhs-expr>
+
+Create a connection. This is equivialent to adding the statement 'assign
+<lhs-expr> = <rhs-expr>;' to the verilog input. Per default, all existing
+drivers for <lhs-expr> are unconnected. This can be overwritten by using
+the -nounset option.
+
+
+    connect [-nomap] -unset <expr>
+
+Unconnect all existing drivers for the specified expression.
+
+
+    connect [-nomap] -port <cell> <port> <expr>
+
+Connect the specified cell port to the specified cell port.
+
+
+Per default signal alias names are resolved and all signal names are mapped
+the the signal name of the primary driver. Using the -nomap option deactivates
+this behavior.
+
+The connect command operates in one module only. Either only one module must
+be selected or an active module must be set using the 'cd' command.
+
+This command does not operate on module with processes.
+\end{lstlisting}
+
+\section{connwrappers -- replace undef values with defined constants}
+\label{cmd:connwrappers}
+\begin{lstlisting}[numbers=left,frame=single]
+    connwrappers [options] [selection]
+
+Wrappers are used in coarse-grain synthesis to wrap cells with smaller ports
+in wrapper cells with a (larger) constant port size. I.e. the upper bits
+of the wrapper outut are signed/unsigned bit extended. This command uses this
+knowlege to rewire the inputs of the driven cells to match the output of
+the driving cell.
+
+    -signed <cell_type> <port_name> <width_param>
+    -unsigned <cell_type> <port_name> <width_param>
+        consider the specified signed/unsigned wrapper output
+
+    -port <cell_type> <port_name> <width_param> <sign_param>
+        use the specified parameter to decide if signed or unsigned
+
+The options -signed, -unsigned, and -port can be specified multiple times.
+\end{lstlisting}
+
+\section{copy -- copy modules in the design}
+\label{cmd:copy}
+\begin{lstlisting}[numbers=left,frame=single]
+    copy old_name new_name
+
+Copy the specified module. Note that selection patterns are not supported
+by this command.
+\end{lstlisting}
+
+\section{cover -- print code coverage counters}
+\label{cmd:cover}
+\begin{lstlisting}[numbers=left,frame=single]
+    cover [options] [pattern]
+
+Print the code coverage counters collected using the cover() macro in the Yosys
+C++ code. This is useful to figure out what parts of Yosys are utilized by a
+test bench.
+
+    -q
+        Do not print output to the normal destination (console and/or log file)
+
+    -o file
+        Write output to this file, truncate if exists.
+
+    -a file
+        Write output to this file, append if exists.
+
+    -d dir
+        Write output to a newly created file in the specified directory.
+
+When one or more pattern (shell wildcards) are specified, then only counters
+matching at least one pattern are printed.
+
+
+It is also possible to instruct Yosys to print the coverage counters on program
+exit to a file using environment variables:
+
+    YOSYS_COVER_DIR="{dir-name}" yosys {args}
+
+        This will create a file (with an auto-generated name) in this
+        directory and write the coverage counters to it.
+
+    YOSYS_COVER_FILE="{file-name}" yosys {args}
+
+        This will append the coverage counters to the specified file.
+
+
+Hint: Use the following AWK command to consolidate Yosys coverage files:
+
+    gawk '{ p[$3] = $1; c[$3] += $2; } END { for (i in p)
+      printf "%-60s %10d %s\n", p[i], c[i], i; }' {files} | sort -k3
+
+
+Coverage counters are only available in debug builds of Yosys for Linux.
+\end{lstlisting}
+
+\section{delete -- delete objects in the design}
+\label{cmd:delete}
+\begin{lstlisting}[numbers=left,frame=single]
+    delete [selection]
+
+Deletes the selected objects. This will also remove entire modules, if the
+whole module is selected.
+
+
+    delete {-input|-output|-port} [selection]
+
+Does not delete any object but removes the input and/or output flag on the
+selected wires, thus 'deleting' module ports.
+\end{lstlisting}
+
 \section{design -- save, restore and reset current design}
 \label{cmd:design}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -105,10 +303,36 @@ Clear the current design.
 Save the current design under the given name.
 
 
+    design -stash <name>
+
+Save the current design under the given name and then clear the current design.
+
+
+    design -push
+
+Push the current design to the stack and then clear the current design.
+
+
+    design -pop
+
+Reset the current design and pop the last design from the stack.
+
+
     design -load <name>
 
 Reset the current design and load the design previously saved under the given
 name.
+
+
+    design -copy-from <name> [-as <new_mod_name>] <selection>
+
+Copy modules from the specified design into the current one. The selection is
+evaluated in the other design.
+
+
+    design -copy-to <name> [-as <new_mod_name>] [selection]
+
+Copy modules from the current design into the soecified one.
 \end{lstlisting}
 
 \section{dfflibmap -- technology mapping of flip-flops}
@@ -139,7 +363,23 @@ ilang format.
         only dump the module headers if the entire module is selected
 
     -outfile <filename>
-        Write to the specified file.
+        write to the specified file.
+
+    -append <filename>
+        like -outfile but append instead of overwrite
+\end{lstlisting}
+
+\section{echo -- turning echoing back of commands on and off}
+\label{cmd:echo}
+\begin{lstlisting}[numbers=left,frame=single]
+    echo on
+
+Print all commands to log before executing them.
+
+
+    echo off
+
+Do not print all commands to log before executing them. (default)
 \end{lstlisting}
 
 \section{eval -- evaluate the circuit given an input}
@@ -164,6 +404,38 @@ inputs.
         then all output ports of the current module are used.
 \end{lstlisting}
 
+\section{expose -- convert internal signals to module ports}
+\label{cmd:expose}
+\begin{lstlisting}[numbers=left,frame=single]
+    expose [options] [selection]
+
+This command exposes all selected internal signals of a module as additional
+outputs.
+
+    -dff
+        only consider wires that are directly driven by register cell.
+
+    -cut
+        when exposing a wire, create an input/output pair and cut the internal
+        signal path at that wire.
+
+    -shared
+        only expose those signals that are shared ammong the selected modules.
+        this is useful for preparing modules for equivialence checking.
+
+    -evert
+        also turn connections to instances of other modules to additional
+        inputs and outputs and remove the module instances.
+
+    -evert-dff
+        turn flip-flops to sets of inputs and outputs.
+
+    -sep <separator>
+        when creating new wire/port names, the original object name is suffixed
+        with this separator (default: '.') and the port name or a type
+        designator for the exposed signal.
+\end{lstlisting}
+
 \section{extract -- find subcircuits and replace them with cells}
 \label{cmd:extract}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -175,7 +447,12 @@ in the given map file and replaces them with instances of this modules. The
 map file can be a verilog source file (*.v) or an ilang file (*.il).
 
     -map <map_file>
-        use the modules in this file as reference
+        use the modules in this file as reference. This option can be used
+        multiple times.
+
+    -map %<design-name>
+        use the modules in this in-memory design as reference. This option can
+        be used multiple times.
 
     -verbose
         print debug output while analyzing
@@ -209,6 +486,12 @@ map file can be a verilog source file (*.v) or an ilang file (*.il).
     -wire_attr <attribute_name>
         Attributes on wires with the given name must match.
 
+    -ignore_parameters
+        Do not use parameters when matching cells.
+
+    -ignore_param <cell_type> <parameter_name>
+        Do not use this parameter when matching cells.
+
 This pass does not operate on modules with uprocessed processes in it.
 (I.e. the 'proc' pass should be used first to convert processes to netlists.)
 
@@ -257,11 +540,27 @@ pass is using the current design as mapping library.
 
 This pass performs functional reduction in the circuit. I.e. if two nodes are
 equivialent, they are merged to one node and one of the redundant drivers is
-removed.
+disconnected. A subsequent call to 'clean' will remove the redundant drivers.
+
+    -v, -vv
+        enable verbose or very verbose output
+
+    -inv
+        enable explicit handling of inverted signals
+
+    -stop <n>
+        stop after <n> reduction operations. this is mostly used for
+        debugging the freduce command itself.
 
-    -try
-        do not issue an error when the analysis fails.
-        (usually beacause of logic loops in the design)
+    -dump <prefix>
+        dump the design to <prefix>_<module>_<num>.il after each reduction
+        operation. this is mostly used for debugging the freduce command.
+
+This pass is undef-aware, i.e. it considers don't-care values for detecting
+equivialent nodes.
+
+All selected wires are considered for rewiring. The selected cells cover the
+circuit that is analyzed.
 \end{lstlisting}
 
 \section{fsm -- extract and optimize finite state machines}
@@ -428,10 +727,24 @@ needed.
         also check the design hierarchy. this generates an error when
         an unknown module is used as cell type.
 
+    -purge_lib
+        by default the hierarchy command will not remove library (blackbox)
+        module. use this options to also remove unused blackbox modules.
+
+    -libdir <directory>
+        search for files named <module_name>.v in the specified directory
+        for unknown modules and automatically run read_verilog for each
+        unknown module.
+
     -keep_positionals
         per default this pass also converts positional arguments in cells
         to arguments using port names. this option disables this behavior.
 
+    -nokeep_asserts
+        per default this pass sets the "keep" attribute on all modules
+        that directly or indirectly contain one or more $assert cells. this
+        option disables this behavior.
+
     -top <module>
         use the specified top module to built a design hierarchy. modules
         outside this tree (unused modules) are removed.
@@ -457,6 +770,25 @@ This pass ignores the current selection and always operates on all modules
 in the current design.
 \end{lstlisting}
 
+\section{hilomap -- technology mapping of constant hi- and/or lo-drivers}
+\label{cmd:hilomap}
+\begin{lstlisting}[numbers=left,frame=single]
+    hilomap [options] [selection]
+
+Map constants to 'tielo' and 'tiehi' driver cells.
+
+    -hicell <celltype> <portname>
+        Replace constant hi bits with this cell.
+
+    -locell <celltype> <portname>
+        Replace constant lo bits with this cell.
+
+    -singleton
+        Create only one hi/lo cell and connect all constant bits
+        to that cell. Per default a separate cell is created for
+        each constant bit.
+\end{lstlisting}
+
 \section{history -- show last interactive commands}
 \label{cmd:history}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -491,6 +823,35 @@ the resulting cells to more sophisticated PAD cells.
 
     -nameparam <param_name>
         Use the specified parameter to set the port name.
+
+    -bits
+        create individual bit-wide buffers even for ports that
+        are wider. (the default behavio is to create word-wide
+        buffers use -widthparam to set the word size on the cell.)
+\end{lstlisting}
+
+\section{log -- print text and log files}
+\label{cmd:log}
+\begin{lstlisting}[numbers=left,frame=single]
+    log string
+
+Print the given string to the screen and/or the log file. This is useful for TCL
+scripts, because the TCL command "puts" only goes to stdout but not to
+logfiles.
+
+    -stdout
+        Print the output to stdout too. This is useful when all Yosys is executed
+        with a script and the -q (quiet operation) argument to notify the user.
+
+    -stderr
+        Print the output to stderr too.
+
+    -nolog
+        Don't use the internal log() command. Use either -stdout or -stderr,
+        otherwise no output will be generated at all.
+
+    -n
+        do not append a newline
 \end{lstlisting}
 
 \section{ls -- list modules or objects in modules}
@@ -509,6 +870,15 @@ on the whole design or whole active module. Use 'select -list' to show a list
 of currently selected objects.
 \end{lstlisting}
 
+\section{maccmap -- mapping macc cells}
+\label{cmd:maccmap}
+\begin{lstlisting}[numbers=left,frame=single]
+    maccmap [-unmap] [selection]
+
+This pass maps $macc cells to yosys gate primitives. When the -unmap option is
+used then the $macc cell is mapped to $and, $sub, etc. cells instead.
+\end{lstlisting}
+
 \section{memory -- translate memories to basic cells}
 \label{cmd:memory}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -517,6 +887,9 @@ of currently selected objects.
 This pass calls all the other memory_* passes in a useful order:
 
     memory_dff
+    opt_clean
+    memory_share
+    opt_clean
     memory_collect
     memory_map          (skipped if called with -nomap)
 
@@ -536,11 +909,14 @@ memory cells.
 \section{memory\_dff -- merge input/output DFFs into memories}
 \label{cmd:memory_dff}
 \begin{lstlisting}[numbers=left,frame=single]
-    memory_dff [selection]
+    memory_dff [options] [selection]
 
 This pass detects DFFs at memory ports and merges them into the memory port.
 I.e. it consumes an asynchronous memory port and the flip-flops at its
 interface and yields a synchronous memory port.
+
+    -wr_only
+        do not merge registers on read ports
 \end{lstlisting}
 
 \section{memory\_map -- translate multiport memories to basic cells}
@@ -552,26 +928,101 @@ This pass converts multiport memory cells as generated by the memory_collect
 pass to word-wide DFFs and address decoders.
 \end{lstlisting}
 
+\section{memory\_share -- consolidate memory ports}
+\label{cmd:memory_share}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_share [selection]
+
+This pass merges share-able memory ports into single memory ports.
+
+The following methods are used to consolidate the number of memory ports:
+
+  - When write ports are connected to async read ports accessing the same
+    address, then this feedback path is converted to a write port with
+    byte/part enable signals.
+
+  - When multiple write ports access the same address then this is converted
+    to a single write port with a more complex data and/or enable logic path.
+
+  - When multiple write ports are never accessed at the same time (a SAT
+    solver is used to determine this), then the ports are merged into a single
+    write port.
+
+Note that in addition to the algorithms implemented in this pass, the $memrd
+and $memwr cells are also subject to generic resource sharing passes (and other
+optimizations) such as opt_share.
+\end{lstlisting}
+
+\section{memory\_unpack -- unpack multi-port memory cells}
+\label{cmd:memory_unpack}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_unpack [selection]
+
+This pass converts the multi-port $mem memory cells into individual $memrd and
+$memwr cells. It is the counterpart to the memory_collect pass.
+\end{lstlisting}
+
+\section{miter -- automatically create a miter circuit}
+\label{cmd:miter}
+\begin{lstlisting}[numbers=left,frame=single]
+    miter -equiv [options] gold_name gate_name miter_name
+
+Creates a miter circuit for equivialence checking. The gold- and gate- modules
+must have the same interfaces. The miter circuit will have all inputs of the
+two source modules, prefixed with 'in_'. The miter circuit has a 'trigger'
+output that goes high if an output mismatch between the two source modules is
+detected.
+
+    -ignore_gold_x
+        a undef (x) bit in the gold module output will match any value in
+        the gate module output.
+
+    -make_outputs
+        also route the gold- and gate-outputs to 'gold_*' and 'gate_*' outputs
+        on the miter circuit.
+
+    -make_outcmp
+        also create a cmp_* output for each gold/gate output pair.
+
+    -make_assert
+        also create an 'assert' cell that checks if trigger is always low.
+
+    -flatten
+        call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit.
+\end{lstlisting}
+
 \section{opt -- perform simple optimizations}
 \label{cmd:opt}
 \begin{lstlisting}[numbers=left,frame=single]
-    opt [selection]
+    opt [options] [selection]
 
 This pass calls all the other opt_* passes in a useful order. This performs
 a series of trivial optimizations and cleanups. This pass executes the other
 passes in the following order:
 
-    opt_const
+    opt_const [-mux_undef] [-mux_bool] [-undriven] [-fine] [-full] [-keepdc]
     opt_share -nomux
 
     do
         opt_muxtree
-        opt_reduce
+        opt_reduce [-fine] [-full]
         opt_share
         opt_rmdff
-        opt_clean
-        opt_const
-    while [changed design]
+        opt_clean [-purge]
+        opt_const [-mux_undef] [-mux_bool] [-undriven] [-fine] [-full] [-keepdc]
+    while <changed design>
+
+When called with -fast the following script is used instead:
+
+    do
+        opt_const [-mux_undef] [-mux_bool] [-undriven] [-fine] [-full] [-keepdc]
+        opt_share
+        opt_rmdff
+        opt_clean [-purge]
+    while <changed design in opt_rmdff>
+
+Note: Options in square brackets (such as [-keepdc]) are passed through to
+the opt_* commands when given to 'opt'.
 \end{lstlisting}
 
 \section{opt\_clean -- remove unused cells and wires}
@@ -593,9 +1044,30 @@ This pass only operates on completely selected modules without processes.
 \section{opt\_const -- perform const folding}
 \label{cmd:opt_const}
 \begin{lstlisting}[numbers=left,frame=single]
-    opt_const [selection]
+    opt_const [options] [selection]
 
 This pass performs const folding on internal cell types with constant inputs.
+
+    -mux_undef
+        remove 'undef' inputs from $mux, $pmux and $_MUX_ cells
+
+    -mux_bool
+        replace $mux cells with inverters or buffers when possible
+
+    -undriven
+        replace undriven nets with undef (x) constants
+
+    -fine
+        perform fine-grain optimizations
+
+    -full
+        alias for -mux_undef -mux_bool -undriven -fine
+
+    -keepdc
+        some optimizations change the behavior of the circuit with respect to
+        don't-care bits. for example in 'a+0' a single x-bit in 'a' will cause
+        all result bits to be set to x. this behavior changes when 'a+0' is
+        replaced by 'a'. the -keepdc option disables all such optimizations.
 \end{lstlisting}
 
 \section{opt\_muxtree -- eliminate dead trees in multiplexer trees}
@@ -613,7 +1085,7 @@ This pass only operates on completely selected modules without processes.
 \section{opt\_reduce -- simplify large MUXes and AND/OR gates}
 \label{cmd:opt_reduce}
 \begin{lstlisting}[numbers=left,frame=single]
-    opt_reduce [selection]
+    opt_reduce [options] [selection]
 
 This pass performs two interlinked optimizations:
 
@@ -622,6 +1094,12 @@ duplicated inputs.
 
 2. it identifies duplicated inputs to MUXes and replaces them with a single
 input with the original control signals OR'ed together.
+
+    -fine
+      perform fine-grain optimizations
+
+    -full
+      alias for -fine
 \end{lstlisting}
 
 \section{opt\_rmdff -- remove DFFs with constant inputs}
@@ -645,6 +1123,23 @@ are then merged to one cell.
         Do not merge MUX cells.
 \end{lstlisting}
 
+\section{plugin -- load and list loaded plugins}
+\label{cmd:plugin}
+\begin{lstlisting}[numbers=left,frame=single]
+    plugin [options]
+
+Load and list loaded plugins.
+
+    -i <plugin_filename>
+        Load (install) the specified plugin.
+
+    -a <alias_name>
+        Register the specified alias name for the loaded plugin
+
+    -l
+        List loaded plugins
+\end{lstlisting}
+
 \section{proc -- translate processes to netlists}
 \label{cmd:proc}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -739,14 +1234,43 @@ Load modules from an ilang file to the current design. (ilang is a text
 representation of a design in yosys's internal format.)
 \end{lstlisting}
 
+\section{read\_liberty -- read cells from liberty file}
+\label{cmd:read_liberty}
+\begin{lstlisting}[numbers=left,frame=single]
+    read_liberty [filename]
+
+Read cells from liberty file as modules into current design.
+
+    -lib
+        only create empty blackbox modules
+
+    -ignore_redef
+        ignore re-definitions of modules. (the default behavior is to
+        create an error message.)
+
+    -ignore_miss_func
+        ignore cells with missing function specification of outputs
+
+    -ignore_miss_dir
+        ignore cells with a missing or invalid direction
+        specification on a pin
+
+    -setattr <attribute_name>
+        set the specified attribute (to the value 1) on all loaded modules
+\end{lstlisting}
+
 \section{read\_verilog -- read modules from verilog file}
 \label{cmd:read_verilog}
 \begin{lstlisting}[numbers=left,frame=single]
-    read_verilog [filename]
+    read_verilog [options] [filename]
 
 Load modules from a verilog file to the current design. A large subset of
 Verilog-2005 is supported.
 
+    -sv
+        enable support for SystemVerilog features. (only a small subset
+        of SystemVerilog is supported)
+
     -dump_ast1
         dump abstract syntax tree (before simplification)
 
@@ -794,10 +1318,21 @@ Verilog-2005 is supported.
         don't perform basic optimizations (such as const folding) in the
         high-level front-end.
 
+    -icells
+        interpret cell types starting with '$' as internal cell types
+
     -ignore_redef
         ignore re-definitions of modules. (the default behavior is to
         create an error message.)
 
+    -defer
+        only read the abstract syntax tree and defer actual compilation
+        to a later 'hierarchy' command. Useful in cases where the default
+        parameters of modules yield invalid or not synthesizable code.
+
+    -setattr <attribute_name>
+        set the specified attribute (to the value 1) on all loaded modules
+
     -Dname[=definition]
         define the preprocessor symbol 'name' and set its optional value
         'definition'
@@ -805,6 +1340,14 @@ Verilog-2005 is supported.
     -Idir
         add 'dir' to the directories which are used when searching include
         files
+
+The command 'verilog_defaults' can be used to register default options for
+subsequent calls to 'read_verilog'.
+
+Note that the Verilog frontend does a pretty good job of processing valid
+verilog input, but has not very good error reporting. It generally is
+recommended to use a simulator (for example icarus verilog) for checking
+the syntax of the code, rather than to rely on read_verilog for that.
 \end{lstlisting}
 
 \section{rename -- rename object in the design}
@@ -816,10 +1359,17 @@ Rename the specified object. Note that selection patterns are not supported
 by this command.
 
 
-    rename -enumerate [selection]
+    rename -enumerate [-pattern <pattern>] [selection]
 
 Assign short auto-generated names to all selected wires and cells with private
-names.
+names. The -pattern option can be used to set the pattern for the new names.
+The character % in the pattern is replaced with a integer number. The default
+pattern is '_%_'.
+
+    rename -hide [selection]
+
+Assign private names (the ones with $-prefix) to all selected wires and cells
+with public names. This ignores all selected ports.
 \end{lstlisting}
 
 \section{sat -- solve a SAT problem in the circuit}
@@ -864,9 +1414,15 @@ and additional constraints passed as parameters.
         show the model for the specified signal. if no -show option is
         passed then a set of signals to be shown is automatically selected.
 
+    -show-inputs, -show-outputs
+        add all module input (output) ports to the list of shown signals
+
     -ignore_div_by_zero
         ignore all solutions that involve a division by zero
 
+    -ignore_unknown_cells
+        ignore all cells that can not be matched to a SAT model
+
 The following options can be used to set up a sequential problem:
 
     -seq <N>
@@ -889,21 +1445,50 @@ The following options can be used to set up a sequential problem:
     -set-init-undef
         set all initial states (not set using -set-init) to undef
 
+    -set-init-def
+        do not force a value for the initial state but do not allow undef
+
+    -set-init-zero
+        set all initial states (not set using -set-init) to zero
+
+    -dump_vcd <vcd-file-name>
+        dump SAT model (counter example in proof) to VCD file
+
+    -dump_cnf <cnf-file-name>
+        dump CNF of SAT problem (in DIMACS format). in temporal induction
+        proofs this is the CNF of the first induction step.
+
 The following additional options can be used to set up a proof. If also -seq
 is passed, a temporal induction proof is performed.
 
+    -tempinduct
+        Perform a temporal induction proof. In a temporalinduction proof it is
+        proven that the condition holds forever after the number of time steps
+        specified using -seq.
+
+    -tempinduct-def
+        Perform a temporal induction proof. Assume an initial state with all
+        registers set to defined values for the induction step.
+
     -prove <signal> <value>
-        Attempt to proof that <signal> is always <value>. In a temporal
-        induction proof it is proven that the condition holds forever after
-        the number of time steps passed using -seq.
+        Attempt to proof that <signal> is always <value>.
 
     -prove-x <signal> <value>
         Like -prove, but an undef (x) bit in the lhs matches any value on
         the right hand side. Useful for equivialence checking.
 
+    -prove-asserts
+        Prove that all asserts in the design hold.
+
+    -prove-skip <N>
+        Do not enforce the prove-condition for the first <N> time steps.
+
     -maxsteps <N>
         Set a maximum length for the induction.
 
+    -initsteps <N>
+        Set initial length for the induction.
+
     -timeout <N>
         Maximum number of seconds a single SAT instance may take.
 
@@ -912,6 +1497,12 @@ is passed, a temporal induction proof is performed.
 
     -verify-no-timeout
         Like -verify but do not return an error for timeouts.
+
+    -falsify
+        Return an error and stop the synthesis script if the proof succeeds.
+
+    -falsify-no-timeout
+        Like -falsify but do not return an error for timeouts.
 \end{lstlisting}
 
 \section{scatter -- add additional intermediate nets}
@@ -960,15 +1551,24 @@ design.
 \section{script -- execute commands from script file}
 \label{cmd:script}
 \begin{lstlisting}[numbers=left,frame=single]
-    script <filename>
+    script <filename> [<from_label>:<to_label>]
 
 This command executes the yosys commands in the specified file.
+
+The 2nd argument can be used to only execute the section of the
+file between the specified labels. An empty from label is synonymous
+for the beginning of the file and an empty to label is synonymous
+for the end of the file.
+
+If only one label is specified (without ':') then only the block
+marked with that label (until the next label) is executed.
 \end{lstlisting}
 
 \section{select -- modify and view the list of selected objects}
 \label{cmd:select}
 \begin{lstlisting}[numbers=left,frame=single]
     select [ -add | -del | -set <name> ] <selection>
+    select [ -assert-none | -assert-any ] <selection>
     select [ -list | -write <filename> | -count | -clear ]
     select -module <modname>
 
@@ -987,7 +1587,22 @@ described here.
 
     -set <name>
         do not modify the current selection. instead save the new selection
-        under the given name (see @<name> below).
+        under the given name (see @<name> below). to save the current selection,
+        use "select -set <name> %"
+
+    -assert-none
+        do not modify the current selection. instead assert that the given
+        selection is empty. i.e. produce an error if any object matching the
+        selection is found.
+
+    -assert-any
+        do not modify the current selection. instead assert that the given
+        selection is non-empty. i.e. produce an error if no object matching
+        the selection is found.
+
+    -assert-count N
+        do not modify the current selection. instead assert that the given
+        selection contains exactly N objects.
 
     -list
         list all objects in the current selection
@@ -999,8 +1614,12 @@ described here.
         count all objects in the current selection
 
     -clear
-        clear the current selection. this effectively selects the
-        whole design.
+        clear the current selection. this effectively selects the whole
+        design. it also resets the selected module (see -module). use the
+        command 'select *' to select everything but stay in the current module.
+
+    -none
+        create an empty selection. the current module is unchanged.
 
     -module <modname>
         limit the current scope to the specified module.
@@ -1030,8 +1649,12 @@ Pushing (selecting) object when in -module mode:
     <obj_pattern>
         select the specified object(s) from the current module
 
-A <mod_pattern> can be a module name or wildcard expression (*, ?, [..])
-matching module names.
+A <mod_pattern> can be a module name, wildcard expression (*, ?, [..])
+matching module names, or one of the following:
+
+    A:<pattern>, A:<pattern>=<pattern>
+        all modules with an attribute matching the given pattern
+        in addition to = also <, <=, >=, and > are supported
 
 An <obj_pattern> can be an object name, wildcard expression, or one of
 the following:
@@ -1039,6 +1662,12 @@ the following:
     w:<pattern>
         all wires with a name matching the given wildcard pattern
 
+    i:<pattern>, o:<pattern>, x:<pattern>
+        all inputs (i:), outputs (o:) or any ports (x:) with matching names
+
+    s:<size>, s:<min>:<max>
+        all wires with a matching width
+
     m:<pattern>
         all memories with a name matching the given pattern
 
@@ -1055,7 +1684,11 @@ the following:
         all objects with an attribute name matching the given pattern
 
     a:<pattern>=<pattern>
-        all objects with a matching attribute name-value-pair
+        all objects with a matching attribute name-value-pair.
+        in addition to = also <, <=, >=, and > are supported
+
+    r:<pattern>, r:<pattern>=<pattern>
+        cells with matching parameters. also with <, <=, >= and >.
 
     n:<pattern>
         all objects with a name matching the given pattern
@@ -1084,6 +1717,12 @@ The following actions can be performed on the top sets on the stack:
     %d
         pop the top set from the stack and subtract it from the new top
 
+    %D
+        like %d but swap the roles of two top sets on the stack
+
+    %c
+        create a copy of the top set rom the stack and push it
+
     %x[<num1>|*][.<num2>][:<rule>[:<rule>..]]
         expand top set <num1> num times according to the specified rules.
         (i.e. select all cells connected to selected wires and select all
@@ -1101,12 +1740,96 @@ The following actions can be performed on the top sets on the stack:
     %co[<num1>|*][.<num2>][:<rule>[:<rule>..]]
         simmilar to %x, but only select input (%ci) or output cones (%co)
 
+    %a
+        expand top set by selecting all wires that are (at least in part)
+        aliases for selected wires.
+
+    %s
+        expand top set by adding all modules of instantiated cells in selected
+        modules
+
+    %m
+        expand top set by selecting all modules that contain selected objects
+
 Example: the following command selects all wires that are connected to a
 'GATE' input of a 'SWITCH' cell:
 
     select */t:SWITCH %x:+[GATE] */t:SWITCH %d
 \end{lstlisting}
 
+\section{setattr -- set/unset attributes on objects}
+\label{cmd:setattr}
+\begin{lstlisting}[numbers=left,frame=single]
+    setattr [ -mod ] [ -set name value | -unset name ]... [selection]
+
+Set/unset the given attributes on the selected objects. String values must be
+passed in double quotes (").
+
+When called with -mod, this command will set and unset attributes on modules
+instead of objects within modules.
+\end{lstlisting}
+
+\section{setparam -- set/unset parameters on objects}
+\label{cmd:setparam}
+\begin{lstlisting}[numbers=left,frame=single]
+    setparam [ -set name value | -unset name ]... [selection]
+
+Set/unset the given parameters on the selected cells. String values must be
+passed in double quotes (").
+\end{lstlisting}
+
+\section{setundef -- replace undef values with defined constants}
+\label{cmd:setundef}
+\begin{lstlisting}[numbers=left,frame=single]
+    setundef [options] [selection]
+
+This command replaced undef (x) constants with defined (0/1) constants.
+
+    -undriven
+        also set undriven nets to constant values
+
+    -zero
+        replace with bits cleared (0)
+
+    -one
+        replace with bits set (1)
+
+    -random <seed>
+        replace with random bits using the specified integer als seed
+        value for the random number generator.
+\end{lstlisting}
+
+\section{share -- perform sat-based resource sharing}
+\label{cmd:share}
+\begin{lstlisting}[numbers=left,frame=single]
+    share [options] [selection]
+
+This pass merges shareable resources into a single resource. A SAT solver
+is used to determine if two resources are share-able.
+
+  -force
+    Per default the selection of cells that is considered for sharing is
+    narrowed using a list of cell types. With this option all selected
+    cells are considered for resource sharing.
+
+    IMPORTANT NOTE: If the -all option is used then no cells with internal
+    state must be selected!
+
+  -aggressive
+    Per default some heuristics are used to reduce the number of cells
+    considered for resource sharing to only large resources. This options
+    turns this heuristics off, resulting in much more cells being considered
+    for resource sharing.
+
+  -fast
+    Only consider the simple part of the control logic in SAT solving, resulting
+    in much easier SAT problems at the cost of maybe missing some oportunities
+    for resource sharing.
+
+  -limit N
+    Only perform the first N merges, then stop. This is useful for debugging.
+\end{lstlisting}
+
 \section{shell -- enter interactive command mode}
 \label{cmd:shell}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -1163,11 +1886,16 @@ to a graphics file (usually SVG or PostScript).
     -prefix <prefix>
         generate <prefix>.* instead of ~/.yosys_show.*
 
-    -color <color> <wire>
-        assign the specified color to the specified wire. The object can be
+    -color <color> <object>
+        assign the specified color to the specified object. The object can be
         a single selection wildcard expressions or a saved set of objects in
         the @<name> syntax (see "help select" for details).
 
+    -label <text> <object>
+        assign the specified label text to the specified object. The object can
+        be a single selection wildcard expressions or a saved set of objects in
+        the @<name> syntax (see "help select" for details).
+
     -colors <seed>
         Randomly assign colors to the wires. The integer argument is the seed
         for the random number generator. Change the seed value if the colored
@@ -1176,6 +1904,10 @@ to a graphics file (usually SVG or PostScript).
     -width
         annotate busses with a label indicating the width of the bus.
 
+    -signed
+        mark ports (A, B) that are declarted as signed (using the [AB]_SIGNED
+        cell parameter) with an asterisk next to the port name.
+
     -stretch
         stretch the graph so all inputs are on the left side and all outputs
         (including inout ports) are on the right side.
@@ -1189,8 +1921,11 @@ to a graphics file (usually SVG or PostScript).
     -long
         do not abbeviate objects with internal ($-prefixed) names
 
-When no <format> is specified, SVG is used. When no <format> and <viewer> is
-specified, 'yosys-svgviewer' is used to display the schematic.
+    -notitle
+        do not add the module name as graph title to the dot file
+
+When no <format> is specified, 'dot' is used. When no <format> and <viewer> is
+specified, 'xdot' is used to display the schematic.
 
 The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>',
 unless another prefix is specified using -prefix <prefix>.
@@ -1210,6 +1945,43 @@ primitives. The following internal cell types are mapped by this pass:
   $sr, $dff, $dffsr, $adff, $dlatch
 \end{lstlisting}
 
+\section{splice -- create explicit splicing cells}
+\label{cmd:splice}
+\begin{lstlisting}[numbers=left,frame=single]
+    splice [options] [selection]
+
+This command adds $slice and $concat cells to the design to make the splicing
+of multi-bit signals explicit. This for example is useful for coarse grain
+synthesis, where dedidacted hardware is needed to splice signals.
+
+    -sel_by_cell
+        only select the cell ports to rewire by the cell. if the selection
+        contains a cell, than all cell inputs are rewired, if necessary.
+
+    -sel_by_wire
+        only select the cell ports to rewire by the wire. if the selection
+        contains a wire, than all cell ports driven by this wire are wired,
+        if necessary.
+
+    -sel_any_bit
+        it is sufficient if the driver of any bit of a cell port is selected.
+        by default all bits must be selected.
+
+    -no_outputs
+        do not rewire selected module outputs.
+
+    -port <name>
+        only rewire cell ports with the specified name. can be used multiple
+        times. implies -no_output.
+
+    -no_port <name>
+        do not rewire cell ports with the specified name. can be used multiple
+        times. can not be combined with -port <name>.
+
+By default selected output wires and all cell ports of selected cells driven
+by selected wires are rewired.
+\end{lstlisting}
+
 \section{splitnets -- split up multi-bit nets}
 \label{cmd:splitnets}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -1217,13 +1989,18 @@ primitives. The following internal cell types are mapped by this pass:
 
 This command splits multi-bit nets into single-bit nets.
 
-    -format char1[char2]
+    -format char1[char2[char3]]
         the first char is inserted between the net name and the bit index, the
         second char is appended to the netname. e.g. -format () creates net
-        names like 'mysignal(42)'. the default is '[]'.
+        names like 'mysignal(42)'. the 3rd character is the range separation
+        character when creating multi-bit wires. the default is '[]:'.
 
     -ports
         also split module ports. per default only internal signals are split.
+
+    -driver
+        don't blindly split nets in individual bits. instead look at the driver
+        and split nets so that no driver drives only part of a net.
 \end{lstlisting}
 
 \section{stat -- print some statistics}
@@ -1238,6 +2015,10 @@ design.
         print design hierarchy with this module as top. if the design is fully
         selected and a module has the 'top' attribute set, this module is used
         default value for this option.
+
+    -width
+        annotate internal cell types with their word width.
+        e.g. $add_8 for an 8 bit wide $add cell.
 \end{lstlisting}
 
 \section{submod -- moving part of a module to a new submodule}
@@ -1263,6 +2044,52 @@ Only objects from one module might be selected. The value of the -name option
 is used as the value of the 'submod' attribute above.
 \end{lstlisting}
 
+\section{synth -- generic synthesis script}
+\label{cmd:synth}
+\begin{lstlisting}[numbers=left,frame=single]
+    synth [options]
+
+This command runs the default synthesis script. This command does not operate
+on partly selected designs.
+
+    -top <module>
+        use the specified module as top module (default='top')
+
+    -run <from_label>[:<to_label>]
+        only run the commands between the labels (see below). an empty
+        from label is synonymous to 'begin', and empty to label is
+        synonymous to the end of the command list.
+
+
+The following commands are executed by this synthesis command:
+
+    begin:
+        hierarchy -check [-top <top>]
+
+    coarse:
+        proc
+        opt
+        wreduce
+        alumacc
+        share
+        opt
+        fsm
+        opt -fast
+        memory -nomap
+        opt_clean
+
+    fine:
+        opt -fast -full
+        memory_map
+        opt -full
+        techmap
+        opt -fast
+
+    abc:
+        abc -fast
+        opt -fast
+\end{lstlisting}
+
 \section{synth\_xilinx -- synthesis for Xilinx FPGAs}
 \label{cmd:synth_xilinx}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -1340,7 +2167,7 @@ command 'proc' is wrapped using the tcl command 'procs' in order
 to avoid a name collision with the tcl builting command 'proc'.
 \end{lstlisting}
 
-\section{techmap -- simple technology mapper}
+\section{techmap -- generic technology mapper}
 \label{cmd:techmap}
 \begin{lstlisting}[numbers=left,frame=single]
     techmap [-map filename] [selection]
@@ -1355,11 +2182,34 @@ file.
         transforms the internal RTL cells to the internal gate
         library.
 
+    -map %<design-name>
+        like -map above, but with an in-memory design instead of a file.
+
     -share_map filename
         like -map, but look for the file in the share directory (where the
         yosys data files are). this is mainly used internally when techmap
         is called from other commands.
 
+    -extern
+        load the cell implementations as separate modules into the design
+        instead of inlining them.
+
+    -max_iter <number>
+        only run the specified number of iterations.
+
+    -recursive
+        instead of the iterative breadth-first algorithm use a recursive
+        depth-first algorithm. both methods should yield equivialent results,
+        but may differ in performance.
+
+    -autoproc
+        Automatically call "proc" on implementations that contain processes.
+
+    -assert
+        this option will cause techmap to exit with an error if it can't map
+        a selected cell. only cell types that end on an underscore are accepted
+        as final cell types by this mode.
+
     -D <define>, -I <incdir>
         this options are passed as-is to the verilog frontend for loading the
         map file. Note that the verilog frontend is also called with the
@@ -1372,6 +2222,13 @@ the module name will be used to match the cell.
 When a module in the map file has the 'techmap_simplemap' attribute set, techmap
 will use 'simplemap' (see 'help simplemap') to map cells matching the module.
 
+When a module in the map file has the 'techmap_maccmap' attribute set, techmap
+will use 'maccmap' (see 'help maccmap') to map cells matching the module.
+
+When a module in the map file has the 'techmap_wrap' attribute set, techmap
+will create a wrapper for the cell and then run the command string that the
+attribute is set to on the wrapper module.
+
 All wires in the modules from the map file matching the pattern _TECHMAP_*
 or *._TECHMAP_* are special wires that are used to pass instructions from
 the mapping module to the techmap command. At the moment the following special
@@ -1396,6 +2253,20 @@ wires are supported:
         wire to start out as non-constant and evaluate to a constant value
         during processing of other _TECHMAP_DO_* commands.
 
+        A _TECHMAP_DO_* command may start with the special token 'CONSTMAP; '.
+        in this case techmap will create a copy for each distinct configuration
+        of constant inputs and shorted inputs at this point and import the
+        constant and connected bits into the map module. All further commands
+        are executed in this copy. This is a very convenient way of creating
+        optimizied specializations of techmap modules without using the special
+        parameters described below.
+
+        A _TECHMAP_DO_* command may start with the special token 'RECURSION; '.
+        then techmap will recursively replace the cells in the module with their
+        implementation. This is not affected by the -max_iter option.
+
+        It is possible to combine both prefixes to 'RECURSION; CONSTMAP; '.
+
 In addition to this special wires, techmap also supports special parameters in
 modules in the map file:
 
@@ -1403,21 +2274,70 @@ modules in the map file:
         When a parameter with this name exists, it will be set to the type name
         of the cell that matches the module.
 
+    _TECHMAP_CONSTMSK_<port-name>_
+    _TECHMAP_CONSTVAL_<port-name>_
+        When this pair of parameters is available in a module for a port, then
+        former has a 1-bit for each constant input bit and the latter has the
+        value for this bit. The unused bits of the latter are set to undef (x).
+
+    _TECHMAP_BITS_CONNMAP_
+    _TECHMAP_CONNMAP_<port-name>_
+        For an N-bit port, the _TECHMAP_CONNMAP_<port-name>_ parameter, if it
+        exists, will be set to an N*_TECHMAP_BITS_CONNMAP_ bit vector containing
+        N words (of _TECHMAP_BITS_CONNMAP_ bits each) that assign each single
+        bit driver a unique id. The values 0-3 are reserved for 0, 1, x, and z.
+        This can be used to detect shorted inputs.
+
 When a module in the map file has a parameter where the according cell in the
 design has a port, the module from the map file is only used if the port in
 the design is connected to a constant value. The parameter is then set to the
 constant value.
 
+A cell with the name _TECHMAP_REPLACE_ in the map file will inherit the name
+of the cell that is beeing replaced.
+
 See 'help extract' for a pass that does the opposite thing.
 
 See 'help flatten' for a pass that does flatten the design (which is
 esentially techmap but using the design itself as map library).
 \end{lstlisting}
 
-\section{write\_autotest -- generate simple test benches}
-\label{cmd:write_autotest}
+\section{tee -- redirect command output to file}
+\label{cmd:tee}
+\begin{lstlisting}[numbers=left,frame=single]
+    tee [-q] [-o logfile|-a logfile] cmd
+
+Execute the specified command, optionally writing the commands output to the
+specified logfile(s).
+
+    -q
+        Do not print output to the normal destination (console and/or log file)
+
+    -o logfile
+        Write output to this file, truncate if exists.
+
+    -a logfile
+        Write output to this file, append if exists.
+\end{lstlisting}
+
+\section{test\_abcloop -- automatically test handling of loops in abc command}
+\label{cmd:test_abcloop}
+\begin{lstlisting}[numbers=left,frame=single]
+    test_abcloop [options]
+
+Test handling of logic loops in ABC.
+
+    -n {integer}
+        create this number of circuits and test them (default = 100).
+
+    -s {positive_integer}
+        use this value as rng seed value (default = unix time).
+\end{lstlisting}
+
+\section{test\_autotb -- generate simple test benches}
+\label{cmd:test_autotb}
 \begin{lstlisting}[numbers=left,frame=single]
-    write_autotest [filename]
+    test_autotb [options] [filename]
 
 Automatically create primitive verilog test benches for all modules in the
 design. The generated testbenches toggle the input pins of the module in
@@ -1433,6 +2353,148 @@ be forced to be interpreted as clock signal by setting the attribute
 The attribute 'gentb_constant' can be used to force a signal to a constant
 value after initialization. This can e.g. be used to force a reset signal
 low in order to explore more inner states in a state machine.
+
+    -n <int>
+        number of iterations the test bench shuld run (default = 1000)
+\end{lstlisting}
+
+\section{test\_cell -- automatically test the implementation of a cell type}
+\label{cmd:test_cell}
+\begin{lstlisting}[numbers=left,frame=single]
+    test_cell [options] {cell-types}
+
+Tests the internal implementation of the given cell type (for example '$add')
+by comparing SAT solver, EVAL and TECHMAP implementations of the cell types..
+
+Run with 'all' instead of a cell type to run the test on all supported
+cell types.
+
+    -n {integer}
+        create this number of cell instances and test them (default = 100).
+
+    -s {positive_integer}
+        use this value as rng seed value (default = unix time).
+
+    -f {ilang_file}
+        don't generate circuits. instead load the specified ilang file.
+
+    -map {filename}
+        pass this option to techmap.
+
+    -simlib
+        use "techmap -map +/simlib.v -max_iter 2 -autoproc"
+
+    -script {script_file}
+        instead of calling "techmap", call "script {script_file}".
+
+    -const
+        set some input bits to random constant values
+
+    -nosat
+        do not check SAT model or run SAT equivalence checking
+
+    -v
+        print additional debug information to the console
+
+    -vlog {filename}
+        create a verilog test bench to test simlib and write_verilog
+\end{lstlisting}
+
+\section{trace -- redirect command output to file}
+\label{cmd:trace}
+\begin{lstlisting}[numbers=left,frame=single]
+    trace cmd
+
+Execute the specified command, logging all changes the command performs on
+the design in real time.
+\end{lstlisting}
+
+\section{verific -- load Verilog and VHDL designs using Verific}
+\label{cmd:verific}
+\begin{lstlisting}[numbers=left,frame=single]
+    verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv} <verilog-file>..
+
+Load the specified Verilog/SystemVerilog files into Verific.
+
+
+    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008} <vhdl-file>..
+
+Load the specified VHDL files into Verific.
+
+
+    verific -import [-gates] {-all | <top-module>..}
+
+Elaborate the design for the sepcified top modules, import to Yosys and
+reset the internal state of Verific. A gate-level netlist is created
+when called with -gates.
+
+Visit http://verific.com/ for more information on Verific.
+\end{lstlisting}
+
+\section{verilog\_defaults -- set default options for read\_verilog}
+\label{cmd:verilog_defaults}
+\begin{lstlisting}[numbers=left,frame=single]
+    verilog_defaults -add [options]
+
+Add the sepcified options to the list of default options to read_verilog.
+
+
+    verilog_defaults -clear
+Clear the list of verilog default options.
+
+
+    verilog_defaults -push    verilog_defaults -pop
+Push or pop the list of default options to a stack. Note that -push does
+not imply -clear.
+\end{lstlisting}
+
+\section{vhdl2verilog -- importing VHDL designs using vhdl2verilog}
+\label{cmd:vhdl2verilog}
+\begin{lstlisting}[numbers=left,frame=single]
+    vhdl2verilog [options] <vhdl-file>..
+
+This command reads VHDL source files using the 'vhdl2verilog' tool and the
+Yosys Verilog frontend.
+
+    -out <out_file>
+        do not import the vhdl2verilog output. instead write it to the
+        specified file.
+
+    -vhdl2verilog_dir <directory>
+        do use the specified vhdl2verilog installation. this is the directory
+        that contains the setup_env.sh file. when this option is not present,
+        it is assumed that vhdl2verilog is in the PATH environment variable.
+
+    -top <top-entity-name>
+        The name of the top entity. This option is mandatory.
+
+The following options are passed as-is to vhdl2verilog:
+
+    -arch <architecture_name>
+    -unroll_generate
+    -nogenericeval
+    -nouniquify
+    -oldparser
+    -suppress <list>
+    -quiet
+    -nobanner
+    -mapfile <file>
+
+vhdl2verilog can be obtained from:
+http://www.edautils.com/vhdl2verilog.html
+\end{lstlisting}
+
+\section{wreduce -- reduce the word size of operations is possible}
+\label{cmd:wreduce}
+\begin{lstlisting}[numbers=left,frame=single]
+    wreduce [options] [selection]
+
+This command reduces the word size of operations. For example it will replace
+the 32 bit adders in the following code with adders of more appropriate widths:
+
+    module test(input [3:0] a, b, c, output [7:0] y);
+        assign y = a + b + c + 1;
+    endmodule
 \end{lstlisting}
 
 \section{write\_blif -- write design to BLIF file}
@@ -1456,18 +2518,33 @@ The following options can be useful when the generated file is not going to be
 read by a BLIF parser but a custom tool. It is recommended to not name the output
 file *.blif when any of this options is used.
 
-    -subckt
+    -icells
         do not translate Yosys's internal gates to generic BLIF logic
-        functions. Instead create .subckt lines for all cells.
+        functions. Instead create .subckt or .gate lines for all cells.
+
+    -gates
+        print .gate instead of .subckt lines for all cells that are not
+        instantiations of other modules from this design.
 
     -conn
         do not generate buffers for connected wires. instead use the
         non-standard .conn statement.
 
+    -param
+        use the non-standard .param statement to write module parameters
+
     -impltf
         do not write definitions for the $true and $false wires.
 \end{lstlisting}
 
+\section{write\_btor -- write design to BTOR file}
+\label{cmd:write_btor}
+\begin{lstlisting}[numbers=left,frame=single]
+    write_btor [filename]
+
+Write the current design to an BTOR file.
+\end{lstlisting}
+
 \section{write\_edif -- write design to EDIF netlist file}
 \label{cmd:write_edif}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -1484,6 +2561,24 @@ necessary to make small modifications to this command when a different tool
 is targeted.
 \end{lstlisting}
 
+\section{write\_file -- write a text to a file}
+\label{cmd:write_file}
+\begin{lstlisting}[numbers=left,frame=single]
+    write_file [options] output_file [input_file]
+
+Write the text fron the input file to the output file.
+
+    -a
+        Append to output file (instead of overwriting)
+
+
+Inside a script the input file can also can a here-document:
+
+    write_file hello.txt <<EOT
+    Hello World!
+    EOT
+\end{lstlisting}
+
 \section{write\_ilang -- write design to ilang file}
 \label{cmd:write_ilang}
 \begin{lstlisting}[numbers=left,frame=single]
diff --git a/manual/manual.tex b/manual/manual.tex
index 19d3b7b2..84be86e5 100644
--- a/manual/manual.tex
+++ b/manual/manual.tex
@@ -61,6 +61,7 @@ bookmarksopen=false%
 \usepackage{multibib}
 \usepackage{multirow}
 \usepackage{booktabs}
+\usepackage{pdfpages}
 
 \usepackage{listings}
 \usepackage{pifont}
@@ -202,7 +203,7 @@ YOSYS       & Yosys Open SYnthesis Suite \\
 \include{CHAPTER_Verilog}
 \include{CHAPTER_Optimize}
 \include{CHAPTER_Techmap}
-\include{CHAPTER_Eval}
+% \include{CHAPTER_Eval}
 
 \appendix
 
@@ -214,7 +215,7 @@ YOSYS       & Yosys Open SYnthesis Suite \\
 \input{command-reference-manual}
 
 \include{CHAPTER_Appnotes}
-\include{CHAPTER_StateOfTheArt}
+% \include{CHAPTER_StateOfTheArt}
 
 \bibliography{literature}
 \bibliographystyle{alphadin}
diff --git a/manual/presentation.sh b/manual/presentation.sh
index 980e1772..a3557a47 100755
--- a/manual/presentation.sh
+++ b/manual/presentation.sh
@@ -24,6 +24,8 @@ done
 
 PDFTEX_OPT="-shell-escape -halt-on-error"
 
+set -ex
+
 if ! $fast_mode; then
 	md5sum *.aux *.snm *.nav *.toc > autoloop.old
 	make -C PRESENTATION_Intro
diff --git a/manual/presentation.tex b/manual/presentation.tex
index 9a876de0..ee96253a 100644
--- a/manual/presentation.tex
+++ b/manual/presentation.tex
@@ -133,7 +133,7 @@ I like writing open source software. For example:
 \item OpenSCAD (now maintained by Marius Kintel)
 \item SPL (a not very popular scripting language)
 \item EmbedVM (a very simple compiler+vm for 8 bit micros)
-\item Lib(X)SVF (a library to play SVF/XSVF files over JTAG, used at LHC)
+\item Lib(X)SVF (a library to play SVF/XSVF files over JTAG)
 \item ROCK Linux (discontinued since 2010)
 \end{itemize}
 \end{frame}