3 % http://ftp.univie.ac.at/packages/tex/macros/latex/contrib/IEEEtran/IEEEtran_HOWTO.pdf
4 \documentclass[9pt,technote,
a4paper]{IEEEtran
}
6 \usepackage[T1]{fontenc} % required for luximono!
7 \usepackage[scaled=
0.8]{luximono
} % typewriter font with bold face
9 % To install the luximono font files:
10 % getnonfreefonts-sys --all or
11 % getnonfreefonts-sys luximono
13 % when there are trouble you might need to:
14 % - Create /etc/texmf/updmap.d/99local-luximono.cfg
15 % containing the single line: Map ul9.map
16 % - Run update-updmap followed by mktexlsr and updmap-sys
18 % This commands must be executed as root with a root environment
19 % (i.e. run "sudo su" and then execute the commands in the root
20 % shell, don't just prefix the commands with "sudo").
22 \usepackage[unicode,bookmarks=false
]{hyperref
}
23 \usepackage[english
]{babel
}
24 \usepackage[utf8
]{inputenc}
33 \usepackage{algpseudocode
}
45 \usetikzlibrary{arrows
}
46 \usetikzlibrary{scopes
}
47 \usetikzlibrary{through
}
48 \usetikzlibrary{shapes.geometric
}
50 \def\FIXME{{\color{red
}\bf FIXME
}}
52 \lstset{basicstyle=
\ttfamily,frame=trBL,xleftmargin=
0.7cm,xrightmargin=
0.2cm,numbers=left
}
56 \title{Yosys Application Note
011: \\ Interactive Design Investigation
}
57 \author{Clifford Wolf \\ Original Version December
2013}
61 Yosys
\cite{yosys
} can be a great environment for building custom synthesis
62 flows. It can also be an excellent tool for teaching and learning Verilog based
63 RTL synthesis. In both applications it is of great importance to be able to
64 analyze the designs it produces easily.
66 This Yosys application note covers the generation of circuit diagrams with the
67 Yosys
{\tt show
} command, the selection of interesting parts of the circuit
68 using the
{\tt select
} command, and briefly discusses advanced investigation
69 commands for evaluating circuits and solving SAT problems.
72 \section{Installation and Prerequisites
}
74 This Application Note is based on the Yosys
\cite{yosys
} GIT Rev.
{\tt 2b90ba1
} from
75 2013-
12-
08. The
{\tt README
} file covers how to install Yosys. The
76 {\tt show
} command requires a working installation of GraphViz
\cite{graphviz
}
77 and
\cite{xdot
} for generating the actual circuit diagrams.
81 This application note is structured as follows:
83 Sec.~
\ref{intro_show
} introduces the
{\tt show
} command and explains the
84 symbols used in the circuit diagrams generated by it.
86 Sec.~
\ref{navigate
} introduces additional commands used to navigate in the
87 design, select portions of the design, and print additional information on
88 the elements in the design that are not contained in the circuit diagrams.
90 Sec.~
\ref{poke
} introduces commands to evaluate the design and solve SAT
91 problems within the design.
93 Sec.~
\ref{conclusion
} concludes the
document and summarizes the key points.
95 \section{Introduction to the
{\tt show
} command
}
101 read_verilog example.v
109 module example(input clk, a, b, c,
111 always @(posedge clk)
113 y <= c ? a + b :
2'd0;
116 \caption{Yosys script with
{\tt show
} commands and example design
}
121 \includegraphics[width=
\linewidth]{APPNOTE_011_Design_Investigation/example_00.pdf
}
122 \includegraphics[width=
\linewidth]{APPNOTE_011_Design_Investigation/example_01.pdf
}
123 \includegraphics[width=
\linewidth]{APPNOTE_011_Design_Investigation/example_02.pdf
}
124 \caption{Output of the three
{\tt show
} commands from Fig.~
\ref{example_src
}}
128 The
{\tt show
} command generates a circuit diagram for the design in its
129 current state. Various options can be used to change the appearance of the
130 circuit diagram, set the name and format for the output file, and so forth.
131 When called without any special options, it saves the circuit diagram in
132 a temporary file and launches
{\tt xdot
} to display the diagram.
133 Subsequent calls to
{\tt show
} re-use the
{\tt xdot
} instance
136 \subsection{A simple circuit
}
138 Fig.~
\ref{example_src
} shows a simple synthesis script and a Verilog file that
139 demonstrate the usage of
{\tt show
} in a simple setting. Note that
{\tt show
}
140 is called with the
{\tt -pause
} option, that halts execution of the Yosys
141 script until the user presses the Enter key. The
{\tt show -pause
} command
142 also allows the user to enter an interactive shell to further investigate the
143 circuit before continuing synthesis.
145 So this script, when executed, will show the design after each of the three
146 synthesis commands. The generated circuit diagrams are shown in Fig.~
\ref{example_out
}.
148 The first diagram (from top to bottom) shows the design directly after being
149 read by the Verilog front-end. Input and output ports are displayed as
150 octagonal shapes. Cells are displayed as rectangles with inputs on the left
151 and outputs on the right side. The cell labels are two lines long: The first line
152 contains a unique identifier for the cell and the second line contains the cell
153 type. Internal cell types are prefixed with a dollar sign. The Yosys manual
154 contains a chapter on the internal cell library used in Yosys.
156 Constants are shown as ellipses with the constant value as label. The syntax
157 {\tt <bit
\_width>'<bits>
} is used for for constants that are not
32-bit wide
158 and/or contain bits that are not
0 or
1 (i.e.
{\tt x
} or
{\tt z
}). Ordinary
159 32-bit constants are written using decimal numbers.
161 Single-bit signals are shown as thin arrows pointing from the driver to the
162 load. Signals that are multiple bits wide are shown as think arrows.
164 Finally
{\it processes\/
} are shown in boxes with round corners. Processes
165 are Yosys' internal representation of the decision-trees and synchronization
166 events modelled in a Verilog
{\tt always
}-block. The label reads
{\tt PROC
}
167 followed by a unique identifier in the first line and contains the source code
168 location of the original
{\tt always
}-block in the
2nd line. Note how the
169 multiplexer from the
{\tt ?:
}-expression is represented as a
{\tt \$mux
} cell
170 but the multiplexer from the
{\tt if
}-statement is yet still hidden within the
175 The
{\tt proc
} command transforms the process from the first diagram into a
176 multiplexer and a d-type flip-flip, which brings us to the
2nd diagram.
178 The Rhombus shape to the right is a dangling wire. (Wire nodes are only shown
179 if they are dangling or have ``public'' names, for example names assigned from
180 the Verilog input.) Also note that the design now contains two instances of a
181 {\tt BUF
}-node. This are artefacts left behind by the
{\tt proc
}-command. It is
182 quite usual to see such artefacts after calling commands that perform changes
183 in the design, as most commands only care about doing the transformation in the
184 least complicated way, not about cleaning up after them. The next call to
{\tt
185 clean
} (or
{\tt opt
}, which includes
{\tt clean
} as one of its operations) will
186 clean up this artefacts. This operation is so common in Yosys scripts that it
187 can simply be abbreviated with the
{\tt ;;
} token, which doubles as
188 separator for commands. Unless one wants to specifically analyze this artefacts
189 left behind some operations, it is therefore recommended to always call
{\tt clean
}
190 before calling
{\tt show
}.
194 In this script we directly call
{\tt opt
} as next step, which finally leads us to
195 the
3rd diagram in Fig.~
\ref{example_out
}. Here we see that the
{\tt opt
} command
196 not only has removed the artifacts left behind by
{\tt proc
}, but also determined
197 correctly that it can remove the first
{\tt \$mux
} cell without changing the behavior
201 \includegraphics[width=
\linewidth,trim=
0 2cm
0 0]{APPNOTE_011_Design_Investigation/splice.pdf
}
202 \caption{Output of
{\tt yosys -p 'proc; opt; show' splice.v
}}
207 \lstinputlisting{APPNOTE_011_Design_Investigation/splice.v
}
208 \caption{\tt splice.v
}
213 \includegraphics[height=
\linewidth]{APPNOTE_011_Design_Investigation/cmos_00.pdf
}
214 \includegraphics[width=
\linewidth]{APPNOTE_011_Design_Investigation/cmos_01.pdf
}
215 \caption{Effects of
{\tt splitnets
} command and of providing a cell library. (The
216 circuit is a half-adder built from simple CMOS gates.)
}
217 \label{splitnets_libfile
}
220 \subsection{Break-out boxes for signal vectors
}
222 As has been indicated by the last example, Yosys is can manage signal vectors (aka.
223 multi-bit wires or buses) as native objects. This provides great advantages
224 when analyzing circuits that operate on wide integers. But it also introduces
225 some additional complexity when the individual bits of of a signal vector
226 are accessed. The example show in Fig.~
\ref{splice_dia
} and
\ref{splice_src
}
227 demonstrates how such circuits are visualized by the
{\tt show
} command.
229 The key elements in understanding this circuit diagram are of course the boxes
230 with round corners and rows labeled
{\tt <MSB
\_LEFT>:<LSB
\_LEFT> -- <MSB
\_RIGHT>:<LSB
\_RIGHT>
}.
231 Each of this boxes has one signal per row on one side and a common signal for all rows on the
232 other side. The
{\tt <MSB>:<LSB>
} tuples specify which bits of the signals are broken out
233 and connected. So the top row of the box connecting the signals
{\tt a
} and
{\tt x
} indicates
234 that the bit
0 (i.e. the range
0:
0) from signal
{\tt a
} is connected to bit
1 (i.e. the range
235 1:
1) of signal
{\tt x
}.
237 Lines connecting such boxes together and lines connecting such boxes to cell
238 ports have a slightly different look to emphasise that they are not actual signal
239 wires but a necessity of the graphical representation. This distinction seems
240 like a technicality, until one wants to debug a problem related to the way
241 Yosys internally represents signal vectors, for example when writing custom
244 \subsection{Gate level netlists
}
246 Finally Fig.~
\ref{splitnets_libfile
} shows two common pitfalls when working
247 with designs mapped to a cell library. The top figure has two problems: First
248 Yosys did not have access to the cell library when this diagram was generated,
249 resulting in all cell ports defaulting to being inputs. This is why all ports
250 are drawn on the left side the cells are awkwardly arranged in a large column.
251 Secondly the two-bit vector
{\tt y
} requires breakout-boxes for its individual
252 bits, resulting in an unnecessary complex diagram.
254 For the
2nd diagram Yosys has been given a description of the cell library as
255 Verilog file containing blackbox modules. There are two ways to load cell
256 descriptions into Yosys: First the Verilog file for the cell library can be
257 passed directly to the
{\tt show
} command using the
{\tt -lib <filename>
}
258 option. Secondly it is possible to load cell libraries into the design with
259 the
{\tt read
\_verilog -lib <filename>
} command. The
2nd method has the great
260 advantage that the library only needs to be loaded once and can then be used
261 in all subsequent calls to the
{\tt show
} command.
263 In addition to that, the
2nd diagram was generated after
{\tt splitnet -ports
}
264 was run on the design. This command splits all signal vectors into individual
265 signal bits, which is often desirable when looking at gate-level circuits. The
266 {\tt -ports
} option is required to also split module ports. Per default the
267 command only operates on interior signals.
269 \subsection{Miscellaneous notes
}
271 Per default the
{\tt show
} command outputs a temporary
{\tt dot
} file and launches
272 {\tt xdot
} to display it. The options
{\tt -format
},
{\tt -viewer
}
273 and
{\tt -prefix
} can be used to change format, viewer and filename prefix.
274 Note that the
{\tt pdf
} and
{\tt ps
} format are the only formats that support
275 plotting multiple modules in one run.
277 In densely connected circuits it is sometimes hard to keep track of the
278 individual signal wires. For this cases it can be useful to call
{\tt show
}
279 with the
{\tt -colors <integer>
} argument, which randomly assigns colors to the
280 nets. The integer (>
0) is used as seed value for the random
color
281 assignments. Sometimes it is necessary it try some values to find an assignment
282 of colors that looks good.
284 The command
{\tt help show
} prints a complete listing of all options supported
285 by the
{\tt show
} command.
287 \section{Navigating the design
}
290 Plotting circuit diagrams for entire modules in the design brings us only helps
291 in simple cases. For complex modules the generated circuit diagrams are just stupidly big
292 and are no help at all. In such cases one first has to select the relevant
293 portions of the circuit.
295 In addition to
{\it what\/
} to display one also needs to carefully decide
296 {\it when\/
} to display it, with respect to the synthesis flow. In general
297 it is a good idea to troubleshoot a circuit in the earliest state in which
298 a problem can be reproduced. So if, for example, the internal state before calling
299 the
{\tt techmap
} command already fails to verify, it is better to troubleshoot
300 the coarse-grain version of the circuit before
{\tt techmap
} than the gate-level
301 circuit after
{\tt techmap
}.
305 Note: It is generally recommended to verify the internal state of a design by
306 writing it to a Verilog file using
{\tt write
\_verilog -noexpr
} and using the
307 simulation models from
{\tt simlib.v
} and
{\tt simcells.v
} from the Yosys data
308 directory (as printed by
{\tt yosys-config -
{}-datdir
}).
310 \subsection{Interactive Navigation
}
337 \caption{Demonstration of
{\tt ls
} and
{\tt cd
} using
{\tt example.v
} from Fig.~
\ref{example_src
}}
343 attribute
\src "example.v:
5"
344 cell $add $add$example.v:
5$
2
345 parameter
\A_SIGNED 0
347 parameter
\B_SIGNED 0
352 connect
\Y $add$example.v:
5$
2_Y
355 \caption{Output of
{\tt dump \$
2} using the design from Fig.~
\ref{example_src
} and Fig.~
\ref{example_out
}}
359 Once the right state within the synthesis flow for debugging the circuit has
360 been identified, it is recommended to simply add the
{\tt shell
} command
361 to the matching place in the synthesis script. This command will stop the
362 synthesis at the specified moment and go to shell mode, where the user can
363 interactively enter commands.
365 For most cases, the shell will start with the whole design selected (i.e. when
366 the synthesis script does not already narrow the selection). The command
{\tt
367 ls
} can now be used to create a list of all modules. The command
{\tt cd
} can
368 be used to switch to one of the modules (type
{\tt cd ..
} to switch back). Now
369 the
{\tt ls
} command lists the objects within that module. Fig.~
\ref{lscd
}
370 demonstrates this using the design from Fig.~
\ref{example_src
}.
372 There is a thing to note in Fig.~
\ref{lscd
}: We can see that the cell names
373 from Fig.~
\ref{example_out
} are just abbreviations of the actual cell names,
374 namely the part after the last dollar-sign. Most auto-generated names (the ones
375 starting with a dollar sign) are rather long and contains some additional
376 information on the origin of the named object. But in most cases those names
377 can simply be abbreviated using the last part.
379 Usually all interactive work is done with one module selected using the
{\tt cd
}
380 command. But it is also possible to work from the design-context (
{\tt cd ..
}). In
381 this case all object names must be prefixed with
{\tt <module
\_name>/
}. For
382 example
{\tt a*/b*
} would refer to all objects whose names start with
{\tt b
} from
383 all modules whose names start with
{\tt a
}.
385 The
{\tt dump
} command can be used to print all information about an object.
386 For example
{\tt dump \$
2} will print Fig.~
\ref{dump2
}. This can for example
387 be useful to determine the names of nets connected to cells, as the net-names
388 are usually suppressed in the circuit diagram if they are auto-generated.
390 For the remainder of this
document we will assume that the commands are run from
391 module-context and not design-context.
393 \subsection{Working with selections
}
396 \includegraphics[width=
\linewidth]{APPNOTE_011_Design_Investigation/example_03.pdf
}
397 \caption{Output of
{\tt show
} after
{\tt select \$
2} or
{\tt select t:\$add
}
398 (see also Fig.~
\ref{example_out
})
}
402 When a module is selected using the
{\tt cd
} command, all commands (with a few
403 exceptions, such as the
{\tt read
\_*
} and
{\tt write
\_*
} commands) operate
404 only on the selected module. This can also be useful for synthesis scripts
405 where different synthesis strategies should be applied to different modules
408 But for most interactive work we want to further narrow the set of selected
409 objects. This can be done using the
{\tt select
} command.
411 For example, if the command
{\tt select \$
2} is executed, a subsequent
{\tt show
}
412 command will yield the diagram shown in Fig.~
\ref{seladd
}. Note that the nets are
413 now displayed in ellipses. This indicates that they are not selected, but only
414 shown because the diagram contains a cell that is connected to the net. This
415 of course makes no difference for the circuit that is shown, but it can be a useful
416 information when manipulating selections.
418 Objects can not only be selected by their name but also by other properties.
419 For example
{\tt select t:\$add
} will select all cells of type
{\tt \$add
}. In
420 this case this is also yields the diagram shown in Fig.~
\ref{seladd
}.
423 \lstinputlisting{APPNOTE_011_Design_Investigation/foobaraddsub.v
}
424 \caption{Test module for operations on selections
}
428 The output of
{\tt help select
} contains a complete syntax reference for
429 matching different properties.
431 Many commands can operate on explicit selections. For example the command
{\tt
432 dump t:\$add
} will print information on all
{\tt \$add
} cells in the active
433 module. Whenever a command has
{\tt [selection
]} as last argument in its usage
434 help, this means that it will use the engine behind the
{\tt select
} command
435 to evaluate additional arguments and use the resulting selection instead of
436 the selection created by the last
{\tt select
} command.
438 Normally the
{\tt select
} command overwrites a previous selection. The
439 commands
{\tt select -add
} and
{\tt select -del
} can be used to add
440 or remove objects from the current selection.
442 The command
{\tt select -clear
} can be used to reset the selection to the
443 default, which is a complete selection of everything in the current module.
445 \subsection{Operations on selections
}
448 \lstinputlisting{APPNOTE_011_Design_Investigation/sumprod.v
}
449 \caption{Another test module for operations on selections
}
454 \includegraphics[width=
\linewidth]{APPNOTE_011_Design_Investigation/sumprod_00.pdf
}
455 \caption{Output of
{\tt show a:sumstuff
} on Fig.~
\ref{sumprod
}}
459 The
{\tt select
} command is actually much more powerful than it might seem on
460 the first glimpse. When it is called with multiple arguments, each argument is
461 evaluated and pushed separately on a stack. After all arguments have been
462 processed it simply creates the union of all elements on the stack. So the
463 following command will select all
{\tt \$add
} cells and all objects with
464 the
{\tt foo
} attribute set:
470 (Try this with the design shown in Fig.~
\ref{foobaraddsub
}. Use the
{\tt
471 select -list
} command to list the current selection.)
473 In many cases simply adding more and more stuff to the selection is an
474 ineffective way of selecting the interesting part of the design. Special
475 arguments can be used to combine the elements on the stack.
476 For example the
{\tt \%i
} arguments pops the last two elements from
477 the stack, intersects them, and pushes the result back on the stack. So the
478 following command will select all
{\$add
} cells that have the
{\tt foo
}
482 select t:$add a:foo
%i
485 The listing in Fig.~
\ref{sumprod
} uses the Yosys non-standard
{\tt \
{* ... *\
}}
486 syntax to set the attribute
{\tt sumstuff
} on all cells generated by the first
487 assign statement. (This works on arbitrary large blocks of Verilog code an
488 can be used to mark portions of code for analysis.)
490 Selecting
{\tt a:sumstuff
} in this module will yield the circuit diagram shown
491 in Fig.~
\ref{sumprod_00
}. As only the cells themselves are selected, but not
492 the temporary wire
{\tt \$
1\_Y}, the two adders are shown as two disjunct
493 parts. This can be very useful for global signals like clock and reset signals: just
494 unselect them using a command such as
{\tt select -del clk rst
} and each cell
495 using them will get its own net label.
497 In this case however we would like to see the cells connected properly. This
498 can be achieved using the
{\tt \%x
} action, that broadens the selection, i.e.
499 for each selected wire it selects all cells connected to the wire and vice
500 versa. So
{\tt show a:sumstuff \%x
} yields the diagram shown in Fig.~
\ref{sumprod_01
}.
503 \includegraphics[width=
\linewidth]{APPNOTE_011_Design_Investigation/sumprod_01.pdf
}
504 \caption{Output of
{\tt show a:sumstuff \%x
} on Fig.~
\ref{sumprod
}}
508 \subsection{Selecting logic cones
}
510 Fig.~
\ref{sumprod_01
} shows what is called the
{\it input cone\/
} of
{\tt sum
}, i.e.
511 all cells and signals that are used to generate the signal
{\tt sum
}. The
{\tt \%ci
}
512 action can be used to select the input cones of all object in the top selection
513 in the stack maintained by the
{\tt select
} command.
515 As the
{\tt \%x
} action, this commands broadens the selection by one ``step''. But
516 this time the operation only works against the direction of data flow. That means,
517 wires only select cells via output ports and cells only select wires via input ports.
519 Fig.~
\ref{select_prod
} show the sequence of diagrams generated by the following
526 show prod
%ci %ci %ci
529 When selecting many levels of logic, repeating
{\tt \%ci
} over and over again
530 can be a bit dull. So there is a shortcut for that: the number of iterations
531 can be appended to the action. So for example the action
{\tt \%ci3
} is
532 identical to performing the
{\tt \%ci
} action three times.
534 The action
{\tt \%ci*
} performs the
{\tt \%ci
} action over and over again until
535 it has no effect anymore.
538 \hfill \includegraphics[width=
4cm,trim=
0 1cm
0 1cm
]{APPNOTE_011_Design_Investigation/sumprod_02.pdf
} \\
539 \includegraphics[width=
\linewidth,trim=
0 0cm
0 1cm
]{APPNOTE_011_Design_Investigation/sumprod_03.pdf
} \\
540 \includegraphics[width=
\linewidth,trim=
0 0cm
0 1cm
]{APPNOTE_011_Design_Investigation/sumprod_04.pdf
} \\
541 \includegraphics[width=
\linewidth,trim=
0 2cm
0 1cm
]{APPNOTE_011_Design_Investigation/sumprod_05.pdf
} \\
542 \caption{Objects selected by
{\tt select prod \%ci...
}}
548 In most cases there are certain cell types and/or ports that should not be considered for the
{\tt \%ci
}
549 action, or we only want to follow certain cell types and/or ports. This can be achieved using additional
550 patterns that can be appended to the
{\tt \%ci
} action.
552 Lets consider the design from Fig.~
\ref{memdemo_src
}. It serves no purpose other than being a non-trivial
553 circuit for demonstrating some of the advanced Yosys features. We synthesize the circuit using
{\tt proc;
554 opt; memory; opt
} and change to the
{\tt memdemo
} module with
{\tt cd memdemo
}. If we type
{\tt show
}
555 now we see the diagram shown in Fig.~
\ref{memdemo_00
}.
558 \lstinputlisting{APPNOTE_011_Design_Investigation/memdemo.v
}
559 \caption{Demo circuit for demonstrating some advanced Yosys features
}
564 \includegraphics[width=
\linewidth,trim=
0 0cm
0 0cm
]{APPNOTE_011_Design_Investigation/memdemo_00.pdf
} \\
565 \caption{Complete circuit diagram for the design shown in Fig.~
\ref{memdemo_src
}}
569 But maybe we are only interested in the tree of multiplexers that select the
570 output value. In order to get there, we would start by just showing the output signal
571 and its immediate predecessors:
577 From this we would learn that
{\tt y
} is driven by a
{\tt \$dff cell
}, that
578 {\tt y
} is connected to the output port
{\tt Q
}, that the
{\tt clk
} signal goes
579 into the
{\tt CLK
} input port of the cell, and that the data comes from a
580 auto-generated wire into the input
{\tt D
} of the flip-flop cell.
582 As we are not interested in the clock signal we add an additional pattern to the
{\tt \%ci
}
583 action, that tells it to only follow ports
{\tt Q
} and
{\tt D
} of
{\tt \$dff
} cells:
586 show y
%ci2:+$dff[Q,D]
589 To add a pattern we add a colon followed by the pattern to the
{\tt \%ci
}
590 action. The pattern it self starts with
{\tt -
} or
{\tt +
}, indicating if it is
591 an include or exclude pattern, followed by an optional comma separated list
592 of cell types, followed by an optional comma separated list of port names in
595 Since we know that the only cell considered in this case is a
{\tt \$dff
} cell,
596 we could as well only specify the port names:
602 Or we could decide to tell the
{\tt \%ci
} action to not follow the
{\tt CLK
} input:
609 \includegraphics[width=
\linewidth,trim=
0 0cm
0 0cm
]{APPNOTE_011_Design_Investigation/memdemo_01.pdf
} \\
610 \caption{Output of
{\tt show y \%ci2:+\$dff
[Q,D
] \%ci*:-\$mux
[S
]:-\$dff
}}
614 Next we would investigate the next logic level by adding another
{\tt \%ci2
} to
618 show y
%ci2:-[CLK] %ci2
621 From this we would learn that the next cell is a
{\tt \$mux
} cell and we would add additional
622 pattern to narrow the selection on the path we are interested. In the end we would end up
623 with a command such as
626 show y
%ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff
629 in which the first
{\tt \%ci
} jumps over the initial d-type flip-flop and the
630 2nd action selects the entire input cone without going over multiplexer select
631 inputs and flip-flop cells. The diagram produces by this command is shown in
632 Fig.~
\ref{memdemo_01
}.
636 Similar to
{\tt \%ci
} exists an action
{\tt \%co
} to select output cones that
637 accepts the same syntax for pattern and repetition. The
{\tt \%x
} action mentioned
638 previously also accepts this advanced syntax.
640 This actions for traversing the circuit graph, combined with the actions for
641 boolean operations such as intersection (
{\tt \%i
}) and difference (
{\tt \%d
})
642 are powerful tools for extracting the relevant portions of the circuit under
645 See
{\tt help select
} for a complete list of actions available in selections.
647 \subsection{Storing and recalling selections
}
649 The current selection can be stored in memory with the command
{\tt select -set
650 <name>
}. It can later be recalled using
{\tt select @<name>
}. In fact, the
{\tt
651 @<name>
} expression pushes the stored selection on the stack maintained by the
652 {\tt select
} command. So for example
658 will select the intersection between the stored selections
{\tt foo
} and
{\tt bar
}.
662 In larger investigation efforts it is highly recommended to maintain a script that
663 sets up relevant selections, so they can easily be recalled, for example when
664 Yosys needs to be re-run after a design or source code change.
666 The
{\tt history
} command can be used to list all recent interactive commands.
667 This feature can be useful for creating such a script from the commands used in
668 an interactive session.
670 \section{Advanced investigation techniques
}
673 When working with very large modules, it is often not enough to just select the
674 interesting part of the module. Instead it can be useful to extract the
675 interesting part of the circuit into a separate module. This can for example be
676 useful if one wants to run a series of synthesis commands on the critical part
677 of the module and wants to carefully read all the debug output created by the
678 commands in order to spot a problem. This kind of troubleshooting is much easier
679 if the circuit under investigation is encapsulated in a separate module.
681 Fig.~
\ref{submod
} shows how the
{\tt submod
} command can be used to split the
682 circuit from Fig.~
\ref{memdemo_src
} and
\ref{memdemo_00
} into its components.
683 The
{\tt -name
} option is used to specify the name of the new module and
684 also the name of the new cell in the current module.
687 \includegraphics[width=
\linewidth,trim=
0 1.3cm
0 0cm
]{APPNOTE_011_Design_Investigation/submod_00.pdf
} \\
\centerline{\tt memdemo
} \vskip1em\par
688 \includegraphics[width=
\linewidth,trim=
0 1.3cm
0 0cm
]{APPNOTE_011_Design_Investigation/submod_01.pdf
} \\
\centerline{\tt scramble
} \vskip1em\par
689 \includegraphics[width=
\linewidth,trim=
0 1.3cm
0 0cm
]{APPNOTE_011_Design_Investigation/submod_02.pdf
} \\
\centerline{\tt outstage
} \vskip1em\par
690 \includegraphics[width=
\linewidth,trim=
0 1.3cm
0 0cm
]{APPNOTE_011_Design_Investigation/submod_03.pdf
} \\
\centerline{\tt selstage
} \vskip1em\par
691 \begin{lstlisting
}[basicstyle=
\ttfamily\scriptsize]
692 select -set outstage y
%ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff
693 select -set selstage y
%ci2:+$dff[Q,D] %ci*:-$dff @outstage %d
694 select -set scramble mem*
%ci2 %ci*:-$dff mem* %d @selstage %d
695 submod -name scramble @scramble
696 submod -name outstage @outstage
697 submod -name selstage @selstage
699 \caption{The circuit from Fig.~
\ref{memdemo_src
} and
\ref{memdemo_00
} broken up using
{\tt submod
}}
703 \subsection{Evaluation of combinatorial circuits
}
705 The
{\tt eval
} command can be used to evaluate combinatorial circuits.
706 For example (see Fig.~
\ref{submod
} for the circuit diagram of
{\tt selstage
}):
710 yosys
[selstage
]> eval -set s2,s1
4'b1001 -set d
4'hc -show n2 -show n1
712 9. Executing EVAL pass (evaluate the circuit given an input).
713 Full command line: eval -set s2,s1
4'b1001 -set d
4'hc -show n2 -show n1
714 Eval result:
\n2 =
2'
10.
715 Eval result:
\n1 =
2'
10.
719 So the
{\tt -set
} option is used to set input values and the
{\tt -show
} option
720 is used to specify the nets to evaluate. If no
{\tt -show
} option is specified,
721 all selected output ports are used per default.
723 If a necessary input value is not given, an error is produced. The option
724 {\tt -set-undef
} can be used to instead set all unspecified input nets to
727 The
{\tt -table
} option can be used to create a truth table. For example:
731 yosys
[selstage
]> eval -set-undef -set d
[3:
1] 0 -table s1,d
[0]
733 10. Executing EVAL pass (evaluate the circuit given an input).
734 Full command line: eval -set-undef -set d
[3:
1] 0 -table s1,d
[0]
737 ---- ------ | ---- ----
747 Assumed undef (x) value for the following signals:
\s2
751 Note that the
{\tt eval
} command (as well as the
{\tt sat
} command discussed in
752 the next sections) does only operate on flattened modules. It can not analyze
753 signals that are passed through design hierarchy levels. So the
{\tt flatten
}
754 command must be used on modules that instantiate other modules before this
755 commands can be applied.
757 \subsection{Solving combinatorial SAT problems
}
760 \lstinputlisting{APPNOTE_011_Design_Investigation/primetest.v
}
761 \caption{A simple miter circuit for testing if a number is prime. But it has a
762 problem (see main text and Fig.~
\ref{primesat
}).
}
767 \begin{lstlisting
}[basicstyle=
\ttfamily\small]
768 yosys
[primetest
]> sat -prove ok
1 -set p
31
770 8. Executing SAT pass (solving SAT problems in the circuit).
771 Full command line: sat -prove ok
1 -set p
31
773 Setting up SAT problem:
774 Import set-constraint:
\p =
16'
0000000000011111
775 Final constraint equation:
\p =
16'
0000000000011111
776 Imported
6 cells to SAT database.
777 Import proof-constraint:
\ok =
1'
1
778 Final proof equation:
\ok =
1'
1
780 Solving problem with
2790 variables and
8241 clauses..
781 SAT proof finished - model found: FAIL!
783 ______ ___ ___ _ _ _ _
784 (_____ \ / __) / __) (_) | | | |
785 _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |
786 | ____/ ___) _ \ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|
787 | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_
788 |_| |_|
\___/
\___/ |_| |_|
\_____|_|
\_)_____)
\____|_|
791 Signal Name Dec Hex Bin
792 -------------------- ---------- ---------- ---------------------
793 \a 15029 3ab5
0011101010110101
794 \b 4099 1003 0001000000000011
796 \p 31 1f
0000000000011111
798 yosys
[primetest
]> sat -prove ok
1 -set p
31 -set a
[15:
8],b
[15:
8] 0
800 9. Executing SAT pass (solving SAT problems in the circuit).
801 Full command line: sat -prove ok
1 -set p
31 -set a
[15:
8],b
[15:
8] 0
803 Setting up SAT problem:
804 Import set-constraint:
\p =
16'
0000000000011111
805 Import set-constraint:
{ \a [15:
8] \b [15:
8] } =
16'
0000000000000000
806 Final constraint equation:
{ \a [15:
8] \b [15:
8] \p } =
{ 16'
0000000000000000 16'
0000000000011111 }
807 Imported
6 cells to SAT database.
808 Import proof-constraint:
\ok =
1'
1
809 Final proof equation:
\ok =
1'
1
811 Solving problem with
2790 variables and
8257 clauses..
812 SAT proof finished - no model found: SUCCESS!
814 /$$$$$$ /$$$$$$$$ /$$$$$$$
815 /$$__ $$ | $$_____/ | $$__ $$
816 | $$ \ $$ | $$ | $$ \ $$
817 | $$ | $$ | $$$$$ | $$ | $$
818 | $$ | $$ | $$__/ | $$ | $$
819 | $$/$$ $$ | $$ | $$ | $$
820 | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$
821 \____ $$$|__/|________/|__/|_______/|__/
824 \caption{Experiments with the miter circuit from Fig.~
\ref{primetest
}. The first attempt of proving that
31
825 is prime failed because the SAT solver found a creative way of factorizing
31 using integer overflow.
}
829 Often the opposite of the
{\tt eval
} command is needed, i.e. the circuits
830 output is given and we want to find the matching input signals. For small
831 circuits with only a few input bits this can be accomplished by trying all
832 possible input combinations, as it is done by the
{\tt eval -table
} command.
833 For larger circuits however, Yosys provides the
{\tt sat
} command that uses
834 a SAT
\cite{CircuitSAT
} solver
\cite{MiniSAT
} to solve this kind of problems.
836 The
{\tt sat
} command works very similar to the
{\tt eval
} command. The main
837 difference is that it is now also possible to set output values and find the
838 corresponding input values. For Example:
842 yosys
[selstage
]> sat -show s1,s2,d -set s1 s2 -set n2,n1
4'b1001
844 11. Executing SAT pass (solving SAT problems in the circuit).
845 Full command line: sat -show s1,s2,d -set s1 s2 -set n2,n1
4'b1001
847 Setting up SAT problem:
848 Import set-constraint:
\s1 =
\s2
849 Import set-constraint:
{ \n2 \n1 } =
4'
1001
850 Final constraint equation:
{ \n2 \n1 \s1 } =
{ 4'
1001 \s2 }
851 Imported
3 cells to SAT database.
852 Import show expression:
{ \s1 \s2 \d }
854 Solving problem with
81 variables and
207 clauses..
855 SAT solving finished - model found:
857 Signal Name Dec Hex Bin
858 -------------------- ---------- ---------- ---------------
865 Note that the
{\tt sat
} command supports signal names in both arguments
866 to the
{\tt -set
} option. In the above example we used
{\tt -set s1 s2
}
867 to constraint
{\tt s1
} and
{\tt s2
} to be equal. When more complex
868 constraints are needed, a wrapper circuit must be constructed that
869 checks the constraints and signals if the constraint was met using an
870 extra output port, which then can be forced to a value using the
{\tt
871 -set
} option. (Such a circuit that contains the circuit under test
872 plus additional constraint checking circuitry is called a
{\it miter\/
}
875 Fig.~
\ref{primetest
} shows a miter circuit that is supposed to be used as a
876 prime number test. If
{\tt ok
} is
1 for all input values
{\tt a
} and
{\tt b
}
877 for a given
{\tt p
}, then
{\tt p
} is prime, or at least that is the idea.
879 The Yosys shell session shown in Fig.~
\ref{primesat
} demonstrates that SAT
880 solvers can even find the unexpected solutions to a problem: Using integer
881 overflow there actually is a way of ``factorizing''
31. The clean solution
882 would of course be to perform the test in
32 bits, for example by replacing
883 {\tt p != a*b
} in the miter with
{\tt p != \
{16'd0,a\
}*b
}, or by using a
884 temporary variable for the
32 bit product
{\tt a*b
}. But as
31 fits well into
885 8 bits (and as the purpose of this
document is to show off Yosys features)
886 we can also simply force the upper
8 bits of
{\tt a
} and
{\tt b
} to zero for
887 the
{\tt sat
} call, as is done in the second command in Fig.~
\ref{primesat
}
890 The
{\tt -prove
} option used in this example works similar to
{\tt -set
}, but
891 tries to find a case in which the two arguments are not equal. If such a case is
892 not found, the property is proven to hold for all inputs that satisfy the other
895 It might be worth noting, that SAT solvers are not particularly efficient at
896 factorizing large numbers. But if a small factorization problem occurs as
897 part of a larger circuit problem, the Yosys SAT solver is perfectly capable
900 \subsection{Solving sequential SAT problems
}
903 \begin{lstlisting
}[basicstyle=
\ttfamily\scriptsize]
904 yosys
[memdemo
]> sat -seq
6 -show y -show d -set-init-undef \
905 -max_undef -set-at
4 y
1 -set-at
5 y
2 -set-at
6 y
3
907 6. Executing SAT pass (solving SAT problems in the circuit).
908 Full command line: sat -seq
6 -show y -show d -set-init-undef
909 -max_undef -set-at
4 y
1 -set-at
5 y
2 -set-at
6 y
3
911 Setting up time step
1:
912 Final constraint equation:
{ } =
{ }
913 Imported
29 cells to SAT database.
915 Setting up time step
2:
916 Final constraint equation:
{ } =
{ }
917 Imported
29 cells to SAT database.
919 Setting up time step
3:
920 Final constraint equation:
{ } =
{ }
921 Imported
29 cells to SAT database.
923 Setting up time step
4:
924 Import set-constraint for timestep:
\y =
4'
0001
925 Final constraint equation:
\y =
4'
0001
926 Imported
29 cells to SAT database.
928 Setting up time step
5:
929 Import set-constraint for timestep:
\y =
4'
0010
930 Final constraint equation:
\y =
4'
0010
931 Imported
29 cells to SAT database.
933 Setting up time step
6:
934 Import set-constraint for timestep:
\y =
4'
0011
935 Final constraint equation:
\y =
4'
0011
936 Imported
29 cells to SAT database.
938 Setting up initial state:
939 Final constraint equation:
{ \y \s2 \s1 \mem[3] \mem[2] \mem[1]
940 \mem[0] } =
24'xxxxxxxxxxxxxxxxxxxxxxxx
942 Import show expression:
\y
943 Import show expression:
\d
945 Solving problem with
10322 variables and
27881 clauses..
946 SAT model found. maximizing number of undefs.
947 SAT solving finished - model found:
949 Time Signal Name Dec Hex Bin
950 ---- -------------------- ---------- ---------- ---------------
951 init
\mem[0] -- -- xxxx
952 init
\mem[1] -- -- xxxx
953 init
\mem[2] -- -- xxxx
954 init
\mem[3] -- -- xxxx
958 ---- -------------------- ---------- ---------- ---------------
961 ---- -------------------- ---------- ---------- ---------------
964 ---- -------------------- ---------- ---------- ---------------
967 ---- -------------------- ---------- ---------- ---------------
970 ---- -------------------- ---------- ---------- ---------------
973 ---- -------------------- ---------- ---------- ---------------
977 \caption{Solving a sequential SAT problem in the
{\tt memdemo
} module from Fig.~
\ref{memdemo_src
}.
}
981 The SAT solver functionality in Yosys can not only be used to solve
982 combinatorial problems, but can also solve sequential problems. Let's consider
983 the entire
{\tt memdemo
} module from Fig.~
\ref{memdemo_src
} and suppose we
984 want to know which sequence of input values for
{\tt d
} will cause the output
985 {\tt y
} to produce the sequence
1,
2,
3 from any initial state.
986 Fig.~
\ref{memdemo_sat
} show the solution to this question, as produced by
987 the following command:
990 sat -seq
6 -show y -show d -set-init-undef \
991 -max_undef -set-at
4 y
1 -set-at
5 y
2 -set-at
6 y
3
994 The
{\tt -seq
6} option instructs the
{\tt sat
} command to solve a sequential
995 problem in
6 time steps. (Experiments with lower number of steps have show that
996 at least
3 cycles are necessary to bring the circuit in a state from which
997 the sequence
1,
2,
3 can be produced.)
999 The
{\tt -set-init-undef
} option tells the
{\tt sat
} command to initialize
1000 all registers to the undef (
{\tt x
}) state. The way the
{\tt x
} state
1001 is treated in Verilog will ensure that the solution will work for any
1004 The
{\tt -max
\_undef} option instructs the
{\tt sat
} command to find a solution
1005 with a maximum number of undefs. This way we can see clearly which inputs bits
1006 are relevant to the solution.
1008 Finally the three
{\tt -set-at
} options add constraints for the
{\tt y
}
1009 signal to play the
1,
2,
3 sequence, starting with time step
4.
1011 It is not surprising that the solution sets
{\tt d =
0} in the first step, as
1012 this is the only way of setting the
{\tt s1
} and
{\tt s2
} registers to a known
1013 value. The input values for the other steps are a bit harder to work out
1014 manually, but the SAT solver finds the correct solution in an instant.
1018 There is much more to write about the
{\tt sat
} command. For example, there is
1019 a set of options that can be used to performs sequential proofs using temporal
1020 induction
\cite{tip
}. The command
{\tt help sat
} can be used to print a list
1021 of all options with short descriptions of their functions.
1023 \section{Conclusion
}
1026 Yosys provides a wide range of functions to analyze and investigate designs. For
1027 many cases it is sufficient to simply display circuit diagrams, maybe use some
1028 additional commands to narrow the scope of the circuit diagrams to the interesting
1029 parts of the circuit. But some cases require more than that. For this applications
1030 Yosys provides commands that can be used to further inspect the behavior of the
1031 circuit, either by evaluating which output values are generated from certain input values
1032 (
{\tt eval
}) or by evaluation which input values and initial conditions can result
1033 in a certain behavior at the outputs (
{\tt sat
}). The SAT command can even be used
1034 to prove (or disprove) theorems regarding the circuit, in more advanced cases
1035 with the additional help of a miter circuit.
1037 This features can be powerful tools for the circuit designer using Yosys as a
1038 utility for building circuits and the software developer using Yosys as a
1039 framework for new algorithms alike.
1041 \begin{thebibliography
}{9}
1044 Clifford Wolf. The Yosys Open SYnthesis Suite.
1045 \url{http://www.clifford.at/yosys/
}
1048 Graphviz - Graph Visualization Software.
1049 \url{http://www.graphviz.org/
}
1052 xdot.py - an interactive viewer for graphs written in Graphviz's dot language.
1053 \url{https://github.com/jrfonseca/xdot.py
}
1055 \bibitem{CircuitSAT
}
1056 {\it Circuit satisfiability problem
} on Wikipedia
1057 \url{http://en.wikipedia.org/wiki/Circuit_satisfiability
}
1060 MiniSat: a minimalistic open-source SAT solver.
1061 \url{http://minisat.se/
}
1064 Niklas Een and Niklas S\"orensson (
2003).
1065 Temporal Induction by Incremental SAT Solving.
1066 \url{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=
10.1.1.4.8161}
1068 \end{thebibliography
}