summaryrefslogtreecommitdiff log msg author committer range
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  pre { line-height: 125%; margin: 0; } td.linenos pre { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; } span.linenos { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; } td.linenos pre.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; } span.linenos.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; } .highlight .hll { background-color: #ffffcc } .highlight .c { color: #888888 } /* Comment */ .highlight .err { color: #a61717; background-color: #e3d2d2 } /* Error */ .highlight .k { color: #008800; font-weight: bold } /* Keyword */ .highlight .ch { color: #888888 } /* Comment.Hashbang */ .highlight .cm { color: #888888 } /* Comment.Multiline */ .highlight .cp { color: #cc0000; font-weight: bold } /* Comment.Preproc */ .highlight .cpf { color: #888888 } /* Comment.PreprocFile */ .highlight .c1 { color: #888888 } /* Comment.Single */ .highlight .cs { color: #cc0000; font-weight: bold; background-color: #fff0f0 } /* Comment.Special */ .highlight .gd { color: #000000; background-color: #ffdddd } /* Generic.Deleted */ .highlight .ge { font-style: italic } /* Generic.Emph */ .highlight .gr { color: #aa0000 } /* Generic.Error */ .highlight .gh { color: #333333 } /* Generic.Heading */ .highlight .gi { color: #000000; background-color: #ddffdd } /* Generic.Inserted */ .highlight .go { color: #888888 } /* Generic.Output */ .highlight .gp { color: #555555 } /* Generic.Prompt */ .highlight .gs { font-weight: bold } /* Generic.Strong */ .highlight .gu { color: #666666 } /* Generic.Subheading */ .highlight .gt { color: #aa0000 } /* Generic.Traceback */ .highlight .kc { color: #008800; font-weight: bold } /* Keyword.Constant */ .highlight .kd { color: #008800; font-weight: bold } /* Keyword.Declaration */ .highlight .kn { color: #008800; font-weight: bold } /* Keyword.Namespace */ .highlight .kp { color: #008800 } /* Keyword.Pseudo */ .highlight .kr { color: #008800; font-weight: bold } /* Keyword.Reserved */ .highlight .kt { color: #888888; font-weight: bold } /* Keyword.Type */ .highlight .m { color: #0000DD; font-weight: bold } /* Literal.Number */ .highlight .s { color: #dd2200; background-color: #fff0f0 } /* Literal.String */ .highlight .na { color: #336699 } /* Name.Attribute */ .highlight .nb { color: #003388 } /* Name.Builtin */ .highlight .nc { color: #bb0066; font-weight: bold } /* Name.Class */ .highlight .no { color: #003366; font-weight: bold } /* Name.Constant */ .highlight .nd { color: #555555 } /* Name.Decorator */ .highlight .ne { color: #bb0066; font-weight: bold } /* Name.Exception */ .highlight .nf { color: #0066bb; font-weight: bold } /* Name.Function */ .highlight .nl { color: #336699; font-style: italic } /* Name.Label */ .highlight .nn { color: #bb0066; font-weight: bold } /* Name.Namespace */ .highlight .py { color: #336699; font-weight: bold } /* Name.Property */ .highlight .nt { color: #bb0066; font-weight: bold } /* Name.Tag */ .highlight .nv { color: #336699 } /* Name.Variable */ .highlight .ow { color: #008800 } /* Operator.Word */ .highlight .w { color: #bbbbbb } /* Text.Whitespace */ .highlight .mb { color: #0000DD; font-weight: bold } /* Literal.Number.Bin */ .highlight .mf { color: #0000DD; font-weight: bold } /* Literal.Number.Float */ .highlight .mh { color: #0000DD; font-weight: bold } /* Literal.Number.Hex */ .highlight .mi { color: #0000DD; font-weight: bold } /* Literal.Number.Integer */ .highlight .mo { color: #0000DD; font-weight: bold } /* Literal.Number.Oct */ .highlight .sa { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Affix */ .highlight .sb { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Backtick */ .highlight .sc { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Char */ .highlight .dl { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Delimiter */ .highlight .sd { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Doc */ .highlight .s2 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Double */ .highlight .se { color: #0044dd; background-color: #fff0f0 } /* Literal.String.Escape */ .highlight .sh { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Heredoc */ .highlight .si { color: #3333bb; background-color: #fff0f0 } /* Literal.String.Interpol */ .highlight .sx { color: #22bb22; background-color: #f0fff0 } /* Literal.String.Other */ .highlight .sr { color: #008800; background-color: #fff0ff } /* Literal.String.Regex */ .highlight .s1 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Single */ .highlight .ss { color: #aa6600; background-color: #fff0f0 } /* Literal.String.Symbol */ .highlight .bp { color: #003388 } /* Name.Builtin.Pseudo */ .highlight .fm { color: #0066bb; font-weight: bold } /* Name.Function.Magic */ .highlight .vc { color: #336699 } /* Name.Variable.Class */ .highlight .vg { color: #dd7700 } /* Name.Variable.Global */ .highlight .vi { color: #3333bb } /* Name.Variable.Instance */ .highlight .vm { color: #336699 } /* Name.Variable.Magic */ .highlight .il { color: #0000DD; font-weight: bold } /* Literal.Number.Integer.Long */% 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 '} 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 : -- :}. 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 :} 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 } option. Secondly it is possible to load cell libraries into the design with the {\tt read\_verilog -lib } 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 } 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 /}. 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 }. It can later be recalled using {\tt select @}. In fact, the {\tt @} 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}