summaryrefslogtreecommitdiff
path: root/manual/APPNOTE_011_Design_Investigation.tex
blob: 9a8f604b6722de9d5d824d552ed5d8712bdccbab (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
% IEEEtran howto:
% http://ftp.univie.ac.at/packages/tex/macros/latex/contrib/IEEEtran/IEEEtran_HOWTO.pdf
\documentclass[9pt,technote,a4paper]{IEEEtran}

\usepackage[T1]{fontenc}   % required for luximono!
\usepackage[scaled=0.8]{luximono}  % typewriter font with bold face

% To install the luximono font files:
% getnonfreefonts-sys --all        or
% getnonfreefonts-sys luximono
%
% when there are trouble you might need to:
% - Create /etc/texmf/updmap.d/99local-luximono.cfg
%   containing the single line: Map ul9.map
% - Run update-updmap followed by mktexlsr and updmap-sys
%
% This commands must be executed as root with a root environment
% (i.e. run "sudo su" and then execute the commands in the root
% shell, don't just prefix the commands with "sudo").

\usepackage[unicode,bookmarks=false]{hyperref}
\usepackage[english]{babel}
\usepackage[utf8]{inputenc}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{units}
\usepackage{nicefrac}
\usepackage{eurosym}
\usepackage{graphicx}
\usepackage{verbatim}
\usepackage{algpseudocode}
\usepackage{scalefnt}
\usepackage{xspace}
\usepackage{color}
\usepackage{colortbl}
\usepackage{multirow}
\usepackage{hhline}
\usepackage{listings}
\usepackage{float}

\usepackage{tikz}
\usetikzlibrary{calc}
\usetikzlibrary{arrows}
\usetikzlibrary{scopes}
\usetikzlibrary{through}
\usetikzlibrary{shapes.geometric}

\def\FIXME{{\color{red}\bf FIXME}}

\lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=0.7cm,xrightmargin=0.2cm,numbers=left}

\begin{document}

\title{Yosys Application Note 011: \\ Interactive Design Investigation}
\author{Clifford Wolf \\ December 2013}
\maketitle

\begin{abstract}
Yosys \cite{yosys} can be a great environment for building custom synthesis
flows. It can also be an excellent tool for teaching and learning Verilog based
RTL synthesis. In both applications it is of great importance to be able to
analyze the designs it produces easily.

This Yosys application note covers the generation of circuit diagrams with the
Yosys {\tt show} command, the selection of interesting parts of the circuit
using the {\tt select} command, and briefly discusses advanced investigation
commands for evaluating circuits and solving SAT problems.
\end{abstract}

\section{Installation and Prerequisites}

This Application Note is based on the Yosys \cite{yosys} GIT Rev. {\tt \FIXME} from
\FIXME{}. The {\tt README} file covers how to install Yosys. The
{\tt show} command requires a working installation of GraphViz \cite{graphviz}
for generating the actual circuit diagrams. Yosys must be build with Qt
support for the built-in SVG viewer. Alternatively an external viewer can be
used, if Qt is not available.

\section{Overview}

This application note is structured as follows:

Sec.~\ref{intro_show} introduces the {\tt show} command and explains the
symbols used in the circuit diagrams generated by it.

Sec.~\ref{navigate} 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.

Sec.~\ref{poke} introduces commands to evaluate the design and solve SAT
problems within the design.

Sec.~\ref{conclusion} concludes the document and summarizes the key points.

\section{Introduction to the {\tt show} command}
\label{intro_show}

\begin{figure}[b]
\begin{lstlisting}
$ 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
\end{lstlisting}
\caption{Yosys script with {\tt show} commands and example design}
\label{example_src}
\end{figure}

\begin{figure}[b!]
\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_00.pdf}
\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_01.pdf}
\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_02.pdf}
\caption{Output of the three {\tt show} commands from Fig.~\ref{example_src}}
\label{example_out}
\end{figure}

