diff options
| author | Ahmed Irfan <irfan@levert.(none)> | 2015-04-03 16:38:07 +0200 |
|---|---|---|
| committer | Ahmed Irfan <irfan@levert.(none)> | 2015-04-03 16:38:07 +0200 |
| commit | bdf6b2b19ab2206f5957ad5b2ec582c2730d45ee (patch) | |
| tree | 1d02541701054a1c3b1cdb66478d0cbc31c2d38f /manual | |
| parent | 8acdd90bc918b780ad45cdac42b3baf84d2cc476 (diff) | |
| parent | 4b4490761949e738dee54bdfc52e080e0a5c9067 (diff) | |
Merge branch 'master' of https://github.com/cliffordwolf/yosys
Diffstat (limited to 'manual')
37 files changed, 1757 insertions, 194 deletions
diff --git a/manual/APPNOTE_010_Verilog_to_BLIF.tex b/manual/APPNOTE_010_Verilog_to_BLIF.tex index 9ee87bc4..0f521fb0 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. @@ -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/cmos_00.dot b/manual/APPNOTE_011_Design_Investigation/cmos_00.dot index 85ca7849..49c63008 100644 --- a/manual/APPNOTE_011_Design_Investigation/cmos_00.dot +++ b/manual/APPNOTE_011_Design_Investigation/cmos_00.dot @@ -31,4 +31,4 @@ n5:e -> c11:p7:w [color="black", label=""]; n6:e -> x0:s0:w [color="black", label=""]; n6:e -> x1:s0:w [color="black", label=""]; n6:e -> x2:s0:w [color="black", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/cmos_01.dot b/manual/APPNOTE_011_Design_Investigation/cmos_01.dot index de9af170..ea6f4403 100644 --- a/manual/APPNOTE_011_Design_Investigation/cmos_01.dot +++ b/manual/APPNOTE_011_Design_Investigation/cmos_01.dot @@ -20,4 +20,4 @@ n5:e -> c12:p8:w [color="black", label=""]; c15:p10:e -> n6:w [color="black", label=""]; c14:p10:e -> n7:w [color="black", label=""]; n7:e -> c15:p9:w [color="black", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/example_00.dot b/manual/APPNOTE_011_Design_Investigation/example_00.dot index b38862c4..1e23ed0e 100644 --- a/manual/APPNOTE_011_Design_Investigation/example_00.dot +++ b/manual/APPNOTE_011_Design_Investigation/example_00.dot @@ -20,4 +20,4 @@ n7:e -> p1:w [color="black", label=""]; p1:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; n8:e -> p1:w [color="black", style="setlinewidth(3)", label=""]; v0:e -> c14:p9:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/example_01.dot b/manual/APPNOTE_011_Design_Investigation/example_01.dot index e2e3f02d..e89292b5 100644 --- a/manual/APPNOTE_011_Design_Investigation/example_01.dot +++ b/manual/APPNOTE_011_Design_Investigation/example_01.dot @@ -30,4 +30,4 @@ n8:e -> c21:p19:w [color="black", label=""]; n8:e -> x1:w:w [color="black", label=""]; n9:e -> c18:p15:w [color="black", label=""]; v0:e -> c21:p11:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/example_02.dot b/manual/APPNOTE_011_Design_Investigation/example_02.dot index 4b57f89c..f950ed2e 100644 --- a/manual/APPNOTE_011_Design_Investigation/example_02.dot +++ b/manual/APPNOTE_011_Design_Investigation/example_02.dot @@ -17,4 +17,4 @@ n5:e -> c17:p16:w [color="black", label=""]; n6:e -> c15:p12:w [color="black", label=""]; c15:p14:e -> n7:w [color="black", style="setlinewidth(3)", label=""]; n7:e -> c17:p8:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/example_03.dot b/manual/APPNOTE_011_Design_Investigation/example_03.dot index 6c00c29a..e19d24af 100644 --- a/manual/APPNOTE_011_Design_Investigation/example_03.dot +++ b/manual/APPNOTE_011_Design_Investigation/example_03.dot @@ -8,4 +8,4 @@ c4 [ shape=record, label="{{<p1> A|<p2> B}|$2\n$add|{<p3> Y}}" ]; v0:e -> c4:p1:w [color="black", label=""]; v1:e -> c4:p2:w [color="black", label=""]; c4:p3:e -> v2:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/memdemo_00.dot b/manual/APPNOTE_011_Design_Investigation/memdemo_00.dot index 9e81edbc..0336a9aa 100644 --- a/manual/APPNOTE_011_Design_Investigation/memdemo_00.dot +++ b/manual/APPNOTE_011_Design_Investigation/memdemo_00.dot @@ -135,4 +135,4 @@ v6:e -> c47:p34:w [color="black", label=""]; v7:e -> c48:p33:w [color="black", style="setlinewidth(3)", label=""]; v8:e -> c49:p33:w [color="black", style="setlinewidth(3)", label=""]; v9:e -> c50:p33:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/memdemo_01.dot b/manual/APPNOTE_011_Design_Investigation/memdemo_01.dot index bbd7fcc6..2ad92c78 100644 --- a/manual/APPNOTE_011_Design_Investigation/memdemo_01.dot +++ b/manual/APPNOTE_011_Design_Investigation/memdemo_01.dot @@ -26,4 +26,4 @@ v0:e -> c13:p11:w [color="black", label=""]; v1:e -> c14:p11:w [color="black", label=""]; v2:e -> c15:p11:w [color="black", label=""]; v3:e -> c19:p16:w [color="black", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/splice.dot b/manual/APPNOTE_011_Design_Investigation/splice.dot index 1bcd55b4..4657feed 100644 --- a/manual/APPNOTE_011_Design_Investigation/splice.dot +++ b/manual/APPNOTE_011_Design_Investigation/splice.dot @@ -36,4 +36,4 @@ x1:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; x3:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; x3:s1:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; x6:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/submod_00.dot b/manual/APPNOTE_011_Design_Investigation/submod_00.dot index 4567dfb4..2e55268e 100644 --- a/manual/APPNOTE_011_Design_Investigation/submod_00.dot +++ b/manual/APPNOTE_011_Design_Investigation/submod_00.dot @@ -42,4 +42,4 @@ c21:p8:e -> n8:w [color="black", style="setlinewidth(3)", label=""]; n8:e -> c20:p8:w [color="black", style="setlinewidth(3)", label=""]; c21:p9:e -> n9:w [color="black", style="setlinewidth(3)", label=""]; n9:e -> c20:p9:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/submod_01.dot b/manual/APPNOTE_011_Design_Investigation/submod_01.dot index b1daae23..f8f8c008 100644 --- a/manual/APPNOTE_011_Design_Investigation/submod_01.dot +++ b/manual/APPNOTE_011_Design_Investigation/submod_01.dot @@ -84,4 +84,4 @@ v4:e -> c35:p24:w [color="black", style="setlinewidth(3)", label=""]; v5:e -> c36:p24:w [color="black", style="setlinewidth(3)", label=""]; v6:e -> c37:p24:w [color="black", style="setlinewidth(3)", label=""]; v7:e -> c38:p24:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/submod_02.dot b/manual/APPNOTE_011_Design_Investigation/submod_02.dot index 68266db9..1a672c48 100644 --- a/manual/APPNOTE_011_Design_Investigation/submod_02.dot +++ b/manual/APPNOTE_011_Design_Investigation/submod_02.dot @@ -30,4 +30,4 @@ n8:e -> c17:p12:w [color="black", style="setlinewidth(3)", label=""]; n9:e -> x0:s0:w [color="black", label=""]; n9:e -> x1:s0:w [color="black", label=""]; n9:e -> x2:s0:w [color="black", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/submod_03.dot b/manual/APPNOTE_011_Design_Investigation/submod_03.dot index 92ef5759..0dbbe3ba 100644 --- a/manual/APPNOTE_011_Design_Investigation/submod_03.dot +++ b/manual/APPNOTE_011_Design_Investigation/submod_03.dot @@ -23,4 +23,4 @@ x1:s1:e -> n5:w [color="black", style="setlinewidth(3)", label=""]; n6:e -> x2:s1:w [color="black", style="setlinewidth(3)", label=""]; n7:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""]; v0:e -> c13:p8:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_00.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_00.dot index 6f9b7d3d..06522dcc 100644 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_00.dot +++ b/manual/APPNOTE_011_Design_Investigation/sumprod_00.dot @@ -15,4 +15,4 @@ c4:p3:e -> v2:w [color="black", style="setlinewidth(3)", label=""]; v3:e -> c5:p1:w [color="black", style="setlinewidth(3)", label=""]; v4:e -> c5:p2:w [color="black", style="setlinewidth(3)", label=""]; c5:p3:e -> v5:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_01.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_01.dot index d0252270..aefe7a6d 100644 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_01.dot +++ b/manual/APPNOTE_011_Design_Investigation/sumprod_01.dot @@ -12,4 +12,4 @@ n2:e -> c9:p6:w [color="black", style="setlinewidth(3)", label=""]; n3:e -> c9:p7:w [color="black", style="setlinewidth(3)", label=""]; n4:e -> c10:p7:w [color="black", style="setlinewidth(3)", label=""]; c10:p8:e -> n5:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_02.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_02.dot index af87651b..4646c994 100644 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_02.dot +++ b/manual/APPNOTE_011_Design_Investigation/sumprod_02.dot @@ -2,4 +2,4 @@ digraph "sumprod" { rankdir="LR"; remincross=true; n1 [ shape=octagon, label="prod", color="black", fontcolor="black" ]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_03.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_03.dot index 21155135..dcfea2b5 100644 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_03.dot +++ b/manual/APPNOTE_011_Design_Investigation/sumprod_03.dot @@ -8,4 +8,4 @@ c5 [ shape=record, label="{{<p2> A|<p3> B}|$4\n$mul|{<p4> Y}}" ]; c5:p4:e -> n1:w [color="black", style="setlinewidth(3)", label=""]; v0:e -> c5:p2:w [color="black", style="setlinewidth(3)", label=""]; v1:e -> c5:p3:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_04.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_04.dot index 5223577e..e77c41aa 100644 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_04.dot +++ b/manual/APPNOTE_011_Design_Investigation/sumprod_04.dot @@ -8,4 +8,4 @@ n1 [ shape=diamond, label="$3_Y" ]; n1:e -> c7:p4:w [color="black", style="setlinewidth(3)", label=""]; n2:e -> c7:p5:w [color="black", style="setlinewidth(3)", label=""]; c7:p6:e -> n3:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/APPNOTE_011_Design_Investigation/sumprod_05.dot b/manual/APPNOTE_011_Design_Investigation/sumprod_05.dot index 45d00134..b5444129 100644 --- a/manual/APPNOTE_011_Design_Investigation/sumprod_05.dot +++ b/manual/APPNOTE_011_Design_Investigation/sumprod_05.dot @@ -12,4 +12,4 @@ n2:e -> c8:p5:w [color="black", style="setlinewidth(3)", label=""]; c8:p6:e -> n3:w [color="black", style="setlinewidth(3)", label=""]; v0:e -> c7:p4:w [color="black", style="setlinewidth(3)", label=""]; v1:e -> c7:p5:w [color="black", style="setlinewidth(3)", label=""]; -}; +} diff --git a/manual/CHAPTER_Appnotes.tex b/manual/CHAPTER_Appnotes.tex index 959aabd2..2abfa85d 100644 --- a/manual/CHAPTER_Appnotes.tex +++ b/manual/CHAPTER_Appnotes.tex @@ -2,11 +2,24 @@ \chapter{Application Notes} \label{chapter:appnotes} -\begin{fixme} -This appendix will cover some typical use-cases of Yosys in the form of application notes. -\end{fixme} +% \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{Reconfigurable Coarse-Grain Synthesis using Intersynth} -\section{Synthesizing using a Cell Library in Liberty Format} -\section{Reverse Engeneering the MOS6502 from an NMOS Transistor Netlist} -\section{Reconfigurable Coarse-Grain Synthesis using Intersynth} +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 +\end{itemize} + +\eject\label{app:010} +\includepdf[pages=-,pagecommand=\thispagestyle{plain}]{APPNOTE_010_Verilog_to_BLIF.pdf} + +\eject\label{app:011} +\includepdf[pages=-,pagecommand=\thispagestyle{plain}]{APPNOTE_011_Design_Investigation.pdf} diff --git a/manual/CHAPTER_Auxprogs.tex b/manual/CHAPTER_Auxprogs.tex index cce3741c..a0089382 100644 --- a/manual/CHAPTER_Auxprogs.tex +++ b/manual/CHAPTER_Auxprogs.tex @@ -17,3 +17,9 @@ The {\tt yosys-filterlib} tool is a small utility that can be used to strip or extract information from a Liberty file. See Sec.~\ref{sec:techmap_extern} for details. +\section{yosys-abc} + +This is a unmodified copy of ABC \citeweblink{ABC}. Not all versions of Yosys +work with all versions of ABC. So Yosys comes with its own yosys-abc to avoid +compatibility issues between the two. + diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index 64d3633e..c9bf978a 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -357,7 +357,7 @@ Add a brief description of the {\tt \$fsm} cell type. For gate level logic networks, fixed function single bit cells are used that do not provide any parameters. -Simulation models for these cells can be found in the file {\tt techlibs/common/stdcells\_sim.v} in the Yosys +Simulation models for these cells can be found in the file {\tt techlibs/common/simcells.v} in the Yosys source tree. \begin{table}[t] @@ -417,7 +417,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} cells. +Add information about {\tt \$assert}, {\tt \$assume}, and {\tt \$equiv} cells. \end{fixme} \begin{fixme} @@ -429,6 +429,14 @@ Add information about {\tt \$alu}, {\tt \$macc}, {\tt \$fa}, and {\tt \$lcu} cel \end{fixme} \begin{fixme} +Add information about {\tt \$dffe}, {\tt \$dffsr}, {\tt \$dlatch}, and {\tt \$dlatchsr} cells. +\end{fixme} + +\begin{fixme} +Add information about {\tt \$\_DFFE\_??\_}, {\tt \$\_DFFSR\_???\_}, {\tt \$\_DLATCH\_?\_}, and {\tt \$\_DLATCHSR\_???\_} cells. +\end{fixme} + +\begin{fixme} Add information about {\tt \$\_NAND\_}, {\tt \$\_NOR\_}, {\tt \$\_XNOR\_}, {\tt \$\_AOI3\_}, {\tt \$\_OAI3\_}, {\tt \$\_AOI4\_}, and {\tt \$\_OAI4\_} cells. \end{fixme} diff --git a/manual/CHAPTER_Prog.tex b/manual/CHAPTER_Prog.tex index 3918594a..3cbc95a1 100644 --- a/manual/CHAPTER_Prog.tex +++ b/manual/CHAPTER_Prog.tex @@ -2,16 +2,21 @@ \chapter{Programming Yosys Extensions} \label{chapter:prog} -\begin{fixme} -This chapter will contain a guided tour to the Yosys APIs and conclude -with an example module. -\end{fixme} +This chapter contains some bits and pieces of information about programming +yosys extensions. Also consult the section on programming in the ``Yosys +Presentation'' (can be downloaded from the Yosys website as PDF) and don't +be afraid to ask questions on the Yosys Subreddit. -\section{Programming with RTLIL} -\section{Internal Utility Libraries} -\section{Loadable Modules} +\section{The ``CodingReadme'' File} + +The following is an excerpt of the {\tt CodingReadme} file from the Yosys source tree. + +\lstinputlisting[title=CodingReadme,rangeprefix=--,rangesuffix=--,includerangemarker=false,linerange=snip-snap,numbers=left,frame=single]{../CodingReadme} + +\section{The ``stubsnets'' Example Module} + +The following is the complete code of the ``stubsnets'' example module. It is included in the Yosys source distribution as {\tt manual/CHAPTER\_Prog/stubnets.cc}. -\section{Example Module} \lstinputlisting[title=stubnets.cc,numbers=left,frame=single,language=C++]{CHAPTER_Prog/stubnets.cc} diff --git a/manual/CHAPTER_Prog/.gitignore b/manual/CHAPTER_Prog/.gitignore new file mode 100644 index 00000000..fa83c321 --- /dev/null +++ b/manual/CHAPTER_Prog/.gitignore @@ -0,0 +1,3 @@ +stubnets.so +stubnets.d +*.log diff --git a/manual/CHAPTER_Prog/stubnets.cc b/manual/CHAPTER_Prog/stubnets.cc index ef4b1245..4849c6a7 100644 --- a/manual/CHAPTER_Prog/stubnets.cc +++ b/manual/CHAPTER_Prog/stubnets.cc @@ -5,15 +5,16 @@ // binary, for any purpose, commercial or non-commercial, and by any // means. -#include "kernel/rtlil.h" -#include "kernel/register.h" +#include "kernel/yosys.h" #include "kernel/sigtools.h" -#include "kernel/log.h" #include <string> #include <map> #include <set> +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + // this function is called for each module in the design static void find_stub_nets(RTLIL::Design *design, RTLIL::Module *module, bool report_bits) { @@ -62,7 +63,7 @@ static void find_stub_nets(RTLIL::Design *design, RTLIL::Module *module, bool re // for each bit (unless it is a constant): // check if it is used at least two times and add to stub_bits otherwise - for (int i = 0; i < SIZE(sig); i++) + for (int i = 0; i < GetSize(sig); i++) if (sig[i].wire != NULL && (bit_usage_count[sig[i]] + usage_offset) < 2) stub_bits.insert(i); @@ -72,7 +73,7 @@ static void find_stub_nets(RTLIL::Design *design, RTLIL::Module *module, bool re // report stub bits and/or stub wires, don't report single bits // if called with report_bits set to false. - if (SIZE(stub_bits) == SIZE(sig)) { + if (GetSize(stub_bits) == GetSize(sig)) { log(" found stub wire: %s\n", RTLIL::id2cstr(wire->name)); } else { if (!report_bits) @@ -126,3 +127,4 @@ struct StubnetsPass : public Pass { } } StubnetsPass; +PRIVATE_NAMESPACE_END diff --git a/manual/PRESENTATION_ExAdv.tex b/manual/PRESENTATION_ExAdv.tex index 471516b4..74350091 100644 --- a/manual/PRESENTATION_ExAdv.tex +++ b/manual/PRESENTATION_ExAdv.tex @@ -790,7 +790,7 @@ Unwrap in {\tt test2}: \hfil\begin{tikzpicture} \node at (0,0) {\includegraphics[width=11cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2d.pdf}}; -\node at (0,-4) {\includegraphics[width=11cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2e.pdf}}; +\node at (0,-4) {\includegraphics[width=8cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2e.pdf}}; \node at (1,-1.7) {\begin{lstlisting}[linewidth=5.5cm, frame=single, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] techmap -map macc_xilinx_unwrap_map.v ;; \end{lstlisting}}; diff --git a/manual/PRESENTATION_ExOth/axis_master.v b/manual/PRESENTATION_ExOth/axis_master.v index 25a1feee..fe9008ad 100644 --- a/manual/PRESENTATION_ExOth/axis_master.v +++ b/manual/PRESENTATION_ExOth/axis_master.v @@ -13,7 +13,7 @@ module axis_master(aclk, aresetn, tvalid, tready, tdata); if (tvalid && tready) tvalid <= 0; if (!tvalid || !tready) begin - // ^- should be not inverted! + // ^- should not be inverted! state = state ^ state << 13; state = state ^ state >> 7; state = state ^ state << 17; diff --git a/manual/PRESENTATION_ExSyn.tex b/manual/PRESENTATION_ExSyn.tex index 80398229..b7d6b8a6 100644 --- a/manual/PRESENTATION_ExSyn.tex +++ b/manual/PRESENTATION_ExSyn.tex @@ -268,7 +268,7 @@ memory -nomap; techmap -map my_memory_map.v; memory_map \end{frame} \begin{frame}[t, fragile]{\subsecname{} -- Example 1/2} -\vbox to 0cm{\includegraphics[width=\linewidth,trim=0cm 0cm 0cm -10cm]{PRESENTATION_ExSyn/memory_01.pdf}\vss} +\vbox to 0cm{\includegraphics[width=0.7\linewidth,trim=0cm 0cm 0cm -10cm]{PRESENTATION_ExSyn/memory_01.pdf}\vss} \vskip-1cm \begin{columns} \column[t]{5cm} @@ -455,7 +455,7 @@ read_verilog -D WITH_MULT cpu_alu.v hierarchy -check -top cpu_top # high-level synthesis -proc; opt; memory -nomap;; fsm; opt +proc; opt; fsm;; memory -nomap; opt # substitute block rams techmap -map map_rams.v @@ -497,7 +497,7 @@ the next part (Section 3, ``Advanced Synthesis'') of this presentation.} \item Yosys provides commands for each phase of the synthesis. \item Each command solves a (more or less) simple problem. \item Complex commands are often only front-ends to simple commands. -\item {\tt proc; opt; memory; opt; fsm; opt; techmap; opt; abc;;} +\item {\tt proc; opt; fsm; opt; memory; opt; techmap; opt; abc;;} \end{itemize} \bigskip diff --git a/manual/PRESENTATION_Intro.tex b/manual/PRESENTATION_Intro.tex index 7697266d..5aeebd9f 100644 --- a/manual/PRESENTATION_Intro.tex +++ b/manual/PRESENTATION_Intro.tex @@ -277,7 +277,7 @@ Direct link to the files: \\ \footnotesize \medskip {\color{YosysGreen}\# the high-level stuff}\\ -\boxalert<3>{proc}; \boxalert<4>{opt}; \boxalert<5>{memory}; \boxalert<6>{opt}; \boxalert<7>{fsm}; \boxalert<8>{opt} +\boxalert<3>{proc}; \boxalert<4>{opt}; \boxalert<5>{fsm}; \boxalert<6>{opt}; \boxalert<7>{memory}; \boxalert<8>{opt} \medskip {\color{YosysGreen}\# mapping to internal cell library}\\ @@ -308,9 +308,9 @@ Direct link to the files: \\ \footnotesize \only<2>{hierarchy -check -top counter}% \only<3>{proc}% \only<4>{opt}% -\only<5>{memory}% +\only<5>{fsm}% \only<6>{opt}% -\only<7>{fsm}% +\only<7>{memory}% \only<8>{opt}% \only<9>{techmap}% \only<10>{opt}% @@ -333,13 +333,13 @@ Direct link to the files: \\ \footnotesize Perform some basic optimizations and cleanups. }% \only<5>{ - Analyze memories and create circuits to implement them. + Analyze and optimize finite state machines. }% \only<6>{ Perform some basic optimizations and cleanups. }% \only<7>{ - Analyze and optimize finite state machines. + Analyze memories and create circuits to implement them. }% \only<8>{ Perform some basic optimizations and cleanups. @@ -398,7 +398,7 @@ hierarchy -check -top counter \begin{frame}[t, fragile]{\subsecname{} -- Step 2/4} \begin{verbatim} -proc; opt; memory; opt; fsm; opt +proc; opt; fsm; opt; memory; opt \end{verbatim} \vfill @@ -411,7 +411,7 @@ techmap; opt \end{verbatim} \vfill -\includegraphics[width=\linewidth,trim=0 0cm 0 0cm]{PRESENTATION_Intro/counter_02.pdf} +\includegraphics[width=\linewidth,trim=0 0cm 0 2cm]{PRESENTATION_Intro/counter_02.pdf} \end{frame} \begin{frame}[t, fragile]{\subsecname{} -- Step 4/4} @@ -427,6 +427,48 @@ clean %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\subsection{The synth command} + +\begin{frame}[fragile]{\subsecname{}} +Yosys contains a default (recommended example) synthesis script in form of the +{\tt synth} command. The following commands are executed by this synthesis command: + +\begin{columns} +\column[t]{5cm} +\begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] +begin: + hierarchy -check [-top <top>] + +coarse: + proc + opt + wreduce + alumacc + share + opt + fsm + opt -fast + memory -nomap + opt_clean +\end{lstlisting} +\column[t]{5cm} +\begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] +fine: + opt -fast -full + memory_map + opt -full + techmap + opt -fast + +abc: + abc -fast + opt -fast +\end{lstlisting} +\end{columns} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \subsection{Yosys Commands} \begin{frame}[fragile]{\subsecname{} 1/3 \hspace{0pt plus 1 filll} (excerpt)} @@ -500,6 +542,7 @@ Commands for writing the results: \bigskip Script-Commands for standard synthesis tasks: \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] + synth # generic synthesis script synth_xilinx # synthesis for Xilinx FPGAs \end{lstlisting} @@ -603,12 +646,8 @@ endmodule \begin{frame}{\subsecname} \begin{itemize} -\item Multi-dimensional arrays (memories) -\item Writing to arrays using bit- and part-selects (todo for 0.4.0) -\item The wor/wand wire types (maybe for 0.4.0) \item Tri-state logic - -\bigskip +\item The wor/wand wire types (maybe for 0.5) \item Latched logic (is synthesized as logic with feedback loops) \item Some non-synthesizable features that should be ignored in synthesis are not supported by the parser and cause a parser error (file a bug report if you encounter this problem) \end{itemize} @@ -813,10 +852,12 @@ control logic because it is simpler than setting up a commercial flow. \item When building on other Linux distributions: \begin{itemize} \item Needs compiler with some C++11 support +\item See README file for build instructions \item Post to the subreddit if you get stuck \end{itemize} \item Ported to OS X (Darwin) and OpenBSD -\item No win32 support (yet) +\item Native win32 build with VisualStudio +\item Cross win32 build with MXE \end{itemize} \end{frame} diff --git a/manual/PRESENTATION_Prog.tex b/manual/PRESENTATION_Prog.tex index 590451be..96189e55 100644 --- a/manual/PRESENTATION_Prog.tex +++ b/manual/PRESENTATION_Prog.tex @@ -89,12 +89,13 @@ left with a much simpler version of RTLIL: \bigskip Many commands simply choose to only work on this simpler version: \begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont] -if (module->processes.size() != 0 || module->memories.size() != 0) - log_error("This command does not operate on modules with processes " - "and/or memories! Run 'proc' and 'memory' first.\n"); +for (RTLIL::Module *module : design->selected_modules() { + if (module->has_memories_warn() || module->has_processes_warn()) + continue; + .... +} \end{lstlisting} -\bigskip For simplicity we only discuss this version of RTLIL in this presentation. \end{frame} @@ -122,8 +123,9 @@ has been executed. \subsection{The RTLIL Data Structures} \begin{frame}{\subsecname} -The RTLIL data structures are simple structs utilizing C++ {\tt std::} -containers. +The RTLIL data structures are simple structs utilizing {\tt pool<>} and +{\tt dict<>} containers (drop-in replacementments for {\tt +std::unordered\_set<>} and {\tt std::unordered\_map<>}). \bigskip \begin{itemize} @@ -145,7 +147,9 @@ See {\tt yosys/kernel/rtlil.h} for details. \subsubsection{RTLIL::IdString} \begin{frame}{\subsubsecname}{} -{\tt RTLIL::IdString} is a simple wrapper for {\tt std::string}. It is used for names of RTLIL objects. +{\tt RTLIL::IdString} in many ways behave like a {\tt std::string}. It is used +for names of RTLIL objects. Internally a RTLIL::IdString object is only a +single integer. \medskip The first character of a {\tt RTLIL::IdString} specifies if the name is {\it public\/} or {\it private\/}: @@ -168,25 +172,25 @@ Use the {\tt NEW\_ID} macro to create a new unique private name. \begin{frame}[t, fragile]{\subsubsecname} The {\tt RTLIL::Design} and {\tt RTLIL::Module} structs are the top-level RTLIL -data structures. - -Yosys always operates on one active design, but can hold many designs in memory. +data structures. Yosys always operates on one active design, but can hold many designs in memory. \bigskip \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++] struct RTLIL::Design { - std::map<RTLIL::IdString, RTLIL::Module*> modules; + dict<RTLIL::IdString, RTLIL::Module*> modules_; ... }; struct RTLIL::Module { RTLIL::IdString name; - std::map<RTLIL::IdString, RTLIL::Wire*> wires; - std::map<RTLIL::IdString, RTLIL::Cell*> cells; - std::vector<RTLIL::SigSig> connections; + dict<RTLIL::IdString, RTLIL::Wire*> wires_; + dict<RTLIL::IdString, RTLIL::Cell*> cells_; + std::vector<RTLIL::SigSig> connections_; ... }; \end{lstlisting} + +(Use the various accessor functions instead of directly working with the {\tt *\_} members.) \end{frame} \subsubsection{The RTLIL::Wire Structure} @@ -251,21 +255,22 @@ constants are part of the RTLIL representation itself. \begin{frame}[t, fragile]{\subsubsecname} The {\tt RTLIL::SigSpec} struct represents a signal vector. Each bit can either be a bit from a wire -or a constant value. Consecutive bits from a wire or consecutive constant bits are consolidated into -a {\tt RTLIL::SigChunk}: +or a constant value. \bigskip \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++] -struct RTLIL::SigChunk { +struct RTLIL::SigBit +{ RTLIL::Wire *wire; - RTLIL::Const data; // only used if wire == NULL - int width, offset; + union { + RTLIL::State data; // used if wire == NULL + int offset; // used if wire != NULL + }; ... }; struct RTLIL::SigSpec { - std::vector<RTLIL::SigChunk> chunks; // LSB at index 0 - int width; + std::vector<RTLIL::SigBit> bits_; // LSB at index 0 ... }; \end{lstlisting} @@ -289,8 +294,8 @@ instances: \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++] struct RTLIL::Cell { RTLIL::IdString name, type; - std::map<RTLIL::IdString, RTLIL::SigSpec> connections; - std::map<RTLIL::IdString, RTLIL::Const> parameters; + dict<RTLIL::IdString, RTLIL::SigSpec> connections_; + dict<RTLIL::IdString, RTLIL::Const> parameters; ... }; \end{lstlisting} @@ -345,7 +350,7 @@ typedef std::pair<RTLIL::SigSpec, RTLIL::SigSpec> RTLIL::SigSig; struct RTLIL::Module { ... - std::vector<RTLIL::SigSig> connections; + std::vector<RTLIL::SigSig> connections_; ... }; \end{lstlisting} @@ -354,8 +359,8 @@ struct RTLIL::Module { {\tt RTLIL::SigSig::first} is the driven signal and {\tt RTLIL::SigSig::second} is the driving signal. Example usage (setting wire {\tt foo} to value {\tt 42}): \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++] -module->connections.push_back(RTLIL::SigSig(module->wires.at("\\foo"), - RTLIL::SigSpec(42, module->wires.at("\\foo")->width))); +module->connect(module->wire("\\foo"), + RTLIL::SigSpec(42, module->wire("\\foo")->width)); \end{lstlisting} \end{frame} @@ -378,17 +383,19 @@ endmodule RTLIL::Module *module = new RTLIL::Module; module->name = "\\absval"; -RTLIL::Wire *a = module->new_wire(4, "\\a"); +RTLIL::Wire *a = module->addWire("\\a", 4); a->port_input = true; a->port_id = 1; -RTLIL::Wire *y = module->new_wire(4, "\\y"); +RTLIL::Wire *y = module->addWire("\\y", 4); y->port_output = true; y->port_id = 2; -RTLIL::Wire *a_inv = module->new_wire(4, NEW_ID); +RTLIL::Wire *a_inv = module->addWire(NEW_ID, 4); module->addNeg(NEW_ID, a, a_inv, true); module->addMux(NEW_ID, a, a_inv, RTLIL::SigSpec(a, 1, 3), y); + +module->fixup_ports(); \end{lstlisting} \end{frame} @@ -431,8 +438,8 @@ In this case {\tt a}, {\tt x}, and {\tt y} are all different names for the same \smallskip \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++] -RTLIL::SigSpec a(module->wires.at("\\a")), x(module->wires.at("\\x")), - y(module->wires.at("\\y")); +RTLIL::SigSpec a(module->wire("\\a")), x(module->wire("\\x")), + y(module->wire("\\y")); log("%d %d %d\n", a == x, x == y, y == a); // will print "0 0 0" \end{lstlisting} @@ -462,9 +469,9 @@ log("Mapped signal x: %s\n", log_signal(sigmap(x))); \end{lstlisting} \medskip -Use {\tt RTLIL::id2cstr()} to create a C-string for an {\tt RTLIL::IdString}: +Use {\tt log\_id()} to create a C-string for an {\tt RTLIL::IdString}: \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++] -log("Name of this module: %s\n", RTLIL::id2cstr(module->name)); +log("Name of this module: %s\n", log_id(module->name)); \end{lstlisting} \medskip @@ -513,9 +520,8 @@ a new yosys command: \bigskip \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=C++] -#include "kernel/rtlil.h" -#include "kernel/register.h" -#include "kernel/log.h" +#include "kernel/yosys.h" +USING_YOSYS_NAMESPACE struct MyPass : public Pass { MyPass() : Pass("my_cmd", "just a simple test") { } @@ -526,9 +532,9 @@ struct MyPass : public Pass { log(" %s\n", arg.c_str()); log("Modules in current design:\n"); - for (auto &mod : design->modules) - log(" %s (%zd wires, %zd cells)\n", RTLIL::id2cstr(mod.first), - mod.second->wires.size(), mod.second->cells.size()); + for (auto mod : design->modules()) + log(" %s (%d wires, %d cells)\n", log_id(mod), + GetSize(mod->wires), GetSize(mod->cells)); } } MyPass; \end{lstlisting} @@ -550,6 +556,12 @@ yosys-config --exec --cxx --cxxflags --ldflags \ \end{lstlisting} \bigskip +Or shorter: +\begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont] +yosys-config --build my_cmd.so my_cmd.cc +\end{lstlisting} + +\bigskip Load the plugin using the yosys {\tt -m} option: \begin{lstlisting}[xleftmargin=1cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont] yosys -m ./my_cmd.so -p 'my_cmd foo bar' @@ -566,7 +578,7 @@ yosys -m ./my_cmd.so -p 'my_cmd foo bar' \item \dots and even simpler if you don't need RTLIL::Memory or RTLIL::Process objects. \bigskip -\item Writing synthesis software? Consider learning the Yosys API and make your stuff +\item Writing synthesis software? Consider learning the Yosys API and make your work part of the Yosys framework. \end{itemize} diff --git a/manual/PRESENTATION_Prog/.gitignore b/manual/PRESENTATION_Prog/.gitignore index 7fd56076..ccdd6bd5 100644 --- a/manual/PRESENTATION_Prog/.gitignore +++ b/manual/PRESENTATION_Prog/.gitignore @@ -1 +1,2 @@ my_cmd.so +my_cmd.d diff --git a/manual/PRESENTATION_Prog/my_cmd.cc b/manual/PRESENTATION_Prog/my_cmd.cc index 381b0587..1d28ce97 100644 --- a/manual/PRESENTATION_Prog/my_cmd.cc +++ b/manual/PRESENTATION_Prog/my_cmd.cc @@ -1,6 +1,9 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + struct MyPass : public Pass { MyPass() : Pass("my_cmd", "just a simple test") { } virtual void execute(std::vector<std::string> args, RTLIL::Design *design) @@ -12,7 +15,7 @@ struct MyPass : public Pass { log("Modules in current design:\n"); for (auto mod : design->modules()) log(" %s (%zd wires, %zd cells)\n", log_id(mod), - SIZE(mod->wires()), SIZE(mod->cells())); + GetSize(mod->wires()), GetSize(mod->cells())); } } MyPass; @@ -25,6 +28,7 @@ struct Test1Pass : public Pass { log_error("A module with the name absval already exists!\n"); RTLIL::Module *module = design->addModule("\\absval"); + log("Name of this module: %s\n", log_id(module)); RTLIL::Wire *a = module->addWire("\\a", 4); a->port_input = true; @@ -38,7 +42,7 @@ struct Test1Pass : public Pass { module->addNeg(NEW_ID, a, a_inv, true); module->addMux(NEW_ID, a, a_inv, RTLIL::SigSpec(a, 3), y); - log("Name of this module: %s\n", log_id(module)); + module->fixup_ports(); } } Test1Pass; @@ -69,3 +73,4 @@ struct Test2Pass : public Pass { } } Test2Pass; +PRIVATE_NAMESPACE_END diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index 35249ed8..d653f409 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -15,22 +15,99 @@ library to a target architecture. -script <file> 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 + leading plus sign is removed and all commas (,) in the string are + replaced with blanks before the string is passed to ABC. + + if no -script parameter is given, the following scripts are used: + + for -liberty without -constr: + strash; scorr; ifraig; retime {D}; strash; dch -f; map {D} + + for -liberty with -constr: + strash; scorr; ifraig; retime {D}; strash; dch -f; map {D}; + buffer; upsize {D}; dnsize {D}; stime -p + + for -lut: + strash; scorr; ifraig; retime; strash; dch -f; if + + otherwise: + strash; scorr; ifraig; retime; strash; dch -f; map + + -fast + use different default scripts that are slightly faster (at the cost + of output quality): + + for -liberty without -constr: + retime {D}; map {D} + + for -liberty with -constr: + retime {D}; map {D}; buffer; upsize {D}; dnsize {D}; stime -p + + for -lut: + retime; if + + otherwise: + retime; map + -liberty <file> generate netlists for the specified cell library (using the liberty - file format). Without this option, ABC is used to optimize the netlist - but keeps using yosys's internal gate library. This option is ignored if - the -script option is also used. + file format). -constr <file> - pass this file with timing constraints to ABC + pass this file with timing constraints to ABC. use with -liberty. + + a constr file contains two lines: + set_driving_cell <cell_name> + set_load <floating_point_number> + + the set_driving_cell statement defines which cell type is assumed to + drive the primary inputs and the set_load statement sets the load in + femtofarads for each primary output. + + -D <picoseconds> + set delay target. the string {D} in the default scripts above is + replaced by this option when used, and an empty string otherwise. -lut <width> generate netlist using luts of (max) the specified width. + -lut <w1>:<w2> + generate netlist using luts of (max) the specified width <w2>. All + luts with width <= <w1> have constant cost. for luts larger than <w1> + the area cost doubles with each additional input bit. the delay cost + is still constant for all lut widths. + + -dff + also pass $_DFF_?_ and $_DFFE_??_ cells through ABC. modules with many + clock domains are automatically partitioned in clock domains and each + domain is passed through ABC independently. + + -clk [!]<clock-signal-name>[,[!]<enable-signal-name>] + use only the specified clock domain. this is like -dff, but only FF + cells that belong to the specified clock domain are used. + + -keepff + set the "keep" attribute on flip-flop output wires. (and thus preserve + them, for example for equivialence checking.) + -nocleanup when this option is used, the temporary files created by this pass are not removed. this is useful for debugging. + -showtmp + print the temp dir name in log. usually this is suppressed so that the + command output is identical across runs. + + -markgroups + set a 'abcgroup' attribute on all objects created by ABC. The value of + this attribute is a unique integer for each ABC process started. This + is useful for debugging the partitioning of clock domains. + +When neither -liberty nor -lut is used, the Yosys standard cell library is +loaded into ABC before the ABC script is executed. + 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.) @@ -59,6 +136,15 @@ Like 'add -input', but also connect the signal between instances of the selected modules. \end{lstlisting} +\section{alumacc -- extract ALU and MACC cells} +\label{cmd:alumacc} +\begin{lstlisting}[numbers=left,frame=single] + alumacc [selection] + +This pass translates arithmetic operations like $add, $mul, $lt, etc. to $alu +and $macc cells. +\end{lstlisting} + \section{cd -- a shortcut for 'select -module <name>'} \label{cmd:cd} \begin{lstlisting}[numbers=left,frame=single] @@ -92,6 +178,129 @@ When commands are separated using the ';;;' token, this command will be executed in -purge mode between the commands. \end{lstlisting} +\section{connect -- create or remove connections} +\label{cmd:connect} +\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 +drivers for <lhs-expr> are unconnected. This can be overwritten by using +the -nounset option. + + + connect [-nomap] -unset <expr> + +Unconnect all existing drivers for the specified expression. + + + connect [-nomap] -port <cell> <port> <expr> + +Connect the specified cell port to the specified cell port. + + +Per default signal alias names are resolved and all signal names are mapped +the the signal name of the primary driver. Using the -nomap option deactivates +this behavior. + +The connect command operates in one module only. Either only one module must +be selected or an active module must be set using the 'cd' command. + +This command does not operate on module with processes. +\end{lstlisting} + +\section{connwrappers -- replace undef values with defined constants} +\label{cmd:connwrappers} +\begin{lstlisting}[numbers=left,frame=single] + connwrappers [options] [selection] + +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 +the driving cell. + + -signed <cell_type> <port_name> <width_param> + -unsigned <cell_type> <port_name> <width_param> + consider the specified signed/unsigned wrapper output + + -port <cell_type> <port_name> <width_param> <sign_param> + use the specified parameter to decide if signed or unsigned + +The options -signed, -unsigned, and -port can be specified multiple times. +\end{lstlisting} + +\section{copy -- copy modules in the design} +\label{cmd:copy} +\begin{lstlisting}[numbers=left,frame=single] + copy old_name new_name + +Copy the specified module. Note that selection patterns are not supported +by this command. +\end{lstlisting} + +\section{cover -- print code coverage counters} +\label{cmd:cover} +\begin{lstlisting}[numbers=left,frame=single] + cover [options] [pattern] + +Print the code coverage counters collected using the cover() macro in the Yosys +C++ code. This is useful to figure out what parts of Yosys are utilized by a +test bench. + + -q + Do not print output to the normal destination (console and/or log file) + + -o file + Write output to this file, truncate if exists. + + -a file + Write output to this file, append if exists. + + -d dir + Write output to a newly created file in the specified directory. + +When one or more pattern (shell wildcards) are specified, then only counters +matching at least one pattern are printed. + + +It is also possible to instruct Yosys to print the coverage counters on program +exit to a file using environment variables: + + YOSYS_COVER_DIR="{dir-name}" yosys {args} + + This will create a file (with an auto-generated name) in this + directory and write the coverage counters to it. + + YOSYS_COVER_FILE="{file-name}" yosys {args} + + This will append the coverage counters to the specified file. + + +Hint: Use the following AWK command to consolidate Yosys coverage files: + + gawk '{ p[$3] = $1; c[$3] += $2; } END { for (i in p) + printf "%-60s %10d %s\n", p[i], c[i], i; }' {files} | sort -k3 + + +Coverage counters are only available in Yosys for Linux. +\end{lstlisting} + +\section{delete -- delete objects in the design} +\label{cmd:delete} +\begin{lstlisting}[numbers=left,frame=single] + delete [selection] + +Deletes the selected objects. This will also remove entire modules, if the +whole module is selected. + + + delete {-input|-output|-port} [selection] + +Does not delete any object but removes the input and/or output flag on the +selected wires, thus 'deleting' module ports. +\end{lstlisting} + \section{design -- save, restore and reset current design} \label{cmd:design} \begin{lstlisting}[numbers=left,frame=single] @@ -105,22 +314,75 @@ Clear the current design. Save the current design under the given name. + design -stash <name> + +Save the current design under the given name and then clear the current design. + + + design -push + +Push the current design to the stack and then clear the current design. + + + design -pop + +Reset the current design and pop the last design from the stack. + + design -load <name> Reset the current design and load the design previously saved under the given name. + + + design -copy-from <name> [-as <new_mod_name>] <selection> + +Copy modules from the specified design into the current one. The selection is +evaluated in the other design. + + + design -copy-to <name> [-as <new_mod_name>] [selection] + +Copy modules from the current design into the soecified one. +\end{lstlisting} + +\section{dff2dffe -- transform \$dff cells to \$dffe cells} +\label{cmd:dff2dffe} +\begin{lstlisting}[numbers=left,frame=single] + dff2dffe [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 +$_DFF_P_, $_DFF_N_ and $_MUX_. + + -unmap + operate in the opposite direction: replace $dffe cells with combinations + of $dff and $mux cells. the options below are ignore in unmap mode. + + -direct <internal_gate_type> <external_gate_type> + map directly to external gate type. <internal_gate_type> can + be any internal gate-level FF cell (except $_DFFE_??_). the + <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 + that is then translated to the final type using 'techmap'. \end{lstlisting} \section{dfflibmap -- technology mapping of flip-flops} \label{cmd:dfflibmap} \begin{lstlisting}[numbers=left,frame=single] - dfflibmap -liberty <file> [selection] + dfflibmap [-prepare] -liberty <file> [selection] Map internal flip-flop cells to the flip-flop cells in the technology library specified in the given liberty file. This pass may add inverters as needed. Therefore it is recommended to first run this pass and then map the logic paths to the target technology. + +When called with -prepare, this command will convert the internal FF cells +to the internal cell types that best match the cells found in the given +liberty file. \end{lstlisting} \section{dump -- print parts of the design in ilang format} @@ -138,8 +400,151 @@ ilang format. -n only dump the module headers if the entire module is selected - -outfile <filename> - Write to the specified file. + -o <filename> + write to the specified file. + + -a <filename> + like -outfile but append instead of overwrite +\end{lstlisting} + +\section{echo -- turning echoing back of commands on and off} +\label{cmd:echo} +\begin{lstlisting}[numbers=left,frame=single] + echo on + +Print all commands to log before executing them. + + + echo off + +Do not print all commands to log before executing them. (default) +\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 + +This command adds an $equiv cell for the specified signals. +\end{lstlisting} + +\section{equiv\_induct -- proving \$equiv cells using temporal induction} +\label{cmd:equiv_induct} +\begin{lstlisting}[numbers=left,frame=single] + equiv_induct [options] [selection] + +Uses a version of temporal induction to prove $equiv cells. + +Only selected $equiv cells are proven and only selected cells are used to +perform the proof. + + -undef + enable modelling of undef states + + -seq <N> + the max. number of time steps to be considered (default = 4) + +This command is very effective in proving complex sequential circuits, when +the internal state of the circuit quickly propagates to $equiv cells. + +However, this command uses a weak definition of 'equivalence': This command +proves that the two circuits will not diverge after they produce equal +outputs (observable points via $equiv) for at least <N> cycles (the <N> +specified via -seq). + +Combined with simulation this is very powerful because simulation can give +you confidence that the circuits start out synced for at least <N> cycles +after reset. +\end{lstlisting} + +\section{equiv\_make -- prepare a circuit for equivalence checking} +\label{cmd:equiv_make} +\begin{lstlisting}[numbers=left,frame=single] + equiv_make [options] gold_module gate_module equiv_module + +This creates a module annotated with $equiv cells from two presumably +equivalent modules. Use commands such as 'equiv_simple' and 'equiv_status' +to work with the created equivalent checking module. + + -inames + Also match cells and wires with $... names. + + -blacklist <file> + Do not match cells or signals that match the names in the file. + + -encfile <file> + Match FSM encodings using the desiption from the file. + See 'help fsm_recode' for details. + +Note: The circuit created by this command is not a miter (with something like +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\_miter -- extract miter from equiv circuit} +\label{cmd:equiv_miter} +\begin{lstlisting}[numbers=left,frame=single] + equiv_miter [options] miter_module [selection] + +This creates a miter module for further analysis of the selected $equiv cells. + + -trigger + Create a trigger output + + -cmp + Create cmp_* outputs for individual unproven $equiv cells + + -assert + Create a $assert cell for each unproven $equiv cell + + -undef + Create compare logic that handles undefs correctly +\end{lstlisting} + +\section{equiv\_remove -- remove \$equiv cells} +\label{cmd:equiv_remove} +\begin{lstlisting}[numbers=left,frame=single] + equiv_remove [options] [selection] + +This command removes the selected $equiv cells. If neither -gold nor -gate is +used then only proven cells are removed. + + -gold + keep gold circuit + + -gate + keep gate circuit +\end{lstlisting} + +\section{equiv\_simple -- try proving simple \$equiv instances} +\label{cmd:equiv_simple} +\begin{lstlisting}[numbers=left,frame=single] + equiv_simple [options] [selection] + +This command tries to prove $equiv cells using a simple direct SAT approach. + + -v + verbose output + + -undef + enable modelling of undef states + + -nogroup + disabling grouping of $equiv cells by output wire + + -seq <N> + the max. number of time steps to be considered (default = 1) +\end{lstlisting} + +\section{equiv\_status -- print status of equivalent checking module} +\label{cmd:equiv_status} +\begin{lstlisting}[numbers=left,frame=single] + equiv_status [options] [selection] + +This command prints status information for all selected $equiv cells. + + -assert + produce an error if any unproven $equiv cell is found \end{lstlisting} \section{eval -- evaluate the circuit given an input} @@ -164,6 +569,38 @@ inputs. then all output ports of the current module are used. \end{lstlisting} +\section{expose -- convert internal signals to module ports} +\label{cmd:expose} +\begin{lstlisting}[numbers=left,frame=single] + expose [options] [selection] + +This command exposes all selected internal signals of a module as additional +outputs. + + -dff + only consider wires that are directly driven by register cell. + + -cut + when exposing a wire, create an input/output pair and cut the internal + 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. + + -evert + also turn connections to instances of other modules to additional + inputs and outputs and remove the module instances. + + -evert-dff + turn flip-flops to sets of inputs and outputs. + + -sep <separator> + when creating new wire/port names, the original object name is suffixed + with this separator (default: '.') and the port name or a type + designator for the exposed signal. +\end{lstlisting} + \section{extract -- find subcircuits and replace them with cells} \label{cmd:extract} \begin{lstlisting}[numbers=left,frame=single] @@ -175,7 +612,12 @@ 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 <map_file> - use the modules in this file as reference + use the modules in this file as reference. This option can be used + multiple times. + + -map %<design-name> + use the modules in this in-memory design as reference. This option can + be used multiple times. -verbose print debug output while analyzing @@ -209,6 +651,12 @@ map file can be a verilog source file (*.v) or an ilang file (*.il). -wire_attr <attribute_name> Attributes on wires with the given name must match. + -ignore_parameters + Do not use parameters when matching cells. + + -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. (I.e. the 'proc' pass should be used first to convert processes to netlists.) @@ -257,11 +705,27 @@ pass is using the current design as mapping library. 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 -removed. +disconnected. A subsequent call to 'clean' will remove the redundant drivers. + + -v, -vv + enable verbose or very verbose output + + -inv + enable explicit handling of inverted signals + + -stop <n> + stop after <n> reduction operations. this is mostly used for + debugging the freduce command itself. + + -dump <prefix> + dump the design to <prefix>_<module>_<num>.il after each reduction + operation. this is mostly used for debugging the freduce command. - -try - do not issue an error when the analysis fails. - (usually beacause of logic loops in the design) +This pass is undef-aware, i.e. it considers don't-care values for detecting +equivialent nodes. + +All selected wires are considered for rewiring. The selected cells cover the +circuit that is analyzed. \end{lstlisting} \section{fsm -- extract and optimize finite state machines} @@ -297,6 +761,7 @@ Options: -encoding tye -fm_set_fsm_file file + -encfile file passed through to fsm_recode pass \end{lstlisting} @@ -393,16 +858,24 @@ combination with the 'opt_clean' pass (see also 'help fsm'). \section{fsm\_recode -- recoding finite state machines} \label{cmd:fsm_recode} \begin{lstlisting}[numbers=left,frame=single] - fsm_recode [-encoding type] [-fm_set_fsm_file file] [selection] + fsm_recode [options] [selection] This pass reassign the state encodings for FSM cells. At the moment only -one-hot encoding and binary encoding is supported. The option -encoding -can be used to specify the encoding scheme used for FSMs without the -`fsm_encoding' attribute (or with the attribute set to `auto'. +one-hot encoding and binary encoding is supported. + -encoding <type> + specify the encoding scheme used for FSMs without the + 'fsm_encoding' attribute or with the attribute set to `auto'. + + -fm_set_fsm_file <file> + generate a file containing the mapping from old to new FSM encoding + in form of Synopsys Formality set_fsm_* commands. -The option -fm_set_fsm_file can be used to generate a file containing the -mapping from old to new FSM encoding in form of Synopsys Formality set_fsm_* -commands. + -encfile <file> + write the mappings from old to new FSM encoding to a file in the + following format: + + .fsm <module_name> <state_signal> + .map <old_bitpattern> <new_bitpattern> \end{lstlisting} \section{help -- display help messages} @@ -428,10 +901,24 @@ needed. also check the design hierarchy. this generates an error when an unknown module is used as cell type. + -purge_lib + by default the hierarchy command will not remove library (blackbox) + module. use this options to also remove unused blackbox modules. + + -libdir <directory> + search for files named <module_name>.v in the specified directory + for unknown modules and automatically run read_verilog for each + unknown module. + -keep_positionals per default this pass also converts positional arguments in cells to arguments using port names. this option disables this behavior. + -nokeep_asserts + per default this pass sets the "keep" attribute on all modules + that directly or indirectly contain one or more $assert cells. this + option disables this behavior. + -top <module> use the specified top module to built a design hierarchy. modules outside this tree (unused modules) are removed. @@ -457,6 +944,25 @@ This pass ignores the current selection and always operates on all modules in the current design. \end{lstlisting} +\section{hilomap -- technology mapping of constant hi- and/or lo-drivers} +\label{cmd:hilomap} +\begin{lstlisting}[numbers=left,frame=single] + hilomap [options] [selection] + +Map constants to 'tielo' and 'tiehi' driver cells. + + -hicell <celltype> <portname> + Replace constant hi bits with this cell. + + -locell <celltype> <portname> + Replace constant lo bits with this cell. + + -singleton + Create only one hi/lo cell and connect all constant bits + to that cell. Per default a separate cell is created for + each constant bit. +\end{lstlisting} + \section{history -- show last interactive commands} \label{cmd:history} \begin{lstlisting}[numbers=left,frame=single] @@ -491,39 +997,160 @@ the resulting cells to more sophisticated PAD cells. -nameparam <param_name> Use the specified parameter to set the port name. + + -bits + create individual bit-wide buffers even for ports that + are wider. (the default behavior is to create word-wide + buffers using -widthparam to set the word size on the cell.) +\end{lstlisting} + +\section{log -- print text and log files} +\label{cmd:log} +\begin{lstlisting}[numbers=left,frame=single] + log string + +Print the given string to the screen and/or the log file. This is useful for TCL +scripts, because the TCL command "puts" only goes to stdout but not to +logfiles. + + -stdout + Print the output to stdout too. This is useful when all Yosys is executed + with a script and the -q (quiet operation) argument to notify the user. + + -stderr + Print the output to stderr too. + + -nolog + Don't use the internal log() command. Use either -stdout or -stderr, + otherwise no output will be generated at all. + + -n + do not append a newline \end{lstlisting} \section{ls -- list modules or objects in modules} \label{cmd:ls} \begin{lstlisting}[numbers=left,frame=single] - ls [pattern] + ls [selection] -When no active module is selected, this prints a list of all modules. +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} -If a pattern is given, the objects matching the pattern are printed +\section{maccmap -- mapping macc cells} +\label{cmd:maccmap} +\begin{lstlisting}[numbers=left,frame=single] + maccmap [-unmap] [selection] -Note that this command does not use the selection mechanism and always operates -on the whole design or whole active module. Use 'select -list' to show a list -of currently selected objects. +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. \end{lstlisting} \section{memory -- translate memories to basic cells} \label{cmd:memory} \begin{lstlisting}[numbers=left,frame=single] - memory [-nomap] [selection] + memory [-nomap] [-bram <bram_rules>] [selection] This pass calls all the other memory_* passes in a useful order: memory_dff + opt_clean + memory_share + opt_clean memory_collect - memory_map (skipped if called with -nomap) + memory_bram -rules <bram_rules> (when called with -bram) + memory_map (skipped if called with -nomap) This converts memories to word-wide DFFs and address decoders or multiport memory blocks if called with the -nomap option. \end{lstlisting} +\section{memory\_bram -- map memories to block rams} +\label{cmd:memory_bram} +\begin{lstlisting}[numbers=left,frame=single] + memory_bram -rules <rule_file> [selection] + +This pass converts the multi-port $mem memory cells into block ram instances. +The given rules file describes the available resources and how they should be +used. + +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 + 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) + clocks 1 2 # clock configuration + clkpol 2 2 # clock polarity configuration + endbram + +For the option 'transp' the value 0 means non-transparent, 1 means transparent +and a value greater than 1 means configurable. All groups with the same +value greater than 1 share the same configuration bit. + +For the option 'clocks' the value 0 means non-clocked, and a value greater +than 0 means clocked. All groups with the same value share the same clock +signal. + +For the option 'clkpol' the value 0 means negative edge, 1 means positive edge +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. + +It is also possible to create variants by repeating statements in the bram block +and appending '@<label>' to the individual statements. + +A match rule looks like this: + + match RAMB1024X32 + max waste 16384 # only use this bram if <= 16k ram bits are unused + min efficiency 80 # only use this bram if efficiency is at least 80% + endmatch + +It is possible to match against the following values with min/max rules: + + words ........ number of words in memory in design + abits ........ number of address bits on memory in design + dbits ........ number of data bits on memory in design + wports ....... number of write ports on memory in design + rports ....... number of read ports on memory in design + ports ........ number of ports on memory in design + bits ......... number of bits in memory in design + dups .......... number of duplications for more read ports + + awaste ....... number of unused address slots for this match + dwaste ....... number of unused data bits for this match + bwaste ....... number of unused bram bits for this match + waste ........ total number of unused bram bits (bwaste*dups) + efficiency ... total percentage of used and non-duplicated bits + + acells ....... number of cells in 'address-direction' + 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 +description. Use 'techmap' to convert the created bram instances into +instances of the actual bram cells of your target architecture. + +A match containing the command 'or_next_if_better' is only used if it +has a higher efficiency than the next match (and the one after that if +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 'shuffle_enable A' will re-organize +the data bits to accommodate the enable pattern of port A. +\end{lstlisting} + \section{memory\_collect -- creating multi-port memory cells} \label{cmd:memory_collect} \begin{lstlisting}[numbers=left,frame=single] @@ -536,11 +1163,14 @@ memory cells. \section{memory\_dff -- merge input/output DFFs into memories} \label{cmd:memory_dff} \begin{lstlisting}[numbers=left,frame=single] - memory_dff [selection] + memory_dff [options] [selection] 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 + do not merge registers on read ports \end{lstlisting} \section{memory\_map -- translate multiport memories to basic cells} @@ -552,26 +1182,101 @@ This pass converts multiport memory cells as generated by the memory_collect pass to word-wide DFFs and address decoders. \end{lstlisting} +\section{memory\_share -- consolidate memory ports} +\label{cmd:memory_share} +\begin{lstlisting}[numbers=left,frame=single] + memory_share [selection] + +This pass merges share-able memory ports into single memory ports. + +The following methods are used to consolidate the number of memory ports: + + - When write ports are connected to async read ports accessing the same + address, then this feedback path is converted to a write port with + byte/part enable signals. + + - When multiple write ports access the same address then this is converted + to a single write port with a more complex data and/or enable logic path. + + - When multiple write ports are never accessed at the same time (a SAT + solver is used to determine this), then the ports are merged into a single + write port. + +Note that in addition to the algorithms implemented in this pass, the $memrd +and $memwr cells are also subject to generic resource sharing passes (and other +optimizations) such as opt_share. +\end{lstlisting} + +\section{memory\_unpack -- unpack multi-port memory cells} +\label{cmd:memory_unpack} +\begin{lstlisting}[numbers=left,frame=single] + memory_unpack [selection] + +This pass converts the multi-port $mem memory cells into individual $memrd and +$memwr cells. It is the counterpart to the memory_collect pass. +\end{lstlisting} + +\section{miter -- automatically create a miter circuit} +\label{cmd:miter} +\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 +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 +detected. + + -ignore_gold_x + a undef (x) bit in the gold module output will match any value in + the gate module output. + + -make_outputs + also route the gold- and gate-outputs to 'gold_*' and 'gate_*' outputs + on the miter circuit. + + -make_outcmp + also create a cmp_* output for each gold/gate output pair. + + -make_assert + also create an 'assert' cell that checks if trigger is always low. + + -flatten + call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit. +\end{lstlisting} + \section{opt -- perform simple optimizations} \label{cmd:opt} \begin{lstlisting}[numbers=left,frame=single] - opt [selection] + opt [options] [selection] 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 + opt_const [-mux_undef] [-mux_bool] [-undriven] [-fine] [-full] [-keepdc] opt_share -nomux do opt_muxtree - opt_reduce + opt_reduce [-fine] [-full] opt_share opt_rmdff - opt_clean - opt_const - while [changed design] + opt_clean [-purge] + opt_const [-mux_undef] [-mux_bool] [-undriven] [-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_rmdff + opt_clean [-purge] + while <changed design in opt_rmdff> + +Note: Options in square brackets (such as [-keepdc]) are passed through to +the opt_* commands when given to 'opt'. \end{lstlisting} \section{opt\_clean -- remove unused cells and wires} @@ -593,9 +1298,30 @@ This pass only operates on completely selected modules without processes. \section{opt\_const -- perform const folding} \label{cmd:opt_const} \begin{lstlisting}[numbers=left,frame=single] - opt_const [selection] + opt_const [options] [selection] This pass performs const folding on internal cell types with constant inputs. + + -mux_undef + remove 'undef' inputs from $mux, $pmux and $_MUX_ cells + + -mux_bool + replace $mux cells with inverters or buffers when possible + + -undriven + replace undriven nets with undef (x) constants + + -fine + perform fine-grain optimizations + + -full + alias for -mux_undef -mux_bool -undriven -fine + + -keepdc + some optimizations change the behavior of the circuit with respect to + don't-care bits. for example in 'a+0' a single x-bit in 'a' will cause + all result bits to be set to x. this behavior changes when 'a+0' is + replaced by 'a'. the -keepdc option disables all such optimizations. \end{lstlisting} \section{opt\_muxtree -- eliminate dead trees in multiplexer trees} @@ -613,7 +1339,7 @@ This pass only operates on completely selected modules without processes. \section{opt\_reduce -- simplify large MUXes and AND/OR gates} \label{cmd:opt_reduce} \begin{lstlisting}[numbers=left,frame=single] - opt_reduce [selection] + opt_reduce [options] [selection] This pass performs two interlinked optimizations: @@ -622,6 +1348,12 @@ duplicated inputs. 2. it identifies duplicated inputs to MUXes and replaces them with a single input with the original control signals OR'ed together. + + -fine + perform fine-grain optimizations + + -full + alias for -fine \end{lstlisting} \section{opt\_rmdff -- remove DFFs with constant inputs} @@ -645,6 +1377,23 @@ are then merged to one cell. Do not merge MUX cells. \end{lstlisting} +\section{plugin -- load and list loaded plugins} +\label{cmd:plugin} +\begin{lstlisting}[numbers=left,frame=single] + plugin [options] + +Load and list loaded plugins. + + -i <plugin_filename> + Load (install) the specified plugin. + + -a <alias_name> + Register the specified alias name for the loaded plugin + + -l + List loaded plugins +\end{lstlisting} + \section{proc -- translate processes to netlists} \label{cmd:proc} \begin{lstlisting}[numbers=left,frame=single] @@ -739,14 +1488,43 @@ Load modules from an ilang file to the current design. (ilang is a text representation of a design in yosys's internal format.) \end{lstlisting} +\section{read\_liberty -- read cells from liberty file} +\label{cmd:read_liberty} +\begin{lstlisting}[numbers=left,frame=single] + read_liberty [filename] + +Read cells from liberty file as modules into current design. + + -lib + only create empty blackbox modules + + -ignore_redef + ignore re-definitions of modules. (the default behavior is to + create an error message.) + + -ignore_miss_func + ignore cells with missing function specification of outputs + + -ignore_miss_dir + ignore cells with a missing or invalid direction + specification on a pin + + -setattr <attribute_name> + set the specified attribute (to the value 1) on all loaded modules +\end{lstlisting} + \section{read\_verilog -- read modules from verilog file} \label{cmd:read_verilog} \begin{lstlisting}[numbers=left,frame=single] - read_verilog [filename] + read_verilog [options] [filename] 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) + -dump_ast1 dump abstract syntax tree (before simplification) @@ -794,10 +1572,21 @@ Verilog-2005 is supported. don't perform basic optimizations (such as const folding) in the high-level front-end. + -icells + interpret cell types starting with '$' as internal cell types + -ignore_redef ignore re-definitions of modules. (the default behavior is to create an error message.) + -defer + only read the abstract syntax tree and defer actual compilation + to a later 'hierarchy' command. Useful in cases where the default + parameters of modules yield invalid or not synthesizable code. + + -setattr <attribute_name> + set the specified attribute (to the value 1) on all loaded modules + -Dname[=definition] define the preprocessor symbol 'name' and set its optional value 'definition' @@ -805,6 +1594,14 @@ Verilog-2005 is supported. -Idir add 'dir' to the directories which are used when searching include files + +The command 'verilog_defaults' can be used to register default options for +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 +the syntax of the code, rather than to rely on read_verilog for that. \end{lstlisting} \section{rename -- rename object in the design} @@ -816,10 +1613,17 @@ Rename the specified object. Note that selection patterns are not supported by this command. - rename -enumerate [selection] + rename -enumerate [-pattern <pattern>] [selection] Assign short auto-generated names to all selected wires and cells with private -names. +names. The -pattern option can be used to set the pattern for the new names. +The character % in the pattern is replaced with a integer number. The default +pattern is '_%_'. + + rename -hide [selection] + +Assign private names (the ones with $-prefix) to all selected wires and cells +with public names. This ignores all selected ports. \end{lstlisting} \section{sat -- solve a SAT problem in the circuit} @@ -864,9 +1668,15 @@ and additional constraints passed as parameters. show the model for the specified signal. if no -show option is passed then a set of signals to be shown is automatically selected. + -show-inputs, -show-outputs, -show-ports + add all module (input/output) ports to the list of shown signals + -ignore_div_by_zero ignore all solutions that involve a division by zero + -ignore_unknown_cells + ignore all cells that can not be matched to a SAT model + The following options can be used to set up a sequential problem: -seq <N> @@ -889,21 +1699,50 @@ The following options can be used to set up a sequential problem: -set-init-undef set all initial states (not set using -set-init) to undef + -set-init-def + do not force a value for the initial state but do not allow undef + + -set-init-zero + set all initial states (not set using -set-init) to zero + + -dump_vcd <vcd-file-name> + dump SAT model (counter example in proof) to VCD 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. + 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 + proven that the condition holds forever after the number of time steps + specified using -seq. + + -tempinduct-def + Perform a temporal induction proof. Assume an initial state with all + registers set to defined values for the induction step. + -prove <signal> <value> - Attempt to proof that <signal> is always <value>. In a temporal - induction proof it is proven that the condition holds forever after - the number of time steps passed using -seq. + 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. + -prove-asserts + Prove that all asserts in the design hold. + + -prove-skip <N> + Do not enforce the prove-condition for the first <N> time steps. + -maxsteps <N> Set a maximum length for the induction. + -initsteps <N> + Set initial length for the induction. + -timeout <N> Maximum number of seconds a single SAT instance may take. @@ -912,6 +1751,12 @@ is passed, a temporal induction proof is performed. -verify-no-timeout Like -verify but do not return an error for timeouts. + + -falsify + Return an error and stop the synthesis script if the proof succeeds. + + -falsify-no-timeout + Like -falsify but do not return an error for timeouts. \end{lstlisting} \section{scatter -- add additional intermediate nets} @@ -960,15 +1805,24 @@ design. \section{script -- execute commands from script file} \label{cmd:script} \begin{lstlisting}[numbers=left,frame=single] - script <filename> + script <filename> [<from_label>:<to_label>] This command executes the yosys commands in the specified file. + +The 2nd argument can be used to only execute the section of the +file between the specified labels. An empty from label is synonymous +for the beginning of the file and an empty to label is synonymous +for the end of the file. + +If only one label is specified (without ':') then only the block +marked with that label (until the next label) is executed. \end{lstlisting} \section{select -- modify and view the list of selected objects} \label{cmd:select} \begin{lstlisting}[numbers=left,frame=single] - select [ -add | -del | -set <name> ] <selection> + select [ -add | -del | -set <name> ] {-read <filename> | <selection>} + select [ -assert-none | -assert-any ] {-read <filename> | <selection>} select [ -list | -write <filename> | -count | -clear ] select -module <modname> @@ -987,7 +1841,22 @@ described here. -set <name> do not modify the current selection. instead save the new selection - under the given name (see @<name> below). + under the given name (see @<name> below). to save the current selection, + use "select -set <name> %" + + -assert-none + do not modify the current selection. instead assert that the given + selection is empty. i.e. produce an error if any object matching the + selection is found. + + -assert-any + do not modify the current selection. instead assert that the given + selection is non-empty. i.e. produce an error if no object matching + the selection is found. + + -assert-count N + do not modify the current selection. instead assert that the given + selection contains exactly N objects. -list list all objects in the current selection @@ -995,12 +1864,19 @@ described here. -write <filename> like -list but write the output to the specified file + -read <filename> + read the specified file (written by -write) + -count count all objects in the current selection -clear - clear the current selection. this effectively selects the - whole design. + clear the current selection. this effectively selects the whole + design. it also resets the selected module (see -module). use the + command 'select *' to select everything but stay in the current module. + + -none + create an empty selection. the current module is unchanged. -module <modname> limit the current scope to the specified module. @@ -1030,8 +1906,12 @@ Pushing (selecting) object when in -module mode: <obj_pattern> select the specified object(s) from the current module -A <mod_pattern> can be a module name or wildcard expression (*, ?, [..]) -matching module names. +A <mod_pattern> can be a module name, wildcard expression (*, ?, [..]) +matching module names, or one of the following: + + A:<pattern>, A:<pattern>=<pattern> + all modules with an attribute matching the given pattern + in addition to = also <, <=, >=, and > are supported An <obj_pattern> can be an object name, wildcard expression, or one of the following: @@ -1039,6 +1919,12 @@ the following: w:<pattern> all wires with a name matching the given wildcard pattern + i:<pattern>, o:<pattern>, x:<pattern> + all inputs (i:), outputs (o:) or any ports (x:) with matching names + + s:<size>, s:<min>:<max> + all wires with a matching width + m:<pattern> all memories with a name matching the given pattern @@ -1055,7 +1941,11 @@ the following: all objects with an attribute name matching the given pattern a:<pattern>=<pattern> - all objects with a matching attribute name-value-pair + all objects with a matching attribute name-value-pair. + in addition to = also <, <=, >=, and > are supported + + r:<pattern>, r:<pattern>=<pattern> + cells with matching parameters. also with <, <=, >= and >. n:<pattern> all objects with a name matching the given pattern @@ -1084,6 +1974,12 @@ The following actions can be performed on the top sets on the stack: %d pop the top set from the stack and subtract it from the new top + %D + 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 + %x[<num1>|*][.<num2>][:<rule>[:<rule>..]] expand top set <num1> num times according to the specified rules. (i.e. select all cells connected to selected wires and select all @@ -1101,12 +1997,96 @@ The following actions can be performed on the top sets on the stack: %co[<num1>|*][.<num2>][:<rule>[:<rule>..]] simmilar to %x, but only select input (%ci) or output cones (%co) + %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 + modules + + %m + expand top set by selecting all modules that contain selected objects + Example: the following command selects all wires that are connected to a 'GATE' input of a 'SWITCH' cell: select */t:SWITCH %x:+[GATE] */t:SWITCH %d \end{lstlisting} +\section{setattr -- set/unset attributes on objects} +\label{cmd:setattr} +\begin{lstlisting}[numbers=left,frame=single] + setattr [ -mod ] [ -set name value | -unset name ]... [selection] + +Set/unset the given attributes on the selected objects. String values must be +passed in double quotes ("). + +When called with -mod, this command will set and unset attributes on modules +instead of objects within modules. +\end{lstlisting} + +\section{setparam -- set/unset parameters on objects} +\label{cmd:setparam} +\begin{lstlisting}[numbers=left,frame=single] + setparam [ -set name value | -unset name ]... [selection] + +Set/unset the given parameters on the selected cells. String values must be +passed in double quotes ("). +\end{lstlisting} + +\section{setundef -- replace undef values with defined constants} +\label{cmd:setundef} +\begin{lstlisting}[numbers=left,frame=single] + setundef [options] [selection] + +This command replaced undef (x) constants with defined (0/1) constants. + + -undriven + also set undriven nets to constant values + + -zero + replace with bits cleared (0) + + -one + replace with bits set (1) + + -random <seed> + replace with random bits using the specified integer als seed + value for the random number generator. +\end{lstlisting} + +\section{share -- perform sat-based resource sharing} +\label{cmd:share} +\begin{lstlisting}[numbers=left,frame=single] + share [options] [selection] + +This pass merges shareable resources into a single resource. A SAT solver +is used to determine if two resources are share-able. + + -force + Per default the selection of cells that is considered for sharing is + narrowed using a list of cell types. With this option all selected + cells are considered for resource sharing. + + IMPORTANT NOTE: If the -all option is used then no cells with internal + state must be selected! + + -aggressive + Per default some heuristics are used to reduce the number of cells + considered for resource sharing to only large resources. This options + turns this heuristics off, resulting in much more cells being considered + for resource sharing. + + -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 + for resource sharing. + + -limit N + Only perform the first N merges, then stop. This is useful for debugging. +\end{lstlisting} + \section{shell -- enter interactive command mode} \label{cmd:shell} \begin{lstlisting}[numbers=left,frame=single] @@ -1163,19 +2143,32 @@ to a graphics file (usually SVG or PostScript). -prefix <prefix> generate <prefix>.* instead of ~/.yosys_show.* - -color <color> <wire> - assign the specified color to the specified wire. The object can be + -color <color> <object> + assign the specified color to the specified object. The object can be a single selection wildcard expressions or a saved set of objects in the @<name> syntax (see "help select" for details). + -label <text> <object> + assign the specified label text to the specified object. The object can + be a single selection wildcard expressions or a saved set of objects in + the @<name> syntax (see "help select" for details). + -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. + -colorattr <attribute_name> + Use the specified attribute to assign colors. A unique color is + assigned to each unique value of this attribute. + -width 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 + cell parameter) with an asterisk next to the port name. + -stretch stretch the graph so all inputs are on the left side and all outputs (including inout ports) are on the right side. @@ -1189,8 +2182,11 @@ to a graphics file (usually SVG or PostScript). -long do not abbeviate objects with internal ($-prefixed) names -When no <format> is specified, SVG is used. When no <format> and <viewer> is -specified, 'yosys-svgviewer' is used to display the schematic. + -notitle + do not add the module name as graph title to the dot file + +When no <format> is specified, 'dot' is used. When no <format> and <viewer> is +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>. @@ -1210,6 +2206,43 @@ primitives. The following internal cell types are mapped by this pass: $sr, $dff, $dffsr, $adff, $dlatch \end{lstlisting} +\section{splice -- create explicit splicing cells} +\label{cmd:splice} +\begin{lstlisting}[numbers=left,frame=single] + splice [options] [selection] + +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. + + -sel_by_cell + only select the cell ports to rewire by the cell. if the selection + contains a cell, than all cell inputs are rewired, if necessary. + + -sel_by_wire + only select the cell ports to rewire by the wire. if the selection + contains a wire, than all cell ports driven by this wire are wired, + if necessary. + + -sel_any_bit + it is sufficient if the driver of any bit of a cell port is selected. + by default all bits must be selected. + + -no_outputs + do not rewire selected module outputs. + + -port <name> + only rewire cell ports with the specified name. can be used multiple + times. implies -no_output. + + -no_port <name> + do not rewire cell ports with the specified name. can be used multiple + times. can not be combined with -port <name>. + +By default selected output wires and all cell ports of selected cells driven +by selected wires are rewired. +\end{lstlisting} + \section{splitnets -- split up multi-bit nets} \label{cmd:splitnets} \begin{lstlisting}[numbers=left,frame=single] @@ -1217,13 +2250,18 @@ primitives. The following internal cell types are mapped by this pass: This command splits multi-bit nets into single-bit nets. - -format char1[char2] + -format char1[char2[char3]] the first char is inserted between the net name and the bit index, the second char is appended to the netname. e.g. -format () creates net - names like 'mysignal(42)'. the default is '[]'. + names like 'mysignal(42)'. the 3rd character is the range separation + character when creating multi-bit wires. the default is '[]:'. -ports also split module ports. per default only internal signals are split. + + -driver + don't blindly split nets in individual bits. instead look at the driver + and split nets so that no driver drives only part of a net. \end{lstlisting} \section{stat -- print some statistics} @@ -1238,6 +2276,10 @@ design. print design hierarchy with this module as top. if the design is fully selected and a module has the 'top' attribute set, this module is used default value for this option. + + -width + annotate internal cell types with their word width. + e.g. $add_8 for an 8 bit wide $add cell. \end{lstlisting} \section{submod -- moving part of a module to a new submodule} @@ -1263,22 +2305,70 @@ Only objects from one module might be selected. The value of the -name option is used as the value of the 'submod' attribute above. \end{lstlisting} +\section{synth -- generic synthesis script} +\label{cmd:synth} +\begin{lstlisting}[numbers=left,frame=single] + synth [options] + +This command runs the default synthesis script. This command does not operate +on partly selected designs. + + -top <module> + use the specified module as top module (default='top') + + -encfile <file> + passed to 'fsm_recode' via 'fsm' + + -noabc + do not run abc (as if yosys was compiled without ABC support) + + -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>] + + coarse: + proc + opt + wreduce + alumacc + share + opt + fsm + opt -fast + memory -nomap + opt_clean + + fine: + opt -fast -full + memory_map + opt -full + techmap + opt -fast + + abc: + abc -fast + opt -fast +\end{lstlisting} + \section{synth\_xilinx -- synthesis for Xilinx FPGAs} \label{cmd:synth_xilinx} \begin{lstlisting}[numbers=left,frame=single] synth_xilinx [options] This command runs synthesis for Xilinx FPGAs. This command does not operate on -partly selected designs. +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') - -arch <arch> - select architecture. the following architectures are supported: - spartan6 (default), artix7, kintex7, virtex7, zynq7000 - (this parameter is not used by the command at the moment) - -edif <file> write the design to the specified edif file. writing of an output file is omitted if this parameter is not specified. @@ -1288,40 +2378,46 @@ partly selected designs. from label is synonymous to 'begin', and empty to label is synonymous to the end of the command list. + -flatten + flatten design before synthesis + + -retime + run 'abc' with -dff option + The following commands are executed by this synthesis command: begin: + read_verilog -lib +/xilinx/cells_sim.v hierarchy -check -top <top> - coarse: + flatten: (only if -flatten) proc - opt - memory - clean - fsm - opt + flatten + + coarse: + synth -run coarse + dff2dffe + + bram: + memory_bram -rules +/xilinx/brams.txt + techmap -map +/xilinx/brams_map.v fine: - techmap - opt + opt -fast -full + memory_map + opt -full + techmap -map +/techmap.v -map +/xilinx/arith_map.v + opt -fast map_luts: - abc -lut 6 + abc -lut 5:8 [-dff] clean map_cells: - techmap -share_map xilinx/cells.v + techmap -map +/xilinx/cells_map.v clean - clkbuf: - select -set xilinx_clocks <top>/t:FDRE %x:+FDRE[C] <top>/t:FDRE %d - iopadmap -inpad BUFGP O:I @xilinx_clocks - - iobuf: - select -set xilinx_nonclocks <top>/w:* <top>/t:BUFGP %x:+BUFGP[I] %d - iopadmap -outpad OBUF I:O -inpad IBUF O:I @xilinx_nonclocks - edif: write_edif synth.edif \end{lstlisting} @@ -1340,7 +2436,7 @@ command 'proc' is wrapped using the tcl command 'procs' in order to avoid a name collision with the tcl builting command 'proc'. \end{lstlisting} -\section{techmap -- simple technology mapper} +\section{techmap -- generic technology mapper} \label{cmd:techmap} \begin{lstlisting}[numbers=left,frame=single] techmap [-map filename] [selection] @@ -1355,11 +2451,34 @@ file. transforms the internal RTL cells to the internal gate library. + -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. + + -max_iter <number> + only run the specified number of iterations. + + -recursive + instead of the iterative breadth-first algorithm use a recursive + depth-first algorithm. both methods should yield equivialent results, + but may differ in performance. + + -autoproc + Automatically call "proc" on implementations that contain processes. + + -assert + this option will cause techmap to exit with an error if it can't map + a selected cell. only cell types that end on an underscore are accepted + 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 @@ -1372,6 +2491,13 @@ the module name will be used to match the cell. When a module in the map file has the 'techmap_simplemap' attribute set, techmap will use 'simplemap' (see 'help simplemap') to map cells matching the module. +When a module in the map file has the 'techmap_maccmap' attribute set, techmap +will use 'maccmap' (see 'help maccmap') to map cells matching the module. + +When a module in the map file has the 'techmap_wrap' attribute set, techmap +will create a wrapper for the cell and then run the command string that the +attribute is set to on the wrapper module. + All wires in the modules from the map file matching the pattern _TECHMAP_* or *._TECHMAP_* are special wires that are used to pass instructions from the mapping module to the techmap command. At the moment the following special @@ -1396,6 +2522,20 @@ wires are supported: wire to start out as non-constant and evaluate to a constant value during processing of other _TECHMAP_DO_* commands. + A _TECHMAP_DO_* command may start with the special token 'CONSTMAP; '. + in this case techmap will create a copy for each distinct configuration + 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 + parameters described below. + + A _TECHMAP_DO_* command may start with the special token 'RECURSION; '. + then techmap will recursively replace the cells in the module with their + implementation. This is not affected by the -max_iter option. + + It is possible to combine both prefixes to 'RECURSION; CONSTMAP; '. + In addition to this special wires, techmap also supports special parameters in modules in the map file: @@ -1403,21 +2543,70 @@ modules in the map file: When a parameter with this name exists, it will be set to the type name of the cell that matches the module. + _TECHMAP_CONSTMSK_<port-name>_ + _TECHMAP_CONSTVAL_<port-name>_ + When this pair of parameters is available in a module for a port, then + former has a 1-bit for each constant input bit and the latter has the + value for this bit. The unused bits of the latter are set to undef (x). + + _TECHMAP_BITS_CONNMAP_ + _TECHMAP_CONNMAP_<port-name>_ + For an N-bit port, the _TECHMAP_CONNMAP_<port-name>_ parameter, if it + exists, will be set to an N*_TECHMAP_BITS_CONNMAP_ bit vector containing + N words (of _TECHMAP_BITS_CONNMAP_ bits each) that assign each single + bit driver a unique id. The values 0-3 are reserved for 0, 1, x, and z. + This can be used to detect shorted inputs. + When a module in the map file has a parameter where the according cell in the design has a port, the module from the map file is only used if the port in 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. + 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). \end{lstlisting} -\section{write\_autotest -- generate simple test benches} -\label{cmd:write_autotest} +\section{tee -- redirect command output to file} +\label{cmd:tee} \begin{lstlisting}[numbers=left,frame=single] - write_autotest [filename] + tee [-q] [-o logfile|-a logfile] cmd + +Execute the specified command, optionally writing the commands output to the +specified logfile(s). + + -q + Do not print output to the normal destination (console and/or log file) + + -o logfile + Write output to this file, truncate if exists. + + -a logfile + Write output to this file, append if exists. +\end{lstlisting} + +\section{test\_abcloop -- automatically test handling of loops in abc command} +\label{cmd:test_abcloop} +\begin{lstlisting}[numbers=left,frame=single] + test_abcloop [options] + +Test handling of logic loops in ABC. + + -n {integer} + create this number of circuits and test them (default = 100). + + -s {positive_integer} + use this value as rng seed value (default = unix time). +\end{lstlisting} + +\section{test\_autotb -- generate simple test benches} +\label{cmd:test_autotb} +\begin{lstlisting}[numbers=left,frame=single] + test_autotb [options] [filename] Automatically create primitive verilog test benches for all modules in the design. The generated testbenches toggle the input pins of the module in @@ -1433,6 +2622,156 @@ be forced to be interpreted as clock signal by setting the attribute The attribute 'gentb_constant' can be used to force a signal to a constant 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) +\end{lstlisting} + +\section{test\_cell -- automatically test the implementation of a cell type} +\label{cmd:test_cell} +\begin{lstlisting}[numbers=left,frame=single] + test_cell [options] {cell-types} + +Tests the internal implementation of the given cell type (for example '$add') +by comparing SAT solver, EVAL and TECHMAP implementations of the cell types.. + +Run with 'all' instead of a cell type to run the test on all supported +cell types. Use for example 'all /$add' for all cell types except $add. + + -n {integer} + create this number of cell instances and test them (default = 100). + + -s {positive_integer} + use this value as rng seed value (default = unix time). + + -f {ilang_file} + don't generate circuits. instead load the specified ilang file. + + -w {filename_prefix} + don't test anything. just generate the circuits and write them + to ilang files with the specified prefix + + -map {filename} + pass this option to techmap. + + -simlib + use "techmap -map +/simlib.v -max_iter 2 -autoproc" + + -muxdiv + when creating test benches with dividers, create an additional mux + to mask out the division-by-zero case + + -script {script_file} + instead of calling "techmap", call "script {script_file}". + + -const + set some input bits to random constant values + + -nosat + do not check SAT model or run SAT equivalence checking + + -v + print additional debug information to the console + + -vlog {filename} + create a verilog test bench to test simlib and write_verilog +\end{lstlisting} + +\section{trace -- redirect command output to file} +\label{cmd:trace} +\begin{lstlisting}[numbers=left,frame=single] + trace cmd + +Execute the specified command, logging all changes the command performs on +the design in real time. +\end{lstlisting} + +\section{verific -- load Verilog and VHDL designs using Verific} +\label{cmd:verific} +\begin{lstlisting}[numbers=left,frame=single] + verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv} <verilog-file>.. + +Load the specified Verilog/SystemVerilog files into Verific. + + + verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008} <vhdl-file>.. + +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 +reset the internal state of Verific. A gate-level netlist is created +when called with -gates. + +Visit http://verific.com/ for more information on Verific. +\end{lstlisting} + +\section{verilog\_defaults -- set default options for read\_verilog} +\label{cmd:verilog_defaults} +\begin{lstlisting}[numbers=left,frame=single] + verilog_defaults -add [options] + +Add the sepcified options to the list of default options to read_verilog. + + + verilog_defaults -clear +Clear the list of verilog default options. + + + verilog_defaults -push verilog_defaults -pop +Push or pop the list of default options to a stack. Note that -push does +not imply -clear. +\end{lstlisting} + +\section{vhdl2verilog -- importing VHDL designs using vhdl2verilog} +\label{cmd:vhdl2verilog} +\begin{lstlisting}[numbers=left,frame=single] + vhdl2verilog [options] <vhdl-file>.. + +This command reads VHDL source files using the 'vhdl2verilog' tool and the +Yosys Verilog frontend. + + -out <out_file> + do not import the vhdl2verilog output. instead write it to the + specified file. + + -vhdl2verilog_dir <directory> + do use the specified vhdl2verilog installation. this is the directory + that contains the setup_env.sh file. when this option is not present, + it is assumed that vhdl2verilog is in the PATH environment variable. + + -top <top-entity-name> + The name of the top entity. This option is mandatory. + +The following options are passed as-is to vhdl2verilog: + + -arch <architecture_name> + -unroll_generate + -nogenericeval + -nouniquify + -oldparser + -suppress <list> + -quiet + -nobanner + -mapfile <file> + +vhdl2verilog can be obtained from: +http://www.edautils.com/vhdl2verilog.html +\end{lstlisting} + +\section{wreduce -- reduce the word size of operations is possible} +\label{cmd:wreduce} +\begin{lstlisting}[numbers=left,frame=single] + wreduce [options] [selection] + +This command reduces the word size of operations. For example it will replace +the 32 bit adders in the following code with adders of more appropriate widths: + + module test(input [3:0] a, b, c, output [7:0] y); + assign y = a + b + c + 1; + endmodule \end{lstlisting} \section{write\_blif -- write design to BLIF file} @@ -1448,24 +2787,50 @@ Write the current design to an BLIF file. -buf <cell-type> <in-port> <out-port> use cells of type <cell-type> with the specified port names for buffers + -unbuf <cell-type> <in-port> <out-port> + replace buffer cells with the specified name and port names with + a .names statement that models a buffer + -true <cell-type> <out-port> -false <cell-type> <out-port> - use the specified cell types to drive nets that are constant 1 or 0 + -undef <cell-type> <out-port> + use the specified cell types to drive nets that are constant 1, 0, or + undefined. when '-' is used as <cell-type>, then <out-port> specifies + the wire name to be used for the constant signal and no cell driving + that wire is generated. The following options can be useful when the generated file is not going to be read by a BLIF parser but a custom tool. It is recommended to not name the output file *.blif when any of this options is used. - -subckt + -icells do not translate Yosys's internal gates to generic BLIF logic - functions. Instead create .subckt lines for all cells. + functions. Instead create .subckt or .gate lines for all cells. + + -gates + print .gate instead of .subckt lines for all cells that are not + instantiations of other modules from this design. -conn do not generate buffers for connected wires. instead use the non-standard .conn statement. + -param + use the non-standard .param statement to write module parameters + + -blackbox + write blackbox cells with .blackbox statement. + -impltf - do not write definitions for the $true and $false wires. + do not write definitions for the $true, $false and $undef wires. +\end{lstlisting} + +\section{write\_btor -- write design to BTOR file} +\label{cmd:write_btor} +\begin{lstlisting}[numbers=left,frame=single] + write_btor [filename] + +Write the current design to an BTOR file. \end{lstlisting} \section{write\_edif -- write design to EDIF netlist file} @@ -1484,6 +2849,24 @@ necessary to make small modifications to this command when a different tool is targeted. \end{lstlisting} +\section{write\_file -- write a text to a file} +\label{cmd:write_file} +\begin{lstlisting}[numbers=left,frame=single] + write_file [options] output_file [input_file] + +Write the text fron the input file to the output file. + + -a + Append to output file (instead of overwriting) + + +Inside a script the input file can also can a here-document: + + write_file hello.txt <<EOT + Hello World! + EOT +\end{lstlisting} + \section{write\_ilang -- write design to ilang file} \label{cmd:write_ilang} \begin{lstlisting}[numbers=left,frame=single] @@ -1520,6 +2903,83 @@ a tool for Coarse-Grain Example-Driven Interconnect Synthesis. http://www.clifford.at/intersynth/ \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). + +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. +Only ports, and signals with the 'keep' attribute set are made available via +such functions. Without the -bv option, multi-bit wires are exported as +separate functions of type Bool for the individual bits. With the -bv option +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. + + -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. + + -tpl <template_file> + use the given template file. the line containing only the token '%%' + is replaced with the regular output of this command. + +[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David +R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf + +--------------------------------------------------------------------------- + +Example: + +Consider the following module (test.v). We want to prove that the output can +never transition from a non-zero value to a zero value. + + module test(input clk, output reg [3:0] y); + always @(posedge clk) + y <= (y << 1) | ^y; + endmodule + +For this proof we create the following template (test.tpl). + + ; we need QF_UFBV for this poof + (set-logic QF_UFBV) + + ; insert the auto-generated code here + %% + + ; declare two state variables s1 and s2 + (declare-fun s1 () test_s) + (declare-fun s2 () test_s) + + ; state s2 is the successor of state s1 + (assert (test_t s1 s2)) + + ; we are looking for a model with y non-zero in s1 + (assert (distinct (|test_n y| s1) #b0000)) + + ; we are looking for a model with y zero in s2 + (assert (= (|test_n y| s2) #b0000)) + + ; is there such a model? + (check-sat) + +The following yosys script will create a 'test.smt2' file for our proof: + + read_verilog test.v + hierarchy; proc; techmap; opt -fast + 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\_spice -- write design to SPICE netlist file} \label{cmd:write_spice} \begin{lstlisting}[numbers=left,frame=single] diff --git a/manual/manual.tex b/manual/manual.tex index 19d3b7b2..84be86e5 100644 --- a/manual/manual.tex +++ b/manual/manual.tex @@ -61,6 +61,7 @@ bookmarksopen=false% \usepackage{multibib} \usepackage{multirow} \usepackage{booktabs} +\usepackage{pdfpages} \usepackage{listings} \usepackage{pifont} @@ -202,7 +203,7 @@ YOSYS & Yosys Open SYnthesis Suite \\ \include{CHAPTER_Verilog} \include{CHAPTER_Optimize} \include{CHAPTER_Techmap} -\include{CHAPTER_Eval} +% \include{CHAPTER_Eval} \appendix @@ -214,7 +215,7 @@ YOSYS & Yosys Open SYnthesis Suite \\ \input{command-reference-manual} \include{CHAPTER_Appnotes} -\include{CHAPTER_StateOfTheArt} +% \include{CHAPTER_StateOfTheArt} \bibliography{literature} \bibliographystyle{alphadin} diff --git a/manual/presentation.sh b/manual/presentation.sh index 980e1772..ca8a6c93 100755 --- a/manual/presentation.sh +++ b/manual/presentation.sh @@ -24,8 +24,10 @@ done PDFTEX_OPT="-shell-escape -halt-on-error" +set -ex + if ! $fast_mode; then - md5sum *.aux *.snm *.nav *.toc > autoloop.old + ! md5sum *.aux *.snm *.nav *.toc > autoloop.old make -C PRESENTATION_Intro make -C PRESENTATION_ExSyn make -C PRESENTATION_ExAdv diff --git a/manual/presentation.tex b/manual/presentation.tex index 9a876de0..dc512775 100644 --- a/manual/presentation.tex +++ b/manual/presentation.tex @@ -74,7 +74,7 @@ {\usebeamerfont{subsection name}\usebeamercolor[fg]{subsection name}of \sectionname~\insertsectionnumber} \vskip1em\par \setbeamercolor{graybox}{bg=gray} -\begin{beamercolorbox}[sep=8pt,center,bg=gray]{graybox} +\begin{beamercolorbox}[sep=8pt,center]{graybox} \usebeamerfont{subsection title}\insertsection\par \end{beamercolorbox} \end{centering}} @@ -133,7 +133,7 @@ I like writing open source software. For example: \item OpenSCAD (now maintained by Marius Kintel) \item SPL (a not very popular scripting language) \item EmbedVM (a very simple compiler+vm for 8 bit micros) -\item Lib(X)SVF (a library to play SVF/XSVF files over JTAG, used at LHC) +\item Lib(X)SVF (a library to play SVF/XSVF files over JTAG) \item ROCK Linux (discontinued since 2010) \end{itemize} \end{frame} |