riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Progress on AppNote 011

This commit is contained in:
Clifford Wolf 2013-12-08 15:08:51 +01:00
parent 2b90ba1e96
commit 0bd08688b8
1 changed files with 88 additions and 86 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

174
manual/APPNOTE_011_Design_Investigation.tex
View File

@ -49,34 +49,34 @@
\def\FIXME{{\color{red}\bf FIXME}} \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} \begin{document}
\title{Yosys Application Note 011: \\ Interactive Design Investigation} \title{Yosys Application Note 011: \\ Interactive Design Investigation}
\author{Clifford Wolf \\ November 2013} \author{Clifford Wolf \\ December 2013}
\maketitle \maketitle
\begin{abstract} \begin{abstract}
Yosys \cite{yosys} can be a great environment for building custom synthesis 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 flows. It can also be an excellent tool for teaching and learning Verilog based
learning Verilog based RTL synthesis. In both applications it is of great RTL synthesis. In both applications it is of great importance to be able to
importance to be able to analyze the designs it produces easily. analyze the designs it produces easily.
This Yosys application note covers the generation of circuit diagrams with the This Yosys application note covers the generation of circuit diagrams with the
Yosys {\tt show} command, the selection of interesting parts of the circuit Yosys {\tt show} command, the selection of interesting parts of the circuit
using the {\tt select} command, and briefly discusses advanced commands for using the {\tt select} command, and briefly discusses advanced investigation
investigating the actual behavior of circuits. commands for evaluating circuits and solving SAT problems.
\end{abstract} \end{abstract}
\section{Installation and Prerequisites} \section{Installation and Prerequisites}
This Application Note is based on GIT Rev. {\tt \FIXME} from \FIXME{} of This Application Note is based on the Yosys \cite{yosys} GIT Rev. {\tt \FIXME} from
Yosys \cite{yosys}. The {\tt README} file covers how to install Yosys. The \FIXME{}. The {\tt README} file covers how to install Yosys. The
{\tt show} command requires a working installation of GraphViz \cite{graphviz} {\tt show} command requires a working installation of GraphViz \cite{graphviz}
for generating the actual circuit diagrams. Yosys must be build with Qt for generating the actual circuit diagrams. Yosys must be build with Qt
support in order to activate the built-in SVG viewer. Alternatively an support for the built-in SVG viewer. Alternatively an external viewer can be
external viewer can be used. used, if Qt is not available.
\section{Overview} \section{Overview}
@ -86,7 +86,7 @@ Sec.~\ref{intro_show} introduces the {\tt show} command and explains the
symbols used in the circuit diagrams generated by it. symbols used in the circuit diagrams generated by it.
Sec.~\ref{navigate} introduces additional commands used to navigate in the 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. 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 Sec.~\ref{poke} introduces commands to evaluate the design and solve SAT
@ -137,8 +137,8 @@ Subsequent calls to {\tt show} re-use the {\tt yosys-svgviewer} instance
\subsection{A simple circuit} \subsection{A simple circuit}
Fig.~\ref{example_src} shows a simple synthesis script and Verilog file that Fig.~\ref{example_src} shows a simple synthesis script and a Verilog file that
demonstrates the usage of {\tt show} in a simple setting. Note that {\tt show} 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 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 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 also allows the user to enter an interactive shell to further investigate the
@ -148,8 +148,8 @@ So this script, when executed, will show the design after each of the three
synthesis commands. The generated circuit diagrams are shown in Fig.~\ref{example_out}. 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 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 read by the Verilog front-end. Input and output ports are displayed as
octagonal shapes. Cells are visualized as rectangles with inputs on the left 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 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 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 type. Internal cell types are prefixed with a dollar sign. The Yosys manual
@ -157,7 +157,7 @@ contains a chapter on the internal cell library used in Yosys.
Constants are shown as ellipses with the constant value as label. The syntax 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 {\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. 32-bit constants are written using decimal numbers.
Single-bit signals are shown as thin arrows pointing from the driver to the Single-bit signals are shown as thin arrows pointing from the driver to the
@ -178,7 +178,7 @@ The {\tt proc} command transforms the process from the first diagram into a
multiplexer and a d-type flip-flip, which brings us to the 2nd diagram. 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 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 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 {\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 quite usual to see such artefacts after calling commands that perform changes
@ -186,9 +186,9 @@ in the design, as most commands only care about doing the transformation in the
least complicated way, not about cleaning up after them. The next call to {\tt 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} (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 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 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}. before calling {\tt show}.
\medskip \medskip
@ -224,20 +224,20 @@ circuit is a half-adder built from simple CMOS gates.)}
As has been indicated by the last example, Yosys is can manage signal vectors (aka. 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 multi-bit wires or buses) as native objects. This provides great advantages
when analyzing circuits that operate on wide integers. But it also introduces 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 some additional complexity when the individual bits of of a signal vector
to be accessed. The example show in Fig.~\ref{splice_dia} and \ref{splice_src} 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. demonstrates how such circuits are visualized by the {\tt show} command.
The key elements in understanding this circuit diagram are of course the boxes 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>}. 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 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 other side. The {\tt <MSB>:<LSB>} tuples specify which bits of the signals are broken out
and are connected. So The top row of the box connecting the signals {\tt a} and {\tt b} indicates 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 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}. 1:1) of signal {\tt x}.
Lines connecting such boxes together and lines connecting such boxes to cell 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 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 like a technicality, until one wants to debug a problem related to the way
Yosys internally represents signal vectors, for example when writing custom Yosys internally represents signal vectors, for example when writing custom
@ -258,11 +258,11 @@ Verilog file containing blackbox modules. There are two ways to load cell
descriptions into Yosys: First the Verilog file for the cell library can be 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>} 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 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 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 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 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 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 {\tt -ports} option is required to also split module ports. Per default the
@ -279,15 +279,15 @@ plotting multiple modules in one run.
In {\tt yosys-svgviewer} the left mouse button is per default bound to move the 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 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 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 View->Interactive checkbox must be activated. This switches the rendering back-end
to one that supports interaction with the SVG file, such as selecting text. 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 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} 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 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 nets. The integer (> 0) is used as seed value for the random color
generation. Sometimes it is necessary it try some values to find an assignment assignments. Sometimes it is necessary it try some values to find an assignment
of colors that works. of colors that looks good.
The command {\tt help show} prints a complete listing of all options supported The command {\tt help show} prints a complete listing of all options supported
by the {\tt show} command. by the {\tt show} command.
@ -295,15 +295,15 @@ by the {\tt show} command.
\section{Navigating the design} \section{Navigating the design}
\label{navigate} \label{navigate}
Plotting circuit diagrams for entire modules in the design brings us only so Plotting circuit diagrams for entire modules in the design brings us only helps
far. For complex modules the generated circuit diagrams are just stupidly big 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 and are no help at all. In such cases one first has to select the relevant
portions of the circuit. 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 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 it is a good idea to troubleshoot a circuit in the earliest state in which
a problem can be reproduces. So if for example internal state before calling 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 the coarse-grain version of the circuit before {\tt techmap} than the gate-level
circuit after {\tt techmap}. circuit after {\tt techmap}.
@ -313,7 +313,7 @@ circuit after {\tt techmap}.
Note: It is generally recommended to verify the internal state of a design by 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 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 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} \subsection{Interactive Navigation}
@ -407,9 +407,9 @@ module-context and not design-context.
\label{seladd} \label{seladd}
\end{figure} \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 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 where different synthesis strategies should be applied to different modules
in the design. in the design.
@ -441,7 +441,7 @@ dump t:\$add} will print information on all {\tt \$add} cells in the active
module. Whenever a command has {\tt [selection]} as last argument in its usage 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 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 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 Normally the {\tt select} command overwrites a previous selection. The
commands {\tt select -add} and {\tt select -del} can be used to add commands {\tt select -add} and {\tt select -del} can be used to add
@ -480,9 +480,9 @@ select -list} command to list the current selection.)
In many cases simply adding more and more stuff to the selection is an 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 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 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} following command will select all {\$add} cells that have the {\tt foo}
attribute set: attribute set:
@ -498,7 +498,7 @@ can be used to mark portions of code for analysis.)
Selecting {\tt a:sumstuff} in this module will yield the circuit diagram shown 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 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 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 unselect them using a command such as {\tt select -del clk rst} and each cell
using them will get its own net label. using them will get its own net label.
@ -520,8 +520,8 @@ all cells and signals that are used to generate the signal {\tt sum}. The {\tt \
action can be used to select the input cones of all object in the top selection 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. in the stack maintained by the {\tt select} command.
As the {\tt \%x} action, this commands broadens the selection by one "`step"'. But 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, 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. 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 Fig.~\ref{select_prod} show the sequence of diagrams generated by the following
@ -558,13 +558,13 @@ action, or we only want to follow certain cell types and/or ports. This can be a
patterns that can be appended to the {\tt \%ci} action. 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 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} 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}. now we see the diagram shown in Fig.~\ref{memdemo_00}.
\begin{figure}[b!] \begin{figure}[b!]
\lstinputlisting{APPNOTE_011_Design_Investigation/memdemo.v} \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} \label{memdemo_src}
\end{figure} \end{figure}
@ -600,8 +600,8 @@ an include or exclude pattern, followed by an optional comma separated list
of cell types, followed by an optional comma separated list of port names in of cell types, followed by an optional comma separated list of port names in
square brackets. square brackets.
Since we know that the only cell considered in this case we could as well only Since we know that the only cell considered in this case is a {\tt \$dff} cell,
specify the port names: we could as well only specify the port names:
\begin{verbatim} \begin{verbatim}
show y %ci2:+[Q,D] show y %ci2:+[Q,D]
@ -628,14 +628,14 @@ show y %ci2:-[CLK] %ci2
From this we would learn that the next cell is a {\tt \$mux} cell and we would add additional 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 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} \begin{verbatim}
show y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff show y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff
\end{verbatim} \end{verbatim}
in which the first {\tt \%ci} jumps over the initial d-type flip-flop and the 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 inputs and flip-flop cells. The diagram produces by this command is shown in
Fig.~\ref{memdemo_01}. Fig.~\ref{memdemo_01}.
@ -647,7 +647,7 @@ previously also accepts this advanced syntax.
This actions for traversing the circuit graph, combined with the actions for This actions for traversing the circuit graph, combined with the actions for
boolean operations such as intersection ({\tt \%i}) and difference ({\tt \%d}) 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. investigation.
See {\tt help select} for a complete list of actions available in selections. See {\tt help select} for a complete list of actions available in selections.
@ -672,7 +672,7 @@ 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. 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. The {\tt history} command can be used to list all recent interactive commands.
A feature that can be useful to create such a script from the commands used in This feature can be useful for creating such a script from the commands used in
an interactive session. an interactive session.
\section{Advanced investigation techniques} \section{Advanced investigation techniques}
@ -688,7 +688,7 @@ 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 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. circuit from Fig.~\ref{memdemo_src} and \ref{memdemo_00} into its components.
The {\tt -name} option can is used to specify the name of the new module and 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. also the name of the new cell in the current module.
\begin{figure}[t] \begin{figure}[t]
@ -766,7 +766,8 @@ commands can be applied.
\begin{figure}[b] \begin{figure}[b]
\lstinputlisting{APPNOTE_011_Design_Investigation/primetest.v} \lstinputlisting{APPNOTE_011_Design_Investigation/primetest.v}
\caption{A simple miter circuit for testing if a number is prime} \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} \label{primetest}
\end{figure} \end{figure}
@ -869,48 +870,51 @@ corresponding input values. For Example:
\end{verbatim} \end{verbatim}
} }
Note that the {\tt sat} command support signal names in both arguments 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 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 to constraint {\tt s1} and {\tt s2} to be equal. When more complex
constraints are needed, a wrapper circuit must be constructed that constraints are needed, a wrapper circuit must be constructed that
checks the constraints and signals if the constraint was met using an 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 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 -set} option. (Such a circuit that contains the circuit under test
plus additional constraint checking circuitry is called a {\tt miter\/} plus additional constraint checking circuitry is called a {\it miter\/}
circuit.) circuit.)
Fig.~\ref{primetest} shows a miter circuit that is supposed to be used as a 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} 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. 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} demonstrate that SAT The Yosys shell session shown in Fig.~\ref{primesat} demonstrates that SAT
solvers can even find the unexpected solutions to a problem: Using integer solvers can even find the unexpected solutions to a problem: Using integer
overflow there actually is a way of "`factorizing"' 31. A solution would of overflow there actually is a way of ``factorizing'' 31. The clean solution
course be to perform the test in 32 bits, for example by replacing {\tt would of course be to perform the test in 32 bits, for example by replacing
p != a*b} in the miter with {\tt p != \{16'd0,a\}*b}. But as 31 fits well into {\tt p != a*b} in the miter with {\tt p != \{16'd0,a\}*b}, or by using a
8 bits, we can also simply force the upper 8 bits of {\tt a} and {\tt b} temporary variable for the 32 bit product {\tt a*b}. But as 31 fits well into
to zero, as is done in the second command in Fig.~\ref{primesat}. 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 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 tries to find a case in which the two arguments are not equal. If such a case is
not found, the property proven to hold for all inputs that satisfy the other not found, the property is proven to hold for all inputs that satisfy the other
constraints. constraints.
It might be worth noting, that SAT solvers are not particularly efficient at It might be worth noting, that SAT solvers are not particularly efficient at
factorizing large numbers. But if a small factorization problem occurs as factorizing large numbers. But if a small factorization problem occurs as
part of a larger circuit problem, the Yosys SAT solver is perfectly capable part of a larger circuit problem, the Yosys SAT solver is perfectly capable
of solving it. This can, for example, be an issue when using SAT solvers of solving it.
to prove the correct behavior of ALU circuits.
\subsection{Solving sequential SAT problems} \subsection{Solving sequential SAT problems}
\begin{figure}[t] \begin{figure}[t!]
\begin{lstlisting}[basicstyle=\ttfamily\scriptsize] \begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
yosys [memdemo]> sat -seq 6 -show y -show d -set-init-undef \ yosys [memdemo]> sat -seq 6 -show y -show d -set-init-undef \
-set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3 -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 Full command line: sat -seq 6 -show y -show d -set-init-undef
-set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3 -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3
Setting up time step 1: Setting up time step 1:
Final constraint equation: { } = { } Final constraint equation: { } = { }
@ -947,6 +951,7 @@ Import show expression: \y
Import show expression: \d Import show expression: \d
Solving problem with 10322 variables and 27881 clauses.. Solving problem with 10322 variables and 27881 clauses..
SAT model found. maximizing number of undefs.
SAT solving finished - model found: SAT solving finished - model found:
Time Signal Name Dec Hex Bin Time Signal Name Dec Hex Bin
@ -974,7 +979,7 @@ SAT solving finished - model found:
5 \d -- -- 001x 5 \d -- -- 001x
5 \y 2 2 0010 5 \y 2 2 0010
---- -------------------- ---------- ---------- --------------- ---- -------------------- ---------- ---------- ---------------
6 \d 1 1 0001 6 \d -- -- xxxx
6 \y 3 3 0011 6 \y 3 3 0011
\end{lstlisting} \end{lstlisting}
\caption{Solving a sequential SAT problem in the {\tt memdemo} module from Fig.~\ref{memdemo_src}.} \caption{Solving a sequential SAT problem in the {\tt memdemo} module from Fig.~\ref{memdemo_src}.}
@ -990,8 +995,8 @@ Fig.~\ref{memdemo_sat} show the solution to this question, as produced by
the following command: the following command:
\begin{verbatim} \begin{verbatim}
sat -seq 6 -show y -show d -set-init-undef \ sat -seq 6 -show y -show d -set-init-undef \
-set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3 -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3
\end{verbatim} \end{verbatim}
The {\tt -seq 6} option instructs the {\tt sat} command to solve a sequential The {\tt -seq 6} option instructs the {\tt sat} command to solve a sequential
@ -1004,13 +1009,17 @@ 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 is treated in Verilog will ensure that the solution will work for any
initial state. 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} 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. 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 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 this is the only way of setting the {\tt s1} and {\tt s2} registers to a known
value. The other options are a bit more difficult to work out manually, but value. The input values for the other steps are a bit harder to work out
the SAT solver finds the correct solution in an instant. manually, but the SAT solver finds the correct solution in an instant.
\medskip \medskip
@ -1027,14 +1036,14 @@ 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 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 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 Yosys provides commands that can be used to further inspect the behavior of the
circuit, either by evaluating which outputs are generated from certain inputs circuit, either by evaluating which output values are generated from certain input values
({\tt eval}) or by evaluation which inputs and initial conditions can result ({\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 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 to prove (or disprove) theorems regarding the circuit, in more advanced cases
with the additional help of a miter circuit. with the additional help of a miter circuit.
This features can be powerful tools, for the circuit designer using Yosys as a 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 utility for building circuits and the software developer using Yosys as a
framework for new algorithms alike. framework for new algorithms alike.
\begin{thebibliography}{9} \begin{thebibliography}{9}
@ -1043,13 +1052,6 @@ framework for new algorithms alike.
Clifford Wolf. The Yosys Open SYnthesis Suite. Clifford Wolf. The Yosys Open SYnthesis Suite.
\url{http://www.clifford.at/yosys/} \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} \bibitem{graphviz}
Graphviz - Graph Visualization Software. Graphviz - Graph Visualization Software.
\url{http://www.graphviz.org/} \url{http://www.graphviz.org/}