Interactive design investigation

A look at the show command

This section explores the show command and explains the symbols used in the circuit diagrams generated by it. The code used is included in the Yosys code base under docs/source/code_examples/show.

A simple circuit

example.v below provides the Verilog code for a simple circuit which we will use to demonstrate the usage of show in a simple setting.

Listing 71 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 Yosys synthesis script we will be running is included as Listing 72. Note that show is called with the -pause option, that halts execution of the Yosys script until the user presses the Enter key. Using show -pause also allows the user to enter an interactive shell to further investigate the circuit before continuing synthesis.

Listing 72 example_show.ys

read_verilog example.v
show -pause # first
proc
show -pause # second
opt
show -pause # third

This script, when executed, will show the design after each of the three synthesis commands. We will now look at each of these diagrams and explain what is shown.

Note

The images uses in this document are generated from the example.ys file, rather than example_show.ys. example.ys outputs the schematics as .dot files rather than displaying them directly. You can view these images yourself by running yosys example.ys and then xdot example_first.dot etc.

Fig. 44 Output of the first show command in Listing 72

The first output 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. For more details on the internal cell library, see Internal cell library.

Constants are shown as ellipses with the constant value as label. The syntax <bit_width>'<bits> is used 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 second 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-flop, which brings us to the second diagram:

Fig. 45 Output of the second show command in Listing 72

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. These 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 these 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 the next step, which finally leads us to the third diagram:

Fig. 46 Output of the third show command in example_show.ys

Here we see that the proc 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.

Break-out boxes for signal vectors

The code listing below shows a simple circuit which uses a lot of spliced signal accesses.

Listing 73 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;
assign 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

Notice how the output for this circuit from the show command (Fig. 47) appears quite complex. This is an unfortunate side effect of the way Yosys handles signal vectors (aka. multi-bit wires or buses) as native objects. While this provides great advantages when analyzing circuits that operate on wide integers, it also introduces some additional complexity when the individual bits of of a signal vector are accessed.

Fig. 47 Output of yosys -p 'prep -top splice_demo; show' splice.v

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 these boxes have 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

Fig. 48 shows two common pitfalls when working with designs mapped to a cell library:

Fig. 48 A half-adder built from simple CMOS gates, demonstrating common pitfalls when using show

Listing 74 Generating Fig. 48

read_verilog cmos.v
prep -top cmos_demo
techmap
abc -liberty ../intro/mycells.lib;; 
show -format dot -prefix cmos_00

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.

Fig. 49 Effects of splitnets command and of providing a cell library on design in Fig. 48

Listing 75 Generating Fig. 49

read_verilog cmos.v
prep -top cmos_demo
techmap
splitnets -ports
abc -liberty ../intro/mycells.lib;; 
show -lib ../intro/mycells.v -format dot -prefix cmos_01

For Fig. 49, 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 second 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, Fig. 49 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. The dot format can be used to output multiple modules, however xdot will raise an error when trying to read them.

In densely connected circuits it is sometimes hard to keep track of the individual signal wires. For these 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).

Interactive navigation

Once the right state within the synthesis flow for debugging the circuit has been identified, it is recommended to simply add the shell command to the matching place in the synthesis script. This command will stop the synthesis at the specified moment and go to shell mode, where the user can interactively enter commands.

For most cases, the shell will start with the whole design selected (i.e. when the synthesis script does not already narrow the selection). The command ls can now be used to create a list of all modules. The command cd can be used to switch to one of the modules (type cd .. to switch back). Now the ls command lists the objects within that module. This is demonstrated below using example.v from A simple circuit:

Listing 76 Output of ls and cd after running yosys example.v

yosys> ls

1 modules:
  example

yosys> cd example

yosys [example]> ls

8 wires:
  $0\y[1:0]
  $add$example.v:5$2_Y
  $ternary$example.v:5$3_Y
  a
  b
  c
  clk
  y

2 cells:
  $add$example.v:5$2
  $ternary$example.v:5$3

1 processes:
  $proc$example.v:3$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.

We can see that the cell names from Fig. 46 are just abbreviations of the actual cell names, namely the part after the last dollar-sign. Most auto-generated names (the ones starting with a dollar sign) are rather long and contains some additional information on the origin of the named object. But in most cases those names can simply be abbreviated using the last part.

Usually all interactive work is done with one module selected using the cd command. But it is also possible to work from the design-context (cd ..). In this case all object names must be prefixed with <module_name>/. For example a*/b* would refer to all objects whose names start with b from all modules whose names start with a.

The dump command can be used to print all information about an object. For example, calling dump $2 after the cd example above:

Listing 77 Output of dump $2 after Listing 76

attribute \src "example.v:5.22-5.27"
cell $add $add$example.v:5$2
  parameter \Y_WIDTH 2
  parameter \B_WIDTH 1
  parameter \A_WIDTH 1
  parameter \B_SIGNED 0
  parameter \A_SIGNED 0
  connect \Y $add$example.v:5$2_Y
  connect \B \b
  connect \A \a
end

This can for example be useful to determine the names of nets connected to cells, as the net-names are usually suppressed in the circuit diagram if they are auto-generated. Note that the output is in the RTLIL representation, described in The RTL Intermediate Language (RTLIL).

Interactive Design Investigation

Yosys can also be used to investigate designs (or netlists created from other tools).

