diff options
Diffstat (limited to 'manual')
| -rw-r--r-- | manual/APPNOTE_012_Verilog_to_BTOR.tex | 4 | ||||
| -rw-r--r-- | manual/CHAPTER_CellLib.tex | 6 | ||||
| -rw-r--r-- | manual/CHAPTER_Optimize.tex | 26 | ||||
| -rw-r--r-- | manual/CHAPTER_Overview.tex | 6 | ||||
| -rw-r--r-- | manual/CHAPTER_Prog/stubnets.cc | 2 | ||||
| -rw-r--r-- | manual/PRESENTATION_ExSyn.tex | 10 | ||||
| -rw-r--r-- | manual/PRESENTATION_Prog.tex | 4 | ||||
| -rw-r--r-- | manual/PRESENTATION_Prog/my_cmd.cc | 2 | ||||
| -rw-r--r-- | manual/command-reference-manual.tex | 6 | ||||
| -rw-r--r-- | manual/manual.tex | 6 |
10 files changed, 40 insertions, 32 deletions
diff --git a/manual/APPNOTE_012_Verilog_to_BTOR.tex b/manual/APPNOTE_012_Verilog_to_BTOR.tex index 245a6b0b..1bc27787 100644 --- a/manual/APPNOTE_012_Verilog_to_BTOR.tex +++ b/manual/APPNOTE_012_Verilog_to_BTOR.tex @@ -208,7 +208,7 @@ read_verilog -sv $1; hierarchy -top $3; hierarchy -libdir $DIR; hierarchy -check; proc; opt; -opt_const -mux_undef; opt; +opt_expr -mux_undef; opt; rename -hide;;; splice; opt; memory_dff -wr_only; memory_collect;; @@ -263,7 +263,7 @@ read_verilog -sv $1; hierarchy -top $3; hierarchy -libdir $DIR; hierarchy -check; proc; opt; -opt_const -mux_undef; opt; +opt_expr -mux_undef; opt; rename -hide;;; splice; opt; memory;; diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index c648eb1f..bd73ae23 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -421,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}, {\tt \$assume}, and {\tt \$equiv} cells. +Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$equiv}, {\tt \$initstate}, and {\tt \$anyconst} cells. \end{fixme} \begin{fixme} @@ -429,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_Optimize.tex b/manual/CHAPTER_Optimize.tex index d09b3c47..eee92ef5 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. @@ -76,10 +76,10 @@ 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. @@ -222,6 +222,10 @@ This heuristic has proven to work very well. It is possible to overwrite it by s and setting \B{fsm\_encoding}{\tt = "none"} on registers that match the above criteria but should not be considered FSM state registers. +Note however that marking state registers with \B{fsm\_encoding} that are not +suitable for FSM recoding can cause synthesis to fail or produce invalid +results. + \subsection{FSM Extraction} The {\tt fsm\_extract} pass operates on all state signals marked with the diff --git a/manual/CHAPTER_Overview.tex b/manual/CHAPTER_Overview.tex index 032c0f8c..964875d5 100644 --- a/manual/CHAPTER_Overview.tex +++ b/manual/CHAPTER_Overview.tex @@ -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 976107fb..eb77bd40 100644 --- a/manual/CHAPTER_Prog/stubnets.cc +++ b/manual/CHAPTER_Prog/stubnets.cc @@ -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/PRESENTATION_ExSyn.tex b/manual/PRESENTATION_ExSyn.tex index 1b56374d..655720eb 100644 --- a/manual/PRESENTATION_ExSyn.tex +++ b/manual/PRESENTATION_ExSyn.tex @@ -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} diff --git a/manual/PRESENTATION_Prog.tex b/manual/PRESENTATION_Prog.tex index 6b105a70..b85eda89 100644 --- a/manual/PRESENTATION_Prog.tex +++ b/manual/PRESENTATION_Prog.tex @@ -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 1d28ce97..d99bfe1e 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/command-reference-manual.tex b/manual/command-reference-manual.tex index 99d4a1fa..425d89b6 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -3783,10 +3783,10 @@ The following node-types may be used: - the inverted value of the specified input port bit [ "and", <node-index>, <node-index>, <out-list> ] - - the ANDed value of the speciefied nodes + - the ANDed value of the specified nodes [ "nand", <node-index>, <node-index>, <out-list> ] - - the inverted ANDed value of the speciefied nodes + - the inverted ANDed value of the specified nodes [ "true", <out-list> ] - the constant value 1 @@ -3817,7 +3817,7 @@ inferred by the following code: ] Future version of Yosys might add support for additional fields in the JSON -format. A program processing this format must ignore all unkown fields. +format. A program processing this format must ignore all unknown fields. \end{lstlisting} \section{write\_smt2 -- write design to SMT-LIBv2 file} diff --git a/manual/manual.tex b/manual/manual.tex index ecc7e4c9..67982cbc 100644 --- a/manual/manual.tex +++ b/manual/manual.tex @@ -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 \\ |