\def\FIXME{{\color{red}\bf FIXME}}
-\lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=2em,xrightmargin=1em,numbers=left}
+\lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=0.7cm,xrightmargin=0.2cm,numbers=left}
\begin{document}
\title{Yosys Application Note 011: \\ Interactive Design Investigation}
-\author{Clifford Wolf \\ November 2013}
+\author{Clifford Wolf \\ Original Version December 2013}
\maketitle
\begin{abstract}
Yosys \cite{yosys} can be a great environment for building custom synthesis
-flows \cite{glaserwolf}. It can also be an excellent tool for teaching and
-learning Verilog based RTL synthesis. In both applications it is of great
-importance to be able to analyze the designs it produces easily.
+flows. It can also be an excellent tool for teaching and learning Verilog based
+RTL synthesis. In both applications it is of great importance to be able to
+analyze the designs it produces easily.
This Yosys application note covers the generation of circuit diagrams with the
Yosys {\tt show} command, the selection of interesting parts of the circuit
-using the {\tt select} command, and briefly discusses advanced commands for
-investigating the actual behavior of circuits.
+using the {\tt select} command, and briefly discusses advanced investigation
+commands for evaluating circuits and solving SAT problems.
\end{abstract}
\section{Installation and Prerequisites}
-This Application Note is based on GIT Rev. {\tt \FIXME} from \FIXME{} of
-Yosys \cite{yosys}. The {\tt README} file covers how to install Yosys. The
+This Application Note is based on the Yosys \cite{yosys} GIT Rev. {\tt 2b90ba1} from
+2013-12-08. The {\tt README} file covers how to install Yosys. The
{\tt show} command requires a working installation of GraphViz \cite{graphviz}
-for generating the actual circuit diagrams. Yosys must be build with Qt
-support in order to activate the built-in SVG viewer. Alternatively an
-external viewer can be used.
+and \cite{xdot} for generating the actual circuit diagrams.
\section{Overview}
symbols used in the circuit diagrams generated by it.
Sec.~\ref{navigate} introduces additional commands used to navigate in the
-design and select portions of the design and print additional information on
+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
current state. Various options can be used to change the appearance of the
circuit diagram, set the name and format for the output file, and so forth.
When called without any special options, it saves the circuit diagram in
-a temporary file and launches {\tt yosys-svgviewer} to display the diagram.
-Subsequent calls to {\tt show} re-use the {\tt yosys-svgviewer} instance
+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 Verilog file that
-demonstrates the usage of {\tt show} in a simple setting. Note that {\tt show}
+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
synthesis commands. The generated circuit diagrams are shown in Fig.~\ref{example_out}.
The first diagram (from top to bottom) shows the design directly after being
-read by the Verilog front-end. Input and output ports are visualized using
-octagonal shapes. Cells are visualized as rectangles with inputs on the left
+read by the Verilog front-end. Input and output ports are displayed as
+octagonal shapes. Cells are displayed as rectangles with inputs on the left
and outputs on the right side. The cell labels are two lines long: The first line
contains 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
Constants are shown as ellipses with the constant value as label. The syntax
{\tt <bit\_width>'<bits>} is used for for constants that are not 32-bit wide
-and/or contain bits that are not 0 or 1 (but {\tt x} or {\tt z}). Ordinary
+and/or contain bits that are not 0 or 1 (i.e. {\tt x} or {\tt z}). Ordinary
32-bit constants are written using decimal numbers.
Single-bit signals are shown as thin arrows pointing from the driver to the
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
+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
least complicated way, not about cleaning up after them. The next call to {\tt
clean} (or {\tt opt}, which includes {\tt clean} as one of its operations) will
clean up this artefacts. This operation is so common in Yosys scripts that it
-can simply be abbreviated by using the {\tt ;;} token, which doubles as
+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 call {\tt clean}
+left behind some operations, it is therefore recommended to always call {\tt clean}
before calling {\tt show}.
\medskip
As has been indicated by the last example, Yosys is can manage signal vectors (aka.
multi-bit wires or buses) as native objects. This provides great advantages
when analyzing circuits that operate on wide integers. But it also introduces
-some additional complexity when the individual bits of of a signal vector need
-to be accessed. The example show in Fig.~\ref{splice_dia} and \ref{splice_src}
+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 are broken out from the signals
-and are connected. So The top row of the box connecting the signals {\tt a} and {\tt b} indicates
+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 slightly different look to emphasise that they are not actual signal
+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
descriptions into Yosys: First the Verilog file for the cell library can be
passed directly to the {\tt show} command using the {\tt -lib <filename>}
option. Secondly it is possible to load cell libraries into the design with
-the {\tt read\_verilog -lib <filename>} command. The later option has the great
+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}
+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
\subsection{Miscellaneous notes}
-Per default the {\tt show} command outputs a temporary SVG file and launches
-{\tt yosys-svgviewer} to display it. The options {\tt -format}, {\tt -viewer}
+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 {\tt yosys-svgviewer} the left mouse button is per default bound to move the
-diagram (and the mouse wheel can be used for zooming in and out). However, in
-some cases one wants to copy text from the diagram. In this cases the
-View->Interactive checkbox must be activated. This switch the rendering back-end
-to one that supports interaction with the SVG file, such as selecting text.
-
In densely connected circuits it is sometimes hard to keep track of the
individual signal wires. For this cases it can be useful to call {\tt show}
with the {\tt -colors <integer>} argument, which randomly assigns colors to the
-nets. The integer (> 0) is used as seed value for the random number
-generation. Sometimes it is necessary it try some values to find an assignment
-of colors that works.
+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 so
-far. For complex modules the generated circuit diagrams are just stupidly big
+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 only needs to carefully decide
+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 where
-a problem can be reproduces. So if for example internal state before calling
-the {\tt techmap} command already fails to verify, it is better to troubleshoot
+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}.
Note: It is generally recommended to verify the internal state of a design by
writing it to a Verilog file using {\tt write\_verilog -noexpr} and using the
simulation models from {\tt simlib.v} and {\tt simcells.v} from the Yosys data
-directory (see {\tt yosys-config -{}-datdir}).
+directory (as printed by {\tt yosys-config -{}-datdir}).
\subsection{Interactive Navigation}
1 modules:
example
-yosys> cd example
+yosys> cd example
yosys [example]> ls
\label{seladd}
\end{figure}
-When a module is selected using {\tt cd} command, all commands (with a few
+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. So this can also be useful for synthesis scripts
+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.
module. Whenever a command has {\tt [selection]} as last argument in its usage
help, this means that it will use the engine behind the {\tt select} command
to evaluate additional arguments and use the resulting selection instead of
-the selection performed by the last {\tt select} command.
+the 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
In many cases simply adding more and more stuff to the selection is an
ineffective way of selecting the interesting part of the design. Special
-arguments can be used to differently combine the elements on the stack.
+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 pushed the result back on the stack. So the
+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:
Selecting {\tt a:sumstuff} in this module will yield the circuit diagram shown
in Fig.~\ref{sumprod_00}. As only the cells themselves are selected, but not
the temporary wire {\tt \$1\_Y}, the two adders are shown as two disjunct
-parts. This can be very useful for global signal like clock and reset signals: just
+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 schon in Fig.~\ref{sumprod_01}.
+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}
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 to operation inly works against the direction of data flow. That means,
+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
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 the usage of {\tt \%ci} pattern. We synthesize the circuit using {\tt proc;
+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 cell/port pattern in {\tt \%ci} actions}
+\caption{Demo circuit for demonstrating some advanced Yosys features}
\label{memdemo_src}
\end{figure}
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 we could as well only
-specify the port names:
+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]
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 commands such as
+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 multiplexer select
+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}.
This actions for traversing the circuit graph, combined with the actions for
boolean operations such as intersection ({\tt \%i}) and difference ({\tt \%d})
-are a powerful tool for extracting the relevant portions of the circuit under
+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}
-\FIXME{}
+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}
-\FIXME{} --- submod, eval, sat
+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}
-\FIXME
+Yosys provides a wide range of functions to analyze and investigate designs. For
+many cases it is sufficient to simply display circuit diagrams, maybe use some
+additional commands to narrow the scope of the circuit diagrams to the interesting
+parts of the circuit. But some cases require more than that. For this applications
+Yosys provides commands that can be used to further inspect the behavior of the
+circuit, either by evaluating which output values are generated from certain input values
+({\tt eval}) or by evaluation which input values and initial conditions can result
+in a certain behavior at the outputs ({\tt sat}). The SAT command can even be used
+to prove (or disprove) theorems regarding the circuit, in more advanced cases
+with the additional help of a miter circuit.
+
+This features can be powerful tools for the circuit designer using Yosys as a
+utility for building circuits and the software developer using Yosys as a
+framework for new algorithms alike.
\begin{thebibliography}{9}
Clifford Wolf. The Yosys Open SYnthesis Suite.
\url{http://www.clifford.at/yosys/}
-\bibitem{glaserwolf}
-Johann Glaser. Clifford Wolf. Methodology and Example-Driven Interconnect
-Synthesis for Designing Heterogeneous Coarse-Grain Reconfigurable
-Architectures. In: Jan Haase (Editor). {\it Models, Methods, and Tools for Complex Chip Design.
-Lecture Notes in Electrical Engineering. Volume 265, 2014, pp 201-221.\/}
-\href{http://dx.doi.org/10.1007/978-3-319-01418-0_12}{DOI 10.1007/978-3-319-01418-0\_12}
-
\bibitem{graphviz}
Graphviz - Graph Visualization Software.
\url{http://www.graphviz.org/}
+\bibitem{xdot}
+xdot.py - an interactive viewer for graphs written in Graphviz's dot language.
+\url{https://github.com/jrfonseca/xdot.py}
+
+\bibitem{CircuitSAT}
+{\it Circuit satisfiability problem} on Wikipedia
+\url{http://en.wikipedia.org/wiki/Circuit_satisfiability}
+
+\bibitem{MiniSAT}
+MiniSat: a minimalistic open-source SAT solver.
+\url{http://minisat.se/}
+
+\bibitem{tip}
+Niklas Een and Niklas S\"orensson (2003).
+Temporal Induction by Incremental SAT Solving.
+\url{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.8161}
+
\end{thebibliography}
\end{document}
projects / yosys.git / blobdiff