• The selection mechanism, especially patterns such as %ci and %co, can be used to figure out how parts of the design are connected.

• Commands such as submod, expose, and splice can be used to transform the design into an equivalent design that is easier to analyse.

• Commands such as eval and sat can be used to investigate the behavior of the circuit.

• show - generate schematics using graphviz.

• dump - print parts of the design in RTLIL format.

• add - add objects to the design and delete - delete objects in the design can be used to modify and reorganize a design dynamically.

The code used is included in the Yosys code base under docs/source/code_examples/scrambler.

Changing design hierarchy

Commands such as flatten and submod can be used to change the design hierarchy, i.e. flatten the hierarchy or moving parts of a module to a submodule. This has applications in synthesis scripts as well as in reverse engineering and analysis. An example using submod is shown below for reorganizing a module in Yosys and checking the resulting circuit.

Listing 78 scrambler.v

module scrambler(
        input clk, rst, in_bit,
        output reg out_bit
);
    reg [31:0] xs;
    always @(posedge clk) begin
    	if (rst)
	    xs = 1;
        xs = xs ^ (xs << 13);
        xs = xs ^ (xs >> 17);
        xs = xs ^ (xs << 5);
        out_bit <= in_bit ^ xs[0];
    end
endmodule

Listing 79 scrambler.ys

read_verilog scrambler.v

hierarchy; proc;;

cd scrambler
submod -name xorshift32 xs %c %ci %D %c %ci:+[D] %D %ci*:-$dff xs %co %ci %d

Analyzing the resulting circuit with eval - evaluate the circuit given an input:

> cd xorshift32
> rename n2 in
> rename n1 out

> eval -set in 1 -show out
Eval result: \out = 270369.

> eval -set in 270369 -show out
Eval result: \out = 67634689.

> sat -set out 632435482
Signal Name                 Dec        Hex                                   Bin
-------------------- ---------- ---------- -------------------------------------
\in                   745495504   2c6f5bd0      00101100011011110101101111010000
\out                  632435482   25b2331a      00100101101100100011001100011010

Behavioral changes

Commands such as techmap can be used to make behavioral changes to the design, for example changing asynchronous resets to synchronous resets. This has applications in design space exploration (evaluation of various architectures for one circuit).

The following techmap map file replaces all positive-edge async reset flip-flops with positive-edge sync reset flip-flops. The code is taken from the example Yosys script for ASIC synthesis of the Amber ARMv2 CPU.

(* techmap_celltype = "$adff" *)
module adff2dff (CLK, ARST, D, Q);

    parameter WIDTH = 1;
    parameter CLK_POLARITY = 1;
    parameter ARST_POLARITY = 1;
    parameter ARST_VALUE = 0;

    input CLK, ARST;
    input [WIDTH-1:0] D;
    output reg [WIDTH-1:0] Q;

    wire [1023:0] _TECHMAP_DO_ = "proc";

    wire _TECHMAP_FAIL_ = !CLK_POLARITY || !ARST_POLARITY;

    always @(posedge CLK)
        if (ARST)
            Q <= ARST_VALUE;
        else
            Q <= D;

endmodule

For more on the techmap command, see the page on Techmap by example.

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.

Recall the memdemo design from Advanced logic cone selection:

Fig. 50 memdemo

Because this produces a rather large circuit, it can be useful to split it into smaller parts for viewing and working with. Listing 80 does exactly that, utilising the submod command to split the circuit into three sections: outstage, selstage, and scramble.

Listing 80 Using submod to break up the circuit from memdemo.v

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

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. The resulting circuits are shown below.

Fig. 51 outstage

Fig. 52 selstage

Fig. 53 scramble

Evaluation of combinatorial circuits

The eval command can be used to evaluate combinatorial circuits. As an example, we will use the selstage subnet of memdemo which we found above and is shown in Fig. 52.

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 these commands can be applied.

Solving combinatorial SAT problems

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.

Note

While it is possible to perform model checking directly in Yosys, it is highly recommended to use SBY or EQY for formal hardware verification.

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 81 primetest.v, a simple miter circuit for testing if a number is prime. But it has a problem.

module primetest(p, a, b, ok);
input [15:0] p, a, b;
output ok = p != a*b || a == 1 || b == 1;
endmodule

Listing 81 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.

Listing 82 Experiments with the miter circuit from primetest.v.

yosys [primetest]> sat -prove ok 1 -set p 31

1. 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

The Yosys shell session shown in Listing 82 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 below.

Listing 83 Miter circuit from primetest.v, with the upper 8 bits of a and b constrained to prevent overflow.

yosys [primetest]> sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0

1. 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!

                  /$$$$$$      /$$$$$$$$     /$$$$$$$
                 /$$__  $$    | $$_____/    | $$__  $$
                | $$  \ $$    | $$          | $$  \ $$
                | $$  | $$    | $$$$$       | $$  | $$
                | $$  | $$    | $$__/       | $$  | $$
                | $$/$$ $$    | $$          | $$  | $$
                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$
                 \____ $$$|__/|________/|__/|_______/|__/
                       \__/

The -prove option used in Listing 83 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

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 memdemo design from Advanced logic cone selection again, 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. Let’s use 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.

This produces the following output:

Listing 84 Solving a sequential SAT problem in the memdemo module.

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

1. 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

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.