diff options
Diffstat (limited to 'manual')
38 files changed, 2104 insertions, 693 deletions
diff --git a/manual/APPNOTE_010_Verilog_to_BLIF.tex b/manual/APPNOTE_010_Verilog_to_BLIF.tex index 9ee87bc44..0ecdf6194 100644 --- a/manual/APPNOTE_010_Verilog_to_BLIF.tex +++ b/manual/APPNOTE_010_Verilog_to_BLIF.tex @@ -61,7 +61,7 @@ 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) is a simple file format for +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. @@ -100,7 +100,7 @@ regression testing Yosys. \section{Getting Started} -We start our tour with the Navré processor from yosys-bigsim. The Navré +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 @@ -150,11 +150,11 @@ write_blif softusb_navre.blif \end{figure} The first and last line obviously read the Verilog file and write the BLIF -file. +file. \medskip -The 2nd line checks the design hierarchy and instantiates parametrized +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 @@ -174,7 +174,7 @@ 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 +\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 @@ -226,7 +226,7 @@ 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é CPU: +for the Navr\'e CPU: \begin{figure}[H] \begin{lstlisting}[language=sh] @@ -445,7 +445,7 @@ yosys-bigsim, a collection of real-world Verilog designs for regression testing \url{https://github.com/cliffordwolf/yosys-bigsim} \bibitem{navre} -Sebastien Bourdeauducq. Navré AVR clone (8-bit RISC). \\ +Sebastien Bourdeauducq. Navr\'e AVR clone (8-bit RISC). \\ \url{http://opencores.org/project,navre} \bibitem{amber} @@ -456,6 +456,10 @@ Conor Santifort. Amber ARM-compatible core. \\ 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} diff --git a/manual/APPNOTE_011_Design_Investigation.tex b/manual/APPNOTE_011_Design_Investigation.tex index 504ab7ec6..9780c7833 100644 --- a/manual/APPNOTE_011_Design_Investigation.tex +++ b/manual/APPNOTE_011_Design_Investigation.tex @@ -54,7 +54,7 @@ \begin{document} \title{Yosys Application Note 011: \\ Interactive Design Investigation} -\author{Clifford Wolf \\ Original Verision December 2013} +\author{Clifford Wolf \\ Original Version December 2013} \maketitle \begin{abstract} @@ -256,7 +256,7 @@ 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 +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. @@ -296,7 +296,7 @@ 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 {\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}. @@ -316,7 +316,7 @@ yosys> ls 1 modules: example -yosys> cd example +yosys> cd example yosys [example]> ls @@ -497,7 +497,7 @@ using them will get its own net label. In this case however we would like to see the cells connected properly. This can be achieved using the {\tt \%x} action, that broadens the selection, i.e. for each selected wire it selects all cells connected to the wire and vice -versa. So {\tt show a:sumstuff \%x} yields the diagram schon in Fig.~\ref{sumprod_01}. +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} @@ -708,7 +708,7 @@ 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. @@ -729,10 +729,10 @@ 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 @@ -743,8 +743,8 @@ The {\tt -table} option can be used to create a truth table. For example: 2'10 1'1 | 2'xx 2'10 2'11 1'0 | 2'00 2'00 2'11 1'1 | 2'xx 2'11 - - Assumend undef (x) value for the following singals: \s2 + + Assumed undef (x) value for the following signals: \s2 \end{verbatim} } @@ -780,11 +780,11 @@ Final proof equation: \ok = 1'1 Solving problem with 2790 variables and 8241 clauses.. SAT proof finished - model found: FAIL! - ______ ___ ___ _ _ _ _ + ______ ___ ___ _ _ _ _ (_____ \ / __) / __) (_) | | | | _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | | | ____/ ___) _ \ / _ (_ __) (_ __|____ | | || ___ |/ _ |_| - | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ + | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ |_| |_| \___/ \___/ |_| |_| \_____|_|\_)_____)\____|_| @@ -811,15 +811,15 @@ 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.} @@ -840,20 +840,20 @@ 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 @@ -1061,7 +1061,7 @@ MiniSat: a minimalistic open-source SAT solver. \url{http://minisat.se/} \bibitem{tip} -Niklas Een and Niklas Sörensson (2003). +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} diff --git a/manual/APPNOTE_012_Verilog_to_BTOR.tex b/manual/APPNOTE_012_Verilog_to_BTOR.tex new file mode 100644 index 000000000..1bc277876 --- /dev/null +++ b/manual/APPNOTE_012_Verilog_to_BTOR.tex @@ -0,0 +1,435 @@ + +% 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 Clifford 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} +Clifford Wolf. The Yosys Open SYnthesis Suite. \\ +\url{http://www.clifford.at/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/CHAPTER_Appnotes.tex b/manual/CHAPTER_Appnotes.tex index 2abfa85da..e0d093290 100644 --- a/manual/CHAPTER_Appnotes.tex +++ b/manual/CHAPTER_Appnotes.tex @@ -5,9 +5,9 @@ % \begin{fixme} % This appendix will cover some typical use-cases of Yosys in the form of application notes. % \end{fixme} -% +% % \section{Synthesizing using a Cell Library in Liberty Format} -% \section{Reverse Engeneering the MOS6502 from an NMOS Transistor Netlist} +% \section{Reverse Engineering the MOS6502 from an NMOS Transistor Netlist} % \section{Reconfigurable Coarse-Grain Synthesis using Intersynth} This appendix contains copies of the Yosys application notes. @@ -15,6 +15,7 @@ This appendix contains copies of the Yosys application notes. \begin{itemize} \item Yosys AppNote 010: Converting Verilog to BLIF \dotfill Page \pageref{app:010} \hskip2cm\null \item Yosys AppNote 011: Interactive Design Investigation \dotfill Page \pageref{app:011} \hskip2cm\null +\item Yosys AppNote 012: Converting Verilog to BTOR \dotfill Page \pageref{app:012} \hskip2cm\null \end{itemize} \eject\label{app:010} @@ -23,3 +24,6 @@ This appendix contains copies of the Yosys application notes. \eject\label{app:011} \includepdf[pages=-,pagecommand=\thispagestyle{plain}]{APPNOTE_011_Design_Investigation.pdf} +\eject\label{app:012} +\includepdf[pages=-,pagecommand=\thispagestyle{plain}]{APPNOTE_012_Verilog_to_BTOR.pdf} + diff --git a/manual/CHAPTER_Approach.tex b/manual/CHAPTER_Approach.tex index 691225805..4b170ee0a 100644 --- a/manual/CHAPTER_Approach.tex +++ b/manual/CHAPTER_Approach.tex @@ -59,7 +59,7 @@ script. \section{Internal Formats in Yosys} -Yosys uses two different internal formats. The first is used to store an abstract syntax tree (AST) of a verilog +Yosys uses two different internal formats. The first is used to store an abstract syntax tree (AST) of a Verilog input file. This format is simply called {\it AST} and is generated by the Verilog Frontend. This data structure is consumed by a subsystem called {\it AST Frontend}\footnote{In Yosys the term {\it pass} is only used to refer to commands that operate on the RTLIL data structure.}. This AST Frontend then generates a design in Yosys' @@ -107,7 +107,7 @@ from the input file {\tt design.v} to a gate-level netlist {\tt synth.v} using t described by the Liberty file \citeweblink{LibertyFormat} {\tt cells.lib}: \begin{lstlisting}[language=sh,numbers=left,frame=single] -# read input file tpo internal representation +# read input file to internal representation read_verilog design.v # convert high-level behavioral parts ("processes") to d-type flip-flops and muxes diff --git a/manual/CHAPTER_Auxlibs.tex b/manual/CHAPTER_Auxlibs.tex index 8d3ed7430..440ea1375 100644 --- a/manual/CHAPTER_Auxlibs.tex +++ b/manual/CHAPTER_Auxlibs.tex @@ -1,7 +1,7 @@ -\chapter{Auxilary Libraries} +\chapter{Auxiliary Libraries} -The Yosys source distribution contains some auxilary libraries that are bundled +The Yosys source distribution contains some auxiliary libraries that are bundled with Yosys. \section{SHA1} diff --git a/manual/CHAPTER_Auxprogs.tex b/manual/CHAPTER_Auxprogs.tex index a00893828..724d37f0b 100644 --- a/manual/CHAPTER_Auxprogs.tex +++ b/manual/CHAPTER_Auxprogs.tex @@ -1,5 +1,5 @@ -\chapter{Auxilary Programs} +\chapter{Auxiliary Programs} Besides the main {\tt yosys} executable, the Yosys distribution contains a set of additional helper programs. diff --git a/manual/CHAPTER_Basics.tex b/manual/CHAPTER_Basics.tex index c0eda0e84..5c60b7305 100644 --- a/manual/CHAPTER_Basics.tex +++ b/manual/CHAPTER_Basics.tex @@ -56,8 +56,8 @@ and how they relate to different kinds of synthesis. Regardless of the way a lower level representation of a circuit is obtained (synthesis or manual design), the lower level representation is usually verified by comparing simulation results of the lower level and the higher level -representation \footnote{In recent years formal equivalence -checking also became an important verification method for validating RTL and +representation \footnote{In recent years formal equivalence +checking also became an important verification method for validating RTL and lower abstraction representation of the design.}. Therefore even if no synthesis is used, there must still be a simulatable representation of the circuit in all levels to allow for verification of the @@ -116,7 +116,7 @@ value or a condition in the sensitivity list is triggered. A synthesis tool must be able to transfer this representation into an appropriate datapath followed by the appropriate types of register. -For example consider the following verilog code fragment: +For example consider the following Verilog code fragment: \begin{lstlisting}[numbers=left,frame=single,language=Verilog] always @(posedge clk) @@ -141,8 +141,8 @@ App.~\ref{chapter:sota}). \subsection{Register-Transfer Level (RTL)} On the Register-Transfer Level the design is represented by combinatorial data -paths and registers (usually d-type flip flops). The following verilog code fragment -is equivalent to the previous verilog example, but is in RTL representation: +paths and registers (usually d-type flip flops). The following Verilog code fragment +is equivalent to the previous Verilog example, but is in RTL representation: \begin{lstlisting}[numbers=left,frame=single,language=Verilog] assign tmp = a + b; // combinatorial data path @@ -162,7 +162,7 @@ detection and optimization, identification of memories or other larger building and identification of shareable resources. Note that RTL is the first abstraction level in which the circuit is represented as a -graph of circuit elements (registers and combinatorical cells) and signals. Such a graph, +graph of circuit elements (registers and combinatorial cells) and signals. Such a graph, when encoded as list of cells and connections, is called a netlist. RTL synthesis is easy as each circuit node element in the netlist can simply be replaced @@ -262,15 +262,15 @@ Verilog syntax. Only the following language constructs are used in this case: \end{itemize} Many tools (especially at the back end of the synthesis chain) only support -structural verilog as input. ABC is an example of such a tool. Unfortunately +structural Verilog as input. ABC is an example of such a tool. Unfortunately there is no standard specifying what {\it Structural Verilog} actually is, leading to some confusion about what syntax constructs are supported in -structural verilog when it comes to features such as attributes or multi-bit +structural Verilog when it comes to features such as attributes or multi-bit signals. \subsection{Expressions in Verilog} -In all situations where Verilog accepts a constant value or signal name, +In all situations where Verilog accepts a constant value or signal name, expressions using arithmetic operations such as \lstinline[language=Verilog]{+}, \lstinline[language=Verilog]{-} and \lstinline[language=Verilog]{*}, boolean operations such as @@ -280,8 +280,8 @@ and many others (comparison operations, unary operator, etc.) can also be used. During synthesis these operators are replaced by cells that implement the respective function. Many FOSS tools that claim to be able to process Verilog in fact only support -basic structural verilog and simple expressions. Yosys can be used to convert -full featured synthesizable verilog to this simpler subset, thus enabling such +basic structural Verilog and simple expressions. Yosys can be used to convert +full featured synthesizable Verilog to this simpler subset, thus enabling such applications to be used with a richer set of Verilog features. \subsection{Behavioural Modelling} @@ -470,7 +470,7 @@ optimizes the design. First of all because not all optimizations are applicable designs and all synthesis tasks. Some optimizations work (best) on a coarse-grained level (with complex cells such as adders or multipliers) and others work (best) on a fine-grained level (single bit gates). Some optimizations target area and others target speed. -Some work well on large designs while others don't scale well and can only be applied +Some work well on large designs while others don't scale well and can only be applied to small designs. A good tool is capable of applying a wide range of optimizations at different @@ -561,7 +561,7 @@ In order to guarantee reproducibility it is important to be able to re-run all automatic steps in a design project with a fixed set of settings easily. Because of this, usually all programs used in a synthesis flow can be controlled using scripts. This means that all functions are available via -text commands. When such a tool provides a gui, this is complementary to, +text commands. When such a tool provides a GUI, this is complementary to, and not instead of, a command line interface. Usually a synthesis flow in an UNIX/Linux environment would be controlled by a diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index 43d40c73f..f97d4ffa5 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -104,7 +104,7 @@ Multiplexers are generated by the Verilog HDL frontend for {\tt from RTLIL::Process objects to logic. The simplest multiplexer cell type is {\tt \$mux}. Cells of this type have a \B{WIDTH} parameter -and data inputs \B{A} and \B{B} and a data ouput \B{Y}, all of the specified width. This cell also +and data inputs \B{A} and \B{B} and a data output \B{Y}, all of the specified width. This cell also has a single bit control input \B{S}. If \B{S} is 0 the value from the \B{A} input is sent to the output, if it is 1 the value from the \B{B} input is sent to the output. So the {\tt \$mux} cell implements the function \lstinline[language=Verilog]; Y = S ? B : A;. @@ -220,8 +220,9 @@ cell is created. Having individual cells for read and write ports has the advant consolidated using resource sharing passes. In some cases this drastically reduces the number of required ports on the memory cell. -The {\tt \$memrd} cells have a clock input \B{CLK}, an address input \B{ADDR} and a data output -\B{DATA}. They also have the following parameters: +The {\tt \$memrd} cells have a clock input \B{CLK}, an enable input \B{EN}, an +address input \B{ADDR}, and a data output \B{DATA}. They also have the +following parameters: \begin{itemize} \item \B{MEMID} \\ @@ -322,6 +323,9 @@ The {\tt \$mem} cell has the following ports: \item \B{RD\_CLK} \\ This input is \B{RD\_PORTS} bits wide, containing all clock signals for the read ports. +\item \B{RD\_EN} \\ +This input is \B{RD\_PORTS} bits wide, containing all enable signals for the read ports. + \item \B{RD\_ADDR} \\ This input is \B{RD\_PORTS}*\B{ABITS} bits wide, containing all address signals for the read ports. @@ -399,7 +403,7 @@ represent d-type flip-flops. The cell types {\tt \$\_DFF\_NN0\_}, {\tt \$\_DFF\_NN1\_}, {\tt \$\_DFF\_NP0\_}, {\tt \$\_DFF\_NP1\_}, {\tt \$\_DFF\_PN0\_}, {\tt \$\_DFF\_PN1\_}, {\tt \$\_DFF\_PP0\_} and {\tt \$\_DFF\_PP1\_} implement d-type flip-flops with asynchronous resets. The values in the table for these cell types relate to the -following verilog code template, where \lstinline[mathescape,language=Verilog];$RstEdge$; is \lstinline[language=Verilog];posedge; +following Verilog code template, where \lstinline[mathescape,language=Verilog];$RstEdge$; is \lstinline[language=Verilog];posedge; if \lstinline[mathescape,language=Verilog];$RstLvl$; if \lstinline[language=Verilog];1;, and \lstinline[language=Verilog];negedge; otherwise. @@ -417,7 +421,7 @@ pass. The combinatorial logic cells can be mapped to physical cells from a Liber using the {\tt abc} pass. \begin{fixme} -Add information about {\tt \$assert} and {\tt \$equiv} cells. +Add information about {\tt \$assert}, {\tt \$assume}, and {\tt \$equiv} cells. \end{fixme} \begin{fixme} @@ -425,6 +429,10 @@ Add information about {\tt \$slice} and {\tt \$concat} cells. \end{fixme} \begin{fixme} +Add information about {\tt \$lut} and {\tt \$sop} cells. +\end{fixme} + +\begin{fixme} Add information about {\tt \$alu}, {\tt \$macc}, {\tt \$fa}, and {\tt \$lcu} cells. \end{fixme} diff --git a/manual/CHAPTER_Eval.tex b/manual/CHAPTER_Eval.tex index c27a000bf..f719618d5 100644 --- a/manual/CHAPTER_Eval.tex +++ b/manual/CHAPTER_Eval.tex @@ -43,7 +43,7 @@ The following measures were taken to increase the confidence in the correctness make test} is executed. During development of Yosys it was shown that this collection of test cases is sufficient to catch most bugs. The following more sophisticated test procedures only caught a few additional bugs. Whenever this -happend, an appropiate test case was added to the collection of small test +happened, an appropriate test case was added to the collection of small test cases for {\tt make test} to ensure better testability of the feature in question in the future. @@ -64,7 +64,7 @@ validate successfully using Formality. \item VlogHammer \citeweblink{VlogHammer} is a set of scripts that auto-generate a large collection of test cases\footnote{At the time of this writing over 6600 test cases.} and synthesize them using Yosys and the -following freely available propritary synthesis tools. +following freely available proprietary synthesis tools. \begin{itemize} \item Xilinx Vivado WebPack (2013.2) \citeweblink{XilinxWebPACK} \item Xilinx ISE (XST) WebPack (14.5) \citeweblink{XilinxWebPACK} diff --git a/manual/CHAPTER_Eval/grep-it.sh b/manual/CHAPTER_Eval/grep-it.sh index f92eb52cf..0f4f95ae5 100644 --- a/manual/CHAPTER_Eval/grep-it.sh +++ b/manual/CHAPTER_Eval/grep-it.sh @@ -79,6 +79,6 @@ done # if [ $luts -gt 0 -a $luts_ys -gt 0 ]; then luts_p=$(( 100*luts_ys / luts )); else luts_p=NaN; fi # if [ $freq -gt 0 -a $freq_ys -gt 0 ]; then freq_p=$(( 100*freq_ys / freq )); else freq_p=NaN; fi # printf '%-30s %3s %3s %3s\n' $mod $regs_p $luts_p $freq_p -# +# # done diff --git a/manual/CHAPTER_Intro.tex b/manual/CHAPTER_Intro.tex index f735d46b2..76e5d847b 100644 --- a/manual/CHAPTER_Intro.tex +++ b/manual/CHAPTER_Intro.tex @@ -35,7 +35,7 @@ The proposed custom HDL synthesis tool should be licensed under a Free and Open Source Software (FOSS) licence. So an existing FOSS Verilog or VHDL synthesis tool would have been needed as basis to build upon. The main advantages of choosing Verilog or VHDL is the ability to synthesize existing HDL code and -to mitigate the requirement for circuit-designers to learn a new language. In order to take full advantage of any existing FOSS Verilog or VHDL tool, +to mitigate the requirement for circuit-designers to learn a new language. In order to take full advantage of any existing FOSS Verilog or VHDL tool, such a tool would have to provide a feature-complete implementation of the synthesizable HDL subset. @@ -68,7 +68,7 @@ problem of implementing a HDL synthesis tool is approached in the case of Yosys. Chapter~\ref{chapter:overview} contains a more detailed overview of the -implementation of Yosys. This chapter covers the data structures used in +implementation of Yosys. This chapter covers the data structures used in Yosys to represent a design in detail and is therefore recommended reading for everyone who is interested in understanding the Yosys internals. @@ -81,7 +81,7 @@ is recommended reading for everyone who actually wants to read or write Yosys source code. The chapter concludes with an example loadable module for Yosys. -Chapters~\ref{chapter:verilog}, \ref{chapter:opt}, and \ref{chapter:techmap} +Chapters~\ref{chapter:verilog}, \ref{chapter:opt}, and \ref{chapter:techmap} cover three important pieces of the synthesis pipeline: The Verilog frontend, the optimization passes and the technology mapping to the target architecture, respectively. diff --git a/manual/CHAPTER_Optimize.tex b/manual/CHAPTER_Optimize.tex index af8e22497..4b09c2231 100644 --- a/manual/CHAPTER_Optimize.tex +++ b/manual/CHAPTER_Optimize.tex @@ -15,23 +15,23 @@ passes that each perform a simple optimization: \begin{itemize} \item Once at the beginning of {\tt opt}: \begin{itemize} -\item {\tt opt\_const} -\item {\tt opt\_share -nomux} +\item {\tt opt\_expr} +\item {\tt opt\_merge -nomux} \end{itemize} \item Repeat until result is stable: \begin{itemize} \item {\tt opt\_muxtree} \item {\tt opt\_reduce} -\item {\tt opt\_share} +\item {\tt opt\_merge} \item {\tt opt\_rmdff} \item {\tt opt\_clean} -\item {\tt opt\_const} +\item {\tt opt\_expr} \end{itemize} \end{itemize} The following section describes each of the {\tt opt\_*} passes. -\subsection{The opt\_const pass} +\subsection{The opt\_expr pass} This pass performs const folding on the internal combinational cell types described in Chap.~\ref{chapter:celllib}. This means a cell with all constant @@ -57,11 +57,11 @@ this pass can also optimize cells with some constant inputs. $a$ & 1 & $a$ \\ 1 & $b$ & $b$ \\ \end{tabular} - \caption{Const folding rules for {\tt\$\_AND\_} cells as used in {\tt opt\_const}.} - \label{tab:opt_const_and} + \caption{Const folding rules for {\tt\$\_AND\_} cells as used in {\tt opt\_expr}.} + \label{tab:opt_expr_and} \end{table} -Table~\ref{tab:opt_const_and} shows the replacement rules used for optimizing +Table~\ref{tab:opt_expr_and} shows the replacement rules used for optimizing an {\tt\$\_AND\_} gate. The first three rules implement the obvious const folding rules. Note that `any' might include dynamic values calculated by other parts of the circuit. The following three lines propagate undef (X) states. @@ -69,17 +69,17 @@ These are the only three cases in which it is allowed to propagate an undef according to Sec.~5.1.10 of IEEE Std. 1364-2005 \cite{Verilog2005}. The next two lines assume the value 0 for undef states. These two rules are only -used if no other subsitutions are possible in the current module. If other substitutions +used if no other substitutions are possible in the current module. If other substitutions are possible they are performed first, in the hope that the `any' will change to an undef value or a 1 and therefore the output can be set to undef. The last two lines simply replace an {\tt\$\_AND\_} gate with one constant-1 input with a buffer. -Besides this basic const folding the {\tt opt\_const} pass can replace 1-bit wide +Besides this basic const folding the {\tt opt\_expr} pass can replace 1-bit wide {\tt \$eq} and {\tt \$ne} cells with buffers or not-gates if one input is constant. -The {\tt opt\_const} pass is very conservative regarding optimizing {\tt \$mux} cells, +The {\tt opt\_expr} pass is very conservative regarding optimizing {\tt \$mux} cells, as these cells are often used to model decision-trees and breaking these trees can interfere with other optimizations. @@ -130,7 +130,7 @@ This pass identifies unused signals and cells and removes them from the design. creates an \B{unused\_bits} attribute on wires with unused bits. This attribute can be used for debugging or by other optimization passes. -\subsection{The opt\_share pass} +\subsection{The opt\_merge pass} This pass performs trivial resource sharing. This means that this pass identifies cells with identical inputs and replaces them with a single instance of the cell. @@ -241,7 +241,7 @@ by identifying the driver for the state signal. From there the {\tt \$mux}-tree driving the state register inputs is recursively traversed. All select inputs are control signals and the leaves of the -{\tt \$mux}-tree are the states. The algorithm fails if a non-constant leaf +{\tt \$mux}-tree are the states. The algorithm fails if a non-constant leaf that is not the state signal itself is found. The list of control outputs is initialized with the bits from the state signal. @@ -296,7 +296,7 @@ table altered to give the same performance without the external feedback path. \item Entries in the transition table that yield the same output and only differ in the value of a single control input bit are merged and the different bit is removed from the sensitivity list (turned into a don't-care bit). -\item Constant inputs are removed and the transition table is alterered to give an unchanged behaviour. +\item Constant inputs are removed and the transition table is altered to give an unchanged behaviour. \item Unused inputs are removed. \end{itemize} diff --git a/manual/CHAPTER_Overview.tex b/manual/CHAPTER_Overview.tex index ec402231f..964875d57 100644 --- a/manual/CHAPTER_Overview.tex +++ b/manual/CHAPTER_Overview.tex @@ -238,7 +238,7 @@ An RTLIL::Wire object has the following properties: \end{itemize} As with modules, the attributes can be Verilog attributes imported by the -Verilog frontend or attributes assigned by passees. +Verilog frontend or attributes assigned by passes. In Yosys, busses (signal vectors) are represented using a single wire object with a width > 1. So Yosys does not convert signal vectors to individual signals. @@ -307,11 +307,11 @@ process $proc$ff_with_en_and_async_reset.v:4$1 switch \reset case 1'1 assign $0\q[0:0] 1'0 - case + case switch \enable case 1'1 assign $0\q[0:0] \d - case + case end end sync posedge \clock @@ -338,7 +338,7 @@ An RTLIL::CaseRule is a container for zero or more assignments (RTLIL::SigSig) and zero or more RTLIL::SwitchRule objects. An RTLIL::SwitchRule objects is a container for zero or more RTLIL::CaseRule objects. -In the above example the lines $2 \dots 12$ are the root case. Here {\tt \$0\textbackslash{}q[0:0]} is first +In the above example the lines $2 \dots 12$ are the root case. Here {\tt \$0\textbackslash{}q[0:0]} is first assigned the old value {\tt \textbackslash{}q} as default value (line 2). The root case also contains an RTLIL::SwitchRule object (lines $3 \dots 12$). Such an object is very similar to the C {\tt switch} statement as it uses a control signal ({\tt \textbackslash{}reset} in this case) to determine @@ -371,7 +371,7 @@ process $proc$ff_with_en_and_async_reset.v:4$1 switch \enable case 1'1 assign $0\q[0:0] \d - case + case end sync posedge \clock update \q $0\q[0:0] @@ -412,7 +412,7 @@ Some passes refuse to operate on modules that still contain RTLIL::Process objec presence of these objects in a module increases the complexity. Therefore the passes to translate processes to a netlist of cells are usually called early in a synthesis script. The {\tt proc} pass calls a series of other passes that together perform this conversion in a way that is suitable -for most synthesis taks. +for most synthesis tasks. \subsection{RTLIL::Memory} @@ -449,7 +449,7 @@ See Sec.~\ref{sec:memcells} for details about the memory cell types. Yosys reads and processes commands from synthesis scripts, command line arguments and an interactive command prompt. Yosys commands consist of a command name and an optional whitespace separated list of arguments. Commands are terminated using the newline character -or a semicolon ({\tt ;}). Empty lines and lines starting with the hash sign ({\tt \#}) are ignored. +or a semicolon ({\tt ;}). Empty lines and lines starting with the hash sign ({\tt \#}) are ignored. See Sec.~\ref{sec:typusecase} for an example synthesis script. The command {\tt help} can be used to access the command reference manual. @@ -488,8 +488,8 @@ select.cc}, {\tt show.cc}, \dots) and a couple of other small utility libraries. \item {\tt passes/} \\ This directory contains a subdirectory for each pass or group of passes. For example as of this writing the directory {\tt passes/opt/} contains the code for seven -passes: {\tt opt}, {\tt opt\_const}, {\tt opt\_muxtree}, {\tt opt\_reduce}, -{\tt opt\_rmdff}, {\tt opt\_rmunused} and {\tt opt\_share}. +passes: {\tt opt}, {\tt opt\_expr}, {\tt opt\_muxtree}, {\tt opt\_reduce}, +{\tt opt\_rmdff}, {\tt opt\_rmunused} and {\tt opt\_merge}. \item {\tt techlibs/} \\ This directory contains simulation models and standard implementations for the @@ -513,7 +513,7 @@ Yosys. So it is not needed to add additional commands to a central list of comma \end{sloppypar} Good starting points for reading example source code to learn how to write passes -are {\tt passes/opt/opt\_rmdff.cc} and {\tt passes/opt/opt\_share.cc}. +are {\tt passes/opt/opt\_rmdff.cc} and {\tt passes/opt/opt\_merge.cc}. See the top-level README file for a quick {\it Getting Started} guide and build instructions. The Yosys build is based solely on Makefiles. diff --git a/manual/CHAPTER_Prog/stubnets.cc b/manual/CHAPTER_Prog/stubnets.cc index 4849c6a7b..eb77bd404 100644 --- a/manual/CHAPTER_Prog/stubnets.cc +++ b/manual/CHAPTER_Prog/stubnets.cc @@ -1,5 +1,5 @@ // This is free and unencumbered software released into the public domain. -// +// // Anyone is free to copy, modify, publish, use, compile, sell, or // distribute this software, either in source code form or as a compiled // binary, for any purpose, commercial or non-commercial, and by any @@ -24,7 +24,7 @@ static void find_stub_nets(RTLIL::Design *design, RTLIL::Module *module, bool re // count how many times a single-bit signal is used std::map<RTLIL::SigBit, int> bit_usage_count; - // count ouput lines for this module (needed only for summary output at the end) + // count output lines for this module (needed only for summary output at the end) int line_count = 0; log("Looking for stub wires in module %s:\n", RTLIL::id2cstr(module->name)); @@ -103,7 +103,7 @@ struct StubnetsPass : public Pass { // variables to mirror information from passed options bool report_bits = 0; - log_header("Executing STUBNETS pass (find stub nets).\n"); + log_header(design, "Executing STUBNETS pass (find stub nets).\n"); // parse options size_t argidx; diff --git a/manual/CHAPTER_StateOfTheArt.tex b/manual/CHAPTER_StateOfTheArt.tex index 7e62230ef..2d0c77a01 100644 --- a/manual/CHAPTER_StateOfTheArt.tex +++ b/manual/CHAPTER_StateOfTheArt.tex @@ -248,7 +248,7 @@ passes). This architecture will simplify implementing additional HDL front ends and/or additional synthesis passes. Chapter~\ref{chapter:eval} contains a more detailed evaluation of Yosys using real-world -designes that are far out of reach for any of the other tools discussed in this appendix. +designs that are far out of reach for any of the other tools discussed in this appendix. \vskip2cm \begin{table}[h] diff --git a/manual/CHAPTER_StateOfTheArt/simlib_hana.v b/manual/CHAPTER_StateOfTheArt/simlib_hana.v index fc82f1389..7fb54fa49 100644 --- a/manual/CHAPTER_StateOfTheArt/simlib_hana.v +++ b/manual/CHAPTER_StateOfTheArt/simlib_hana.v @@ -1,4 +1,4 @@ -/* +/* Copyright (C) 2009-2010 Parvez Ahmad Written by Parvez Ahmad <parvez_ahmad@yahoo.co.uk>. @@ -45,7 +45,7 @@ module AND3 #(parameter SIZE = 3) (input [SIZE-1:0] in, output out); assign out = ∈ endmodule - + module AND4 #(parameter SIZE = 4) (input [SIZE-1:0] in, output out); assign out = ∈ @@ -63,7 +63,7 @@ module OR3 #(parameter SIZE = 3) (input [SIZE-1:0] in, output out); assign out = |in; endmodule - + module OR4 #(parameter SIZE = 4) (input [SIZE-1:0] in, output out); assign out = |in; @@ -82,7 +82,7 @@ module NAND3 #(parameter SIZE = 3) (input [SIZE-1:0] in, output out); assign out = ~∈ endmodule - + module NAND4 #(parameter SIZE = 4) (input [SIZE-1:0] in, output out); assign out = ~∈ @@ -100,7 +100,7 @@ module NOR3 #(parameter SIZE = 3) (input [SIZE-1:0] in, output out); assign out = ~|in; endmodule - + module NOR4 #(parameter SIZE = 4) (input [SIZE-1:0] in, output out); assign out = ~|in; @@ -119,7 +119,7 @@ module XOR3 #(parameter SIZE = 3) (input [SIZE-1:0] in, output out); assign out = ^in; endmodule - + module XOR4 #(parameter SIZE = 4) (input [SIZE-1:0] in, output out); assign out = ^in; @@ -138,7 +138,7 @@ module XNOR3 #(parameter SIZE = 3) (input [SIZE-1:0] in, output out); assign out = ~^in; endmodule - + module XNOR4 #(parameter SIZE = 4) (input [SIZE-1:0] in, output out); assign out = ~^in; @@ -156,7 +156,7 @@ always @(in or enable) 1'b1 : out = 2'b10; endcase end -endmodule +endmodule module DEC2 (input [1:0] in, input enable, output reg [3:0] out); @@ -171,7 +171,7 @@ always @(in or enable) 2'b11 : out = 4'b1000; endcase end -endmodule +endmodule module DEC3 (input [2:0] in, input enable, output reg [7:0] out); @@ -190,7 +190,7 @@ always @(in or enable) 3'b111 : out = 8'b10000000; endcase end -endmodule +endmodule module DEC4 (input [3:0] in, input enable, output reg [15:0] out); @@ -217,7 +217,7 @@ always @(in or enable) 4'b1111 : out = 16'b1000000000000000; endcase end -endmodule +endmodule module DEC5 (input [4:0] in, input enable, output reg [31:0] out); always @(in or enable) @@ -259,7 +259,7 @@ always @(in or enable) 5'b11111 : out = 32'b10000000000000000000000000000000; endcase end -endmodule +endmodule module DEC6 (input [5:0] in, input enable, output reg [63:0] out); @@ -335,7 +335,7 @@ always @(in or enable) 6'b111111 : out = 64'b1000000000000000000000000000000000000000000000000000000000000000; endcase end -endmodule +endmodule module MUX2(input [1:0] in, input select, output reg out); @@ -345,7 +345,7 @@ always @( in or select) 0: out = in[0]; 1: out = in[1]; endcase -endmodule +endmodule module MUX4(input [3:0] in, input [1:0] select, output reg out); @@ -357,7 +357,7 @@ always @( in or select) 2: out = in[2]; 3: out = in[3]; endcase -endmodule +endmodule module MUX8(input [7:0] in, input [2:0] select, output reg out); @@ -373,7 +373,7 @@ always @( in or select) 6: out = in[6]; 7: out = in[7]; endcase -endmodule +endmodule module MUX16(input [15:0] in, input [3:0] select, output reg out); @@ -396,7 +396,7 @@ always @( in or select) 14: out = in[14]; 15: out = in[15]; endcase -endmodule +endmodule module MUX32(input [31:0] in, input [4:0] select, output reg out); @@ -435,7 +435,7 @@ always @( in or select) 30: out = in[30]; 31: out = in[31]; endcase -endmodule +endmodule module MUX64(input [63:0] in, input [5:0] select, output reg out); @@ -506,7 +506,7 @@ always @( in or select) 62: out = in[62]; 63: out = in[63]; endcase -endmodule +endmodule module ADD1(input in1, in2, cin, output out, cout); @@ -514,41 +514,41 @@ assign {cout, out} = in1 + in2 + cin; endmodule -module ADD2 #(parameter SIZE = 2)(input [SIZE-1:0] in1, in2, +module ADD2 #(parameter SIZE = 2)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 + in2 + cin; endmodule -module ADD4 #(parameter SIZE = 4)(input [SIZE-1:0] in1, in2, +module ADD4 #(parameter SIZE = 4)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 + in2 + cin; endmodule -module ADD8 #(parameter SIZE = 8)(input [SIZE-1:0] in1, in2, +module ADD8 #(parameter SIZE = 8)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 + in2 + cin; endmodule -module ADD16 #(parameter SIZE = 16)(input [SIZE-1:0] in1, in2, +module ADD16 #(parameter SIZE = 16)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 + in2 + cin; endmodule -module ADD32 #(parameter SIZE = 32)(input [SIZE-1:0] in1, in2, +module ADD32 #(parameter SIZE = 32)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 + in2 + cin; endmodule -module ADD64 #(parameter SIZE = 64)(input [SIZE-1:0] in1, in2, +module ADD64 #(parameter SIZE = 64)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 + in2 + cin; @@ -561,41 +561,41 @@ assign {cout, out} = in1 - in2 - cin; endmodule -module SUB2 #(parameter SIZE = 2)(input [SIZE-1:0] in1, in2, +module SUB2 #(parameter SIZE = 2)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 - in2 - cin; endmodule -module SUB4 #(parameter SIZE = 4)(input [SIZE-1:0] in1, in2, +module SUB4 #(parameter SIZE = 4)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 - in2 - cin; endmodule -module SUB8 #(parameter SIZE = 8)(input [SIZE-1:0] in1, in2, +module SUB8 #(parameter SIZE = 8)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 - in2 - cin; endmodule -module SUB16 #(parameter SIZE = 16)(input [SIZE-1:0] in1, in2, +module SUB16 #(parameter SIZE = 16)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 - in2 - cin; endmodule -module SUB32 #(parameter SIZE = 32)(input [SIZE-1:0] in1, in2, +module SUB32 #(parameter SIZE = 32)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 - in2 - cin; endmodule -module SUB64 #(parameter SIZE = 64)(input [SIZE-1:0] in1, in2, +module SUB64 #(parameter SIZE = 64)(input [SIZE-1:0] in1, in2, input cin, output [SIZE-1:0] out, output cout); assign {cout, out} = in1 - in2 - cin; @@ -651,7 +651,7 @@ assign rem = in1%in2; endmodule -module DIV2 #(parameter SIZE = 2)(input [SIZE-1:0] in1, in2, +module DIV2 #(parameter SIZE = 2)(input [SIZE-1:0] in1, in2, output [SIZE-1:0] out, rem); assign out = in1/in2; @@ -659,7 +659,7 @@ assign rem = in1%in2; endmodule -module DIV4 #(parameter SIZE = 4)(input [SIZE-1:0] in1, in2, +module DIV4 #(parameter SIZE = 4)(input [SIZE-1:0] in1, in2, output [SIZE-1:0] out, rem); assign out = in1/in2; @@ -667,7 +667,7 @@ assign rem = in1%in2; endmodule -module DIV8 #(parameter SIZE = 8)(input [SIZE-1:0] in1, in2, +module DIV8 #(parameter SIZE = 8)(input [SIZE-1:0] in1, in2, output [SIZE-1:0] out, rem); assign out = in1/in2; @@ -675,7 +675,7 @@ assign rem = in1%in2; endmodule -module DIV16 #(parameter SIZE = 16)(input [SIZE-1:0] in1, in2, +module DIV16 #(parameter SIZE = 16)(input [SIZE-1:0] in1, in2, output [SIZE-1:0] out, rem); assign out = in1/in2; @@ -683,7 +683,7 @@ assign rem = in1%in2; endmodule -module DIV32 #(parameter SIZE = 32)(input [SIZE-1:0] in1, in2, +module DIV32 #(parameter SIZE = 32)(input [SIZE-1:0] in1, in2, output [SIZE-1:0] out, rem); assign out = in1/in2; @@ -691,7 +691,7 @@ assign rem = in1%in2; endmodule -module DIV64 #(parameter SIZE = 64)(input [SIZE-1:0] in1, in2, +module DIV64 #(parameter SIZE = 64)(input [SIZE-1:0] in1, in2, output [SIZE-1:0] out, rem); assign out = in1/in2; @@ -711,7 +711,7 @@ always @(posedge clk or posedge reset) q <= 0; else q <= d; -endmodule +endmodule module SFF(input d, clk, set, output reg q); always @(posedge clk or posedge set) @@ -719,7 +719,7 @@ always @(posedge clk or posedge set) q <= 1; else q <= d; -endmodule +endmodule module RSFF(input d, clk, set, reset, output reg q); always @(posedge clk or posedge reset or posedge set) @@ -745,30 +745,30 @@ module LATCH(input d, enable, output reg q); always @( d or enable) if(enable) q <= d; -endmodule +endmodule module RLATCH(input d, reset, enable, output reg q); always @( d or enable or reset) if(enable) if(reset) q <= 0; - else + else q <= d; -endmodule +endmodule module LSHIFT1 #(parameter SIZE = 1)(input in, shift, val, output reg out); always @ (in, shift, val) begin if(shift) out = val; - else + else out = in; end endmodule -module LSHIFT2 #(parameter SIZE = 2)(input [SIZE-1:0] in, +module LSHIFT2 #(parameter SIZE = 2)(input [SIZE-1:0] in, input [SIZE-1:0] shift, input val, output reg [SIZE-1:0] out); @@ -776,58 +776,58 @@ always @(in or shift or val) begin out = in << shift; if(val) out = out | ({SIZE-1 {1'b1} } >> (SIZE-1-shift)); -end +end endmodule -module LSHIFT4 #(parameter SIZE = 4)(input [SIZE-1:0] in, +module LSHIFT4 #(parameter SIZE = 4)(input [SIZE-1:0] in, input [2:0] shift, input val, output reg [SIZE-1:0] out); always @(in or shift or val) begin out = in << shift; if(val) out = out | ({SIZE-1 {1'b1} } >> (SIZE-1-shift)); -end +end endmodule -module LSHIFT8 #(parameter SIZE = 8)(input [SIZE-1:0] in, +module LSHIFT8 #(parameter SIZE = 8)(input [SIZE-1:0] in, input [3:0] shift, input val, output reg [SIZE-1:0] out); always @(in or shift or val) begin out = in << shift; if(val) out = out | ({SIZE-1 {1'b1} } >> (SIZE-1-shift)); -end +end endmodule -module LSHIFT16 #(parameter SIZE = 16)(input [SIZE-1:0] in, +module LSHIFT16 #(parameter SIZE = 16)(input [SIZE-1:0] in, input [4:0] shift, input val, output reg [SIZE-1:0] out); always @(in or shift or val) begin out = in << shift; if(val) out = out | ({SIZE-1 {1'b1} } >> (SIZE-1-shift)); -end +end endmodule -module LSHIFT32 #(parameter SIZE = 32)(input [SIZE-1:0] in, +module LSHIFT32 #(parameter SIZE = 32)(input [SIZE-1:0] in, input [5:0] shift, input val, output reg [SIZE-1:0] out); always @(in or shift or val) begin out = in << shift; if(val) out = out | ({SIZE-1 {1'b1} } >> (SIZE-1-shift)); -end +end endmodule -module LSHIFT64 #(parameter SIZE = 64)(input [SIZE-1:0] in, +module LSHIFT64 #(parameter SIZE = 64)(input [SIZE-1:0] in, input [6:0] shift, input val, output reg [SIZE-1:0] out); always @(in or shift or val) begin out = in << shift; if(val) out = out | ({SIZE-1 {1'b1} } >> (SIZE-1-shift)); -end +end endmodule module RSHIFT1 #(parameter SIZE = 1)(input in, shift, val, output reg out); @@ -841,7 +841,7 @@ end endmodule -module RSHIFT2 #(parameter SIZE = 2)(input [SIZE-1:0] in, +module RSHIFT2 #(parameter SIZE = 2)(input [SIZE-1:0] in, input [SIZE-1:0] shift, input val, output reg [SIZE-1:0] out); @@ -849,12 +849,12 @@ always @(in or shift or val) begin out = in >> shift; if(val) out = out | ({SIZE-1 {1'b1} } << (SIZE-1-shift)); -end +end endmodule -module RSHIFT4 #(parameter SIZE = 4)(input [SIZE-1:0] in, +module RSHIFT4 #(parameter SIZE = 4)(input [SIZE-1:0] in, input [2:0] shift, input val, output reg [SIZE-1:0] out); @@ -862,10 +862,10 @@ always @(in or shift or val) begin out = in >> shift; if(val) out = out | ({SIZE-1 {1'b1} } << (SIZE-1-shift)); -end +end endmodule -module RSHIFT8 #(parameter SIZE = 8)(input [SIZE-1:0] in, +module RSHIFT8 #(parameter SIZE = 8)(input [SIZE-1:0] in, input [3:0] shift, input val, output reg [SIZE-1:0] out); @@ -873,11 +873,11 @@ always @(in or shift or val) begin out = in >> shift; if(val) out = out | ({SIZE-1 {1'b1} } << (SIZE-1-shift)); -end +end endmodule -module RSHIFT16 #(parameter SIZE = 16)(input [SIZE-1:0] in, +module RSHIFT16 #(parameter SIZE = 16)(input [SIZE-1:0] in, input [4:0] shift, input val, output reg [SIZE-1:0] out); @@ -885,11 +885,11 @@ always @(in or shift or val) begin out = in >> shift; if(val) out = out | ({SIZE-1 {1'b1} } << (SIZE-1-shift)); -end +end endmodule -module RSHIFT32 #(parameter SIZE = 32)(input [SIZE-1:0] in, +module RSHIFT32 #(parameter SIZE = 32)(input [SIZE-1:0] in, input [5:0] shift, input val, output reg [SIZE-1:0] out); @@ -897,10 +897,10 @@ always @(in or shift or val) begin out = in >> shift; if(val) out = out | ({SIZE-1 {1'b1} } << (SIZE-1-shift)); -end +end endmodule -module RSHIFT64 #(parameter SIZE = 64)(input [SIZE-1:0] in, +module RSHIFT64 #(parameter SIZE = 64)(input [SIZE-1:0] in, input [6:0] shift, input val, output reg [SIZE-1:0] out); @@ -908,10 +908,10 @@ always @(in or shift or val) begin out = in >> shift; if(val) out = out | ({SIZE-1 {1'b1} } << (SIZE-1-shift)); -end +end endmodule -module CMP1 #(parameter SIZE = 1) (input in1, in2, +module CMP1 #(parameter SIZE = 1) (input in1, in2, output reg equal, unequal, greater, lesser); always @ (in1 or in2) begin @@ -920,7 +920,7 @@ always @ (in1 or in2) begin unequal = 0; greater = 0; lesser = 0; - end + end else begin equal = 0; unequal = 1; @@ -928,17 +928,17 @@ always @ (in1 or in2) begin if(in1 < in2) begin greater = 0; lesser = 1; - end + end else begin greater = 1; lesser = 0; - end - end + end + end end endmodule -module CMP2 #(parameter SIZE = 2) (input [SIZE-1:0] in1, in2, +module CMP2 #(parameter SIZE = 2) (input [SIZE-1:0] in1, in2, output reg equal, unequal, greater, lesser); always @ (in1 or in2) begin @@ -947,7 +947,7 @@ always @ (in1 or in2) begin unequal = 0; greater = 0; lesser = 0; - end + end else begin equal = 0; unequal = 1; @@ -955,16 +955,16 @@ always @ (in1 or in2) begin if(in1 < in2) begin greater = 0; lesser = 1; - end + end else begin greater = 1; lesser = 0; - end - end + end + end end endmodule -module CMP4 #(parameter SIZE = 4) (input [SIZE-1:0] in1, in2, +module CMP4 #(parameter SIZE = 4) (input [SIZE-1:0] in1, in2, output reg equal, unequal, greater, lesser); always @ (in1 or in2) begin @@ -973,7 +973,7 @@ always @ (in1 or in2) begin unequal = 0; greater = 0; lesser = 0; - end + end else begin equal = 0; unequal = 1; @@ -981,16 +981,16 @@ always @ (in1 or in2) begin if(in1 < in2) begin greater = 0; lesser = 1; - end + end else begin greater = 1; lesser = 0; - end - end + end + end end endmodule -module CMP8 #(parameter SIZE = 8) (input [SIZE-1:0] in1, in2, +module CMP8 #(parameter SIZE = 8) (input [SIZE-1:0] in1, in2, output reg equal, unequal, greater, lesser); always @ (in1 or in2) begin @@ -999,7 +999,7 @@ always @ (in1 or in2) begin unequal = 0; greater = 0; lesser = 0; - end + end else begin equal = 0; unequal = 1; @@ -1007,16 +1007,16 @@ always @ (in1 or in2) begin if(in1 < in2) begin greater = 0; lesser = 1; - end + end else begin greater = 1; lesser = 0; - end - end + end + end end endmodule -module CMP16 #(parameter SIZE = 16) (input [SIZE-1:0] in1, in2, +module CMP16 #(parameter SIZE = 16) (input [SIZE-1:0] in1, in2, output reg equal, unequal, greater, lesser); always @ (in1 or in2) begin @@ -1025,7 +1025,7 @@ always @ (in1 or in2) begin unequal = 0; greater = 0; lesser = 0; - end + end else begin equal = 0; unequal = 1; @@ -1033,16 +1033,16 @@ always @ (in1 or in2) begin if(in1 < in2) begin greater = 0; lesser = 1; - end + end else begin greater = 1; lesser = 0; - end - end + end + end end endmodule -module CMP32 #(parameter SIZE = 32) (input [SIZE-1:0] in1, in2, +module CMP32 #(parameter SIZE = 32) (input [SIZE-1:0] in1, in2, output reg equal, unequal, greater, lesser); always @ (in1 or in2) begin @@ -1051,7 +1051,7 @@ always @ (in1 or in2) begin unequal = 0; greater = 0; lesser = 0; - end + end else begin equal = 0; unequal = 1; @@ -1059,16 +1059,16 @@ always @ (in1 or in2) begin if(in1 < in2) begin greater = 0; lesser = 1; - end + end else begin greater = 1; lesser = 0; - end - end + end + end end endmodule -module CMP64 #(parameter SIZE = 64) (input [SIZE-1:0] in1, in2, +module CMP64 #(parameter SIZE = 64) (input [SIZE-1:0] in1, in2, output reg equal, unequal, greater, lesser); always @ (in1 or in2) begin @@ -1077,7 +1077,7 @@ always @ (in1 or in2) begin unequal = 0; greater = 0; lesser = 0; - end + end else begin equal = 0; unequal = 1; @@ -1085,12 +1085,12 @@ always @ (in1 or in2) begin if(in1 < in2) begin greater = 0; lesser = 1; - end + end else begin greater = 1; lesser = 0; - end - end + end + end end endmodule diff --git a/manual/CHAPTER_StateOfTheArt/simlib_yosys.v b/manual/CHAPTER_StateOfTheArt/simlib_yosys.v index 54c076614..454c9a83f 100644 --- a/manual/CHAPTER_StateOfTheArt/simlib_yosys.v +++ b/manual/CHAPTER_StateOfTheArt/simlib_yosys.v @@ -2,11 +2,11 @@ * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> - * + * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. - * + * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR @@ -19,7 +19,7 @@ * * The internal logic cell simulation library. * - * This verilog library contains simple simulation models for the internal + * This Verilog library contains simple simulation models for the internal * logic cells (_NOT_, _AND_, ...) that are generated by the default technology * mapper (see "stdcells.v" in this directory) and expected by the "abc" pass. * diff --git a/manual/CHAPTER_Techmap.tex b/manual/CHAPTER_Techmap.tex index e5c7456c4..13aa8e5a3 100644 --- a/manual/CHAPTER_Techmap.tex +++ b/manual/CHAPTER_Techmap.tex @@ -5,7 +5,7 @@ Previous chapters outlined how HDL code is transformed into an RTL netlist. The RTL netlist is still based on abstract coarse-grain cell types like arbitrary width adders and even multipliers. This chapter covers how an RTL netlist is -transformed into a functionally equivialent netlist utililizing the cell types +transformed into a functionally equivalent netlist utilizing the cell types available in the target architecture. Technology mapping is often performed in two phases. In the first phase RTL cells diff --git a/manual/CHAPTER_Verilog.tex b/manual/CHAPTER_Verilog.tex index 485b4f357..e9ca6114e 100644 --- a/manual/CHAPTER_Verilog.tex +++ b/manual/CHAPTER_Verilog.tex @@ -98,7 +98,7 @@ The lexer does little more than identifying all keywords and literals recognised by the Yosys Verilog frontend. \end{sloppypar} -The lexer keeps track of the current location in the verilog source code using +The lexer keeps track of the current location in the Verilog source code using some global variables. These variables are used by the constructor of AST nodes to annotate each node with the source code location it originated from. @@ -168,11 +168,11 @@ Created by the simplifier when an undeclared signal name is used. \\ \hline % {\tt AST\_PARASET} & -Parameter set in cell instanciation \\ +Parameter set in cell instantiation \\ \hline % {\tt AST\_ARGUMENT} & -Port connection in cell instanciation \\ +Port connection in cell instantiation \\ \hline % {\tt AST\_RANGE} & @@ -184,7 +184,7 @@ A literal value \\ \hline % {\tt AST\_CELLTYPE} & -The type of cell in cell instanciation \\ +The type of cell in cell instantiation \\ \hline % {\tt AST\_IDENTIFIER} & @@ -251,8 +251,8 @@ The unary reduction operators \break \hline % {\tt AST\_REDUCE\_BOOL} & -Conversion from multi-bit value to boolian value -(equivialent to {\tt AST\_REDUCE\_OR}) \\ +Conversion from multi-bit value to boolean value +(equivalent to {\tt AST\_REDUCE\_OR}) \\ \hline % {\tt AST\_SHIFT\_LEFT}, @@ -327,7 +327,7 @@ An \lstinline[language=Verilog];assign; statement \\ \hline % {\tt AST\_CELL} & -A cell instanciation \\ +A cell instantiation \\ \hline % {\tt AST\_PRIMITIVE} & @@ -359,7 +359,7 @@ and the default case respectively \\ \hline % {\tt AST\_FOR} & -A \lstinline[language=Verilog];for;-loop witn an +A \lstinline[language=Verilog];for;-loop with an \lstinline[language=Verilog];always;- or \lstinline[language=Verilog];initial;-block \\ \hline @@ -470,7 +470,7 @@ This produces an AST that is fairly easy to convert to the RTLIL format. \subsection{Generating RTLIL} After AST simplification, the \lstinline[language=C++]{AST::AstNode::genRTLIL()} method of each {\tt AST\_MODULE} node -in the AST is called. This initiates a recursive process that generates equivialent RTLIL data for the AST data. +in the AST is called. This initiates a recursive process that generates equivalent RTLIL data for the AST data. The \lstinline[language=C++]{AST::AstNode::genRTLIL()} method returns an \lstinline[language=C++]{RTLIL::SigSpec} structure. For nodes that represent expressions (operators, constants, signals, etc.), the cells needed to implement the calculation @@ -550,23 +550,23 @@ process $proc$<input>:1$1 switch \in2 case 1'1 assign $1\out1[0:0] $logic_not$<input>:4$2_Y - case + case assign $1\out1[0:0] \in1 end switch \in3 case 1'1 assign $0\out2[0:0] \out2 - case + case end switch \in4 case 1'1 switch \in5 case 1'1 assign $0\out3[0:0] \in6 - case + case assign $0\out3[0:0] \in7 end - case + case end sync posedge \clock update \out1 $0\out1[0:0] @@ -641,7 +641,7 @@ A pointer to a \lstinline[language=C++]{RTLIL::CaseRule} object. Initially this generated \lstinline[language=C++]{RTLIL::Process}. \end{itemize} -As the algorithm runs these variables are continously modified as well as pushed +As the algorithm runs these variables are continuously modified as well as pushed to the stack and later restored to their earlier values by popping from the stack. On startup the ProcessGenerator generates a new @@ -703,7 +703,7 @@ the ProcessGenerator: \item A new \lstinline[language=C++]{RTLIL::SwitchRule} object is generated, the selection expression is evaluated using \lstinline[language=C++]{AST::AstNode::genRTLIL()} (with the use of \lstinline[language=C++]{subst_rvalue_from} and \lstinline[language=C++]{subst_rvalue_to}) and added to the \lstinline[language=C++]{RTLIL::SwitchRule} object and the -obect is added to the \lstinline[language=C++]{current_case}. +object is added to the \lstinline[language=C++]{current_case}. % \item All lvalues assigned to within the {\tt AST\_CASE} node using blocking assignments are collected and saved in the local variable \lstinline[language=C++]{this_case_eq_lvalue}. @@ -837,7 +837,7 @@ as sr-latches or d-latches, without having to extend the actual Verilog frontend \begin{fixme} Add some information on the generation of {\tt \$memrd} and {\tt \$memwr} cells -and how they are processsed in the {\tt memory} pass. +and how they are processed in the {\tt memory} pass. \end{fixme} \section{Synthesizing Parametric Designs} diff --git a/manual/PRESENTATION_ExAdv.tex b/manual/PRESENTATION_ExAdv.tex index 743500918..ef8f64cec 100644 --- a/manual/PRESENTATION_ExAdv.tex +++ b/manual/PRESENTATION_ExAdv.tex @@ -245,7 +245,7 @@ show -color red @cone_ab -color magenta @cone_a -color blue @cone_b \begin{itemize} \item The {\tt techmap} command replaces cells in the design with implementations given -as verilog code (called ``map files''). It can replace Yosys' internal cell +as Verilog code (called ``map files''). It can replace Yosys' internal cell types (such as {\tt \$or}) as well as user-defined cell types. \medskip\item Verilog parameters are used extensively to customize the internal cell types. @@ -480,7 +480,7 @@ cells in ASICS or dedicated carry logic in FPGAs. \subsubsection{Intro to coarse-grain synthesis} \begin{frame}[fragile]{\subsubsecname} -In coarse-grain synthesis the target architecure has cells of the same +In coarse-grain synthesis the target architecture has cells of the same complexity or larger complexity than the internal RTL representation. For example: @@ -558,7 +558,7 @@ $\downarrow$ & $\downarrow$ \\ \begin{frame}{\subsubsecname} \scriptsize Often a coarse-grain element has a constant bit-width, but can be used to -implement oprations with a smaller bit-width. For example, a 18x25-bit multiplier +implement operations with a smaller bit-width. For example, a 18x25-bit multiplier can also be used to implement 16x20-bit multiplication. \bigskip @@ -821,7 +821,7 @@ scripts as well as in reverse engineering and analysis. \item {\bf Behavioral changes} \\ Commands such as {\tt techmap} can be used to make behavioral changes to the design, for example -changing asynchonous resets to synchronous resets. This has applications in design space exploration +changing asynchronous resets to synchronous resets. This has applications in design space exploration (evaluation of various architectures for one circuit). \end{itemize} \end{frame} @@ -844,13 +844,13 @@ module adff2dff (CLK, ARST, D, Q); 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; \end{lstlisting} \vss} @@ -877,7 +877,7 @@ endmodule \begin{frame}{\subsecname} \begin{itemize} -\item A lot can be achived in Yosys just with the standard set of commands. +\item A lot can be achieved in Yosys just with the standard set of commands. \item The commands {\tt techmap} and {\tt extract} can be used to prototype many complex synthesis tasks. \end{itemize} diff --git a/manual/PRESENTATION_ExAdv/addshift_map.v b/manual/PRESENTATION_ExAdv/addshift_map.v index b6d91b01b..13ecf0bae 100644 --- a/manual/PRESENTATION_ExAdv/addshift_map.v +++ b/manual/PRESENTATION_ExAdv/addshift_map.v @@ -4,17 +4,17 @@ module \$add (A, B, Y); parameter A_WIDTH = 1; parameter B_WIDTH = 1; parameter Y_WIDTH = 1; - + input [A_WIDTH-1:0] A; input [B_WIDTH-1:0] B; output [Y_WIDTH-1:0] Y; - + parameter _TECHMAP_BITS_CONNMAP_ = 0; parameter _TECHMAP_CONNMAP_A_ = 0; parameter _TECHMAP_CONNMAP_B_ = 0; - + wire _TECHMAP_FAIL_ = A_WIDTH != B_WIDTH || B_WIDTH < Y_WIDTH || _TECHMAP_CONNMAP_A_ != _TECHMAP_CONNMAP_B_; - + assign Y = A << 1; endmodule diff --git a/manual/PRESENTATION_ExAdv/red_or3x1_map.v b/manual/PRESENTATION_ExAdv/red_or3x1_map.v index 24ca9dab4..8c37b1dba 100644 --- a/manual/PRESENTATION_ExAdv/red_or3x1_map.v +++ b/manual/PRESENTATION_ExAdv/red_or3x1_map.v @@ -3,10 +3,10 @@ module \$reduce_or (A, Y); parameter A_SIGNED = 0; parameter A_WIDTH = 0; parameter Y_WIDTH = 0; - + input [A_WIDTH-1:0] A; output [Y_WIDTH-1:0] Y; - + function integer min; input integer a, b; begin @@ -16,7 +16,7 @@ module \$reduce_or (A, Y); min = b; end endfunction - + genvar i; generate begin if (A_WIDTH == 0) begin diff --git a/manual/PRESENTATION_ExAdv/sym_mul_map.v b/manual/PRESENTATION_ExAdv/sym_mul_map.v index 293c5b841..b4dbd9e07 100644 --- a/manual/PRESENTATION_ExAdv/sym_mul_map.v +++ b/manual/PRESENTATION_ExAdv/sym_mul_map.v @@ -4,12 +4,12 @@ module \$mul (A, B, Y); parameter A_WIDTH = 1; parameter B_WIDTH = 1; parameter Y_WIDTH = 1; - + input [A_WIDTH-1:0] A; input [B_WIDTH-1:0] B; output [Y_WIDTH-1:0] Y; - + wire _TECHMAP_FAIL_ = A_WIDTH != B_WIDTH || B_WIDTH != Y_WIDTH; - + MYMUL #( .WIDTH(Y_WIDTH) ) g ( .A(A), .B(B), .Y(Y) ); endmodule diff --git a/manual/PRESENTATION_ExOth.tex b/manual/PRESENTATION_ExOth.tex index f86dcd7ac..73f8bea2e 100644 --- a/manual/PRESENTATION_ExOth.tex +++ b/manual/PRESENTATION_ExOth.tex @@ -33,8 +33,8 @@ as {\tt \%ci} and {\tt \%co}, can be used to figure out how parts of the design are connected. \item -Commands such as {\tt submod}, {\tt expose}, {\tt splice}, \dots can be used -to transform the design into an equivialent design that is easier to analyse. +Commands such as {\tt submod}, {\tt expose}, {\tt splice}, \dots can be used +to transform the design into an equivalent design that is easier to analyse. \item Commands such as {\tt eval} and {\tt sat} can be used to investigate the @@ -102,7 +102,7 @@ Symbolic Model Checking (SMC) is used to formally prove that a circuit has (or has not) a given property. \bigskip -One appliction is Formal Equivalence Checking: Proving that two circuits +One application is Formal Equivalence Checking: Proving that two circuits are identical. For example this is a very useful feature when debugging custom passes in Yosys. @@ -115,7 +115,7 @@ The {\tt sat} command in Yosys can be used to perform Symbolic Model Checking. \end{frame} \begin{frame}[t]{Example: Formal Equivalence Checking (1/2)} -Remember the following example? +Remember the following example? \vskip1em \vbox to 0cm{ @@ -143,11 +143,11 @@ rename test test_mapped # apply the techmap only to test_mapped techmap -map techmap_01_map.v test_mapped -# create a miter circuit to test equivialence +# create a miter circuit to test equivalence miter -equiv -make_assert -make_outputs test_orig test_mapped miter flatten miter -# run equivialence check +# run equivalence check sat -verify -prove-asserts -show-inputs -show-outputs miter \end{lstlisting} diff --git a/manual/PRESENTATION_ExOth/equiv.ys b/manual/PRESENTATION_ExOth/equiv.ys index 09a4045db..8db0a88a5 100644 --- a/manual/PRESENTATION_ExOth/equiv.ys +++ b/manual/PRESENTATION_ExOth/equiv.ys @@ -9,9 +9,9 @@ rename test test_mapped # apply the techmap only to test_mapped techmap -map ../PRESENTATION_ExSyn/techmap_01_map.v test_mapped -# create a miter circuit to test equivialence +# create a miter circuit to test equivalence miter -equiv -make_assert -make_outputs test_orig test_mapped miter flatten miter -# run equivialence check +# run equivalence check sat -verify -prove-asserts -show-inputs -show-outputs miter diff --git a/manual/PRESENTATION_ExSyn.tex b/manual/PRESENTATION_ExSyn.tex index b7d6b8a6d..655720ebc 100644 --- a/manual/PRESENTATION_ExSyn.tex +++ b/manual/PRESENTATION_ExSyn.tex @@ -22,7 +22,7 @@ \item Convert remaining logic to bit-level logic functions \item Perform optimizations on bit-level logic functions \item Map bit-level logic gates and registers to cell library -\item Write results to output file +\item Write results to output file \end{itemize} \end{frame} @@ -144,16 +144,16 @@ The {\tt opt} command implements a series of simple optimizations. It also is a macro command that calls other commands: \begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -opt_const # const folding -opt_share -nomux # merging identical cells +opt_expr # const folding and simple expression rewriting +opt_merge -nomux # merging identical cells do opt_muxtree # remove never-active branches from multiplexer tree opt_reduce # consolidate trees of boolean ops to reduce functions - opt_share # merging identical cells + opt_merge # merging identical cells opt_rmdff # remove/simplify registers with constant inputs opt_clean # remove unused objects (cells, wires) from design - opt_const # const folding + opt_expr # const folding and simple expression rewriting while [changed design] \end{lstlisting} @@ -161,7 +161,7 @@ The command {\tt clean} can be used as alias for {\tt opt\_clean}. And {\tt ;;} can be used as shortcut for {\tt clean}. For example: \begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -proc; opt; memory; opt_const;; fsm;; +proc; opt; memory; opt_expr;; fsm;; \end{lstlisting} \end{frame} @@ -216,7 +216,7 @@ proc; opt; memory; opt_const;; fsm;; \begin{frame}{\subsecname} Usually it does not hurt to call {\tt opt} after each regular command in the synthesis script. But it increases the synthesis time, so it is favourable -to only call {\tt opt} when an improvement can be archieved. +to only call {\tt opt} when an improvement can be achieved. \bigskip The designs in {\tt yosys-bigsim} are a good playground for experimenting with @@ -320,7 +320,7 @@ fsm_map # unless got option -nomap \end{frame} \begin{frame}{\subsecname{} -- details} -Some details on the most importand commands from the {\tt fsm\_*} group: +Some details on the most important commands from the {\tt fsm\_*} group: \bigskip The {\tt fsm\_detect} command identifies FSM state registers and marks them diff --git a/manual/PRESENTATION_Intro.tex b/manual/PRESENTATION_Intro.tex index 5aeebd9f9..555ec9175 100644 --- a/manual/PRESENTATION_Intro.tex +++ b/manual/PRESENTATION_Intro.tex @@ -31,12 +31,12 @@ \only<3>{Netlists}% \only<4>{Hardware Description Languages (HDLs)}} \only<1>{ - Graphical representation of the circtuit topology. Circuit elements - are represented by symbols and electrical connections by lines. The gometric + Graphical representation of the circuit topology. Circuit elements + are represented by symbols and electrical connections by lines. The geometric layout is for readability only. }% \only<2>{ - The actual physical geometry of the device (PCB or ASIC manufracturing masks). + The actual physical geometry of the device (PCB or ASIC manufacturing masks). This is the final product of the design process. }% \only<3>{ @@ -86,7 +86,7 @@ }% \only<4>{ List of registers (flip-flops) and logic functions that calculate the next state from the previous one. Usually - a netlist utilizing high-level cells such as adders, multiplieres, multiplexer, etc. + a netlist utilizing high-level cells such as adders, multipliers, multiplexer, etc. }% \only<5>{ Netlist of single-bit registers and basic logic gates (such as AND, OR, @@ -95,7 +95,7 @@ }% \only<6>{ Netlist of cells that actually are available on the target architecture - (such as CMOS gates in an ASCI or LUTs in an FPGA). Optimized for + (such as CMOS gates in an ASIC or LUTs in an FPGA). Optimized for area, power, and/or speed (static timing or number of logic levels). }% \only<7>{ @@ -155,7 +155,7 @@ Things Yosys can do: \begin{itemize} \item Read and process (most of) modern Verilog-2005 code. \item Perform all kinds of operations on netlist (RTL, Logic, Gate). -\item Perform logic optimiziations and gate mapping with ABC\footnote[frame]{\url{http://www.eecs.berkeley.edu/~alanmi/abc/}}. +\item Perform logic optimizations and gate mapping with ABC\footnote[frame]{\url{http://www.eecs.berkeley.edu/~alanmi/abc/}}. \end{itemize} \bigskip @@ -176,7 +176,7 @@ as Qflow\footnote[frame]{\url{http://opencircuitdesign.com/qflow/}} for ASIC des \subsection{Yosys Data- and Control-Flow} \begin{frame}{\subsecname} - A (usually short) synthesis script controlls Yosys. + A (usually short) synthesis script controls Yosys. This scripts contain three types of commands: \begin{itemize} @@ -503,7 +503,7 @@ Commands for executing scripts or entering interactive mode: Commands for reading and elaborating the design: \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] read_ilang # read modules from ilang file - read_verilog # read modules from verilog file + read_verilog # read modules from Verilog file hierarchy # check, expand and clean up design hierarchy \end{lstlisting} @@ -536,7 +536,7 @@ Commands for writing the results: write_edif # write design to EDIF netlist file write_ilang # write design to ilang file write_spice # write design to SPICE netlist file - write_verilog # write design to verilog file + write_verilog # write design to Verilog file \end{lstlisting} \bigskip @@ -658,7 +658,7 @@ endmodule \subsection{Verification of Yosys} \begin{frame}{\subsecname} -Contiously checking the correctness of Yosys and making sure that new features +Continuously checking the correctness of Yosys and making sure that new features do not break old ones is a high priority in Yosys. \bigskip @@ -697,7 +697,7 @@ the other tools used as external reference where found and reported so far. \begin{frame}{\subsecname{} -- yosys-bigsim} yosys-bigsim is a collection of real-world open-source Verilog designs and test -benches. yosys-bigsim compares the testbench outpus of simulations of the original +benches. yosys-bigsim compares the testbench outputs of simulations of the original Verilog code and synthesis results. \bigskip @@ -721,7 +721,7 @@ The following designs are included in yosys-bigsim (excerpt): \begin{frame}{\subsecname} \begin{itemize} \item Cost (also applies to ``free as in free beer'' solutions) -\item Availablity and Reproducability +\item Availability and Reproducibility \item Framework- and all-in-one-aspects \item Educational Tool \end{itemize} @@ -739,7 +739,7 @@ the cost for the design tools needed to design the mask layouts. Open Source ASIC flows are an important enabler for ASIC-level Open Source Hardware. \bigskip -\item Availablity and Reproducability: \smallskip\par +\item Availability and Reproducibility: \smallskip\par If you are a researcher who is publishing, you want to use tools that everyone else can also use. Even if most universities have access to all major commercial tools, you usually do not have easy access to the version that was @@ -757,18 +757,18 @@ basic functionality. Extensibility was one of Yosys' design goals. \bigskip \item All-in-one: \smallskip\par -Because of the framework characterisitcs of Yosys, an increasing number of features +Because of the framework characteristics of Yosys, an increasing number of features become available in one tool. Yosys not only can be used for circuit synthesis but -also for formal equivialence checking, SAT solving, and for circuit analysis, to +also for formal equivalence checking, SAT solving, and for circuit analysis, to name just a few other application domains. With proprietary software one needs to -learn a new tool for each of this applications. +learn a new tool for each of these applications. \end{itemize} \end{frame} \begin{frame}{\subsecname{} -- 3/3} \begin{itemize} \item Educational Tool: \smallskip\par -Propritaery synthesis tools are at times very secretive about their inner +Proprietary synthesis tools are at times very secretive about their inner workings. They often are ``black boxes''. Yosys is very open about its internals and it is easy to observe the different steps of synthesis. \end{itemize} @@ -789,8 +789,8 @@ copyright notice and this permission notice appear in all copies. \begin{itemize} \item Synthesis of final production designs \item Pre-production synthesis (trial runs before investing in other tools) -\item Convertion of full-featured Verilog to simple Verilog -\item Convertion of Verilog to other formats (BLIF, BTOR, etc) +\item Conversion of full-featured Verilog to simple Verilog +\item Conversion of Verilog to other formats (BLIF, BTOR, etc) \item Demonstrating synthesis algorithms (e.g. for educational purposes) \item Framework for experimenting with new algorithms \item Framework for building custom flows\footnote[frame]{Not limited to synthesis @@ -908,7 +908,7 @@ control logic because it is simpler than setting up a commercial flow. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{Documentation, Downloads, Contatcs} +\subsection{Documentation, Downloads, Contacts} \begin{frame}{\subsecname} \begin{itemize} @@ -916,7 +916,7 @@ control logic because it is simpler than setting up a commercial flow. \smallskip\hskip1cm\url{http://www.clifford.at/yosys/} \bigskip -\item Manual, Command Reference, Appliction Notes: \\ +\item Manual, Command Reference, Application Notes: \\ \smallskip\hskip1cm\url{http://www.clifford.at/yosys/documentation.html} \bigskip diff --git a/manual/PRESENTATION_Intro/counter.ys b/manual/PRESENTATION_Intro/counter.ys index 8b3390ed4..cc4e7cd31 100644 --- a/manual/PRESENTATION_Intro/counter.ys +++ b/manual/PRESENTATION_Intro/counter.ys @@ -1,4 +1,4 @@ -# read design +# read design read_verilog counter.v hierarchy -check -top counter diff --git a/manual/PRESENTATION_Prog.tex b/manual/PRESENTATION_Prog.tex index 96189e55f..b85eda892 100644 --- a/manual/PRESENTATION_Prog.tex +++ b/manual/PRESENTATION_Prog.tex @@ -124,7 +124,7 @@ has been executed. \begin{frame}{\subsecname} The RTLIL data structures are simple structs utilizing {\tt pool<>} and -{\tt dict<>} containers (drop-in replacementments for {\tt +{\tt dict<>} containers (drop-in replacements for {\tt std::unordered\_set<>} and {\tt std::unordered\_map<>}). \bigskip @@ -325,7 +325,7 @@ Simulation models (i.e. {\it documentation\/} :-) for the internal cell library: \bigskip The lower-case cell types (such as {\tt \$and}) are parameterized cells of variable -width. This so-called {\it RTL Cells\/} are the cells described in {\tt simlib.v}. +width. This so-called {\it RTL Cells\/} are the cells described in {\tt simlib.v}. \bigskip The upper-case cell types (such as {\tt \$\_AND\_}) are single-bit cells that are not @@ -413,7 +413,7 @@ When modifying existing modules, stick to the following DOs and DON'Ts: \item Use {\tt module->fixup\_ports()} after changing the {\tt port\_*} properties of wires. -\item You can safely remove cells or change the {\tt connetions} property of a cell, but be careful when +\item You can safely remove cells or change the {\tt connections} property of a cell, but be careful when changing the size of the {\tt SigSpec} connected to a cell port. \item Use the {\tt SigMap} helper class (see next slide) when you need a unique handle for each signal bit. @@ -477,7 +477,7 @@ log("Name of this module: %s\n", log_id(module->name)); \medskip Use {\tt log\_header()} and {\tt log\_push()}/{\tt log\_pop()} to structure log messages: \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++] -log_header("Doing important stuff!\n"); +log_header(design, "Doing important stuff!\n"); log_push(); for (int i = 0; i < 10; i++) log("Log message #%d.\n", i); @@ -534,7 +534,7 @@ struct MyPass : public Pass { log("Modules in current design:\n"); for (auto mod : design->modules()) log(" %s (%d wires, %d cells)\n", log_id(mod), - GetSize(mod->wires), GetSize(mod->cells)); + GetSize(mod->wires()), GetSize(mod->cells())); } } MyPass; \end{lstlisting} diff --git a/manual/PRESENTATION_Prog/my_cmd.cc b/manual/PRESENTATION_Prog/my_cmd.cc index 1d28ce974..d99bfe1e8 100644 --- a/manual/PRESENTATION_Prog/my_cmd.cc +++ b/manual/PRESENTATION_Prog/my_cmd.cc @@ -65,7 +65,7 @@ struct Test2Pass : public Pass { log("Mapped signal x: %s\n", log_signal(sigmap(x))); - log_header("Doing important stuff!\n"); + log_header(design, "Doing important stuff!\n"); log_push(); for (int i = 0; i < 10; i++) log("Log message #%d.\n", i); diff --git a/manual/appnotes.sh b/manual/appnotes.sh index 1160af6af..0ae52862e 100755 --- a/manual/appnotes.sh +++ b/manual/appnotes.sh @@ -1,7 +1,7 @@ #!/bin/bash set -ex -for job in APPNOTE_010_Verilog_to_BLIF APPNOTE_011_Design_Investigation +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 diff --git a/manual/clean.sh b/manual/clean.sh index f4a2ea83a..11c2e7bf2 100755 --- a/manual/clean.sh +++ b/manual/clean.sh @@ -1,2 +1,2 @@ #!/bin/bash -for f in $( find . -name .gitignore ); do sed -re "s,^,find ${f%.gitignore} -name ',; s,$,' | xargs -r rm -f,;" $f; done | bash -v +for f in $( find . -name .gitignore ); do sed -re "s,^,find ${f%.gitignore} -name ',; s,$,' | xargs rm -f,;" $f; done | bash -v diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index 047ec4214..425d89b67 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -16,7 +16,7 @@ library to a target architecture. use the specified ABC script file instead of the default script. if <file> starts with a plus sign (+), then the rest of the filename - string is interprated as the command string to be passed to ABC. the + string is interpreted as the command string to be passed to ABC. The leading plus sign is removed and all commas (,) in the string are replaced with blanks before the string is passed to ABC. @@ -79,6 +79,15 @@ library to a target architecture. the area cost doubles with each additional input bit. the delay cost is still constant for all lut widths. + -luts <cost1>,<cost2>,<cost3>,<sizeN>:<cost4-N>,.. + generate netlist using luts. Use the specified costs for luts with 1, + 2, 3, .. inputs. + + -g type1,type2,... + Map the the specified list of gate types. Supported gates types are: + AND, NAND, OR, NOR, XOR, XNOR, MUX, AOI3, OAI3, AOI4, OAI4. + (The NOT gate is always added to this list automatically.) + -dff also pass $_DFF_?_ and $_DFFE_??_ cells through ABC. modules with many clock domains are automatically partitioned in clock domains and each @@ -90,7 +99,7 @@ library to a target architecture. -keepff set the "keep" attribute on flip-flop output wires. (and thus preserve - them, for example for equivialence checking.) + them, for example for equivalence checking.) -nocleanup when this option is used, the temporary files created by this pass @@ -136,6 +145,18 @@ Like 'add -input', but also connect the signal between instances of the selected modules. \end{lstlisting} +\section{aigmap -- map logic to and-inverter-graph circuit} +\label{cmd:aigmap} +\begin{lstlisting}[numbers=left,frame=single] + aigmap [options] [selection] + +Replace all logic cells with circuits made of only $_AND_ and +$_NOT_ cells. + + -nand + Enable creation of $_NAND_ cells +\end{lstlisting} + \section{alumacc -- extract ALU and MACC cells} \label{cmd:alumacc} \begin{lstlisting}[numbers=left,frame=single] @@ -156,7 +177,7 @@ This is just a shortcut for 'select -module <modname>'. cd <cellname> When no module with the specified name is found, but there is a cell -with the specified name in the current module, then this is equivialent +with the specified name in the current module, then this is equivalent to 'cd <celltype>'. cd .. @@ -164,6 +185,40 @@ to 'cd <celltype>'. This is just a shortcut for 'select -clear'. \end{lstlisting} +\section{check -- check for obvious problems in the design} +\label{cmd:check} +\begin{lstlisting}[numbers=left,frame=single] + check [options] [selection] + +This pass identifies the following problems in the current design: + + - combinatorial loops + + - two or more conflicting drivers for one wire + + - used wires that do not have a driver + +When called with -noinit then this command also checks for wires which have +the 'init' attribute set. + +When called with -assert then the command will produce an error if any +problems are found in the current design. +\end{lstlisting} + +\section{chparam -- re-evaluate modules with new parameters} +\label{cmd:chparam} +\begin{lstlisting}[numbers=left,frame=single] + chparam [ -set name value ]... [selection] + +Re-evaluate the selected modules with new parameters. String values must be +passed in double quotes ("). + + + chparam -list [selection] + +List the available parameters of the selected modules. +\end{lstlisting} + \section{clean -- remove unused cells and wires} \label{cmd:clean} \begin{lstlisting}[numbers=left,frame=single] @@ -183,8 +238,8 @@ in -purge mode between the commands. \begin{lstlisting}[numbers=left,frame=single] connect [-nomap] [-nounset] -set <lhs-expr> <rhs-expr> -Create a connection. This is equivialent to adding the statement 'assign -<lhs-expr> = <rhs-expr>;' to the verilog input. Per default, all existing +Create a connection. This is equivalent to adding the statement 'assign +<lhs-expr> = <rhs-expr>;' to the Verilog input. Per default, all existing drivers for <lhs-expr> are unconnected. This can be overwritten by using the -nounset option. @@ -216,8 +271,8 @@ This command does not operate on module with processes. Wrappers are used in coarse-grain synthesis to wrap cells with smaller ports in wrapper cells with a (larger) constant port size. I.e. the upper bits -of the wrapper outut are signed/unsigned bit extended. This command uses this -knowlege to rewire the inputs of the driven cells to match the output of +of the wrapper output are signed/unsigned bit extended. This command uses this +knowledge to rewire the inputs of the driven cells to match the output of the driving cell. -signed <cell_type> <port_name> <width_param> @@ -343,13 +398,13 @@ evaluated in the other design. design -copy-to <name> [-as <new_mod_name>] [selection] -Copy modules from the current design into the soecified one. +Copy modules from the current design into the specified one. \end{lstlisting} -\section{dff2dffe -- transform $dff cells to $dffe cells} +\section{dff2dffe -- transform \$dff cells to \$dffe cells} \label{cmd:dff2dffe} \begin{lstlisting}[numbers=left,frame=single] - dff2dffe [selection] + dff2dffe [options] [selection] This pass transforms $dff cells driven by a tree of multiplexers with one or more feedback paths to $dffe cells. It also works on gate-level cells such as @@ -365,8 +420,27 @@ $_DFF_P_, $_DFF_N_ and $_MUX_. <external_gate_type> is the cell type name for a cell with an identical interface to the <internal_gate_type>, except it also has an high-active enable port 'E'. - Usually <external_gate_type> is an intemediate cell type + Usually <external_gate_type> is an intermediate cell type that is then translated to the final type using 'techmap'. + + -direct-match <pattern> + like -direct for all DFF cell types matching the expression. + this will use $__DFFE_* as <external_gate_type> matching the + internal gate type $_DFF_*_, except for $_DFF_[NP]_, which is + converted to $_DFFE_[NP]_. +\end{lstlisting} + +\section{dffinit -- set INIT param on FF cells} +\label{cmd:dffinit} +\begin{lstlisting}[numbers=left,frame=single] + dffinit [options] [selection] + +This pass sets an FF cell parameter to the the initial value of the net it +drives. (This is primarily used in FPGA flows.) + + -ff <cell_name> <output_port> <init_param> + operate on the specified cell type. this option can be used + multiple times. \end{lstlisting} \section{dfflibmap -- technology mapping of flip-flops} @@ -385,6 +459,15 @@ to the internal cell types that best match the cells found in the given liberty file. \end{lstlisting} +\section{dffsr2dff -- convert DFFSR cells to simpler FF cell types} +\label{cmd:dffsr2dff} +\begin{lstlisting}[numbers=left,frame=single] + dffsr2dff [options] [selection] + +This pass converts DFFSR cells ($dffsr, $_DFFSR_???_) and ADFF cells ($adff, +$_DFF_???_) to simpler FF cell types when any of the set/reset inputs is unused. +\end{lstlisting} + \section{dump -- print parts of the design in ilang format} \label{cmd:dump} \begin{lstlisting}[numbers=left,frame=single] @@ -420,15 +503,29 @@ Print all commands to log before executing them. Do not print all commands to log before executing them. (default) \end{lstlisting} -\section{equiv\_add -- add a $equiv cell} +\section{edgetypes -- list all types of edges in selection} +\label{cmd:edgetypes} +\begin{lstlisting}[numbers=left,frame=single] + edgetypes [options] [selection] + +This command lists all unique types of 'edges' found in the selection. An 'edge' +is a 4-tuple of source and sink cell type and port name. +\end{lstlisting} + +\section{equiv\_add -- add a \$equiv cell} \label{cmd:equiv_add} \begin{lstlisting}[numbers=left,frame=single] - equiv_add gold_sig gate_sig + equiv_add [-try] gold_sig gate_sig This command adds an $equiv cell for the specified signals. + + + equiv_add [-try] -cell gold_cell gate_cell + +This command adds $equiv cells for the ports of the specified cells. \end{lstlisting} -\section{equiv\_induct -- proving $equiv cells using temporal induction} +\section{equiv\_induct -- proving \$equiv cells using temporal induction} \label{cmd:equiv_induct} \begin{lstlisting}[numbers=left,frame=single] equiv_induct [options] [selection] @@ -473,7 +570,7 @@ to work with the created equivalent checking module. Do not match cells or signals that match the names in the file. -encfile <file> - Match FSM encodings using the desiption from the file. + Match FSM encodings using the description from the file. See 'help fsm_recode' for details. Note: The circuit created by this command is not a miter (with something like @@ -481,6 +578,17 @@ a trigger output), but instead uses $equiv cells to encode the equivalence checking problem. Use 'miter -equiv' if you want to create a miter circuit. \end{lstlisting} +\section{equiv\_mark -- mark equivalence checking regions} +\label{cmd:equiv_mark} +\begin{lstlisting}[numbers=left,frame=single] + equiv_mark [options] [selection] + +This command marks the regions in an equivalence checking module. Region 0 is +the proven part of the circuit. Regions with higher numbers are connected +unproven subcricuits. The integer attribute 'equiv_region' is set on all +wires and cells. +\end{lstlisting} + \section{equiv\_miter -- extract miter from equiv circuit} \label{cmd:equiv_miter} \begin{lstlisting}[numbers=left,frame=single] @@ -501,7 +609,17 @@ This creates a miter module for further analysis of the selected $equiv cells. Create compare logic that handles undefs correctly \end{lstlisting} -\section{equiv\_remove -- remove $equiv cells} +\section{equiv\_purge -- purge equivalence checking module} +\label{cmd:equiv_purge} +\begin{lstlisting}[numbers=left,frame=single] + equiv_purge [options] [selection] + +This command removes the proven part of an equivalence checking module, leaving +only the unproven segments in the design. This will also remove and add module +ports as needed. +\end{lstlisting} + +\section{equiv\_remove -- remove \$equiv cells} \label{cmd:equiv_remove} \begin{lstlisting}[numbers=left,frame=single] equiv_remove [options] [selection] @@ -516,7 +634,7 @@ used then only proven cells are removed. keep gate circuit \end{lstlisting} -\section{equiv\_simple -- try proving simple $equiv instances} +\section{equiv\_simple -- try proving simple \$equiv instances} \label{cmd:equiv_simple} \begin{lstlisting}[numbers=left,frame=single] equiv_simple [options] [selection] @@ -547,6 +665,36 @@ This command prints status information for all selected $equiv cells. produce an error if any unproven $equiv cell is found \end{lstlisting} +\section{equiv\_struct -- structural equivalence checking} +\label{cmd:equiv_struct} +\begin{lstlisting}[numbers=left,frame=single] + equiv_struct [options] [selection] + +This command adds additional $equiv cells based on the assumption that the +gold and gate circuit are structurally equivalent. Note that this can introduce +bad $equiv cells in cases where the netlists are not structurally equivalent, +for example when analyzing circuits with cells with commutative inputs. This +command will also de-duplicate gates. + + -fwd + by default this command performans forward sweeps until nothing can + be merged by forwards sweeps, then backward sweeps until forward + sweeps are effective again. with this option set only forward sweeps + are performed. + + -fwonly <cell_type> + add the specified cell type to the list of cell types that are only + merged in forward sweeps and never in backward sweeps. $equiv is in + this list automatically. + + -icells + by default, the internal RTL and gate cell types are ignored. add + this option to also process those cell types with this command. + + -maxiter <N> + maximum number of iterations to run before aborting +\end{lstlisting} + \section{eval -- evaluate the circuit given an input} \label{cmd:eval} \begin{lstlisting}[numbers=left,frame=single] @@ -585,8 +733,8 @@ outputs. signal path at that wire. -shared - only expose those signals that are shared ammong the selected modules. - this is useful for preparing modules for equivialence checking. + only expose those signals that are shared among the selected modules. + this is useful for preparing modules for equivalence checking. -evert also turn connections to instances of other modules to additional @@ -609,7 +757,7 @@ outputs. This pass looks for subcircuits that are isomorphic to any of the modules in the given map file and replaces them with instances of this modules. The -map file can be a verilog source file (*.v) or an ilang file (*.il). +map file can be a Verilog source file (*.v) or an ilang file (*.il). -map <map_file> use the modules in this file as reference. This option can be used @@ -638,11 +786,11 @@ map file can be a verilog source file (*.v) or an ilang file (*.il). match. This option can be used multiple times. -swap <needle_type> <port1>,<port2>[,...] - Register a set of swapable ports for a needle cell type. + Register a set of swappable ports for a needle cell type. This option can be used multiple times. -perm <needle_type> <port1>,<port2>[,...] <portA>,<portB>[,...] - Register a valid permutation of swapable ports for a needle + Register a valid permutation of swappable ports for a needle cell type. This option can be used multiple times. -cell_attr <attribute_name> @@ -657,7 +805,7 @@ map file can be a verilog source file (*.v) or an ilang file (*.il). -ignore_param <cell_type> <parameter_name> Do not use this parameter when matching cells. -This pass does not operate on modules with uprocessed processes in it. +This pass does not operate on modules with unprocessed processes in it. (I.e. the 'proc' pass should be used first to convert processes to netlists.) This pass can also be used for mining for frequent subcircuits. In this mode @@ -694,8 +842,11 @@ See 'help techmap' for a pass that does the opposite thing. flatten [selection] This pass flattens the design by replacing cells by their implementation. This -pass is very simmilar to the 'techmap' pass. The only difference is that this +pass is very similar to the 'techmap' pass. The only difference is that this pass is using the current design as mapping library. + +Cells and/or modules with the 'keep_hierarchy' attribute set will not be +flattened by this command. \end{lstlisting} \section{freduce -- perform functional reduction} @@ -704,7 +855,7 @@ pass is using the current design as mapping library. freduce [options] [selection] This pass performs functional reduction in the circuit. I.e. if two nodes are -equivialent, they are merged to one node and one of the redundant drivers is +equivalent, they are merged to one node and one of the redundant drivers is disconnected. A subsequent call to 'clean' will remove the redundant drivers. -v, -vv @@ -722,7 +873,7 @@ disconnected. A subsequent call to 'clean' will remove the redundant drivers. operation. this is mostly used for debugging the freduce command. This pass is undef-aware, i.e. it considers don't-care values for detecting -equivialent nodes. +equivalent nodes. All selected wires are considered for rewiring. The selected cells cover the circuit that is analyzed. @@ -734,7 +885,7 @@ circuit that is analyzed. fsm [options] [selection] This pass calls all the other fsm_* passes in a useful order. This performs -FSM extraction and optimiziation. It also calls opt_clean as needed: +FSM extraction and optimization. It also calls opt_clean as needed: fsm_detect unless got option -nodetect fsm_extract @@ -759,7 +910,7 @@ Options: -expand, -norecode, -export, -nomap enable or disable passes as indicated above - -encoding tye + -encoding type -fm_set_fsm_file file -encfile file passed through to fsm_recode pass @@ -787,7 +938,7 @@ Signals can be protected from being detected by this pass by setting the The fsm_extract pass is conservative about the cells that belong to a finite state machine. This pass can be used to merge additional auxiliary gates into -the finate state machine. +the finite state machine. \end{lstlisting} \section{fsm\_export -- exporting FSMs to KISS2 files} @@ -881,9 +1032,13 @@ one-hot encoding and binary encoding is supported. \section{help -- display help messages} \label{cmd:help} \begin{lstlisting}[numbers=left,frame=single] - help ............. list all commands - help <command> ... print help message for given command - help -all ........ print complete command reference + help ................ list all commands + help <command> ...... print help message for given command + help -all ........... print complete command reference + + help -cells .......... list all cell types + help <celltype> ..... print help message for given cell type + help <celltype>+ .... print verilog code for given cell type \end{lstlisting} \section{hierarchy -- check, expand and clean up design hierarchy} @@ -903,7 +1058,7 @@ needed. -purge_lib by default the hierarchy command will not remove library (blackbox) - module. use this options to also remove unused blackbox modules. + modules. use this option to also remove unused blackbox modules. -libdir <directory> search for files named <module_name>.v in the specified directory @@ -927,6 +1082,9 @@ needed. specified top module. otherwise a module with the 'top' attribute set will implicitly be used as top module, if such a module exists. + -auto-top + automatically determine the top of the design hierarchy and mark it. + In -generate mode this pass generates blackbox modules for the given cell types (wildcards supported). For this the design is searched for cells that match the given types and then the given port declarations are used to @@ -936,7 +1094,7 @@ determine the direction of the ports. The syntax for a port declaration is: Input ports are specified with the 'i' prefix, output ports with the 'o' prefix and inout ports with the 'io' prefix. The optional <num> specifies -the position of the port in the parameter list (needed when instanciated +the position of the port in the parameter list (needed when instantiated using positional arguments). When <num> is not specified, the <portname> can also contain wildcard characters. @@ -973,6 +1131,39 @@ all commands executed in an interactive session, but not the commands from executed scripts. \end{lstlisting} +\section{ice40\_ffinit -- iCE40: handle FF init values} +\label{cmd:ice40_ffinit} +\begin{lstlisting}[numbers=left,frame=single] + ice40_ffinit [options] [selection] + +Remove zero init values for FF output signals. Add inverters to implement +nonzero init values. +\end{lstlisting} + +\section{ice40\_ffssr -- iCE40: merge synchronous set/reset into FF cells} +\label{cmd:ice40_ffssr} +\begin{lstlisting}[numbers=left,frame=single] + ice40_ffssr [options] [selection] + +Merge synchronous set/reset $_MUX_ cells into iCE40 FFs. +\end{lstlisting} + +\section{ice40\_opt -- iCE40: perform simple optimizations} +\label{cmd:ice40_opt} +\begin{lstlisting}[numbers=left,frame=single] + ice40_opt [options] [selection] + +This command executes the following script: + + do + <ice40 specific optimizations> + opt_const -mux_undef -undriven [-full] + opt_share + opt_rmdff + opt_clean + while <changed design> +\end{lstlisting} + \section{iopadmap -- technology mapping of i/o pads (or buffers)} \label{cmd:iopadmap} \begin{lstlisting}[numbers=left,frame=single] @@ -983,10 +1174,10 @@ can only map to very simple PAD cells. Use 'techmap' to further map the resulting cells to more sophisticated PAD cells. -inpad <celltype> <portname>[:<portname>] - Map module input ports to the given cell type with - the given port name. if a 2nd portname is given, the + Map module input ports to the given cell type with the + given output port name. if a 2nd portname is given, the signal is passed through the pad call, using the 2nd - portname as output. + portname as input. -outpad <celltype> <portname>[:<portname>] -inoutpad <celltype> <portname>[:<portname>] @@ -1004,6 +1195,22 @@ the resulting cells to more sophisticated PAD cells. buffers using -widthparam to set the word size on the cell.) \end{lstlisting} +\section{json -- write design in JSON format} +\label{cmd:json} +\begin{lstlisting}[numbers=left,frame=single] + json [options] [selection] + +Write a JSON netlist of all selected objects. + + -o <filename> + write to the specified file. + + -aig + also include AIG models for the different gate types + +See 'help write_json' for a description of the JSON format used. +\end{lstlisting} + \section{log -- print text and log files} \label{cmd:log} \begin{lstlisting}[numbers=left,frame=single] @@ -1038,23 +1245,31 @@ When no active module is selected, this prints a list of modules. When an active module is selected, this prints a list of objects in the module. \end{lstlisting} +\section{lut2mux -- convert \$lut to \$\_MUX\_} +\label{cmd:lut2mux} +\begin{lstlisting}[numbers=left,frame=single] + lut2mux [options] [selection] + +This pass converts $lut cells to $_MUX_ gates. +\end{lstlisting} + \section{maccmap -- mapping macc cells} \label{cmd:maccmap} \begin{lstlisting}[numbers=left,frame=single] maccmap [-unmap] [selection] -This pass maps $macc cells to yosys gate primitives. When the -unmap option is -used then the $macc cell is mapped to $and, $sub, etc. cells instead. +This pass maps $macc cells to yosys $fa and $alu cells. When the -unmap option +is used then the $macc cell is mapped to $add, $sub, etc. cells instead. \end{lstlisting} \section{memory -- translate memories to basic cells} \label{cmd:memory} \begin{lstlisting}[numbers=left,frame=single] - memory [-nomap] [-bram <bram_rules>] [selection] + memory [-nomap] [-nordff] [-bram <bram_rules>] [selection] This pass calls all the other memory_* passes in a useful order: - memory_dff + memory_dff [-nordff] opt_clean memory_share opt_clean @@ -1079,13 +1294,14 @@ The rules file contains a set of block ram description and a sequence of match rules. A block ram description looks like this: bram RAMB1024X32 # name of BRAM cell + init 1 # set to '1' if BRAM can be initialized abits 10 # number of address bits dbits 32 # number of data bits groups 2 # number of port groups ports 1 1 # number of ports in each group wrmode 1 0 # set to '1' if this groups is write ports - enable 4 0 # number of enable bits (for write ports) - transp 0 2 # transparatent (for read ports) + enable 4 1 # number of enable bits + transp 0 2 # transparent (for read ports) clocks 1 2 # clock configuration clkpol 2 2 # clock polarity configuration endbram @@ -1103,7 +1319,7 @@ and a value greater than 1 means configurable. All groups with the same value greater than 1 share the same configuration bit. Using the same bram name in different bram blocks will create different variants -of the bram. Verilog configration parameters for the bram are created as needed. +of the bram. Verilog configuration parameters for the bram are created as needed. It is also possible to create variants by repeating statements in the bram block and appending '@<label>' to the individual statements. @@ -1136,7 +1352,7 @@ It is possible to match against the following values with min/max rules: dcells ....... number of cells in 'data-direction' cells ........ total number of cells (acells*dcells*dups) -The interface for the created bram instances is dervived from the bram +The interface for the created bram instances is derived from the bram description. Use 'techmap' to convert the created bram instances into instances of the actual bram cells of your target architecture. @@ -1147,6 +1363,9 @@ the next also has 'or_next_if_better' set, and so forth). A match containing the command 'make_transp' will add external circuitry to simulate 'transparent read', if necessary. +A match containing the command 'make_outreg' will add external flip-flops +to implement synchronous read ports, if necessary. + A match containing the command 'shuffle_enable A' will re-organize the data bits to accommodate the enable pattern of port A. \end{lstlisting} @@ -1169,7 +1388,7 @@ This pass detects DFFs at memory ports and merges them into the memory port. I.e. it consumes an asynchronous memory port and the flip-flops at its interface and yields a synchronous memory port. - -wr_only + -nordfff do not merge registers on read ports \end{lstlisting} @@ -1221,7 +1440,7 @@ $memwr cells. It is the counterpart to the memory_collect pass. \begin{lstlisting}[numbers=left,frame=single] miter -equiv [options] gold_name gate_name miter_name -Creates a miter circuit for equivialence checking. The gold- and gate- modules +Creates a miter circuit for equivalence checking. The gold- and gate- modules must have the same interfaces. The miter circuit will have all inputs of the two source modules, prefixed with 'in_'. The miter circuit has a 'trigger' output that goes high if an output mismatch between the two source modules is @@ -1243,6 +1462,53 @@ detected. -flatten call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit. + + + miter -assert [options] module [miter_name] + +Creates a miter circuit for property checking. All input ports are kept, +output ports are discarded. An additional output 'trigger' is created that +goes high when an assert is violated. Without a miter_name, the existing +module is modified. + + -make_outputs + keep module output ports. + + -flatten + call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit. +\end{lstlisting} + +\section{muxcover -- cover trees of MUX cells with wider MUXes} +\label{cmd:muxcover} +\begin{lstlisting}[numbers=left,frame=single] + muxcover [options] [selection] + +Cover trees of $_MUX_ cells with $_MUX{4,8,16}_ cells + + -mux4, -mux8, -mux16 + Use the specified types of MUXes. If none of those options are used, + the effect is the same as if all of them where used. + + -nodecode + Do not insert decoder logic. This reduces the number of possible + substitutions, but guarantees that the resulting circuit is not + less efficient than the original circuit. +\end{lstlisting} + +\section{nlutmap -- map to LUTs of different sizes} +\label{cmd:nlutmap} +\begin{lstlisting}[numbers=left,frame=single] + nlutmap [options] [selection] + +This pass uses successive calls to 'abc' to map to an architecture. That +provides a small number of differently sized LUTs. + + -luts N_1,N_2,N_3,... + The number of LUTs with 1, 2, 3, ... inputs that are + available in the target architecture. + +Excess logic that does not fit into the specified LUTs is mapped back +to generic logic gates ($_AND_, etc.). \end{lstlisting} \section{opt -- perform simple optimizations} @@ -1254,23 +1520,23 @@ This pass calls all the other opt_* passes in a useful order. This performs a series of trivial optimizations and cleanups. This pass executes the other passes in the following order: - opt_const [-mux_undef] [-mux_bool] [-undriven] [-fine] [-full] [-keepdc] - opt_share -nomux + opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] + opt_share [-share_all] -nomux do opt_muxtree opt_reduce [-fine] [-full] - opt_share + opt_share [-share_all] opt_rmdff opt_clean [-purge] - opt_const [-mux_undef] [-mux_bool] [-undriven] [-fine] [-full] [-keepdc] + opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] while <changed design> When called with -fast the following script is used instead: do - opt_const [-mux_undef] [-mux_bool] [-undriven] [-fine] [-full] [-keepdc] - opt_share + opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc] + opt_share [-share_all] opt_rmdff opt_clean [-purge] while <changed design in opt_rmdff> @@ -1311,6 +1577,9 @@ This pass performs const folding on internal cell types with constant inputs. -undriven replace undriven nets with undef (x) constants + -clkinv + optimize clock inverters by changing FF types + -fine perform fine-grain optimizations @@ -1368,13 +1637,16 @@ a constant driver. \section{opt\_share -- consolidate identical cells} \label{cmd:opt_share} \begin{lstlisting}[numbers=left,frame=single] - opt_share [-nomux] [selection] + opt_share [options] [selection] This pass identifies cells with identical type and input signals. Such cells are then merged to one cell. -nomux Do not merge MUX cells. + + -share_all + Operate on all cell types, not just built-in types. \end{lstlisting} \section{plugin -- load and list loaded plugins} @@ -1394,6 +1666,57 @@ Load and list loaded plugins. List loaded plugins \end{lstlisting} +\section{pmuxtree -- transform \$pmux cells to trees of \$mux cells} +\label{cmd:pmuxtree} +\begin{lstlisting}[numbers=left,frame=single] + pmuxtree [options] [selection] + +This pass transforms $pmux cells to a trees of $mux cells. +\end{lstlisting} + +\section{prep -- generic synthesis script} +\label{cmd:prep} +\begin{lstlisting}[numbers=left,frame=single] + prep [options] + +This command runs a conservative RTL synthesis. A typical application for this +is the preparation stage of a verification flow. This command does not operate +on partly selected designs. + + -top <module> + use the specified module as top module (default='top') + + -nordff + passed to 'memory_dff'. prohibits merging of FFs into memory read ports + + -run <from_label>[:<to_label>] + only run the commands between the labels (see below). an empty + from label is synonymous to 'begin', and empty to label is + synonymous to the end of the command list. + + +The following commands are executed by this synthesis command: + + begin: + hierarchy -check [-top <top>] + + prep: + proc + opt_const + opt_clean + check + opt -keepdc + wreduce + memory_dff [-nordff] + opt_clean + memory_collect + opt -keepdc -fast + + check: + stat + check +\end{lstlisting} + \section{proc -- translate processes to netlists} \label{cmd:proc} \begin{lstlisting}[numbers=left,frame=single] @@ -1406,10 +1729,12 @@ This pass calls all the other proc_* passes in the most common order. proc_init proc_arst proc_mux + proc_dlatch proc_dff proc_clean -This replaces the processes in the design with multiplexers and flip-flops. +This replaces the processes in the design with multiplexers, +flip-flops and latches. The following options are supported: @@ -1452,12 +1777,21 @@ This pass identifies flip-flops in the processes and converts them to d-type flip-flop cells. \end{lstlisting} +\section{proc\_dlatch -- extract latches from processes} +\label{cmd:proc_dlatch} +\begin{lstlisting}[numbers=left,frame=single] + proc_dlatch [selection] + +This pass identifies latches in the processes and converts them to +d-type latches. +\end{lstlisting} + \section{proc\_init -- convert initial block to init attributes} \label{cmd:proc_init} \begin{lstlisting}[numbers=left,frame=single] proc_init [selection] -This pass extracts the 'init' actions from processes (generated from verilog +This pass extracts the 'init' actions from processes (generated from Verilog 'initial' blocks) and sets the initial value to the 'init' attribute on the respective wire. \end{lstlisting} @@ -1479,6 +1813,40 @@ and case statements) to trees of multiplexer cells. This pass identifies unreachable branches in decision trees and removes them. \end{lstlisting} +\section{qwp -- quadratic wirelength placer} +\label{cmd:qwp} +\begin{lstlisting}[numbers=left,frame=single] + qwp [options] [selection] + +This command runs quadratic wirelength placement on the selected modules and +annotates the cells in the design with 'qwp_position' attributes. + + -ltr + Add left-to-right constraints: constrain all inputs on the left border + outputs to the right border. + + -alpha + Add constraints for inputs/outputs to be placed in alphanumerical + order along the y-axis (top-to-bottom). + + -grid N + Number of grid divisions in x- and y-direction. (default=16) + + -dump <html_file_name> + Dump a protocol of the placement algorithm to the html file. + +Note: This implementation of a quadratic wirelength placer uses exact +dense matrix operations. It is only a toy-placer for small circuits. +\end{lstlisting} + +\section{read\_blif -- read BLIF file} +\label{cmd:read_blif} +\begin{lstlisting}[numbers=left,frame=single] + read_blif [filename] + +Load modules from a BLIF file into the current design. +\end{lstlisting} + \section{read\_ilang -- read modules from ilang file} \label{cmd:read_ilang} \begin{lstlisting}[numbers=left,frame=single] @@ -1513,18 +1881,22 @@ Read cells from liberty file as modules into current design. set the specified attribute (to the value 1) on all loaded modules \end{lstlisting} -\section{read\_verilog -- read modules from verilog file} +\section{read\_verilog -- read modules from Verilog file} \label{cmd:read_verilog} \begin{lstlisting}[numbers=left,frame=single] read_verilog [options] [filename] -Load modules from a verilog file to the current design. A large subset of +Load modules from a Verilog file to the current design. A large subset of Verilog-2005 is supported. -sv enable support for SystemVerilog features. (only a small subset of SystemVerilog is supported) + -formal + enable support for assert() and assume() from SystemVerilog + replace the implicit -D SYNTHESIS with -D FORMAL + -dump_ast1 dump abstract syntax tree (before simplification) @@ -1532,7 +1904,7 @@ Verilog-2005 is supported. dump abstract syntax tree (after simplification) -dump_vlog - dump ast as verilog code (after simplification) + dump ast as Verilog code (after simplification) -yydebug enable parser debug output @@ -1554,19 +1926,31 @@ Verilog-2005 is supported. this can also be achieved by setting the 'nomem2reg' attribute on the respective module or register. + This is potentially dangerous. Usually the front-end has good + reasons for converting an array to a list of registers. + Prohibiting this step will likely result in incorrect synthesis + results. + -mem2reg always convert memories to registers. this can also be achieved by setting the 'mem2reg' attribute on the respective module or register. + -nomeminit + do not infer $meminit cells and instead convert initialized + memories to registers directly in the front-end. + -ppdump - dump verilog code after pre-processor + dump Verilog code after pre-processor -nopp do not run the pre-processor + -nodpi + disable DPI-C support + -lib - only create empty blackbox modules + only create empty blackbox modules. This implies -DBLACKBOX. -noopt don't perform basic optimizations (such as const folding) in the @@ -1584,6 +1968,9 @@ Verilog-2005 is supported. to a later 'hierarchy' command. Useful in cases where the default parameters of modules yield invalid or not synthesizable code. + -noautowire + make the default of `default_nettype be "none" instead of "wire". + -setattr <attribute_name> set the specified attribute (to the value 1) on all loaded modules @@ -1600,7 +1987,7 @@ subsequent calls to 'read_verilog'. Note that the Verilog frontend does a pretty good job of processing valid verilog input, but has not very good error reporting. It generally is -recommended to use a simulator (for example icarus verilog) for checking +recommended to use a simulator (for example Icarus Verilog) for checking the syntax of the code, rather than to rely on read_verilog for that. \end{lstlisting} @@ -1624,6 +2011,10 @@ pattern is '_%_'. Assign private names (the ones with $-prefix) to all selected wires and cells with public names. This ignores all selected ports. + + rename -top new_name + +Rename top module. \end{lstlisting} \section{sat -- solve a SAT problem in the circuit} @@ -1671,6 +2062,9 @@ and additional constraints passed as parameters. -show-inputs, -show-outputs, -show-ports add all module (input/output) ports to the list of shown signals + -show-regs, -show-public, -show-all + show all registers, show signals with 'public' names, show all signals + -ignore_div_by_zero ignore all solutions that involve a division by zero @@ -1683,11 +2077,17 @@ The following options can be used to set up a sequential problem: set up a sequential problem with <N> time steps. The steps will be numbered from 1 to N. + note: for large <N> it can be significantly faster to use + -tempinduct-baseonly -maxsteps <N> instead of -seq <N>. + -set-at <N> <signal> <value> -unset-at <N> <signal> set or unset the specified signal to the specified value in the given timestep. this has priority over a -set for the same signal. + -set-assumes + set all assumptions provided via $assume cells + -set-def-at <N> <signal> -set-any-undef-at <N> <signal> -set-all-undef-at <N> <signal> @@ -1708,6 +2108,9 @@ The following options can be used to set up a sequential problem: -dump_vcd <vcd-file-name> dump SAT model (counter example in proof) to VCD file + -dump_json <json-file-name> + dump SAT model (counter example in proof) to a WaveJSON file. + -dump_cnf <cnf-file-name> dump CNF of SAT problem (in DIMACS format). in temporal induction proofs this is the CNF of the first induction step. @@ -1716,7 +2119,7 @@ The following additional options can be used to set up a proof. If also -seq is passed, a temporal induction proof is performed. -tempinduct - Perform a temporal induction proof. In a temporalinduction proof it is + Perform a temporal induction proof. In a temporal induction proof it is proven that the condition holds forever after the number of time steps specified using -seq. @@ -1724,12 +2127,26 @@ is passed, a temporal induction proof is performed. Perform a temporal induction proof. Assume an initial state with all registers set to defined values for the induction step. + -tempinduct-baseonly + Run only the basecase half of temporal induction (requires -maxsteps) + + -tempinduct-inductonly + Run only the induction half of temporal induction + + -tempinduct-skip <N> + Skip the first <N> steps of the induction proof. + + note: this will assume that the base case holds for <N> steps. + this must be proven independently with "-tempinduct-baseonly + -maxsteps <N>". Use -initsteps if you just want to set a + minimal induction length. + -prove <signal> <value> Attempt to proof that <signal> is always <value>. -prove-x <signal> <value> Like -prove, but an undef (x) bit in the lhs matches any value on - the right hand side. Useful for equivialence checking. + the right hand side. Useful for equivalence checking. -prove-asserts Prove that all asserts in the design hold. @@ -1742,6 +2159,13 @@ is passed, a temporal induction proof is performed. -initsteps <N> Set initial length for the induction. + This will speed up the search of the right induction length + for deep induction proofs. + + -stepsize <N> + Increase the size of the induction proof in steps of <N>. + This will speed up the search of the right induction length + for deep induction proofs. -timeout <N> Maximum number of seconds a single SAT instance may take. @@ -1780,10 +2204,18 @@ Use the opt_clean command to get rid of the additional nets. This command identifies strongly connected components (aka logic loops) in the design. + -expect <num> + expect to find exactly <num> SSCs. A different number of SSCs will + produce an error. + -max_depth <num> - limit to loops not longer than the specified number of cells. This can - e.g. be useful in identifying local loops in a module that turns out - to be one gigantic SCC. + limit to loops not longer than the specified number of cells. This + can e.g. be useful in identifying small local loops in a module that + implements one large SCC. + + -nofeedback + do not count cells that have their output fed back into one of their + inputs as single-cell scc. -all_cell_types Usually this command only considers internal non-memory cells. With @@ -1978,7 +2410,7 @@ The following actions can be performed on the top sets on the stack: like %d but swap the roles of two top sets on the stack %c - create a copy of the top set rom the stack and push it + create a copy of the top set from the stack and push it %x[<num1>|*][.<num2>][:<rule>[:<rule>..]] expand top set <num1> num times according to the specified rules. @@ -1995,19 +2427,31 @@ The following actions can be performed on the top sets on the stack: %ci[<num1>|*][.<num2>][:<rule>[:<rule>..]] %co[<num1>|*][.<num2>][:<rule>[:<rule>..]] - simmilar to %x, but only select input (%ci) or output cones (%co) + similar to %x, but only select input (%ci) or output cones (%co) + + %xe[...] %cie[...] %coe + like %x, %ci, and %co but only consider combinatorial cells %a expand top set by selecting all wires that are (at least in part) aliases for selected wires. %s - expand top set by adding all modules of instantiated cells in selected + expand top set by adding all modules that implement cells in selected modules %m expand top set by selecting all modules that contain selected objects + %M + select modules that implement selected cells + + %C + select cells that implement selected modules + + %R[<num>] + select <num> random objects from top selection (default 1) + Example: the following command selects all wires that are connected to a 'GATE' input of a 'SWITCH' cell: @@ -2080,7 +2524,7 @@ is used to determine if two resources are share-able. -fast Only consider the simple part of the control logic in SAT solving, resulting - in much easier SAT problems at the cost of maybe missing some oportunities + in much easier SAT problems at the cost of maybe missing some opportunities for resource sharing. -limit N @@ -2140,6 +2584,10 @@ to a graphics file (usually SVG or PostScript). inputs or outputs. This option can be used multiple times to specify more than one library. + note: in most cases it is better to load the library before calling + show with 'read_verilog -lib <filename>'. it is also possible to + load liberty files with 'read_liberty -lib <filename>'. + -prefix <prefix> generate <prefix>.* instead of ~/.yosys_show.* @@ -2156,7 +2604,7 @@ to a graphics file (usually SVG or PostScript). -colors <seed> Randomly assign colors to the wires. The integer argument is the seed for the random number generator. Change the seed value if the colored - graph still is ambigous. A seed of zero deactivates the coloring. + graph still is ambiguous. A seed of zero deactivates the coloring. -colorattr <attribute_name> Use the specified attribute to assign colors. A unique color is @@ -2166,7 +2614,7 @@ to a graphics file (usually SVG or PostScript). annotate busses with a label indicating the width of the bus. -signed - mark ports (A, B) that are declarted as signed (using the [AB]_SIGNED + mark ports (A, B) that are declared as signed (using the [AB]_SIGNED cell parameter) with an asterisk next to the port name. -stretch @@ -2180,7 +2628,7 @@ to a graphics file (usually SVG or PostScript). enumerate objects with internal ($-prefixed) names -long - do not abbeviate objects with internal ($-prefixed) names + do not abbreviate objects with internal ($-prefixed) names -notitle do not add the module name as graph title to the dot file @@ -2190,6 +2638,9 @@ specified, 'xdot' is used to display the schematic. The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>', unless another prefix is specified using -prefix <prefix>. + +Yosys on Windows and YosysJS use different defaults: The output is written +to 'show.dot' in the current directory and new viewer is launched. \end{lstlisting} \section{simplemap -- mapping simple coarse-grain cells} @@ -2202,10 +2653,26 @@ primitives. The following internal cell types are mapped by this pass: $not, $pos, $and, $or, $xor, $xnor $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool - $logic_not, $logic_and, $logic_or, $mux + $logic_not, $logic_and, $logic_or, $mux, $tribuf $sr, $dff, $dffsr, $adff, $dlatch \end{lstlisting} +\section{singleton -- create singleton modules} +\label{cmd:singleton} +\begin{lstlisting}[numbers=left,frame=single] + singleton [selection] + +By default, a module that is instantiated by several other modules is only +kept once in the design. This preserves the original modularity of the design +and reduces the overall size of the design in memory. But it prevents certain +optimizations and other operations on the design. This pass creates singleton +modules for all selected cells. The created modules are marked with the +'singleton' attribute. + +This commands only operates on modules that by themself have the 'singleton' +attribute set (the 'top' module is a singleton implicitly). +\end{lstlisting} + \section{splice -- create explicit splicing cells} \label{cmd:splice} \begin{lstlisting}[numbers=left,frame=single] @@ -2213,7 +2680,7 @@ primitives. The following internal cell types are mapped by this pass: This command adds $slice and $concat cells to the design to make the splicing of multi-bit signals explicit. This for example is useful for coarse grain -synthesis, where dedidacted hardware is needed to splice signals. +synthesis, where dedicated hardware is needed to splice signals. -sel_by_cell only select the cell ports to rewire by the cell. if the selection @@ -2228,6 +2695,9 @@ synthesis, where dedidacted hardware is needed to splice signals. it is sufficient if the driver of any bit of a cell port is selected. by default all bits must be selected. + -wires + also add $slice and $concat cells to drive otherwise unused wires. + -no_outputs do not rewire selected module outputs. @@ -2277,6 +2747,9 @@ design. selected and a module has the 'top' attribute set, this module is used default value for this option. + -liberty <liberty_file> + use cell area information from the provided liberty file + -width annotate internal cell types with their word width. e.g. $add_8 for an 8 bit wide $add cell. @@ -2285,7 +2758,7 @@ design. \section{submod -- moving part of a module to a new submodule} \label{cmd:submod} \begin{lstlisting}[numbers=left,frame=single] - submod [selection] + submod [-copy] [selection] This pass identifies all cells with the 'submod' attribute and moves them to a newly created module. The value of the attribute is used as name for the @@ -2298,11 +2771,15 @@ This pass only operates on completely selected modules with no processes or memories. - submod -name <name> [selection] + submod -name <name> [-copy] [selection] As above, but don't use the 'submod' attribute but instead use the selection. Only objects from one module might be selected. The value of the -name option is used as the value of the 'submod' attribute above. + +By default the cells are 'moved' from the source module and the source module +will use an instance of the new module after this command is finished. Call +with -copy to not modify the source module. \end{lstlisting} \section{synth -- generic synthesis script} @@ -2319,9 +2796,19 @@ on partly selected designs. -encfile <file> passed to 'fsm_recode' via 'fsm' + -nofsm + do not run FSM optimization + -noabc do not run abc (as if yosys was compiled without ABC support) + -noalumacc + do not run 'alumacc' pass. i.e. keep arithmetic operators in + their direct form ($add, $sub, etc.). + + -nordff + passed to 'memory'. prohibits merging of FFs into memory read ports + -run <from_label>[:<to_label>] only run the commands between the labels (see below). an empty from label is synonymous to 'begin', and empty to label is @@ -2335,6 +2822,9 @@ The following commands are executed by this synthesis command: coarse: proc + opt_const + opt_clean + check opt wreduce alumacc @@ -2351,10 +2841,183 @@ The following commands are executed by this synthesis command: opt -full techmap opt -fast - - abc: abc -fast opt -fast + + check: + hierarchy -check + stat + check +\end{lstlisting} + +\section{synth\_greenpak4 -- synthesis for GreenPAK4 FPGAs} +\label{cmd:synth_greenpak4} +\begin{lstlisting}[numbers=left,frame=single] + synth_greenpak4 [options] + +This command runs synthesis for GreenPAK4 FPGAs. This work is experimental. + + -top <module> + use the specified module as top module (default='top') + + -blif <file> + write the design to the specified BLIF file. writing of an output file + is omitted if this parameter is not specified. + + -edif <file> + write the design to the specified edif file. writing of an output file + is omitted if this parameter is not specified. + + -run <from_label>:<to_label> + only run the commands between the labels (see below). an empty + from label is synonymous to 'begin', and empty to label is + synonymous to the end of the command list. + + -noflatten + do not flatten design before synthesis + + -retime + run 'abc' with -dff option + + +The following commands are executed by this synthesis command: + + begin: + read_verilog -lib +/greenpak4/cells_sim.v + hierarchy -check -top <top> + + flatten: (unless -noflatten) + proc + flatten + tribuf -logic + + coarse: + synth -run coarse + + fine: + opt -fast -mux_undef -undriven -fine + memory_map + opt -undriven -fine + techmap + dfflibmap -prepare -liberty +/greenpak4/gp_dff.lib + opt -fast + abc -dff (only if -retime) + + map_luts: + nlutmap -luts 0,8,16,2 + clean + + map_cells: + techmap -map +/greenpak4/cells_map.v + clean + + check: + hierarchy -check + stat + check -noinit + + blif: + write_blif -gates -attr -param <file-name> + + edif: + write_edif <file-name> +\end{lstlisting} + +\section{synth\_ice40 -- synthesis for iCE40 FPGAs} +\label{cmd:synth_ice40} +\begin{lstlisting}[numbers=left,frame=single] + synth_ice40 [options] + +This command runs synthesis for iCE40 FPGAs. This work is experimental. + + -top <module> + use the specified module as top module (default='top') + + -blif <file> + write the design to the specified BLIF file. writing of an output file + is omitted if this parameter is not specified. + + -edif <file> + write the design to the specified edif file. writing of an output file + is omitted if this parameter is not specified. + + -run <from_label>:<to_label> + only run the commands between the labels (see below). an empty + from label is synonymous to 'begin', and empty to label is + synonymous to the end of the command list. + + -noflatten + do not flatten design before synthesis + + -retime + run 'abc' with -dff option + + -nocarry + do not use SB_CARRY cells in output netlist + + -nobram + do not use SB_RAM40_4K* cells in output netlist + + -abc2 + run two passes of 'abc' for slightly improved logic density + + +The following commands are executed by this synthesis command: + + begin: + read_verilog -lib +/ice40/cells_sim.v + hierarchy -check -top <top> + + flatten: (unless -noflatten) + proc + flatten + tribuf -logic + + coarse: + synth -run coarse + + bram: (skip if -nobram) + memory_bram -rules +/ice40/brams.txt + techmap -map +/ice40/brams_map.v + + fine: + opt -fast -mux_undef -undriven -fine + memory_map + opt -undriven -fine + techmap -map +/techmap.v [-map +/ice40/arith_map.v] + abc -dff (only if -retime) + ice40_opt + + map_ffs: + dffsr2dff + dff2dffe -direct-match $_DFF_* + techmap -map +/ice40/cells_map.v + opt_const -mux_undef + simplemap + ice40_ffinit + ice40_ffssr + ice40_opt -full + + map_luts: + abc (only if -abc2) + ice40_opt (only if -abc2) + abc -lut 4 + clean + + map_cells: + techmap -map +/ice40/cells_map.v + clean + + check: + hierarchy -check + stat + check -noinit + + blif: + write_blif -gates -attr -param <file-name> + + edif: + write_edif <file-name> \end{lstlisting} \section{synth\_xilinx -- synthesis for Xilinx FPGAs} @@ -2367,7 +3030,7 @@ partly selected designs. At the moment this command creates netlists that are compatible with 7-Series Xilinx devices. -top <module> - use the specified module as top module (default='top') + use the specified module as top module -edif <file> write the design to the specified edif file. writing of an output file @@ -2389,6 +3052,8 @@ The following commands are executed by this synthesis command: begin: read_verilog -lib +/xilinx/cells_sim.v + read_verilog -lib +/xilinx/brams_bb.v + read_verilog -lib +/xilinx/drams_bb.v hierarchy -check -top <top> flatten: (only if -flatten) @@ -2397,29 +3062,40 @@ The following commands are executed by this synthesis command: coarse: synth -run coarse - dff2dffe bram: memory_bram -rules +/xilinx/brams.txt techmap -map +/xilinx/brams_map.v + dram: + memory_bram -rules +/xilinx/drams.txt + techmap -map +/xilinx/drams_map.v + fine: opt -fast -full memory_map + dffsr2dff + dff2dffe opt -full techmap -map +/techmap.v -map +/xilinx/arith_map.v opt -fast map_luts: - abc -lut 5:8 [-dff] + abc -luts 2:2,3,6:5,10,20 [-dff] clean map_cells: techmap -map +/xilinx/cells_map.v + dffinit -ff FDRE Q INIT -ff FDCE Q INIT -ff FDPE Q INIT clean - edif: - write_edif synth.edif + check: + hierarchy -check + stat + check -noinit + + edif: (only if -edif) + write_edif <file-name> \end{lstlisting} \section{tcl -- execute a TCL script file} @@ -2433,7 +3109,7 @@ Use 'yosys cmd' to run the yosys command 'cmd' from tcl. The tcl command 'yosys -import' can be used to import all yosys commands directly as tcl commands to the tcl shell. The yosys command 'proc' is wrapped using the tcl command 'procs' in order -to avoid a name collision with the tcl builting command 'proc'. +to avoid a name collision with the tcl builtin command 'proc'. \end{lstlisting} \section{techmap -- generic technology mapper} @@ -2442,7 +3118,7 @@ to avoid a name collision with the tcl builting command 'proc'. techmap [-map filename] [selection] This pass implements a very simple technology mapper that replaces cells in -the design with implementations given in form of a verilog or ilang source +the design with implementations given in form of a Verilog or ilang source file. -map filename @@ -2454,11 +3130,6 @@ file. -map %<design-name> like -map above, but with an in-memory design instead of a file. - -share_map filename - like -map, but look for the file in the share directory (where the - yosys data files are). this is mainly used internally when techmap - is called from other commands. - -extern load the cell implementations as separate modules into the design instead of inlining them. @@ -2468,7 +3139,7 @@ file. -recursive instead of the iterative breadth-first algorithm use a recursive - depth-first algorithm. both methods should yield equivialent results, + depth-first algorithm. both methods should yield equivalent results, but may differ in performance. -autoproc @@ -2480,8 +3151,8 @@ file. as final cell types by this mode. -D <define>, -I <incdir> - this options are passed as-is to the verilog frontend for loading the - map file. Note that the verilog frontend is also called with the + this options are passed as-is to the Verilog frontend for loading the + map file. Note that the Verilog frontend is also called with the '-ignore_redef' option set. When a module in the map file has the 'techmap_celltype' attribute set, it will @@ -2527,7 +3198,7 @@ wires are supported: of constant inputs and shorted inputs at this point and import the constant and connected bits into the map module. All further commands are executed in this copy. This is a very convenient way of creating - optimizied specializations of techmap modules without using the special + optimized specializations of techmap modules without using the special parameters described below. A _TECHMAP_DO_* command may start with the special token 'RECURSION; '. @@ -2563,12 +3234,12 @@ the design is connected to a constant value. The parameter is then set to the constant value. A cell with the name _TECHMAP_REPLACE_ in the map file will inherit the name -of the cell that is beeing replaced. +of the cell that is being replaced. See 'help extract' for a pass that does the opposite thing. See 'help flatten' for a pass that does flatten the design (which is -esentially techmap but using the design itself as map library). +essentially techmap but using the design itself as map library). \end{lstlisting} \section{tee -- redirect command output to file} @@ -2608,7 +3279,7 @@ Test handling of logic loops in ABC. \begin{lstlisting}[numbers=left,frame=single] test_autotb [options] [filename] -Automatically create primitive verilog test benches for all modules in the +Automatically create primitive Verilog test benches for all modules in the design. The generated testbenches toggle the input pins of the module in a semi-random manner and dumps the resulting output signals. @@ -2624,7 +3295,7 @@ value after initialization. This can e.g. be used to force a reset signal low in order to explore more inner states in a state machine. -n <int> - number of iterations the test bench shuld run (default = 1000) + number of iterations the test bench should run (default = 1000) \end{lstlisting} \section{test\_cell -- automatically test the implementation of a cell type} @@ -2657,6 +3328,9 @@ cell types. Use for example 'all /$add' for all cell types except $add. -simlib use "techmap -map +/simlib.v -max_iter 2 -autoproc" + -aigmap + instead of calling "techmap", call "aigmap" + -muxdiv when creating test benches with dividers, create an additional mux to mask out the division-by-zero case @@ -2670,11 +3344,29 @@ cell types. Use for example 'all /$add' for all cell types except $add. -nosat do not check SAT model or run SAT equivalence checking + -noeval + do not check const-eval models + -v print additional debug information to the console -vlog {filename} - create a verilog test bench to test simlib and write_verilog + create a Verilog test bench to test simlib and write_verilog +\end{lstlisting} + +\section{torder -- print cells in topological order} +\label{cmd:torder} +\begin{lstlisting}[numbers=left,frame=single] + torder [options] [selection] + +This command prints the selected cells in topological order. + + -stop <cell_type> <cell_port> + do not use the specified cell port in topological sorting + + -noautostop + by default Q outputs of internal FF cells and memory read port outputs + are not used in topological sorting. this option deactivates that. \end{lstlisting} \section{trace -- redirect command output to file} @@ -2686,6 +3378,22 @@ Execute the specified command, logging all changes the command performs on the design in real time. \end{lstlisting} +\section{tribuf -- infer tri-state buffers} +\label{cmd:tribuf} +\begin{lstlisting}[numbers=left,frame=single] + tribuf [options] [selection] + +This pass transforms $mux cells with 'z' inputs to tristate buffers. + + -merge + merge multiple tri-state buffers driving the same net + into a single buffer. + + -logic + convert tri-state buffers that do not drive output ports + to non-tristate logic. this option implies -merge. +\end{lstlisting} + \section{verific -- load Verilog and VHDL designs using Verific} \label{cmd:verific} \begin{lstlisting}[numbers=left,frame=single] @@ -2701,7 +3409,7 @@ Load the specified VHDL files into Verific. verific -import [-gates] {-all | <top-module>..} -Elaborate the design for the sepcified top modules, import to Yosys and +Elaborate the design for the specified top modules, import to Yosys and reset the internal state of Verific. A gate-level netlist is created when called with -gates. @@ -2713,11 +3421,11 @@ Visit http://verific.com/ for more information on Verific. \begin{lstlisting}[numbers=left,frame=single] verilog_defaults -add [options] -Add the sepcified options to the list of default options to read_verilog. +Add the specified options to the list of default options to read_verilog. verilog_defaults -clear -Clear the list of verilog default options. +Clear the list of Verilog default options. verilog_defaults -push verilog_defaults -pop @@ -2761,7 +3469,7 @@ vhdl2verilog can be obtained from: http://www.edautils.com/vhdl2verilog.html \end{lstlisting} -\section{wreduce -- reduce the word size of operations is possible} +\section{wreduce -- reduce the word size of operations if possible} \label{cmd:wreduce} \begin{lstlisting}[numbers=left,frame=single] wreduce [options] [selection] @@ -2815,8 +3523,14 @@ file *.blif when any of this options is used. do not generate buffers for connected wires. instead use the non-standard .conn statement. + -attr + use the non-standard .attr statement to write cell attributes + -param - use the non-standard .param statement to write module parameters + use the non-standard .param statement to write cell parameters + + -cname + use the non-standard .cname statement to write cell names -blackbox write blackbox cells with .blackbox statement. @@ -2854,7 +3568,7 @@ is targeted. \begin{lstlisting}[numbers=left,frame=single] write_file [options] output_file [input_file] -Write the text fron the input file to the output file. +Write the text from the input file to the output file. -a Append to output file (instead of overwriting) @@ -2903,14 +3617,217 @@ a tool for Coarse-Grain Example-Driven Interconnect Synthesis. http://www.clifford.at/intersynth/ \end{lstlisting} +\section{write\_json -- write design to a JSON file} +\label{cmd:write_json} +\begin{lstlisting}[numbers=left,frame=single] + write_json [options] [filename] + +Write a JSON netlist of the current design. + + -aig + include AIG models for the different gate types + + +The general syntax of the JSON output created by this command is as follows: + + { + "modules": { + <module_name>: { + "ports": { + <port_name>: <port_details>, + ... + }, + "cells": { + <cell_name>: <cell_details>, + ... + }, + "netnames": { + <net_name>: <net_details>, + ... + } + } + }, + "models": { + ... + }, + } + +Where <port_details> is: + + { + "direction": <"input" | "output" | "inout">, + "bits": <bit_vector> + } + +And <cell_details> is: + + { + "hide_name": <1 | 0>, + "type": <cell_type>, + "parameters": { + <parameter_name>: <parameter_value>, + ... + }, + "attributes": { + <attribute_name>: <attribute_value>, + ... + }, + "port_directions": { + <port_name>: <"input" | "output" | "inout">, + ... + }, + "connections": { + <port_name>: <bit_vector>, + ... + }, + } + +And <net_details> is: + + { + "hide_name": <1 | 0>, + "bits": <bit_vector> + } + +The "hide_name" fields are set to 1 when the name of this cell or net is +automatically created and is likely not of interest for a regular user. + +The "port_directions" section is only included for cells for which the +interface is known. + +Module and cell ports and nets can be single bit wide or vectors of multiple +bits. Each individual signal bit is assigned a unique integer. The <bit_vector> +values referenced above are vectors of this integers. Signal bits that are +connected to a constant driver are denoted as string "0" or "1" instead of +a number. + +For example the following Verilog code: + + module test(input x, y); + (* keep *) foo #(.P(42), .Q(1337)) + foo_inst (.A({x, y}), .B({y, x}), .C({4'd10, {4{x}}})); + endmodule + +Translates to the following JSON output: + + { + "modules": { + "test": { + "ports": { + "x": { + "direction": "input", + "bits": [ 2 ] + }, + "y": { + "direction": "input", + "bits": [ 3 ] + } + }, + "cells": { + "foo_inst": { + "hide_name": 0, + "type": "foo", + "parameters": { + "Q": 1337, + "P": 42 + }, + "attributes": { + "keep": 1, + "src": "test.v:2" + }, + "connections": { + "C": [ 2, 2, 2, 2, "0", "1", "0", "1" ], + "B": [ 2, 3 ], + "A": [ 3, 2 ] + } + } + }, + "netnames": { + "y": { + "hide_name": 0, + "bits": [ 3 ], + "attributes": { + "src": "test.v:1" + } + }, + "x": { + "hide_name": 0, + "bits": [ 2 ], + "attributes": { + "src": "test.v:1" + } + } + } + } + } + } + +The models are given as And-Inverter-Graphs (AIGs) in the following form: + + "models": { + <model_name>: [ + /* 0 */ [ <node-spec> ], + /* 1 */ [ <node-spec> ], + /* 2 */ [ <node-spec> ], + ... + ], + ... + }, + +The following node-types may be used: + + [ "port", <portname>, <bitindex>, <out-list> ] + - the value of the specified input port bit + + [ "nport", <portname>, <bitindex>, <out-list> ] + - the inverted value of the specified input port bit + + [ "and", <node-index>, <node-index>, <out-list> ] + - the ANDed value of the specified nodes + + [ "nand", <node-index>, <node-index>, <out-list> ] + - the inverted ANDed value of the specified nodes + + [ "true", <out-list> ] + - the constant value 1 + + [ "false", <out-list> ] + - the constant value 0 + +All nodes appear in topological order. I.e. only nodes with smaller indices +are referenced by "and" and "nand" nodes. + +The optional <out-list> at the end of a node specification is a list of +output portname and bitindex pairs, specifying the outputs driven by this node. + +For example, the following is the model for a 3-input 3-output $reduce_and cell +inferred by the following code: + + module test(input [2:0] in, output [2:0] out); + assign in = &out; + endmodule + + "$reduce_and:3U:3": [ + /* 0 */ [ "port", "A", 0 ], + /* 1 */ [ "port", "A", 1 ], + /* 2 */ [ "and", 0, 1 ], + /* 3 */ [ "port", "A", 2 ], + /* 4 */ [ "and", 2, 3, "Y", 0 ], + /* 5 */ [ "false", "Y", 1, "Y", 2 ] + ] + +Future version of Yosys might add support for additional fields in the JSON +format. A program processing this format must ignore all unknown fields. +\end{lstlisting} + \section{write\_smt2 -- write design to SMT-LIBv2 file} \label{cmd:write_smt2} \begin{lstlisting}[numbers=left,frame=single] write_smt2 [options] [filename] Write a SMT-LIBv2 [1] description of the current design. For a module with name -'<mod>' this will declare the sort '<mod>_s' (state of the module) and the the -function '<mod>_t' (state transition function). +'<mod>' this will declare the sort '<mod>_s' (state of the module) and the +functions operating on that state. The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions are provided that can be used to access the values of the signals in the module. @@ -2922,11 +3839,37 @@ multi-bit wires are exported as single functions of type BitVec. The '<mod>_t' function evaluates to 'true' when the given pair of states describes a valid state transition. +The '<mod>_a' function evaluates to 'true' when the given state satisfies +the asserts in the module. + +The '<mod>_u' function evaluates to 'true' when the given state satisfies +the assumptions in the module. + +The '<mod>_i' function evaluates to 'true' when the given state conforms +to the initial state. + + -verbose + this will print the recursive walk used to export the modules. + -bv enable support for BitVec (FixedSizeBitVectors theory). with this option set multi-bit wires are represented using the BitVec sort and support for coarse grain cells (incl. arithmetic) is enabled. + -mem + enable support for memories (via ArraysEx theory). this option + also implies -bv. only $mem cells without merged registers in + read ports are supported. call "memory" with -nordff to make sure + that no registers are merged into $mem read ports. '<mod>_m' functions + will be generated for accessing the arrays that are used to represent + memories. + + -regs + also create '<mod>_n' functions for all registers. + + -wires + also create '<mod>_n' functions for all public wires. + -tpl <template_file> use the given template file. the line containing only the token '%%' is replaced with the regular output of this command. @@ -2973,13 +3916,30 @@ For this proof we create the following template (test.tpl). The following yosys script will create a 'test.smt2' file for our proof: read_verilog test.v - hierarchy; proc; techmap; opt -fast + hierarchy -check; proc; opt; check -assert write_smt2 -bv -tpl test.tpl test.smt2 Running 'cvc4 test.smt2' will print 'unsat' because y can never transition from non-zero to zero in the test design. \end{lstlisting} +\section{write\_smv -- write design to SMV file} +\label{cmd:write_smv} +\begin{lstlisting}[numbers=left,frame=single] + write_smv [options] [filename] + +Write an SMV description of the current design. + + -verbose + this will print the recursive walk used to export the modules. + + -tpl <template_file> + use the given template file. the line containing only the token '%%' + is replaced with the regular output of this command. + +THIS COMMAND IS UNDER CONSTRUCTION +\end{lstlisting} + \section{write\_spice -- write design to SPICE netlist file} \label{cmd:write_spice} \begin{lstlisting}[numbers=left,frame=single] @@ -2988,7 +3948,7 @@ from non-zero to zero in the test design. Write the current design to an SPICE netlist file. -big_endian - generate multi-bit ports in MSB first order + generate multi-bit ports in MSB first order (default is LSB first) -neg net_name @@ -3004,12 +3964,12 @@ Write the current design to an SPICE netlist file. set the specified module as design top module \end{lstlisting} -\section{write\_verilog -- write design to verilog file} +\section{write\_verilog -- write design to Verilog file} \label{cmd:write_verilog} \begin{lstlisting}[numbers=left,frame=single] write_verilog [options] [filename] -Write the current design to a verilog file. +Write the current design to a Verilog file. -norename without this option all internal object names (the ones with a dollar @@ -3023,7 +3983,7 @@ Write the current design to a verilog file. with this option attributes are included as comments in the output -noexpr - without this option all internal cells are converted to verilog + without this option all internal cells are converted to Verilog expressions. -blackboxes diff --git a/manual/literature.bib b/manual/literature.bib index 91bc1f382..372e882ac 100644 --- a/manual/literature.bib +++ b/manual/literature.bib @@ -1,163 +1,163 @@ -
-@inproceedings{intersynth,
- title={Example-driven interconnect synthesis for heterogeneous coarse-grain reconfigurable logic},
- author={Clifford Wolf and Johann Glaser and Florian Schupfer and Jan Haase and Christoph Grimm},
- booktitle={FDL Proceeding of the 2012 Forum on Specification and Design Languages},
- pages={194--201},
- year={2012}
-}
-
-@incollection{intersynthFdlBookChapter,
- title={Methodology and Example-Driven Interconnect Synthesis for Designing Heterogeneous Coarse-Grain Reconfigurable Architectures},
- author={Johann Glaser and Clifford Wolf},
- booktitle={Advances in Models, Methods, and Tools for Complex Chip Design --- Selected contributions from FDL'12},
- editor={Jan Haase},
- publisher={Springer},
- year={2013},
- note={to appear}
-}
-
-@unpublished{BACC,
- author = {Clifford Wolf},
- title = {Design and Implementation of the Yosys Open SYnthesis Suite},
- note = {Bachelor Thesis, Vienna University of Technology},
- year = {2013}
-}
-
-@unpublished{VerilogFossEval,
- author = {Clifford Wolf},
- title = {Evaluation of Open Source Verilog Synthesis Tools for Feature-Completeness and Extensibility},
- note = {Unpublished Student Research Paper, Vienna University of Technology},
- year = {2012}
-}
-
-@article{ABEL,
- title={A High-Level Design Language for Programmable Logic Devices},
- author={Kyu Y. Lee and Michael Holley and Mary Bailey and Walter Bright},
- journal={VLSI Design (Manhasset NY: CPM Publications)},
- year={June 1985},
- pages={50-62}
-}
-
-@MISC{Cheng93vl2mv:a,
- author = {S-T Cheng and G York and R K Brayton},
- title = {VL2MV: A Compiler from Verilog to BLIF-MV},
- year = {1993}
-}
-
-@MISC{Odin,
- author = {Peter Jamieson and Jonathan Rose},
- title = {A VERILOG RTL SYNTHESIS TOOL FOR HETEROGENEOUS FPGAS},
- year = {2005}
-}
-
-@inproceedings{vtr2012,
- title={The VTR Project: Architecture and CAD for FPGAs from Verilog to Routing},
- author={Jonathan Rose and Jason Luu and Chi Wai Yu and Opal Densmore and Jeff Goeders and Andrew Somerville and Kenneth B. Kent and Peter Jamieson and Jason Anderson},
- booktitle={Proceedings of the 20th ACM/SIGDA International Symposium on Field-Programmable Gate Arrays},
- pages={77--86},
- year={2012},
- organization={ACM}
-}
-
-@MISC{LogicSynthesis,
- author = {G D Hachtel and F Somenzi},
- title = {Logic Synthesis and Verification Algorithms},
- year = {1996}
-}
-
-@ARTICLE{Verilog2005,
- journal={IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001)},
- title={IEEE Standard for Verilog Hardware Description Language},
- year={2006},
- doi={10.1109/IEEESTD.2006.99495}
-}
-
-@ARTICLE{VerilogSynth,
- journal={IEEE Std 1364.1-2002},
- title={IEEE Standard for Verilog Register Transfer Level Synthesis},
- year={2002},
- doi={10.1109/IEEESTD.2002.94220}
-}
-
-@ARTICLE{VHDL,
- journal={IEEE Std 1076-2008 (Revision of IEEE Std 1076-2002)}, title={IEEE Standard VHDL Language Reference Manual},
- year={2009},
- month={26},
- doi={10.1109/IEEESTD.2009.4772740}
-}
-
-@ARTICLE{VHDLSynth,
- journal={IEEE Std 1076.6-2004 (Revision of IEEE Std 1076.6-1999)}, title={IEEE Standard for VHDL Register Transfer Level (RTL) Synthesis},
- year={2004},
- doi={10.1109/IEEESTD.2004.94802}
-}
-
-@ARTICLE{IP-XACT,
-journal={IEEE Std 1685-2009}, title={IEEE Standard for IP-XACT, Standard Structure for Packaging, Integrating, and Reusing IP within Tools Flows},
-year={2010},
-pages={C1-360},
-keywords={abstraction definitions, address space specification, bus definitions, design environment, EDA, electronic design automation, electronic system level, ESL, implementation constraints, IP-XACT, register transfer level, RTL, SCRs, semantic consistency rules, TGI, tight generator interface, tool and data interoperability, use models, XML design meta-data, XML schema},
-doi={10.1109/IEEESTD.2010.5417309},}
-
-@book{Dragonbook,
-author = {Aho, Alfred V. and Sethi, Ravi and Ullman, Jeffrey D.},
-title = {Compilers: principles, techniques, and tools},
-year = {1986},
-isbn = {0-201-10088-6},
-publisher = {Addison-Wesley Longman Publishing Co., Inc.},
-address = {Boston, MA, USA},
-}
-
-@INPROCEEDINGS{Cummings00,
-author = {Clifford E. Cummings and Sunburst Design Inc},
-title = {Nonblocking Assignments in Verilog Synthesis, Coding Styles That Kill},
-booktitle = {SNUG (Synopsys Users Group) 2000 User Papers, section-MC1 (1 st paper},
-year = {2000}
-}
-
-@ARTICLE{MURPHY,
- author={D. L. Klipstein},
- journal={Cahners Publishing Co., EEE Magazine, Vol. 15, No. 8},
- title={The Contributions of Edsel Murphy to the Understanding of the Behavior of Inanimate Objects},
- year={August 1967}
-}
-
-@INPROCEEDINGS{fsmextract,
-author={Yiqiong Shi and Chan Wai Ting and Bah-Hwee Gwee and Ye Ren},
-booktitle={Circuits and Systems (ISCAS), Proceedings of 2010 IEEE International Symposium on},
-title={A highly efficient method for extracting FSMs from flattened gate-level netlist},
-year={2010},
-pages={2610-2613},
-keywords={circuit CAD;finite state machines;microcontrollers;FSM;control-intensive circuits;finite state machines;flattened gate-level netlist;state register elimination technique;Automata;Circuit synthesis;Continuous wavelet transforms;Design automation;Digital circuits;Hardware design languages;Logic;Microcontrollers;Registers;Signal processing},
-doi={10.1109/ISCAS.2010.5537093},}
-
-@ARTICLE{MultiLevelLogicSynth,
-author={Brayton, R.K. and Hachtel, G.D. and Sangiovanni-Vincentelli, A.L.},
-journal={Proceedings of the IEEE},
-title={Multilevel logic synthesis},
-year={1990},
-volume={78},
-number={2},
-pages={264-300},
-keywords={circuit layout CAD;integrated logic circuits;logic CAD;capsule summaries;definitions;detailed analysis;in-depth background;logic decomposition;logic minimisation;logic synthesis;logic synthesis techniques;multilevel combinational logic;multilevel logic synthesis;notation;perspective;survey;synthesis methods;technology mapping;testing;Application specific integrated circuits;Design automation;Integrated circuit synthesis;Logic design;Logic devices;Logic testing;Network synthesis;Programmable logic arrays;Signal synthesis;Silicon},
-doi={10.1109/5.52213},
-ISSN={0018-9219},}
-
-@article{UllmannSubgraphIsomorphism,
- author = {Ullmann, J. R.},
- title = {An Algorithm for Subgraph Isomorphism},
- journal = {J. ACM},
- issue_date = {Jan. 1976},
- volume = {23},
- number = {1},
- month = jan,
- year = {1976},
- issn = {0004-5411},
- pages = {31--42},
- numpages = {12},
- doi = {10.1145/321921.321925},
- acmid = {321925},
- publisher = {ACM},
- address = {New York, NY, USA},
-}
+ +@inproceedings{intersynth, + title={Example-driven interconnect synthesis for heterogeneous coarse-grain reconfigurable logic}, + author={Clifford Wolf and Johann Glaser and Florian Schupfer and Jan Haase and Christoph Grimm}, + booktitle={FDL Proceeding of the 2012 Forum on Specification and Design Languages}, + pages={194--201}, + year={2012} +} + +@incollection{intersynthFdlBookChapter, + title={Methodology and Example-Driven Interconnect Synthesis for Designing Heterogeneous Coarse-Grain Reconfigurable Architectures}, + author={Johann Glaser and Clifford Wolf}, + booktitle={Advances in Models, Methods, and Tools for Complex Chip Design --- Selected contributions from FDL'12}, + editor={Jan Haase}, + publisher={Springer}, + year={2013}, + note={to appear} +} + +@unpublished{BACC, + author = {Clifford Wolf}, + title = {Design and Implementation of the Yosys Open SYnthesis Suite}, + note = {Bachelor Thesis, Vienna University of Technology}, + year = {2013} +} + +@unpublished{VerilogFossEval, + author = {Clifford Wolf}, + title = {Evaluation of Open Source Verilog Synthesis Tools for Feature-Completeness and Extensibility}, + note = {Unpublished Student Research Paper, Vienna University of Technology}, + year = {2012} +} + +@article{ABEL, + title={A High-Level Design Language for Programmable Logic Devices}, + author={Kyu Y. Lee and Michael Holley and Mary Bailey and Walter Bright}, + journal={VLSI Design (Manhasset NY: CPM Publications)}, + year={June 1985}, + pages={50-62} +} + +@MISC{Cheng93vl2mv:a, + author = {S-T Cheng and G York and R K Brayton}, + title = {VL2MV: A Compiler from Verilog to BLIF-MV}, + year = {1993} +} + +@MISC{Odin, + author = {Peter Jamieson and Jonathan Rose}, + title = {A VERILOG RTL SYNTHESIS TOOL FOR HETEROGENEOUS FPGAS}, + year = {2005} +} + +@inproceedings{vtr2012, + title={The VTR Project: Architecture and CAD for FPGAs from Verilog to Routing}, + author={Jonathan Rose and Jason Luu and Chi Wai Yu and Opal Densmore and Jeff Goeders and Andrew Somerville and Kenneth B. Kent and Peter Jamieson and Jason Anderson}, + booktitle={Proceedings of the 20th ACM/SIGDA International Symposium on Field-Programmable Gate Arrays}, + pages={77--86}, + year={2012}, + organization={ACM} +} + +@MISC{LogicSynthesis, + author = {G D Hachtel and F Somenzi}, + title = {Logic Synthesis and Verification Algorithms}, + year = {1996} +} + +@ARTICLE{Verilog2005, + journal={IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001)}, + title={IEEE Standard for Verilog Hardware Description Language}, + year={2006}, + doi={10.1109/IEEESTD.2006.99495} +} + +@ARTICLE{VerilogSynth, + journal={IEEE Std 1364.1-2002}, + title={IEEE Standard for Verilog Register Transfer Level Synthesis}, + year={2002}, + doi={10.1109/IEEESTD.2002.94220} +} + +@ARTICLE{VHDL, + journal={IEEE Std 1076-2008 (Revision of IEEE Std 1076-2002)}, title={IEEE Standard VHDL Language Reference Manual}, + year={2009}, + month={26}, + doi={10.1109/IEEESTD.2009.4772740} +} + +@ARTICLE{VHDLSynth, + journal={IEEE Std 1076.6-2004 (Revision of IEEE Std 1076.6-1999)}, title={IEEE Standard for VHDL Register Transfer Level (RTL) Synthesis}, + year={2004}, + doi={10.1109/IEEESTD.2004.94802} +} + +@ARTICLE{IP-XACT, +journal={IEEE Std 1685-2009}, title={IEEE Standard for IP-XACT, Standard Structure for Packaging, Integrating, and Reusing IP within Tools Flows}, +year={2010}, +pages={C1-360}, +keywords={abstraction definitions, address space specification, bus definitions, design environment, EDA, electronic design automation, electronic system level, ESL, implementation constraints, IP-XACT, register transfer level, RTL, SCRs, semantic consistency rules, TGI, tight generator interface, tool and data interoperability, use models, XML design meta-data, XML schema}, +doi={10.1109/IEEESTD.2010.5417309},} + +@book{Dragonbook, +author = {Aho, Alfred V. and Sethi, Ravi and Ullman, Jeffrey D.}, +title = {Compilers: principles, techniques, and tools}, +year = {1986}, +isbn = {0-201-10088-6}, +publisher = {Addison-Wesley Longman Publishing Co., Inc.}, +address = {Boston, MA, USA}, +} + +@INPROCEEDINGS{Cummings00, +author = {Clifford E. Cummings and Sunburst Design Inc}, +title = {Nonblocking Assignments in Verilog Synthesis, Coding Styles That Kill}, +booktitle = {SNUG (Synopsys Users Group) 2000 User Papers, section-MC1 (1 st paper}, +year = {2000} +} + +@ARTICLE{MURPHY, + author={D. L. Klipstein}, + journal={Cahners Publishing Co., EEE Magazine, Vol. 15, No. 8}, + title={The Contributions of Edsel Murphy to the Understanding of the Behavior of Inanimate Objects}, + year={August 1967} +} + +@INPROCEEDINGS{fsmextract, +author={Yiqiong Shi and Chan Wai Ting and Bah-Hwee Gwee and Ye Ren}, +booktitle={Circuits and Systems (ISCAS), Proceedings of 2010 IEEE International Symposium on}, +title={A highly efficient method for extracting FSMs from flattened gate-level netlist}, +year={2010}, +pages={2610-2613}, +keywords={circuit CAD;finite state machines;microcontrollers;FSM;control-intensive circuits;finite state machines;flattened gate-level netlist;state register elimination technique;Automata;Circuit synthesis;Continuous wavelet transforms;Design automation;Digital circuits;Hardware design languages;Logic;Microcontrollers;Registers;Signal processing}, +doi={10.1109/ISCAS.2010.5537093},} + +@ARTICLE{MultiLevelLogicSynth, +author={Brayton, R.K. and Hachtel, G.D. and Sangiovanni-Vincentelli, A.L.}, +journal={Proceedings of the IEEE}, +title={Multilevel logic synthesis}, +year={1990}, +volume={78}, +number={2}, +pages={264-300}, +keywords={circuit layout CAD;integrated logic circuits;logic CAD;capsule summaries;definitions;detailed analysis;in-depth background;logic decomposition;logic minimisation;logic synthesis;logic synthesis techniques;multilevel combinational logic;multilevel logic synthesis;notation;perspective;survey;synthesis methods;technology mapping;testing;Application specific integrated circuits;Design automation;Integrated circuit synthesis;Logic design;Logic devices;Logic testing;Network synthesis;Programmable logic arrays;Signal synthesis;Silicon}, +doi={10.1109/5.52213}, +ISSN={0018-9219},} + +@article{UllmannSubgraphIsomorphism, + author = {Ullmann, J. R.}, + title = {An Algorithm for Subgraph Isomorphism}, + journal = {J. ACM}, + issue_date = {Jan. 1976}, + volume = {23}, + number = {1}, + month = jan, + year = {1976}, + issn = {0004-5411}, + pages = {31--42}, + numpages = {12}, + doi = {10.1145/321921.321925}, + acmid = {321925}, + publisher = {ACM}, + address = {New York, NY, USA}, +} diff --git a/manual/manual.tex b/manual/manual.tex index 84be86e5b..67982cbc8 100644 --- a/manual/manual.tex +++ b/manual/manual.tex @@ -17,7 +17,7 @@ % (i.e. run "sudo su" and then execute the commands in the root % shell, don't just prefix the commands with "sudo"). -% formats the text accourding the set language +% formats the text according the set language \usepackage[english]{babel} \usepackage[table,usenames]{xcolor} % generates indices with the "\index" command @@ -151,14 +151,14 @@ availability of a Free and Open Source (FOSS) synthesis tool that can be used as basis for custom tools would be helpful. In the absence of such a tool, the Yosys Open SYnthesis Suite (Yosys) was -developped. This document covers the design and implementation of this tool. +developed. This document covers the design and implementation of this tool. At the moment the main focus of Yosys lies on the high-level aspects of digital synthesis. The pre-existing FOSS logic-synthesis tool ABC is used by Yosys to perform advanced gate-level optimizations. An evaluation of Yosys based on real-world designs is included. It is shown that Yosys can be used as-is to synthesize such designs. The results produced -by Yosys in this tests where successflly verified using formal verification +by Yosys in this tests where successfully verified using formal verification and are comparable in quality to the results produced by a commercial synthesis tool. @@ -172,7 +172,7 @@ University of Technology \cite{BACC}. AIG & And-Inverter-Graph \\ ASIC & Application-Specific Integrated Circuit \\ AST & Abstract Syntax Tree \\ -BDD & Binary Decicion Diagram \\ +BDD & Binary Decision Diagram \\ BLIF & Berkeley Logic Interchange Format \\ EDA & Electronic Design Automation \\ EDIF & Electronic Design Interchange Format \\ diff --git a/manual/presentation.tex b/manual/presentation.tex index dc5127755..63b963bbd 100644 --- a/manual/presentation.tex +++ b/manual/presentation.tex @@ -18,7 +18,7 @@ % (i.e. run "sudo su" and then execute the commands in the root % shell, don't just prefix the commands with "sudo"). -% formats the text accourding the set language +% formats the text according the set language \usepackage[english]{babel} \usepackage{amsmath} \usepackage{multirow} @@ -118,7 +118,7 @@ hobbyists, educators and engineers alike. \bigskip This presentation covers basic concepts of Yosys, writing synthesis scripts for a wide range of applications, creating Yosys scripts for various -non-synthesis applications (such as formal equivialence checking) and +non-synthesis applications (such as formal equivalence checking) and writing extensions to Yosys using the C++ API. \end{frame} diff --git a/manual/weblinks.bib b/manual/weblinks.bib index 5215a6ca3..d5f83315d 100644 --- a/manual/weblinks.bib +++ b/manual/weblinks.bib @@ -1,134 +1,134 @@ -
-@misc{YosysGit,
- author = {Clifford Wolf},
- title = {{Yosys Open SYnthesis Suite (YOSYS)}},
- note = {\url{http://github.com/cliffordwolf/yosys}}
-}
-
-@misc{YosysTestsGit,
- author = {Clifford Wolf},
- title = {{Yosys Test Bench}},
- note = {\url{http://github.com/cliffordwolf/yosys-tests}}
-}
-
-@misc{VlogHammer,
- author = {Clifford Wolf},
- title = {{VlogHammer Verilog Synthesis Regression Tests}},
- note = {\url{http://github.com/cliffordwolf/VlogHammer}}
-}
-
-@misc{Icarus,
- author = {Stephen Williams},
- title = {{Icarus Verilog}},
- note = {Version 0.8.7, \url{http://iverilog.icarus.com/}}
-}
-
-@misc{VTR,
- author= {Jonathan Rose and Jason Luu and Chi Wai Yu and Opal Densmore and Jeff Goeders and Andrew Somerville and Kenneth B. Kent and Peter Jamieson and Jason Anderson},
- title = {{The Verilog-to-Routing (VTR) Project for FPGAs}},
- note = {Version 1.0, \url{https://code.google.com/p/vtr-verilog-to-routing/}}
-}
-
-@misc{HANA,
- author = {Parvez Ahmad},
- title = {{HDL Analyzer and Netlist Architect (HANA)}},
- note = {Verison linux64-1.0-alpha (2012-10-14), \url{http://sourceforge.net/projects/sim-sim/}}
-}
-
-@misc{MVSIS,
- author = {MVSIS group at Berkeley studies logic synthesis and verification for VLSI design},
- title = {{MVSIS: Logic Synthesis and Verification}},
- note = {Version 3.0, \url{http://embedded.eecs.berkeley.edu/mvsis/}}
-}
-
-@misc{VIS,
- author = {{The VIS group}},
- title = {{VIS: A system for Verification and Synthesis}},
- note = {Version 2.4, \url{http://vlsi.colorado.edu/~vis/}}
-}
-
-@misc{ABC,
- author = {{Berkeley Logic Synthesis and Verification Group}},
- title = {{ABC: A System for Sequential Synthesis and Verification}},
- note = {HQ Rev b5750272659f, 2012-10-28, \url{http://www.eecs.berkeley.edu/~alanmi/abc/}}
-}
-
-@misc{AIGER,
- author = {{Armin Biere, Johannes Kepler University Linz, Austria}},
- title = {{AIGER}},
- note = {\url{http://fmv.jku.at/aiger/}}
-}
-
-@misc{XilinxWebPACK,
- author = {{Xilinx, Inc.}},
- title = {{ISE WebPACK Design Software}},
- note = {\url{http://www.xilinx.com/products/design-tools/ise-design-suite/ise-webpack.htm}}
-}
-
-@misc{QuartusWeb,
- author = {{Altera, Inc.}},
- title = {{Quartus II Web Edition Software}},
- note = {\url{http://www.altera.com/products/software/quartus-ii/web-edition/qts-we-index.html}}
-}
-
-@misc{OR1200,
- title = {{OpenRISC 1200 CPU}},
- note = {\url{http://opencores.org/or1k/OR1200\_OpenRISC\_Processor}}
-}
-
-@misc{openMSP430,
- title = {{openMSP430 CPU}},
- note = {\url{http://opencores.org/project,openmsp430}}
-}
-
-@misc{i2cmaster,
- title = {{OpenCores I$^2$C Core}},
- note = {\url{http://opencores.org/project,i2c}}
-}
-
-@misc{k68,
- title = {{OpenCores k68 Core}},
- note = {\url{http://opencores.org/project,k68}}
-}
-
-@misc{bison,
- title = {{GNU Bison}},
- note = {\url{http://www.gnu.org/software/bison/}}
-}
-
-@misc{flex,
- title = {{Flex}},
- note = {\url{http://flex.sourceforge.net/}}
-}
-
-@misc{C_to_Verilog,
- title = {{C-to-Verilog}},
- note = {\url{http://www.c-to-verilog.com/}}
-}
-
-@misc{LegUp,
- title = {{LegUp}},
- note = {\url{http://legup.eecg.utoronto.ca/}}
-}
-
-@misc{LibertyFormat,
- title = {{The Liberty Library Modeling Standard}},
- note = {\url{http://www.opensourceliberty.org/}}
-}
-
-@misc{ASIC-WORLD,
- title = {{World of ASIC}},
- note = {\url{http://www.asic-world.com/}}
-}
-
-@misc{Formality,
- title = {{Synopsys Formality Equivalence Checking}},
- note = {\url{http://www.synopsys.com/Tools/Verification/FormalEquivalence/Pages/Formality.aspx}},
-}
-
-@misc{bigint,
- author = {Matt McCutchen},
- title = {{C++ Big Integer Library}},
- note = {\url{http://mattmccutchen.net/bigint/}}
-}
-
+ +@misc{YosysGit, + author = {Clifford Wolf}, + title = {{Yosys Open SYnthesis Suite (YOSYS)}}, + note = {\url{http://github.com/cliffordwolf/yosys}} +} + +@misc{YosysTestsGit, + author = {Clifford Wolf}, + title = {{Yosys Test Bench}}, + note = {\url{http://github.com/cliffordwolf/yosys-tests}} +} + +@misc{VlogHammer, + author = {Clifford Wolf}, + title = {{VlogHammer Verilog Synthesis Regression Tests}}, + note = {\url{http://github.com/cliffordwolf/VlogHammer}} +} + +@misc{Icarus, + author = {Stephen Williams}, + title = {{Icarus Verilog}}, + note = {Version 0.8.7, \url{http://iverilog.icarus.com/}} +} + +@misc{VTR, + author= {Jonathan Rose and Jason Luu and Chi Wai Yu and Opal Densmore and Jeff Goeders and Andrew Somerville and Kenneth B. Kent and Peter Jamieson and Jason Anderson}, + title = {{The Verilog-to-Routing (VTR) Project for FPGAs}}, + note = {Version 1.0, \url{https://code.google.com/p/vtr-verilog-to-routing/}} +} + +@misc{HANA, + author = {Parvez Ahmad}, + title = {{HDL Analyzer and Netlist Architect (HANA)}}, + note = {Verison linux64-1.0-alpha (2012-10-14), \url{http://sourceforge.net/projects/sim-sim/}} +} + +@misc{MVSIS, + author = {MVSIS group at Berkeley studies logic synthesis and verification for VLSI design}, + title = {{MVSIS: Logic Synthesis and Verification}}, + note = {Version 3.0, \url{http://embedded.eecs.berkeley.edu/mvsis/}} +} + +@misc{VIS, + author = {{The VIS group}}, + title = {{VIS: A system for Verification and Synthesis}}, + note = {Version 2.4, \url{http://vlsi.colorado.edu/~vis/}} +} + +@misc{ABC, + author = {{Berkeley Logic Synthesis and Verification Group}}, + title = {{ABC: A System for Sequential Synthesis and Verification}}, + note = {HQ Rev b5750272659f, 2012-10-28, \url{http://www.eecs.berkeley.edu/~alanmi/abc/}} +} + +@misc{AIGER, + author = {{Armin Biere, Johannes Kepler University Linz, Austria}}, + title = {{AIGER}}, + note = {\url{http://fmv.jku.at/aiger/}} +} + +@misc{XilinxWebPACK, + author = {{Xilinx, Inc.}}, + title = {{ISE WebPACK Design Software}}, + note = {\url{http://www.xilinx.com/products/design-tools/ise-design-suite/ise-webpack.htm}} +} + +@misc{QuartusWeb, + author = {{Altera, Inc.}}, + title = {{Quartus II Web Edition Software}}, + note = {\url{http://www.altera.com/products/software/quartus-ii/web-edition/qts-we-index.html}} +} + +@misc{OR1200, + title = {{OpenRISC 1200 CPU}}, + note = {\url{http://opencores.org/or1k/OR1200\_OpenRISC\_Processor}} +} + +@misc{openMSP430, + title = {{openMSP430 CPU}}, + note = {\url{http://opencores.org/project,openmsp430}} +} + +@misc{i2cmaster, + title = {{OpenCores I$^2$C Core}}, + note = {\url{http://opencores.org/project,i2c}} +} + +@misc{k68, + title = {{OpenCores k68 Core}}, + note = {\url{http://opencores.org/project,k68}} +} + +@misc{bison, + title = {{GNU Bison}}, + note = {\url{http://www.gnu.org/software/bison/}} +} + +@misc{flex, + title = {{Flex}}, + note = {\url{http://flex.sourceforge.net/}} +} + +@misc{C_to_Verilog, + title = {{C-to-Verilog}}, + note = {\url{http://www.c-to-verilog.com/}} +} + +@misc{LegUp, + title = {{LegUp}}, + note = {\url{http://legup.eecg.utoronto.ca/}} +} + +@misc{LibertyFormat, + title = {{The Liberty Library Modeling Standard}}, + note = {\url{http://www.opensourceliberty.org/}} +} + +@misc{ASIC-WORLD, + title = {{World of ASIC}}, + note = {\url{http://www.asic-world.com/}} +} + +@misc{Formality, + title = {{Synopsys Formality Equivalence Checking}}, + note = {\url{http://www.synopsys.com/Tools/Verification/FormalEquivalence/Pages/Formality.aspx}}, +} + +@misc{bigint, + author = {Matt McCutchen}, + title = {{C++ Big Integer Library}}, + note = {\url{http://mattmccutchen.net/bigint/}} +} + |