The {\tt 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 {\tt yosys-svgviewer} to display the diagram.
Subsequent calls to {\tt show} re-use the {\tt yosys-svgviewer} instance
(if still running).

\subsection{A simple circuit}

Fig.~\ref{example_src} shows a simple synthesis script and a Verilog file that
demonstrate the usage of {\tt show} in a simple setting. Note that {\tt show}
is called with the {\tt -pause} option, that halts execution of the Yosys
script until the user presses the Enter key. The {\tt show -pause} command
also allows the user to enter an interactive shell to further investigate the
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.~\ref{example_out}.

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
{\tt <bit\_width>'<bits>} is used for for constants that are not 32-bit wide
and/or contain bits that are not 0 or 1 (i.e. {\tt x} or {\tt 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 {\it processes\/} are shown in boxes with round corners. Processes
are Yosys' internal representation of the decision-trees and synchronization
events modelled in a Verilog {\tt always}-block. The label reads {\tt PROC}
followed by a unique identifier in the first line and contains the source code
location of the original {\tt always}-block in the 2nd line. Note how the
multiplexer from the {\tt ?:}-expression is represented as a {\tt \$mux} cell
but the multiplexer from the {\tt if}-statement is yet still hidden within the
process.

\medskip

The {\tt proc} command transforms the process from the first diagram into a
multiplexer and a d-type flip-flip, which brings us to the 2nd diagram.

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
{\tt BUF}-node. This are artefacts left behind by the {\tt proc}-command. It is
quite usual to see such artefacts after calling commands that perform changes
in the design, as most commands only care about doing the transformation in the
least complicated way, not about cleaning up after them. The next call to {\tt
clean} (or {\tt opt}, which includes {\tt clean} as one of its operations) will
clean up this artefacts.  This operation is so common in Yosys scripts that it
can simply be abbreviated with the {\tt ;;} 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 {\tt clean}
before calling {\tt show}.

\medskip

In this script we directly call {\tt opt} as next step, which finally leads us to
the 3rd diagram in Fig.~\ref{example_out}. Here we see that the {\tt opt} command
not only has removed the artifacts left behind by {\tt proc}, but also determined
correctly that it can remove the first {\tt \$mux} cell without changing the behavior
of the circuit.

\begin{figure}[b!]
\includegraphics[width=\linewidth,trim=0 2cm 0 0]{APPNOTE_011_Design_Investigation/splice.pdf}
\caption{Output of {\tt yosys -p 'proc; opt; show' splice.v}}
\label{splice_dia}
\end{figure}

\begin{figure}[b!]
\lstinputlisting{APPNOTE_011_Design_Investigation/splice.v}
\caption{\tt splice.v}
\label{splice_src}
\end{figure}

\begin{figure}[t!]
\includegraphics[height=\linewidth]{APPNOTE_011_Design_Investigation/cmos_00.pdf}
\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/cmos_01.pdf}
\caption{Effects of {\tt splitnets} command and of providing a cell library. (The
circuit is a half-adder built from simple CMOS gates.)}
\label{splitnets_libfile}
\end{figure}

\subsection{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 Fig.~\ref{splice_dia} and \ref{splice_src}
demonstrates how such circuits are visualized by the {\tt show} command.

The key elements in understanding this circuit diagram are of course the boxes
with round corners and rows labeled {\tt <MSB\_LEFT>:<LSB\_LEFT> -- <MSB\_RIGHT>:<LSB\_RIGHT>}.
Each of this boxes has one signal per row on one side and a common signal for all rows on the
other side. The {\tt <MSB>:<LSB>} tuples specify which bits of the signals are broken out
and connected. So the top row of the box connecting the signals {\tt a} and {\tt x} indicates
that the bit 0 (i.e. the range 0:0) from signal {\tt a} is connected to bit 1 (i.e. the range
1:1) of signal {\tt 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.

\subsection{Gate level netlists}

Finally Fig.~\ref{splitnets_libfile} 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 {\tt 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 {\tt show} command using the {\tt -lib <filename>}
option. Secondly it is possible to load cell libraries into the design with
the {\tt read\_verilog -lib <filename>} command. The 2nd method has the great 
advantage that the library only needs to be loaded once and can then be used
in all subsequent calls to the {\tt show} command.

In addition to that, the 2nd diagram was generated after {\tt splitnet -ports}
was run on the design. This command splits all signal vectors into individual
signal bits, which is often desirable when looking at gate-level circuits. The
{\tt -ports} option is required to also split module ports. Per default the
command only operates on interior signals.

\subsection{Miscellaneous notes}

Per default the {\tt show} command outputs a temporary SVG file and launches
{\tt yosys-svgviewer} to display it. The options {\tt -format}, {\tt -viewer}
and {\tt -prefix} can be used to change format, viewer and filename prefix.
Note that the {\tt pdf} and {\tt ps} format are the only formats that support
plotting multiple modules in one run.

In {\tt yosys-svgviewer} the left mouse button is per default bound to move the
diagram (and the mouse wheel can be used for zooming in and out). However, in
some cases one wants to copy text from the diagram. In this cases the
View->Interactive checkbox must be activated. This switches the rendering back-end
in a mode that supports interaction with the SVG file, such as selecting text.

In densely connected circuits it is sometimes hard to keep track of the
individual signal wires. For this cases it can be useful to call {\tt show}
with the {\tt -colors <integer>} argument, which randomly assigns colors to the
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 {\tt help show} prints a complete listing of all options supported
by the {\tt show} command.

\section{Navigating the design}
\label{navigate}

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 {\it what\/} to display one also needs to carefully decide
{\it when\/} to display it, with respect to the synthesis flow. In general
it is a good idea to troubleshoot a circuit in the earliest state in which
a problem can be reproduced. So if, for example, the internal state before calling
the {\tt techmap} command already fails to verify, it is better to troubleshoot 
the coarse-grain version of the circuit before {\tt techmap} than the gate-level
circuit after {\tt techmap}.

\medskip

Note: It is generally recommended to verify the internal state of a design by
writing it to a Verilog file using {\tt write\_verilog -noexpr} and using the
simulation models from {\tt simlib.v} and {\tt simcells.v} from the Yosys data
directory (as printed by {\tt yosys-config -{}-datdir}).

\subsection{Interactive Navigation}

\begin{figure}
\begin{lstlisting}
yosys> ls

1 modules:
  example

yosys> cd example 

yosys [example]> ls

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

3 cells:
  $add$example.v:5$2
  $procdff$7
  $procmux$5
\end{lstlisting}
\caption{Demonstration of {\tt ls} and {\tt cd} using {\tt example.v} from Fig.~\ref{example_src}}
\label{lscd}
\end{figure}

\begin{figure}[b]
\begin{lstlisting}
  attribute \src "example.v:5"
  cell $add $add$example.v:5$2
    parameter \A_SIGNED 0
    parameter \A_WIDTH 1
    parameter \B_SIGNED 0
    parameter \B_WIDTH 1
    parameter \Y_WIDTH 2
    connect \A \a
    connect \B \b
    connect \Y $add$example.v:5$2_Y
  end
\end{lstlisting}
\caption{Output of {\tt dump \$2} using the design from Fig.~\ref{example_src} and  Fig.~\ref{example_out}}
\label{dump2}
\end{figure}

Once the right state within the synthesis flow for debugging the circuit has
been identified, it is recommended to simply add the {\tt 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 {\tt
ls} can now be used to create a list of all modules. The command {\tt cd} can
be used to switch to one of the modules (type {\tt cd ..} to switch back). Now
the {\tt ls} command lists the objects within that module. Fig.~\ref{lscd}
demonstrates this using the design from Fig.~\ref{example_src}.

There is a thing to note in Fig.~\ref{lscd}: We can see that the cell names
from Fig.~\ref{example_out} 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 {\tt cd}
command. But it is also possible to work from the design-context ({\tt cd ..}). In
this case all object names must be prefixed with {\tt <module\_name>/}. For
example {\tt a*/b*} would refer to all objects whose names start with {\tt b} from
all modules whose names start with {\tt a}.

The {\tt dump} command can be used to print all information about an object.
For example {\tt dump \$2} will print Fig.~\ref{dump2}. 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.

For the remainder of this document we will assume that the commands are run from
module-context and not design-context.

\subsection{Working with selections}

\begin{figure}[t]
\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/example_03.pdf}
\caption{Output of {\tt show} after {\tt select \$2} or {\tt select t:\$add}
(see also Fig.~\ref{example_out})}
\label{seladd}
\end{figure}

When a module is selected using the {\tt cd} command, all commands (with a few
exceptions, such as the {\tt read\_*} and {\tt write\_*} commands) operate
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 {\tt select} command.

For example, if the command {\tt select \$2} is executed, a subsequent {\tt show}
command will yield the diagram shown in Fig.~\ref{seladd}. 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 {\tt select t:\$add} will select all cells of type {\tt \$add}. In
this case this is also yields the diagram shown in Fig.~\ref{seladd}.

\begin{figure}[b]
\lstinputlisting{APPNOTE_011_Design_Investigation/foobaraddsub.v}
\caption{Test module for operations on selections}
\label{foobaraddsub}
\end{figure}

The output of {\tt help select} contains a complete syntax reference for
matching different properties.

Many commands can operate on explicit selections. For example the command {\tt
dump t:\$add} will print information on all {\tt \$add} cells in the active
module. Whenever a command has {\tt [selection]} as last argument in its usage
help, this means that it will use the engine behind the {\tt select} command
to evaluate additional arguments and use the resulting selection instead of
the selection created by the last {\tt select} command.

Normally the {\tt select} command overwrites a previous selection. The
commands {\tt select -add} and {\tt select -del} can be used to add
or remove objects from the current selection.

The command {\tt select -clear} can be used to reset the selection to the
default, which is a complete selection of everything in the current module.

\subsection{Operations on selections}

\begin{figure}[t]
\lstinputlisting{APPNOTE_011_Design_Investigation/sumprod.v}
\caption{Another test module for operations on selections}
\label{sumprod}
\end{figure}

\begin{figure}[b]
\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/sumprod_00.pdf}
\caption{Output of {\tt show a:sumstuff} on Fig.~\ref{sumprod}}
\label{sumprod_00}
\end{figure}

The {\tt 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 {\tt \$add} cells and all objects with
the {\tt foo} attribute set:

\begin{verbatim}
select t:$add a:foo
\end{verbatim}

(Try this with the design shown in Fig.~\ref{foobaraddsub}. Use the {\tt
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 {\tt \%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 {\tt foo}
attribute set:

\begin{verbatim}
select t:$add a:foo %i
\end{verbatim}

The listing in Fig.~\ref{sumprod} uses the Yosys non-standard {\tt \{* ... *\}}
syntax to set the attribute {\tt 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 {\tt a:sumstuff} in this module will yield the circuit diagram shown
in Fig.~\ref{sumprod_00}. As only the cells themselves are selected, but not
the temporary wire {\tt \$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 {\tt 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 {\tt \%x} action, that broadens the selection, i.e.
for each selected wire it selects all cells connected to the wire and vice
versa. So {\tt show a:sumstuff \%x} yields the diagram schon in Fig.~\ref{sumprod_01}.

\begin{figure}[t]
\includegraphics[width=\linewidth]{APPNOTE_011_Design_Investigation/sumprod_01.pdf}
\caption{Output of {\tt show a:sumstuff \%x} on Fig.~\ref{sumprod}}
\label{sumprod_01}
\end{figure}

\subsection{Selecting logic cones}

Fig.~\ref{sumprod_01} shows what is called the {\it input cone\/} of {\tt sum}, i.e.
all cells and signals that are used to generate the signal {\tt sum}. The {\tt \%ci}
action can be used to select the input cones of all object in the top selection
in the stack maintained by the {\tt select} command.

As the {\tt \%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.~\ref{select_prod} show the sequence of diagrams generated by the following
commands:

\begin{verbatim}
show prod
show prod %ci
show prod %ci %ci
show prod %ci %ci %ci
\end{verbatim}

When selecting many levels of logic, repeating {\tt \%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 {\tt \%ci3} is
identical to performing the {\tt \%ci} action three times.

The action {\tt \%ci*} performs the {\tt \%ci} action over and over again until
it has no effect anymore.

\begin{figure}[t]
\hfill \includegraphics[width=4cm,trim=0 1cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_02.pdf} \\
\includegraphics[width=\linewidth,trim=0 0cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_03.pdf} \\
\includegraphics[width=\linewidth,trim=0 0cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_04.pdf} \\
\includegraphics[width=\linewidth,trim=0 2cm 0 1cm]{APPNOTE_011_Design_Investigation/sumprod_05.pdf} \\
\caption{Objects selected by {\tt select prod \%ci...}}
\label{select_prod}
\end{figure}

\medskip

In most cases there are certain cell types and/or ports that should not be considered for the {\tt \%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 {\tt \%ci} action.

Lets consider the design from Fig.~\ref{memdemo_src}. It serves no purpose other than being a non-trivial
circuit for demonstrating some of the advanced Yosys features. We synthesize the circuit using {\tt proc;
opt; memory; opt} and change to the {\tt memdemo} module with {\tt cd memdemo}. If we type {\tt show}
now we see the diagram shown in Fig.~\ref{memdemo_00}.

\begin{figure}[b!]
\lstinputlisting{APPNOTE_011_Design_Investigation/memdemo.v}
\caption{Demo circuit for demonstrating some advanced Yosys features}
\label{memdemo_src}
\end{figure}

\begin{figure*}[t]
\includegraphics[width=\linewidth,trim=0 0cm 0 0cm]{APPNOTE_011_Design_Investigation/memdemo_00.pdf} \\
\caption{Complete circuit diagram for the design shown in Fig.~\ref{memdemo_src}}
\label{memdemo_00}
\end{figure*}

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:

\begin{verbatim}
show y %ci2
\end{verbatim}

From this we would learn that {\tt y} is driven by a {\tt \$dff cell}, that
{\tt y} is connected to the output port {\tt Q}, that the {\tt clk} signal goes
into the {\tt CLK} input port of the cell, and that the data comes from a
auto-generated wire into the input {\tt D} of the flip-flop cell.

As we are not interested in the clock signal we add an additional pattern to the {\tt \%ci}
action, that tells it to only follow ports {\tt Q} and {\tt D} of {\tt \$dff} cells:

\begin{verbatim}
show y %ci2:+$dff[Q,D]
\end{verbatim}

To add a pattern we add a colon followed by the pattern to the {\tt \%ci}
action. The pattern it self starts with {\tt -} or {\tt +}, 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 {\tt \$dff} cell,
we could as well only specify the port names:

\begin{verbatim}
show y %ci2:+[Q,D]
\end{verbatim}

Or we could decide to tell the {\tt \%ci} action to not follow the {\tt CLK} input:

\begin{verbatim}
show y %ci2:-[CLK]
\end{verbatim}

\begin{figure}[b]
\includegraphics[width=\linewidth,trim=0 0cm 0 0cm]{APPNOTE_011_Design_Investigation/memdemo_01.pdf} \\
\caption{Output of {\tt show y \%ci2:+\$dff[Q,D] \%ci*:-\$mux[S]:-\$dff}}
\label{memdemo_01}
\end{figure}

Next we would investigate the next logic level by adding another {\tt \%ci2} to
the command:

\begin{verbatim}
show y %ci2:-[CLK] %ci2
\end{verbatim}

From this we would learn that the next cell is a {\tt \$mux} cell and we would add additional
pattern to narrow the selection on the path we are interested. In the end we would end up
with a command such as

\begin{verbatim}
show y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff
\end{verbatim}

in which the first {\tt \%ci} jumps over the initial d-type flip-flop and the
2nd action selects the entire input cone without going over multiplexer select
inputs and flip-flop cells. The diagram produces by this command is shown in
Fig.~\ref{memdemo_01}.

\medskip

Similar to {\tt \%ci} exists an action {\tt \%co} to select output cones that
accepts the same syntax for pattern and repetition. The {\tt \%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 ({\tt \%i}) and difference ({\tt \%d})
are powerful tools for extracting the relevant portions of the circuit under
investigation.

See {\tt help select} for a complete list of actions available in selections.

\subsection{Storing and recalling selections}

The current selection can be stored in memory with the command {\tt select -set
<name>}. It can later be recalled using {\tt select @<name>}. In fact, the {\tt
@<name>} expression pushes the stored selection on the stack maintained by the
{\tt select} command. So for example

\begin{verbatim}
select @foo @bar %i
\end{verbatim}

will select the intersection between the stored selections {\tt foo} and {\tt bar}.

\medskip

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 {\tt 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.

\section{Advanced investigation techniques}
\label{poke}

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.

Fig.~\ref{submod} shows how the {\tt submod} command can be used to split the
circuit from Fig.~\ref{memdemo_src} and \ref{memdemo_00} into its components.
The {\tt -name} option is used to specify the name of the new module and
also the name of the new cell in the current module.

\begin{figure}[t]
\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_00.pdf} \\ \centerline{\tt memdemo} \vskip1em\par
\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_01.pdf} \\ \centerline{\tt scramble} \vskip1em\par
\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_02.pdf} \\ \centerline{\tt outstage} \vskip1em\par
\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{APPNOTE_011_Design_Investigation/submod_03.pdf} \\ \centerline{\tt selstage} \vskip1em\par
\begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
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
\end{lstlisting}
\caption{The circuit from Fig.~\ref{memdemo_src} and \ref{memdemo_00} broken up using {\tt submod}}
\label{submod}
\end{figure}

\subsection{Evaluation of combinatorial circuits}

The {\tt eval} command can be used to evaluate combinatorial circuits.
For example (see Fig.~\ref{submod} for the circuit diagram of {\tt selstage}):

{\scriptsize
\begin{verbatim}
   yosys [selstage]> eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1
   
   9. Executing EVAL pass (evaluate the circuit given an input).
   Full command line: eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1
   Eval result: \n2 = 2'10.
   Eval result: \n1 = 2'10.
\end{verbatim}
\par}

So the {\tt -set} option is used to set input values and the {\tt -show} option
is used to specify the nets to evaluate. If no {\tt -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
{\tt -set-undef} can be used to instead set all unspecified input nets to
undef ({\tt x}).

The {\tt -table} option can be used to create a truth table. For example:

{\scriptsize
\begin{verbatim}
   yosys [selstage]> eval -set-undef -set d[3:1] 0 -table s1,d[0]
   
   10. Executing EVAL pass (evaluate the circuit given an input).
   Full command line: eval -set-undef -set d[3:1] 0 -table s1,d[0]
   
     \s1 \d [0] |  \n1  \n2
    ---- ------ | ---- ----
    2'00    1'0 | 2'00 2'00
    2'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
   
   Assumend undef (x) value for the following singals: \s2
\end{verbatim}
}

Note that the {\tt eval} command (as well as the {\tt 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 {\tt flatten}
command must be used on modules that instantiate other modules before this
commands can be applied.

\subsection{Solving combinatorial SAT problems}

\begin{figure}[b]
\lstinputlisting{APPNOTE_011_Design_Investigation/primetest.v}
\caption{A simple miter circuit for testing if a number is prime. But it has a
problem (see main text and Fig.~\ref{primesat}).}
\label{primetest}
\end{figure}

\begin{figure*}[!t]
\begin{lstlisting}[basicstyle=\ttfamily\small]
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!

                  /$$$$$$      /$$$$$$$$     /$$$$$$$    
                 /$$__  $$    | $$_____/    | $$__  $$   
                | $$  \ $$    | $$          | $$  \ $$   
                | $$  | $$    | $$$$$       | $$  | $$   
                | $$  | $$    | $$__/       | $$  | $$   
                | $$/$$ $$    | $$          | $$  | $$   
                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$
                 \____ $$$|__/|________/|__/|_______/|__/
                       \__/                              
\end{lstlisting}
\caption{Experiments with the miter circuit from Fig.~\ref{primetest}. The first attempt of proving that 31
is prime failed because the SAT solver found a creative way of factorizing 31 using integer overflow.}
\label{primesat}
\end{figure*}

Often the opposite of the {\tt 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 {\tt eval -table} command.
For larger circuits however, Yosys provides the {\tt sat} command that uses
a SAT \cite{CircuitSAT} solver \cite{MiniSAT} to solve this kind of problems.

The {\tt sat} command works very similar to the {\tt eval} command. The main
difference is that it is now also possible to set output values and find the
corresponding input values. For Example:

{\scriptsize
\begin{verbatim}
   yosys [selstage]> sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001
   
   11. Executing SAT pass (solving SAT problems in the circuit).
   Full command line: sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001
   
   Setting up SAT problem:
   Import set-constraint: \s1 = \s2
   Import set-constraint: { \n2 \n1 } = 4'1001
   Final constraint equation: { \n2 \n1 \s1 } = { 4'1001 \s2 }
   Imported 3 cells to SAT database.
   Import show expression: { \s1 \s2 \d }
   
   Solving problem with 81 variables and 207 clauses..
   SAT solving finished - model found:
   
     Signal Name                 Dec        Hex             Bin
     -------------------- ---------- ---------- ---------------
     \d                            9          9            1001
     \s1                           0          0              00
     \s2                           0          0              00
\end{verbatim}
}

Note that the {\tt sat} command supports signal names in both arguments
to the {\tt -set} option. In the above example we used {\tt -set s1 s2}
to constraint {\tt s1} and {\tt 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 {\tt
-set} option. (Such a circuit that contains the circuit under test
plus additional constraint checking circuitry is called a {\it miter\/}
circuit.)

Fig.~\ref{primetest} shows a miter circuit that is supposed to be used as a
prime number test. If {\tt ok} is 1 for all input values {\tt a} and {\tt b}
for a given {\tt p}, then {\tt p} is prime, or at least that is the idea.

The Yosys shell session shown in Fig.~\ref{primesat} 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
{\tt p != a*b} in the miter with {\tt p != \{16'd0,a\}*b}, or by using a
temporary variable for the 32 bit product {\tt 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 {\tt a} and {\tt b} to zero for
the {\tt sat} call, as is done in the second command in Fig.~\ref{primesat}
(line 31).

The {\tt -prove} option used in this example works similar to {\tt -set}, but
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.

\subsection{Solving sequential SAT problems}

\begin{figure}[t!]
\begin{lstlisting}[basicstyle=\ttfamily\scriptsize]
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
\end{lstlisting}
\caption{Solving a sequential SAT problem in the {\tt memdemo} module from Fig.~\ref{memdemo_src}.}
\label{memdemo_sat}
\end{figure}

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 {\tt memdemo} module from Fig.~\ref{memdemo_src} and suppose we
want to know which sequence of input values for {\tt d} will cause the output
{\tt y} to produce the sequence 1, 2, 3 from any initial state.
Fig.~\ref{memdemo_sat} show the solution to this question, as produced by
the following command:

\begin{verbatim}
   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
\end{verbatim}

The {\tt -seq 6} option instructs the {\tt 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 {\tt -set-init-undef} option tells the {\tt sat} command to initialize
all registers to the undef ({\tt x}) state. The way the {\tt x} state
is treated in Verilog will ensure that the solution will work for any
initial state.

The {\tt -max\_undef} option instructs the {\tt sat} command to find a solution
with a maximum number of undefs. This way we can see clearly which inputs bits
are relevant to the solution.

Finally the three {\tt -set-at} options add constraints for the {\tt y}
signal to play the 1, 2, 3 sequence, starting with time step 4.

It is not surprising that the solution sets {\tt d = 0} in the first step, as
this is the only way of setting the {\tt s1} and {\tt 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.

\medskip

There is much more to write about the {\tt sat} command. For example, there is
a set of options that can be used to performs sequential proofs using temporal
induction \cite{tip}. The command {\tt help sat} can be used to print a list
of all options with short descriptions of their functions.

\section{Conclusion}
\label{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
({\tt eval}) or by evaluation which input values and initial conditions can result
in a certain behavior at the outputs ({\tt sat}). The SAT command can even be used
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.

\begin{thebibliography}{9}

\bibitem{yosys}
Clifford Wolf. The Yosys Open SYnthesis Suite.
\url{http://www.clifford.at/yosys/}

\bibitem{graphviz}
Graphviz - Graph Visualization Software.
\url{http://www.graphviz.org/}

\bibitem{CircuitSAT}
{\it Circuit satisfiability problem} on Wikipedia
\url{http://en.wikipedia.org/wiki/Circuit_satisfiability}

\bibitem{MiniSAT}
MiniSat: a minimalistic open-source SAT solver.
\url{http://minisat.se/}

\bibitem{tip}
Niklas Een and Niklas Sörensson (2003).
Temporal Induction by Incremental SAT Solving.
\url{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.8161}

\end{thebibliography}

\end{document}