diff options
Diffstat (limited to 'manual')
33 files changed, 0 insertions, 2721 deletions
diff --git a/manual/APPNOTE_010_Verilog_to_BLIF.tex b/manual/APPNOTE_010_Verilog_to_BLIF.tex deleted file mode 100644 index 16254d593..000000000 --- a/manual/APPNOTE_010_Verilog_to_BLIF.tex +++ /dev/null @@ -1,466 +0,0 @@ - -% 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} - -\lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=2em,xrightmargin=1em,numbers=left} - -\begin{document} - -\title{Yosys Application Note 010: \\ Converting Verilog to BLIF} -\author{Claire Xenia Wolf \\ November 2013} -\maketitle - -\begin{abstract} -Verilog-2005 is a powerful Hardware Description Language (HDL) that can be used -to easily create complex designs from small HDL code. It is the preferred -method of design entry for many designers\footnote{The other half prefers VHDL, -a very different but -- of course -- equally powerful language.}. - -The Berkeley Logic Interchange Format (BLIF) \cite{blif} is a simple file format for -exchanging sequential logic between programs. It is easy to generate and -easy to parse and is therefore the preferred method of design entry for -many authors of logic synthesis tools. - -Yosys \cite{yosys} is a feature-rich -Open-Source Verilog synthesis tool that can be used to bridge the gap between -the two file formats. It implements most of Verilog-2005 and thus can be used -to import modern behavioral Verilog designs into BLIF-based design flows -without dependencies on proprietary synthesis tools. - -The scope of Yosys goes of course far beyond Verilog logic synthesis. But -it is a useful and important feature and this Application Note will focus -on this aspect of Yosys. -\end{abstract} - -\section{Installation} - -Yosys written in C++ (using features from C++11) and is tested on modern Linux. -It should compile fine on most UNIX systems with a C++11 compiler. The README -file contains useful information on building Yosys and its prerequisites. - -Yosys is a large and feature-rich program with a couple of dependencies. It is, -however, possible to deactivate some of the dependencies in the Makefile, -resulting in features in Yosys becoming unavailable. When problems with building -Yosys are encountered, a user who is only interested in the features of Yosys -that are discussed in this Application Note may deactivate {\tt TCL}, {\tt Qt} -and {\tt MiniSAT} support in the {\tt Makefile} and may opt against building -{\tt yosys-abc}. - -\bigskip - -This Application Note is based on GIT Rev. {\tt e216e0e} from 2013-11-23 of -Yosys \cite{yosys}. The Verilog sources used for the examples are taken from -yosys-bigsim \cite{bigsim}, a collection of real-world designs used for -regression testing Yosys. - -\section{Getting Started} - -We start our tour with the Navr\'e processor from yosys-bigsim. The Navr\'e -processor \cite{navre} is an Open Source AVR clone. It is a single module ({\tt -softusb\_navre}) in a single design file ({\tt softusb\_navre.v}). It also is -using only features that map nicely to the BLIF format, for example it only -uses synchronous resets. - -Converting {\tt softusb\_navre.v} to {\tt softusb\_navre.blif} could not be -easier: - -\begin{figure}[H] -\begin{lstlisting}[language=sh] -yosys -o softusb_navre.blif -S softusb_navre.v -\end{lstlisting} - \renewcommand{\figurename}{Listing} -\caption{Calling Yosys without script file} -\end{figure} - -Behind the scenes Yosys is controlled by synthesis scripts that execute -commands that operate on Yosys' internal state. For example, the {\tt -o -softusb\_navre.blif} option just adds the command {\tt write\_blif -softusb\_navre.blif} to the end of the script. Likewise a file on the -command line -- {\tt softusb\_navre.v} in this case -- adds the command -{\tt read\_verilog softusb\_navre.v} to the beginning of the -synthesis script. In both cases the file type is detected from the -file extension. - -Finally the option {\tt -S} instantiates a built-in default synthesis script. -Instead of using {\tt -S} one could also specify the synthesis commands -for the script on the command line using the {\tt -p} option, either using -individual options for each command or by passing one big command string -with a semicolon-separated list of commands. But in most cases it is more -convenient to use an actual script file. - -\section{Using a Synthesis Script} - -With a script file we have better control over Yosys. The following script -file replicates what the command from the last section did: - -\begin{figure}[H] -\begin{lstlisting}[language=sh] -read_verilog softusb_navre.v -hierarchy -proc; opt; memory; opt; techmap; opt -write_blif softusb_navre.blif -\end{lstlisting} - \renewcommand{\figurename}{Listing} -\caption{\tt softusb\_navre.ys} -\end{figure} - -The first and last line obviously read the Verilog file and write the BLIF -file. - -\medskip - -The 2nd line checks the design hierarchy and instantiates parametrized -versions of the modules in the design, if necessary. In the case of this -simple design this is a no-op. However, as a general rule a synthesis script -should always contain this command as first command after reading the input -files. - -\medskip - -The 3rd line does most of the actual work: - -\begin{itemize} -\item The command {\tt opt} is the Yosys' built-in optimizer. It can perform -some simple optimizations such as const-folding and removing unconnected parts -of the design. It is common practice to call opt after each major step in the -synthesis procedure. In cases where too much optimization is not appreciated -(for example when analyzing a design), it is recommended to call {\tt clean} -instead of {\tt opt}. -\item The command {\tt proc} converts {\it processes} (Yosys' internal -representation of Verilog {\tt always}- and {\tt initial}-blocks) to circuits -of multiplexers and storage elements (various types of flip-flops). -\item The command {\tt memory} converts Yosys' internal representations of -arrays and array accesses to multi-port block memories, and then maps this -block memories to address decoders and flip-flops, unless the option {\tt -nomap} -is used, in which case the multi-port block memories stay in the design -and can then be mapped to architecture-specific memory primitives using -other commands. -\item The command {\tt techmap} turns a high-level circuit with coarse grain -cells such as wide adders and multipliers to a fine-grain circuit of simple -logic primitives and single-bit storage elements. The command does that by -substituting the complex cells by circuits of simpler cells. It is possible -to provide a custom set of rules for this process in the form of a Verilog -source file, as we will see in the next section. -\end{itemize} - -Now Yosys can be run with the filename of the synthesis script as argument: - -\begin{figure}[H] -\begin{lstlisting}[language=sh] -yosys softusb_navre.ys -\end{lstlisting} - \renewcommand{\figurename}{Listing} -\caption{Calling Yosys with script file} -\end{figure} - -\medskip - -Now that we are using a synthesis script we can easily modify how Yosys -synthesizes the design. The first thing we should customize is the -call to the {\tt hierarchy} command: - -Whenever it is known that there are no implicit blackboxes in the design, i.e. -modules that are referenced but are not defined, the {\tt hierarchy} command -should be called with the {\tt -check} option. This will then cause synthesis -to fail when implicit blackboxes are found in the design. - -The 2nd thing we can improve regarding the {\tt hierarchy} command is that we -can tell it the name of the top level module of the design hierarchy. It will -then automatically remove all modules that are not referenced from this top -level module. - -\medskip - -For many designs it is also desired to optimize the encodings for the finite -state machines (FSMs) in the design. The {\tt fsm} command finds FSMs, extracts -them, performs some basic optimizations and then generate a circuit from -the extracted and optimized description. It would also be possible to tell -the {\tt fsm} command to leave the FSMs in their extracted form, so they can be -further processed using custom commands. But in this case we don't want that. - -\medskip - -So now we have the final synthesis script for generating a BLIF file -for the Navr\'e CPU: - -\begin{figure}[H] -\begin{lstlisting}[language=sh] -read_verilog softusb_navre.v -hierarchy -check -top softusb_navre -proc; opt; memory; opt; fsm; opt; techmap; opt -write_blif softusb_navre.blif -\end{lstlisting} - \renewcommand{\figurename}{Listing} -\caption{{\tt softusb\_navre.ys} (improved)} -\end{figure} - -\section{Advanced Example: The Amber23 ARMv2a CPU} - -Our 2nd example is the Amber23 \cite{amber} -ARMv2a CPU. Once again we base our example on the Verilog code that is included -in yosys-bigsim \cite{bigsim}. - -\begin{figure}[b!] -\begin{lstlisting}[language=sh] -read_verilog a23_alu.v -read_verilog a23_barrel_shift_fpga.v -read_verilog a23_barrel_shift.v -read_verilog a23_cache.v -read_verilog a23_coprocessor.v -read_verilog a23_core.v -read_verilog a23_decode.v -read_verilog a23_execute.v -read_verilog a23_fetch.v -read_verilog a23_multiply.v -read_verilog a23_ram_register_bank.v -read_verilog a23_register_bank.v -read_verilog a23_wishbone.v -read_verilog generic_sram_byte_en.v -read_verilog generic_sram_line_en.v -hierarchy -check -top a23_core -add -global_input globrst 1 -proc -global_arst globrst -techmap -map adff2dff.v -opt; memory; opt; fsm; opt; techmap -write_blif amber23.blif -\end{lstlisting} - \renewcommand{\figurename}{Listing} -\caption{\tt amber23.ys} -\label{aber23.ys} -\end{figure} - -The problem with this core is that it contains no dedicated reset logic. -Instead the coding techniques shown in Listing~\ref{glob_arst} are used to -define reset values for the global asynchronous reset in an FPGA -implementation. This design can not be expressed in BLIF as it is. Instead we -need to use a synthesis script that transforms this form to synchronous resets that -can be expressed in BLIF. - -(Note that there is no problem if this coding techniques are used to model -ROM, where the register is initialized using this syntax but is never updated -otherwise.) - -\medskip - -Listing~\ref{aber23.ys} shows the synthesis script for the Amber23 core. In -line 17 the {\tt add} command is used to add a 1-bit wide global input signal -with the name {\tt globrst}. That means that an input with that name is added -to each module in the design hierarchy and then all module instantiations are -altered so that this new signal is connected throughout the whole design -hierarchy. - -\begin{figure}[t!] -\begin{lstlisting}[language=Verilog] -reg [7:0] a = 13, b; -initial b = 37; -\end{lstlisting} - \renewcommand{\figurename}{Listing} -\caption{Implicit coding of global asynchronous resets} -\label{glob_arst} -\end{figure} - -\begin{figure}[b!] -\begin{lstlisting}[language=Verilog] -(* techmap_celltype = "$adff" *) -module adff2dff (CLK, ARST, D, Q); - -parameter WIDTH = 1; -parameter CLK_POLARITY = 1; -parameter ARST_POLARITY = 1; -parameter ARST_VALUE = 0; - -input CLK, ARST; -input [WIDTH-1:0] D; -output reg [WIDTH-1:0] Q; - -wire [1023:0] _TECHMAP_DO_ = "proc"; - -wire _TECHMAP_FAIL_ = - !CLK_POLARITY || !ARST_POLARITY; - -always @(posedge CLK) - if (ARST) - Q <= ARST_VALUE; - else - Q <= D; - -endmodule -\end{lstlisting} -\renewcommand{\figurename}{Listing} -\caption{\tt adff2dff.v} -\label{adff2dff.v} -\end{figure} - -In line 18 the {\tt proc} command is called. But in this script the signal name -{\tt globrst} is passed to the command as a global reset signal for resetting -the registers to their assigned initial values. - -Finally in line 19 the {\tt techmap} command is used to replace all instances -of flip-flops with asynchronous resets with flip-flops with synchronous resets. -The map file used for this is shown in Listing~\ref{adff2dff.v}. Note how the -{\tt techmap\_celltype} attribute is used in line 1 to tell the techmap command -which cells to replace in the design, how the {\tt \_TECHMAP\_FAIL\_} wire in -lines 15 and 16 (which evaluates to a constant value) determines if the -parameter set is compatible with this replacement circuit, and how the {\tt -\_TECHMAP\_DO\_} wire in line 13 provides a mini synthesis-script to be used to -process this cell. - -\begin{figure*} -\begin{lstlisting}[language=C] -#include <stdint.h> -#include <stdbool.h> - -#define BITMAP_SIZE 64 -#define OUTPORT 0x10000000 - -static uint32_t bitmap[BITMAP_SIZE/32]; - -static void bitmap_set(uint32_t idx) { bitmap[idx/32] |= 1 << (idx % 32); } -static bool bitmap_get(uint32_t idx) { return (bitmap[idx/32] & (1 << (idx % 32))) != 0; } -static void output(uint32_t val) { *((volatile uint32_t*)OUTPORT) = val; } - -int main() { - uint32_t i, j, k; - output(2); - for (i = 0; i < BITMAP_SIZE; i++) { - if (bitmap_get(i)) continue; - output(3+2*i); - for (j = 2*(3+2*i);; j += 3+2*i) { - if (j%2 == 0) continue; - k = (j-3)/2; - if (k >= BITMAP_SIZE) break; - bitmap_set(k); - } - } - output(0); - return 0; -} -\end{lstlisting} -\renewcommand{\figurename}{Listing} -\caption{Test program for the Amber23 CPU (Sieve of Eratosthenes). Compiled using -GCC 4.6.3 for ARM with {\tt -Os -marm -march=armv2a -mno-thumb-interwork --ffreestanding}, linked with {\tt -{}-fix-v4bx} set and booted with a custom -setup routine written in ARM assembler.} -\label{sieve} -\end{figure*} - -\section{Verification of the Amber23 CPU} - -The BLIF file for the Amber23 core, generated using Listings~\ref{aber23.ys} -and \ref{adff2dff.v} and the version of the Amber23 RTL source that is bundled -with yosys-bigsim, was verified using the test-bench from yosys-bigsim. -It successfully executed the program shown in Listing~\ref{sieve} in the -test-bench. - -For simulation the BLIF file was converted back to Verilog using ABC -\cite{ABC}. So this test includes the successful transformation of the BLIF -file into ABC's internal format as well. - -The only thing left to write about the simulation itself is that it probably -was one of the most energy inefficient and time consuming ways of successfully -calculating the first 31 primes the author has ever conducted. - -\section{Limitations} - -At the time of this writing Yosys does not support multi-dimensional memories, -does not support writing to individual bits of array elements, does not -support initialization of arrays with {\tt \$readmemb} and {\tt \$readmemh}, -and has only limited support for tristate logic, to name just a few -limitations. - -That being said, Yosys can synthesize an overwhelming majority of real-world -Verilog RTL code. The remaining cases can usually be modified to be compatible -with Yosys quite easily. - -The various designs in yosys-bigsim are a good place to look for examples -of what is within the capabilities of Yosys. - -\section{Conclusion} - -Yosys is a feature-rich Verilog-2005 synthesis tool. It has many uses, but -one is to provide an easy gateway from high-level Verilog code to low-level -logic circuits. - -The command line option {\tt -S} can be used to quickly synthesize Verilog -code to BLIF files without a hassle. - -With custom synthesis scripts it becomes possible to easily perform high-level -optimizations, such as re-encoding FSMs. In some extreme cases, such as the -Amber23 ARMv2 CPU, the more advanced Yosys features can be used to change a -design to fit a certain need without actually touching the RTL code. - -\begin{thebibliography}{9} - -\bibitem{yosys} -Claire Xenia Wolf. The Yosys Open SYnthesis Suite. \\ -\url{https://yosyshq.net/yosys/} - -\bibitem{bigsim} -yosys-bigsim, a collection of real-world Verilog designs for regression testing purposes. \\ -\url{https://github.com/YosysHQ/yosys-bigsim} - -\bibitem{navre} -Sebastien Bourdeauducq. Navr\'e AVR clone (8-bit RISC). \\ -\url{http://opencores.org/project,navre} - -\bibitem{amber} -Conor Santifort. Amber ARM-compatible core. \\ -\url{http://opencores.org/project,amber} - -\bibitem{ABC} -Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. \\ -\url{http://www.eecs.berkeley.edu/~alanmi/abc/} - -\bibitem{blif} -Berkeley Logic Interchange Format (BLIF) \\ -\url{http://vlsi.colorado.edu/~vis/blif.ps} - -\end{thebibliography} - - -\end{document} diff --git a/manual/APPNOTE_011_Design_Investigation.tex b/manual/APPNOTE_011_Design_Investigation.tex deleted file mode 100644 index 881212fe9..000000000 --- a/manual/APPNOTE_011_Design_Investigation.tex +++ /dev/null @@ -1,1070 +0,0 @@ - -% 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{Claire Xenia Wolf \\ Original Version 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 2b90ba1} from -2013-12-08. The {\tt README} file covers how to install Yosys. The -{\tt show} command requires a working installation of GraphViz \cite{graphviz} -and \cite{xdot} for generating the actual circuit diagrams. - -\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 xdot} to display the diagram. -Subsequent calls to {\tt show} re-use the {\tt xdot} 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 {\tt dot} file and launches -{\tt xdot} 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 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 shown 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 - - Assumed undef (x) value for the following signals: \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} -Claire Xenia Wolf. The Yosys Open SYnthesis Suite. -\url{https://yosyshq.net/yosys/} - -\bibitem{graphviz} -Graphviz - Graph Visualization Software. -\url{http://www.graphviz.org/} - -\bibitem{xdot} -xdot.py - an interactive viewer for graphs written in Graphviz's dot language. -\url{https://github.com/jrfonseca/xdot.py} - -\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\"orensson (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} diff --git a/manual/APPNOTE_011_Design_Investigation/cmos.v b/manual/APPNOTE_011_Design_Investigation/cmos.v deleted file mode 100644 index 2912c760a..000000000 --- a/manual/APPNOTE_011_Design_Investigation/cmos.v +++ /dev/null @@ -1,3 +0,0 @@ -module cmos_demo(input a, b, output [1:0] y); -assign y = a + b; -endmodule diff --git a/manual/APPNOTE_011_Design_Investigation/cmos_00.dot b/manual/APPNOTE_011_Design_Investigation/cmos_00.dot deleted file mode 100644 index 49c630080..000000000 --- a/manual/APPNOTE_011_Design_Investigation/cmos_00.dot +++ /dev/null @@ -1,34 +0,0 @@ -digraph "cmos_demo" { -rankdir="LR"; -remincross=true; -n4 [ shape=octagon, label="a", color="black", fontcolor="black" ]; -n5 [ shape=octagon, label="b", color="black", fontcolor="black" ]; -n6 [ shape=octagon, label="y", color="black", fontcolor="black" ]; -c10 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g0\nNOR|{}}" ]; -c11 [ shape=record, label="{{<p7> A|<p9> Y}|$g1\nNOT|{}}" ]; -c12 [ shape=record, label="{{<p7> A|<p9> Y}|$g2\nNOT|{}}" ]; -c13 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g3\nNOR|{}}" ]; -x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ]; -x0:e -> c13:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""]; -c14 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g4\nNOR|{}}" ]; -x1 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ]; -x1:e -> c14:p8:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""]; -x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ]; -x2:e -> c14:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""]; -n1 [ shape=diamond, label="$n4" ]; -n1:e -> c10:p9:w [color="black", label=""]; -n1:e -> c14:p7:w [color="black", label=""]; -n2 [ shape=diamond, label="$n5" ]; -n2:e -> c11:p9:w [color="black", label=""]; -n2:e -> c13:p7:w [color="black", label=""]; -n3 [ shape=diamond, label="$n6_1" ]; -n3:e -> c12:p9:w [color="black", label=""]; -n3:e -> c13:p8:w [color="black", label=""]; -n4:e -> c10:p8:w [color="black", label=""]; -n4:e -> c12:p7:w [color="black", label=""]; -n5:e -> c10:p7:w [color="black", label=""]; -n5:e -> c11:p7:w [color="black", label=""]; -n6:e -> x0:s0:w [color="black", label=""]; -n6:e -> x1:s0:w [color="black", label=""]; -n6:e -> x2:s0:w [color="black", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/cmos_01.dot b/manual/APPNOTE_011_Design_Investigation/cmos_01.dot deleted file mode 100644 index ea6f4403c..000000000 --- a/manual/APPNOTE_011_Design_Investigation/cmos_01.dot +++ /dev/null @@ -1,23 +0,0 @@ -digraph "cmos_demo" { -rankdir="LR"; -remincross=true; -n4 [ shape=octagon, label="a", color="black", fontcolor="black" ]; -n5 [ shape=octagon, label="b", color="black", fontcolor="black" ]; -n6 [ shape=octagon, label="y[0]", color="black", fontcolor="black" ]; -n7 [ shape=octagon, label="y[1]", color="black", fontcolor="black" ]; -c11 [ shape=record, label="{{<p8> A|<p9> B}|$g0\nNOR|{<p10> Y}}" ]; -c12 [ shape=record, label="{{<p8> A}|$g1\nNOT|{<p10> Y}}" ]; -c13 [ shape=record, label="{{<p8> A}|$g2\nNOT|{<p10> Y}}" ]; -c14 [ shape=record, label="{{<p8> A|<p9> B}|$g3\nNOR|{<p10> Y}}" ]; -c15 [ shape=record, label="{{<p8> A|<p9> B}|$g4\nNOR|{<p10> Y}}" ]; -c11:p10:e -> c15:p8:w [color="black", label=""]; -c12:p10:e -> c14:p8:w [color="black", label=""]; -c13:p10:e -> c14:p9:w [color="black", label=""]; -n4:e -> c11:p9:w [color="black", label=""]; -n4:e -> c13:p8:w [color="black", label=""]; -n5:e -> c11:p8:w [color="black", label=""]; -n5:e -> c12:p8:w [color="black", label=""]; -c15:p10:e -> n6:w [color="black", label=""]; -c14:p10:e -> n7:w [color="black", label=""]; -n7:e -> c15:p9:w [color="black", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/example.v b/manual/APPNOTE_011_Design_Investigation/example.v deleted file mode 100644 index 8c71989b3..000000000 --- a/manual/APPNOTE_011_Design_Investigation/example.v +++ /dev/null @@ -1,6 +0,0 @@ -module example(input clk, a, b, c, - output reg [1:0] y); - always @(posedge clk) - if (c) - y <= c ? a + b : 2'd0; -endmodule diff --git a/manual/APPNOTE_011_Design_Investigation/example.ys b/manual/APPNOTE_011_Design_Investigation/example.ys deleted file mode 100644 index b1e956088..000000000 --- a/manual/APPNOTE_011_Design_Investigation/example.ys +++ /dev/null @@ -1,11 +0,0 @@ -read_verilog example.v -show -format dot -prefix example_00 -proc -show -format dot -prefix example_01 -opt -show -format dot -prefix example_02 - -cd example -select t:$add -show -format dot -prefix example_03 - diff --git a/manual/APPNOTE_011_Design_Investigation/example_00.dot b/manual/APPNOTE_011_Design_Investigation/example_00.dot deleted file mode 100644 index 1e23ed0ea..000000000 --- a/manual/APPNOTE_011_Design_Investigation/example_00.dot +++ /dev/null @@ -1,23 +0,0 @@ -digraph "example" { -rankdir="LR"; -remincross=true; -n4 [ shape=octagon, label="a", color="black", fontcolor="black" ]; -n5 [ shape=octagon, label="b", color="black", fontcolor="black" ]; -n6 [ shape=octagon, label="c", color="black", fontcolor="black" ]; -n7 [ shape=octagon, label="clk", color="black", fontcolor="black" ]; -n8 [ shape=octagon, label="y", color="black", fontcolor="black" ]; -c12 [ shape=record, label="{{<p9> A|<p10> B}|$2\n$add|{<p11> Y}}" ]; -v0 [ label="2'00" ]; -c14 [ shape=record, label="{{<p9> A|<p10> B|<p13> S}|$3\n$mux|{<p11> Y}}" ]; -p1 [shape=box, style=rounded, label="PROC $1\nexample.v:3"]; -c12:p11:e -> c14:p10:w [color="black", style="setlinewidth(3)", label=""]; -c14:p11:e -> p1:w [color="black", style="setlinewidth(3)", label=""]; -n4:e -> c12:p9:w [color="black", label=""]; -n5:e -> c12:p10:w [color="black", label=""]; -n6:e -> c14:p13:w [color="black", label=""]; -n6:e -> p1:w [color="black", label=""]; -n7:e -> p1:w [color="black", label=""]; -p1:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; -n8:e -> p1:w [color="black", style="setlinewidth(3)", label=""]; -v0:e -> c14:p9:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/example_01.dot b/manual/APPNOTE_011_Design_Investigation/example_01.dot deleted file mode 100644 index e89292b51..000000000 --- a/manual/APPNOTE_011_Design_Investigation/example_01.dot +++ /dev/null @@ -1,33 +0,0 @@ -digraph "example" { -rankdir="LR"; -remincross=true; -n6 [ shape=octagon, label="a", color="black", fontcolor="black" ]; -n7 [ shape=octagon, label="b", color="black", fontcolor="black" ]; -n8 [ shape=octagon, label="c", color="black", fontcolor="black" ]; -n9 [ shape=octagon, label="clk", color="black", fontcolor="black" ]; -n10 [ shape=octagon, label="y", color="black", fontcolor="black" ]; -c14 [ shape=record, label="{{<p11> A|<p12> B}|$2\n$add|{<p13> Y}}" ]; -c18 [ shape=record, label="{{<p15> CLK|<p16> D}|$7\n$dff|{<p17> Q}}" ]; -c20 [ shape=record, label="{{<p11> A|<p12> B|<p19> S}|$5\n$mux|{<p13> Y}}" ]; -v0 [ label="2'00" ]; -c21 [ shape=record, label="{{<p11> A|<p12> B|<p19> S}|$3\n$mux|{<p13> Y}}" ]; -x1 [shape=box, style=rounded, label="BUF"]; -x2 [shape=box, style=rounded, label="BUF"]; -n1 [ shape=diamond, label="$0\\y[1:0]" ]; -x2:e:e -> n1:w [color="black", style="setlinewidth(3)", label=""]; -c18:p17:e -> n10:w [color="black", style="setlinewidth(3)", label=""]; -n10:e -> c20:p11:w [color="black", style="setlinewidth(3)", label=""]; -c14:p13:e -> c21:p12:w [color="black", style="setlinewidth(3)", label=""]; -n3 [ shape=point ]; -c20:p13:e -> n3:w [color="black", style="setlinewidth(3)", label=""]; -n3:e -> c18:p16:w [color="black", style="setlinewidth(3)", label=""]; -n3:e -> x2:w:w [color="black", style="setlinewidth(3)", label=""]; -x1:e:e -> c20:p19:w [color="black", label=""]; -c21:p13:e -> c20:p12:w [color="black", style="setlinewidth(3)", label=""]; -n6:e -> c14:p11:w [color="black", label=""]; -n7:e -> c14:p12:w [color="black", label=""]; -n8:e -> c21:p19:w [color="black", label=""]; -n8:e -> x1:w:w [color="black", label=""]; -n9:e -> c18:p15:w [color="black", label=""]; -v0:e -> c21:p11:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/example_02.dot b/manual/APPNOTE_011_Design_Investigation/example_02.dot deleted file mode 100644 index f950ed2ed..000000000 --- a/manual/APPNOTE_011_Design_Investigation/example_02.dot +++ /dev/null @@ -1,20 +0,0 @@ -digraph "example" { -rankdir="LR"; -remincross=true; -n3 [ shape=octagon, label="a", color="black", fontcolor="black" ]; -n4 [ shape=octagon, label="b", color="black", fontcolor="black" ]; -n5 [ shape=octagon, label="c", color="black", fontcolor="black" ]; -n6 [ shape=octagon, label="clk", color="black", fontcolor="black" ]; -n7 [ shape=octagon, label="y", color="black", fontcolor="black" ]; -c11 [ shape=record, label="{{<p8> A|<p9> B}|$2\n$add|{<p10> Y}}" ]; -c15 [ shape=record, label="{{<p12> CLK|<p13> D}|$7\n$dff|{<p14> Q}}" ]; -c17 [ shape=record, label="{{<p8> A|<p9> B|<p16> S}|$5\n$mux|{<p10> Y}}" ]; -c17:p10:e -> c15:p13:w [color="black", style="setlinewidth(3)", label=""]; -c11:p10:e -> c17:p9:w [color="black", style="setlinewidth(3)", label=""]; -n3:e -> c11:p8:w [color="black", label=""]; -n4:e -> c11:p9:w [color="black", label=""]; -n5:e -> c17:p16:w [color="black", label=""]; -n6:e -> c15:p12:w [color="black", label=""]; -c15:p14:e -> n7:w [color="black", style="setlinewidth(3)", label=""]; -n7:e -> c17:p8:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/example_03.dot b/manual/APPNOTE_011_Design_Investigation/example_03.dot deleted file mode 100644 index e19d24af7..000000000 --- a/manual/APPNOTE_011_Design_Investigation/example_03.dot +++ /dev/null @@ -1,11 +0,0 @@ -digraph "example" { -rankdir="LR"; -remincross=true; -v0 [ label="a" ]; -v1 [ label="b" ]; -v2 [ label="$2_Y" ]; -c4 [ shape=record, label="{{<p1> A|<p2> B}|$2\n$add|{<p3> Y}}" ]; -v0:e -> c4:p1:w [color="black", label=""]; -v1:e -> c4:p2:w [color="black", label=""]; -c4:p3:e -> v2:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/foobaraddsub.v b/manual/APPNOTE_011_Design_Investigation/foobaraddsub.v deleted file mode 100644 index 0f277211d..000000000 --- a/manual/APPNOTE_011_Design_Investigation/foobaraddsub.v +++ /dev/null @@ -1,8 +0,0 @@ -module foobaraddsub(a, b, c, d, fa, fs, ba, bs); - input [7:0] a, b, c, d; - output [7:0] fa, fs, ba, bs; - assign fa = a + (* foo *) b; - assign fs = a - (* foo *) b; - assign ba = c + (* bar *) d; - assign bs = c - (* bar *) d; -endmodule diff --git a/manual/APPNOTE_011_Design_Investigation/make.sh b/manual/APPNOTE_011_Design_Investigation/make.sh deleted file mode 100644 index 3845dac6b..000000000 --- a/manual/APPNOTE_011_Design_Investigation/make.sh +++ /dev/null @@ -1,23 +0,0 @@ -#!/bin/bash -set -ex -if false; then - rm -f *.dot - ../../yosys example.ys - ../../yosys -p 'proc; opt; show -format dot -prefix splice' splice.v - ../../yosys -p 'techmap; abc -liberty ../../techlibs/cmos/cmos_cells.lib;; show -format dot -prefix cmos_00' cmos.v - ../../yosys -p 'techmap; splitnets -ports; abc -liberty ../../techlibs/cmos/cmos_cells.lib;; show -lib ../../techlibs/cmos/cmos_cells.v -format dot -prefix cmos_01' cmos.v - ../../yosys -p 'opt; cd sumprod; select a:sumstuff; show -format dot -prefix sumprod_00' sumprod.v - ../../yosys -p 'opt; cd sumprod; select a:sumstuff %x; show -format dot -prefix sumprod_01' sumprod.v - ../../yosys -p 'opt; cd sumprod; select prod; show -format dot -prefix sumprod_02' sumprod.v - ../../yosys -p 'opt; cd sumprod; select prod %ci; show -format dot -prefix sumprod_03' sumprod.v - ../../yosys -p 'opt; cd sumprod; select prod %ci2; show -format dot -prefix sumprod_04' sumprod.v - ../../yosys -p 'opt; cd sumprod; select prod %ci3; show -format dot -prefix sumprod_05' sumprod.v - ../../yosys -p 'proc; opt; memory; opt; cd memdemo; show -format dot -prefix memdemo_00' memdemo.v - ../../yosys -p 'proc; opt; memory; opt; cd memdemo; show -format dot -prefix memdemo_01 y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff' memdemo.v - ../../yosys submod.ys - sed -i '/^label=/ d;' *.dot -fi -for dot_file in *.dot; do - pdf_file=${dot_file%.dot}.pdf - dot -Tpdf -o $pdf_file $dot_file -done diff --git a/manual/APPNOTE_011_Design_Investigation/memdemo.v b/manual/APPNOTE_011_Design_Investigation/memdemo.v deleted file mode 100644 index b39564ddc..000000000 --- a/manual/APPNOTE_011_Design_Investigation/memdemo.v +++ /dev/null @@ -1,19 +0,0 @@ -module memdemo(clk, d, y); - -input clk; -input [3:0] d; -output reg [3:0] y; - -integer i; -reg [1:0] s1, s2; -reg [3:0] mem [0:3]; - -always @(posedge clk) begin - for (i = 0; i < 4; i = i+1) - mem[i] <= mem[(i+1) % 4] + mem[(i+2) % 4]; - { s2, s1 } = d ? { s1, s2 } ^ d : 4'b0; - mem[s1] <= d; - y <= mem[s2]; -end - -endmodule diff --git a/manual/APPNOTE_011_Design_Investigation/memdemo_00.dot b/manual/APPNOTE_011_Design_Investigation/memdemo_00.dot deleted file mode 100644 index 0336a9aac..000000000 --- a/manual/APPNOTE_011_Design_Investigation/memdemo_00.dot +++ /dev/null @@ -1,138 +0,0 @@ -digraph "memdemo" { -rankdir="LR"; -remincross=true; -n24 [ shape=octagon, label="clk", color="black", fontcolor="black" ]; -n25 [ shape=octagon, label="d", color="black", fontcolor="black" ]; -n26 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ]; -n27 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ]; -n28 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ]; -n29 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ]; -n30 [ shape=diamond, label="s1", color="black", fontcolor="black" ]; -n31 [ shape=diamond, label="s2", color="black", fontcolor="black" ]; -n32 [ shape=octagon, label="y", color="black", fontcolor="black" ]; -c36 [ shape=record, label="{{<p33> A|<p34> B}|$28\n$add|{<p35> Y}}" ]; -c37 [ shape=record, label="{{<p33> A|<p34> B}|$31\n$add|{<p35> Y}}" ]; -c38 [ shape=record, label="{{<p33> A|<p34> B}|$34\n$add|{<p35> Y}}" ]; -c39 [ shape=record, label="{{<p33> A|<p34> B}|$37\n$add|{<p35> Y}}" ]; -c41 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$110\n$mux|{<p35> Y}}" ]; -x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ]; -x0:e -> c41:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""]; -c42 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$113\n$mux|{<p35> Y}}" ]; -x1 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ]; -x1:e -> c42:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""]; -c43 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$116\n$mux|{<p35> Y}}" ]; -x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ]; -x2:e -> c43:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""]; -v3 [ label="1'1" ]; -c44 [ shape=record, label="{{<p33> A|<p34> B}|$145\n$and|{<p35> Y}}" ]; -v4 [ label="1'1" ]; -c45 [ shape=record, label="{{<p33> A|<p34> B}|$175\n$and|{<p35> Y}}" ]; -v5 [ label="1'1" ]; -c46 [ shape=record, label="{{<p33> A|<p34> B}|$205\n$and|{<p35> Y}}" ]; -v6 [ label="1'1" ]; -c47 [ shape=record, label="{{<p33> A|<p34> B}|$235\n$and|{<p35> Y}}" ]; -v7 [ label="2'00" ]; -c48 [ shape=record, label="{{<p33> A|<p34> B}|$143\n$eq|{<p35> Y}}" ]; -v8 [ label="2'01" ]; -c49 [ shape=record, label="{{<p33> A|<p34> B}|$173\n$eq|{<p35> Y}}" ]; -v9 [ label="2'10" ]; -c50 [ shape=record, label="{{<p33> A|<p34> B}|$203\n$eq|{<p35> Y}}" ]; -v10 [ label="2'11" ]; -c51 [ shape=record, label="{{<p33> A|<p34> B}|$233\n$eq|{<p35> Y}}" ]; -c52 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$147\n$mux|{<p35> Y}}" ]; -c53 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$177\n$mux|{<p35> Y}}" ]; -c54 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$207\n$mux|{<p35> Y}}" ]; -c55 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$237\n$mux|{<p35> Y}}" ]; -c59 [ shape=record, label="{{<p56> CLK|<p57> D}|$66\n$dff|{<p58> Q}}" ]; -c60 [ shape=record, label="{{<p56> CLK|<p57> D}|$68\n$dff|{<p58> Q}}" ]; -c61 [ shape=record, label="{{<p56> CLK|<p57> D}|$70\n$dff|{<p58> Q}}" ]; -c62 [ shape=record, label="{{<p56> CLK|<p57> D}|$72\n$dff|{<p58> Q}}" ]; -c63 [ shape=record, label="{{<p56> CLK|<p57> D}|$59\n$dff|{<p58> Q}}" ]; -c64 [ shape=record, label="{{<p56> CLK|<p57> D}|$63\n$dff|{<p58> Q}}" ]; -c65 [ shape=record, label="{{<p56> CLK|<p57> D}|$64\n$dff|{<p58> Q}}" ]; -c66 [ shape=record, label="{{<p33> A}|$39\n$reduce_bool|{<p35> Y}}" ]; -v11 [ label="4'0000" ]; -c67 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$40\n$mux|{<p35> Y}}" ]; -x12 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 1:0 " ]; -c67:p35:e -> x12:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""]; -c68 [ shape=record, label="{{<p33> A|<p34> B}|$38\n$xor|{<p35> Y}}" ]; -x13 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ]; -x13:e -> c68:p33:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""]; -c36:p35:e -> c52:p33:w [color="black", style="setlinewidth(3)", label=""]; -c44:p35:e -> c52:p40:w [color="black", label=""]; -c45:p35:e -> c53:p40:w [color="black", label=""]; -c46:p35:e -> c54:p40:w [color="black", label=""]; -c47:p35:e -> c55:p40:w [color="black", label=""]; -c48:p35:e -> c44:p33:w [color="black", label=""]; -c49:p35:e -> c45:p33:w [color="black", label=""]; -c50:p35:e -> c46:p33:w [color="black", label=""]; -c51:p35:e -> c47:p33:w [color="black", label=""]; -c52:p35:e -> c59:p57:w [color="black", style="setlinewidth(3)", label=""]; -c53:p35:e -> c60:p57:w [color="black", style="setlinewidth(3)", label=""]; -c37:p35:e -> c53:p33:w [color="black", style="setlinewidth(3)", label=""]; -c54:p35:e -> c61:p57:w [color="black", style="setlinewidth(3)", label=""]; -c55:p35:e -> c62:p57:w [color="black", style="setlinewidth(3)", label=""]; -c66:p35:e -> c67:p40:w [color="black", label=""]; -c68:p35:e -> c67:p34:w [color="black", style="setlinewidth(3)", label=""]; -n24:e -> c59:p56:w [color="black", label=""]; -n24:e -> c60:p56:w [color="black", label=""]; -n24:e -> c61:p56:w [color="black", label=""]; -n24:e -> c62:p56:w [color="black", label=""]; -n24:e -> c63:p56:w [color="black", label=""]; -n24:e -> c64:p56:w [color="black", label=""]; -n24:e -> c65:p56:w [color="black", label=""]; -n25:e -> c52:p34:w [color="black", style="setlinewidth(3)", label=""]; -n25:e -> c53:p34:w [color="black", style="setlinewidth(3)", label=""]; -n25:e -> c54:p34:w [color="black", style="setlinewidth(3)", label=""]; -n25:e -> c55:p34:w [color="black", style="setlinewidth(3)", label=""]; -n25:e -> c66:p33:w [color="black", style="setlinewidth(3)", label=""]; -n25:e -> c68:p34:w [color="black", style="setlinewidth(3)", label=""]; -c59:p58:e -> n26:w [color="black", style="setlinewidth(3)", label=""]; -n26:e -> c38:p34:w [color="black", style="setlinewidth(3)", label=""]; -n26:e -> c39:p33:w [color="black", style="setlinewidth(3)", label=""]; -n26:e -> c42:p33:w [color="black", style="setlinewidth(3)", label=""]; -c60:p58:e -> n27:w [color="black", style="setlinewidth(3)", label=""]; -n27:e -> c36:p33:w [color="black", style="setlinewidth(3)", label=""]; -n27:e -> c39:p34:w [color="black", style="setlinewidth(3)", label=""]; -n27:e -> c42:p34:w [color="black", style="setlinewidth(3)", label=""]; -c61:p58:e -> n28:w [color="black", style="setlinewidth(3)", label=""]; -n28:e -> c36:p34:w [color="black", style="setlinewidth(3)", label=""]; -n28:e -> c37:p33:w [color="black", style="setlinewidth(3)", label=""]; -n28:e -> c43:p33:w [color="black", style="setlinewidth(3)", label=""]; -c62:p58:e -> n29:w [color="black", style="setlinewidth(3)", label=""]; -n29:e -> c37:p34:w [color="black", style="setlinewidth(3)", label=""]; -n29:e -> c38:p33:w [color="black", style="setlinewidth(3)", label=""]; -n29:e -> c43:p34:w [color="black", style="setlinewidth(3)", label=""]; -c38:p35:e -> c54:p33:w [color="black", style="setlinewidth(3)", label=""]; -c63:p58:e -> n30:w [color="black", style="setlinewidth(3)", label=""]; -n30:e -> x13:s1:w [color="black", style="setlinewidth(3)", label=""]; -c64:p58:e -> n31:w [color="black", style="setlinewidth(3)", label=""]; -n31:e -> x13:s0:w [color="black", style="setlinewidth(3)", label=""]; -c65:p58:e -> n32:w [color="black", style="setlinewidth(3)", label=""]; -c39:p35:e -> c55:p33:w [color="black", style="setlinewidth(3)", label=""]; -n5 [ shape=point ]; -x12:s0:e -> n5:w [color="black", style="setlinewidth(3)", label=""]; -n5:e -> c48:p34:w [color="black", style="setlinewidth(3)", label=""]; -n5:e -> c49:p34:w [color="black", style="setlinewidth(3)", label=""]; -n5:e -> c50:p34:w [color="black", style="setlinewidth(3)", label=""]; -n5:e -> c51:p34:w [color="black", style="setlinewidth(3)", label=""]; -n5:e -> c63:p57:w [color="black", style="setlinewidth(3)", label=""]; -n6 [ shape=point ]; -x12:s1:e -> n6:w [color="black", style="setlinewidth(3)", label=""]; -n6:e -> c64:p57:w [color="black", style="setlinewidth(3)", label=""]; -n6:e -> x0:s0:w [color="black", style="setlinewidth(3)", label=""]; -n6:e -> x1:s0:w [color="black", style="setlinewidth(3)", label=""]; -n6:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""]; -c41:p35:e -> c65:p57:w [color="black", style="setlinewidth(3)", label=""]; -c42:p35:e -> c41:p33:w [color="black", style="setlinewidth(3)", label=""]; -c43:p35:e -> c41:p34:w [color="black", style="setlinewidth(3)", label=""]; -v10:e -> c51:p33:w [color="black", style="setlinewidth(3)", label=""]; -v11:e -> c67:p33:w [color="black", style="setlinewidth(3)", label=""]; -v3:e -> c44:p34:w [color="black", label=""]; -v4:e -> c45:p34:w [color="black", label=""]; -v5:e -> c46:p34:w [color="black", label=""]; -v6:e -> c47:p34:w [color="black", label=""]; -v7:e -> c48:p33:w [color="black", style="setlinewidth(3)", label=""]; -v8:e -> c49:p33:w [color="black", style="setlinewidth(3)", label=""]; -v9:e -> c50:p33:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/memdemo_01.dot b/manual/APPNOTE_011_Design_Investigation/memdemo_01.dot deleted file mode 100644 index 2ad92c78b..000000000 --- a/manual/APPNOTE_011_Design_Investigation/memdemo_01.dot +++ /dev/null @@ -1,29 +0,0 @@ -digraph "memdemo" { -rankdir="LR"; -remincross=true; -n4 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ]; -n5 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ]; -n6 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ]; -n7 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ]; -n8 [ shape=octagon, label="y", color="black", fontcolor="black" ]; -v0 [ label="$0\\s2[1:0] [1]" ]; -c13 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$110\n$mux|{<p12> Y}}" ]; -v1 [ label="$0\\s2[1:0] [0]" ]; -c14 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$113\n$mux|{<p12> Y}}" ]; -v2 [ label="$0\\s2[1:0] [0]" ]; -c15 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$116\n$mux|{<p12> Y}}" ]; -v3 [ label="clk" ]; -c19 [ shape=record, label="{{<p16> CLK|<p17> D}|$64\n$dff|{<p18> Q}}" ]; -c13:p12:e -> c19:p17:w [color="black", style="setlinewidth(3)", label=""]; -c14:p12:e -> c13:p9:w [color="black", style="setlinewidth(3)", label=""]; -c15:p12:e -> c13:p10:w [color="black", style="setlinewidth(3)", label=""]; -n4:e -> c14:p9:w [color="black", style="setlinewidth(3)", label=""]; -n5:e -> c14:p10:w [color="black", style="setlinewidth(3)", label=""]; -n6:e -> c15:p9:w [color="black", style="setlinewidth(3)", label=""]; -n7:e -> c15:p10:w [color="black", style="setlinewidth(3)", label=""]; -c19:p18:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; -v0:e -> c13:p11:w [color="black", label=""]; -v1:e -> c14:p11:w [color="black", label=""]; -v2:e -> c15:p11:w [color="black", label=""]; -v3:e -> c19:p16:w [color="black", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/primetest.v b/manual/APPNOTE_011_Design_Investigation/primetest.v deleted file mode 100644 index 6cb766b73..000000000 --- a/manual/APPNOTE_011_Design_Investigation/primetest.v +++ /dev/null @@ -1,4 +0,0 @@ -module primetest(p, a, b, ok); -input [15:0] p, a, b; -output ok = p != a*b || a == 1 || b == 1; -endmodule diff --git a/manual/APPNOTE_011_Design_Investigation/splice.dot b/manual/APPNOTE_011_Design_Investigation/splice.dot deleted file mode 100644 index 4657feed1..000000000 --- a/manual/APPNOTE_011_Design_Investigation/splice.dot +++ /dev/null @@ -1,39 +0,0 @@ -digraph "splice_demo" { -rankdir="LR"; -remincross=true; -n1 [ shape=octagon, label="a", color="black", fontcolor="black" ]; -n2 [ shape=octagon, label="b", color="black", fontcolor="black" ]; -n3 [ shape=octagon, label="c", color="black", fontcolor="black" ]; -n4 [ shape=octagon, label="d", color="black", fontcolor="black" ]; -n5 [ shape=octagon, label="e", color="black", fontcolor="black" ]; -n6 [ shape=octagon, label="f", color="black", fontcolor="black" ]; -n7 [ shape=octagon, label="x", color="black", fontcolor="black" ]; -n8 [ shape=octagon, label="y", color="black", fontcolor="black" ]; -c11 [ shape=record, label="{{<p9> A}|$2\n$neg|{<p10> Y}}" ]; -x0 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ]; -x0:e -> c11:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""]; -x1 [ shape=record, style=rounded, label="<s0> 3:0 - 7:4 " ]; -c11:p10:e -> x1:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""]; -c12 [ shape=record, label="{{<p9> A}|$1\n$not|{<p10> Y}}" ]; -x2 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ]; -x2:e -> c12:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""]; -x3 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 3:2 " ]; -c12:p10:e -> x3:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""]; -x4 [ shape=record, style=rounded, label="<s1> 0:0 - 1:1 |<s0> 1:1 - 0:0 " ]; -x5 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ]; -x6 [ shape=record, style=rounded, label="<s0> 3:0 - 11:8 " ]; -x5:e -> x6:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""]; -n1:e -> x4:s0:w [color="black", style="setlinewidth(3)", label=""]; -n1:e -> x4:s1:w [color="black", style="setlinewidth(3)", label=""]; -n1:e -> x5:s1:w [color="black", style="setlinewidth(3)", label=""]; -n2:e -> x5:s0:w [color="black", style="setlinewidth(3)", label=""]; -n3:e -> x0:s1:w [color="black", style="setlinewidth(3)", label=""]; -n4:e -> x0:s0:w [color="black", style="setlinewidth(3)", label=""]; -n5:e -> x2:s1:w [color="black", style="setlinewidth(3)", label=""]; -n6:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""]; -x4:e -> n7:w [color="black", style="setlinewidth(3)", label=""]; -x1:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; -x3:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; -x3:s1:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; -x6:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/splice.v b/manual/APPNOTE_011_Design_Investigation/splice.v deleted file mode 100644 index 1cf7274c0..000000000 --- a/manual/APPNOTE_011_Design_Investigation/splice.v +++ /dev/null @@ -1,10 +0,0 @@ -module splice_demo(a, b, c, d, e, f, x, y); - -input [1:0] a, b, c, d, e, f; -output [1:0] x = {a[0], a[1]}; - -output [11:0] y; -assign {y[11:4], y[1:0], y[3:2]} = - {a, b, -{c, d}, ~{e, f}}; - -endmodule diff --git a/manual/APPNOTE_011_Design_Investigation/submod.ys b/manual/APPNOTE_011_Design_Investigation/submod.ys deleted file mode 100644 index 29ad61076..000000000 --- a/manual/APPNOTE_011_Design_Investigation/submod.ys +++ /dev/null @@ -1,16 +0,0 @@ -read_verilog memdemo.v -proc; opt; memory; opt - -cd memdemo -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 - -cd .. -show -format dot -prefix submod_00 memdemo -show -format dot -prefix submod_01 scramble -show -format dot -prefix submod_02 outstage -show -format dot -prefix submod_03 selstage diff --git a/manual/APPNOTE_011_Design_Investigation/submod_00.dot b/manual/APPNOTE_011_Design_Investigation/submod_00.dot deleted file mode 100644 index 2e55268ee..000000000 --- a/manual/APPNOTE_011_Design_Investigation/submod_00.dot +++ /dev/null @@ -1,45 +0,0 @@ -digraph "memdemo" { -rankdir="LR"; -remincross=true; -n5 [ shape=octagon, label="clk", color="black", fontcolor="black" ]; -n6 [ shape=octagon, label="d", color="black", fontcolor="black" ]; -n7 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ]; -n8 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ]; -n9 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ]; -n10 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ]; -n11 [ shape=diamond, label="s1", color="black", fontcolor="black" ]; -n12 [ shape=diamond, label="s2", color="black", fontcolor="black" ]; -n13 [ shape=octagon, label="y", color="black", fontcolor="black" ]; -c17 [ shape=record, label="{{<p14> CLK|<p15> D}|$59\n$dff|{<p16> Q}}" ]; -c18 [ shape=record, label="{{<p14> CLK|<p15> D}|$63\n$dff|{<p16> Q}}" ]; -c20 [ shape=record, label="{{<p5> clk|<p7> mem[0]|<p8> mem[1]|<p9> mem[2]|<p10> mem[3]|<p19> n1}|outstage\noutstage|{<p13> y}}" ]; -c21 [ shape=record, label="{{<p5> clk|<p6> d|<p19> n1}|scramble\nscramble|{<p7> mem[0]|<p8> mem[1]|<p9> mem[2]|<p10> mem[3]}}" ]; -c23 [ shape=record, label="{{<p6> d|<p11> s1|<p12> s2}|selstage\nselstage|{<p19> n1|<p22> n2}}" ]; -n1 [ shape=point ]; -c23:p19:e -> n1:w [color="black", style="setlinewidth(3)", label=""]; -n1:e -> c17:p15:w [color="black", style="setlinewidth(3)", label=""]; -n1:e -> c21:p19:w [color="black", style="setlinewidth(3)", label=""]; -c21:p10:e -> n10:w [color="black", style="setlinewidth(3)", label=""]; -n10:e -> c20:p10:w [color="black", style="setlinewidth(3)", label=""]; -c17:p16:e -> n11:w [color="black", style="setlinewidth(3)", label=""]; -n11:e -> c23:p11:w [color="black", style="setlinewidth(3)", label=""]; -c18:p16:e -> n12:w [color="black", style="setlinewidth(3)", label=""]; -n12:e -> c23:p12:w [color="black", style="setlinewidth(3)", label=""]; -c20:p13:e -> n13:w [color="black", style="setlinewidth(3)", label=""]; -n2 [ shape=point ]; -c23:p22:e -> n2:w [color="black", style="setlinewidth(3)", label=""]; -n2:e -> c18:p15:w [color="black", style="setlinewidth(3)", label=""]; -n2:e -> c20:p19:w [color="black", style="setlinewidth(3)", label=""]; -n5:e -> c17:p14:w [color="black", label=""]; -n5:e -> c18:p14:w [color="black", label=""]; -n5:e -> c20:p5:w [color="black", label=""]; -n5:e -> c21:p5:w [color="black", label=""]; -n6:e -> c21:p6:w [color="black", style="setlinewidth(3)", label=""]; -n6:e -> c23:p6:w [color="black", style="setlinewidth(3)", label=""]; -c21:p7:e -> n7:w [color="black", style="setlinewidth(3)", label=""]; -n7:e -> c20:p7:w [color="black", style="setlinewidth(3)", label=""]; -c21:p8:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; -n8:e -> c20:p8:w [color="black", style="setlinewidth(3)", label=""]; -c21:p9:e -> n9:w [color="black", style="setlinewidth(3)", label=""]; -n9:e -> c20:p9:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/submod_01.dot b/manual/APPNOTE_011_Design_Investigation/submod_01.dot deleted file mode 100644 index f8f8c008a..000000000 --- a/manual/APPNOTE_011_Design_Investigation/submod_01.dot +++ /dev/null @@ -1,87 +0,0 @@ -digraph "scramble" { -rankdir="LR"; -remincross=true; -n17 [ shape=octagon, label="clk", color="black", fontcolor="black" ]; -n18 [ shape=octagon, label="d", color="black", fontcolor="black" ]; -n19 [ shape=octagon, label="mem[0]", color="black", fontcolor="black" ]; -n20 [ shape=octagon, label="mem[1]", color="black", fontcolor="black" ]; -n21 [ shape=octagon, label="mem[2]", color="black", fontcolor="black" ]; -n22 [ shape=octagon, label="mem[3]", color="black", fontcolor="black" ]; -n23 [ shape=octagon, label="n1", color="black", fontcolor="black" ]; -c27 [ shape=record, label="{{<p24> A|<p25> B}|$28\n$add|{<p26> Y}}" ]; -c28 [ shape=record, label="{{<p24> A|<p25> B}|$31\n$add|{<p26> Y}}" ]; -c29 [ shape=record, label="{{<p24> A|<p25> B}|$34\n$add|{<p26> Y}}" ]; -c30 [ shape=record, label="{{<p24> A|<p25> B}|$37\n$add|{<p26> Y}}" ]; -v0 [ label="1'1" ]; -c31 [ shape=record, label="{{<p24> A|<p25> B}|$145\n$and|{<p26> Y}}" ]; -v1 [ label="1'1" ]; -c32 [ shape=record, label="{{<p24> A|<p25> B}|$175\n$and|{<p26> Y}}" ]; -v2 [ label="1'1" ]; -c33 [ shape=record, label="{{<p24> A|<p25> B}|$205\n$and|{<p26> Y}}" ]; -v3 [ label="1'1" ]; -c34 [ shape=record, label="{{<p24> A|<p25> B}|$235\n$and|{<p26> Y}}" ]; -v4 [ label="2'00" ]; -c35 [ shape=record, label="{{<p24> A|<p25> B}|$143\n$eq|{<p26> Y}}" ]; -v5 [ label="2'01" ]; -c36 [ shape=record, label="{{<p24> A|<p25> B}|$173\n$eq|{<p26> Y}}" ]; -v6 [ label="2'10" ]; -c37 [ shape=record, label="{{<p24> A|<p25> B}|$203\n$eq|{<p26> Y}}" ]; -v7 [ label="2'11" ]; -c38 [ shape=record, label="{{<p24> A|<p25> B}|$233\n$eq|{<p26> Y}}" ]; -c40 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$147\n$mux|{<p26> Y}}" ]; -c41 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$177\n$mux|{<p26> Y}}" ]; -c42 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$207\n$mux|{<p26> Y}}" ]; -c43 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$237\n$mux|{<p26> Y}}" ]; -c47 [ shape=record, label="{{<p44> CLK|<p45> D}|$66\n$dff|{<p46> Q}}" ]; -c48 [ shape=record, label="{{<p44> CLK|<p45> D}|$68\n$dff|{<p46> Q}}" ]; -c49 [ shape=record, label="{{<p44> CLK|<p45> D}|$70\n$dff|{<p46> Q}}" ]; -c50 [ shape=record, label="{{<p44> CLK|<p45> D}|$72\n$dff|{<p46> Q}}" ]; -c27:p26:e -> c40:p24:w [color="black", style="setlinewidth(3)", label=""]; -c36:p26:e -> c32:p24:w [color="black", label=""]; -c37:p26:e -> c33:p24:w [color="black", label=""]; -c38:p26:e -> c34:p24:w [color="black", label=""]; -c40:p26:e -> c47:p45:w [color="black", style="setlinewidth(3)", label=""]; -c41:p26:e -> c48:p45:w [color="black", style="setlinewidth(3)", label=""]; -c42:p26:e -> c49:p45:w [color="black", style="setlinewidth(3)", label=""]; -c43:p26:e -> c50:p45:w [color="black", style="setlinewidth(3)", label=""]; -n17:e -> c47:p44:w [color="black", label=""]; -n17:e -> c48:p44:w [color="black", label=""]; -n17:e -> c49:p44:w [color="black", label=""]; -n17:e -> c50:p44:w [color="black", label=""]; -n18:e -> c40:p25:w [color="black", style="setlinewidth(3)", label=""]; -n18:e -> c41:p25:w [color="black", style="setlinewidth(3)", label=""]; -n18:e -> c42:p25:w [color="black", style="setlinewidth(3)", label=""]; -n18:e -> c43:p25:w [color="black", style="setlinewidth(3)", label=""]; -c47:p46:e -> n19:w [color="black", style="setlinewidth(3)", label=""]; -n19:e -> c29:p25:w [color="black", style="setlinewidth(3)", label=""]; -n19:e -> c30:p24:w [color="black", style="setlinewidth(3)", label=""]; -c28:p26:e -> c41:p24:w [color="black", style="setlinewidth(3)", label=""]; -c48:p46:e -> n20:w [color="black", style="setlinewidth(3)", label=""]; -n20:e -> c27:p24:w [color="black", style="setlinewidth(3)", label=""]; -n20:e -> c30:p25:w [color="black", style="setlinewidth(3)", label=""]; -c49:p46:e -> n21:w [color="black", style="setlinewidth(3)", label=""]; -n21:e -> c27:p25:w [color="black", style="setlinewidth(3)", label=""]; -n21:e -> c28:p24:w [color="black", style="setlinewidth(3)", label=""]; -c50:p46:e -> n22:w [color="black", style="setlinewidth(3)", label=""]; -n22:e -> c28:p25:w [color="black", style="setlinewidth(3)", label=""]; -n22:e -> c29:p24:w [color="black", style="setlinewidth(3)", label=""]; -n23:e -> c35:p25:w [color="black", style="setlinewidth(3)", label=""]; -n23:e -> c36:p25:w [color="black", style="setlinewidth(3)", label=""]; -n23:e -> c37:p25:w [color="black", style="setlinewidth(3)", label=""]; -n23:e -> c38:p25:w [color="black", style="setlinewidth(3)", label=""]; -c29:p26:e -> c42:p24:w [color="black", style="setlinewidth(3)", label=""]; -c30:p26:e -> c43:p24:w [color="black", style="setlinewidth(3)", label=""]; -c31:p26:e -> c40:p39:w [color="black", label=""]; -c32:p26:e -> c41:p39:w [color="black", label=""]; -c33:p26:e -> c42:p39:w [color="black", label=""]; -c34:p26:e -> c43:p39:w [color="black", label=""]; -c35:p26:e -> c31:p24:w [color="black", label=""]; -v0:e -> c31:p25:w [color="black", label=""]; -v1:e -> c32:p25:w [color="black", label=""]; -v2:e -> c33:p25:w [color="black", label=""]; -v3:e -> c34:p25:w [color="black", label=""]; -v4:e -> c35:p24:w [color="black", style="setlinewidth(3)", label=""]; -v5:e -> c36:p24:w [color="black", style="setlinewidth(3)", label=""]; -v6:e -> c37:p24:w [color="black", style="setlinewidth(3)", label=""]; -v7:e -> c38:p24:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/submod_02.dot b/manual/APPNOTE_011_Design_Investigation/submod_02.dot deleted file mode 100644 index 1a672c484..000000000 --- a/manual/APPNOTE_011_Design_Investigation/submod_02.dot +++ /dev/null @@ -1,33 +0,0 @@ -digraph "outstage" { -rankdir="LR"; -remincross=true; -n4 [ shape=octagon, label="clk", color="black", fontcolor="black" ]; -n5 [ shape=octagon, label="mem[0]", color="black", fontcolor="black" ]; -n6 [ shape=octagon, label="mem[1]", color="black", fontcolor="black" ]; -n7 [ shape=octagon, label="mem[2]", color="black", fontcolor="black" ]; -n8 [ shape=octagon, label="mem[3]", color="black", fontcolor="black" ]; -n9 [ shape=octagon, label="n1", color="black", fontcolor="black" ]; -n10 [ shape=octagon, label="y", color="black", fontcolor="black" ]; -c15 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$110\n$mux|{<p14> Y}}" ]; -x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ]; -x0:e -> c15:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""]; -c16 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$113\n$mux|{<p14> Y}}" ]; -x1 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ]; -x1:e -> c16:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""]; -c17 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$116\n$mux|{<p14> Y}}" ]; -x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ]; -x2:e -> c17:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""]; -c21 [ shape=record, label="{{<p18> CLK|<p19> D}|$64\n$dff|{<p20> Q}}" ]; -c15:p14:e -> c21:p19:w [color="black", style="setlinewidth(3)", label=""]; -c21:p20:e -> n10:w [color="black", style="setlinewidth(3)", label=""]; -c16:p14:e -> c15:p11:w [color="black", style="setlinewidth(3)", label=""]; -c17:p14:e -> c15:p12:w [color="black", style="setlinewidth(3)", label=""]; -n4:e -> c21:p18:w [color="black", label=""]; -n5:e -> c16:p11:w [color="black", style="setlinewidth(3)", label=""]; -n6:e -> c16:p12:w [color="black", style="setlinewidth(3)", label=""]; -n7:e -> c17:p11:w [color="black", style="setlinewidth(3)", label=""]; -n8:e -> c17:p12:w [color="black", style="setlinewidth(3)", label=""]; -n9:e -> x0:s0:w [color="black", label=""]; -n9:e -> x1:s0:w [color="black", label=""]; -n9:e -> x2:s0:w [color="black", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/submod_03.dot b/manual/APPNOTE_011_Design_Investigation/submod_03.dot deleted file mode 100644 index 0dbbe3baa..000000000 --- a/manual/APPNOTE_011_Design_Investigation/submod_03.dot +++ /dev/null @@ -1,26 +0,0 @@ -digraph "selstage" { -rankdir="LR"; -remincross=true; -n3 [ shape=octagon, label="d", color="black", fontcolor="black" ]; -n4 [ shape=octagon, label="n1", color="black", fontcolor="black" ]; -n5 [ shape=octagon, label="n2", color="black", fontcolor="black" ]; -n6 [ shape=octagon, label="s1", color="black", fontcolor="black" ]; -n7 [ shape=octagon, label="s2", color="black", fontcolor="black" ]; -c10 [ shape=record, label="{{<p8> A}|$39\n$reduce_bool|{<p9> Y}}" ]; -v0 [ label="4'0000" ]; -c13 [ shape=record, label="{{<p8> A|<p11> B|<p12> S}|$40\n$mux|{<p9> Y}}" ]; -x1 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 1:0 " ]; -c13:p9:e -> x1:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""]; -c14 [ shape=record, label="{{<p8> A|<p11> B}|$38\n$xor|{<p9> Y}}" ]; -x2 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ]; -x2:e -> c14:p8:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""]; -c10:p9:e -> c13:p12:w [color="black", label=""]; -c14:p9:e -> c13:p11:w [color="black", style="setlinewidth(3)", label=""]; -n3:e -> c10:p8:w [color="black", style="setlinewidth(3)", label=""]; -n3:e -> c14:p11:w [color="black", style="setlinewidth(3)", label=""]; -x1:s0:e -> n4:w [color="black", style="setlinewidth(3)", label=""]; -x1:s1:e -> n5:w [color="black", style="setlinewidth(3)", label=""]; -n6:e -> x2:s1:w [color="black", style="setlinewidth(3)", label=""]; -n7:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""]; -v0:e -> c13:p8:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod.v b/manual/APPNOTE_011_Design_Investigation/sumprod.v deleted file mode 100644 index 4091bf0a1..000000000 --- a/manual/APPNOTE_011_Design_Investigation/sumprod.v +++ /dev/null @@ -1,12 +0,0 @@ -module sumprod(a, b, c, sum, prod); - - input [7:0] a, b, c; - output [7:0] sum, prod; - - {* sumstuff *} - assign sum = a + b + c; - {* *} - - assign prod = a * b * c; - -endmodule diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_00.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_00.dot deleted file mode 100644 index 06522dcc9..000000000 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_00.dot +++ /dev/null @@ -1,18 +0,0 @@ -digraph "sumprod" { -rankdir="LR"; -remincross=true; -v0 [ label="a" ]; -v1 [ label="b" ]; -v2 [ label="$1_Y" ]; -c4 [ shape=record, label="{{<p1> A|<p2> B}|$1\n$add|{<p3> Y}}" ]; -v3 [ label="$1_Y" ]; -v4 [ label="c" ]; -v5 [ label="sum" ]; -c5 [ shape=record, label="{{<p1> A|<p2> B}|$2\n$add|{<p3> Y}}" ]; -v0:e -> c4:p1:w [color="black", style="setlinewidth(3)", label=""]; -v1:e -> c4:p2:w [color="black", style="setlinewidth(3)", label=""]; -c4:p3:e -> v2:w [color="black", style="setlinewidth(3)", label=""]; -v3:e -> c5:p1:w [color="black", style="setlinewidth(3)", label=""]; -v4:e -> c5:p2:w [color="black", style="setlinewidth(3)", label=""]; -c5:p3:e -> v5:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_01.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_01.dot deleted file mode 100644 index aefe7a6da..000000000 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_01.dot +++ /dev/null @@ -1,15 +0,0 @@ -digraph "sumprod" { -rankdir="LR"; -remincross=true; -n2 [ shape=octagon, label="a", color="black", fontcolor="black" ]; -n3 [ shape=octagon, label="b", color="black", fontcolor="black" ]; -n4 [ shape=octagon, label="c", color="black", fontcolor="black" ]; -n5 [ shape=octagon, label="sum", color="black", fontcolor="black" ]; -c9 [ shape=record, label="{{<p6> A|<p7> B}|$1\n$add|{<p8> Y}}" ]; -c10 [ shape=record, label="{{<p6> A|<p7> B}|$2\n$add|{<p8> Y}}" ]; -c9:p8:e -> c10:p6:w [color="black", style="setlinewidth(3)", label=""]; -n2:e -> c9:p6:w [color="black", style="setlinewidth(3)", label=""]; -n3:e -> c9:p7:w [color="black", style="setlinewidth(3)", label=""]; -n4:e -> c10:p7:w [color="black", style="setlinewidth(3)", label=""]; -c10:p8:e -> n5:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_02.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_02.dot deleted file mode 100644 index 4646c9947..000000000 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_02.dot +++ /dev/null @@ -1,5 +0,0 @@ -digraph "sumprod" { -rankdir="LR"; -remincross=true; -n1 [ shape=octagon, label="prod", color="black", fontcolor="black" ]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_03.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_03.dot deleted file mode 100644 index dcfea2b56..000000000 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_03.dot +++ /dev/null @@ -1,11 +0,0 @@ -digraph "sumprod" { -rankdir="LR"; -remincross=true; -n1 [ shape=octagon, label="prod", color="black", fontcolor="black" ]; -v0 [ label="$3_Y" ]; -v1 [ label="c" ]; -c5 [ shape=record, label="{{<p2> A|<p3> B}|$4\n$mul|{<p4> Y}}" ]; -c5:p4:e -> n1:w [color="black", style="setlinewidth(3)", label=""]; -v0:e -> c5:p2:w [color="black", style="setlinewidth(3)", label=""]; -v1:e -> c5:p3:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_04.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_04.dot deleted file mode 100644 index e77c41aa2..000000000 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_04.dot +++ /dev/null @@ -1,11 +0,0 @@ -digraph "sumprod" { -rankdir="LR"; -remincross=true; -n2 [ shape=octagon, label="c", color="black", fontcolor="black" ]; -n3 [ shape=octagon, label="prod", color="black", fontcolor="black" ]; -c7 [ shape=record, label="{{<p4> A|<p5> B}|$4\n$mul|{<p6> Y}}" ]; -n1 [ shape=diamond, label="$3_Y" ]; -n1:e -> c7:p4:w [color="black", style="setlinewidth(3)", label=""]; -n2:e -> c7:p5:w [color="black", style="setlinewidth(3)", label=""]; -c7:p6:e -> n3:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_05.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_05.dot deleted file mode 100644 index b54441290..000000000 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_05.dot +++ /dev/null @@ -1,15 +0,0 @@ -digraph "sumprod" { -rankdir="LR"; -remincross=true; -n2 [ shape=octagon, label="c", color="black", fontcolor="black" ]; -n3 [ shape=octagon, label="prod", color="black", fontcolor="black" ]; -v0 [ label="a" ]; -v1 [ label="b" ]; -c7 [ shape=record, label="{{<p4> A|<p5> B}|$3\n$mul|{<p6> Y}}" ]; -c8 [ shape=record, label="{{<p4> A|<p5> B}|$4\n$mul|{<p6> Y}}" ]; -c7:p6:e -> c8:p4:w [color="black", style="setlinewidth(3)", label=""]; -n2:e -> c8:p5:w [color="black", style="setlinewidth(3)", label=""]; -c8:p6:e -> n3:w [color="black", style="setlinewidth(3)", label=""]; -v0:e -> c7:p4:w [color="black", style="setlinewidth(3)", label=""]; -v1:e -> c7:p5:w [color="black", style="setlinewidth(3)", label=""]; -} diff --git a/manual/APPNOTE_012_Verilog_to_BTOR.tex b/manual/APPNOTE_012_Verilog_to_BTOR.tex deleted file mode 100644 index aabdc63c4..000000000 --- a/manual/APPNOTE_012_Verilog_to_BTOR.tex +++ /dev/null @@ -1,435 +0,0 @@ - -% 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} - -\lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=2em,xrightmargin=1em,numbers=left} - -\begin{document} - -\title{Yosys Application Note 012: \\ Converting Verilog to BTOR} -\author{Ahmed Irfan and Claire Xenia Wolf \\ April 2015} -\maketitle - -\begin{abstract} -Verilog-2005 is a powerful Hardware Description Language (HDL) that -can be used to easily create complex designs from small HDL code. -BTOR~\cite{btor} is a bit-precise word-level format for model -checking. It is a simple format and easy to parse. It allows to model -the model checking problem over the theory of bit-vectors with -one-dimensional arrays, thus enabling to model Verilog designs with -registers and memories. Yosys~\cite{yosys} is an Open-Source Verilog -synthesis tool that can be used to convert Verilog designs with simple -assertions to BTOR format. - -\end{abstract} - -\section{Installation} - -Yosys written in C++ (using features from C++11) and is tested on -modern Linux. It should compile fine on most UNIX systems with a -C++11 compiler. The README file contains useful information on -building Yosys and its prerequisites. - -Yosys is a large and feature-rich program with some dependencies. For -this work, we may deactivate other extra features such as {\tt TCL} -and {\tt ABC} support in the {\tt Makefile}. - -\bigskip - -This Application Note is based on GIT Rev. {\tt 082550f} from -2015-04-04 of Yosys~\cite{yosys}. - -\section{Quick Start} - -We assume that the Verilog design is synthesizable and we also assume -that the design does not have multi-dimensional memories. As BTOR -implicitly initializes registers to zero value and memories stay -uninitialized, we assume that the Verilog design does -not contain initial blocks. For more details about the BTOR format, -please refer to~\cite{btor}. - -We provide a shell script {\tt verilog2btor.sh} which can be used to -convert a Verilog design to BTOR. The script can be found in the -{\tt backends/btor} directory. The following example shows its usage: - -\begin{figure}[H] -\begin{lstlisting}[language=sh,numbers=none] -verilog2btor.sh fsm.v fsm.btor test -\end{lstlisting} - \renewcommand{\figurename}{Listing} -\caption{Using verilog2btor script} -\end{figure} - -The script {\tt verilog2btor.sh} takes three parameters. In the above -example, the first parameter {\tt fsm.v} is the input design, the second -parameter {\tt fsm.btor} is the file name of BTOR output, and the third -parameter {\tt test} is the name of top module in the design. - -To specify the properties (that need to be checked), we have two -options: -\begin{itemize} -\item We can use the Verilog {\tt assert} statement in the procedural block - or module body of the Verilog design, as shown in - Listing~\ref{specifying_property_assert}. This is the preferred option. -\item We can use a single-bit output wire, whose name starts with - {\tt safety}. The value of this output wire needs to be driven low - when the property is met, i.e. the solver will try to find a model - that makes the safety pin go high. This is demonstrated in - Listing~\ref{specifying_property_output}. -\end{itemize} - -\begin{figure}[H] -\begin{lstlisting}[language=Verilog,numbers=none] -module test(input clk, input rst, output y); - - reg [2:0] state; - - always @(posedge clk) begin - if (rst || state == 3) begin - state <= 0; - end else begin - assert(state < 3); - state <= state + 1; - end - end - - assign y = state[2]; - - assert property (y !== 1'b1); - -endmodule -\end{lstlisting} -\renewcommand{\figurename}{Listing} -\caption{Specifying property in Verilog design with {\tt assert}} -\label{specifying_property_assert} -\end{figure} - -\begin{figure}[H] -\begin{lstlisting}[language=Verilog,numbers=none] -module test(input clk, input rst, - output y, output safety1); - - reg [2:0] state; - - always @(posedge clk) begin - if (rst || state == 3) - state <= 0; - else - state <= state + 1; - end - - assign y = state[2]; - - assign safety1 = !(y !== 1'b1); - -endmodule -\end{lstlisting} -\renewcommand{\figurename}{Listing} -\caption{Specifying property in Verilog design with output wire} -\label{specifying_property_output} -\end{figure} - -We can run Boolector~\cite{boolector}~$1.4.1$\footnote{ -Newer version of Boolector do not support sequential models. -Boolector 1.4.1 can be built with picosat-951. Newer versions -of picosat have an incompatible API.} on the generated BTOR -file: - -\begin{figure}[H] -\begin{lstlisting}[language=sh,numbers=none] -$ boolector fsm.btor -unsat -\end{lstlisting} - \renewcommand{\figurename}{Listing} -\caption{Running boolector on BTOR file} -\end{figure} - -We can also use nuXmv~\cite{nuxmv}, but on BTOR designs it does not -support memories yet. With the next release of nuXmv, we will be also -able to verify designs with memories. - -\section{Detailed Flow} - -Yosys is able to synthesize Verilog designs up to the gate level. -We are interested in keeping registers and memories when synthesizing -the design. For this purpose, we describe a customized Yosys synthesis -flow, that is also provided by the {\tt verilog2btor.sh} script. -Listing~\ref{btor_script_memory} shows the Yosys commands that are -executed by {\tt verilog2btor.sh}. - -\begin{figure}[H] -\begin{lstlisting}[language=sh] -read_verilog -sv $1; -hierarchy -top $3; hierarchy -libdir $DIR; -hierarchy -check; -proc; opt; -opt_expr -mux_undef; opt; -rename -hide;;; -splice; opt; -memory_dff -wr_only; memory_collect;; -flatten;; -memory_unpack; -splitnets -driver; -setundef -zero -undriven; -opt;;; -write_btor $2; -\end{lstlisting} - \renewcommand{\figurename}{Listing} -\caption{Synthesis Flow for BTOR with memories} -\label{btor_script_memory} -\end{figure} - -Here is short description of what is happening in the script line by -line: - -\begin{enumerate} -\item Reading the input file. -\item Setting the top module in the hierarchy and trying to read - automatically the files which are given as {\tt include} in the file - read in first line. -\item Checking the design hierarchy. -\item Converting processes to multiplexers (muxs) and flip-flops. -\item Removing undef signals from muxs. -\item Hiding all signal names that are not used as module ports. -\item Explicit type conversion, by introducing slice and concat cells - in the circuit. -\item Converting write memories to synchronous memories, and - collecting the memories to multi-port memories. -\item Flattening the design to get only one module. -\item Separating read and write memories. -\item Splitting the signals that are partially assigned -\item Setting undef to zero value. -\item Final optimization pass. -\item Writing BTOR file. -\end{enumerate} - -For detailed description of the commands mentioned above, please refer -to the Yosys documentation, or run {\tt yosys -h \it command\_name}. - -The script presented earlier can be easily modified to have a BTOR -file that does not contain memories. This is done by removing the line -number~8 and 10, and introduces a new command {\tt memory} at line -number~8. Listing~\ref{btor_script_without_memory} shows the -modified Yosys script file: - -\begin{figure}[H] -\begin{lstlisting}[language=sh,numbers=none] -read_verilog -sv $1; -hierarchy -top $3; hierarchy -libdir $DIR; -hierarchy -check; -proc; opt; -opt_expr -mux_undef; opt; -rename -hide;;; -splice; opt; -memory;; -flatten;; -splitnets -driver; -setundef -zero -undriven; -opt;;; -write_btor $2; -\end{lstlisting} - \renewcommand{\figurename}{Listing} -\caption{Synthesis Flow for BTOR without memories} -\label{btor_script_without_memory} -\end{figure} - -\section{Example} - -Here is an example Verilog design that we want to convert to BTOR: - -\begin{figure}[H] -\begin{lstlisting}[language=Verilog,numbers=none] -module array(input clk); - - reg [7:0] counter; - reg [7:0] mem [7:0]; - - always @(posedge clk) begin - counter <= counter + 8'd1; - mem[counter] <= counter; - end - - assert property (!(counter > 8'd0) || - mem[counter - 8'd1] == counter - 8'd1); - -endmodule -\end{lstlisting} -\renewcommand{\figurename}{Listing} -\caption{Example - Verilog Design} -\label{example_verilog} -\end{figure} - -The generated BTOR file that contain memories, using the script shown -in Listing~\ref{btor_script_memory}: -\begin{figure}[H] -\begin{lstlisting}[numbers=none] -1 var 1 clk -2 array 8 3 -3 var 8 $auto$rename.cc:150:execute$20 -4 const 8 00000001 -5 sub 8 3 4 -6 slice 3 5 2 0 -7 read 8 2 6 -8 slice 3 3 2 0 -9 add 8 3 4 -10 const 8 00000000 -11 ugt 1 3 10 -12 not 1 11 -13 const 8 11111111 -14 slice 1 13 0 0 -15 one 1 -16 eq 1 1 15 -17 and 1 16 14 -18 write 8 3 2 8 3 -19 acond 8 3 17 18 2 -20 anext 8 3 2 19 -21 eq 1 7 5 -22 or 1 12 21 -23 const 1 1 -24 one 1 -25 eq 1 23 24 -26 cond 1 25 22 24 -27 root 1 -26 -28 cond 8 1 9 3 -29 next 8 3 28 -\end{lstlisting} -\renewcommand{\figurename}{Listing} -\caption{Example - Converted BTOR with memory} -\label{example_btor} -\end{figure} - -And the BTOR file obtained by the script shown in -Listing~\ref{btor_script_without_memory}, which expands the memory -into individual elements: -\begin{figure}[H] -\begin{lstlisting}[numbers=none,escapechar=@] -1 var 1 clk -2 var 8 mem[0] -3 var 8 $auto$rename.cc:150:execute$20 -4 slice 3 3 2 0 -5 slice 1 4 0 0 -6 not 1 5 -7 slice 1 4 1 1 -8 not 1 7 -9 slice 1 4 2 2 -10 not 1 9 -11 and 1 8 10 -12 and 1 6 11 -13 cond 8 12 3 2 -14 cond 8 1 13 2 -15 next 8 2 14 -16 const 8 00000001 -17 add 8 3 16 -18 const 8 00000000 -19 ugt 1 3 18 -20 not 1 19 -21 var 8 mem[2] -22 and 1 7 10 -23 and 1 6 22 -24 cond 8 23 3 21 -25 cond 8 1 24 21 -26 next 8 21 25 -27 sub 8 3 16 - -@\vbox to 0pt{\vss\vdots\vskip3pt}@ -54 cond 1 53 50 52 -55 root 1 -54 - -@\vbox to 0pt{\vss\vdots\vskip3pt}@ -77 cond 8 76 3 44 -78 cond 8 1 77 44 -79 next 8 44 78 -\end{lstlisting} -\renewcommand{\figurename}{Listing} -\caption{Example - Converted BTOR without memory} -\label{example_btor} -\end{figure} - -\section{Limitations} - -BTOR does not support initialization of memories and registers, i.e. they are -implicitly initialized to value zero, so the initial block for -memories need to be removed when converting to BTOR. It should -also be kept in consideration that BTOR does not support the {\tt x} or {\tt z} -values of Verilog. - -Another thing to bear in mind is that Yosys will convert multi-dimensional -memories to one-dimensional memories and address decoders. Therefore -out-of-bounds memory accesses can yield unexpected results. - -\section{Conclusion} - -Using the described flow, we can use Yosys to generate word-level -verification benchmarks with or without memories from Verilog designs. - -\begin{thebibliography}{9} - -\bibitem{yosys} -Claire Xenia Wolf. The Yosys Open SYnthesis Suite. \\ -\url{https://yosyshq.net/yosys/} - -\bibitem{boolector} -Robert Brummayer and Armin Biere, Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays\\ -\url{http://fmv.jku.at/boolector/} - -\bibitem{btor} -Robert Brummayer and Armin Biere and Florian Lonsing, BTOR: -Bit-Precise Modelling of Word-Level Problems for Model Checking\\ -\url{http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf} - -\bibitem{nuxmv} -Roberto Cavada and Alessandro Cimatti and Michele Dorigatti and -Alberto Griggio and Alessandro Mariotti and Andrea Micheli and Sergio -Mover and Marco Roveri and Stefano Tonetta, The nuXmv Symbolic Model -Checker\\ -\url{https://es-static.fbk.eu/tools/nuxmv/index.php} - -\end{thebibliography} - - -\end{document} diff --git a/manual/appnotes.sh b/manual/appnotes.sh deleted file mode 100755 index 0ae52862e..000000000 --- a/manual/appnotes.sh +++ /dev/null @@ -1,22 +0,0 @@ -#!/bin/bash - -set -ex -for job in APPNOTE_010_Verilog_to_BLIF APPNOTE_011_Design_Investigation APPNOTE_012_Verilog_to_BTOR -do - [ -f $job.ok -a $job.ok -nt $job.tex ] && continue - if [ -f $job/make.sh ]; then - cd $job - bash make.sh - cd .. - fi - old_md5=$([ -f $job.aux ] && md5sum < $job.aux || true) - while - pdflatex -shell-escape -halt-on-error $job.tex || exit - new_md5=$(md5sum < $job.aux) - [ "$old_md5" != "$new_md5" ] - do - old_md5="$new_md5" - done - touch $job.ok -done - |