011: Interactive design investigation page¶
Installation and prerequisites¶
This Application Note is based on the Yosys GIT Rev. 2b90ba1 from
2013-12-08. The README file covers how to install Yosys. The show command
requires a working installation of GraphViz and xdot for generating the
actual circuit diagrams.
Overview¶
This application note is structured as follows:
Introduction to the show command introduces the show command and explains the symbols used
in the circuit diagrams generated by it.
Navigating the design introduces additional commands used to navigate in the design, select portions of the design, and print additional information on the elements in the design that are not contained in the circuit diagrams.
Advanced investigation techniques introduces commands to evaluate the design and solve SAT problems within the design.
Conclusion concludes the document and summarizes the key points.
Introduction to the show command¶
$ cat example.ys
read_verilog example.v
show -pause
proc
show -pause
opt
show -pause
$ cat example.v
module example(input clk, a, b, c,
output reg [1:0] y);
always @(posedge clk)
if (c)
y <= c ? a + b : 2'd0;
endmodule
The show command generates a circuit diagram for the design in its 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 xdot to display the diagram. Subsequent calls to show re-use the
xdot instance (if still running).
A simple circuit¶
Listing 5 shows a simple synthesis script and a Verilog file that
demonstrate the usage of show in a simple setting. Note that show is called with
the -pause option, that halts execution of the Yosys script until the user
presses the Enter key. The show -pause command also allows the user to enter
an interactive shell to further investigate the circuit before continuing
synthesis.
So this script, when executed, will show the design after each of the three synthesis commands. The generated circuit diagrams are shown in Fig. 1.
The first diagram (from top to bottom) shows the design directly after being 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 contains a chapter on the internal cell library used in Yosys.
Constants are shown as ellipses with the constant value as label. The syntax
<bit_width>'<bits> is used for for constants that are not 32-bit wide and/or
contain bits that are not 0 or 1 (i.e. x or z). Ordinary 32-bit
constants are written using decimal numbers.
Single-bit signals are shown as thin arrows pointing from the driver to the load. Signals that are multiple bits wide are shown as think arrows.
Finally processes are shown in boxes with round corners. Processes are Yosys’
internal representation of the decision-trees and synchronization events
modelled in a Verilog always-block. The label reads PROC followed by a
unique identifier in the first line and contains the source code location of the
original always-block in the 2nd line. Note how the multiplexer from the
?:-expression is represented as a $mux cell but the multiplexer from the
if-statement is yet still hidden within the process.
The 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.
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 the
Verilog input.) Also note that the design now contains two instances of a
BUF-node. This are artefacts left behind by the proc-command. It is
quite usual to see such artefacts after calling commands that perform changes 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
clean (or opt, which includes 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 with the ;; token, which doubles as separator for
commands. Unless one wants to specifically analyze this artefacts left behind
some operations, it is therefore recommended to always call clean before
calling show.
In this script we directly call opt as next step, which finally leads us to
the 3rd diagram in Fig. 1. Here we see that the opt command
not only has removed the artifacts left behind by proc, but also determined
correctly that it can remove the first $mux cell without changing the
behavior of the circuit.
Fig. 2 Output of yosys -p 'proc; opt; show' splice.v¶
module splice_demo(a, b, c, d, e, f, x, y);
input [1:0] a, b, c, d, e, f;
output [1:0] x = {a[0], a[1]};
output [11:0] y;
assign {y[11:4], y[1:0], y[3:2]} =
{a, b, -{c, d}, ~{e, f}};
endmodule
Fig. 3 Effects of splitnets command and of providing a cell library. (The
circuit is a half-adder built from simple CMOS gates.)¶
Break-out boxes for signal vectors¶
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 are accessed. The example show in Listing 6 demonstrates
how such circuits are visualized by the show command.
The key elements in understanding this circuit diagram are of course the boxes
with round corners and rows labeled <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 <MSB>:<LSB> tuples
specify which bits of the signals are broken out and connected. So the top row
of the box connecting the signals a and x indicates that the bit 0 (i.e.
the range 0:0) from signal a is connected to bit 1 (i.e. the range 1:1) of
signal x.
Lines connecting such boxes together and lines connecting such boxes to cell 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 Yosys commands.
Gate level netlists¶
Finally Fig. 3 shows two common pitfalls when working with
designs mapped to a cell library. The top figure has two problems: First Yosys
did not have access to the cell library when this diagram was generated,
resulting in all cell ports defaulting to being inputs. This is why all ports
are drawn on the left side the cells are awkwardly arranged in a large column.
Secondly the two-bit vector y requires breakout-boxes for its individual
bits, resulting in an unnecessary complex diagram.
For the 2nd diagram Yosys has been given a description of the cell library as
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
passed directly to the show command using the -lib <filename> option.
Secondly it is possible to load cell libraries into the design with the
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 show command.
In addition to that, the 2nd diagram was generated after 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
-ports option is required to also split module ports. Per default the
command only operates on interior signals.
Miscellaneous notes¶
Per default the show command outputs a temporary dot file and launches
xdot to display it. The options -format, -viewer and -prefix can
be used to change format, viewer and filename prefix. Note that the pdf and
ps format are the only formats that support plotting multiple modules in one
run.
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 show with
the -colors <integer> argument, which randomly assigns colors to the 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 help show prints a complete listing of all options supported by
the show command.
Navigating the design¶
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 what to display one also needs to carefully decide 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 techmap command already fails to verify, it is better to
troubleshoot the coarse-grain version of the circuit before techmap than
the gate-level circuit after techmap.
Note
It is generally recommended to verify the internal state of a
design by writing it to a Verilog file using write_verilog -noexpr
and using the simulation models from simlib.v and simcells.v
from the Yosys data directory (as printed by yosys-config --datdir).
Working with selections¶
Fig. 4 Output of show after select $2 or select t:$add (see also
Fig. 1)¶
When a module is selected using the cd command, all commands (with a few
exceptions, such as the read_ and write_ commands) operate 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.
But for most interactive work we want to further narrow the set of
selected objects. This can be done using the select command.
For example, if the command select $2 is executed, a subsequent show
command will yield the diagram shown in Fig. 4. Note that the nets are
now displayed in ellipses. This indicates that they are not selected, but only
shown because the diagram contains a cell that is connected to the net. This of
course makes no difference for the circuit that is shown, but it can be a useful
information when manipulating selections.
Objects can not only be selected by their name but also by other properties. For
example select t:$add will select all cells of type $add. In this case
this is also yields the diagram shown in Fig. 4.
module foobaraddsub(a, b, c, d, fa, fs, ba, bs);
input [7:0] a, b, c, d;
output [7:0] fa, fs, ba, bs;
assign fa = a + (* foo *) b;
assign fs = a - (* foo *) b;
assign ba = c + (* bar *) d;
assign bs = c - (* bar *) d;
endmodule
The output of help select contains a complete syntax reference for
matching different properties.
Many commands can operate on explicit selections. For example the command dump
t:$add will print information on all $add cells in the active module.
Whenever a command has [selection] as last argument in its usage help, this
means that it will use the engine behind the select command to evaluate
additional arguments and use the resulting selection instead of the selection
created by the last select command.
Normally the select command overwrites a previous selection. The commands
select -add and select -del can be used to add or remove objects from
the current selection.
The command select -clear can be used to reset the selection to the default,
which is a complete selection of everything in the current module.
Operations on selections¶
module sumprod(a, b, c, sum, prod);
input [7:0] a, b, c;
output [7:0] sum, prod;
{* sumstuff *}
assign sum = a + b + c;
{* *}
assign prod = a * b * c;
endmodule
Fig. 5 Output of show a:sumstuff on Listing 10¶
The select command is actually much more powerful than it might seem on the
first glimpse. When it is called with multiple arguments, each argument is
evaluated and pushed separately on a stack. After all arguments have been
processed it simply creates the union of all elements on the stack. So the
following command will select all $add cells and all objects with the
foo attribute set:
select t:$add a:foo
(Try this with the design shown in Listing 9. Use the select
-list command to list the current selection.)
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 combine the elements on the stack. For example
the %i arguments pops the last two elements from the stack, intersects
them, and pushes the result back on the stack. So the following command
will select all $add ``cells that have the ``foo attribute set:
select t:$add a:foo %i
The listing in Listing 10 uses the Yosys non-standard {... \*} syntax
to set the attribute sumstuff on all cells generated by the first assign
statement. (This works on arbitrary large blocks of Verilog code an can be used
to mark portions of code for analysis.)
Selecting a:sumstuff in this module will yield the circuit diagram shown in
Fig. 5. As only the cells themselves are selected, but not the
temporary wire $1_Y, the two adders are shown as two disjunct parts. This
can be very useful for global signals like clock and reset signals: just
unselect them using a command such as 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 %x action, that broadens the selection, i.e. for each
selected wire it selects all cells connected to the wire and vice versa. So
show a:sumstuff %x yields the diagram shown in Fig. 6.
Fig. 6 Output of show a:sumstuff %x on Listing 10¶
Selecting logic cones¶
Fig. 6 shows what is called the input cone of sum, i.e.
all cells and signals that are used to generate the signal sum. The %ci
action can be used to select the input cones of all object in the top selection
in the stack maintained by the select command.
As the %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. 7 show the sequence of diagrams generated by the following commands:
show prod
show prod %ci
show prod %ci %ci
show prod %ci %ci %ci
When selecting many levels of logic, repeating %ci over and over again can
be a bit dull. So there is a shortcut for that: the number of iterations can be
appended to the action. So for example the action %ci3 is identical to
performing the %ci action three times.
The action %ci\* performs the %ci action over and over again until it
has no effect anymore.
Fig. 7 Objects selected by select prod \%ci...¶
In most cases there are certain cell types and/or ports that should not be
considered for the %ci action, or we only want to follow certain cell types
and/or ports. This can be achieved using additional patterns that can be
appended to the %ci action.
Lets consider the design from Listing 11. It serves no purpose other
than being a non-trivial circuit for demonstrating some of the advanced Yosys
features. We synthesize the circuit using proc; opt; memory; opt and change
to the memdemo module with cd memdemo. If we type show now we see
the diagram shown in Fig. 8.
module memdemo(clk, d, y);
input clk;
input [3:0] d;
output reg [3:0] y;
integer i;
reg [1:0] s1, s2;
reg [3:0] mem [0:3];
always @(posedge clk) begin
for (i = 0; i < 4; i = i+1)
mem[i] <= mem[(i+1) % 4] + mem[(i+2) % 4];
{ s2, s1 } = d ? { s1, s2 } ^ d : 4'b0;
mem[s1] <= d;
y <= mem[s2];
end
endmodule
Fig. 8 Complete circuit diagram for the design shown in Listing 11¶
But maybe we are only interested in the tree of multiplexers that select the output value. In order to get there, we would start by just showing the output signal and its immediate predecessors:
show y %ci2
From this we would learn that y is driven by a $dff cell, that y is
connected to the output port Q, that the clk signal goes into the
CLK input port of the cell, and that the data comes from a auto-generated
wire into the input D of the flip-flop cell.
As we are not interested in the clock signal we add an additional pattern to the
%ci action, that tells it to only follow ports Q and D of $dff
cells:
show y %ci2:+$dff[Q,D]
To add a pattern we add a colon followed by the pattern to the %ci action.
The pattern it self starts with - or +, indicating if it is 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 square brackets.
Since we know that the only cell considered in this case is a $dff cell,
we could as well only specify the port names:
show y %ci2:+[Q,D]
Or we could decide to tell the %ci action to not follow the CLK input:
show y %ci2:-[CLK]
Fig. 9 Output of show y \%ci2:+\$dff[Q,D] \%ci*:-\$mux[S]:-\$dff¶
Next we would investigate the next logic level by adding another %ci2 to
the command:
show y %ci2:-[CLK] %ci2
From this we would learn that the next cell is a $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 command such as
show y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff
in which the first %ci jumps over the initial d-type flip-flop and the 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. 9.
Similar to %ci exists an action %co to select output cones that accepts
the same syntax for pattern and repetition. The %x action mentioned
previously also accepts this advanced syntax.
This actions for traversing the circuit graph, combined with the actions for
boolean operations such as intersection (%i) and difference (%d) are
powerful tools for extracting the relevant portions of the circuit under
investigation.
See help select for a complete list of actions available in selections.
Storing and recalling selections¶
The current selection can be stored in memory with the command select -set
<name>. It can later be recalled using select @<name>. In fact, the
@<name> expression pushes the stored selection on the stack maintained by
the select command. So for example
select @foo @bar %i
will select the intersection between the stored selections foo and bar.
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 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.
Advanced investigation techniques¶
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.
Listing 12 shows how the submod command can be used to split the
circuit from Listing 11 and Fig. 8 into its components.
The -name option is used to specify the name of the new module and also the
name of the new cell in the current module.
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
Evaluation of combinatorial circuits¶
The eval command can be used to evaluate combinatorial circuits. For example
(see Listing 12 for the circuit diagram of selstage):
yosys [selstage]> eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1
1. 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.
So the -set option is used to set input values and the -show option is
used to specify the nets to evaluate. If no -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
-set-undef can be used to instead set all unspecified input nets to undef
(x).
The -table option can be used to create a truth table. For example:
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
Note that the eval command (as well as the 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 flatten
command must be used on modules that instantiate other modules before this
commands can be applied.
Solving combinatorial SAT problems¶
module primetest(p, a, b, ok);
input [15:0] p, a, b;
output ok = p != a*b || a == 1 || b == 1;
endmodule
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!
/$$$$$$ /$$$$$$$$ /$$$$$$$
/$$__ $$ | $$_____/ | $$__ $$
| $$ \ $$ | $$ | $$ \ $$
| $$ | $$ | $$$$$ | $$ | $$
| $$ | $$ | $$__/ | $$ | $$
| $$/$$ $$ | $$ | $$ | $$
| $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$
\____ $$$|__/|________/|__/|_______/|__/
\__/
Often the opposite of the 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 eval -table command. For larger circuits
however, Yosys provides the sat command that uses a SAT solver,
MiniSAT, to solve this kind of problems.
The sat command works very similar to the eval command. The main
difference is that it is now also possible to set output values and find the
corresponding input values. For Example:
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
Note that the sat command supports signal names in both arguments to the
-set option. In the above example we used -set s1 s2 to constraint
s1 and 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 -set option. (Such a circuit that contains the circuit under
test plus additional constraint checking circuitry is called a miter
circuit.)
Listing 13 shows a miter circuit that is supposed to be used as a prime
number test. If ok is 1 for all input values a and b for a given
p, then p is prime, or at least that is the idea.
The Yosys shell session shown in Listing 14 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 p !=
a*b in the miter with p != {16'd0,a}b, or by using a temporary variable
for the 32 bit product 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 a and b to zero for the sat call, as is done in
the second command in Listing 14 (line 31).
The -prove option used in this example works similar to -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.
Solving sequential SAT problems¶
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
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 memdemo module from Listing 11 and suppose we want to know
which sequence of input values for d will cause the output y to produce the
sequence 1, 2, 3 from any initial state. Listing 15 show the solution
to this question, as produced by the following command:
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
The -seq 6 option instructs the 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 -set-init-undef option tells the sat command to initialize all
registers to the undef (x) state. The way the x state is treated in
Verilog will ensure that the solution will work for any initial state.
The -max_undef option instructs the 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 -set-at options add constraints for the y signal to
play the 1, 2, 3 sequence, starting with time step 4.
It is not surprising that the solution sets d = 0 in the first step, as this
is the only way of setting the s1 and 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.
There is much more to write about the sat command. For example, there is a
set of options that can be used to performs sequential proofs using temporal
induction [EenSorensson03]. The command help sat can be used to
print a list of all options with short descriptions of their functions.
Conclusion¶
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 (eval) or by evaluation which input values and initial conditions
can result in a certain behavior at the outputs (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.