\begin{document}
\title{Yosys Application Note 011: \\ Interactive Design Investigation}
-\author{Clifford Wolf \\ December 2013}
+\author{Clifford Wolf \\ Original Version December 2013}
\maketitle
\begin{abstract}
\section{Installation and Prerequisites}
-This Application Note is based on the Yosys \cite{yosys} GIT Rev. {\tt \FIXME} from
-\FIXME{}. 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 for the built-in SVG viewer. Alternatively an external viewer can be
-used, if Qt is not available.
+and \cite{xdot} for generating the actual circuit diagrams.
\section{Overview}
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}
descriptions into Yosys: First the Verilog file for the cell library can be
passed directly to the {\tt show} command using the {\tt -lib <filename>}
option. Secondly it is possible to load cell libraries into the design with
-the {\tt read\_verilog -lib <filename>} command. The 2nd method has the great
+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.
\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 switches the rendering back-end
-in a mode 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
{\it when\/} to display it, with respect to the synthesis flow. In general
it is a good idea to troubleshoot a circuit in the earliest state in which
a problem can be reproduced. So if, for example, the internal state before calling
-the {\tt techmap} command already fails to verify, it is better to troubleshoot
+the {\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}.
1 modules:
example
-yosys> cd example
+yosys> cd example
yosys [example]> ls
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}
{\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.
{\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'10 1'1 | 2'xx 2'10
2'11 1'0 | 2'00 2'00
2'11 1'1 | 2'xx 2'11
-
- Assumend undef (x) value for the following singals: \s2
+
+ Assumed undef (x) value for the following signals: \s2
\end{verbatim}
}
Solving problem with 2790 variables and 8241 clauses..
SAT proof finished - model found: FAIL!
- ______ ___ ___ _ _ _ _
+ ______ ___ ___ _ _ _ _
(_____ \ / __) / __) (_) | | | |
_____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |
| ____/ ___) _ \ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|
- | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_
+ | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_
|_| |_| \___/ \___/ |_| |_| \_____|_|\_)_____)\____|_|
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.}
{\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
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}
\url{http://minisat.se/}
\bibitem{tip}
-Niklas Een and Niklas Sรถrensson (2003).
+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}
projects / yosys.git / blobdiff