From a14dec79ebc85fae807684fa027d8098a16a4d34 Mon Sep 17 00:00:00 2001 From: KrystalDelusion <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 16 Nov 2022 00:55:22 +1300 Subject: Rst docs conversion (#3496) Rst docs conversion --- docs/.gitignore | 10 + docs/Makefile | 226 +++++ docs/images/011/example_out.tex | 18 + docs/images/011/select_prod.tex | 19 + docs/images/011/splitnets_libfile.tex | 15 + docs/images/011/submod_dots.tex | 27 + docs/images/Makefile | 44 + docs/images/approach_flow.png | Bin 0 -> 9709 bytes docs/images/approach_flow.tex | 38 + docs/images/basics_abstractions.png | Bin 0 -> 29158 bytes docs/images/basics_abstractions.tex | 41 + docs/images/basics_ast.png | Bin 0 -> 9478 bytes docs/images/basics_ast.tex | 30 + docs/images/basics_flow.png | Bin 0 -> 12540 bytes docs/images/basics_flow.tex | 44 + docs/images/basics_parsetree.png | Bin 0 -> 23196 bytes docs/images/basics_parsetree.tex | 44 + docs/images/overview_flow.png | Bin 0 -> 17668 bytes docs/images/overview_flow.tex | 37 + docs/images/overview_rtlil.png | Bin 0 -> 16034 bytes docs/images/overview_rtlil.tex | 27 + docs/images/verilog_flow.png | Bin 0 -> 15934 bytes docs/images/verilog_flow.tex | 67 ++ docs/source/CHAPTER_Approach.rst | 141 +++ docs/source/CHAPTER_Basics.rst | 776 +++++++++++++++ docs/source/CHAPTER_CellLib.rst | 1020 ++++++++++++++++++++ docs/source/CHAPTER_Eval.rst | 233 +++++ docs/source/CHAPTER_Intro.rst | 96 ++ docs/source/CHAPTER_Optimize.rst | 330 +++++++ docs/source/CHAPTER_Overview.rst | 571 +++++++++++ docs/source/CHAPTER_Prog.rst | 46 + docs/source/CHAPTER_Techmap.rst | 105 ++ docs/source/CHAPTER_Verilog.rst | 666 +++++++++++++ .../appendix/APPNOTE_010_Verilog_to_BLIF.rst | 336 +++++++ .../appendix/APPNOTE_011_Design_Investigation.rst | 965 ++++++++++++++++++ .../appendix/APPNOTE_012_Verilog_to_BTOR.rst | 333 +++++++ docs/source/appendix/CHAPTER_Auxlibs.rst | 42 + docs/source/appendix/CHAPTER_Auxprogs.rst | 29 + docs/source/appendix/CHAPTER_StateOfTheArt.rst | 410 ++++++++ docs/source/appendix/CHAPTER_TextRtlil.rst | 298 ++++++ docs/source/bib.rst | 9 + docs/source/cmd_ref.rst | 11 + docs/source/conf.py | 62 ++ docs/source/index.rst | 72 ++ docs/source/literature.bib | 202 ++++ docs/source/requirements.txt | 2 + docs/static/custom.css | 1 + docs/static/favico.png | Bin 0 -> 33435 bytes docs/static/logo.png | Bin 0 -> 15938 bytes docs/static/yosyshq.css | 78 ++ docs/util/RtlilLexer.py | 45 + docs/util/YoscryptLexer.py | 73 ++ 52 files changed, 7639 insertions(+) create mode 100644 docs/.gitignore create mode 100644 docs/Makefile create mode 100644 docs/images/011/example_out.tex create mode 100644 docs/images/011/select_prod.tex create mode 100644 docs/images/011/splitnets_libfile.tex create mode 100644 docs/images/011/submod_dots.tex create mode 100644 docs/images/Makefile create mode 100644 docs/images/approach_flow.png create mode 100644 docs/images/approach_flow.tex create mode 100644 docs/images/basics_abstractions.png create mode 100644 docs/images/basics_abstractions.tex create mode 100644 docs/images/basics_ast.png create mode 100644 docs/images/basics_ast.tex create mode 100644 docs/images/basics_flow.png create mode 100644 docs/images/basics_flow.tex create mode 100644 docs/images/basics_parsetree.png create mode 100644 docs/images/basics_parsetree.tex create mode 100644 docs/images/overview_flow.png create mode 100644 docs/images/overview_flow.tex create mode 100644 docs/images/overview_rtlil.png create mode 100644 docs/images/overview_rtlil.tex create mode 100644 docs/images/verilog_flow.png create mode 100644 docs/images/verilog_flow.tex create mode 100644 docs/source/CHAPTER_Approach.rst create mode 100644 docs/source/CHAPTER_Basics.rst create mode 100644 docs/source/CHAPTER_CellLib.rst create mode 100644 docs/source/CHAPTER_Eval.rst create mode 100644 docs/source/CHAPTER_Intro.rst create mode 100644 docs/source/CHAPTER_Optimize.rst create mode 100644 docs/source/CHAPTER_Overview.rst create mode 100644 docs/source/CHAPTER_Prog.rst create mode 100644 docs/source/CHAPTER_Techmap.rst create mode 100644 docs/source/CHAPTER_Verilog.rst create mode 100644 docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst create mode 100644 docs/source/appendix/APPNOTE_011_Design_Investigation.rst create mode 100644 docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst create mode 100644 docs/source/appendix/CHAPTER_Auxlibs.rst create mode 100644 docs/source/appendix/CHAPTER_Auxprogs.rst create mode 100644 docs/source/appendix/CHAPTER_StateOfTheArt.rst create mode 100644 docs/source/appendix/CHAPTER_TextRtlil.rst create mode 100644 docs/source/bib.rst create mode 100644 docs/source/cmd_ref.rst create mode 100644 docs/source/conf.py create mode 100644 docs/source/index.rst create mode 100644 docs/source/literature.bib create mode 100644 docs/source/requirements.txt create mode 100644 docs/static/custom.css create mode 100644 docs/static/favico.png create mode 100644 docs/static/logo.png create mode 100644 docs/static/yosyshq.css create mode 100644 docs/util/RtlilLexer.py create mode 100644 docs/util/YoscryptLexer.py (limited to 'docs') diff --git a/docs/.gitignore b/docs/.gitignore new file mode 100644 index 000000000..26645e4cb --- /dev/null +++ b/docs/.gitignore @@ -0,0 +1,10 @@ +/build/ +/source/cmd +/images/*.log +/images/*.aux +/images/*.pdf +/images/*.svg +/images/011/*.log +/images/011/*.aux +/images/011/*.pdf +/images/011/*.svg diff --git a/docs/Makefile b/docs/Makefile new file mode 100644 index 000000000..2319e1665 --- /dev/null +++ b/docs/Makefile @@ -0,0 +1,226 @@ +# Makefile for Sphinx documentation +# + +# You can set these variables from the command line. +SPHINXOPTS = +SPHINXBUILD = sphinx-build +PAPER = +BUILDDIR = build + +# Internal variables. +PAPEROPT_a4 = -D latex_paper_size=a4 +PAPEROPT_letter = -D latex_paper_size=letter +ALLSPHINXOPTS = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) source +# the i18n builder cannot share the environment and doctrees with the others +I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) source + +.PHONY: help +help: + @echo "Please use \`make ' where is one of" + @echo " html to make standalone HTML files" + @echo " dirhtml to make HTML files named index.html in directories" + @echo " singlehtml to make a single large HTML file" + @echo " pickle to make pickle files" + @echo " json to make JSON files" + @echo " htmlhelp to make HTML files and a HTML help project" + @echo " qthelp to make HTML files and a qthelp project" + @echo " applehelp to make an Apple Help Book" + @echo " devhelp to make HTML files and a Devhelp project" + @echo " epub to make an epub" + @echo " epub3 to make an epub3" + @echo " latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter" + @echo " latexpdf to make LaTeX files and run them through pdflatex" + @echo " latexpdfja to make LaTeX files and run them through platex/dvipdfmx" + @echo " text to make text files" + @echo " man to make manual pages" + @echo " texinfo to make Texinfo files" + @echo " info to make Texinfo files and run them through makeinfo" + @echo " gettext to make PO message catalogs" + @echo " changes to make an overview of all changed/added/deprecated items" + @echo " xml to make Docutils-native XML files" + @echo " pseudoxml to make pseudoxml-XML files for display purposes" + @echo " linkcheck to check all external links for integrity" + @echo " doctest to run all doctests embedded in the documentation (if enabled)" + @echo " coverage to run coverage check of the documentation (if enabled)" + @echo " dummy to check syntax errors of document sources" + +.PHONY: clean +clean: + rm -rf $(BUILDDIR)/* + +.PHONY: html +html: + $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html + @echo + @echo "Build finished. The HTML pages are in $(BUILDDIR)/html." + +.PHONY: dirhtml +dirhtml: + $(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml + @echo + @echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml." + +# singlehtml section links are broken +.PHONY: singlehtml +singlehtml: + $(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/singlehtml + @echo + @echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml." + +.PHONY: pickle +pickle: + $(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle + @echo + @echo "Build finished; now you can process the pickle files." + +.PHONY: json +json: + $(SPHINXBUILD) -b json $(ALLSPHINXOPTS) $(BUILDDIR)/json + @echo + @echo "Build finished; now you can process the JSON files." + +.PHONY: htmlhelp +htmlhelp: + $(SPHINXBUILD) -b htmlhelp $(ALLSPHINXOPTS) $(BUILDDIR)/htmlhelp + @echo + @echo "Build finished; now you can run HTML Help Workshop with the" \ + ".hhp project file in $(BUILDDIR)/htmlhelp." + +.PHONY: qthelp +qthelp: + $(SPHINXBUILD) -b qthelp $(ALLSPHINXOPTS) $(BUILDDIR)/qthelp + @echo + @echo "Build finished; now you can run "qcollectiongenerator" with the" \ + ".qhcp project file in $(BUILDDIR)/qthelp, like this:" + @echo "# qcollectiongenerator $(BUILDDIR)/qthelp/SymbiYosys.qhcp" + @echo "To view the help file:" + @echo "# assistant -collectionFile $(BUILDDIR)/qthelp/SymbiYosys.qhc" + +.PHONY: applehelp +applehelp: + $(SPHINXBUILD) -b applehelp $(ALLSPHINXOPTS) $(BUILDDIR)/applehelp + @echo + @echo "Build finished. The help book is in $(BUILDDIR)/applehelp." + @echo "N.B. You won't be able to view it unless you put it in" \ + "~/Library/Documentation/Help or install it in your application" \ + "bundle." + +.PHONY: devhelp +devhelp: + $(SPHINXBUILD) -b devhelp $(ALLSPHINXOPTS) $(BUILDDIR)/devhelp + @echo + @echo "Build finished." + @echo "To view the help file:" + @echo "# mkdir -p $$HOME/.local/share/devhelp/SymbiYosys" + @echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/SymbiYosys" + @echo "# devhelp" + +.PHONY: epub +epub: + $(SPHINXBUILD) -b epub $(ALLSPHINXOPTS) $(BUILDDIR)/epub + @echo + @echo "Build finished. The epub file is in $(BUILDDIR)/epub." + +.PHONY: epub3 +epub3: + $(SPHINXBUILD) -b epub3 $(ALLSPHINXOPTS) $(BUILDDIR)/epub3 + @echo + @echo "Build finished. The epub3 file is in $(BUILDDIR)/epub3." + +.PHONY: latex +latex: + $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex + @echo + @echo "Build finished; the LaTeX files are in $(BUILDDIR)/latex." + @echo "Run \`make' in that directory to run these through (pdf)latex" \ + "(use \`make latexpdf' here to do that automatically)." + +.PHONY: latexpdf +latexpdf: + $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex + @echo "Running LaTeX files through pdflatex..." + $(MAKE) -C $(BUILDDIR)/latex all-pdf + @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex." + +.PHONY: latexpdfja +latexpdfja: + $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex + @echo "Running LaTeX files through platex and dvipdfmx..." + $(MAKE) -C $(BUILDDIR)/latex all-pdf-ja + @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex." + +.PHONY: text +text: + $(SPHINXBUILD) -b text $(ALLSPHINXOPTS) $(BUILDDIR)/text + @echo + @echo "Build finished. The text files are in $(BUILDDIR)/text." + +.PHONY: man +man: + $(SPHINXBUILD) -b man $(ALLSPHINXOPTS) $(BUILDDIR)/man + @echo + @echo "Build finished. The manual pages are in $(BUILDDIR)/man." + +.PHONY: texinfo +texinfo: + $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo + @echo + @echo "Build finished. The Texinfo files are in $(BUILDDIR)/texinfo." + @echo "Run \`make' in that directory to run these through makeinfo" \ + "(use \`make info' here to do that automatically)." + +.PHONY: info +info: + $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo + @echo "Running Texinfo files through makeinfo..." + make -C $(BUILDDIR)/texinfo info + @echo "makeinfo finished; the Info files are in $(BUILDDIR)/texinfo." + +.PHONY: gettext +gettext: + $(SPHINXBUILD) -b gettext $(I18NSPHINXOPTS) $(BUILDDIR)/locale + @echo + @echo "Build finished. The message catalogs are in $(BUILDDIR)/locale." + +.PHONY: changes +changes: + $(SPHINXBUILD) -b changes $(ALLSPHINXOPTS) $(BUILDDIR)/changes + @echo + @echo "The overview file is in $(BUILDDIR)/changes." + +.PHONY: linkcheck +linkcheck: + $(SPHINXBUILD) -b linkcheck $(ALLSPHINXOPTS) $(BUILDDIR)/linkcheck + @echo + @echo "Link check complete; look for any errors in the above output " \ + "or in $(BUILDDIR)/linkcheck/output.txt." + +.PHONY: doctest +doctest: + $(SPHINXBUILD) -b doctest $(ALLSPHINXOPTS) $(BUILDDIR)/doctest + @echo "Testing of doctests in the sources finished, look at the " \ + "results in $(BUILDDIR)/doctest/output.txt." + +.PHONY: coverage +coverage: + $(SPHINXBUILD) -b coverage $(ALLSPHINXOPTS) $(BUILDDIR)/coverage + @echo "Testing of coverage in the sources finished, look at the " \ + "results in $(BUILDDIR)/coverage/python.txt." + +.PHONY: xml +xml: + $(SPHINXBUILD) -b xml $(ALLSPHINXOPTS) $(BUILDDIR)/xml + @echo + @echo "Build finished. The XML files are in $(BUILDDIR)/xml." + +.PHONY: pseudoxml +pseudoxml: + $(SPHINXBUILD) -b pseudoxml $(ALLSPHINXOPTS) $(BUILDDIR)/pseudoxml + @echo + @echo "Build finished. The pseudo-XML files are in $(BUILDDIR)/pseudoxml." + +.PHONY: dummy +dummy: + $(SPHINXBUILD) -b dummy $(ALLSPHINXOPTS) $(BUILDDIR)/dummy + @echo + @echo "Build finished. Dummy builder generates no files." diff --git a/docs/images/011/example_out.tex b/docs/images/011/example_out.tex new file mode 100644 index 000000000..831b036e9 --- /dev/null +++ b/docs/images/011/example_out.tex @@ -0,0 +1,18 @@ +\documentclass[12pt,tikz]{standalone} +\pdfinfoomitdate 1 +\pdfsuppressptexinfo 1 +\pdftrailerid{} +\usepackage[utf8]{inputenc} +\usepackage{tikz} +\pagestyle{empty} + +\begin{document} +\begin{tikzpicture} + \node[inner sep=0pt] at (0,0) + {\includegraphics[width=\linewidth]{example_00.pdf}}; + \node[inner sep=0pt] at (0,-3.8) + {\includegraphics[width=\linewidth]{example_01.pdf}}; + \node[inner sep=0pt] at (0,-7) + {\includegraphics[width=\linewidth]{example_02.pdf}}; +\end{tikzpicture} +\end{document} diff --git a/docs/images/011/select_prod.tex b/docs/images/011/select_prod.tex new file mode 100644 index 000000000..c4a3c6e37 --- /dev/null +++ b/docs/images/011/select_prod.tex @@ -0,0 +1,19 @@ +\documentclass[12pt,tikz]{standalone} +\pdfinfoomitdate 1 +\pdfsuppressptexinfo 1 +\pdftrailerid{} +\usepackage[utf8]{inputenc} +\pagestyle{empty} + +\begin{document} +\begin{tikzpicture} + \node[inner sep=0pt] at (0,0) + {\hfill \includegraphics[width=4cm,trim=0 1cm 0 1cm]{sumprod_02.pdf}}; + \node[inner sep=0pt] at (0,-2.8) + {\includegraphics[width=\linewidth,trim=0 0cm 0 1cm]{sumprod_03.pdf}}; + \node[inner sep=0pt] at (0,-6.2) + {\includegraphics[width=\linewidth,trim=0 0cm 0 1cm]{sumprod_04.pdf}}; + \node[inner sep=0pt] at (0,-9.2) + {\includegraphics[width=\linewidth,trim=0 1cm 0 1cm]{sumprod_05.pdf}}; +\end{tikzpicture} +\end{document} diff --git a/docs/images/011/splitnets_libfile.tex b/docs/images/011/splitnets_libfile.tex new file mode 100644 index 000000000..9669ef841 --- /dev/null +++ b/docs/images/011/splitnets_libfile.tex @@ -0,0 +1,15 @@ +\documentclass[12pt,tikz]{standalone} +\pdfinfoomitdate 1 +\pdfsuppressptexinfo 1 +\pdftrailerid{} +\usepackage[utf8]{inputenc} +\pagestyle{empty} + +\begin{document} +\begin{tikzpicture} + \node[inner sep=0pt] at (0,0) + {\includegraphics[height=\linewidth]{cmos_00.pdf}}; + \node[inner sep=0pt] at (2,-8) + {\includegraphics[width=\linewidth]{cmos_01.pdf}}; +\end{tikzpicture} +\end{document} diff --git a/docs/images/011/submod_dots.tex b/docs/images/011/submod_dots.tex new file mode 100644 index 000000000..3d48b46e5 --- /dev/null +++ b/docs/images/011/submod_dots.tex @@ -0,0 +1,27 @@ +\documentclass[12pt,tikz]{standalone} +\pdfinfoomitdate 1 +\pdfsuppressptexinfo 1 +\pdftrailerid{} +\usepackage[utf8]{inputenc} +\pagestyle{empty} + +\begin{document} +\begin{tikzpicture} + \node[inner sep=0pt] at (0,0) + {\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{submod_00.pdf}}; + \node at (0, -2.5) + {\tt memdemo}; + \node[inner sep=0pt] at (0,-5) + {\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{submod_01.pdf}}; + \node at (0, -7.5) + {\tt scramble}; + \node[inner sep=0pt] at (0, -11) + {\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{submod_02.pdf}}; + \node at (0, -14.8) + {\tt outstage}; + \node[inner sep=0pt] at (0,-16.6) + {\includegraphics[width=\linewidth,trim=0 1.3cm 0 0cm]{submod_03.pdf}}; + \node at (0, -19) + {\tt selstage}; +\end{tikzpicture} +\end{document} diff --git a/docs/images/Makefile b/docs/images/Makefile new file mode 100644 index 000000000..b62f6c7f6 --- /dev/null +++ b/docs/images/Makefile @@ -0,0 +1,44 @@ +all: dots tex svg tidy + +TEX_SOURCE:= $(wildcard *.tex) +DOT_LOC:= ../../manual/APPNOTE_011_Design_Investigation +DOT_SOURCE:= $(wildcard $(DOT_LOC)/*.dot) + +TEX_SOURCE+= 011/example_out.tex +011/example_out.pdf: 011/example_00.pdf 011/example_01.pdf 011/example_02.pdf +TEX_SOURCE+= 011/select_prod.tex +011/select_prod.pdf: 011/sumprod_02.pdf 011/sumprod_03.pdf 011/sumprod_04.pdf 011/sumprod_05.pdf +TEX_SOURCE+= 011/splitnets_libfile.tex +011/splitnets_libfile.pdf: 011/cmos_00.pdf 011/cmos_01.pdf +TEX_SOURCE+= 011/submod_dots.tex +011/submod_dots.pdf: 011/submod_00.pdf 011/submod_01.pdf 011/submod_02.pdf 011/submod_03.pdf + +TEX_PDF:= $(patsubst %.tex,%.pdf,$(TEX_SOURCE)) +DOT_PDF:= $(addprefix 011/,$(notdir $(patsubst %.dot,%.pdf,$(DOT_SOURCE)))) +SVG_OUTPUT:= $(patsubst %.pdf,%.svg,$(TEX_PDF) $(DOT_PDF)) + +dots: $(DOT_PDF) +tex: $(TEX_PDF) +svg: $(SVG_OUTPUT) + +011/%.pdf: $(DOT_LOC)/%.dot + dot -Tpdf -o $@ $< + +011/%.pdf: 011/%.tex + cd 011 && pdflatex $(] (cursor) -- node[above] {Low-Level} ++(3,0); + +\end{tikzpicture} +\end{document} diff --git a/docs/images/basics_abstractions.png b/docs/images/basics_abstractions.png new file mode 100644 index 000000000..a735fbd3b Binary files /dev/null and b/docs/images/basics_abstractions.png differ diff --git a/docs/images/basics_abstractions.tex b/docs/images/basics_abstractions.tex new file mode 100644 index 000000000..ece063623 --- /dev/null +++ b/docs/images/basics_abstractions.tex @@ -0,0 +1,41 @@ +\documentclass[12pt,tikz]{standalone} +\pdfinfoomitdate 1 +\pdfsuppressptexinfo 1 +\pdftrailerid{} +\usepackage[utf8]{inputenc} +\usepackage{amsmath} +\usepackage{pgfplots} +\usepackage{tikz} +\pagestyle{empty} + +\begin{document} +\begin{tikzpicture} + \tikzstyle{lvl} = [draw, fill=green!10, rectangle, minimum height=2em, minimum width=15em] + \node[lvl] (sys) {System Level}; + \node[lvl] (hl) [below of=sys] {High Level}; + \node[lvl] (beh) [below of=hl] {Behavioral Level}; + \node[lvl] (rtl) [below of=beh] {Register-Transfer Level (RTL)}; + \node[lvl] (lg) [below of=rtl] {Logical Gate Level}; + \node[lvl] (pg) [below of=lg] {Physical Gate Level}; + \node[lvl] (sw) [below of=pg] {Switch Level}; + + \draw[dotted] (sys.east) -- ++(1,0) coordinate (sysx); + \draw[dotted] (hl.east) -- ++(1,0) coordinate (hlx); + \draw[dotted] (beh.east) -- ++(1,0) coordinate (behx); + \draw[dotted] (rtl.east) -- ++(1,0) coordinate (rtlx); + \draw[dotted] (lg.east) -- ++(1,0) coordinate (lgx); + \draw[dotted] (pg.east) -- ++(1,0) coordinate (pgx); + \draw[dotted] (sw.east) -- ++(1,0) coordinate (swx); + + \draw[gray,|->] (sysx) -- node[right] {System Design} (hlx); + \draw[|->|] (hlx) -- node[right] {High Level Synthesis (HLS)} (behx); + \draw[->|] (behx) -- node[right] {Behavioral Synthesis} (rtlx); + \draw[->|] (rtlx) -- node[right] {RTL Synthesis} (lgx); + \draw[->|] (lgx) -- node[right] {Logic Synthesis} (pgx); + \draw[gray,->|] (pgx) -- node[right] {Cell Library} (swx); + + \draw[dotted] (behx) -- ++(5,0) coordinate (a); + \draw[dotted] (pgx) -- ++(5,0) coordinate (b); + \draw[|->|] (a) -- node[right] {Yosys} (b); +\end{tikzpicture} +\end{document} diff --git a/docs/images/basics_ast.png b/docs/images/basics_ast.png new file mode 100644 index 000000000..c2d95c844 Binary files /dev/null and b/docs/images/basics_ast.png differ diff --git a/docs/images/basics_ast.tex b/docs/images/basics_ast.tex new file mode 100644 index 000000000..dac6a8d47 --- /dev/null +++ b/docs/images/basics_ast.tex @@ -0,0 +1,30 @@ +\documentclass[12pt,tikz]{standalone} +\pdfinfoomitdate 1 +\pdfsuppressptexinfo 1 +\pdftrailerid{} +\usepackage[utf8]{inputenc} +\usepackage{amsmath} +\usepackage{pgfplots} +\usepackage{tikz} +\usetikzlibrary{shapes.geometric} +\pagestyle{empty} + +\begin{document} +\begin{tikzpicture} + \tikzstyle{node} = [draw, fill=green!10, ellipse, minimum height=2em, minimum width=8em, node distance=10em] + + \draw (+0,+0) node[node] (n1) {\tt ASSIGN}; + + \draw (-2,-2) node[node] (n11) {\tt ID: foo}; + \draw (+2,-2) node[node] (n12) {\tt PLUS}; + + \draw (+0,-4) node[node] (n121) {\tt ID: bar}; + \draw (+4,-4) node[node] (n122) {\tt CONST: 42}; + + \draw[-latex] (n1) -- (n11); + \draw[-latex] (n1) -- (n12); + + \draw[-latex] (n12) -- (n121); + \draw[-latex] (n12) -- (n122); +\end{tikzpicture} +\end{document} diff --git a/docs/images/basics_flow.png b/docs/images/basics_flow.png new file mode 100644 index 000000000..a027b5eac Binary files /dev/null and b/docs/images/basics_flow.png differ diff --git a/docs/images/basics_flow.tex b/docs/images/basics_flow.tex new file mode 100644 index 000000000..53b555487 --- /dev/null +++ b/docs/images/basics_flow.tex @@ -0,0 +1,44 @@ +\documentclass[12pt,tikz]{standalone} +\pdfinfoomitdate 1 +\pdfsuppressptexinfo 1 +\pdftrailerid{} +\usepackage[utf8]{inputenc} +\usepackage{amsmath} +\usepackage{pgfplots} +\usepackage{tikz} +\pagestyle{empty} + +\begin{document} +\begin{tikzpicture} + \tikzstyle{manual} = [draw, fill=green!10, rectangle, minimum height=2em, minimum width=8em, node distance=10em] + \tikzstyle{auto} = [draw, fill=orange!10, rectangle, minimum height=2em, minimum width=8em, node distance=10em] + + \node[manual] (sys) {\begin{minipage}{8em} + \center + System Level \\ + Model + \end{minipage}}; + \node[manual] (beh) [right of=sys] {\begin{minipage}{8em} + \center + Behavioral \\ + Model + \end{minipage}}; + \node[auto] (rtl) [right of=beh] {\begin{minipage}{8em} + \center + RTL \\ + Model + \end{minipage}}; + \node[auto] (gates) [right of=rtl] {\begin{minipage}{8em} + \center + Gate-Level \\ + Model + \end{minipage}}; + + \draw[-latex] (beh) edge[double, bend left] node[above] {synthesis} (rtl); + \draw[-latex] (rtl) edge[double, bend left] node[above] {synthesis} (gates); + + \draw[latex-latex] (sys) edge[bend right] node[below] {verify} (beh); + \draw[latex-latex] (beh) edge[bend right] node[below] {verify} (rtl); + \draw[latex-latex] (rtl) edge[bend right] node[below] {verify} (gates); +\end{tikzpicture} +\end{document} diff --git a/docs/images/basics_parsetree.png b/docs/images/basics_parsetree.png new file mode 100644 index 000000000..ff7a17e2b Binary files /dev/null and b/docs/images/basics_parsetree.png differ diff --git a/docs/images/basics_parsetree.tex b/docs/images/basics_parsetree.tex new file mode 100644 index 000000000..1c8392b88 --- /dev/null +++ b/docs/images/basics_parsetree.tex @@ -0,0 +1,44 @@ +\documentclass[12pt,tikz]{standalone} +\pdfinfoomitdate 1 +\pdfsuppressptexinfo 1 +\pdftrailerid{} +\usepackage[utf8]{inputenc} +\usepackage{amsmath} +\usepackage{pgfplots} +\usepackage{tikz} +\usetikzlibrary{shapes.geometric} +\pagestyle{empty} + +\begin{document} +\begin{tikzpicture} + \tikzstyle{node} = [draw, fill=green!10, ellipse, minimum height=2em, minimum width=8em, node distance=10em] + + \draw (+0,+1) node[node] (n1) {\tt assign\_stmt}; + + \draw (-6,-1) node[node] (n11) {\tt TOK\_ASSIGN}; + \draw (-3,-2) node[node] (n12) {\tt TOK\_IDENTIFIER}; + \draw (+0,-1) node[node] (n13) {\tt TOK\_EQ}; + \draw (+3,-2) node[node] (n14) {\tt expr}; + \draw (+6,-1) node[node] (n15) {\tt TOK\_SEMICOLON}; + + \draw (-1,-4) node[node] (n141) {\tt expr}; + \draw (+3,-4) node[node] (n142) {\tt TOK\_PLUS}; + \draw (+7,-4) node[node] (n143) {\tt expr}; + + \draw (-1,-5.5) node[node] (n1411) {\tt TOK\_IDENTIFIER}; + \draw (+7,-5.5) node[node] (n1431) {\tt TOK\_NUMBER}; + + \draw[-latex] (n1) -- (n11); + \draw[-latex] (n1) -- (n12); + \draw[-latex] (n1) -- (n13); + \draw[-latex] (n1) -- (n14); + \draw[-latex] (n1) -- (n15); + + \draw[-latex] (n14) -- (n141); + \draw[-latex] (n14) -- (n142); + \draw[-latex] (n14) -- (n143); + + \draw[-latex] (n141) -- (n1411); + \draw[-latex] (n143) -- (n1431); +\end{tikzpicture} +\end{document} diff --git a/docs/images/overview_flow.png b/docs/images/overview_flow.png new file mode 100644 index 000000000..c1b13a000 Binary files /dev/null and b/docs/images/overview_flow.png differ diff --git a/docs/images/overview_flow.tex b/docs/images/overview_flow.tex new file mode 100644 index 000000000..ac0afde5f --- /dev/null +++ b/docs/images/overview_flow.tex @@ -0,0 +1,37 @@ +\documentclass[12pt,tikz]{standalone} +\pdfinfoomitdate 1 +\pdfsuppressptexinfo 1 +\pdftrailerid{} +\usepackage[utf8]{inputenc} +\usepackage{amsmath} +\usepackage{pgfplots} +\usepackage{tikz} +\usetikzlibrary{shapes.geometric} +\pagestyle{empty} + +\begin{document} +\begin{tikzpicture} + \tikzstyle{process} = [draw, fill=green!10, rectangle, minimum height=3em, minimum width=10em, node distance=15em] + \tikzstyle{data} = [draw, fill=blue!10, ellipse, minimum height=3em, minimum width=7em, node distance=15em] + \node[process] (vlog) {Verilog Frontend}; + \node[process, dashed, fill=green!5] (vhdl) [right of=vlog] {VHDL Frontend}; + \node[process] (ilang) [right of=vhdl] {RTLIL Frontend}; + \node[data] (ast) [below of=vlog, node distance=5em, xshift=7.5em] {AST}; + \node[process] (astfe) [below of=ast, node distance=5em] {AST Frontend}; + \node[data] (rtlil) [below of=astfe, node distance=5em, xshift=7.5em] {RTLIL}; + \node[process] (pass) [right of=rtlil, node distance=5em, xshift=7.5em] {Passes}; + \node[process] (vlbe) [below of=rtlil, node distance=7em, xshift=-13em] {Verilog Backend}; + \node[process] (ilangbe) [below of=rtlil, node distance=7em, xshift=0em] {RTLIL Backend}; + \node[process, dashed, fill=green!5] (otherbe) [below of=rtlil, node distance=7em, xshift=+13em] {Other Backends}; + + \draw[-latex] (vlog) -- (ast); + \draw[-latex] (vhdl) -- (ast); + \draw[-latex] (ast) -- (astfe); + \draw[-latex] (astfe) -- (rtlil); + \draw[-latex] (ilang) -- (rtlil); + \draw[latex-latex] (rtlil) -- (pass); + \draw[-latex] (rtlil) -- (vlbe); + \draw[-latex] (rtlil) -- (ilangbe); + \draw[-latex] (rtlil) -- (otherbe); +\end{tikzpicture} +\end{document} diff --git a/docs/images/overview_rtlil.png b/docs/images/overview_rtlil.png new file mode 100644 index 000000000..f79c667e8 Binary files /dev/null and b/docs/images/overview_rtlil.png differ diff --git a/docs/images/overview_rtlil.tex b/docs/images/overview_rtlil.tex new file mode 100644 index 000000000..ddacbff00 --- /dev/null +++ b/docs/images/overview_rtlil.tex @@ -0,0 +1,27 @@ +\documentclass[12pt,tikz]{standalone} +\pdfinfoomitdate 1 +\pdfsuppressptexinfo 1 +\pdftrailerid{} +\usepackage[utf8]{inputenc} +\usepackage{amsmath} +\usepackage{pgfplots} +\usepackage{tikz} +\pagestyle{empty} + +\begin{document} +\begin{tikzpicture} + \tikzstyle{entity} = [draw, fill=gray!10, rectangle, minimum height=3em, minimum width=7em, node distance=5em, font={\ttfamily}] + \node[entity] (design) {RTLIL::Design}; + \node[entity] (module) [right of=design, node distance=11em] {RTLIL::Module} edge [-latex] node[above] {\tiny 1 \hskip3em N} (design); + + \node[entity] (process) [fill=green!10, right of=module, node distance=10em] {RTLIL::Process} (process.west) edge [-latex] (module); + \node[entity] (memory) [fill=red!10, below of=process] {RTLIL::Memory} edge [-latex] (module); + \node[entity] (wire) [fill=blue!10, above of=process] {RTLIL::Wire} (wire.west) edge [-latex] (module); + \node[entity] (cell) [fill=blue!10, above of=wire] {RTLIL::Cell} (cell.west) edge [-latex] (module); + + \node[entity] (case) [fill=green!10, right of=process, node distance=10em] {RTLIL::CaseRule} edge [latex-latex] (process); + \node[entity] (sync) [fill=green!10, above of=case] {RTLIL::SyncRule} edge [-latex] (process); + \node[entity] (switch) [fill=green!10, below of=case] {RTLIL::SwitchRule} edge [-latex] (case); + \draw[latex-] (switch.east) -- ++(1em,0) |- (case.east); +\end{tikzpicture} +\end{document} diff --git a/docs/images/verilog_flow.png b/docs/images/verilog_flow.png new file mode 100644 index 000000000..1f3d82780 Binary files /dev/null and b/docs/images/verilog_flow.png differ diff --git a/docs/images/verilog_flow.tex b/docs/images/verilog_flow.tex new file mode 100644 index 000000000..d3e269d0d --- /dev/null +++ b/docs/images/verilog_flow.tex @@ -0,0 +1,67 @@ +\documentclass[12pt,tikz]{standalone} +\pdfinfoomitdate 1 +\pdfsuppressptexinfo 1 +\pdftrailerid{} +\usepackage[utf8]{inputenc} +\usepackage{amsmath} +\usepackage{pgfplots} +\usepackage{tikz} +\usetikzlibrary{shapes.geometric} +\pagestyle{empty} + +\begin{document} +\begin{tikzpicture} + \tikzstyle{process} = [draw, fill=green!10, rectangle, minimum height=3em, minimum width=10em, node distance=5em, font={\ttfamily}] + \tikzstyle{data} = [draw, fill=blue!10, ellipse, minimum height=3em, minimum width=7em, node distance=5em, font={\ttfamily}] + + \node[data] (n1) {Verilog Source}; + \node[process] (n2) [below of=n1] {Verilog Frontend}; + \node[data] (n3) [below of=n2] {AST}; + \node[process] (n4) [below of=n3] {AST Frontend}; + \node[data] (n5) [below of=n4] {RTLIL}; + + \draw[-latex] (n1) -- (n2); + \draw[-latex] (n2) -- (n3); + \draw[-latex] (n3) -- (n4); + \draw[-latex] (n4) -- (n5); + + \tikzstyle{details} = [draw, fill=yellow!5, rectangle, node distance=6cm, font={\ttfamily}] + + \node[details] (d1) [right of=n2] {\begin{minipage}{5cm} + \hfil + \begin{tikzpicture} + \tikzstyle{subproc} = [draw, fill=green!10, rectangle, minimum height=2em, minimum width=10em, node distance=3em, font={\ttfamily}] + \node (s0) {}; + \node[subproc] (s1) [below of=s0] {Preprocessor}; + \node[subproc] (s2) [below of=s1] {Lexer}; + \node[subproc] (s3) [below of=s2] {Parser}; + \node[node distance=3em] (s4) [below of=s3] {}; + \draw[-latex] (s0) -- (s1); + \draw[-latex] (s1) -- (s2); + \draw[-latex] (s2) -- (s3); + \draw[-latex] (s3) -- (s4); + \end{tikzpicture} + \end{minipage}}; + + \draw[dashed] (n2.north east) -- (d1.north west); + \draw[dashed] (n2.south east) -- (d1.south west); + + \node[details] (d2) [right of=n4] {\begin{minipage}{5cm} + \hfil + \begin{tikzpicture} + \tikzstyle{subproc} = [draw, fill=green!10, rectangle, minimum height=2em, minimum width=10em, node distance=3em, font={\ttfamily}] + \node (s0) {}; + \node[subproc] (s1) [below of=s0] {Simplifier}; + \node[subproc] (s2) [below of=s1] {RTLIL Generator}; + \node[node distance=3em] (s3) [below of=s2] {}; + \draw[-latex] (s0) -- (s1); + \draw[-latex] (s1) -- (s2); + \draw[-latex] (s2) -- (s3); + \end{tikzpicture} + \end{minipage}}; + + \draw[dashed] (n4.north east) -- (d2.north west); + \draw[dashed] (n4.south east) -- (d2.south west); + +\end{tikzpicture} +\end{document} diff --git a/docs/source/CHAPTER_Approach.rst b/docs/source/CHAPTER_Approach.rst new file mode 100644 index 000000000..32980e788 --- /dev/null +++ b/docs/source/CHAPTER_Approach.rst @@ -0,0 +1,141 @@ +.. _chapter:approach: + +Approach +======== + +Yosys is a tool for synthesising (behavioural) Verilog HDL code to target +architecture netlists. Yosys aims at a wide range of application domains and +thus must be flexible and easy to adapt to new tasks. This chapter covers the +general approach followed in the effort to implement this tool. + +Data- and control-flow +---------------------- + +The data- and control-flow of a typical synthesis tool is very similar to the +data- and control-flow of a typical compiler: different subsystems are called in +a predetermined order, each consuming the data generated by the last subsystem +and generating the data for the next subsystem (see :numref:`Fig. %s +`). + +.. figure:: ../images/approach_flow.* + :class: width-helper + :name: fig:approach_flow + + General data- and control-flow of a synthesis tool + +The first subsystem to be called is usually called a frontend. It does not +process the data generated by another subsystem but instead reads the user +input—in the case of a HDL synthesis tool, the behavioural HDL code. + +The subsystems that consume data from previous subsystems and produce data for +the next subsystems (usually in the same or a similar format) are called passes. + +The last subsystem that is executed transforms the data generated by the last +pass into a suitable output format and writes it to a disk file. This subsystem +is usually called the backend. + +In Yosys all frontends, passes and backends are directly available as commands +in the synthesis script. Thus the user can easily create a custom synthesis flow +just by calling passes in the right order in a synthesis script. + +Internal formats in Yosys +------------------------- + +Yosys uses two different internal formats. The first is used to store an +abstract syntax tree (AST) of a Verilog input file. This format is simply called +AST and is generated by the Verilog Frontend. This data structure is consumed by +a subsystem called AST Frontend [1]_. This AST Frontend then generates a design +in Yosys' main internal format, the +Register-Transfer-Level-Intermediate-Language (RTLIL) representation. It does +that by first performing a number of simplifications within the AST +representation and then generating RTLIL from the simplified AST data structure. + +The RTLIL representation is used by all passes as input and outputs. This has +the following advantages over using different representational formats between +different passes: + +- The passes can be rearranged in a different order and passes can be removed + or inserted. + +- Passes can simply pass-thru the parts of the design they don't change without + the need to convert between formats. In fact Yosys passes output the same + data structure they received as input and performs all changes in place. + +- All passes use the same interface, thus reducing the effort required to + understand a pass when reading the Yosys source code, e.g. when adding + additional features. + +The RTLIL representation is basically a netlist representation with the +following additional features: + +- An internal cell library with fixed-function cells to represent RTL datapath + and register cells as well as logical gate-level cells (single-bit gates and + registers). + +- Support for multi-bit values that can use individual bits from wires as well + as constant bits to represent coarse-grain netlists. + +- Support for basic behavioural constructs (if-then-else structures and + multi-case switches with a sensitivity list for updating the outputs). + +- Support for multi-port memories. + +The use of RTLIL also has the disadvantage of having a very powerful format +between all passes, even when doing gate-level synthesis where the more advanced +features are not needed. In order to reduce complexity for passes that operate +on a low-level representation, these passes check the features used in the input +RTLIL and fail to run when unsupported high-level constructs are used. In such +cases a pass that transforms the higher-level constructs to lower-level +constructs must be called from the synthesis script first. + +.. _sec:typusecase: + +Typical use case +---------------- + +The following example script may be used in a synthesis flow to convert the +behavioural Verilog code from the input file design.v to a gate-level netlist +synth.v using the cell library described by the Liberty file : + +.. code:: yoscrypt + :number-lines: + + # read input file to internal representation + read_verilog design.v + + # convert high-level behavioral parts ("processes") to d-type flip-flops and muxes + proc + + # perform some simple optimizations + opt + + # convert high-level memory constructs to d-type flip-flops and multiplexers + memory + + # perform some simple optimizations + opt + + # convert design to (logical) gate-level netlists + techmap + + # perform some simple optimizations + opt + + # map internal register types to the ones from the cell library + dfflibmap -liberty cells.lib + + # use ABC to map remaining logic to cells from the cell library + abc -liberty cells.lib + + # cleanup + opt + + # write results to output file + write_verilog synth.v + +A detailed description of the commands available in Yosys can be found in +:ref:`cmd_ref`. + +.. [1] + In Yosys the term pass is only used to refer to commands that operate on the + RTLIL data structure. diff --git a/docs/source/CHAPTER_Basics.rst b/docs/source/CHAPTER_Basics.rst new file mode 100644 index 000000000..618bec545 --- /dev/null +++ b/docs/source/CHAPTER_Basics.rst @@ -0,0 +1,776 @@ +.. role:: verilog(code) + :language: Verilog + +.. _chapter:basics: + +Basic principles +================ + +This chapter contains a short introduction to the basic principles of digital +circuit synthesis. + +Levels of abstraction +--------------------- + +Digital circuits can be represented at different levels of abstraction. During +the design process a circuit is usually first specified using a higher level +abstraction. Implementation can then be understood as finding a functionally +equivalent representation at a lower abstraction level. When this is done +automatically using software, the term synthesis is used. + +So synthesis is the automatic conversion of a high-level representation of a +circuit to a functionally equivalent low-level representation of a circuit. +:numref:`Figure %s ` lists the different levels of +abstraction and how they relate to different kinds of synthesis. + +.. figure:: ../images/basics_abstractions.* + :class: width-helper + :name: fig:Basics_abstractions + + Different levels of abstraction and synthesis. + +Regardless of the way a lower level representation of a circuit is obtained +(synthesis or manual design), the lower level representation is usually verified +by comparing simulation results of the lower level and the higher level +representation [1]_. Therefore even if no synthesis is used, there must still +be a simulatable representation of the circuit in all levels to allow for +verification of the design. + +Note: The exact meaning of terminology such as "High-Level" is of course not +fixed over time. For example the HDL "ABEL" was first introduced in 1985 as "A +High-Level Design Language for Programmable Logic Devices" :cite:p:`ABEL`, but +would not be considered a "High-Level Language" today. + +System level +~~~~~~~~~~~~ + +The System Level abstraction of a system only looks at its biggest building +blocks like CPUs and computing cores. At this level the circuit is usually +described using traditional programming languages like C/C++ or Matlab. +Sometimes special software libraries are used that are aimed at simulation +circuits on the system level, such as SystemC. + +Usually no synthesis tools are used to automatically transform a system level +representation of a circuit to a lower-level representation. But system level +design tools exist that can be used to connect system level building blocks. + +The IEEE 1685-2009 standard defines the IP-XACT file format that can be used to +represent designs on the system level and building blocks that can be used in +such system level designs. :cite:p:`IP-XACT` + +High level +~~~~~~~~~~ + +The high-level abstraction of a system (sometimes referred to as algorithmic +level) is also often represented using traditional programming languages, but +with a reduced feature set. For example when representing a design at the high +level abstraction in C, pointers can only be used to mimic concepts that can be +found in hardware, such as memory interfaces. Full featured dynamic memory +management is not allowed as it has no corresponding concept in digital +circuits. + +Tools exist to synthesize high level code (usually in the form of C/C++/SystemC +code with additional metadata) to behavioural HDL code (usually in the form of +Verilog or VHDL code). Aside from the many commercial tools for high level +synthesis there are also a number of FOSS tools for high level synthesis . + +Behavioural level +~~~~~~~~~~~~~~~~~ + +At the behavioural abstraction level a language aimed at hardware description +such as Verilog or VHDL is used to describe the circuit, but so-called +behavioural modelling is used in at least part of the circuit description. In +behavioural modelling there must be a language feature that allows for +imperative programming to be used to describe data paths and registers. This is +the always-block in Verilog and the process-block in VHDL. + +In behavioural modelling, code fragments are provided together with a +sensitivity list; a list of signals and conditions. In simulation, the code +fragment is executed whenever a signal in the sensitivity list changes its value +or a condition in the sensitivity list is triggered. A synthesis tool must be +able to transfer this representation into an appropriate datapath followed by +the appropriate types of register. + +For example consider the following Verilog code fragment: + +.. code:: verilog + :number-lines: + + always @(posedge clk) + y <= a + b; + +In simulation the statement ``y <= a + b`` is executed whenever a positive edge +on the signal ``clk`` is detected. The synthesis result however will contain an +adder that calculates the sum ``a + b`` all the time, followed by a d-type +flip-flop with the adder output on its D-input and the signal ``y`` on its +Q-output. + +Usually the imperative code fragments used in behavioural modelling can contain +statements for conditional execution (``if``- and ``case``-statements in +Verilog) as well as loops, as long as those loops can be completely unrolled. + +Interestingly there seems to be no other FOSS Tool that is capable of performing +Verilog or VHDL behavioural syntheses besides Yosys. + +Register-Transfer Level (RTL) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +On the Register-Transfer Level the design is represented by combinatorial data +paths and registers (usually d-type flip flops). The following Verilog code +fragment is equivalent to the previous Verilog example, but is in RTL +representation: + +.. code:: verilog + :number-lines: + + assign tmp = a + b; // combinatorial data path + + always @(posedge clk) // register + y <= tmp; + +A design in RTL representation is usually stored using HDLs like Verilog and +VHDL. But only a very limited subset of features is used, namely minimalistic +always-blocks (Verilog) or process-blocks (VHDL) that model the register type +used and unconditional assignments for the datapath logic. The use of HDLs on +this level simplifies simulation as no additional tools are required to simulate +a design in RTL representation. + +Many optimizations and analyses can be performed best at the RTL level. Examples +include FSM detection and optimization, identification of memories or other +larger building blocks and identification of shareable resources. + +Note that RTL is the first abstraction level in which the circuit is represented +as a graph of circuit elements (registers and combinatorial cells) and signals. +Such a graph, when encoded as list of cells and connections, is called a +netlist. + +RTL synthesis is easy as each circuit node element in the netlist can simply be +replaced with an equivalent gate-level circuit. However, usually the term RTL +synthesis does not only refer to synthesizing an RTL netlist to a gate level +netlist but also to performing a number of highly sophisticated optimizations +within the RTL representation, such as the examples listed above. + +A number of FOSS tools exist that can perform isolated tasks within the domain +of RTL synthesis steps. But there seems to be no FOSS tool that covers a wide +range of RTL synthesis operations. + +Logical gate level +~~~~~~~~~~~~~~~~~~ + +At the logical gate level the design is represented by a netlist that uses only +cells from a small number of single-bit cells, such as basic logic gates (AND, +OR, NOT, XOR, etc.) and registers (usually D-Type Flip-flops). + +A number of netlist formats exists that can be used on this level, e.g. the +Electronic Design Interchange Format (EDIF), but for ease of simulation often a +HDL netlist is used. The latter is a HDL file (Verilog or VHDL) that only uses +the most basic language constructs for instantiation and connecting of cells. + +There are two challenges in logic synthesis: First finding opportunities for +optimizations within the gate level netlist and second the optimal (or at least +good) mapping of the logic gate netlist to an equivalent netlist of physically +available gate types. + +The simplest approach to logic synthesis is two-level logic synthesis, where a +logic function is converted into a sum-of-products representation, e.g. using a +Karnaugh map. This is a simple approach, but has exponential worst-case effort +and cannot make efficient use of physical gates other than AND/NAND-, OR/NOR- +and NOT-Gates. + +Therefore modern logic synthesis tools utilize much more complicated multi-level +logic synthesis algorithms :cite:p:`MultiLevelLogicSynth`. Most of these +algorithms convert the logic function to a Binary-Decision-Diagram (BDD) or +And-Inverter-Graph (AIG) and work from that representation. The former has the +advantage that it has a unique normalized form. The latter has much better worst +case performance and is therefore better suited for the synthesis of large logic +functions. + +Good FOSS tools exists for multi-level logic synthesis . + +Yosys contains basic logic synthesis functionality but can also use ABC for the +logic synthesis step. Using ABC is recommended. + +Physical gate level +~~~~~~~~~~~~~~~~~~~ + +On the physical gate level only gates are used that are physically available on +the target architecture. In some cases this may only be NAND, NOR and NOT gates +as well as D-Type registers. In other cases this might include cells that are +more complex than the cells used at the logical gate level (e.g. complete +half-adders). In the case of an FPGA-based design the physical gate level +representation is a netlist of LUTs with optional output registers, as these are +the basic building blocks of FPGA logic cells. + +For the synthesis tool chain this abstraction is usually the lowest level. In +case of an ASIC-based design the cell library might contain further information +on how the physical cells map to individual switches (transistors). + +Switch level +~~~~~~~~~~~~ + +A switch level representation of a circuit is a netlist utilizing single +transistors as cells. Switch level modelling is possible in Verilog and VHDL, +but is seldom used in modern designs, as in modern digital ASIC or FPGA flows +the physical gates are considered the atomic build blocks of the logic circuit. + +Yosys +~~~~~ + +Yosys is a Verilog HDL synthesis tool. This means that it takes a behavioural +design description as input and generates an RTL, logical gate or physical gate +level description of the design as output. Yosys' main strengths are behavioural +and RTL synthesis. A wide range of commands (synthesis passes) exist within +Yosys that can be used to perform a wide range of synthesis tasks within the +domain of behavioural, rtl and logic synthesis. Yosys is designed to be +extensible and therefore is a good basis for implementing custom synthesis tools +for specialised tasks. + +Features of synthesizable Verilog +--------------------------------- + +The subset of Verilog :cite:p:`Verilog2005` that is synthesizable is specified +in a separate IEEE standards document, the IEEE standard 1364.1-2002 +:cite:p:`VerilogSynth`. This standard also describes how certain language +constructs are to be interpreted in the scope of synthesis. + +This section provides a quick overview of the most important features of +synthesizable Verilog, structured in order of increasing complexity. + +Structural Verilog +~~~~~~~~~~~~~~~~~~ + +Structural Verilog (also known as Verilog Netlists) is a Netlist in Verilog +syntax. Only the following language constructs are used in this +case: + +- Constant values +- Wire and port declarations +- Static assignments of signals to other signals +- Cell instantiations + +Many tools (especially at the back end of the synthesis chain) only support +structural Verilog as input. ABC is an example of such a tool. Unfortunately +there is no standard specifying what Structural Verilog actually is, leading to +some confusion about what syntax constructs are supported in structural Verilog +when it comes to features such as attributes or multi-bit signals. + +Expressions in Verilog +~~~~~~~~~~~~~~~~~~~~~~ + +In all situations where Verilog accepts a constant value or signal name, +expressions using arithmetic operations such as ``+``, ``-`` and ``*``, boolean +operations such as ``&`` (AND), ``|`` (OR) and ``^`` (XOR) and many others +(comparison operations, unary operator, etc.) can also be used. + +During synthesis these operators are replaced by cells that implement the +respective function. + +Many FOSS tools that claim to be able to process Verilog in fact only support +basic structural Verilog and simple expressions. Yosys can be used to convert +full featured synthesizable Verilog to this simpler subset, thus enabling such +applications to be used with a richer set of Verilog features. + +Behavioural modelling +~~~~~~~~~~~~~~~~~~~~~ + +Code that utilizes the Verilog always statement is using Behavioural Modelling. +In behavioural modelling, a circuit is described by means of imperative program +code that is executed on certain events, namely any change, a rising edge, or a +falling edge of a signal. This is a very flexible construct during simulation +but is only synthesizable when one +of the following is modelled: + +- | **Asynchronous or latched logic** + | In this case the sensitivity list must contain all expressions that + are used within the always block. The syntax ``@*`` can be used for + these cases. Examples of this kind include: + + .. code:: verilog + :number-lines: + + // asynchronous + always @* begin + if (add_mode) + y <= a + b; + else + y <= a - b; + end + + // latched + always @* begin + if (!hold) + y <= a + b; + end + + Note that latched logic is often considered bad style and in many + cases just the result of sloppy HDL design. Therefore many synthesis + tools generate warnings whenever latched logic is generated. + +- | **Synchronous logic (with optional synchronous reset)** + | This is logic with d-type flip-flops on the output. In this case + the sensitivity list must only contain the respective clock edge. + Example: + + .. code:: verilog + :number-lines: + + // counter with synchronous reset + always @(posedge clk) begin + if (reset) + y <= 0; + else + y <= y + 1; + end + +- | **Synchronous logic with asynchronous reset** + | This is logic with d-type flip-flops with asynchronous resets on + the output. In this case the sensitivity list must only contain the + respective clock and reset edges. The values assigned in the reset + branch must be constant. Example: + + .. code:: verilog + :number-lines: + + // counter with asynchronous reset + always @(posedge clk, posedge reset) begin + if (reset) + y <= 0; + else + y <= y + 1; + end + +Many synthesis tools support a wider subset of flip-flops that can be modelled +using always-statements (including Yosys). But only the ones listed above are +covered by the Verilog synthesis standard and when writing new designs one +should limit herself or himself to these cases. + +In behavioural modelling, blocking assignments (=) and non-blocking assignments +(<=) can be used. The concept of blocking vs. non-blocking assignment is one of +the most misunderstood constructs in Verilog :cite:p:`Cummings00`. + +The blocking assignment behaves exactly like an assignment in any imperative +programming language, while with the non-blocking assignment the right hand side +of the assignment is evaluated immediately but the actual update of the left +hand side register is delayed until the end of the time-step. For example the +Verilog code ``a <= b; b <= a;`` exchanges the values of the two registers. + + +Functions and tasks +~~~~~~~~~~~~~~~~~~~ + +Verilog supports Functions and Tasks to bundle statements that are used in +multiple places (similar to Procedures in imperative programming). Both +constructs can be implemented easily by substituting the function/task-call with +the body of the function or task. + +Conditionals, loops and generate-statements +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Verilog supports ``if-else``-statements and ``for``-loops inside +``always``-statements. + +It also supports both features in ``generate``-statements on the module level. +This can be used to selectively enable or disable parts of the module based on +the module parameters (``if-else``) or to generate a set of similar subcircuits +(``for``). + +While the ``if-else``-statement inside an always-block is part of behavioural +modelling, the three other cases are (at least for a synthesis tool) part of a +built-in macro processor. Therefore it must be possible for the synthesis tool +to completely unroll all loops and evaluate the condition in all +``if-else``-statement in ``generate``-statements using const-folding.. + +Arrays and memories +~~~~~~~~~~~~~~~~~~~ + +Verilog supports arrays. This is in general a synthesizable language feature. In +most cases arrays can be synthesized by generating addressable memories. +However, when complex or asynchronous access patterns are used, it is not +possible to model an array as memory. In these cases the array must be modelled +using individual signals for each word and all accesses to the array must be +implemented using large multiplexers. + +In some cases it would be possible to model an array using memories, but it is +not desired. Consider the following delay circuit: + +.. code:: verilog + :number-lines: + + module (clk, in_data, out_data); + + parameter BITS = 8; + parameter STAGES = 4; + + input clk; + input [BITS-1:0] in_data; + output [BITS-1:0] out_data; + reg [BITS-1:0] ffs [STAGES-1:0]; + + integer i; + always @(posedge clk) begin + ffs[0] <= in_data; + for (i = 1; i < STAGES; i = i+1) + ffs[i] <= ffs[i-1]; + end + + assign out_data = ffs[STAGES-1]; + + endmodule + +This could be implemented using an addressable memory with STAGES input and +output ports. A better implementation would be to use a simple chain of +flip-flops (a so-called shift register). This better implementation can either +be obtained by first creating a memory-based implementation and then optimizing +it based on the static address signals for all ports or directly identifying +such situations in the language front end and converting all memory accesses to +direct accesses to the correct signals. + +Challenges in digital circuit synthesis +--------------------------------------- + +This section summarizes the most important challenges in digital circuit +synthesis. Tools can be characterized by how well they address these topics. + +Standards compliance +~~~~~~~~~~~~~~~~~~~~ + +The most important challenge is compliance with the HDL standards in question +(in case of Verilog the IEEE Standards 1364.1-2002 and 1364-2005). This can be +broken down in two items: + +- Completeness of implementation of the standard +- Correctness of implementation of the standard + +Completeness is mostly important to guarantee compatibility with existing HDL +code. Once a design has been verified and tested, HDL designers are very +reluctant regarding changes to the design, even if it is only about a few minor +changes to work around a missing feature in a new synthesis tool. + +Correctness is crucial. In some areas this is obvious (such as correct synthesis +of basic behavioural models). But it is also crucial for the areas that concern +minor details of the standard, such as the exact rules for handling signed +expressions, even when the HDL code does not target different synthesis tools. +This is because (unlike software source code that is only processed by +compilers), in most design flows HDL code is not only processed by the synthesis +tool but also by one or more simulators and sometimes even a formal verification +tool. It is key for this verification process that all these tools use the same +interpretation for the HDL code. + +Optimizations +~~~~~~~~~~~~~ + +Generally it is hard to give a one-dimensional description of how well a +synthesis tool optimizes the design. First of all because not all optimizations +are applicable to all designs and all synthesis tasks. Some optimizations work +(best) on a coarse-grained level (with complex cells such as adders or +multipliers) and others work (best) on a fine-grained level (single bit gates). +Some optimizations target area and others target speed. Some work well on large +designs while others don't scale well and can only be applied to small designs. + +A good tool is capable of applying a wide range of optimizations at different +levels of abstraction and gives the designer control over which optimizations +are performed (or skipped) and what the optimization goals are. + +Technology mapping +~~~~~~~~~~~~~~~~~~ + +Technology mapping is the process of converting the design into a netlist of +cells that are available in the target architecture. In an ASIC flow this might +be the process-specific cell library provided by the fab. In an FPGA flow this +might be LUT cells as well as special function units such as dedicated +multipliers. In a coarse-grain flow this might even be more complex special +function units. + +An open and vendor independent tool is especially of interest if it supports a +wide range of different types of target architectures. + +Script-based synthesis flows +---------------------------- + +A digital design is usually started by implementing a high-level or system-level +simulation of the desired function. This description is then manually +transformed (or re-implemented) into a synthesizable lower-level description +(usually at the behavioural level) and the equivalence of the two +representations is verified by simulating both and comparing the simulation +results. + +Then the synthesizable description is transformed to lower-level representations +using a series of tools and the results are again verified using simulation. +This process is illustrated in :numref:`Fig. %s `. + +.. figure:: ../images/basics_flow.* + :class: width-helper + :name: fig:Basics_flow + + Typical design flow. Green boxes represent manually created models. + Orange boxes represent modesl generated by synthesis tools. + + +In this example the System Level Model and the Behavioural Model are both +manually written design files. After the equivalence of system level model and +behavioural model has been verified, the lower level representations of the +design can be generated using synthesis tools. Finally the RTL Model and the +Gate-Level Model are verified and the design process is finished. + +However, in any real-world design effort there will be multiple iterations for +this design process. The reason for this can be the late change of a design +requirement or the fact that the analysis of a low-abstraction model +(e.g. gate-level timing analysis) revealed that a design change is required in +order to meet the design requirements (e.g. maximum possible clock speed). + +Whenever the behavioural model or the system level model is changed their +equivalence must be re-verified by re-running the simulations and comparing the +results. Whenever the behavioural model is changed the synthesis must be re-run +and the synthesis results must be re-verified. + +In order to guarantee reproducibility it is important to be able to re-run all +automatic steps in a design project with a fixed set of settings easily. Because +of this, usually all programs used in a synthesis flow can be controlled using +scripts. This means that all functions are available via text commands. When +such a tool provides a GUI, this is complementary to, and not instead of, a +command line interface. + +Usually a synthesis flow in an UNIX/Linux environment would be controlled by a +shell script that calls all required tools (synthesis and +simulation/verification in this example) in the correct order. Each of these +tools would be called with a script file containing commands for the respective +tool. All settings required for the tool would be provided by these script files +so that no manual interaction would be necessary. These script files are +considered design sources and should be kept under version control just like the +source code of the system level and the behavioural model. + +Methods from compiler design +---------------------------- + +Some parts of synthesis tools involve problem domains that are traditionally +known from compiler design. This section addresses some of these domains. + +Lexing and parsing +~~~~~~~~~~~~~~~~~~ + +The best known concepts from compiler design are probably lexing and parsing. +These are two methods that together can be used to process complex computer +languages easily. :cite:p:`Dragonbook` + +A lexer consumes single characters from the input and generates a stream of +lexical tokens that consist of a type and a value. For example the Verilog input +:verilog:`assign foo = bar + 42;` might be translated by the lexer to the list +of lexical tokens given in :numref:`Tab. %s `. + +.. table:: Exemplary token list for the statement :verilog:`assign foo = bar + 42;` + :name: tab:Basics_tokens + + ============== =============== + Token-Type Token-Value + ============== =============== + TOK_ASSIGN \- + TOK_IDENTIFIER "foo" + TOK_EQ \- + TOK_IDENTIFIER "bar" + TOK_PLUS \- + TOK_NUMBER 42 + TOK_SEMICOLON \- + ============== =============== + +The lexer is usually generated by a lexer generator (e.g. flex ) from a +description file that is using regular expressions to specify the text pattern +that should match the individual tokens. + +The lexer is also responsible for skipping ignored characters (such as +whitespace outside string constants and comments in the case of Verilog) and +converting the original text snippet to a token value. + +Note that individual keywords use different token types (instead of a keyword +type with different token values). This is because the parser usually can only +use the Token-Type to make a decision on the grammatical role of a token. + +The parser then transforms the list of tokens into a parse tree that closely +resembles the productions from the computer languages grammar. As the lexer, the +parser is also typically generated by a code generator (e.g. bison ) from a +grammar description in Backus-Naur Form (BNF). + +Let's consider the following BNF (in Bison syntax): + +.. code:: none + :number-lines: + + assign_stmt: TOK_ASSIGN TOK_IDENTIFIER TOK_EQ expr TOK_SEMICOLON; + expr: TOK_IDENTIFIER | TOK_NUMBER | expr TOK_PLUS expr; + +.. figure:: ../images/basics_parsetree.* + :class: width-helper + :name: fig:Basics_parsetree + + Example parse tree for the Verilog expression + :verilog:`assign foo = bar + 42;` + +The parser converts the token list to the parse tree in :numref:`Fig. %s +`. Note that the parse tree never actually exists as a +whole as data structure in memory. Instead the parser calls user-specified code +snippets (so-called reduce-functions) for all inner nodes of the parse tree in +depth-first order. + +In some very simple applications (e.g. code generation for stack machines) it is +possible to perform the task at hand directly in the reduce functions. But +usually the reduce functions are only used to build an in-memory data structure +with the relevant information from the parse tree. This data structure is called +an abstract syntax tree (AST). + +The exact format for the abstract syntax tree is application specific (while the +format of the parse tree and token list are mostly dictated by the grammar of +the language at hand). :numref:`Figure %s ` illustrates what an +AST for the parse tree in :numref:`Fig. %s ` could look +like. + +Usually the AST is then converted into yet another representation that is more +suitable for further processing. In compilers this is often an assembler-like +three-address-code intermediate representation. :cite:p:`Dragonbook` + +.. figure:: ../images/basics_ast.* + :class: width-helper + :name: fig:Basics_ast + + Example abstract syntax tree for the Verilog expression + :verilog:`assign foo = bar + 42;` + + +Multi-pass compilation +~~~~~~~~~~~~~~~~~~~~~~ + +Complex problems are often best solved when split up into smaller problems. This +is certainly true for compilers as well as for synthesis tools. The components +responsible for solving the smaller problems can be connected in two different +ways: through Single-Pass Pipelining and by using Multiple Passes. + +Traditionally a parser and lexer are connected using the pipelined approach: The +lexer provides a function that is called by the parser. This function reads data +from the input until a complete lexical token has been read. Then this token is +returned to the parser. So the lexer does not first generate a complete list of +lexical tokens and then pass it to the parser. Instead they run concurrently and +the parser can consume tokens as the lexer produces them. + +The single-pass pipelining approach has the advantage of lower memory footprint +(at no time must the complete design be kept in memory) but has the disadvantage +of tighter coupling between the interacting components. + +Therefore single-pass pipelining should only be used when the lower memory +footprint is required or the components are also conceptually tightly coupled. +The latter certainly is the case for a parser and its lexer. But when data is +passed between two conceptually loosely coupled components it is often +beneficial to use a multi-pass approach. + +In the multi-pass approach the first component processes all the data and the +result is stored in a in-memory data structure. Then the second component is +called with this data. This reduces complexity, as only one component is running +at a time. It also improves flexibility as components can be exchanged easier. + +Most modern compilers are multi-pass compilers. + +Static Single Assignment (SSA) form +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In imperative programming (and behavioural HDL design) it is possible to assign +the same variable multiple times. This can either mean that the variable is +independently used in two different contexts or that the final value of the +variable depends on a condition. + +The following examples show C code in which one variable is used independently +in two different contexts: + +.. code:: c++ + :number-lines: + + void demo1() + { + int a = 1; + printf("%d\n", a); + + a = 2; + printf("%d\n", a); + } + +.. code:: c++ + + void demo1() + { + int a = 1; + printf("%d\n", a); + + int b = 2; + printf("%d\n", b); + } + +.. code:: c++ + :number-lines: + + void demo2(bool foo) + { + int a; + if (foo) { + a = 23; + printf("%d\n", a); + } else { + a = 42; + printf("%d\n", a); + } + } + +.. code:: c++ + + void demo2(bool foo) + { + int a, b; + if (foo) { + a = 23; + printf("%d\n", a); + } else { + b = 42; + printf("%d\n", b); + } + } + +In both examples the left version (only variable ``a``) and the right version +(variables ``a`` and ``b``) are equivalent. Therefore it is desired for further +processing to bring the code in an equivalent form for both cases. + +In the following example the variable is assigned twice but it cannot be easily +replaced by two variables: + +.. code:: c++ + + void demo3(bool foo) + { + int a = 23 + if (foo) + a = 42; + printf("%d\n", a); + } + +Static single assignment (SSA) form is a representation of imperative code that +uses identical representations for the left and right version of demos 1 and 2, +but can still represent demo 3. In SSA form each assignment assigns a new +variable (usually written with an index). But it also introduces a special +:math:`\Phi`-function to merge the different instances of a variable when +needed. In C-pseudo-code the demo 3 would be written as follows using SSA from: + +.. code:: c++ + + void demo3(bool foo) + { + int a_1, a_2, a_3; + a_1 = 23 + if (foo) + a_2 = 42; + a_3 = phi(a_1, a_2); + printf("%d\n", a_3); + } + +The :math:`\Phi`-function is usually interpreted as "these variables must be +stored in the same memory location" during code generation. Most modern +compilers for imperative languages such as C/C++ use SSA form for at least some +of its passes as it is very easy to manipulate and analyse. + +.. [1] + In recent years formal equivalence checking also became an important + verification method for validating RTL and lower abstraction + representation of the design. diff --git a/docs/source/CHAPTER_CellLib.rst b/docs/source/CHAPTER_CellLib.rst new file mode 100644 index 000000000..c5db434a6 --- /dev/null +++ b/docs/source/CHAPTER_CellLib.rst @@ -0,0 +1,1020 @@ +.. role:: verilog(code) + :language: Verilog + +.. _chapter:celllib: + +Internal cell library +===================== + +Most of the passes in Yosys operate on netlists, i.e. they only care about the +RTLIL::Wire and RTLIL::Cell objects in an RTLIL::Module. This chapter discusses +the cell types used by Yosys to represent a behavioural design internally. + +This chapter is split in two parts. In the first part the internal RTL cells are +covered. These cells are used to represent the design on a coarse grain level. +Like in the original HDL code on this level the cells operate on vectors of +signals and complex cells like adders exist. In the second part the internal +gate cells are covered. These cells are used to represent the design on a +fine-grain gate-level. All cells from this category operate on single bit +signals. + +RTL cells +--------- + +Most of the RTL cells closely resemble the operators available in HDLs such as +Verilog or VHDL. Therefore Verilog operators are used in the following sections +to define the behaviour of the RTL cells. + +Note that all RTL cells have parameters indicating the size of inputs and +outputs. When passes modify RTL cells they must always keep the values of these +parameters in sync with the size of the signals connected to the inputs and +outputs. + +Simulation models for the RTL cells can be found in the file +``techlibs/common/simlib.v`` in the Yosys source tree. + +Unary operators +~~~~~~~~~~~~~~~ + +All unary RTL cells have one input port ``\A`` and one output port ``\Y``. They +also have the following parameters: + +``\A_SIGNED`` + Set to a non-zero value if the input ``\A`` is signed and therefore + should be sign-extended when needed. + +``\A_WIDTH`` + The width of the input port ``\A``. + +``\Y_WIDTH`` + The width of the output port ``\Y``. + +:numref:`tab:CellLib_unary` lists all cells for unary RTL operators. + +.. table:: Cell types for unary operators with their corresponding Verilog expressions. + :name: tab:CellLib_unary + + ================== ============ + Verilog Cell Type + ================== ============ + :verilog:`Y = ~A` $not + :verilog:`Y = +A` $pos + :verilog:`Y = -A` $neg + :verilog:`Y = &A` $reduce_and + :verilog:`Y = |A` $reduce_or + :verilog:`Y = ^A` $reduce_xor + :verilog:`Y = ~^A` $reduce_xnor + :verilog:`Y = |A` $reduce_bool + :verilog:`Y = !A` $logic_not + ================== ============ + +For the unary cells that output a logical value (``$reduce_and``, +``$reduce_or``, ``$reduce_xor``, ``$reduce_xnor``, ``$reduce_bool``, +``$logic_not``), when the ``\Y_WIDTH`` parameter is greater than 1, the output +is zero-extended, and only the least significant bit varies. + +Note that ``$reduce_or`` and ``$reduce_bool`` actually represent the same logic +function. But the HDL frontends generate them in different situations. A +``$reduce_or`` cell is generated when the prefix ``|`` operator is being used. A +``$reduce_bool`` cell is generated when a bit vector is used as a condition in +an ``if``-statement or ``?:``-expression. + +Binary operators +~~~~~~~~~~~~~~~~ + +All binary RTL cells have two input ports ``\A`` and ``\B`` and one output port +``\Y``. They also have the following parameters: + +``\A_SIGNED`` + Set to a non-zero value if the input ``\A`` is signed and therefore + should be sign-extended when needed. + +``\A_WIDTH`` + The width of the input port ``\A``. + +``\B_SIGNED`` + Set to a non-zero value if the input ``\B`` is signed and therefore + should be sign-extended when needed. + +``\B_WIDTH`` + The width of the input port ``\B``. + +``\Y_WIDTH`` + The width of the output port ``\Y``. + +:numref:`tab:CellLib_binary` lists all cells for binary RTL operators. + +.. table:: Cell types for binary operators with their corresponding Verilog expressions. + :name: tab:CellLib_binary + + ======================= ============= ======================= ========= + Verilog Cell Type Verilog Cell Type + ======================= ============= ======================= ========= + :verilog:`Y = A & B` $and :verilog:`Y = A < B` $lt + :verilog:`Y = A | B` $or :verilog:`Y = A <= B` $le + :verilog:`Y = A ^ B` $xor :verilog:`Y = A == B` $eq + :verilog:`Y = A ~^ B` $xnor :verilog:`Y = A != B` $ne + :verilog:`Y = A << B` $shl :verilog:`Y = A >= B` $ge + :verilog:`Y = A >> B` $shr :verilog:`Y = A > B` $gt + :verilog:`Y = A <<< B` $sshl :verilog:`Y = A + B` $add + :verilog:`Y = A >>> B` $sshr :verilog:`Y = A - B` $sub + :verilog:`Y = A && B` $logic_and :verilog:`Y = A * B` $mul + :verilog:`Y = A || B` $logic_or :verilog:`Y = A / B` $div + :verilog:`Y = A === B` $eqx :verilog:`Y = A % B` $mod + :verilog:`Y = A !== B` $nex ``N/A`` $divfloor + :verilog:`Y = A ** B` $pow ``N/A`` $modfoor + ======================= ============= ======================= ========= + +The ``$shl`` and ``$shr`` cells implement logical shifts, whereas the ``$sshl`` +and ``$sshr`` cells implement arithmetic shifts. The ``$shl`` and ``$sshl`` +cells implement the same operation. All four of these cells interpret the second +operand as unsigned, and require ``\B_SIGNED`` to be zero. + +Two additional shift operator cells are available that do not directly +correspond to any operator in Verilog, ``$shift`` and ``$shiftx``. The +``$shift`` cell performs a right logical shift if the second operand is positive +(or unsigned), and a left logical shift if it is negative. The ``$shiftx`` cell +performs the same operation as the ``$shift`` cell, but the vacated bit +positions are filled with undef (x) bits, and corresponds to the Verilog indexed +part-select expression. + +For the binary cells that output a logical value (``$logic_and``, ``$logic_or``, +``$eqx``, ``$nex``, ``$lt``, ``$le``, ``$eq``, ``$ne``, ``$ge``, ``$gt)``, when +the ``\Y_WIDTH`` parameter is greater than 1, the output is zero-extended, and +only the least significant bit varies. + +Division and modulo cells are available in two rounding modes. The original +``$div`` and ``$mod`` cells are based on truncating division, and correspond to +the semantics of the verilog ``/`` and ``%`` operators. The ``$divfloor`` and +``$modfloor`` cells represent flooring division and flooring modulo, the latter +of which is also known as "remainder" in several languages. See +:numref:`tab:CellLib_divmod` for a side-by-side comparison between the different +semantics. + +.. table:: Comparison between different rounding modes for division and modulo cells. + :name: tab:CellLib_divmod + + +-----------+--------+-----------+-----------+-----------+-----------+ + | Division | Result | Truncating | Flooring | + +-----------+--------+-----------+-----------+-----------+-----------+ + | | | $div | $mod | $divfloor | $modfloor | + +===========+========+===========+===========+===========+===========+ + | -10 / 3 | -3.3 | -3 | -1 | -4 | 2 | + +-----------+--------+-----------+-----------+-----------+-----------+ + | 10 / -3 | -3.3 | -3 | 1 | -4 | -2 | + +-----------+--------+-----------+-----------+-----------+-----------+ + | -10 / -3 | 3.3 | 3 | -1 | 3 | -1 | + +-----------+--------+-----------+-----------+-----------+-----------+ + | 10 / 3 | 3.3 | 3 | 1 | 3 | 1 | + +-----------+--------+-----------+-----------+-----------+-----------+ + +Multiplexers +~~~~~~~~~~~~ + +Multiplexers are generated by the Verilog HDL frontend for ``?:``-expressions. +Multiplexers are also generated by the proc pass to map the decision trees from +RTLIL::Process objects to logic. + +The simplest multiplexer cell type is ``$mux``. Cells of this type have a +``\WITDH`` parameter and data inputs ``\A`` and ``\B`` and a data output ``\Y``, +all of the specified width. This cell also has a single bit control input +``\S``. If ``\S`` is 0 the value from the input ``\A`` is sent to the output, if +it is 1 the value from the ``\B`` input is sent to the output. So the ``$mux`` +cell implements the function :verilog:`Y = S ? B : A`. + +The ``$pmux`` cell is used to multiplex between many inputs using a one-hot +select signal. Cells of this type have a ``\WIDTH`` and a ``\S_WIDTH`` parameter +and inputs ``\A``, ``\B``, and ``\S`` and an output ``\Y``. The ``\S`` input is +``\S_WIDTH`` bits wide. The ``\A`` input and the output are both ``\WIDTH`` bits +wide and the ``\B`` input is ``\WIDTH*\S_WIDTH`` bits wide. When all bits of +``\S`` are zero, the value from ``\A`` input is sent to the output. If the +:math:`n`\ 'th bit from ``\S`` is set, the value :math:`n`\ 'th ``\WIDTH`` bits +wide slice of the ``\B`` input is sent to the output. When more than one bit +from ``\S`` is set the output is undefined. Cells of this type are used to model +"parallel cases" (defined by using the ``parallel_case`` attribute or detected +by an optimization). + +The ``$tribuf`` cell is used to implement tristate logic. Cells of this type +have a ``\B`` parameter and inputs ``\A`` and ``\EN`` and an output ``\Y``. The +``\A`` input and ``\Y`` output are ``\WIDTH`` bits wide, and the ``\EN`` input +is one bit wide. When ``\EN`` is 0, the output is not driven. When ``\EN`` is 1, +the value from ``\A`` input is sent to the ``\Y`` output. Therefore, the +``$tribuf`` cell implements the function :verilog:`Y = EN ? A : 'bz`. + +Behavioural code with cascaded if-then-else- and case-statements usually results +in trees of multiplexer cells. Many passes (from various optimizations to FSM +extraction) heavily depend on these multiplexer trees to understand dependencies +between signals. Therefore optimizations should not break these multiplexer +trees (e.g. by replacing a multiplexer between a calculated signal and a +constant zero with an ``$and`` gate). + +Registers +~~~~~~~~~ + +SR-type latches are represented by ``$sr`` cells. These cells have input ports +``\SET`` and ``\CLR`` and an output port ``\Q``. They have the following +parameters: + +``\WIDTH`` + The width of inputs ``\SET`` and ``\CLR`` and output ``\Q``. + +``\SET_POLARITY`` + The set input bits are active-high if this parameter has the value + ``1'b1`` and active-low if this parameter is ``1'b0``. + +``\CLR_POLARITY`` + The reset input bits are active-high if this parameter has the value + ``1'b1`` and active-low if this parameter is ``1'b0``. + +Both set and reset inputs have separate bits for every output bit. When both the +set and reset inputs of an ``$sr`` cell are active for a given bit index, the +reset input takes precedence. + +D-type flip-flops are represented by ``$dff`` cells. These cells have a clock +port ``\CLK``, an input port ``\D`` and an output port ``\Q``. The following +parameters are available for ``$dff`` cells: + +``\WIDTH`` + The width of input ``\D`` and output ``\Q``. + +``\CLK_POLARITY`` + Clock is active on the positive edge if this parameter has the value + ``1'b1`` and on the negative edge if this parameter is ``1'b0``. + +D-type flip-flops with asynchronous reset are represented by ``$adff`` cells. As +the ``$dff`` cells they have ``\CLK``, ``\D`` and ``\Q`` ports. In addition they +also have a single-bit ``\ARST`` input port for the reset pin and the following +additional two parameters: + +``\ARST_POLARITY`` + The asynchronous reset is active-high if this parameter has the value + ``1'b1`` and active-low if this parameter is ``1'b0``. + +``\ARST_VALUE`` + The state of ``\Q`` will be set to this value when the reset is active. + +Usually these cells are generated by the ``proc`` pass using the information in +the designs RTLIL::Process objects. + +D-type flip-flops with synchronous reset are represented by ``$sdff`` cells. As +the ``$dff`` cells they have ``\CLK``, ``\D`` and ``\Q`` ports. In addition they +also have a single-bit ``\SRST`` input port for the reset pin and the following +additional two parameters: + +``\SRST_POLARITY`` + The synchronous reset is active-high if this parameter has the value + ``1'b1`` and active-low if this parameter is ``1'b0``. + +``\SRST_VALUE`` + The state of ``\Q`` will be set to this value when the reset is active. + +Note that the ``$adff`` and ``$sdff`` cells can only be used when the reset value is +constant. + +D-type flip-flops with asynchronous load are represented by ``$aldff`` cells. As +the ``$dff`` cells they have ``\CLK``, ``\D`` and ``\Q`` ports. In addition they +also have a single-bit ``\ALOAD`` input port for the async load enable pin, a +``\AD`` input port with the same width as data for the async load data, and the +following additional parameter: + +``\ALOAD_POLARITY`` + The asynchronous load is active-high if this parameter has the value + ``1'b1`` and active-low if this parameter is ``1'b0``. + +D-type flip-flops with asynchronous set and reset are represented by ``$dffsr`` +cells. As the ``$dff`` cells they have ``\CLK``, ``\D`` and ``\Q`` ports. In +addition they also have multi-bit ``\SET`` and ``\CLR`` input ports and the +corresponding polarity parameters, like ``$sr`` cells. + +D-type flip-flops with enable are represented by ``$dffe``, ``$adffe``, +``$aldffe``, ``$dffsre``, ``$sdffe``, and ``$sdffce`` cells, which are enhanced +variants of ``$dff``, ``$adff``, ``$aldff``, ``$dffsr``, ``$sdff`` (with reset +over enable) and ``$sdff`` (with enable over reset) cells, respectively. They +have the same ports and parameters as their base cell. In addition they also +have a single-bit ``\EN`` input port for the enable pin and the following +parameter: + +``\EN_POLARITY`` + The enable input is active-high if this parameter has the value ``1'b1`` + and active-low if this parameter is ``1'b0``. + +D-type latches are represented by ``$dlatch`` cells. These cells have an enable +port ``\EN``, an input port ``\D``, and an output port ``\Q``. The following +parameters are available for ``$dlatch`` cells: + +``\WIDTH`` + The width of input ``\D`` and output ``\Q``. + +``\EN_POLARITY`` + The enable input is active-high if this parameter has the value ``1'b1`` + and active-low if this parameter is ``1'b0``. + +The latch is transparent when the ``\EN`` input is active. + +D-type latches with reset are represented by ``$adlatch`` cells. In addition to +``$dlatch`` ports and parameters, they also have a single-bit ``\ARST`` input +port for the reset pin and the following additional parameters: + +``\ARST_POLARITY`` + The asynchronous reset is active-high if this parameter has the value + ``1'b1`` and active-low if this parameter is ``1'b0``. + +``\ARST_VALUE`` + The state of ``\Q`` will be set to this value when the reset is active. + +D-type latches with set and reset are represented by ``$dlatchsr`` cells. In +addition to ``$dlatch`` ports and parameters, they also have multi-bit ``\SET`` +and ``\CLR`` input ports and the corresponding polarity parameters, like ``$sr`` +cells. + +.. _sec:memcells: + +Memories +~~~~~~~~ + +Memories are either represented using RTLIL::Memory objects, ``$memrd_v2``, +``$memwr_v2``, and ``$meminit_v2`` cells, or by ``$mem_v2`` cells alone. + +In the first alternative the RTLIL::Memory objects hold the general metadata for +the memory (bit width, size in number of words, etc.) and for each port a +``$memrd_v2`` (read port) or ``$memwr_v2`` (write port) cell is created. Having +individual cells for read and write ports has the advantage that they can be +consolidated using resource sharing passes. In some cases this drastically +reduces the number of required ports on the memory cell. In this alternative, +memory initialization data is represented by ``$meminit_v2`` cells, which allow +delaying constant folding for initialization addresses and data until after the +frontend finishes. + +The ``$memrd_v2`` cells have a clock input ``\CLK``, an enable input ``\EN``, an +address input ``\ADDR``, a data output ``\DATA``, an asynchronous reset input +``\ARST``, and a synchronous reset input ``\SRST``. They also have the following +parameters: + +``\MEMID`` + The name of the RTLIL::Memory object that is associated with this read + port. + +``\ABITS`` + The number of address bits (width of the ``\ADDR`` input port). + +``\WIDTH`` + The number of data bits (width of the ``\DATA`` output port). Note that + this may be a power-of-two multiple of the underlying memory's width -- + such ports are called wide ports and access an aligned group of cells at + once. In this case, the corresponding low bits of ``\ADDR`` must be + tied to 0. + +``\CLK_ENABLE`` + When this parameter is non-zero, the clock is used. Otherwise this read + port is asynchronous and the ``\CLK`` input is not used. + +``\CLK_POLARITY`` + Clock is active on the positive edge if this parameter has the value + ``1'b1`` and on the negative edge if this parameter is ``1'b0``. + +``\TRANSPARENCY_MASK`` + This parameter is a bitmask of write ports that this read port is + transparent with. The bits of this parameter are indexed by the write + port's ``\PORTID`` parameter. Transparency can only be enabled between + synchronous ports sharing a clock domain. When transparency is enabled + for a given port pair, a read and write to the same address in the same + cycle will return the new value. Otherwise the old value is returned. + +``\COLLISION_X_MASK`` + This parameter is a bitmask of write ports that have undefined collision + behavior with this port. The bits of this parameter are indexed by the + write port's ``\PORTID`` parameter. This behavior can only be enabled + between synchronous ports sharing a clock domain. When undefined + collision is enabled for a given port pair, a read and write to the same + address in the same cycle will return the undefined (all-X) value.This + option is exclusive (for a given port pair) with the transparency + option. + +``\ARST_VALUE`` + Whenever the ``\ARST`` input is asserted, the data output will be reset + to this value. Only used for synchronous ports. + +``\SRST_VALUE`` + Whenever the ``\SRST`` input is synchronously asserted, the data output + will be reset to this value. Only used for synchronous ports. + +``\INIT_VALUE`` + The initial value of the data output, for synchronous ports. + +``\CE_OVER_SRST`` + If this parameter is non-zero, the ``\SRST`` input is only recognized + when ``\EN`` is true. Otherwise, ``\SRST`` is recognized regardless of + ``\EN``. + +The ``$memwr_v2`` cells have a clock input ``\CLK``, an enable input ``\EN`` +(one enable bit for each data bit), an address input ``\ADDR`` and a data input +``\DATA``. They also have the following parameters: + +``\MEMID`` + The name of the RTLIL::Memory object that is associated with this write + port. + +``\ABITS`` + The number of address bits (width of the ``\ADDR`` input port). + +``\WIDTH`` + The number of data bits (width of the ``\DATA`` output port). Like with + ``$memrd_v2`` cells, the width is allowed to be any power-of-two + multiple of memory width, with the corresponding restriction on address. + +``\CLK_ENABLE`` + When this parameter is non-zero, the clock is used. Otherwise this write + port is asynchronous and the ``\CLK`` input is not used. + +``\CLK_POLARITY`` + Clock is active on positive edge if this parameter has the value + ``1'b1`` and on the negative edge if this parameter is ``1'b0``. + +``\PORTID`` + An identifier for this write port, used to index write port bit mask parameters. + +``\PRIORITY_MASK`` + This parameter is a bitmask of write ports that this write port has + priority over in case of writing to the same address. The bits of this + parameter are indexed by the other write port's ``\PORTID`` parameter. + Write ports can only have priority over write ports with lower port ID. + When two ports write to the same address and neither has priority over + the other, the result is undefined. Priority can only be set between + two synchronous ports sharing the same clock domain. + +The ``$meminit_v2`` cells have an address input ``\ADDR``, a data input +``\DATA``, with the width of the ``\DATA`` port equal to ``\WIDTH`` parameter +times ``\WORDS`` parameter, and a bit enable mask input ``\EN`` with width equal +to ``\WIDTH`` parameter. All three of the inputs must resolve to a constant for +synthesis to succeed. + +``\MEMID`` + The name of the RTLIL::Memory object that is associated with this + initialization cell. + +``\ABITS`` + The number of address bits (width of the ``\ADDR`` input port). + +``\WIDTH`` + The number of data bits per memory location. + +``\WORDS`` + The number of consecutive memory locations initialized by this cell. + +``\PRIORITY`` + The cell with the higher integer value in this parameter wins an + initialization conflict. + +The HDL frontend models a memory using RTLIL::Memory objects and asynchronous +``$memrd_v2`` and ``$memwr_v2`` cells. The ``memory`` pass (i.e.~its various +sub-passes) migrates ``$dff`` cells into the ``$memrd_v2`` and ``$memwr_v2`` +cells making them synchronous, then converts them to a single ``$mem_v2`` cell +and (optionally) maps this cell type to ``$dff`` cells for the individual words +and multiplexer-based address decoders for the read and write interfaces. When +the last step is disabled or not possible, a ``$mem_v2`` cell is left in the +design. + +The ``$mem_v2`` cell provides the following parameters: + +``\MEMID`` + The name of the original RTLIL::Memory object that became this + ``$mem_v2`` cell. + +``\SIZE`` + The number of words in the memory. + +``\ABITS`` + The number of address bits. + +``\WIDTH`` + The number of data bits per word. + +``\INIT`` + The initial memory contents. + +``\RD_PORTS`` + The number of read ports on this memory cell. + +``\RD_WIDE_CONTINUATION`` + This parameter is ``\RD_PORTS`` bits wide, containing a bitmask of + "wide continuation" read ports. Such ports are used to represent the + extra data bits of wide ports in the combined cell, and must have all + control signals identical with the preceding port, except for address, + which must have the proper sub-cell address encoded in the low bits. + +``\RD_CLK_ENABLE`` + This parameter is ``\RD_PORTS`` bits wide, containing a clock enable bit + for each read port. + +``\RD_CLK_POLARITY`` + This parameter is ``\RD_PORTS`` bits wide, containing a clock polarity + bit for each read port. + +``\RD_TRANSPARENCY_MASK`` + This parameter is ``\RD_PORTS*\WR_PORTS`` bits wide, containing a + concatenation of all ``\TRANSPARENCY_MASK`` values of the original + ``$memrd_v2`` cells. + +``\RD_COLLISION_X_MASK`` + This parameter is ``\RD_PORTS*\WR_PORTS`` bits wide, containing a + concatenation of all ``\COLLISION_X_MASK`` values of the original + ``$memrd_v2`` cells. + +``\RD_CE_OVER_SRST`` + This parameter is ``\RD_PORTS`` bits wide, determining relative + synchronous reset and enable priority for each read port. + +``\RD_INIT_VALUE`` + This parameter is ``\RD_PORTS*\WIDTH`` bits wide, containing the initial + value for each synchronous read port. + +``\RD_ARST_VALUE`` + This parameter is ``\RD_PORTS*\WIDTH`` bits wide, containing the + asynchronous reset value for each synchronous read port. + +``\RD_SRST_VALUE`` + This parameter is ``\RD_PORTS*\WIDTH`` bits wide, containing the + synchronous reset value for each synchronous read port. + +``\WR_PORTS`` + The number of write ports on this memory cell. + +``\WR_WIDE_CONTINUATION`` + This parameter is ``\WR_PORTS`` bits wide, containing a bitmask of + "wide continuation" write ports. + +``\WR_CLK_ENABLE`` + This parameter is ``\WR_PORTS`` bits wide, containing a clock enable bit + for each write port. + +``\WR_CLK_POLARITY`` + This parameter is ``\WR_PORTS`` bits wide, containing a clock polarity + bit for each write port. + +``\WR_PRIORITY_MASK`` + This parameter is ``\WR_PORTS*\WR_PORTS`` bits wide, containing a + concatenation of all ``\PRIORITY_MASK`` values of the original + ``$memwr_v2`` cells. + +The ``$mem_v2`` cell has the following ports: + +``\RD_CLK`` + This input is ``\RD_PORTS`` bits wide, containing all clock signals for + the read ports. + +``\RD_EN`` + This input is ``\RD_PORTS`` bits wide, containing all enable signals for + the read ports. + +``\RD_ADDR`` + This input is ``\RD_PORTS*\ABITS`` bits wide, containing all address + signals for the read ports. + +``\RD_DATA`` + This input is ``\RD_PORTS*\WIDTH`` bits wide, containing all data + signals for the read ports. + +``\RD_ARST`` + This input is ``\RD_PORTS`` bits wide, containing all asynchronous reset + signals for the read ports. + +``\RD_SRST`` + This input is ``\RD_PORTS`` bits wide, containing all synchronous reset + signals for the read ports. + +``\WR_CLK`` + This input is ``\WR_PORTS`` bits wide, containing all clock signals for + the write ports. + +``\WR_EN`` + This input is ``\WR_PORTS*\WIDTH`` bits wide, containing all enable + signals for the write ports. + +``\WR_ADDR`` + This input is ``\WR_PORTS*\ABITS`` bits wide, containing all address + signals for the write ports. + +``\WR_DATA`` + This input is ``\WR_PORTS*\WIDTH`` bits wide, containing all data + signals for the write ports. + +The ``memory_collect`` pass can be used to convert discrete ``$memrd_v2``, +``$memwr_v2``, and ``$meminit_v2`` cells belonging to the same memory to a +single ``$mem_v2`` cell, whereas the ``memory_unpack`` pass performs the inverse +operation. The ``memory_dff`` pass can combine asynchronous memory ports that +are fed by or feeding registers into synchronous memory ports. The +``memory_bram`` pass can be used to recognize ``$mem_v2`` cells that can be +implemented with a block RAM resource on an FPGA. The ``memory_map`` pass can be +used to implement ``$mem_v2`` cells as basic logic: word-wide DFFs and address +decoders. + +Finite state machines +~~~~~~~~~~~~~~~~~~~~~ + +Add a brief description of the ``$fsm`` cell type. + +Specify rules +~~~~~~~~~~~~~ + +Add information about ``$specify2``, ``$specify3``, and ``$specrule`` cells. + +Formal verification cells +~~~~~~~~~~~~~~~~~~~~~~~~~ + +Add information about ``$assert``, ``$assume``, ``$live``, ``$fair``, +``$cover``, ``$equiv``, ``$initstate``, ``$anyconst``, ``$anyseq``, +``$anyinit``, ``$allconst``, ``$allseq`` cells. + +Add information about ``$ff`` and ``$_FF_`` cells. + +.. _sec:celllib_gates: + +Gates +----- + +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 +techlibs/common/simcells.v in the Yosys source tree. + +.. table:: Cell types for gate level logic networks (main list) + :name: tab:CellLib_gates + + ======================================= ============ + Verilog Cell Type + ======================================= ============ + :verilog:`Y = A` $_BUF_ + :verilog:`Y = ~A` $_NOT_ + :verilog:`Y = A & B` $_AND_ + :verilog:`Y = ~(A & B)` $_NAND_ + :verilog:`Y = A & ~B` $_ANDNOT_ + :verilog:`Y = A | B` $_OR_ + :verilog:`Y = ~(A | B)` $_NOR_ + :verilog:`Y = A | ~B` $_ORNOT_ + :verilog:`Y = A ^ B` $_XOR_ + :verilog:`Y = ~(A ^ B)` $_XNOR_ + :verilog:`Y = ~((A & B) | C)` $_AOI3_ + :verilog:`Y = ~((A | B) & C)` $_OAI3_ + :verilog:`Y = ~((A & B) | (C & D))` $_AOI4_ + :verilog:`Y = ~((A | B) & (C | D))` $_OAI4_ + :verilog:`Y = S ? B : A` $_MUX_ + :verilog:`Y = ~(S ? B : A)` $_NMUX_ + (see below) $_MUX4_ + (see below) $_MUX8_ + (see below) $_MUX16_ + :verilog:`Y = EN ? A : 1'bz` $_TBUF_ + :verilog:`always @(negedge C) Q <= D` $_DFF_N_ + :verilog:`always @(posedge C) Q <= D` $_DFF_P_ + :verilog:`always @* if (!E) Q <= D` $_DLATCH_N_ + :verilog:`always @* if (E) Q <= D` $_DLATCH_P_ + ======================================= ============ + +.. table:: Cell types for gate level logic networks (FFs with reset) + :name: tab:CellLib_gates_adff + + ================== ============== ============== ======================= + :math:`ClkEdge` :math:`RstLvl` :math:`RstVal` Cell Type + ================== ============== ============== ======================= + :verilog:`negedge` ``0`` ``0`` $_DFF_NN0_, $_SDFF_NN0_ + :verilog:`negedge` ``0`` ``1`` $_DFF_NN1_, $_SDFF_NN1_ + :verilog:`negedge` ``1`` ``0`` $_DFF_NP0_, $_SDFF_NP0_ + :verilog:`negedge` ``1`` ``1`` $_DFF_NP1_, $_SDFF_NP1_ + :verilog:`posedge` ``0`` ``0`` $_DFF_PN0_, $_SDFF_PN0_ + :verilog:`posedge` ``0`` ``1`` $_DFF_PN1_, $_SDFF_PN1_ + :verilog:`posedge` ``1`` ``0`` $_DFF_PP0_, $_SDFF_PP0_ + :verilog:`posedge` ``1`` ``1`` $_DFF_PP1_, $_SDFF_PP1_ + ================== ============== ============== ======================= + + +.. table:: Cell types for gate level logic networks (FFs with enable) + :name: tab:CellLib_gates_dffe + + ================== ============= =========== + :math:`ClkEdge` :math:`EnLvl` Cell Type + ================== ============= =========== + :verilog:`negedge` ``0`` $_DFFE_NN_ + :verilog:`negedge` ``1`` $_DFFE_NP_ + :verilog:`posedge` ``0`` $_DFFE_PN_ + :verilog:`posedge` ``1`` $_DFFE_PP_ + ================== ============= =========== + + +.. table:: Cell types for gate level logic networks (FFs with reset and enable) + :name: tab:CellLib_gates_adffe + + ================== ============== ============== ============= =========================================== + :math:`ClkEdge` :math:`RstLvl` :math:`RstVal` :math:`EnLvl` Cell Type + ================== ============== ============== ============= =========================================== + :verilog:`negedge` ``0`` ``0`` ``0`` $_DFFE_NN0N_, $_SDFFE_NN0N_, $_SDFFCE_NN0N_ + :verilog:`negedge` ``0`` ``0`` ``1`` $_DFFE_NN0P_, $_SDFFE_NN0P_, $_SDFFCE_NN0P_ + :verilog:`negedge` ``0`` ``1`` ``0`` $_DFFE_NN1N_, $_SDFFE_NN1N_, $_SDFFCE_NN1N_ + :verilog:`negedge` ``0`` ``1`` ``1`` $_DFFE_NN1P_, $_SDFFE_NN1P_, $_SDFFCE_NN1P_ + :verilog:`negedge` ``1`` ``0`` ``0`` $_DFFE_NP0N_, $_SDFFE_NP0N_, $_SDFFCE_NP0N_ + :verilog:`negedge` ``1`` ``0`` ``1`` $_DFFE_NP0P_, $_SDFFE_NP0P_, $_SDFFCE_NP0P_ + :verilog:`negedge` ``1`` ``1`` ``0`` $_DFFE_NP1N_, $_SDFFE_NP1N_, $_SDFFCE_NP1N_ + :verilog:`negedge` ``1`` ``1`` ``1`` $_DFFE_NP1P_, $_SDFFE_NP1P_, $_SDFFCE_NP1P_ + :verilog:`posedge` ``0`` ``0`` ``0`` $_DFFE_PN0N_, $_SDFFE_PN0N_, $_SDFFCE_PN0N_ + :verilog:`posedge` ``0`` ``0`` ``1`` $_DFFE_PN0P_, $_SDFFE_PN0P_, $_SDFFCE_PN0P_ + :verilog:`posedge` ``0`` ``1`` ``0`` $_DFFE_PN1N_, $_SDFFE_PN1N_, $_SDFFCE_PN1N_ + :verilog:`posedge` ``0`` ``1`` ``1`` $_DFFE_PN1P_, $_SDFFE_PN1P_, $_SDFFCE_PN1P_ + :verilog:`posedge` ``1`` ``0`` ``0`` $_DFFE_PP0N_, $_SDFFE_PP0N_, $_SDFFCE_PP0N_ + :verilog:`posedge` ``1`` ``0`` ``1`` $_DFFE_PP0P_, $_SDFFE_PP0P_, $_SDFFCE_PP0P_ + :verilog:`posedge` ``1`` ``1`` ``0`` $_DFFE_PP1N_, $_SDFFE_PP1N_, $_SDFFCE_PP1N_ + :verilog:`posedge` ``1`` ``1`` ``1`` $_DFFE_PP1P_, $_SDFFE_PP1P_, $_SDFFCE_PP1P_ + ================== ============== ============== ============= =========================================== + +.. table:: Cell types for gate level logic networks (FFs with set and reset) + :name: tab:CellLib_gates_dffsr + + ================== ============== ============== ============ + :math:`ClkEdge` :math:`SetLvl` :math:`RstLvl` Cell Type + ================== ============== ============== ============ + :verilog:`negedge` ``0`` ``0`` $_DFFSR_NNN_ + :verilog:`negedge` ``0`` ``1`` $_DFFSR_NNP_ + :verilog:`negedge` ``1`` ``0`` $_DFFSR_NPN_ + :verilog:`negedge` ``1`` ``1`` $_DFFSR_NPP_ + :verilog:`posedge` ``0`` ``0`` $_DFFSR_PNN_ + :verilog:`posedge` ``0`` ``1`` $_DFFSR_PNP_ + :verilog:`posedge` ``1`` ``0`` $_DFFSR_PPN_ + :verilog:`posedge` ``1`` ``1`` $_DFFSR_PPP_ + ================== ============== ============== ============ + + +.. table:: Cell types for gate level logic networks (FFs with set and reset and enable) + :name: tab:CellLib_gates_dffsre + + ================== ============== ============== ============= ============== + :math:`ClkEdge` :math:`SetLvl` :math:`RstLvl` :math:`EnLvl` Cell Type + ================== ============== ============== ============= ============== + :verilog:`negedge` ``0`` ``0`` ``0`` $_DFFSRE_NNNN_ + :verilog:`negedge` ``0`` ``0`` ``1`` $_DFFSRE_NNNP_ + :verilog:`negedge` ``0`` ``1`` ``0`` $_DFFSRE_NNPN_ + :verilog:`negedge` ``0`` ``1`` ``1`` $_DFFSRE_NNPP_ + :verilog:`negedge` ``1`` ``0`` ``0`` $_DFFSRE_NPNN_ + :verilog:`negedge` ``1`` ``0`` ``1`` $_DFFSRE_NPNP_ + :verilog:`negedge` ``1`` ``1`` ``0`` $_DFFSRE_NPPN_ + :verilog:`negedge` ``1`` ``1`` ``1`` $_DFFSRE_NPPP_ + :verilog:`posedge` ``0`` ``0`` ``0`` $_DFFSRE_PNNN_ + :verilog:`posedge` ``0`` ``0`` ``1`` $_DFFSRE_PNNP_ + :verilog:`posedge` ``0`` ``1`` ``0`` $_DFFSRE_PNPN_ + :verilog:`posedge` ``0`` ``1`` ``1`` $_DFFSRE_PNPP_ + :verilog:`posedge` ``1`` ``0`` ``0`` $_DFFSRE_PPNN_ + :verilog:`posedge` ``1`` ``0`` ``1`` $_DFFSRE_PPNP_ + :verilog:`posedge` ``1`` ``1`` ``0`` $_DFFSRE_PPPN_ + :verilog:`posedge` ``1`` ``1`` ``1`` $_DFFSRE_PPPP_ + ================== ============== ============== ============= ============== + + +.. table:: Cell types for gate level logic networks (latches with reset) + :name: tab:CellLib_gates_adlatch + + ============= ============== ============== ============= + :math:`EnLvl` :math:`RstLvl` :math:`RstVal` Cell Type + ============= ============== ============== ============= + ``0`` ``0`` ``0`` $_DLATCH_NN0_ + ``0`` ``0`` ``1`` $_DLATCH_NN1_ + ``0`` ``1`` ``0`` $_DLATCH_NP0_ + ``0`` ``1`` ``1`` $_DLATCH_NP1_ + ``1`` ``0`` ``0`` $_DLATCH_PN0_ + ``1`` ``0`` ``1`` $_DLATCH_PN1_ + ``1`` ``1`` ``0`` $_DLATCH_PP0_ + ``1`` ``1`` ``1`` $_DLATCH_PP1_ + ============= ============== ============== ============= + + +.. table:: Cell types for gate level logic networks (latches with set and reset) + :name: tab:CellLib_gates_dlatchsr + + ============= ============== ============== =============== + :math:`EnLvl` :math:`SetLvl` :math:`RstLvl` Cell Type + ============= ============== ============== =============== + ``0`` ``0`` ``0`` $_DLATCHSR_NNN_ + ``0`` ``0`` ``1`` $_DLATCHSR_NNP_ + ``0`` ``1`` ``0`` $_DLATCHSR_NPN_ + ``0`` ``1`` ``1`` $_DLATCHSR_NPP_ + ``1`` ``0`` ``0`` $_DLATCHSR_PNN_ + ``1`` ``0`` ``1`` $_DLATCHSR_PNP_ + ``1`` ``1`` ``0`` $_DLATCHSR_PPN_ + ``1`` ``1`` ``1`` $_DLATCHSR_PPP_ + ============= ============== ============== =============== + + + +.. table:: Cell types for gate level logic networks (SR latches) + :name: tab:CellLib_gates_sr + + ============== ============== ========= + :math:`SetLvl` :math:`RstLvl` Cell Type + ============== ============== ========= + ``0`` ``0`` $_SR_NN_ + ``0`` ``1`` $_SR_NP_ + ``1`` ``0`` $_SR_PN_ + ``1`` ``1`` $_SR_PP_ + ============== ============== ========= + + +Tables \ :numref:`%s `, :numref:`%s +`, :numref:`%s `, :numref:`%s +`, :numref:`%s `, :numref:`%s +`, :numref:`%s `, +:numref:`%s ` and :numref:`%s +` list all cell types used for gate level logic. The cell +types ``$_BUF_``, ``$_NOT_``, ``$_AND_``, ``$_NAND_``, ``$_ANDNOT_``, ``$_OR_``, +``$_NOR_``, ``$_ORNOT_``, ``$_XOR_``, ``$_XNOR_``, ``$_AOI3_``, ``$_OAI3_``, +``$_AOI4_``, ``$_OAI4_``, ``$_MUX_``, ``$_MUX4_``, ``$_MUX8_``, ``$_MUX16_`` and +``$_NMUX_`` are used to model combinatorial logic. The cell type ``$_TBUF_`` is +used to model tristate logic. + +The ``$_MUX4_``, ``$_MUX8_`` and ``$_MUX16_`` cells are used to model wide +muxes, and correspond to the following Verilog code: + +.. code-block:: verilog + :force: + + // $_MUX4_ + assign Y = T ? (S ? D : C) : + (S ? B : A); + // $_MUX8_ + assign Y = U ? T ? (S ? H : G) : + (S ? F : E) : + T ? (S ? D : C) : + (S ? B : A); + // $_MUX16_ + assign Y = V ? U ? T ? (S ? P : O) : + (S ? N : M) : + T ? (S ? L : K) : + (S ? J : I) : + U ? T ? (S ? H : G) : + (S ? F : E) : + T ? (S ? D : C) : + (S ? B : A); + +The cell types ``$_DFF_N_`` and ``$_DFF_P_`` represent d-type flip-flops. + +The cell types ``$_DFFE_[NP][NP]_`` implement d-type flip-flops with enable. The +values in the table for these cell types relate to the following Verilog code +template. + +.. code-block:: verilog + :force: + + always @(CLK_EDGE C) + if (EN == EN_LVL) + Q <= D; + +The cell types ``$_DFF_[NP][NP][01]_`` implement d-type flip-flops with +asynchronous reset. The values in the table for these cell types relate to the +following Verilog code template, where ``RST_EDGE`` is ``posedge`` if +``RST_LVL`` if ``1``, and ``negedge`` otherwise. + +.. code-block:: verilog + :force: + + always @(CLK_EDGE C, RST_EDGE R) + if (R == RST_LVL) + Q <= RST_VAL; + else + Q <= D; + +The cell types ``$_SDFF_[NP][NP][01]_`` implement d-type flip-flops with +synchronous reset. The values in the table for these cell types relate to the +following Verilog code template: + +.. code-block:: verilog + :force: + + always @(CLK_EDGE C) + if (R == RST_LVL) + Q <= RST_VAL; + else + Q <= D; + +The cell types ``$_DFFE_[NP][NP][01][NP]_`` implement d-type flip-flops with +asynchronous reset and enable. The values in the table for these cell types +relate to the following Verilog code template, where ``RST_EDGE`` is +``posedge`` if ``RST_LVL`` if ``1``, and ``negedge`` otherwise. + +.. code-block:: verilog + :force: + + always @(CLK_EDGE C, RST_EDGE R) + if (R == RST_LVL) + Q <= RST_VAL; + else if (EN == EN_LVL) + Q <= D; + +The cell types ``$_SDFFE_[NP][NP][01][NP]_`` implement d-type flip-flops with +synchronous reset and enable, with reset having priority over enable. The values +in the table for these cell types relate to the following Verilog code template: + +.. code-block:: verilog + :force: + + always @(CLK_EDGE C) + if (R == RST_LVL) + Q <= RST_VAL; + else if (EN == EN_LVL) + Q <= D; + +The cell types ``$_SDFFCE_[NP][NP][01][NP]_`` implement d-type flip-flops with +synchronous reset and enable, with enable having priority over reset. The values +in the table for these cell types relate to the following Verilog code template: + +.. code-block:: verilog + :force: + + always @(CLK_EDGE C) + if (EN == EN_LVL) + if (R == RST_LVL) + Q <= RST_VAL; + else + Q <= D; + +The cell types ``$_DFFSR_[NP][NP][NP]_`` implement d-type flip-flops with +asynchronous set and reset. The values in the table for these cell types relate +to the following Verilog code template, where ``RST_EDGE`` is ``posedge`` if +``RST_LVL`` if ``1``, ``negedge`` otherwise, and ``SET_EDGE`` is ``posedge`` +if ``SET_LVL`` if ``1``, ``negedge`` otherwise. + +.. code-block:: verilog + :force: + + always @(CLK_EDGE C, RST_EDGE R, SET_EDGE S) + if (R == RST_LVL) + Q <= 0; + else if (S == SET_LVL) + Q <= 1; + else + Q <= D; + +The cell types ``$_DFFSRE_[NP][NP][NP][NP]_`` implement d-type flip-flops with +asynchronous set and reset and enable. The values in the table for these cell +types relate to the following Verilog code template, where ``RST_EDGE`` is +``posedge`` if ``RST_LVL`` if ``1``, ``negedge`` otherwise, and ``SET_EDGE`` +is ``posedge`` if ``SET_LVL`` if ``1``, ``negedge`` otherwise. + +.. code-block:: verilog + :force: + + always @(CLK_EDGE C, RST_EDGE R, SET_EDGE S) + if (R == RST_LVL) + Q <= 0; + else if (S == SET_LVL) + Q <= 1; + else if (E == EN_LVL) + Q <= D; + +The cell types ``$_DLATCH_N_`` and ``$_DLATCH_P_`` represent d-type latches. + +The cell types ``$_DLATCH_[NP][NP][01]_`` implement d-type latches with reset. +The values in the table for these cell types relate to the following Verilog +code template: + +.. code-block:: verilog + :force: + + always @* + if (R == RST_LVL) + Q <= RST_VAL; + else if (E == EN_LVL) + Q <= D; + +The cell types ``$_DLATCHSR_[NP][NP][NP]_`` implement d-type latches with set +and reset. The values in the table for these cell types relate to the following +Verilog code template: + +.. code-block:: verilog + :force: + + always @* + if (R == RST_LVL) + Q <= 0; + else if (S == SET_LVL) + Q <= 1; + else if (E == EN_LVL) + Q <= D; + +The cell types ``$_SR_[NP][NP]_`` implement sr-type latches. The values in the +table for these cell types relate to the following Verilog code template: + +.. code-block:: verilog + :force: + + always @* + if (R == RST_LVL) + Q <= 0; + else if (S == SET_LVL) + Q <= 1; + +In most cases gate level logic networks are created from RTL networks using the +techmap pass. The flip-flop cells from the gate level logic network can be +mapped to physical flip-flop cells from a Liberty file using the dfflibmap pass. +The combinatorial logic cells can be mapped to physical cells from a Liberty +file via ABC using the abc pass. + +Add information about ``$slice`` and ``$concat`` cells. + +Add information about ``$lut`` and ``$sop`` cells. + +Add information about ``$alu``, ``$macc``, ``$fa``, and ``$lcu`` cells. diff --git a/docs/source/CHAPTER_Eval.rst b/docs/source/CHAPTER_Eval.rst new file mode 100644 index 000000000..3d463d3f9 --- /dev/null +++ b/docs/source/CHAPTER_Eval.rst @@ -0,0 +1,233 @@ +.. _chapter:eval: + +Evaluation, conclusion, future Work +=================================== + +The Yosys source tree contains over 200 test cases [1]_ which are used +in the make test make-target. Besides these there is an external Yosys +benchmark and test case package that contains a few larger designs . +This package contains the designs listed in +Tab. \ `[tab:yosys-test-designs] <#tab:yosys-test-designs>`__. + +.. table:: Tests included in the yosys-tests package. + + =========== ========= ================ + ====================================================== + Test-Design Source Gates Description / Comments + =========== ========= ================ + ====================================================== + aes_core IWLS2005 :math:`41{,}837` AES Cipher written by Rudolf Usselmann + i2c IWLS2005 :math:`1{,}072` WISHBONE compliant I2C Master by Richard Herveille + openmsp430 OpenCores :math:`7{,}173` MSP430 compatible CPU by Olivier Girard + or1200 OpenCores :math:`42{,}675` The OpenRISC 1200 CPU by Damjan Lampret + sasc IWLS2005 :math:`456` Simple Async. Serial Comm. Device by Rudolf Usselmann + simple_spi IWLS2005 :math:`690` MC68HC11E based SPI interface by Richard Herveille + spi IWLS2005 :math:`2{,}478` SPI IP core by Simon Srot + ss_pcm IWLS2005 :math:`279` PCM IO Slave by Rudolf Usselmann + systemcaes IWLS2005 :math:`6{,}893` AES core (using SystemC to Verilog) by Javier Castillo + usb_phy IWLS2005 :math:`515` USB 1.1 PHY by Rudolf Usselmann + =========== ========= ================ + ====================================================== + +Correctness of synthesis results +-------------------------------- + +The following measures were taken to increase the confidence in the +correctness of the Yosys synthesis results: + +- Yosys comes with a large selection [2]_ of small test cases that are + evaluated when the command make test is executed. During development + of Yosys it was shown that this collection of test cases is + sufficient to catch most bugs. The following more sophisticated test + procedures only caught a few additional bugs. Whenever this happened, + an appropriate test case was added to the collection of small test + cases for make test to ensure better testability of the feature in + question in the future. + +- The designs listed in + Tab. \ `[tab:yosys-test-designs] <#tab:yosys-test-designs>`__ where + validated using the formal verification tool Synopsys Formality. The + Yosys synthesis scripts used to synthesize the individual designs for + this test are slightly different per design in order to broaden the + coverage of Yosys features. The large majority of all errors + encountered using these tests are false-negatives, mostly related to + FSM encoding or signal naming in large array logic (such as in memory + blocks). Therefore the fsm_recode pass was extended so it can be used + to generate TCL commands for Synopsys Formality that describe the + relationship between old and new state encodings. Also the method + used to generate signal and cell names in the Verilog backend was + slightly modified in order to improve the automatic matching of net + names in Synopsys Formality. With these changes in place all designs + in Tab. \ `[tab:yosys-test-designs] <#tab:yosys-test-designs>`__ + validate successfully using Formality. + +- VlogHammer is a set of scripts that auto-generate a large collection + of test cases [3]_ and synthesize them using Yosys and the following + freely available proprietary synthesis tools. + + - Xilinx Vivado WebPack (2013.2) + + - Xilinx ISE (XST) WebPack (14.5) + + - Altera Quartus II Web Edition (13.0) + + The built-in SAT solver of Yosys is used to formally verify the Yosys + RTL- and Gate-Level netlists against the netlists generated by this + other tools. [4]_ When differences are found, the input pattern that + result in different outputs are used for simulating the original + Verilog code as well as the synthesis results using the following + Verilog simulators. + + - Xilinx ISIM (from Xilinx ISE 14.5 ) + + - Modelsim 10.1d (from Quartus II 13.0 ) + + - Icarus Verilog (no specific version) + + The set of tests performed by VlogHammer systematically verify the + correct behaviour of + + - Yosys Verilog Frontend and RTL generation + + - Yosys Gate-Level Technology Mapping + + - Yosys SAT Models for RTL- and Gate-Level cells + + - Yosys Constant Evaluator Models for RTL- and Gate-Level cells + + against the reference provided by the other tools. A few bugs related + to sign extensions and bit-width extensions where found (and have + been fixed meanwhile) using this approach. This test also revealed a + small number of bugs in the other tools (i.e. Vivado, XST, Quartus, + ISIM and Icarus Verilog; no bugs where found in Modelsim using + vlogHammer so far). + +Although complex software can never be expected to be fully bug-free +:cite:p:`MURPHY`, it has been shown that Yosys is mature and +feature-complete enough to handle most real-world cases correctly. + +Quality of synthesis results +---------------------------- + +In this section an attempt to evaluate the quality of Yosys synthesis +results is made. To this end the synthesis results of a commercial FPGA +synthesis tool when presented with the original HDL code vs. when +presented with the Yosys synthesis result are compared. + +The OpenMSP430 and the OpenRISC 1200 test cases were synthesized using +the following Yosys synthesis script: + +:: + + hierarchy -check + proc; opt; fsm; opt; memory; opt + techmap; opt; abc; opt + +The original RTL and the Yosys output where both passed to the Xilinx +XST 14.5 FPGA synthesis tool. The following setting where used for XST: + +:: + + -p artix7 + -use_dsp48 NO + -iobuf NO + -ram_extract NO + -rom_extract NO + -fsm_extract YES + -fsm_encoding Auto + +The results of this comparison is summarized in +Tab. \ `[tab:synth-test] <#tab:synth-test>`__. The used FPGA resources +(registers and LUTs) and performance (maximum frequency as reported by +XST) are given per module (indentation indicates module hierarchy, the +numbers are including all contained modules). + +For most modules the results are very similar between XST and Yosys. XST +is used in both cases for the final mapping of logic to LUTs. So this +comparison only compares the high-level synthesis functions (such as FSM +extraction and encoding) of Yosys and XST. + +.. table:: Synthesis results (as reported by XST) for OpenMSP430 and +OpenRISC 1200 + + ============================ ==== ==== ========== ==== ===== + ========== + \ + Module Regs LUTs Max. Freq. Regs LUTs Max. Freq. + openMSP430 689 2210 71 MHz 719 2779 53 MHz + 1em omsp_clock_module 21 30 645 MHz 21 30 644 MHz + 1em 1em omsp_sync_cell 2 — 1542 MHz 2 — 1542 MHz + 1em 1em omsp_sync_reset 2 — 1542 MHz 2 — 1542 MHz + 1em omsp_dbg 143 344 292 MHz 149 430 353 MHz + 1em 1em omsp_dbg_uart 76 135 377 MHz 79 139 389 MHz + 1em omsp_execution_unit 266 911 80 MHz 266 1034 137 MHz + 1em 1em omsp_alu — 202 — — 263 — + 1em 1em omsp_register_file 231 478 285 MHz 231 506 293 MHz + 1em omsp_frontend 115 340 178 MHz 118 527 206 MHz + 1em omsp_mem_backbone 38 141 1087 MHz 38 144 1087 MHz + 1em omsp_multiplier 73 397 129 MHz 102 1053 55 MHz + 1em omsp_sfr 6 18 1023 MHz 6 20 1023 MHz + 1em omsp_watchdog 24 53 362 MHz 24 70 360 MHz + or1200_top 7148 9969 135 MHz 7173 10238 108 MHz + 1em or1200_alu — 681 — — 641 — + 1em or1200_cfgr — 11 — — 11 — + 1em or1200_ctrl 175 186 464 MHz 174 279 377 MHz + 1em or1200_except 241 451 313 MHz 241 353 301 MHz + 1em or1200_freeze 6 18 507 MHz 6 16 515 MHz + 1em or1200_if 68 143 806 MHz 68 139 790 MHz + 1em or1200_lsu 8 138 — 12 205 1306 MHz + 1em 1em or1200_mem2reg — 60 — — 66 — + 1em 1em or1200_reg2mem — 29 — — 29 — + 1em or1200_mult_mac 394 2209 240 MHz 394 2230 241 MHz + 1em 1em or1200_amultp2_32x32 256 1783 240 MHz 256 1770 241 MHz + 1em or1200_operandmuxes 65 129 1145 MHz 65 129 1145 MHz + 1em or1200_rf 1041 1722 822 MHz 1042 1722 581 MHz + 1em or1200_sprs 18 432 724 MHz 18 469 722 MHz + 1em or1200_wbmux 33 93 — 33 78 — + 1em or1200_dc_top — 5 — — 5 — + 1em or1200_dmmu_top 2445 1004 — 2445 1043 — + 1em 1em or1200_dmmu_tlb 2444 975 — 2444 1013 — + 1em or1200_du 67 56 859 MHz 67 56 859 MHz + 1em or1200_ic_top 39 100 527 MHz 41 136 514 MHz + 1em 1em or1200_ic_fsm 40 42 408 MHz 40 75 484 MHz + 1em or1200_pic 38 50 1169 MHz 38 50 1177 MHz + 1em or1200_tt 64 112 370 MHz 64 186 437 MHz + ============================ ==== ==== ========== ==== ===== + ========== + +Conclusion and future Work +-------------------------- + +Yosys is capable of correctly synthesizing real-world Verilog designs. +The generated netlists are of a decent quality. However, in cases where +dedicated hardware resources should be used for certain functions it is +of course necessary to implement proper technology mapping for these +functions in Yosys. This can be as easy as calling the techmap pass with +an architecture-specific mapping file in the synthesis script. As no +such thing has been done in the above tests, it is only natural that the +resulting designs cannot benefit from these dedicated hardware +resources. + +Therefore future work includes the implementation of +architecture-specific technology mappings besides additional frontends +(VHDL), backends (EDIF), and above all else, application specific +passes. After all, this was the main motivation for the development of +Yosys in the first place. + +.. [1] + Most of this test cases are copied from HANA or the ASIC-WORLD + website . + +.. [2] + At the time of this writing 269 test cases. + +.. [3] + At the time of this writing over 6600 test cases. + +.. [4] + A SAT solver is a program that can solve the boolean satisfiability + problem. The built-in SAT solver in Yosys can be used for formal + equivalence checking, amongst other things. See + Sec. \ \ `[cmd:sat] <#cmd:sat>`__ for details. + +.. footbibliography:: diff --git a/docs/source/CHAPTER_Intro.rst b/docs/source/CHAPTER_Intro.rst new file mode 100644 index 000000000..90b001c23 --- /dev/null +++ b/docs/source/CHAPTER_Intro.rst @@ -0,0 +1,96 @@ +.. _chapter:intro: + +Introduction +============ + +This document presents the Free and Open Source (FOSS) Verilog HDL synthesis +tool "Yosys". Its design and implementation as well as its performance on +real-world designs is discussed in this document. + +History of Yosys +---------------- + +A Hardware Description Language (HDL) is a computer language used to describe +circuits. A HDL synthesis tool is a computer program that takes a formal +description of a circuit written in an HDL as input and generates a netlist that +implements the given circuit as output. + +Currently the most widely used and supported HDLs for digital circuits are +Verilog :cite:p:`Verilog2005,VerilogSynth` and :abbr:`VHDL (VHSIC HDL, where +VHSIC is an acronym for Very-High-Speed Integrated Circuits)` +:cite:p:`VHDL,VHDLSynth`. Both HDLs are used for test and verification purposes +as well as logic synthesis, resulting in a set of synthesizable and a set of +non-synthesizable language features. In this document we only look at the +synthesizable subset of the language features. + +In recent work on heterogeneous coarse-grain reconfigurable logic +:cite:p:`intersynth` the need for a custom application-specific HDL synthesis +tool emerged. It was soon realised that a synthesis tool that understood Verilog +or VHDL would be preferred over a synthesis tool for a custom HDL. Given an +existing Verilog or VHDL front end, the work for writing the necessary +additional features and integrating them in an existing tool can be estimated to +be about the same as writing a new tool with support for a minimalistic custom +HDL. + +The proposed custom HDL synthesis tool should be licensed under a Free and Open +Source Software (FOSS) licence. So an existing FOSS Verilog or VHDL synthesis +tool would have been needed as basis to build upon. The main advantages of +choosing Verilog or VHDL is the ability to synthesize existing HDL code and to +mitigate the requirement for circuit-designers to learn a new language. In order +to take full advantage of any existing FOSS Verilog or VHDL tool, such a tool +would have to provide a feature-complete implementation of the synthesizable HDL +subset. + +Basic RTL synthesis is a well understood field :cite:p:`LogicSynthesis`. Lexing, +parsing and processing of computer languages :cite:p:`Dragonbook` is a +thoroughly researched field. All the information required to write such tools +has been openly available for a long time, and it is therefore likely that a +FOSS HDL synthesis tool with a feature-complete Verilog or VHDL front end must +exist which can be used as a basis for a custom RTL synthesis tool. + +Due to the author's preference for Verilog over VHDL it was decided early on to +go for Verilog instead of VHDL [#]_. So the existing FOSS Verilog synthesis +tools were evaluated. The results of this evaluation are utterly devastating. +Therefore a completely new Verilog synthesis tool was implemented and is +recommended as basis for custom synthesis tools. This is the tool that is +discussed in this document. + +Structure of this document +-------------------------- + +The structure of this document is as follows: + +:numref:`Chapter %s ` is this introduction. + +:numref:`Chapter %s ` covers a short introduction to the world +of HDL synthesis. Basic principles and the terminology are outlined in this +chapter. + +:numref:`Chapter %s ` gives the quickest possible outline to +how the problem of implementing a HDL synthesis tool is approached in the case +of Yosys. + +:numref:`Chapter %s ` contains a more detailed overview of the +implementation of Yosys. This chapter covers the data structures used in Yosys +to represent a design in detail and is therefore recommended reading for +everyone who is interested in understanding the Yosys internals. + +:numref:`Chapter %s ` covers the internal cell library used by +Yosys. This is especially important knowledge for anyone who wants to understand +the intermediate netlists used internally by Yosys. + +:numref:`Chapter %s ` gives a tour to the internal APIs of Yosys. +This is recommended reading for everyone who actually wants to read or write +Yosys source code. The chapter concludes with an example loadable module for +Yosys. + +Chapters :numref:`%s `, :numref:`%s ` and +:numref:`%s ` cover three important pieces of the synthesis +pipeline: The Verilog frontend, the optimization passes and the technology +mapping to the target architecture, respectively. + +Various appendices, including a :ref:`cmd_ref`, complete this document. + +.. [#] + A quick investigation into FOSS VHDL tools yielded similar grim results for + FOSS VHDL synthesis tools. diff --git a/docs/source/CHAPTER_Optimize.rst b/docs/source/CHAPTER_Optimize.rst new file mode 100644 index 000000000..53e0a67aa --- /dev/null +++ b/docs/source/CHAPTER_Optimize.rst @@ -0,0 +1,330 @@ +.. _chapter:opt: + +Optimizations +============= + +Yosys employs a number of optimizations to generate better and cleaner results. +This chapter outlines these optimizations. + +Simple optimizations +-------------------- + +The Yosys pass opt runs a number of simple optimizations. This includes removing +unused signals and cells and const folding. It is recommended to run this pass +after each major step in the synthesis script. At the time of this writing the +opt pass executes the following passes that each perform a simple optimization: + +- Once at the beginning of opt: + + - opt_expr + - opt_merge -nomux + +- Repeat until result is stable: + + - opt_muxtree + - opt_reduce + - opt_merge + - opt_rmdff + - opt_clean + - opt_expr + +The following section describes each of the opt\_ passes. + +The opt_expr pass +~~~~~~~~~~~~~~~~~ + +This pass performs const folding on the internal combinational cell types +described in :numref:`Chap. %s `. This means a cell with all +constant inputs is replaced with the constant value this cell drives. In some +cases this pass can also optimize cells with some constant inputs. + +.. table:: Const folding rules for $_AND\_ cells as used in opt_expr. + :name: tab:opt_expr_and + :align: center + + ========= ========= =========== + A-Input B-Input Replacement + ========= ========= =========== + any 0 0 + 0 any 0 + 1 1 1 + --------- --------- ----------- + X/Z X/Z X + 1 X/Z X + X/Z 1 X + --------- --------- ----------- + any X/Z 0 + X/Z any 0 + --------- --------- ----------- + :math:`a` 1 :math:`a` + 1 :math:`b` :math:`b` + ========= ========= =========== + +.. How to format table? + +:numref:`Table %s ` shows the replacement rules used for +optimizing an $_AND\_ gate. The first three rules implement the obvious const +folding rules. Note that ‘any' might include dynamic values calculated by other +parts of the circuit. The following three lines propagate undef (X) states. +These are the only three cases in which it is allowed to propagate an undef +according to Sec. 5.1.10 of IEEE Std. 1364-2005 :cite:p:`Verilog2005`. + +The next two lines assume the value 0 for undef states. These two rules are only +used if no other substitutions are possible in the current module. If other +substitutions are possible they are performed first, in the hope that the ‘any' +will change to an undef value or a 1 and therefore the output can be set to +undef. + +The last two lines simply replace an $_AND\_ gate with one constant-1 input with +a buffer. + +Besides this basic const folding the opt_expr pass can replace 1-bit wide $eq +and $ne cells with buffers or not-gates if one input is constant. + +The opt_expr pass is very conservative regarding optimizing $mux cells, as these +cells are often used to model decision-trees and breaking these trees can +interfere with other optimizations. + +The opt_muxtree pass +~~~~~~~~~~~~~~~~~~~~ + +This pass optimizes trees of multiplexer cells by analyzing the select inputs. +Consider the following simple example: + +.. code:: verilog + :number-lines: + + module uut(a, y); input a; output [1:0] y = a ? (a ? 1 : 2) : 3; endmodule + +The output can never be 2, as this would require ``a`` to be 1 for the outer +multiplexer and 0 for the inner multiplexer. The opt_muxtree pass detects this +contradiction and replaces the inner multiplexer with a constant 1, yielding the +logic for ``y = a ? 1 : 3``. + +The opt_reduce pass +~~~~~~~~~~~~~~~~~~~ + +This is a simple optimization pass that identifies and consolidates identical +input bits to $reduce_and and $reduce_or cells. It also sorts the input bits to +ease identification of shareable $reduce_and and $reduce_or cells in other +passes. + +This pass also identifies and consolidates identical inputs to multiplexer +cells. In this case the new shared select bit is driven using a $reduce_or cell +that combines the original select bits. + +Lastly this pass consolidates trees of $reduce_and cells and trees of $reduce_or +cells to single large $reduce_and or $reduce_or cells. + +These three simple optimizations are performed in a loop until a stable result +is produced. + +The opt_rmdff pass +~~~~~~~~~~~~~~~~~~ + +This pass identifies single-bit d-type flip-flops ($_DFF\_, $dff, and $adff +cells) with a constant data input and replaces them with a constant driver. + +The opt_clean pass +~~~~~~~~~~~~~~~~~~ + +This pass identifies unused signals and cells and removes them from the design. +It also creates an ``\unused_bits`` attribute on wires with unused bits. This +attribute can be used for debugging or by other optimization passes. + +The opt_merge pass +~~~~~~~~~~~~~~~~~~ + +This pass performs trivial resource sharing. This means that this pass +identifies cells with identical inputs and replaces them with a single instance +of the cell. + +The option -nomux can be used to disable resource sharing for multiplexer cells +($mux and $pmux. This can be useful as it prevents multiplexer trees to be +merged, which might prevent opt_muxtree to identify possible optimizations. + +FSM extraction and encoding +--------------------------- + +The fsm pass performs finite-state-machine (FSM) extraction and recoding. The +fsm pass simply executes the following other passes: + +- Identify and extract FSMs: + + - fsm_detect + - fsm_extract + +- Basic optimizations: + + - fsm_opt + - opt_clean + - fsm_opt + +- Expanding to nearby gate-logic (if called with -expand): + + - fsm_expand + - opt_clean + - fsm_opt + +- Re-code FSM states (unless called with -norecode): + + - fsm_recode + +- Print information about FSMs: + + - fsm_info + +- Export FSMs in KISS2 file format (if called with -export): + + - fsm_export + +- Map FSMs to RTL cells (unless called with -nomap): + + - fsm_map + +The fsm_detect pass identifies FSM state registers and marks them using the +``\fsm_encoding = "auto"`` attribute. The fsm_extract extracts all FSMs marked +using the ``\fsm_encoding`` attribute (unless ``\fsm_encoding`` is set to +"none") and replaces the corresponding RTL cells with a $fsm cell. All other +fsm\_ passes operate on these $fsm cells. The fsm_map call finally replaces the +$fsm cells with RTL cells. + +Note that these optimizations operate on an RTL netlist. I.e. the fsm pass +should be executed after the proc pass has transformed all RTLIL::Process +objects to RTL cells. + +The algorithms used for FSM detection and extraction are influenced by a more +general reported technique :cite:p:`fsmextract`. + +FSM detection +~~~~~~~~~~~~~ + +The fsm_detect pass identifies FSM state registers. It sets the ``\fsm_encoding += "auto"`` attribute on any (multi-bit) wire that matches the following +description: + +- Does not already have the ``\fsm_encoding`` attribute. +- Is not an output of the containing module. +- Is driven by single $dff or $adff cell. +- The ``\D``-Input of this $dff or $adff cell is driven by a multiplexer tree + that only has constants or the old state value on its leaves. +- The state value is only used in the said multiplexer tree or by simple + relational cells that compare the state value to a constant (usually $eq + cells). + +This heuristic has proven to work very well. It is possible to overwrite it by +setting ``\fsm_encoding = "auto"`` on registers that should be considered FSM +state registers and setting ``\fsm_encoding = "none"`` on registers that match +the above criteria but should not be considered FSM state registers. + +Note however that marking state registers with ``\fsm_encoding`` that are not +suitable for FSM recoding can cause synthesis to fail or produce invalid +results. + +FSM extraction +~~~~~~~~~~~~~~ + +The fsm_extract pass operates on all state signals marked with the +(``\fsm_encoding != "none"``) attribute. For each state signal the following +information is determined: + +- The state registers + +- The asynchronous reset state if the state registers use asynchronous reset + +- All states and the control input signals used in the state transition + functions + +- The control output signals calculated from the state signals and control + inputs + +- A table of all state transitions and corresponding control inputs- and + outputs + +The state registers (and asynchronous reset state, if applicable) is simply +determined by identifying the driver for the state signal. + +From there the $mux-tree driving the state register inputs is recursively +traversed. All select inputs are control signals and the leaves of the $mux-tree +are the states. The algorithm fails if a non-constant leaf that is not the state +signal itself is found. + +The list of control outputs is initialized with the bits from the state signal. +It is then extended by adding all values that are calculated by cells that +compare the state signal with a constant value. + +In most cases this will cover all uses of the state register, thus rendering the +state encoding arbitrary. If however a design uses e.g. a single bit of the +state value to drive a control output directly, this bit of the state signal +will be transformed to a control output of the same value. + +Finally, a transition table for the FSM is generated. This is done by using the +ConstEval C++ helper class (defined in kernel/consteval.h) that can be used to +evaluate parts of the design. The ConstEval class can be asked to calculate a +given set of result signals using a set of signal-value assignments. It can also +be passed a list of stop-signals that abort the ConstEval algorithm if the value +of a stop-signal is needed in order to calculate the result signals. + +The fsm_extract pass uses the ConstEval class in the following way to create a +transition table. For each state: + +1. Create a ConstEval object for the module containing the FSM +2. Add all control inputs to the list of stop signals +3. Set the state signal to the current state +4. Try to evaluate the next state and control output +5. If step 4 was not successful: + + - Recursively goto step 4 with the offending stop-signal set to 0. + - Recursively goto step 4 with the offending stop-signal set to 1. + +6. If step 4 was successful: Emit transition + +Finally a $fsm cell is created with the generated transition table and added to +the module. This new cell is connected to the control signals and the old +drivers for the control outputs are disconnected. + +FSM optimization +~~~~~~~~~~~~~~~~ + +The fsm_opt pass performs basic optimizations on $fsm cells (not including state +recoding). The following optimizations are performed (in this order): + +- Unused control outputs are removed from the $fsm cell. The attribute + ``\unused_bits`` (that is usually set by the opt_clean pass) is used to + determine which control outputs are unused. + +- Control inputs that are connected to the same driver are merged. + +- When a control input is driven by a control output, the control input is + removed and the transition table altered to give the same performance without + the external feedback path. + +- Entries in the transition table that yield the same output and only differ in + the value of a single control input bit are merged and the different bit is + removed from the sensitivity list (turned into a don't-care bit). + +- Constant inputs are removed and the transition table is altered to give an + unchanged behaviour. + +- Unused inputs are removed. + +FSM recoding +~~~~~~~~~~~~ + +The fsm_recode pass assigns new bit pattern to the states. Usually this also +implies a change in the width of the state signal. At the moment of this writing +only one-hot encoding with all-zero for the reset state is supported. + +The fsm_recode pass can also write a text file with the changes performed by it +that can be used when verifying designs synthesized by Yosys using Synopsys +Formality . + +Logic optimization +------------------ + +Yosys can perform multi-level combinational logic optimization on gate-level +netlists using the external program ABC . The abc pass extracts the +combinational gate-level parts of the design, passes it through ABC, and +re-integrates the results. The abc pass can also be used to perform other +operations using ABC, such as technology mapping (see :numref:`Sec %s +` for details). diff --git a/docs/source/CHAPTER_Overview.rst b/docs/source/CHAPTER_Overview.rst new file mode 100644 index 000000000..10d2ce478 --- /dev/null +++ b/docs/source/CHAPTER_Overview.rst @@ -0,0 +1,571 @@ +.. _chapter:overview: + +Implementation overview +======================= + +Yosys is an extensible open source hardware synthesis tool. It is aimed at +designers who are looking for an easily accessible, universal, and +vendor-independent synthesis tool, as well as scientists who do research in +electronic design automation (EDA) and are looking for an open synthesis +framework that can be used to test algorithms on complex real-world designs. + +Yosys can synthesize a large subset of Verilog 2005 and has been tested with a +wide range of real-world designs, including the `OpenRISC 1200 CPU`_, the +`openMSP430 CPU`_, the `OpenCores I2C master`_, and the `k68 CPU`_. + +.. _OpenRISC 1200 CPU: https://github.com/openrisc/or1200 + +.. _openMSP430 CPU: http://opencores.org/projects/openmsp430 + +.. _OpenCores I2C master: http://opencores.org/projects/i2c + +.. _k68 CPU: http://opencores.org/projects/k68 + +As of this writing a Yosys VHDL frontend is in development. + +Yosys is written in C++ (using some features from the new C++11 standard). This +chapter describes some of the fundamental Yosys data structures. For the sake of +simplicity the C++ type names used in the Yosys implementation are used in this +chapter, even though the chapter only explains the conceptual idea behind it and +can be used as reference to implement a similar system in any language. + +Simplified data flow +-------------------- + +:numref:`Figure %s ` shows the simplified data flow within +Yosys. Rectangles in the figure represent program modules and ellipses internal +data structures that are used to exchange design data between the program +modules. + +Design data is read in using one of the frontend modules. The high-level HDL +frontends for Verilog and VHDL code generate an abstract syntax tree (AST) that +is then passed to the AST frontend. Note that both HDL frontends use the same +AST representation that is powerful enough to cover the Verilog HDL and VHDL +language. + +The AST Frontend then compiles the AST to Yosys's main internal data format, the +RTL Intermediate Language (RTLIL). A more detailed description of this format is +given in the next section. + +There is also a text representation of the RTLIL data structure that can be +parsed using the RTLIL Frontend. + +The design data may then be transformed using a series of passes that all +operate on the RTLIL representation of the design. + +Finally the design in RTLIL representation is converted back to text by one of +the backends, namely the Verilog Backend for generating Verilog netlists and the +RTLIL Backend for writing the RTLIL data in the same format that is understood +by the RTLIL Frontend. + +With the exception of the AST Frontend, which is called by the high-level HDL +frontends and can't be called directly by the user, all program modules are +called by the user (usually using a synthesis script that contains text commands +for Yosys). + +By combining passes in different ways and/or adding additional passes to Yosys +it is possible to adapt Yosys to a wide range of applications. For this to be +possible it is key that (1) all passes operate on the same data structure +(RTLIL) and (2) that this data structure is powerful enough to represent the +design in different stages of the synthesis. + +.. figure:: ../images/overview_flow.* + :class: width-helper + :name: fig:Overview_flow + + Yosys simplified data flow (ellipses: data structures, rectangles: + program modules) + +The RTL Intermediate Language (RTLIL) +------------------------------------- + +All frontends, passes and backends in Yosys operate on a design in RTLIL +representation. The only exception are the high-level frontends that use the AST +representation as an intermediate step before generating RTLIL data. + +In order to avoid reinventing names for the RTLIL classes, they are simply +referred to by their full C++ name, i.e. including the RTLIL:: namespace prefix, +in this document. + +:numref:`Figure %s ` shows a simplified Entity-Relationship +Diagram (ER Diagram) of RTLIL. In :math:`1:N` relationships the arrow points +from the :math:`N` side to the :math:`1`. For example one RTLIL::Design contains +:math:`N` (zero to many) instances of RTLIL::Module. A two-pointed arrow +indicates a :math:`1:1` relationship. + +The RTLIL::Design is the root object of the RTLIL data structure. There is +always one "current design" in memory which passes operate on, frontends add +data to and backends convert to exportable formats. But in some cases passes +internally generate additional RTLIL::Design objects. For example when a pass is +reading an auxiliary Verilog file such as a cell library, it might create an +additional RTLIL::Design object and call the Verilog frontend with this other +object to parse the cell library. + +.. figure:: ../images/overview_rtlil.* + :class: width-helper + :name: fig:Overview_RTLIL + + Simplified RTLIL Entity-Relationship Diagram + +There is only one active RTLIL::Design object that is used by all frontends, +passes and backends called by the user, e.g. using a synthesis script. The +RTLIL::Design then contains zero to many RTLIL::Module objects. This corresponds +to modules in Verilog or entities in VHDL. Each module in turn contains objects +from three different categories: + +- RTLIL::Cell and RTLIL::Wire objects represent classical netlist data. + +- RTLIL::Process objects represent the decision trees (if-then-else statements, + etc.) and synchronization declarations (clock signals and sensitivity) from + Verilog always and VHDL process blocks. + +- RTLIL::Memory objects represent addressable memories (arrays). + +Usually the output of the synthesis procedure is a netlist, i.e. all +RTLIL::Process and RTLIL::Memory objects must be replaced by RTLIL::Cell and +RTLIL::Wire objects by synthesis passes. + +All features of the HDL that cannot be mapped directly to these RTLIL classes +must be transformed to an RTLIL-compatible representation by the HDL frontend. +This includes Verilog-features such as generate-blocks, loops and parameters. + +The following sections contain a more detailed description of the different +parts of RTLIL and rationale behind some of the design decisions. + +RTLIL identifiers +~~~~~~~~~~~~~~~~~ + +All identifiers in RTLIL (such as module names, port names, signal names, cell +types, etc.) follow the following naming convention: they must either start with +a backslash (\) or a dollar sign ($). + +Identifiers starting with a backslash are public visible identifiers. Usually +they originate from one of the HDL input files. For example the signal name +"\\sig42" is most likely a signal that was declared using the name "sig42" in an +HDL input file. On the other hand the signal name "$sig42" is an auto-generated +signal name. The backends convert all identifiers that start with a dollar sign +to identifiers that do not collide with identifiers that start with a backslash. + +This has three advantages: + +- First, it is impossible that an auto-generated identifier collides with an + identifier that was provided by the user. + +- Second, the information about which identifiers were originally provided by + the user is always available which can help guide some optimizations. For + example the "opt_rmunused" tries to preserve signals with a user-provided + name but doesn't hesitate to delete signals that have auto-generated names + when they just duplicate other signals. + +- Third, the delicate job of finding suitable auto-generated public visible + names is deferred to one central location. Internally auto-generated names + that may hold important information for Yosys developers can be used without + disturbing external tools. For example the Verilog backend assigns names in + the form \_integer\_. + +Whitespace and control characters (any character with an ASCII code 32 or less) +are not allowed in RTLIL identifiers; most frontends and backends cannot support +these characters in identifiers. + +In order to avoid programming errors, the RTLIL data structures check if all +identifiers start with either a backslash or a dollar sign, and contain no +whitespace or control characters. Violating these rules results in a runtime +error. + +All RTLIL identifiers are case sensitive. + +Some transformations, such as flattening, may have to change identifiers +provided by the user to avoid name collisions. When that happens, attribute +"hdlname" is attached to the object with the changed identifier. This attribute +contains one name (if emitted directly by the frontend, or is a result of +disambiguation) or multiple names separated by spaces (if a result of +flattening). All names specified in the "hdlname" attribute are public and do +not include the leading "\". + +RTLIL::Design and RTLIL::Module +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The RTLIL::Design object is basically just a container for RTLIL::Module +objects. In addition to a list of RTLIL::Module objects the RTLIL::Design also +keeps a list of selected objects, i.e. the objects that passes should operate +on. In most cases the whole design is selected and therefore passes operate on +the whole design. But this mechanism can be useful for more complex synthesis +jobs in which only parts of the design should be affected by certain passes. + +Besides the objects shown in the ER diagram in :numref:`Fig. %s +` an RTLIL::Module object contains the following additional +properties: + +- The module name +- A list of attributes +- A list of connections between wires +- An optional frontend callback used to derive parametrized variations of the + module + +The attributes can be Verilog attributes imported by the Verilog frontend or +attributes assigned by passes. They can be used to store additional metadata +about modules or just mark them to be used by certain part of the synthesis +script but not by others. + +Verilog and VHDL both support parametric modules (known as "generic entities" in +VHDL). The RTLIL format does not support parametric modules itself. Instead each +module contains a callback function into the AST frontend to generate a +parametrized variation of the RTLIL::Module as needed. This callback then +returns the auto-generated name of the parametrized variation of the module. (A +hash over the parameters and the module name is used to prohibit the same +parametrized variation from being generated twice. For modules with only a few +parameters, a name directly containing all parameters is generated instead of a +hash string.) + +.. _sec:rtlil_cell_wire: + +RTLIL::Cell and RTLIL::Wire +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A module contains zero to many RTLIL::Cell and RTLIL::Wire objects. Objects of +these types are used to model netlists. Usually the goal of all synthesis +efforts is to convert all modules to a state where the functionality of the +module is implemented only by cells from a given cell library and wires to +connect these cells with each other. Note that module ports are just wires with +a special property. + +An RTLIL::Wire object has the following properties: + +- The wire name +- A list of attributes +- A width (buses are just wires with a width > 1) +- Bus direction (MSB to LSB or vice versa) +- Lowest valid bit index (LSB or MSB depending on bus direction) +- If the wire is a port: port number and direction (input/output/inout) + +As with modules, the attributes can be Verilog attributes imported by the +Verilog frontend or attributes assigned by passes. + +In Yosys, busses (signal vectors) are represented using a single wire object +with a width > 1. So Yosys does not convert signal vectors to individual +signals. This makes some aspects of RTLIL more complex but enables Yosys to be +used for coarse grain synthesis where the cells of the target architecture +operate on entire signal vectors instead of single bit wires. + +In Verilog and VHDL, busses may have arbitrary bounds, and LSB can have either +the lowest or the highest bit index. In RTLIL, bit 0 always corresponds to LSB; +however, information from the HDL frontend is preserved so that the bus will be +correctly indexed in error messages, backend output, constraint files, etc. + +An RTLIL::Cell object has the following properties: + +- The cell name and type +- A list of attributes +- A list of parameters (for parametric cells) +- Cell ports and the connections of ports to wires and constants + +The connections of ports to wires are coded by assigning an RTLIL::SigSpec to +each cell port. The RTLIL::SigSpec data type is described in the next section. + +.. _sec:rtlil_sigspec: + +RTLIL::SigSpec +~~~~~~~~~~~~~~ + +A "signal" is everything that can be applied to a cell port. I.e. + +- | Any constant value of arbitrary bit-width + | 1em For example: ``1337, 16'b0000010100111001, 1'b1, 1'bx`` + +- | All bits of a wire or a selection of bits from a wire + | 1em For example: ``mywire, mywire[24], mywire[15:8]`` + +- | Concatenations of the above + | 1em For example: ``{16'd1337, mywire[15:8]}`` + +The RTLIL::SigSpec data type is used to represent signals. The RTLIL::Cell +object contains one RTLIL::SigSpec for each cell port. + +In addition, connections between wires are represented using a pair of +RTLIL::SigSpec objects. Such pairs are needed in different locations. Therefore +the type name RTLIL::SigSig was defined for such a pair. + +.. _sec:rtlil_process: + +RTLIL::Process +~~~~~~~~~~~~~~ + +When a high-level HDL frontend processes behavioural code it splits it up into +data path logic (e.g. the expression a + b is replaced by the output of an adder +that takes a and b as inputs) and an RTLIL::Process that models the control +logic of the behavioural code. Let's consider a simple example: + +.. code:: verilog + :number-lines: + + module ff_with_en_and_async_reset(clock, reset, enable, d, q); + input clock, reset, enable, d; + output reg q; + always @(posedge clock, posedge reset) + if (reset) + q <= 0; + else if (enable) + q <= d; + endmodule + +In this example there is no data path and therefore the RTLIL::Module generated +by the frontend only contains a few RTLIL::Wire objects and an RTLIL::Process. +The RTLIL::Process in RTLIL syntax: + +.. code:: RTLIL + :number-lines: + + process $proc$ff_with_en_and_async_reset.v:4$1 + assign $0\q[0:0] \q + switch \reset + case 1'1 + assign $0\q[0:0] 1'0 + case + switch \enable + case 1'1 + assign $0\q[0:0] \d + case + end + end + sync posedge \clock + update \q $0\q[0:0] + sync posedge \reset + update \q $0\q[0:0] + end + +This RTLIL::Process contains two RTLIL::SyncRule objects, two RTLIL::SwitchRule +objects and five RTLIL::CaseRule objects. The wire $0\q[0:0] is an automatically +created wire that holds the next value of \\q. The lines :math:`2 \dots 12` +describe how $0\q[0:0] should be calculated. The lines :math:`13 \dots 16` +describe how the value of $0\q[0:0] is used to update \\q. + +An RTLIL::Process is a container for zero or more RTLIL::SyncRule objects and +exactly one RTLIL::CaseRule object, which is called the root case. + +An RTLIL::SyncRule object contains an (optional) synchronization condition +(signal and edge-type), zero or more assignments (RTLIL::SigSig), and zero or +more memory writes (RTLIL::MemWriteAction). The always synchronization condition +is used to break combinatorial loops when a latch should be inferred instead. + +An RTLIL::CaseRule is a container for zero or more assignments (RTLIL::SigSig) +and zero or more RTLIL::SwitchRule objects. An RTLIL::SwitchRule objects is a +container for zero or more RTLIL::CaseRule objects. + +In the above example the lines :math:`2 \dots 12` are the root case. Here +$0\q[0:0] is first assigned the old value \\q as default value (line 2). The +root case also contains an RTLIL::SwitchRule object (lines :math:`3 \dots 12`). +Such an object is very similar to the C switch statement as it uses a control +signal (\\reset in this case) to determine which of its cases should be active. +The RTLIL::SwitchRule object then contains one RTLIL::CaseRule object per case. +In this example there is a case [1]_ for \\reset == 1 that causes $0\q[0:0] to +be set (lines 4 and 5) and a default case that in turn contains a switch that +sets $0\q[0:0] to the value of \\d if \\enable is active (lines :math:`6 \dots +11`). + +A case can specify zero or more compare values that will determine whether it +matches. Each of the compare values must be the exact same width as the control +signal. When more than one compare value is specified, the case matches if any +of them matches the control signal; when zero compare values are specified, the +case always matches (i.e. it is the default case). + +A switch prioritizes cases from first to last: multiple cases can match, but +only the first matched case becomes active. This normally synthesizes to a +priority encoder. The parallel_case attribute allows passes to assume that no +more than one case will match, and full_case attribute allows passes to assume +that exactly one case will match; if these invariants are ever dynamically +violated, the behavior is undefined. These attributes are useful when an +invariant invisible to the synthesizer causes the control signal to never take +certain bit patterns. + +The lines :math:`13 \dots 16` then cause \\q to be updated whenever there is a +positive clock edge on \\clock or \\reset. + +In order to generate such a representation, the language frontend must be able +to handle blocking and nonblocking assignments correctly. However, the language +frontend does not need to identify the correct type of storage element for the +output signal or generate multiplexers for the decision tree. This is done by +passes that work on the RTLIL representation. Therefore it is relatively easy to +substitute these steps with other algorithms that target different target +architectures or perform optimizations or other transformations on the decision +trees before further processing them. + +One of the first actions performed on a design in RTLIL representation in most +synthesis scripts is identifying asynchronous resets. This is usually done using +the proc_arst pass. This pass transforms the above example to the following +RTLIL::Process: + +.. code:: RTLIL + :number-lines: + + process $proc$ff_with_en_and_async_reset.v:4$1 + assign $0\q[0:0] \q + switch \enable + case 1'1 + assign $0\q[0:0] \d + case + end + sync posedge \clock + update \q $0\q[0:0] + sync high \reset + update \q 1'0 + end + +This pass has transformed the outer RTLIL::SwitchRule into a modified +RTLIL::SyncRule object for the \\reset signal. Further processing converts the +RTLIL::Process into e.g. a d-type flip-flop with asynchronous reset and a +multiplexer for the enable signal: + +.. code:: RTLIL + :number-lines: + + cell $adff $procdff$6 + parameter \ARST_POLARITY 1'1 + parameter \ARST_VALUE 1'0 + parameter \CLK_POLARITY 1'1 + parameter \WIDTH 1 + connect \ARST \reset + connect \CLK \clock + connect \D $0\q[0:0] + connect \Q \q + end + cell $mux $procmux$3 + parameter \WIDTH 1 + connect \A \q + connect \B \d + connect \S \enable + connect \Y $0\q[0:0] + end + +Different combinations of passes may yield different results. Note that $adff +and $mux are internal cell types that still need to be mapped to cell types from +the target cell library. + +Some passes refuse to operate on modules that still contain RTLIL::Process +objects as the presence of these objects in a module increases the complexity. +Therefore the passes to translate processes to a netlist of cells are usually +called early in a synthesis script. The proc pass calls a series of other passes +that together perform this conversion in a way that is suitable for most +synthesis tasks. + +.. _sec:rtlil_memory: + +RTLIL::Memory +~~~~~~~~~~~~~ + +For every array (memory) in the HDL code an RTLIL::Memory object is created. A +memory object has the following properties: + +- The memory name +- A list of attributes +- The width of an addressable word +- The size of the memory in number of words + +All read accesses to the memory are transformed to $memrd cells and all write +accesses to $memwr cells by the language frontend. These cells consist of +independent read- and write-ports to the memory. Memory initialization is +transformed to $meminit cells by the language frontend. The ``\MEMID`` parameter +on these cells is used to link them together and to the RTLIL::Memory object +they belong to. + +The rationale behind using separate cells for the individual ports versus +creating a large multiport memory cell right in the language frontend is that +the separate $memrd and $memwr cells can be consolidated using resource sharing. +As resource sharing is a non-trivial optimization problem where different +synthesis tasks can have different requirements it lends itself to do the +optimisation in separate passes and merge the RTLIL::Memory objects and $memrd +and $memwr cells to multiport memory blocks after resource sharing is completed. + +The memory pass performs this conversion and can (depending on the options +passed to it) transform the memories directly to d-type flip-flops and address +logic or yield multiport memory blocks (represented using $mem cells). + +See :numref:`Sec. %s ` for details about the memory cell types. + +Command interface and synthesis scripts +--------------------------------------- + +Yosys reads and processes commands from synthesis scripts, command line +arguments and an interactive command prompt. Yosys commands consist of a command +name and an optional whitespace separated list of arguments. Commands are +terminated using the newline character or a semicolon (;). Empty lines and lines +starting with the hash sign (#) are ignored. See :numref:`Sec. %s +` for an example synthesis script. + +The command help can be used to access the command reference manual. + +Most commands can operate not only on the entire design but also specifically on +selected parts of the design. For example the command dump will print all +selected objects in the current design while dump foobar will only print the +module foobar and dump \* will print the entire design regardless of the current +selection. + +.. code:: yoscrypt + + dump */t:$add %x:+[A] \*/w:\* %i + +The selection mechanism is very powerful. For example the command above will +print all wires that are connected to the ``\A`` port of a ``$add`` cell. +Detailed documentation of the select framework can be found in the command +reference for the ``select`` command. + +Source tree and build system +---------------------------- + +The Yosys source tree is organized into the following top-level +directories: + +- | backends/ + | This directory contains a subdirectory for each of the backend modules. + +- | frontends/ + | This directory contains a subdirectory for each of the frontend modules. + +- | kernel/ + | This directory contains all the core functionality of Yosys. This includes + the functions and definitions for working with the RTLIL data structures + (rtlil.h and rtlil.cc), the main() function (driver.cc), the internal + framework for generating log messages (log.h and log.cc), the internal + framework for registering and calling passes (register.h and register.cc), + some core commands that are not really passes (select.cc, show.cc, …) and a + couple of other small utility libraries. + +- | passes/ + | This directory contains a subdirectory for each pass or group of passes. + For example as of this writing the directory passes/opt/ contains the code + for seven passes: opt, opt_expr, opt_muxtree, opt_reduce, opt_rmdff, + opt_rmunused and opt_merge. + +- | techlibs/ + | This directory contains simulation models and standard implementations for + the cells from the internal cell library. + +- | tests/ + | This directory contains a couple of test cases. Most of the smaller tests + are executed automatically when make test is called. The larger tests must + be executed manually. Most of the larger tests require downloading external + HDL source code and/or external tools. The tests range from comparing + simulation results of the synthesized design to the original sources to + logic equivalence checking of entire CPU cores. + +The top-level Makefile includes frontends/\*/Makefile.inc, +passes/\*/Makefile.inc and backends/\*/Makefile.inc. So when extending Yosys it +is enough to create a new directory in frontends/, passes/ or backends/ with +your sources and a Makefile.inc. The Yosys kernel automatically detects all +commands linked with Yosys. So it is not needed to add additional commands to a +central list of commands. + +Good starting points for reading example source code to learn how to write +passes are passes/opt/opt_rmdff.cc and passes/opt/opt_merge.cc. + +See the top-level README file for a quick Getting Started guide and build +instructions. The Yosys build is based solely on Makefiles. + +Users of the Qt Creator IDE can generate a QT Creator project file using make +qtcreator. Users of the Eclipse IDE can use the "Makefile Project with Existing +Code" project type in the Eclipse "New Project" dialog (only available after the +CDT plugin has been installed) to create an Eclipse project in order to +programming extensions to Yosys or just browse the Yosys code base. + +.. [1] + The syntax 1'1 in the RTLIL code specifies a constant with a length of one + bit (the first "1"), and this bit is a one (the second "1"). diff --git a/docs/source/CHAPTER_Prog.rst b/docs/source/CHAPTER_Prog.rst new file mode 100644 index 000000000..f706123aa --- /dev/null +++ b/docs/source/CHAPTER_Prog.rst @@ -0,0 +1,46 @@ +.. _chapter:prog: + +Programming Yosys extensions +============================ + +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 YosysHQ Slack. + +Guidelines +---------- + +The guidelines directory contains notes on various aspects of Yosys +development. The files GettingStarted and CodingStyle may be of +particular interest, and are reproduced here. + +.. literalinclude:: ../../guidelines/GettingStarted + :language: none + :caption: guidelines/GettingStarted + +.. literalinclude:: ../../guidelines/CodingStyle + :language: none + :caption: guidelines/CodingStyle + +The "stubsnets" example module +------------------------------ + +The following is the complete code of the "stubsnets" example module. It +is included in the Yosys source distribution as +manual/CHAPTER_Prog/stubnets.cc. + +.. literalinclude:: ../../manual/CHAPTER_Prog/stubnets.cc + :language: c++ + :linenos: + :caption: manual/CHAPTER_Prog/stubnets.cc + +.. literalinclude:: ../../manual/CHAPTER_Prog/Makefile + :language: makefile + :linenos: + :caption: manual/CHAPTER_Prog/Makefile + +.. literalinclude:: ../../manual/CHAPTER_Prog/test.v + :language: verilog + :linenos: + :caption: manual/CHAPTER_Prog/test.v diff --git a/docs/source/CHAPTER_Techmap.rst b/docs/source/CHAPTER_Techmap.rst new file mode 100644 index 000000000..6cd1eb44f --- /dev/null +++ b/docs/source/CHAPTER_Techmap.rst @@ -0,0 +1,105 @@ +.. _chapter:techmap: + +Technology mapping +================== + +Previous chapters outlined how HDL code is transformed into an RTL netlist. The +RTL netlist is still based on abstract coarse-grain cell types like arbitrary +width adders and even multipliers. This chapter covers how an RTL netlist is +transformed into a functionally equivalent netlist utilizing the cell types +available in the target architecture. + +Technology mapping is often performed in two phases. In the first phase RTL +cells are mapped to an internal library of single-bit cells (see :numref:`Sec. +%s `). In the second phase this netlist of internal gate +types is transformed to a netlist of gates from the target technology library. + +When the target architecture provides coarse-grain cells (such as block ram or +ALUs), these must be mapped to directly form the RTL netlist, as information on +the coarse-grain structure of the design is lost when it is mapped to bit-width +gate types. + +Cell substitution +----------------- + +The simplest form of technology mapping is cell substitution, as performed by +the techmap pass. This pass, when provided with a Verilog file that implements +the RTL cell types using simpler cells, simply replaces the RTL cells with the +provided implementation. + +When no map file is provided, techmap uses a built-in map file that maps the +Yosys RTL cell types to the internal gate library used by Yosys. The curious +reader may find this map file as techlibs/common/techmap.v in the Yosys source +tree. + +Additional features have been added to techmap to allow for conditional mapping +of cells (see :doc:`cmd/techmap`). This can for example be useful if the target +architecture supports hardware multipliers for certain bit-widths but not for +others. + +A usual synthesis flow would first use the techmap pass to directly map some RTL +cells to coarse-grain cells provided by the target architecture (if any) and +then use techmap with the built-in default file to map the remaining RTL cells +to gate logic. + +Subcircuit substitution +----------------------- + +Sometimes the target architecture provides cells that are more powerful than the +RTL cells used by Yosys. For example a cell in the target architecture that can +calculate the absolute-difference of two numbers does not match any single RTL +cell type but only combinations of cells. + +For these cases Yosys provides the extract pass that can match a given set of +modules against a design and identify the portions of the design that are +identical (i.e. isomorphic subcircuits) to any of the given modules. These +matched subcircuits are then replaced by instances of the given modules. + +The extract pass also finds basic variations of the given modules, such as +swapped inputs on commutative cell types. + +In addition to this the extract pass also has limited support for frequent +subcircuit mining, i.e. the process of finding recurring subcircuits in the +design. This has a few applications, including the design of new coarse-grain +architectures :cite:p:`intersynthFdlBookChapter`. + +The hard algorithmic work done by the extract pass (solving the isomorphic +subcircuit problem and frequent subcircuit mining) is performed using the +SubCircuit library that can also be used stand-alone without Yosys (see +:ref:`sec:SubCircuit`). + +.. _sec:techmap_extern: + +Gate-level technology mapping +----------------------------- + +On the gate-level the target architecture is usually described by a "Liberty +file". The Liberty file format is an industry standard format that can be used +to describe the behaviour and other properties of standard library cells . + +Mapping a design utilizing the Yosys internal gate library (e.g. as a result of +mapping it to this representation using the techmap pass) is performed in two +phases. + +First the register cells must be mapped to the registers that are available on +the target architectures. The target architecture might not provide all +variations of d-type flip-flops with positive and negative clock edge, +high-active and low-active asynchronous set and/or reset, etc. Therefore the +process of mapping the registers might add additional inverters to the design +and thus it is important to map the register cells first. + +Mapping of the register cells may be performed by using the dfflibmap pass. This +pass expects a Liberty file as argument (using the -liberty option) and only +uses the register cells from the Liberty file. + +Secondly the combinational logic must be mapped to the target architecture. This +is done using the external program ABC via the abc pass by using the -liberty +option to the pass. Note that in this case only the combinatorial cells are used +from the cell library. + +Occasionally Liberty files contain trade secrets (such as sensitive timing +information) that cannot be shared freely. This complicates processes such as +reporting bugs in the tools involved. When the information in the Liberty file +used by Yosys and ABC are not part of the sensitive information, the additional +tool yosys-filterlib (see :ref:`sec:filterlib`) can be used to strip the +sensitive information from the Liberty file. diff --git a/docs/source/CHAPTER_Verilog.rst b/docs/source/CHAPTER_Verilog.rst new file mode 100644 index 000000000..484844fba --- /dev/null +++ b/docs/source/CHAPTER_Verilog.rst @@ -0,0 +1,666 @@ +.. _chapter:verilog: + +The Verilog and AST frontends +============================= + +This chapter provides an overview of the implementation of the Yosys Verilog and +AST frontends. The Verilog frontend reads Verilog-2005 code and creates an +abstract syntax tree (AST) representation of the input. This AST representation +is then passed to the AST frontend that converts it to RTLIL data, as +illustrated in :numref:`Fig. %s `. + +.. figure:: ../images/verilog_flow.* + :class: width-helper + :name: fig:Verilog_flow + + Simplified Verilog to RTLIL data flow + +Transforming Verilog to AST +--------------------------- + +The Verilog frontend converts the Verilog sources to an internal AST +representation that closely resembles the structure of the original +Verilog code. The Verilog frontend consists of three components, the +Preprocessor, the Lexer and the Parser. + +The source code to the Verilog frontend can be found in +frontends/verilog/ in the Yosys source tree. + +The Verilog preprocessor +~~~~~~~~~~~~~~~~~~~~~~~~ + +The Verilog preprocessor scans over the Verilog source code and +interprets some of the Verilog compiler directives such as +:literal:`\`include`, :literal:`\`define` and :literal:`\`ifdef`. + +It is implemented as a C++ function that is passed a file descriptor as +input and returns the pre-processed Verilog code as a ``std::string``. + +The source code to the Verilog Preprocessor can be found in +frontends/verilog/preproc.cc in the Yosys source tree. + +The Verilog lexer +~~~~~~~~~~~~~~~~~ + +The Verilog Lexer is written using the lexer generator flex . Its source +code can be found in frontends/verilog/verilog_lexer.l in the Yosys +source tree. The lexer does little more than identifying all keywords +and literals recognised by the Yosys Verilog frontend. + +The lexer keeps track of the current location in the Verilog source code +using some global variables. These variables are used by the constructor +of AST nodes to annotate each node with the source code location it +originated from. + +Finally the lexer identifies and handles special comments such as +"``// synopsys translate_off``" and "``// synopsys full_case``". (It is +recommended to use :literal:`\`ifdef` constructs instead of the +Synsopsys translate_on/off comments and attributes such as +``(* full_case *)`` over "``// synopsys full_case``" whenever possible.) + +The Verilog parser +~~~~~~~~~~~~~~~~~~ + +The Verilog Parser is written using the parser generator bison . Its +source code can be found in frontends/verilog/verilog_parser.y in the +Yosys source tree. + +It generates an AST using the ``AST::AstNode`` data structure defined in +frontends/ast/ast.h. An ``AST::AstNode`` object has the following +properties: + +.. list-table:: AST node types with their corresponding Verilog constructs. + :name: tab:Verilog_AstNodeType + :widths: 50 50 + + * - AST Node Type + - Corresponding Verilog Construct + * - AST_NONE + - This Node type should never be used. + * - AST_DESIGN + - This node type is used for the top node of the AST tree. It has no corresponding Verilog construct. + * - AST_MODULE, AST_TASK, AST_FUNCTION + - ``module``, ``task`` and ``function`` + * - AST_WIRE + - ``input``, ``output``, ``wire``, ``reg`` and ``integer`` + * - AST_MEMORY + - Verilog Arrays + * - AST_AUTOWIRE + - Created by the simplifier when an undeclared signal name is used. + * - AST_PARAMETER, AST_LOCALPARAM + - ``parameter`` and ``localparam`` + * - AST_PARASET + - Parameter set in cell instantiation + * - AST_ARGUMENT + - Port connection in cell instantiation + * - AST_RANGE + - Bit-Index in a signal or element index in array + * - AST_CONSTANT + - A literal value + * - AST_CELLTYPE + - The type of cell in cell instantiation + * - AST_IDENTIFIER + - An Identifier (signal name in expression or cell/task/etc. name in other contexts) + * - AST_PREFIX + - Construct an identifier in the form []. (used only in advanced generate constructs) + * - AST_FCALL, AST_TCALL + - Call to function or task + * - AST_TO_SIGNED, AST_TO_UNSIGNED + - The ``$signed()`` and ``$unsigned()`` functions + * - AST_CONCAT, AST_REPLICATE + - The ``{...}`` and ``{...{...}}`` operators + * - AST_BIT_NOT, AST_BIT_AND, AST_BIT_OR, AST_BIT_XOR, AST_BIT_XNOR + - The bitwise operators ``~``, ``&``, ``|``, ``^`` and ``~^`` + * - AST_REDUCE_AND, AST_REDUCE_OR, AST_REDUCE_XOR, AST_REDUCE_XNOR + - The unary reduction operators ``~``, ``&``, ``|``, ``^`` and ``~^`` + * - AST_REDUCE_BOOL + - Conversion from multi-bit value to boolean value (equivalent to AST_REDUCE_OR) + * - AST_SHIFT_LEFT, AST_SHIFT_RIGHT, AST_SHIFT_SLEFT, AST_SHIFT_SRIGHT + - The shift operators ``<<``, ``>>``, ``<<<`` and ``>>>`` + * - AST_LT, AST_LE, AST_EQ, AST_NE, AST_GE, AST_GT + - The relational operators ``<``, ``<=``, ``==``, ``!=``, ``>=`` and ``>`` + * - AST_ADD, AST_SUB, AST_MUL, AST_DIV, AST_MOD, AST_POW + - The binary operators ``+``, ``-``, ``*``, ``/``, ``%`` and ``**`` + * - AST_POS, AST_NEG + - The prefix operators ``+`` and ``-`` + * - AST_LOGIC_AND, AST_LOGIC_OR, AST_LOGIC_NOT + - The logic operators ``&&``, ``||`` and ``!`` + * - AST_TERNARY + - The ternary ``?:``-operator + * - AST_MEMRD AST_MEMWR + - Read and write memories. These nodes are generated by the AST simplifier for writes/reads to/from Verilog arrays. + * - AST_ASSIGN + - An ``assign`` statement + * - AST_CELL + - A cell instantiation + * - AST_PRIMITIVE + - A primitive cell (``and``, ``nand``, ``or``, etc.) + * - AST_ALWAYS, AST_INITIAL + - Verilog ``always``- and ``initial``-blocks + * - AST_BLOCK + - A ``begin``-``end``-block + * - AST_ASSIGN_EQ. AST_ASSIGN_LE + - Blocking (``=``) and nonblocking (``<=``) assignments within an ``always``- or ``initial``-block + * - AST_CASE. AST_COND, AST_DEFAULT + - The ``case`` (``if``) statements, conditions within a case and the default case respectively + * - AST_FOR + - A ``for``-loop with an ``always``- or ``initial``-block + * - AST_GENVAR, AST_GENBLOCK, AST_GENFOR, AST_GENIF + - The ``genvar`` and ``generate`` keywords and ``for`` and ``if`` within a generate block. + * - AST_POSEDGE, AST_NEGEDGE, AST_EDGE + - Event conditions for ``always`` blocks. + +- | The node type + | This enum (``AST::AstNodeType``) specifies the role of the node. + :numref:`Table %s ` + contains a list of all node types. + +- | The child nodes + | This is a list of pointers to all children in the abstract syntax + tree. + +- | Attributes + | As almost every AST node might have Verilog attributes assigned to + it, the ``AST::AstNode`` has direct support for attributes. Note + that the attribute values are again AST nodes. + +- | Node content + | Each node might have additional content data. A series of member + variables exist to hold such data. For example the member + ``std::string str`` can hold a string value and is used e.g. in the + AST_IDENTIFIER node type to store the identifier name. + +- | Source code location + | Each ``AST::AstNode`` is automatically annotated with the current + source code location by the ``AST::AstNode`` constructor. It is + stored in the ``std::string filename`` and ``int linenum`` member + variables. + +The ``AST::AstNode`` constructor can be called with up to two child +nodes that are automatically added to the list of child nodes for the +new object. This simplifies the creation of AST nodes for simple +expressions a bit. For example the bison code for parsing +multiplications: + +.. code:: none + :number-lines: + + basic_expr '*' attr basic_expr { + $$ = new AstNode(AST_MUL, $1, $4); + append_attr($$, $3); + } | + +The generated AST data structure is then passed directly to the AST +frontend that performs the actual conversion to RTLIL. + +Note that the Yosys command ``read_verilog`` provides the options ``-yydebug`` +and ``-dump_ast`` that can be used to print the parse tree or abstract +syntax tree respectively. + +Transforming AST to RTLIL +------------------------- + +The AST Frontend converts a set of modules in AST representation to +modules in RTLIL representation and adds them to the current design. +This is done in two steps: simplification and RTLIL generation. + +The source code to the AST frontend can be found in ``frontends/ast/`` in +the Yosys source tree. + +AST simplification +~~~~~~~~~~~~~~~~~~ + +A full-featured AST is too complex to be transformed into RTLIL +directly. Therefore it must first be brought into a simpler form. This +is done by calling the ``AST::AstNode::simplify()`` method of all +AST_MODULE nodes in the AST. This initiates a recursive process that +performs the following transformations on the AST data structure: + +- Inline all task and function calls. + +- Evaluate all ``generate``-statements and unroll all ``for``-loops. + +- Perform const folding where it is necessary (e.g. in the value part + of AST_PARAMETER, AST_LOCALPARAM, AST_PARASET and AST_RANGE nodes). + +- Replace AST_PRIMITIVE nodes with appropriate AST_ASSIGN nodes. + +- Replace dynamic bit ranges in the left-hand-side of assignments with + AST_CASE nodes with AST_COND children for each possible case. + +- Detect array access patterns that are too complicated for the + RTLIL::Memory abstraction and replace them with a set of signals and + cases for all reads and/or writes. + +- Otherwise replace array accesses with AST_MEMRD and AST_MEMWR nodes. + +In addition to these transformations, the simplifier also annotates the +AST with additional information that is needed for the RTLIL generator, +namely: + +- All ranges (width of signals and bit selections) are not only const + folded but (when a constant value is found) are also written to + member variables in the AST_RANGE node. + +- All identifiers are resolved and all AST_IDENTIFIER nodes are + annotated with a pointer to the AST node that contains the + declaration of the identifier. If no declaration has been found, an + AST_AUTOWIRE node is created and used for the annotation. + +This produces an AST that is fairly easy to convert to the RTLIL format. + +Generating RTLIL +~~~~~~~~~~~~~~~~ + +After AST simplification, the ``AST::AstNode::genRTLIL()`` method of +each AST_MODULE node in the AST is called. This initiates a recursive +process that generates equivalent RTLIL data for the AST data. + +The ``AST::AstNode::genRTLIL()`` method returns an ``RTLIL::SigSpec`` +structure. For nodes that represent expressions (operators, constants, +signals, etc.), the cells needed to implement the calculation described +by the expression are created and the resulting signal is returned. That +way it is easy to generate the circuits for large expressions using +depth-first recursion. For nodes that do not represent an expression +(such as AST_CELL), the corresponding circuit is generated and an empty +``RTLIL::SigSpec`` is returned. + +Synthesizing Verilog always blocks +-------------------------------------- + +For behavioural Verilog code (code utilizing ``always``- and +``initial``-blocks) it is necessary to also generate ``RTLIL::Process`` +objects. This is done in the following way: + +Whenever ``AST::AstNode::genRTLIL()`` encounters an ``always``- or +``initial``-block, it creates an instance of +``AST_INTERNAL::ProcessGenerator``. This object then generates the +``RTLIL::Process`` object for the block. It also calls +``AST::AstNode::genRTLIL()`` for all right-hand-side expressions +contained within the block. + +First the ``AST_INTERNAL::ProcessGenerator`` creates a list of all +signals assigned within the block. It then creates a set of temporary +signals using the naming scheme $\ \\\ for each +of the assigned signals. + +Then an ``RTLIL::Process`` is created that assigns all intermediate +values for each left-hand-side signal to the temporary signal in its +``RTLIL::CaseRule``/``RTLIL::SwitchRule`` tree. + +Finally a ``RTLIL::SyncRule`` is created for the ``RTLIL::Process`` that +assigns the temporary signals for the final values to the actual +signals. + +A process may also contain memory writes. A ``RTLIL::MemWriteAction`` is +created for each of them. + +Calls to ``AST::AstNode::genRTLIL()`` are generated for right hand sides +as needed. When blocking assignments are used, +``AST::AstNode::genRTLIL()`` is configured using global variables to use +the temporary signals that hold the correct intermediate values whenever +one of the previously assigned signals is used in an expression. + +Unfortunately the generation of a correct +``RTLIL::CaseRule``/``RTLIL::SwitchRule`` tree for behavioural code is a +non-trivial task. The AST frontend solves the problem using the approach +described on the following pages. The following example illustrates what +the algorithm is supposed to do. Consider the following Verilog code: + +.. code:: verilog + :number-lines: + + always @(posedge clock) begin + out1 = in1; + if (in2) + out1 = !out1; + out2 <= out1; + if (in3) + out2 <= out2; + if (in4) + if (in5) + out3 <= in6; + else + out3 <= in7; + out1 = out1 ^ out2; + end + +This is translated by the Verilog and AST frontends into the following +RTLIL code (attributes, cell parameters and wire declarations not +included): + +.. code:: RTLIL + :number-lines: + + cell $logic_not $logic_not$:4$2 + connect \A \in1 + connect \Y $logic_not$:4$2_Y + end + cell $xor $xor$:13$3 + connect \A $1\out1[0:0] + connect \B \out2 + connect \Y $xor$:13$3_Y + end + process $proc$:1$1 + assign $0\out3[0:0] \out3 + assign $0\out2[0:0] $1\out1[0:0] + assign $0\out1[0:0] $xor$:13$3_Y + switch \in2 + case 1'1 + assign $1\out1[0:0] $logic_not$:4$2_Y + case + assign $1\out1[0:0] \in1 + end + switch \in3 + case 1'1 + assign $0\out2[0:0] \out2 + case + end + switch \in4 + case 1'1 + switch \in5 + case 1'1 + assign $0\out3[0:0] \in6 + case + assign $0\out3[0:0] \in7 + end + case + end + sync posedge \clock + update \out1 $0\out1[0:0] + update \out2 $0\out2[0:0] + update \out3 $0\out3[0:0] + end + +Note that the two operators are translated into separate cells outside +the generated process. The signal ``out1`` is assigned using blocking +assignments and therefore ``out1`` has been replaced with a different +signal in all expressions after the initial assignment. The signal +``out2`` is assigned using nonblocking assignments and therefore is not +substituted on the right-hand-side expressions. + +The ``RTLIL::CaseRule``/``RTLIL::SwitchRule`` tree must be interpreted +the following way: + +- On each case level (the body of the process is the root case), first + the actions on this level are evaluated and then the switches within + the case are evaluated. (Note that the last assignment on line 13 of + the Verilog code has been moved to the beginning of the RTLIL process + to line 13 of the RTLIL listing.) + + I.e. the special cases deeper in the switch hierarchy override the + defaults on the upper levels. The assignments in lines 12 and 22 of + the RTLIL code serve as an example for this. + + Note that in contrast to this, the order within the + ``RTLIL::SwitchRule`` objects within a ``RTLIL::CaseRule`` is + preserved with respect to the original AST and Verilog code. + +- The whole ``RTLIL::CaseRule``/``RTLIL::SwitchRule`` tree describes an + asynchronous circuit. I.e. the decision tree formed by the switches + can be seen independently for each assigned signal. Whenever one + assigned signal changes, all signals that depend on the changed + signals are to be updated. For example the assignments in lines 16 + and 18 in the RTLIL code in fact influence the assignment in line 12, + even though they are in the "wrong order". + +The only synchronous part of the process is in the ``RTLIL::SyncRule`` +object generated at line 35 in the RTLIL code. The sync rule is the only +part of the process where the original signals are assigned. The +synchronization event from the original Verilog code has been translated +into the synchronization type (posedge) and signal (\\clock) for the +``RTLIL::SyncRule`` object. In the case of this simple example the +``RTLIL::SyncRule`` object is later simply transformed into a set of +d-type flip-flops and the ``RTLIL::CaseRule``/``RTLIL::SwitchRule`` tree +to a decision tree using multiplexers. + +In more complex examples (e.g. asynchronous resets) the part of the +``RTLIL::CaseRule``/``RTLIL::SwitchRule`` tree that describes the +asynchronous reset must first be transformed to the correct +``RTLIL::SyncRule`` objects. This is done by the proc_adff pass. + +The ProcessGenerator algorithm +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The ``AST_INTERNAL::ProcessGenerator`` uses the following internal state +variables: + +- | ``subst_rvalue_from`` and ``subst_rvalue_to`` + | These two variables hold the replacement pattern that should be + used by ``AST::AstNode::genRTLIL()`` for signals with blocking + assignments. After initialization of + ``AST_INTERNAL::ProcessGenerator`` these two variables are empty. + +- | ``subst_lvalue_from`` and ``subst_lvalue_to`` + | These two variables contain the mapping from left-hand-side signals + (\\\ ) to the current temporary signal for the same thing + (initially $0\\\ ). + +- | ``current_case`` + | A pointer to a ``RTLIL::CaseRule`` object. Initially this is the + root case of the generated ``RTLIL::Process``. + +As the algorithm runs these variables are continuously modified as well +as pushed to the stack and later restored to their earlier values by +popping from the stack. + +On startup the ProcessGenerator generates a new ``RTLIL::Process`` +object with an empty root case and initializes its state variables as +described above. Then the ``RTLIL::SyncRule`` objects are created using +the synchronization events from the AST_ALWAYS node and the initial +values of ``subst_lvalue_from`` and ``subst_lvalue_to``. Then the AST +for this process is evaluated recursively. + +During this recursive evaluation, three different relevant types of AST +nodes can be discovered: AST_ASSIGN_LE (nonblocking assignments), +AST_ASSIGN_EQ (blocking assignments) and AST_CASE (``if`` or ``case`` +statement). + +Handling of nonblocking assignments +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +When an AST_ASSIGN_LE node is discovered, the following actions are +performed by the ProcessGenerator: + +- The left-hand-side is evaluated using ``AST::AstNode::genRTLIL()`` + and mapped to a temporary signal name using ``subst_lvalue_from`` and + ``subst_lvalue_to``. + +- The right-hand-side is evaluated using ``AST::AstNode::genRTLIL()``. + For this call, the values of ``subst_rvalue_from`` and + ``subst_rvalue_to`` are used to map blocking-assigned signals + correctly. + +- Remove all assignments to the same left-hand-side as this assignment + from the ``current_case`` and all cases within it. + +- Add the new assignment to the ``current_case``. + +Handling of blocking assignments +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +When an AST_ASSIGN_EQ node is discovered, the following actions are +performed by the ProcessGenerator: + +- Perform all the steps that would be performed for a nonblocking + assignment (see above). + +- Remove the found left-hand-side (before lvalue mapping) from + ``subst_rvalue_from`` and also remove the respective bits from + ``subst_rvalue_to``. + +- Append the found left-hand-side (before lvalue mapping) to + ``subst_rvalue_from`` and append the found right-hand-side to + ``subst_rvalue_to``. + +Handling of cases and if-statements +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +When an AST_CASE node is discovered, the following actions are performed +by the ProcessGenerator: + +- The values of ``subst_rvalue_from``, ``subst_rvalue_to``, + ``subst_lvalue_from`` and ``subst_lvalue_to`` are pushed to the + stack. + +- A new ``RTLIL::SwitchRule`` object is generated, the selection + expression is evaluated using ``AST::AstNode::genRTLIL()`` (with the + use of ``subst_rvalue_from`` and ``subst_rvalue_to``) and added to + the ``RTLIL::SwitchRule`` object and the object is added to the + ``current_case``. + +- All lvalues assigned to within the AST_CASE node using blocking + assignments are collected and saved in the local variable + ``this_case_eq_lvalue``. + +- New temporary signals are generated for all signals in + ``this_case_eq_lvalue`` and stored in ``this_case_eq_ltemp``. + +- The signals in ``this_case_eq_lvalue`` are mapped using + ``subst_rvalue_from`` and ``subst_rvalue_to`` and the resulting set + of signals is stored in ``this_case_eq_rvalue``. + +Then the following steps are performed for each AST_COND node within the +AST_CASE node: + +- Set ``subst_rvalue_from``, ``subst_rvalue_to``, ``subst_lvalue_from`` + and ``subst_lvalue_to`` to the values that have been pushed to the + stack. + +- Remove ``this_case_eq_lvalue`` from + ``subst_lvalue_from``/``subst_lvalue_to``. + +- Append ``this_case_eq_lvalue`` to ``subst_lvalue_from`` and append + ``this_case_eq_ltemp`` to ``subst_lvalue_to``. + +- Push the value of ``current_case``. + +- Create a new ``RTLIL::CaseRule``. Set ``current_case`` to the new + object and add the new object to the ``RTLIL::SwitchRule`` created + above. + +- Add an assignment from ``this_case_eq_rvalue`` to + ``this_case_eq_ltemp`` to the new ``current_case``. + +- Evaluate the compare value for this case using + ``AST::AstNode::genRTLIL()`` (with the use of ``subst_rvalue_from`` + and ``subst_rvalue_to``) modify the new ``current_case`` accordingly. + +- Recursion into the children of the AST_COND node. + +- Restore ``current_case`` by popping the old value from the stack. + +Finally the following steps are performed: + +- The values of ``subst_rvalue_from``, ``subst_rvalue_to``, + ``subst_lvalue_from`` and ``subst_lvalue_to`` are popped from the + stack. + +- The signals from ``this_case_eq_lvalue`` are removed from the + ``subst_rvalue_from``/``subst_rvalue_to``-pair. + +- The value of ``this_case_eq_lvalue`` is appended to + ``subst_rvalue_from`` and the value of ``this_case_eq_ltemp`` is + appended to ``subst_rvalue_to``. + +- Map the signals in ``this_case_eq_lvalue`` using + ``subst_lvalue_from``/``subst_lvalue_to``. + +- Remove all assignments to signals in ``this_case_eq_lvalue`` in + ``current_case`` and all cases within it. + +- Add an assignment from ``this_case_eq_ltemp`` to + ``this_case_eq_lvalue`` to ``current_case``. + +Further analysis of the algorithm for cases and if-statements +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +With respect to nonblocking assignments the algorithm is easy: later +assignments invalidate earlier assignments. For each signal assigned +using nonblocking assignments exactly one temporary variable is +generated (with the $0-prefix) and this variable is used for all +assignments of the variable. + +Note how all the ``_eq_``-variables become empty when no blocking +assignments are used and many of the steps in the algorithm can then be +ignored as a result of this. + +For a variable with blocking assignments the algorithm shows the +following behaviour: First a new temporary variable is created. This new +temporary variable is then registered as the assignment target for all +assignments for this variable within the cases for this AST_CASE node. +Then for each case the new temporary variable is first assigned the old +temporary variable. This assignment is overwritten if the variable is +actually assigned in this case and is kept as a default value otherwise. + +This yields an ``RTLIL::CaseRule`` that assigns the new temporary +variable in all branches. So when all cases have been processed a final +assignment is added to the containing block that assigns the new +temporary variable to the old one. Note how this step always overrides a +previous assignment to the old temporary variable. Other than +nonblocking assignments, the old assignment could still have an effect +somewhere in the design, as there have been calls to +``AST::AstNode::genRTLIL()`` with a +``subst_rvalue_from``/``subst_rvalue_to``-tuple that contained the +right-hand-side of the old assignment. + +The proc pass +~~~~~~~~~~~~~ + +The ProcessGenerator converts a behavioural model in AST representation +to a behavioural model in ``RTLIL::Process`` representation. The actual +conversion from a behavioural model to an RTL representation is +performed by the proc pass and the passes it launches: + +- | proc_clean and proc_rmdead + | These two passes just clean up the ``RTLIL::Process`` structure. + The proc_clean pass removes empty parts (eg. empty assignments) + from the process and proc_rmdead detects and removes unreachable + branches from the process's decision trees. + +- | proc_arst + | This pass detects processes that describe d-type flip-flops with + asynchronous resets and rewrites the process to better reflect what + they are modelling: Before this pass, an asynchronous reset has two + edge-sensitive sync rules and one top-level for the reset path. + After this pass the sync rule for the reset is level-sensitive and + the top-level has been removed. + +- | proc_mux + | This pass converts the /-tree to a tree of multiplexers per written + signal. After this, the structure only contains the s that describe + the output registers. + +- | proc_dff + | This pass replaces the s to d-type flip-flops (with asynchronous + resets if necessary). + +- | proc_dff + | This pass replaces the s with $memwr cells. + +- | proc_clean + | A final call to proc_clean removes the now empty objects. + +Performing these last processing steps in passes instead of in the +Verilog frontend has two important benefits: + +First it improves the transparency of the process. Everything that +happens in a separate pass is easier to debug, as the RTLIL data +structures can be easily investigated before and after each of the +steps. + +Second it improves flexibility. This scheme can easily be extended to +support other types of storage-elements, such as sr-latches or +d-latches, without having to extend the actual Verilog frontend. + +Synthesizing Verilog arrays +--------------------------- + +Add some information on the generation of $memrd and $memwr cells and +how they are processed in the memory pass. + +Synthesizing parametric designs +------------------------------- + +Add some information on the ``RTLIL::Module::derive()`` method and how +it is used to synthesize parametric modules via the hierarchy pass. diff --git a/docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst b/docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst new file mode 100644 index 000000000..a48401dcc --- /dev/null +++ b/docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst @@ -0,0 +1,336 @@ +==================================== +010: Converting Verilog to BLIF page +==================================== + +Installation +============ + +Yosys written in C++ (using features from C++11) and is tested on modern +Linux. It should compile fine on most UNIX systems with a C++11 +compiler. The README file contains useful information on building Yosys +and its prerequisites. + +Yosys is a large and feature-rich program with a couple of dependencies. +It is, however, possible to deactivate some of the dependencies in the +Makefile, resulting in features in Yosys becoming unavailable. When +problems with building Yosys are encountered, a user who is only +interested in the features of Yosys that are discussed in this +Application Note may deactivate TCL, Qt and MiniSAT support in the +Makefile and may opt against building yosys-abc. + +This Application Note is based on `Yosys GIT`_ `Rev. e216e0e`_ from 2013-11-23. +The Verilog sources used for the examples are taken from `yosys-bigsim`_, a +collection of real-world designs used for regression testing Yosys. + +.. _Yosys GIT: https://github.com/YosysHQ/yosys + +.. _Rev. e216e0e: https://github.com/YosysHQ/yosys/tree/e216e0e + +.. _yosys-bigsim: https://github.com/YosysHQ/yosys-bigsim + +Getting started +=============== + +We start our tour with the Navré processor from yosys-bigsim. The `Navré +processor`_ is an Open Source AVR clone. It is a single module (softusb_navre) +in a single design file (softusb_navre.v). It also is using only features that +map nicely to the BLIF format, for example it only uses synchronous resets. + +.. _Navré processor: http://opencores.org/projects/navre + +Converting softusb_navre.v to softusb_navre.blif could not be easier: + +.. code:: sh + + yosys -o softusb_navre.blif -S softusb_navre.v + +Behind the scenes Yosys is controlled by synthesis scripts that execute +commands that operate on Yosys' internal state. For example, the -o +softusb_navre.blif option just adds the command write_blif +softusb_navre.blif to the end of the script. Likewise a file on the +command line – softusb_navre.v in this case – adds the command +read_verilog softusb_navre.v to the beginning of the synthesis script. +In both cases the file type is detected from the file extension. + +Finally the option -S instantiates a built-in default synthesis script. +Instead of using -S one could also specify the synthesis commands for +the script on the command line using the -p option, either using +individual options for each command or by passing one big command string +with a semicolon-separated list of commands. But in most cases it is +more convenient to use an actual script file. + +Using a synthesis script +======================== + +With a script file we have better control over Yosys. The following +script file replicates what the command from the last section did: + +.. code:: yoscrypt + + read_verilog softusb_navre.v + hierarchy + proc; opt; memory; opt; techmap; opt + write_blif softusb_navre.blif + +The first and last line obviously read the Verilog file and write the +BLIF file. + +The 2nd line checks the design hierarchy and instantiates parametrized +versions of the modules in the design, if necessary. In the case of this +simple design this is a no-op. However, as a general rule a synthesis +script should always contain this command as first command after reading +the input files. + +The 3rd line does most of the actual work: + +- The command opt is the Yosys' built-in optimizer. It can perform some + simple optimizations such as const-folding and removing unconnected + parts of the design. It is common practice to call opt after each + major step in the synthesis procedure. In cases where too much + optimization is not appreciated (for example when analyzing a + design), it is recommended to call clean instead of opt. + +- The command proc converts processes (Yosys' internal representation + of Verilog always- and initial-blocks) to circuits of multiplexers + and storage elements (various types of flip-flops). + +- The command memory converts Yosys' internal representations of arrays + and array accesses to multi-port block memories, and then maps this + block memories to address decoders and flip-flops, unless the option + -nomap is used, in which case the multi-port block memories stay in + the design and can then be mapped to architecture-specific memory + primitives using other commands. + +- The command techmap turns a high-level circuit with coarse grain + cells such as wide adders and multipliers to a fine-grain circuit of + simple logic primitives and single-bit storage elements. The command + does that by substituting the complex cells by circuits of simpler + cells. It is possible to provide a custom set of rules for this + process in the form of a Verilog source file, as we will see in the + next section. + +Now Yosys can be run with the filename of the synthesis script as +argument: + +.. code:: sh + + yosys softusb_navre.ys + +Now that we are using a synthesis script we can easily modify how Yosys +synthesizes the design. The first thing we should customize is the call +to the hierarchy command: + +Whenever it is known that there are no implicit blackboxes in the +design, i.e. modules that are referenced but are not defined, the +hierarchy command should be called with the -check option. This will +then cause synthesis to fail when implicit blackboxes are found in the +design. + +The 2nd thing we can improve regarding the hierarchy command is that we +can tell it the name of the top level module of the design hierarchy. It +will then automatically remove all modules that are not referenced from +this top level module. + +For many designs it is also desired to optimize the encodings for the +finite state machines (FSMs) in the design. The fsm command finds FSMs, +extracts them, performs some basic optimizations and then generate a +circuit from the extracted and optimized description. It would also be +possible to tell the fsm command to leave the FSMs in their extracted +form, so they can be further processed using custom commands. But in +this case we don't want that. + +So now we have the final synthesis script for generating a BLIF file for +the Navré CPU: + +.. code:: yoscrypt + + read_verilog softusb_navre.v + hierarchy -check -top softusb_navre + proc; opt; memory; opt; fsm; opt; techmap; opt + write_blif softusb_navre.blif + +Advanced example: The Amber23 ARMv2a CPU +======================================== + +Our 2nd example is the `Amber23 ARMv2a CPU`_. Once again we base our example on +the Verilog code that is included in `yosys-bigsim`_. + +.. _Amber23 ARMv2a CPU: http://opencores.org/projects/amber + +.. code-block:: yoscrypt + :caption: `amber23.ys` + :name: amber23.ys + + read_verilog a23_alu.v + read_verilog a23_barrel_shift_fpga.v + read_verilog a23_barrel_shift.v + read_verilog a23_cache.v + read_verilog a23_coprocessor.v + read_verilog a23_core.v + read_verilog a23_decode.v + read_verilog a23_execute.v + read_verilog a23_fetch.v + read_verilog a23_multiply.v + read_verilog a23_ram_register_bank.v + read_verilog a23_register_bank.v + read_verilog a23_wishbone.v + read_verilog generic_sram_byte_en.v + read_verilog generic_sram_line_en.v + hierarchy -check -top a23_core + add -global_input globrst 1 + proc -global_arst globrst + techmap -map adff2dff.v + opt; memory; opt; fsm; opt; techmap + write_blif amber23.blif + +The problem with this core is that it contains no dedicated reset logic. Instead +the coding techniques shown in :numref:`glob_arst` are used to define reset +values for the global asynchronous reset in an FPGA implementation. This design +can not be expressed in BLIF as it is. Instead we need to use a synthesis script +that transforms this form to synchronous resets that can be expressed in BLIF. + +(Note that there is no problem if this coding techniques are used to +model ROM, where the register is initialized using this syntax but is +never updated otherwise.) + +:numref:`amber23.ys` shows the synthesis script for the Amber23 core. In line 17 +the add command is used to add a 1-bit wide global input signal with the name +globrst. That means that an input with that name is added to each module in the +design hierarchy and then all module instantiations are altered so that this new +signal is connected throughout the whole design hierarchy. + +.. code-block:: verilog + :caption: Implicit coding of global asynchronous resets + :name: glob_arst + + reg [7:0] a = 13, b; + initial b = 37; + +.. code-block:: verilog + :caption: `adff2dff.v` + :name: adff2dff.v + + (* techmap_celltype = "$adff" *) + module adff2dff (CLK, ARST, D, Q); + + parameter WIDTH = 1; + parameter CLK_POLARITY = 1; + parameter ARST_POLARITY = 1; + parameter ARST_VALUE = 0; + + input CLK, ARST; + input [WIDTH-1:0] D; + output reg [WIDTH-1:0] Q; + + wire [1023:0] _TECHMAP_DO_ = "proc"; + + wire _TECHMAP_FAIL_ = + !CLK_POLARITY || !ARST_POLARITY; + + always @(posedge CLK) + if (ARST) + Q <= ARST_VALUE; + else + Q <= D; + + endmodule + +In line 18 the proc command is called. But in this script the signal +name globrst is passed to the command as a global reset signal for +resetting the registers to their assigned initial values. + +Finally in line 19 the techmap command is used to replace all instances of +flip-flops with asynchronous resets with flip-flops with synchronous resets. The +map file used for this is shown in :numref:`adff2dff.v`. Note how the +techmap_celltype attribute is used in line 1 to tell the techmap command which +cells to replace in the design, how the \_TECHMAP_FAIL\_ wire in lines 15 and 16 +(which evaluates to a constant value) determines if the parameter set is +compatible with this replacement circuit, and how the \_TECHMAP_DO\_ wire in +line 13 provides a mini synthesis-script to be used to process this cell. + +.. code-block:: c + :caption: Test program for the Amber23 CPU (Sieve of Eratosthenes). Compiled + using GCC 4.6.3 for ARM with ``-Os -marm -march=armv2a + -mno-thumb-interwork -ffreestanding``, linked with ``--fix-v4bx`` + set and booted with a custom setup routine written in ARM assembler. + :name: sieve + + #include + #include + + #define BITMAP_SIZE 64 + #define OUTPORT 0x10000000 + + static uint32_t bitmap[BITMAP_SIZE/32]; + + static void bitmap_set(uint32_t idx) { bitmap[idx/32] |= 1 << (idx % 32); } + static bool bitmap_get(uint32_t idx) { return (bitmap[idx/32] & (1 << (idx % 32))) != 0; } + static void output(uint32_t val) { *((volatile uint32_t*)OUTPORT) = val; } + + int main() { + uint32_t i, j, k; + output(2); + for (i = 0; i < BITMAP_SIZE; i++) { + if (bitmap_get(i)) continue; + output(3+2*i); + for (j = 2*(3+2*i);; j += 3+2*i) { + if (j%2 == 0) continue; + k = (j-3)/2; + if (k >= BITMAP_SIZE) break; + bitmap_set(k); + } + } + output(0); + return 0; + } + +Verification of the Amber23 CPU +=============================== + +The BLIF file for the Amber23 core, generated using :numref:`amber23.ys` and +:numref:`adff2dff.v` and the version of the Amber23 RTL source that is bundled +with yosys-bigsim, was verified using the test-bench from yosys-bigsim. It +successfully executed the program shown in :numref:`sieve` in the test-bench. + +For simulation the BLIF file was converted back to Verilog using `ABC`_. So this +test includes the successful transformation of the BLIF file into ABC's internal +format as well. + +.. _ABC: https://github.com/berkeley-abc/abc + +The only thing left to write about the simulation itself is that it +probably was one of the most energy inefficient and time consuming ways +of successfully calculating the first 31 primes the author has ever +conducted. + +Limitations +=========== + +At the time of this writing Yosys does not support multi-dimensional +memories, does not support writing to individual bits of array elements, +does not support initialization of arrays with $readmemb and $readmemh, +and has only limited support for tristate logic, to name just a few +limitations. + +That being said, Yosys can synthesize an overwhelming majority of +real-world Verilog RTL code. The remaining cases can usually be modified +to be compatible with Yosys quite easily. + +The various designs in yosys-bigsim are a good place to look for +examples of what is within the capabilities of Yosys. + +Conclusion +========== + +Yosys is a feature-rich Verilog-2005 synthesis tool. It has many uses, +but one is to provide an easy gateway from high-level Verilog code to +low-level logic circuits. + +The command line option -S can be used to quickly synthesize Verilog +code to BLIF files without a hassle. + +With custom synthesis scripts it becomes possible to easily perform +high-level optimizations, such as re-encoding FSMs. In some extreme +cases, such as the Amber23 ARMv2 CPU, the more advanced Yosys features +can be used to change a design to fit a certain need without actually +touching the RTL code. diff --git a/docs/source/appendix/APPNOTE_011_Design_Investigation.rst b/docs/source/appendix/APPNOTE_011_Design_Investigation.rst new file mode 100644 index 000000000..004d3cb66 --- /dev/null +++ b/docs/source/appendix/APPNOTE_011_Design_Investigation.rst @@ -0,0 +1,965 @@ +========================================== +011: Interactive design investigation page +========================================== + +Installation and prerequisites +============================== + +This Application Note is based on the `Yosys GIT`_ `Rev. 2b90ba1`_ from +2013-12-08. The README file covers how to install Yosys. The ``show`` command +requires a working installation of `GraphViz`_ and `xdot` for generating the +actual circuit diagrams. + +.. _Yosys GIT: https://github.com/YosysHQ/yosys + +.. _Rev. 2b90ba1: https://github.com/YosysHQ/yosys/tree/2b90ba1 + +.. _GraphViz: http://www.graphviz.org/ + +.. _xdot: https://github.com/jrfonseca/xdot.py + +Overview +======== + +This application note is structured as follows: + +:ref:`intro_show` introduces the ``show`` command and explains the symbols used +in the circuit diagrams generated by it. + +:ref:`navigate` introduces additional commands used to navigate in the design, +select portions of the design, and print additional information on the elements +in the design that are not contained in the circuit diagrams. + +:ref:`poke` introduces commands to evaluate the design and solve SAT problems +within the design. + +:ref:`conclusion` concludes the document and summarizes the key points. + +.. _intro_show: + +Introduction to the show command +================================ + +.. code-block:: console + :caption: Yosys script with ``show`` commands and example design + :name: example_src + + $ cat example.ys + read_verilog example.v + show -pause + proc + show -pause + opt + show -pause + + $ cat example.v + module example(input clk, a, b, c, + output reg [1:0] y); + always @(posedge clk) + if (c) + y <= c ? a + b : 2'd0; + endmodule + +.. figure:: ../../images/011/example_out.* + :class: width-helper + :name: example_out + + Output of the three ``show`` commands from :numref:`example_src` + +The ``show`` command generates a circuit diagram for the design in its current +state. Various options can be used to change the appearance of the circuit +diagram, set the name and format for the output file, and so forth. When called +without any special options, it saves the circuit diagram in a temporary file +and launches ``xdot`` to display the diagram. Subsequent calls to show re-use the +``xdot`` instance (if still running). + +A simple circuit +---------------- + +:numref:`example_src` shows a simple synthesis script and a Verilog file that +demonstrate the usage of show in a simple setting. Note that ``show`` is called with +the ``-pause`` option, that halts execution of the Yosys script until the user +presses the Enter key. The ``show -pause`` command also allows the user to enter +an interactive shell to further investigate the circuit before continuing +synthesis. + +So this script, when executed, will show the design after each of the three +synthesis commands. The generated circuit diagrams are shown in +:numref:`example_out`. + +The first diagram (from top to bottom) shows the design directly after being +read by the Verilog front-end. Input and output ports are displayed as octagonal +shapes. Cells are displayed as rectangles with inputs on the left and outputs on +the right side. The cell labels are two lines long: The first line contains a +unique identifier for the cell and the second line contains the cell type. +Internal cell types are prefixed with a dollar sign. The Yosys manual contains a +chapter on the internal cell library used in Yosys. + +Constants are shown as ellipses with the constant value as label. The syntax +``'`` is used for for constants that are not 32-bit wide and/or +contain bits that are not 0 or 1 (i.e. ``x`` or ``z``). Ordinary 32-bit +constants are written using decimal numbers. + +Single-bit signals are shown as thin arrows pointing from the driver to the +load. Signals that are multiple bits wide are shown as think arrows. + +Finally *processes* are shown in boxes with round corners. Processes are Yosys' +internal representation of the decision-trees and synchronization events +modelled in a Verilog ``always``-block. The label reads ``PROC`` followed by a +unique identifier in the first line and contains the source code location of the +original ``always``-block in the 2nd line. Note how the multiplexer from the +``?:``-expression is represented as a ``$mux`` cell but the multiplexer from the +``if``-statement is yet still hidden within the process. + +The ``proc`` command transforms the process from the first diagram into a +multiplexer and a d-type flip-flip, which brings us to the 2nd diagram. + +The Rhombus shape to the right is a dangling wire. (Wire nodes are only shown if +they are dangling or have "public" names, for example names assigned from the +Verilog input.) Also note that the design now contains two instances of a +``BUF``-node. This are artefacts left behind by the ``proc``-command. It is +quite usual to see such artefacts after calling commands that perform changes in +the design, as most commands only care about doing the transformation in the +least complicated way, not about cleaning up after them. The next call to +``clean`` (or ``opt``, which includes ``clean`` as one of its operations) will +clean up this artefacts. This operation is so common in Yosys scripts that it +can simply be abbreviated with the ``;;`` token, which doubles as separator for +commands. Unless one wants to specifically analyze this artefacts left behind +some operations, it is therefore recommended to always call ``clean`` before +calling ``show``. + +In this script we directly call ``opt`` as next step, which finally leads us to +the 3rd diagram in :numref:`example_out`. Here we see that the ``opt`` command +not only has removed the artifacts left behind by ``proc``, but also determined +correctly that it can remove the first ``$mux`` cell without changing the +behavior of the circuit. + +.. figure:: ../../images/011/splice.* + :class: width-helper + :name: splice_dia + + Output of ``yosys -p 'proc; opt; show' splice.v`` + +.. literalinclude:: ../../../manual/APPNOTE_011_Design_Investigation/splice.v + :caption: ``splice.v`` + :name: splice_src + +.. figure:: ../../images/011/splitnets_libfile.* + :class: width-helper + :name: splitnets_libfile + + Effects of ``splitnets`` command and of providing a cell library. (The + circuit is a half-adder built from simple CMOS gates.) + +Break-out boxes for signal vectors +---------------------------------- + +As has been indicated by the last example, Yosys is can manage signal vectors +(aka. multi-bit wires or buses) as native objects. This provides great +advantages when analyzing circuits that operate on wide integers. But it also +introduces some additional complexity when the individual bits of of a signal +vector are accessed. The example ``show`` in :numref:`splice_src` demonstrates +how such circuits are visualized by the ``show`` command. + +The key elements in understanding this circuit diagram are of course the boxes +with round corners and rows labeled ``: - +:``. Each of this boxes has one signal per row on one side +and a common signal for all rows on the other side. The ``:`` tuples +specify which bits of the signals are broken out and connected. So the top row +of the box connecting the signals ``a`` and ``x`` indicates that the bit 0 (i.e. +the range 0:0) from signal ``a`` is connected to bit 1 (i.e. the range 1:1) of +signal ``x``. + +Lines connecting such boxes together and lines connecting such boxes to +cell ports have a slightly different look to emphasise that they are not +actual signal wires but a necessity of the graphical representation. +This distinction seems like a technicality, until one wants to debug a +problem related to the way Yosys internally represents signal vectors, +for example when writing custom Yosys commands. + +Gate level netlists +------------------- + +Finally :numref:`splitnets_libfile` shows two common pitfalls when working with +designs mapped to a cell library. The top figure has two problems: First Yosys +did not have access to the cell library when this diagram was generated, +resulting in all cell ports defaulting to being inputs. This is why all ports +are drawn on the left side the cells are awkwardly arranged in a large column. +Secondly the two-bit vector ``y`` requires breakout-boxes for its individual +bits, resulting in an unnecessary complex diagram. + +For the 2nd diagram Yosys has been given a description of the cell library as +Verilog file containing blackbox modules. There are two ways to load cell +descriptions into Yosys: First the Verilog file for the cell library can be +passed directly to the ``show`` command using the ``-lib `` option. +Secondly it is possible to load cell libraries into the design with the +``read_verilog -lib `` command. The 2nd method has the great advantage +that the library only needs to be loaded once and can then be used in all +subsequent calls to the ``show`` command. + +In addition to that, the 2nd diagram was generated after ``splitnet -ports`` was +run on the design. This command splits all signal vectors into individual signal +bits, which is often desirable when looking at gate-level circuits. The +``-ports`` option is required to also split module ports. Per default the +command only operates on interior signals. + +Miscellaneous notes +------------------- + +Per default the ``show`` command outputs a temporary dot file and launches +``xdot`` to display it. The options ``-format``, ``-viewer`` and ``-prefix`` can +be used to change format, viewer and filename prefix. Note that the ``pdf`` and +``ps`` format are the only formats that support plotting multiple modules in one +run. + +In densely connected circuits it is sometimes hard to keep track of the +individual signal wires. For this cases it can be useful to call ``show`` with +the ``-colors `` argument, which randomly assigns colors to the nets. +The integer (> 0) is used as seed value for the random color assignments. +Sometimes it is necessary it try some values to find an assignment of colors +that looks good. + +The command ``help show`` prints a complete listing of all options supported by +the ``show`` command. + +.. _navigate: + +Navigating the design +===================== + +Plotting circuit diagrams for entire modules in the design brings us +only helps in simple cases. For complex modules the generated circuit +diagrams are just stupidly big and are no help at all. In such cases one +first has to select the relevant portions of the circuit. + +In addition to *what* to display one also needs to carefully decide *when* +to display it, with respect to the synthesis flow. In general it is a +good idea to troubleshoot a circuit in the earliest state in which a +problem can be reproduced. So if, for example, the internal state before +calling the ``techmap`` command already fails to verify, it is better to +troubleshoot the coarse-grain version of the circuit before ``techmap`` than +the gate-level circuit after ``techmap``. + +.. Note:: It is generally recommended to verify the internal state of a + design by writing it to a Verilog file using ``write_verilog -noexpr`` + and using the simulation models from ``simlib.v`` and ``simcells.v`` + from the Yosys data directory (as printed by ``yosys-config --datdir``). + +Interactive navigation +---------------------- + +.. code-block:: none + :caption: Demonstration of ``ls`` and ``cd`` using ``example.v`` from :numref:`example_src` + :name: lscd + + yosys> ls + + 1 modules: + example + + yosys> cd example + + yosys [example]> ls + + 7 wires: + $0\y[1:0] + $add$example.v:5$2_Y + a + b + c + clk + y + + 3 cells: + $add$example.v:5$2 + $procdff$7 + $procmux$5 + +.. code-block:: RTLIL + :caption: Output of ``dump \$2`` using the design from :numref:`example_src` + and :numref:`example_out` + :name: dump2 + + attribute \src "example.v:5" + cell $add $add$example.v:5$2 + parameter \A_SIGNED 0 + parameter \A_WIDTH 1 + parameter \B_SIGNED 0 + parameter \B_WIDTH 1 + parameter \Y_WIDTH 2 + connect \A \a + connect \B \b + connect \Y $add$example.v:5$2_Y + end + +Once the right state within the synthesis flow for debugging the circuit has +been identified, it is recommended to simply add the ``shell`` command to the +matching place in the synthesis script. This command will stop the synthesis at +the specified moment and go to shell mode, where the user can interactively +enter commands. + +For most cases, the shell will start with the whole design selected (i.e. when +the synthesis script does not already narrow the selection). The command ``ls`` +can now be used to create a list of all modules. The command ``cd`` can be used +to switch to one of the modules (type ``cd ..`` to switch back). Now the `ls` +command lists the objects within that module. :numref:`lscd` demonstrates this +using the design from :numref:`example_src`. + +There is a thing to note in :numref:`lscd`: We can see that the cell names from +:numref:`example_out` are just abbreviations of the actual cell names, namely +the part after the last dollar-sign. Most auto-generated names (the ones +starting with a dollar sign) are rather long and contains some additional +information on the origin of the named object. But in most cases those names can +simply be abbreviated using the last part. + +Usually all interactive work is done with one module selected using the ``cd`` +command. But it is also possible to work from the design-context (``cd ..``). In +this case all object names must be prefixed with ``/``. For example +``a*/b\*`` would refer to all objects whose names start with ``b`` from all +modules whose names start with ``a``. + +The ``dump`` command can be used to print all information about an object. For +example ``dump $2`` will print :numref:`dump2`. This can for example be useful +to determine the names of nets connected to cells, as the net-names are usually +suppressed in the circuit diagram if they are auto-generated. + +For the remainder of this document we will assume that the commands are +run from module-context and not design-context. + +Working with selections +----------------------- + +.. figure:: ../../images/011/example_03.* + :class: width-helper + :name: seladd + + Output of ``show`` after ``select $2`` or ``select t:$add`` (see also + :numref:`example_out`) + +When a module is selected using the ``cd`` command, all commands (with a few +exceptions, such as the ``read_`` and ``write_`` commands) operate only on the +selected module. This can also be useful for synthesis scripts where different +synthesis strategies should be applied to different modules in the design. + +But for most interactive work we want to further narrow the set of +selected objects. This can be done using the ``select`` command. + +For example, if the command ``select $2`` is executed, a subsequent ``show`` +command will yield the diagram shown in :numref:`seladd`. Note that the nets are +now displayed in ellipses. This indicates that they are not selected, but only +shown because the diagram contains a cell that is connected to the net. This of +course makes no difference for the circuit that is shown, but it can be a useful +information when manipulating selections. + +Objects can not only be selected by their name but also by other properties. For +example ``select t:$add`` will select all cells of type ``$add``. In this case +this is also yields the diagram shown in :numref:`seladd`. + +.. literalinclude:: ../../../manual/APPNOTE_011_Design_Investigation/foobaraddsub.v + :caption: Test module for operations on selections + :name: foobaraddsub + :language: verilog + +The output of ``help select`` contains a complete syntax reference for +matching different properties. + +Many commands can operate on explicit selections. For example the command ``dump +t:$add`` will print information on all ``$add`` cells in the active module. +Whenever a command has ``[selection]`` as last argument in its usage help, this +means that it will use the engine behind the ``select`` command to evaluate +additional arguments and use the resulting selection instead of the selection +created by the last ``select`` command. + +Normally the ``select`` command overwrites a previous selection. The commands +``select -add`` and ``select -del`` can be used to add or remove objects from +the current selection. + +The command ``select -clear`` can be used to reset the selection to the default, +which is a complete selection of everything in the current module. + +Operations on selections +------------------------ + +.. literalinclude:: ../../../manual/APPNOTE_011_Design_Investigation/sumprod.v + :caption: Another test module for operations on selections + :name: sumprod + :language: verilog + +.. figure:: ../../images/011/sumprod_00.* + :class: width-helper + :name: sumprod_00 + + Output of ``show a:sumstuff`` on :numref:`sumprod` + +The ``select`` command is actually much more powerful than it might seem on the +first glimpse. When it is called with multiple arguments, each argument is +evaluated and pushed separately on a stack. After all arguments have been +processed it simply creates the union of all elements on the stack. So the +following command will select all ``$add`` cells and all objects with the +``foo`` attribute set: + +.. code-block:: yoscrypt + + select t:$add a:foo + +(Try this with the design shown in :numref:`foobaraddsub`. Use the ``select +-list`` command to list the current selection.) + +In many cases simply adding more and more stuff to the selection is an +ineffective way of selecting the interesting part of the design. Special +arguments can be used to combine the elements on the stack. For example +the ``%i`` arguments pops the last two elements from the stack, intersects +them, and pushes the result back on the stack. So the following command +will select all ``$add ``cells that have the ``foo`` attribute set: + +.. code-block:: yoscrypt + + select t:$add a:foo %i + +The listing in :numref:`sumprod` uses the Yosys non-standard ``{... \*}`` syntax +to set the attribute ``sumstuff`` on all cells generated by the first assign +statement. (This works on arbitrary large blocks of Verilog code an can be used +to mark portions of code for analysis.) + +Selecting ``a:sumstuff`` in this module will yield the circuit diagram shown in +:numref:`sumprod_00`. As only the cells themselves are selected, but not the +temporary wire ``$1_Y``, the two adders are shown as two disjunct parts. This +can be very useful for global signals like clock and reset signals: just +unselect them using a command such as ``select -del clk rst`` and each cell +using them will get its own net label. + +In this case however we would like to see the cells connected properly. This can +be achieved using the ``%x`` action, that broadens the selection, i.e. for each +selected wire it selects all cells connected to the wire and vice versa. So +``show a:sumstuff %x`` yields the diagram shown in :numref:`sumprod_01`. + +.. figure:: ../../images/011/sumprod_01.* + :class: width-helper + :name: sumprod_01 + + Output of ``show a:sumstuff %x`` on :numref:`sumprod` + +Selecting logic cones +--------------------- + +:numref:`sumprod_01` shows what is called the ``input cone`` of ``sum``, i.e. +all cells and signals that are used to generate the signal ``sum``. The ``%ci`` +action can be used to select the input cones of all object in the top selection +in the stack maintained by the ``select`` command. + +As the ``%x`` action, this commands broadens the selection by one "step". +But this time the operation only works against the direction of data +flow. That means, wires only select cells via output ports and cells +only select wires via input ports. + +:numref:`select_prod` show the sequence of diagrams generated by the following +commands: + +.. code-block:: yoscrypt + + show prod + show prod %ci + show prod %ci %ci + show prod %ci %ci %ci + +When selecting many levels of logic, repeating ``%ci`` over and over again can +be a bit dull. So there is a shortcut for that: the number of iterations can be +appended to the action. So for example the action ``%ci3`` is identical to +performing the ``%ci`` action three times. + +The action ``%ci\*`` performs the ``%ci`` action over and over again until it +has no effect anymore. + +.. figure:: ../../images/011/select_prod.* + :class: width-helper + :name: select_prod + + Objects selected by ``select prod \%ci...`` + +In most cases there are certain cell types and/or ports that should not be +considered for the ``%ci`` action, or we only want to follow certain cell types +and/or ports. This can be achieved using additional patterns that can be +appended to the ``%ci`` action. + +Lets consider the design from :numref:`memdemo_src`. It serves no purpose other +than being a non-trivial circuit for demonstrating some of the advanced Yosys +features. We synthesize the circuit using ``proc; opt; memory; opt`` and change +to the ``memdemo`` module with ``cd memdemo``. If we type ``show`` now we see +the diagram shown in :numref:`memdemo_00`. + +.. literalinclude:: ../../../manual/APPNOTE_011_Design_Investigation/memdemo.v + :caption: Demo circuit for demonstrating some advanced Yosys features + :name: memdemo_src + :language: verilog + +.. figure:: ../../images/011/memdemo_00.* + :class: width-helper + :name: memdemo_00 + + Complete circuit diagram for the design shown in :numref:`memdemo_src` + +But maybe we are only interested in the tree of multiplexers that select the +output value. In order to get there, we would start by just showing the output +signal and its immediate predecessors: + +.. code-block:: yoscrypt + + show y %ci2 + +From this we would learn that ``y`` is driven by a ``$dff cell``, that ``y`` is +connected to the output port ``Q``, that the ``clk`` signal goes into the +``CLK`` input port of the cell, and that the data comes from a auto-generated +wire into the input ``D`` of the flip-flop cell. + +As we are not interested in the clock signal we add an additional pattern to the +``%ci`` action, that tells it to only follow ports ``Q`` and ``D`` of ``$dff`` +cells: + +.. code-block:: yoscrypt + + show y %ci2:+$dff[Q,D] + +To add a pattern we add a colon followed by the pattern to the ``%ci`` action. +The pattern it self starts with ``-`` or ``+``, indicating if it is an include +or exclude pattern, followed by an optional comma separated list of cell types, +followed by an optional comma separated list of port names in square brackets. + +Since we know that the only cell considered in this case is a ``$dff`` cell, +we could as well only specify the port names: + +.. code-block:: yoscrypt + + show y %ci2:+[Q,D] + +Or we could decide to tell the ``%ci`` action to not follow the ``CLK`` input: + +.. code-block:: yoscrypt + + show y %ci2:-[CLK] + +.. figure:: ../../images/011/memdemo_01.* + :class: width-helper + :name: memdemo_01 + + Output of ``show y \%ci2:+\$dff[Q,D] \%ci*:-\$mux[S]:-\$dff`` + +Next we would investigate the next logic level by adding another ``%ci2`` to +the command: + +.. code-block:: yoscrypt + + show y %ci2:-[CLK] %ci2 + +From this we would learn that the next cell is a ``$mux`` cell and we would +add additional pattern to narrow the selection on the path we are +interested. In the end we would end up with a command such as + +.. code-block:: yoscrypt + + show y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff + +in which the first ``%ci`` jumps over the initial d-type flip-flop and the 2nd +action selects the entire input cone without going over multiplexer select +inputs and flip-flop cells. The diagram produces by this command is shown in +:numref:`memdemo_01`. + +Similar to ``%ci`` exists an action ``%co`` to select output cones that accepts +the same syntax for pattern and repetition. The ``%x`` action mentioned +previously also accepts this advanced syntax. + +This actions for traversing the circuit graph, combined with the actions for +boolean operations such as intersection (``%i``) and difference (``%d``) are +powerful tools for extracting the relevant portions of the circuit under +investigation. + +See ``help select`` for a complete list of actions available in selections. + +Storing and recalling selections +-------------------------------- + +The current selection can be stored in memory with the command ``select -set +``. It can later be recalled using ``select @``. In fact, the +``@`` expression pushes the stored selection on the stack maintained by +the ``select`` command. So for example + +.. code-block:: yoscrypt + + select @foo @bar %i + +will select the intersection between the stored selections ``foo`` and ``bar``. + +In larger investigation efforts it is highly recommended to maintain a +script that sets up relevant selections, so they can easily be recalled, +for example when Yosys needs to be re-run after a design or source code +change. + +The ``history`` command can be used to list all recent interactive commands. +This feature can be useful for creating such a script from the commands +used in an interactive session. + +.. _poke: + +Advanced investigation techniques +================================= + +When working with very large modules, it is often not enough to just select the +interesting part of the module. Instead it can be useful to extract the +interesting part of the circuit into a separate module. This can for example be +useful if one wants to run a series of synthesis commands on the critical part +of the module and wants to carefully read all the debug output created by the +commands in order to spot a problem. This kind of troubleshooting is much easier +if the circuit under investigation is encapsulated in a separate module. + +:numref:`submod` shows how the ``submod`` command can be used to split the +circuit from :numref:`memdemo_src` and :numref:`memdemo_00` into its components. +The ``-name`` option is used to specify the name of the new module and also the +name of the new cell in the current module. + +.. figure:: ../../images/011/submod_dots.* + :class: width-helper + :name: submod_dots + +.. code-block:: yoscrypt + :caption: The circuit from :numref:`memdemo_src` and :numref:`memdemo_00` + broken up using ``submod`` + :name: submod + + select -set outstage y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff + select -set selstage y %ci2:+$dff[Q,D] %ci*:-$dff @outstage %d + select -set scramble mem* %ci2 %ci*:-$dff mem* %d @selstage %d + submod -name scramble @scramble + submod -name outstage @outstage + submod -name selstage @selstage + +Evaluation of combinatorial circuits +------------------------------------ + +The ``eval`` command can be used to evaluate combinatorial circuits. For example +(see :numref:`submod` for the circuit diagram of ``selstage``): + +:: + + yosys [selstage]> eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1 + + 1. Executing EVAL pass (evaluate the circuit given an input). + Full command line: eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1 + Eval result: \n2 = 2'10. + Eval result: \n1 = 2'10. + +So the ``-set`` option is used to set input values and the ``-show`` option is +used to specify the nets to evaluate. If no ``-show`` option is specified, all +selected output ports are used per default. + +If a necessary input value is not given, an error is produced. The option +``-set-undef`` can be used to instead set all unspecified input nets to undef +(``x``). + +The ``-table`` option can be used to create a truth table. For example: + +:: + + yosys [selstage]> eval -set-undef -set d[3:1] 0 -table s1,d[0] + + 10. Executing EVAL pass (evaluate the circuit given an input). + Full command line: eval -set-undef -set d[3:1] 0 -table s1,d[0] + + \s1 \d [0] | \n1 \n2 + ---- ------ | ---- ---- + 2'00 1'0 | 2'00 2'00 + 2'00 1'1 | 2'xx 2'00 + 2'01 1'0 | 2'00 2'00 + 2'01 1'1 | 2'xx 2'01 + 2'10 1'0 | 2'00 2'00 + 2'10 1'1 | 2'xx 2'10 + 2'11 1'0 | 2'00 2'00 + 2'11 1'1 | 2'xx 2'11 + + Assumed undef (x) value for the following signals: \s2 + +Note that the ``eval`` command (as well as the ``sat`` command discussed in the +next sections) does only operate on flattened modules. It can not analyze +signals that are passed through design hierarchy levels. So the ``flatten`` +command must be used on modules that instantiate other modules before this +commands can be applied. + +Solving combinatorial SAT problems +---------------------------------- + +.. literalinclude:: ../../../manual/APPNOTE_011_Design_Investigation/primetest.v + :language: verilog + :caption: A simple miter circuit for testing if a number is prime. But it has + a problem (see main text and :numref:`primesat`). + :name: primetest + +.. code-block:: + :caption: Experiments with the miter circuit from :numref:`primetest`. + The first attempt of proving that 31 is prime failed because the + SAT solver found a creative way of factorizing 31 using integer + overflow. + :name: primesat + + yosys [primetest]> sat -prove ok 1 -set p 31 + + 8. Executing SAT pass (solving SAT problems in the circuit). + Full command line: sat -prove ok 1 -set p 31 + + Setting up SAT problem: + Import set-constraint: \p = 16'0000000000011111 + Final constraint equation: \p = 16'0000000000011111 + Imported 6 cells to SAT database. + Import proof-constraint: \ok = 1'1 + Final proof equation: \ok = 1'1 + + Solving problem with 2790 variables and 8241 clauses.. + SAT proof finished - model found: FAIL! + + ______ ___ ___ _ _ _ _ + (_____ \ / __) / __) (_) | | | | + _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | | + | ____/ ___) _ \ / _ (_ __) (_ __|____ | | || ___ |/ _ |_| + | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ + |_| |_| \___/ \___/ |_| |_| \_____|_|\_)_____)\____|_| + + + Signal Name Dec Hex Bin + -------------------- ---------- ---------- --------------------- + \a 15029 3ab5 0011101010110101 + \b 4099 1003 0001000000000011 + \ok 0 0 0 + \p 31 1f 0000000000011111 + + yosys [primetest]> sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0 + + 9. Executing SAT pass (solving SAT problems in the circuit). + Full command line: sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0 + + Setting up SAT problem: + Import set-constraint: \p = 16'0000000000011111 + Import set-constraint: { \a [15:8] \b [15:8] } = 16'0000000000000000 + Final constraint equation: { \a [15:8] \b [15:8] \p } = { 16'0000000000000000 16'0000000000011111 } + Imported 6 cells to SAT database. + Import proof-constraint: \ok = 1'1 + Final proof equation: \ok = 1'1 + + Solving problem with 2790 variables and 8257 clauses.. + SAT proof finished - no model found: SUCCESS! + + /$$$$$$ /$$$$$$$$ /$$$$$$$ + /$$__ $$ | $$_____/ | $$__ $$ + | $$ \ $$ | $$ | $$ \ $$ + | $$ | $$ | $$$$$ | $$ | $$ + | $$ | $$ | $$__/ | $$ | $$ + | $$/$$ $$ | $$ | $$ | $$ + | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$ + \____ $$$|__/|________/|__/|_______/|__/ + \__/ + +Often the opposite of the ``eval`` command is needed, i.e. the circuits output +is given and we want to find the matching input signals. For small circuits with +only a few input bits this can be accomplished by trying all possible input +combinations, as it is done by the ``eval -table`` command. For larger circuits +however, Yosys provides the ``sat`` command that uses a `SAT`_ solver, +`MiniSAT`_, to solve this kind of problems. + +.. _SAT: http://en.wikipedia.org/wiki/Circuit_satisfiability + +.. _MiniSAT: http://minisat.se/ + +The ``sat`` command works very similar to the ``eval`` command. The main +difference is that it is now also possible to set output values and find the +corresponding input values. For Example: + +:: + + yosys [selstage]> sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001 + + 11. Executing SAT pass (solving SAT problems in the circuit). + Full command line: sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001 + + Setting up SAT problem: + Import set-constraint: \s1 = \s2 + Import set-constraint: { \n2 \n1 } = 4'1001 + Final constraint equation: { \n2 \n1 \s1 } = { 4'1001 \s2 } + Imported 3 cells to SAT database. + Import show expression: { \s1 \s2 \d } + + Solving problem with 81 variables and 207 clauses.. + SAT solving finished - model found: + + Signal Name Dec Hex Bin + -------------------- ---------- ---------- --------------- + \d 9 9 1001 + \s1 0 0 00 + \s2 0 0 00 + +Note that the ``sat`` command supports signal names in both arguments to the +``-set`` option. In the above example we used ``-set s1 s2`` to constraint +``s1`` and ``s2`` to be equal. When more complex constraints are needed, a +wrapper circuit must be constructed that checks the constraints and signals if +the constraint was met using an extra output port, which then can be forced to a +value using the ``-set`` option. (Such a circuit that contains the circuit under +test plus additional constraint checking circuitry is called a ``miter`` +circuit.) + +:numref:`primetest` shows a miter circuit that is supposed to be used as a prime +number test. If ``ok`` is 1 for all input values ``a`` and ``b`` for a given +``p``, then ``p`` is prime, or at least that is the idea. + +The Yosys shell session shown in :numref:`primesat` demonstrates that SAT +solvers can even find the unexpected solutions to a problem: Using integer +overflow there actually is a way of "factorizing" 31. The clean solution would +of course be to perform the test in 32 bits, for example by replacing ``p != +a*b`` in the miter with ``p != {16'd0,a}b``, or by using a temporary variable +for the 32 bit product ``a*b``. But as 31 fits well into 8 bits (and as the +purpose of this document is to show off Yosys features) we can also simply force +the upper 8 bits of ``a`` and ``b`` to zero for the ``sat`` call, as is done in +the second command in :numref:`primesat` (line 31). + +The ``-prove`` option used in this example works similar to ``-set``, but tries +to find a case in which the two arguments are not equal. If such a case is not +found, the property is proven to hold for all inputs that satisfy the other +constraints. + +It might be worth noting, that SAT solvers are not particularly efficient at +factorizing large numbers. But if a small factorization problem occurs as part +of a larger circuit problem, the Yosys SAT solver is perfectly capable of +solving it. + +Solving sequential SAT problems +------------------------------- + +.. code-block:: + :caption: Solving a sequential SAT problem in the ``memdemo`` module from :numref:`memdemo_src`. + :name: memdemo_sat + + yosys [memdemo]> sat -seq 6 -show y -show d -set-init-undef \ + -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3 + + 6. Executing SAT pass (solving SAT problems in the circuit). + Full command line: sat -seq 6 -show y -show d -set-init-undef + -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3 + + Setting up time step 1: + Final constraint equation: { } = { } + Imported 29 cells to SAT database. + + Setting up time step 2: + Final constraint equation: { } = { } + Imported 29 cells to SAT database. + + Setting up time step 3: + Final constraint equation: { } = { } + Imported 29 cells to SAT database. + + Setting up time step 4: + Import set-constraint for timestep: \y = 4'0001 + Final constraint equation: \y = 4'0001 + Imported 29 cells to SAT database. + + Setting up time step 5: + Import set-constraint for timestep: \y = 4'0010 + Final constraint equation: \y = 4'0010 + Imported 29 cells to SAT database. + + Setting up time step 6: + Import set-constraint for timestep: \y = 4'0011 + Final constraint equation: \y = 4'0011 + Imported 29 cells to SAT database. + + Setting up initial state: + Final constraint equation: { \y \s2 \s1 \mem[3] \mem[2] \mem[1] + \mem[0] } = 24'xxxxxxxxxxxxxxxxxxxxxxxx + + Import show expression: \y + Import show expression: \d + + Solving problem with 10322 variables and 27881 clauses.. + SAT model found. maximizing number of undefs. + SAT solving finished - model found: + + Time Signal Name Dec Hex Bin + ---- -------------------- ---------- ---------- --------------- + init \mem[0] -- -- xxxx + init \mem[1] -- -- xxxx + init \mem[2] -- -- xxxx + init \mem[3] -- -- xxxx + init \s1 -- -- xx + init \s2 -- -- xx + init \y -- -- xxxx + ---- -------------------- ---------- ---------- --------------- + 1 \d 0 0 0000 + 1 \y -- -- xxxx + ---- -------------------- ---------- ---------- --------------- + 2 \d 1 1 0001 + 2 \y -- -- xxxx + ---- -------------------- ---------- ---------- --------------- + 3 \d 2 2 0010 + 3 \y 0 0 0000 + ---- -------------------- ---------- ---------- --------------- + 4 \d 3 3 0011 + 4 \y 1 1 0001 + ---- -------------------- ---------- ---------- --------------- + 5 \d -- -- 001x + 5 \y 2 2 0010 + ---- -------------------- ---------- ---------- --------------- + 6 \d -- -- xxxx + 6 \y 3 3 0011 + +The SAT solver functionality in Yosys can not only be used to solve +combinatorial problems, but can also solve sequential problems. Let's consider +the entire memdemo module from :numref:`memdemo_src` and suppose we want to know +which sequence of input values for ``d`` will cause the output y to produce the +sequence 1, 2, 3 from any initial state. :numref:`memdemo_sat` show the solution +to this question, as produced by the following command: + +.. code-block:: yoscrypt + + sat -seq 6 -show y -show d -set-init-undef \ + -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3 + +The ``-seq 6`` option instructs the ``sat`` command to solve a sequential +problem in 6 time steps. (Experiments with lower number of steps have show that +at least 3 cycles are necessary to bring the circuit in a state from which the +sequence 1, 2, 3 can be produced.) + +The ``-set-init-undef`` option tells the ``sat`` command to initialize all +registers to the undef (``x``) state. The way the ``x`` state is treated in +Verilog will ensure that the solution will work for any initial state. + +The ``-max_undef`` option instructs the ``sat`` command to find a solution with +a maximum number of undefs. This way we can see clearly which inputs bits are +relevant to the solution. + +Finally the three ``-set-at`` options add constraints for the ``y`` signal to +play the 1, 2, 3 sequence, starting with time step 4. + +It is not surprising that the solution sets ``d = 0`` in the first step, as this +is the only way of setting the ``s1`` and ``s2`` registers to a known value. The +input values for the other steps are a bit harder to work out manually, but the +SAT solver finds the correct solution in an instant. + +There is much more to write about the ``sat`` command. For example, there is a +set of options that can be used to performs sequential proofs using temporal +induction :cite:p:`een2003temporal`. The command ``help sat`` can be used to +print a list of all options with short descriptions of their functions. + +.. _conclusion: + +Conclusion +========== + +Yosys provides a wide range of functions to analyze and investigate +designs. For many cases it is sufficient to simply display circuit +diagrams, maybe use some additional commands to narrow the scope of the +circuit diagrams to the interesting parts of the circuit. But some cases +require more than that. For this applications Yosys provides commands +that can be used to further inspect the behavior of the circuit, either +by evaluating which output values are generated from certain input +values (``eval``) or by evaluation which input values and initial conditions +can result in a certain behavior at the outputs (``sat``). The SAT command +can even be used to prove (or disprove) theorems regarding the circuit, +in more advanced cases with the additional help of a miter circuit. + +This features can be powerful tools for the circuit designer using Yosys +as a utility for building circuits and the software developer using +Yosys as a framework for new algorithms alike. diff --git a/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst b/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst new file mode 100644 index 000000000..e9e44d1cd --- /dev/null +++ b/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst @@ -0,0 +1,333 @@ +==================================== +012: Converting Verilog to BTOR page +==================================== + +Installation +============ + +Yosys written in C++ (using features from C++11) and is tested on modern Linux. +It should compile fine on most UNIX systems with a C++11 compiler. The README +file contains useful information on building Yosys and its prerequisites. + +Yosys is a large and feature-rich program with some dependencies. For this work, +we may deactivate other extra features such as TCL and ABC support in the +Makefile. + +This Application Note is based on `Yosys GIT`_ `Rev. 082550f` from 2015-04-04. + +.. _Yosys GIT: https://github.com/YosysHQ/yosys + +.. _Rev. 082550f: https://github.com/YosysHQ/yosys/tree/082550f + +Quick start +=========== + +We assume that the Verilog design is synthesizable and we also assume that the +design does not have multi-dimensional memories. As BTOR implicitly initializes +registers to zero value and memories stay uninitialized, we assume that the +Verilog design does not contain initial blocks. For more details about the BTOR +format, please refer to :cite:p:`btor`. + +We provide a shell script ``verilog2btor.sh`` which can be used to convert a +Verilog design to BTOR. The script can be found in the ``backends/btor`` +directory. The following example shows its usage: + +.. code:: sh + + verilog2btor.sh fsm.v fsm.btor test + +The script ``verilog2btor.sh`` takes three parameters. In the above example, the +first parameter ``fsm.v`` is the input design, the second parameter ``fsm.btor`` +is the file name of BTOR output, and the third parameter ``test`` is the name of +top module in the design. + +To specify the properties (that need to be checked), we have two +options: + +- We can use the Verilog ``assert`` statement in the procedural block or module + body of the Verilog design, as shown in :numref:`specifying_property_assert`. + This is the preferred option. + +- We can use a single-bit output wire, whose name starts with ``safety``. The + value of this output wire needs to be driven low when the property is met, + i.e. the solver will try to find a model that makes the safety pin go high. + This is demonstrated in :numref:`specifying_property_output`. + +.. code-block:: verilog + :caption: Specifying property in Verilog design with ``assert`` + :name: specifying_property_assert + + module test(input clk, input rst, output y); + + reg [2:0] state; + + always @(posedge clk) begin + if (rst || state == 3) begin + state <= 0; + end else begin + assert(state < 3); + state <= state + 1; + end + end + + assign y = state[2]; + + assert property (y !== 1'b1); + + endmodule + +.. code-block:: verilog + :caption: Specifying property in Verilog design with output wire + :name: specifying_property_output + + module test(input clk, input rst, + output y, output safety1); + + reg [2:0] state; + + always @(posedge clk) begin + if (rst || state == 3) + state <= 0; + else + state <= state + 1; + end + + assign y = state[2]; + + assign safety1 = !(y !== 1'b1); + + endmodule + +We can run `Boolector`_ ``1.4.1`` [1]_ on the generated BTOR file: + +.. _Boolector: http://fmv.jku.at/boolector/ + +.. code:: sh + + $ boolector fsm.btor + unsat + +We can also use `nuXmv`_, but on BTOR designs it does not support memories yet. +With the next release of nuXmv, we will be also able to verify designs with +memories. + +.. _nuXmv: https://es-static.fbk.eu/tools/nuxmv/index.php + +Detailed flow +============= + +Yosys is able to synthesize Verilog designs up to the gate level. We are +interested in keeping registers and memories when synthesizing the design. For +this purpose, we describe a customized Yosys synthesis flow, that is also +provided by the ``verilog2btor.sh`` script. :numref:`btor_script_memory` shows +the Yosys commands that are executed by ``verilog2btor.sh``. + +.. code-block:: yoscrypt + :caption: Synthesis Flow for BTOR with memories + :name: btor_script_memory + + read_verilog -sv $1; + hierarchy -top $3; hierarchy -libdir $DIR; + hierarchy -check; + proc; opt; + opt_expr -mux_undef; opt; + rename -hide;;; + splice; opt; + memory_dff -wr_only; memory_collect;; + flatten;; + memory_unpack; + splitnets -driver; + setundef -zero -undriven; + opt;;; + write_btor $2; + +Here is short description of what is happening in the script line by +line: + +#. Reading the input file. + +#. Setting the top module in the hierarchy and trying to read automatically the + files which are given as ``include`` in the file read in first line. + +#. Checking the design hierarchy. + +#. Converting processes to multiplexers (muxs) and flip-flops. + +#. Removing undef signals from muxs. + +#. Hiding all signal names that are not used as module ports. + +#. Explicit type conversion, by introducing slice and concat cells in the + circuit. + +#. Converting write memories to synchronous memories, and collecting the + memories to multi-port memories. + +#. Flattening the design to get only one module. + +#. Separating read and write memories. + +#. Splitting the signals that are partially assigned + +#. Setting undef to zero value. + +#. Final optimization pass. + +#. Writing BTOR file. + +For detailed description of the commands mentioned above, please refer +to the Yosys documentation, or run ``yosys -h ``. + +The script presented earlier can be easily modified to have a BTOR file that +does not contain memories. This is done by removing the line number 8 and 10, +and introduces a new command ``memory`` at line number 8. +:numref:`btor_script_without_memory` shows the modified Yosys script file: + +.. code-block:: sh + :caption: Synthesis Flow for BTOR without memories + :name: btor_script_without_memory + + read_verilog -sv $1; + hierarchy -top $3; hierarchy -libdir $DIR; + hierarchy -check; + proc; opt; + opt_expr -mux_undef; opt; + rename -hide;;; + splice; opt; + memory;; + flatten;; + splitnets -driver; + setundef -zero -undriven; + opt;;; + write_btor $2; + +Example +======= + +Here is an example Verilog design that we want to convert to BTOR: + +.. code-block:: verilog + :caption: Example - Verilog Design + :name: example_verilog + + module array(input clk); + + reg [7:0] counter; + reg [7:0] mem [7:0]; + + always @(posedge clk) begin + counter <= counter + 8'd1; + mem[counter] <= counter; + end + + assert property (!(counter > 8'd0) || + mem[counter - 8'd1] == counter - 8'd1); + + endmodule + +The generated BTOR file that contain memories, using the script shown in +:numref:`btor_memory`: + +.. code-block:: + :caption: Example - Converted BTOR with memory + :name: btor_memory + + 1 var 1 clk + 2 array 8 3 + 3 var 8 $auto$rename.cc:150:execute$20 + 4 const 8 00000001 + 5 sub 8 3 4 + 6 slice 3 5 2 0 + 7 read 8 2 6 + 8 slice 3 3 2 0 + 9 add 8 3 4 + 10 const 8 00000000 + 11 ugt 1 3 10 + 12 not 1 11 + 13 const 8 11111111 + 14 slice 1 13 0 0 + 15 one 1 + 16 eq 1 1 15 + 17 and 1 16 14 + 18 write 8 3 2 8 3 + 19 acond 8 3 17 18 2 + 20 anext 8 3 2 19 + 21 eq 1 7 5 + 22 or 1 12 21 + 23 const 1 1 + 24 one 1 + 25 eq 1 23 24 + 26 cond 1 25 22 24 + 27 root 1 -26 + 28 cond 8 1 9 3 + 29 next 8 3 28 + +And the BTOR file obtained by the script shown in +:numref:`btor_without_memory`, which expands the memory into individual +elements: + +.. code-block:: + :caption: Example - Converted BTOR with memory + :name: btor_without_memory + + 1 var 1 clk + 2 var 8 mem[0] + 3 var 8 $auto$rename.cc:150:execute$20 + 4 slice 3 3 2 0 + 5 slice 1 4 0 0 + 6 not 1 5 + 7 slice 1 4 1 1 + 8 not 1 7 + 9 slice 1 4 2 2 + 10 not 1 9 + 11 and 1 8 10 + 12 and 1 6 11 + 13 cond 8 12 3 2 + 14 cond 8 1 13 2 + 15 next 8 2 14 + 16 const 8 00000001 + 17 add 8 3 16 + 18 const 8 00000000 + 19 ugt 1 3 18 + 20 not 1 19 + 21 var 8 mem[2] + 22 and 1 7 10 + 23 and 1 6 22 + 24 cond 8 23 3 21 + 25 cond 8 1 24 21 + 26 next 8 21 25 + 27 sub 8 3 16 + + ... + + 54 cond 1 53 50 52 + 55 root 1 -54 + + ... + + 77 cond 8 76 3 44 + 78 cond 8 1 77 44 + 79 next 8 44 78 + +Limitations +=========== + +BTOR does not support initialization of memories and registers, i.e. they are +implicitly initialized to value zero, so the initial block for memories need to +be removed when converting to BTOR. It should also be kept in consideration that +BTOR does not support the ``x`` or ``z`` values of Verilog. + +Another thing to bear in mind is that Yosys will convert multi-dimensional +memories to one-dimensional memories and address decoders. Therefore +out-of-bounds memory accesses can yield unexpected results. + +Conclusion +========== + +Using the described flow, we can use Yosys to generate word-level verification +benchmarks with or without memories from Verilog designs. + +.. [1] + Newer version of Boolector do not support sequential models. + Boolector 1.4.1 can be built with picosat-951. Newer versions of + picosat have an incompatible API. diff --git a/docs/source/appendix/CHAPTER_Auxlibs.rst b/docs/source/appendix/CHAPTER_Auxlibs.rst new file mode 100644 index 000000000..361f00e02 --- /dev/null +++ b/docs/source/appendix/CHAPTER_Auxlibs.rst @@ -0,0 +1,42 @@ +Auxiliary libraries +=================== + +The Yosys source distribution contains some auxiliary libraries that are bundled +with Yosys. + +SHA1 +---- + +The files in ``libs/sha1/`` provide a public domain SHA1 implementation written +by Steve Reid, Bruce Guenter, and Volker Grabsch. It is used for generating +unique names when specializing parameterized modules. + +BigInt +------ + +The files in ``libs/bigint/`` provide a library for performing arithmetic with +arbitrary length integers. It is written by Matt McCutchen. + +The BigInt library is used for evaluating constant expressions, e.g. using the +ConstEval class provided in kernel/consteval.h. + +See also: http://mattmccutchen.net/bigint/ + +.. _sec:SubCircuit: + +SubCircuit +---------- + +The files in ``libs/subcircuit`` provide a library for solving the subcircuit +isomorphism problem. It is written by C. Wolf and based on the Ullmann Subgraph +Isomorphism Algorithm :cite:p:`UllmannSubgraphIsomorphism`. It is used by the +extract pass (see :doc:`../cmd/extract`). + +ezSAT +----- + +The files in ``libs/ezsat`` provide a library for simplifying generating CNF +formulas for SAT solvers. It also contains bindings of MiniSAT. The ezSAT +library is written by C. Wolf. It is used by the sat pass (see +:doc:`../cmd/sat`). + diff --git a/docs/source/appendix/CHAPTER_Auxprogs.rst b/docs/source/appendix/CHAPTER_Auxprogs.rst new file mode 100644 index 000000000..e4f6f62cf --- /dev/null +++ b/docs/source/appendix/CHAPTER_Auxprogs.rst @@ -0,0 +1,29 @@ +Auxiliary programs +================== + +Besides the main yosys executable, the Yosys distribution contains a set of +additional helper programs. + +yosys-config +------------ + +The yosys-config tool (an auto-generated shell-script) can be used to query +compiler options and other information needed for building loadable modules for +Yosys. See Sec. \ :numref:`chapter:prog` for details. + +.. _sec:filterlib: + +yosys-filterlib +--------------- + +The yosys-filterlib tool is a small utility that can be used to strip or extract +information from a Liberty file. See :numref:`Sec. %s ` for +details. + +yosys-abc +--------- + +This is a fork of ABC with a small set of custom modifications that have not yet +been accepted upstream. 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/docs/source/appendix/CHAPTER_StateOfTheArt.rst b/docs/source/appendix/CHAPTER_StateOfTheArt.rst new file mode 100644 index 000000000..894d0fbbe --- /dev/null +++ b/docs/source/appendix/CHAPTER_StateOfTheArt.rst @@ -0,0 +1,410 @@ +.. _chapter:sota: + +Evaluation of other OSS Verilog Synthesis Tools +=============================================== + +In this appendix [1]_ the existing FOSS Verilog synthesis tools [2]_ are +evaluated. Extremely limited or application specific tools (e.g. pure +Verilog Netlist parsers) as well as Verilog simulators are not included. +These existing solutions are tested using a set of representative +Verilog code snippets. It is shown that no existing FOSS tool implements +even close to a sufficient subset of Verilog to be usable as synthesis +tool for a wide range existing Verilog code. + +The packages evaluated are: + +- Icarus Verilog [3]_ + +- Verilog-to-Routing (VTR) / Odin-II + :cite:p:`vtr2012}`:raw-latex:`\cite{Odin` + +- HDL Analyzer and Netlist Architect (HANA) + +- Verilog front-end to VIS (vl2mv) :cite:p:`Cheng93vl2mv:a` + +In each of the following sections Verilog modules that test a certain +Verilog language feature are presented and the support for these +features is tested in all the tools mentioned above. It is evaluated +whether the tools under test successfully generate netlists for the +Verilog input and whether these netlists match the simulation behavior +of the designs using testbenches. + +All test cases are verified to be synthesizeable using Xilinx XST from +the Xilinx WebPACK suite. + +Trivial features such as support for simple structural Verilog are not +explicitly tested. + +Vl2mv and Odin-II generate output in the BLIF (Berkeley Logic +Interchange Format) and BLIF-MV (an extended version of BLIF) formats +respectively. ABC is used to convert this output to Verilog for +verification using testbenches. + +Icarus Verilog generates EDIF (Electronic Design Interchange Format) +output utilizing LPM (Library of Parameterized Modules) cells. The EDIF +files are converted to Verilog using edif2ngd and netgen from Xilinx +WebPACK. A hand-written implementation of the LPM cells utilized by the +generated netlists is used for verification. + +Following these functional tests, a quick analysis of the extensibility +of the tools under test is provided in a separate section. + +The last section of this chapter finally concludes these series of +evaluations with a summary of the results. + +.. code:: verilog + :number-lines: + + module uut_always01(clock, + reset, count); + + input clock, reset; + output [3:0] count; + reg [3:0] count; + + always @(posedge clock) + count <= reset ? + 0 : count + 1; + + + + endmodule + +.. code:: verilog + + module uut_always02(clock, + reset, count); + + input clock, reset; + output [3:0] count; + reg [3:0] count; + + always @(posedge clock) begin + count <= count + 1; + if (reset) + count <= 0; + end + + endmodule + +[fig:StateOfTheArt_always12] + +.. code:: verilog + :number-lines: + + module uut_always03(clock, in1, in2, in3, in4, in5, in6, in7, + out1, out2, out3); + + input clock, in1, in2, in3, in4, in5, in6, in7; + output out1, out2, out3; + reg out1, out2, out3; + + always @(posedge clock) begin + out1 = in1; + if (in2) + out1 = !out1; + out2 <= out1; + if (in3) + out2 <= out2; + if (in4) + if (in5) + out3 <= in6; + else + out3 <= in7; + out1 = out1 ^ out2; + end + + endmodule + +[fig:StateOfTheArt_always3] + +.. _sec:blocking_nonblocking: + +Always blocks and blocking vs. nonblocking assignments +------------------------------------------------------ + +The "always"-block is one of the most fundamental non-trivial Verilog +language features. It can be used to model a combinatorial path (with +optional registers on the outputs) in a way that mimics a regular +programming language. + +Within an always block, if- and case-statements can be used to model +multiplexers. Blocking assignments (:math:`=`) and nonblocking +assignments (:math:`<=`) are used to populate the leaf-nodes of these +multiplexer trees. Unassigned leaf-nodes default to feedback paths that +cause the output register to hold the previous value. More advanced +synthesis tools often convert these feedback paths to register enable +signals or even generate circuits with clock gating. + +Registers assigned with nonblocking assignments (:math:`<=`) behave +differently from variables in regular programming languages: In a +simulation they are not updated immediately after being assigned. +Instead the right-hand sides are evaluated and the results stored in +temporary memory locations. After all pending updates have been prepared +in this way they are executed, thus yielding semi-parallel execution of +all nonblocking assignments. + +For synthesis this means that every occurrence of that register in an +expression addresses the output port of the corresponding register +regardless of the question whether the register has been assigned a new +value in an earlier command in the same always block. Therefore with +nonblocking assignments the order of the assignments has no effect on +the resulting circuit as long as the left-hand sides of the assignments +are unique. + +The three example codes in +:numref:`Fig. %s ` +and :numref:`Fig. %s ` +use all these features and can thus be used to test the synthesis tools +capabilities to synthesize always blocks correctly. + +The first example is only using the most fundamental Verilog features. +All tools under test were able to successfully synthesize this design. + +.. code:: verilog + :number-lines: + + module uut_arrays01(clock, we, addr, wr_data, rd_data); + + input clock, we; + input [3:0] addr, wr_data; + output [3:0] rd_data; + reg [3:0] rd_data; + + reg [3:0] memory [15:0]; + + always @(posedge clock) begin + if (we) + memory[addr] <= wr_data; + rd_data <= memory[addr]; + end + + endmodule + +[fig:StateOfTheArt_arrays] + +The 2nd example is functionally identical to the 1st one but is using an +if-statement inside the always block. Odin-II fails to synthesize it and +instead produces the following error message: + +:: + + ERROR: (File: always02.v) (Line number: 13) + You've defined the driver "count~0" twice + +Vl2mv does not produce an error message but outputs an invalid synthesis +result that is not using the reset input at all. + +Icarus Verilog also doesn't produce an error message but generates an +invalid output for this 2nd example. The code generated by Icarus +Verilog only implements the reset path for the count register, +effectively setting the output to constant 0. + +So of all tools under test only HANA was able to create correct +synthesis results for the 2nd example. + +The 3rd example is using blocking and nonblocking assignments and many +if statements. Odin also fails to synthesize this example: + +:: + + ERROR: (File: always03.v) (Line number: 8) + ODIN doesn't handle blocking statements in Sequential blocks + +HANA, Icarus Verilog and vl2mv create invalid synthesis results for the +3rd example. + +So unfortunately none of the tools under test provide a complete and +correct implementation of blocking and nonblocking assignments. + +Arrays for memory modelling +--------------------------- + +Verilog arrays are part of the synthesizeable subset of Verilog and are +commonly used to model addressable memory. The Verilog code in +:numref:`Fig. %s ` +demonstrates this by implementing a single port memory. + +For this design HANA, vl2m and ODIN-II generate error messages +indicating that arrays are not supported. + +.. code:: verilog + :number-lines: + + module uut_forgen01(a, y); + + input [4:0] a; + output y; + + integer i, j; + reg [31:0] lut; + + initial begin + for (i = 0; i < 32; i = i+1) begin + lut[i] = i > 1; + for (j = 2; j*j <= i; j = j+1) + if (i % j == 0) + lut[i] = 0; + end + end + + assign y = lut[a]; + + endmodule + +[fig:StateOfTheArt_for] + +Icarus Verilog produces an invalid output that is using the address only +for reads. Instead of using the address input for writes, the generated +design simply loads the data to all memory locations whenever the +write-enable input is active, effectively turning the design into a +single 4-bit D-Flip-Flop with enable input. + +As all tools under test already fail this simple test, there is nothing +to gain by continuing tests on this aspect of Verilog synthesis such as +synthesis of dual port memories, correct handling of write collisions, +and so forth. + +.. code:: verilog + :number-lines: + + module uut_forgen02(a, b, cin, y, cout); + + parameter WIDTH = 8; + + input [WIDTH-1:0] a, b; + input cin; + + output [WIDTH-1:0] y; + output cout; + + genvar i; + wire [WIDTH-1:0] carry; + + generate + for (i = 0; i < WIDTH; i=i+1) begin:adder + wire [2:0] D; + assign D[1:0] = { a[i], b[i] }; + if (i == 0) begin:chain + assign D[2] = cin; + end else begin:chain + assign D[2] = carry[i-1]; + end + assign y[i] = ^D; + assign carry[i] = &D[1:0] | (^D[1:0] & D[2]); + end + endgenerate + + assign cout = carry[WIDTH-1]; + + endmodule + +[fig:StateOfTheArt_gen] + +For-loops and generate blocks +----------------------------- + +For-loops and generate blocks are more advanced Verilog features. These +features allow the circuit designer to add program code to her design +that is evaluated during synthesis to generate (parts of) the circuits +description; something that could only be done using a code generator +otherwise. + +For-loops are only allowed in synthesizeable Verilog if they can be +completely unrolled. Then they can be a powerful tool to generate array +logic or static lookup tables. The code in +:numref:`Fig. %s ` generates a +circuit that tests a 5 bit value for being a prime number using a static +lookup table. + +Generate blocks can be used to model array logic in complex parametric +designs. The code in +:numref:`Fig. %s ` implements a +ripple-carry adder with parametric width from simple assign-statements +and logic operations using a Verilog generate block. + +All tools under test failed to synthesize both test cases. HANA creates +invalid output in both cases. Icarus Verilog creates invalid output for +the first test and fails with an error for the second case. The other +two tools fail with error messages for both tests. + +Extensibility +------------- + +This section briefly discusses the extensibility of the tools under test +and their internal data- and control-flow. As all tools under test +already failed to synthesize simple Verilog always-blocks correctly, not +much resources have been spent on evaluating the extensibility of these +tools and therefore only a very brief discussion of the topic is +provided here. + +HANA synthesizes for a built-in library of standard cells using two +passes over an AST representation of the Verilog input. This approach +executes fast but limits the extensibility as everything happens in only +two comparable complex AST walks and there is no universal intermediate +representation that is flexible enough to be used in arbitrary +optimizations. + +Odin-II and vl2m are both front ends to existing synthesis flows. As +such they only try to quickly convert the Verilog input into the +internal representation of their respective flows (BLIF). So +extensibility is less of an issue here as potential extensions would +likely be implemented in other components of the flow. + +Icarus Verilog is clearly designed to be a simulation tool rather than a +synthesis tool. The synthesis part of Icarus Verilog is an ad-hoc add-on +to Icarus Verilog that aims at converting an internal representation +that is meant for generation of a virtual machine based simulation code +to netlists. + +Summary and Outlook +------------------- + +Table \ :numref:`tab:StateOfTheArt_sum` summarizes +the tests performed. Clearly none of the tools under test make a serious +attempt at providing a feature-complete implementation of Verilog. It +can be argued that Odin-II performed best in the test as it never +generated incorrect code but instead produced error messages indicating +that unsupported Verilog features where used in the Verilog input. + +In conclusion, to the best knowledge of the author, there is no FOSS +Verilog synthesis tool other than Yosys that is anywhere near feature +completeness and therefore there is no other candidate for a generic +Verilog front end and/or synthesis framework to be used as a basis for +custom synthesis tools. + +Yosys could also replace vl2m and/or Odin-II in their respective flows +or function as a pre-compiler that can translate full-featured Verilog +code to the simple subset of Verilog that is understood by vl2m and +Odin-II. + +Yosys is designed for extensibility. It can be used as-is to synthesize +Verilog code to netlists, but its main purpose is to be used as basis +for custom tools. Yosys is structured in a language dependent Verilog +front end and language independent synthesis code (which is in itself +structured in independent passes). This architecture will simplify +implementing additional HDL front ends and/or additional synthesis +passes. + +Chapter \ :numref:`` contains a more detailed +evaluation of Yosys using real-world designs that are far out of reach +for any of the other tools discussed in this appendix. + +…passed 2em …produced error 2em :math:`\skull` …incorrect output + +[tab:StateOfTheArt_sum] + +.. [1] + This appendix is an updated version of an unpublished student + research paper. :cite:p:`VerilogFossEval` + +.. [2] + To the author's best knowledge, all relevant tools that existed at + the time of this writing are included. But as there is no formal + channel through which such tools are published it is hard to give any + guarantees in that matter. + +.. [3] + Icarus Verilog is mainly a simulation tool but also supported + synthesis up to version 0.8. Therefore version 0.8.7 is used for this + evaluation.) diff --git a/docs/source/appendix/CHAPTER_TextRtlil.rst b/docs/source/appendix/CHAPTER_TextRtlil.rst new file mode 100644 index 000000000..dc3d72230 --- /dev/null +++ b/docs/source/appendix/CHAPTER_TextRtlil.rst @@ -0,0 +1,298 @@ +.. _chapter:textrtlil: + +RTLIL text representation +========================= + +This appendix documents the text representation of RTLIL in extended Backus-Naur +form (EBNF). + +The grammar is not meant to represent semantic limitations. That is, the grammar +is "permissive", and later stages of processing perform more rigorous checks. + +The grammar is also not meant to represent the exact grammar used in the RTLIL +frontend, since that grammar is specific to processing by lex and yacc, is even +more permissive, and is somewhat less understandable than simple EBNF notation. + +Finally, note that all statements (rules ending in ``-stmt``) terminate in an +end-of-line. Because of this, a statement cannot be broken into multiple lines. + +Lexical elements +---------------- + +Characters +~~~~~~~~~~ + +An RTLIL file is a stream of bytes. Strictly speaking, a "character" in an RTLIL +file is a single byte. The lexer treats multi-byte encoded characters as +consecutive single-byte characters. While other encodings *may* work, UTF-8 is +known to be safe to use. Byte order marks at the beginning of the file will +cause an error. + +ASCII spaces (32) and tabs (9) separate lexer tokens. + +A ``nonws`` character, used in identifiers, is any character whose encoding +consists solely of bytes above ASCII space (32). + +An ``eol`` is one or more consecutive ASCII newlines (10) and carriage returns +(13). + +Identifiers +~~~~~~~~~~~ + +There are two types of identifiers in RTLIL: + +- Publically visible identifiers +- Auto-generated identifiers + +.. code:: BNF + + ::= | + ::= \ + + ::= $ + + +Values +~~~~~~ + +A *value* consists of a width in bits and a bit representation, most +significant bit first. Bits may be any of: + +- ``0``: A logic zero value +- ``1``: A logic one value +- ``x``: An unknown logic value (or don't care in case patterns) +- ``z``: A high-impedance value (or don't care in case patterns) +- ``m``: A marked bit (internal use only) +- ``-``: A don't care value + +An *integer* is simply a signed integer value in decimal format. **Warning:** +Integer constants are limited to 32 bits. That is, they may only be in the range +:math:`[-2147483648, 2147483648)`. Integers outside this range will result in an +error. + +.. code:: BNF + + ::= + ' * + ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 + ::= 0 | 1 | x | z | m | - + ::= -? + + +Strings +~~~~~~~ + +A string is a series of characters delimited by double-quote characters. Within +a string, any character except ASCII NUL (0) may be used. In addition, certain +escapes can be used: + +- ``\n``: A newline +- ``\t``: A tab +- ``\ooo``: A character specified as a one, two, or three digit octal value + +All other characters may be escaped by a backslash, and become the following +character. Thus: + +- ``\\``: A backslash +- ``\"``: A double-quote +- ``\r``: An 'r' character + +Comments +~~~~~~~~ + +A comment starts with a ``#`` character and proceeds to the end of the line. All +comments are ignored. + +File +---- + +A file consists of an optional autoindex statement followed by zero or more +modules. + +.. code:: BNF + + ::= ? * + +Autoindex statements +~~~~~~~~~~~~~~~~~~~~ + +The autoindex statement sets the global autoindex value used by Yosys when it +needs to generate a unique name, e.g. ``flattenN``. The N part is filled with +the value of the global autoindex value, which is subsequently incremented. This +global has to be dumped into RTLIL, otherwise e.g. dumping and running a pass +would have different properties than just running a pass on a warm design. + +.. code:: BNF + + ::= autoidx + +Modules +~~~~~~~ + +Declares a module, with zero or more attributes, consisting of zero or more +wires, memories, cells, processes, and connections. + +.. code:: BNF + + ::= * + ::= module + ::= ( + | + | + | + | )* + ::= parameter ? + ::= | | + ::= end + +Attribute statements +~~~~~~~~~~~~~~~~~~~~ + +Declares an attribute with the given identifier and value. + +.. code:: BNF + + ::= attribute + +Signal specifications +~~~~~~~~~~~~~~~~~~~~~ + +A signal is anything that can be applied to a cell port, i.e. a constant value, +all bits or a selection of bits from a wire, or concatenations of those. + +**Warning:** When an integer constant is a sigspec, it is always 32 bits wide, +2's complement. For example, a constant of :math:`-1` is the same as +``32'11111111111111111111111111111111``, while a constant of :math:`1` is the +same as ``32'1``. + +See :numref:`Sec. %s ` for an overview of signal +specifications. + +.. code:: BNF + + ::= + | + | [ (:)? ] + | { * } + +Connections +~~~~~~~~~~~ + +Declares a connection between the given signals. + +.. code:: BNF + + ::= connect + +Wires +~~~~~ + +Declares a wire, with zero or more attributes, with the given identifier and +options in the enclosing module. + +See :numref:`Sec. %s ` for an overview of wires. + +.. code:: BNF + + ::= * + ::= wire * + ::= + ::= width + | offset + | input + | output + | inout + | upto + | signed + +Memories +~~~~~~~~ + +Declares a memory, with zero or more attributes, with the given identifier and +options in the enclosing module. + +See :numref:`Sec. %s ` for an overview of memory cells, and +:numref:`Sec. %s ` for details about memory cell types. + +.. code:: BNF + + ::= * + ::= memory * + ::= width + | size + | offset + +Cells +~~~~~ + +Declares a cell, with zero or more attributes, with the given identifier and +type in the enclosing module. + +Cells perform functions on input signals. See :numref:`Chap. %s +` for a detailed list of cell types. + +.. code:: BNF + + ::= * * + ::= cell + ::= + ::= + ::= parameter (signed | real)? + | connect + ::= end + + +Processes +~~~~~~~~~ + +Declares a process, with zero or more attributes, with the given identifier in +the enclosing module. The body of a process consists of zero or more +assignments, exactly one switch, and zero or more syncs. + +See :numref:`Sec. %s ` for an overview of processes. + +.. code:: BNF + + ::= * + ::= process + ::= * ? * * + ::= assign + ::= + ::= + ::= end + +Switches +~~~~~~~~ + +Switches test a signal for equality against a list of cases. Each case specifies +a comma-separated list of signals to check against. If there are no signals in +the list, then the case is the default case. The body of a case consists of zero +or more switches and assignments. Both switches and cases may have zero or more +attributes. + +.. code:: BNF + + ::= * + := * switch + ::= * + ::= case ? + ::= (, )* + ::= ( | )* + ::= end + +Syncs +~~~~~ + +Syncs update signals with other signals when an event happens. Such an event may +be: + +- An edge or level on a signal +- Global clock ticks +- Initialization +- Always + +.. code:: BNF + + ::= * + ::= sync + | sync global + | sync init + | sync always + ::= low | high | posedge | negedge | edge + ::= update diff --git a/docs/source/bib.rst b/docs/source/bib.rst new file mode 100644 index 000000000..21f85a869 --- /dev/null +++ b/docs/source/bib.rst @@ -0,0 +1,9 @@ +.. only:: html + + Literature references + ===================== + + .. rubric:: Bibliography + +.. bibliography:: literature.bib + diff --git a/docs/source/cmd_ref.rst b/docs/source/cmd_ref.rst new file mode 100644 index 000000000..4b9dc91f3 --- /dev/null +++ b/docs/source/cmd_ref.rst @@ -0,0 +1,11 @@ +.. _cmd_ref: + +================================================================================ +Command line reference +================================================================================ +.. toctree:: + :caption: Command reference + :maxdepth: 1 + :glob: + + cmd/* diff --git a/docs/source/conf.py b/docs/source/conf.py new file mode 100644 index 000000000..ab9618c8b --- /dev/null +++ b/docs/source/conf.py @@ -0,0 +1,62 @@ +#!/usr/bin/env python3 +import sys +import os + +project = 'YosysHQ Yosys' +author = 'YosysHQ GmbH' +copyright ='2022 YosysHQ GmbH' + +# select HTML theme +html_theme = 'press' +html_logo = '../static/logo.png' +html_favicon = '../static/favico.png' +html_css_files = ['yosyshq.css', 'custom.css'] +html_sidebars = {'**': ['util/searchbox.html', 'util/sidetoc.html']} + +# These folders are copied to the documentation's HTML output +html_static_path = ['../static', "../images"] + +# code blocks style +pygments_style = 'colorful' +highlight_language = 'none' + +html_theme_options = { + 'external_links' : [ + ('YosysHQ Docs', 'https://yosyshq.readthedocs.io'), + ('Blog', 'https://blog.yosyshq.com'), + ('Website', 'https://www.yosyshq.com'), + ], +} + +extensions = ['sphinx.ext.autosectionlabel', 'sphinxcontrib.bibtex'] + +# Ensure that autosectionlabel will produce unique names +autosectionlabel_prefix_document = True +autosectionlabel_maxdepth = 1 + +# assign figure numbers +numfig = True + +bibtex_bibfiles = ['literature.bib'] + +# unused docs +exclude_patterns = [ + "CHAPTER_Eval.rst", + "appendix/CHAPTER_StateOfTheArt.rst" +] + +latex_elements = { + 'preamble': r''' +\usepackage{lmodern} +\usepackage{comment} + +''' +} + +def setup(sphinx): + sys.path += [os.path.dirname(__file__) + "/../util"] + from RtlilLexer import RtlilLexer + sphinx.add_lexer("RTLIL", RtlilLexer) + + from YoscryptLexer import YoscryptLexer + sphinx.add_lexer("yoscrypt", YoscryptLexer) \ No newline at end of file diff --git a/docs/source/index.rst b/docs/source/index.rst new file mode 100644 index 000000000..fb8643072 --- /dev/null +++ b/docs/source/index.rst @@ -0,0 +1,72 @@ +:Abstract: + Most of today's digital design is done in HDL code (mostly Verilog or + VHDL) and with the help of HDL synthesis tools. + + In special cases such as synthesis for coarse-grain cell libraries or + when testing new synthesis algorithms it might be necessary to write a + custom HDL synthesis tool or add new features to an existing one. In + these cases the availability of a Free and Open Source (FOSS) synthesis + tool that can be used as basis for custom tools would be helpful. + + In the absence of such a tool, the Yosys Open SYnthesis Suite (Yosys) + was developed. This document covers the design and implementation of + this tool. At the moment the main focus of Yosys lies on the high-level + aspects of digital synthesis. The pre-existing FOSS logic-synthesis tool + ABC is used by Yosys to perform advanced gate-level optimizations. + + An evaluation of Yosys based on real-world designs is included. It is + shown that Yosys can be used as-is to synthesize such designs. The + results produced by Yosys in this tests where successfully verified + using formal verification and are comparable in quality to the results + produced by a commercial synthesis tool. + + This document was originally published as bachelor thesis at the Vienna + University of Technology :cite:p:`BACC`. + +================================================================================ +Yosys manual +================================================================================ + +.. toctree:: + :maxdepth: 2 + :caption: Manual + :numbered: + + CHAPTER_Intro + CHAPTER_Basics.rst + CHAPTER_Approach.rst + CHAPTER_Overview.rst + CHAPTER_CellLib.rst + CHAPTER_Prog.rst + + CHAPTER_Verilog.rst + CHAPTER_Optimize.rst + CHAPTER_Techmap.rst + CHAPTER_Eval.rst + +.. raw:: latex + + \appendix + +.. toctree:: + :maxdepth: 2 + :includehidden: + :caption: Appendix + + appendix/CHAPTER_Auxlibs.rst + appendix/CHAPTER_Auxprogs.rst + + appendix/CHAPTER_TextRtlil.rst + appendix/APPNOTE_010_Verilog_to_BLIF.rst + appendix/APPNOTE_011_Design_Investigation.rst + appendix/APPNOTE_012_Verilog_to_BTOR.rst + appendix/CHAPTER_StateOfTheArt.rst + + bib + +.. toctree:: + :maxdepth: 1 + :includehidden: + + cmd_ref + diff --git a/docs/source/literature.bib b/docs/source/literature.bib new file mode 100644 index 000000000..143e3aa36 --- /dev/null +++ b/docs/source/literature.bib @@ -0,0 +1,202 @@ + +@inproceedings{intersynth, + title={Example-driven interconnect synthesis for heterogeneous coarse-grain reconfigurable logic}, + author={C. Wolf and Johann Glaser and Florian Schupfer and Jan Haase and Christoph Grimm}, + booktitle={FDL Proceeding of the 2012 Forum on Specification and Design Languages}, + pages={194--201}, + year={2012} +} + +@incollection{intersynthFdlBookChapter, + title={Methodology and Example-Driven Interconnect Synthesis for Designing Heterogeneous Coarse-Grain Reconfigurable Architectures}, + author={Johann Glaser and C. Wolf}, + booktitle={Advances in Models, Methods, and Tools for Complex Chip Design --- Selected contributions from FDL'12}, + editor={Jan Haase}, + publisher={Springer}, + year={2013}, + note={to appear} +} + +@unpublished{BACC, + author = {C. Wolf}, + title = {Design and Implementation of the Yosys Open SYnthesis Suite}, + note = {Bachelor Thesis, Vienna University of Technology}, + year = {2013} +} + +@unpublished{VerilogFossEval, + author = {C. Wolf}, + title = {Evaluation of Open Source Verilog Synthesis Tools for Feature-Completeness and Extensibility}, + note = {Unpublished Student Research Paper, Vienna University of Technology}, + year = {2012} +} + +@article{ABEL, + title={A High-Level Design Language for Programmable Logic Devices}, + author={Kyu Y. Lee and Michael Holley and Mary Bailey and Walter Bright}, + journal={VLSI Design (Manhasset NY: CPM Publications)}, + year={June 1985}, + pages={50-62} +} + +@MISC{Cheng93vl2mv:a, + author = {S-T Cheng and G York and R K Brayton}, + title = {VL2MV: A Compiler from Verilog to BLIF-MV}, + year = {1993} +} + +@MISC{Odin, + author = {Peter Jamieson and Jonathan Rose}, + title = {A VERILOG RTL SYNTHESIS TOOL FOR HETEROGENEOUS FPGAS}, + year = {2005} +} + +@inproceedings{vtr2012, + title={The VTR Project: Architecture and CAD for FPGAs from Verilog to Routing}, + author={Jonathan Rose and Jason Luu and Chi Wai Yu and Opal Densmore and Jeff Goeders and Andrew Somerville and Kenneth B. Kent and Peter Jamieson and Jason Anderson}, + booktitle={Proceedings of the 20th ACM/SIGDA International Symposium on Field-Programmable Gate Arrays}, + pages={77--86}, + year={2012}, + organization={ACM} +} + +@MISC{LogicSynthesis, + author = {G D Hachtel and F Somenzi}, + title = {Logic Synthesis and Verification Algorithms}, + year = {1996} +} + +@ARTICLE{Verilog2005, + journal={IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001)}, + title={IEEE Standard for Verilog Hardware Description Language}, + author={IEEE Standards Association and others}, + year={2006}, + doi={10.1109/IEEESTD.2006.99495} +} + +@ARTICLE{VerilogSynth, + journal={IEEE Std 1364.1-2002}, + title={IEEE Standard for Verilog Register Transfer Level Synthesis}, + author={IEEE Standards Association and others}, + year={2002}, + doi={10.1109/IEEESTD.2002.94220} +} + +@ARTICLE{VHDL, + journal={IEEE Std 1076-2008 (Revision of IEEE Std 1076-2002)}, + title={IEEE Standard VHDL Language Reference Manual}, + author={IEEE Standards Association and others}, + year={2009}, + month={26}, + doi={10.1109/IEEESTD.2009.4772740} +} + +@ARTICLE{VHDLSynth, + journal={IEEE Std 1076.6-2004 (Revision of IEEE Std 1076.6-1999)}, + title={IEEE Standard for VHDL Register Transfer Level (RTL) Synthesis}, + author={IEEE Standards Association and others}, + year={2004}, + doi={10.1109/IEEESTD.2004.94802} +} + +@ARTICLE{IP-XACT, + journal={IEEE Std 1685-2009}, + title={IEEE Standard for IP-XACT, Standard Structure for Packaging, Integrating, and Reusing IP within Tools Flows}, + author={IEEE Standards Association and others}, + year={2010}, + pages={C1-360}, + keywords={abstraction definitions, address space specification, bus definitions, design environment, EDA, electronic design automation, electronic system level, ESL, implementation constraints, IP-XACT, register transfer level, RTL, SCRs, semantic consistency rules, TGI, tight generator interface, tool and data interoperability, use models, XML design meta-data, XML schema}, + doi={10.1109/IEEESTD.2010.5417309} +} + +@book{Dragonbook, + author = {Aho, Alfred V. and Sethi, Ravi and Ullman, Jeffrey D.}, + title = {Compilers: principles, techniques, and tools}, + year = {1986}, + isbn = {0-201-10088-6}, + publisher = {Addison-Wesley Longman Publishing Co., Inc.}, + address = {Boston, MA, USA} +} + +@INPROCEEDINGS{Cummings00, + author = {Clifford E. Cummings and Sunburst Design Inc}, + title = {Nonblocking Assignments in Verilog Synthesis, Coding Styles That Kill}, + booktitle = {SNUG (Synopsys Users Group) 2000 User Papers, section-MC1 (1 st paper}, + year = {2000} +} + +@ARTICLE{MURPHY, + author={D. L. Klipstein}, + journal={Cahners Publishing Co., EEE Magazine, Vol. 15, No. 8}, + title={The Contributions of Edsel Murphy to the Understanding of the Behavior of Inanimate Objects}, + year={August 1967} +} + +@INPROCEEDINGS{fsmextract, + author={Yiqiong Shi and Chan Wai Ting and Bah-Hwee Gwee and Ye Ren}, + booktitle={Circuits and Systems (ISCAS), Proceedings of 2010 IEEE International Symposium on}, + title={A highly efficient method for extracting FSMs from flattened gate-level netlist}, + year={2010}, + pages={2610-2613}, + keywords={circuit CAD;finite state machines;microcontrollers;FSM;control-intensive circuits;finite state machines;flattened gate-level netlist;state register elimination technique;Automata;Circuit synthesis;Continuous wavelet transforms;Design automation;Digital circuits;Hardware design languages;Logic;Microcontrollers;Registers;Signal processing}, + doi={10.1109/ISCAS.2010.5537093}, +} + +@ARTICLE{MultiLevelLogicSynth, + author={Brayton, R.K. and Hachtel, G.D. and Sangiovanni-Vincentelli, A.L.}, + journal={Proceedings of the IEEE}, + title={Multilevel logic synthesis}, + year={1990}, + volume={78}, + number={2}, + pages={264-300}, + keywords={circuit layout CAD;integrated logic circuits;logic CAD;capsule summaries;definitions;detailed analysis;in-depth background;logic decomposition;logic minimisation;logic synthesis;logic synthesis techniques;multilevel combinational logic;multilevel logic synthesis;notation;perspective;survey;synthesis methods;technology mapping;testing;Application specific integrated circuits;Design automation;Integrated circuit synthesis;Logic design;Logic devices;Logic testing;Network synthesis;Programmable logic arrays;Signal synthesis;Silicon}, + doi={10.1109/5.52213}, + ISSN={0018-9219}, +} + +@article{UllmannSubgraphIsomorphism, + author = {Ullmann, J. R.}, + title = {An Algorithm for Subgraph Isomorphism}, + journal = {J. ACM}, + issue_date = {Jan. 1976}, + volume = {23}, + number = {1}, + month = jan, + year = {1976}, + issn = {0004-5411}, + pages = {31--42}, + numpages = {12}, + doi = {10.1145/321921.321925}, + acmid = {321925}, + publisher = {ACM}, + address = {New York, NY, USA}, +} + +@article{een2003temporal, + title={Temporal induction by incremental SAT solving}, + author={E{\'e}n, Niklas and S{\"o}rensson, Niklas}, + journal={Electronic Notes in Theoretical Computer Science}, + volume={89}, + number={4}, + pages={543--560}, + year={2003}, + publisher={Elsevier} +} + +@inproceedings{btor, + title={BTOR: bit-precise modelling of word-level problems for model checking}, + author={Brummayer, Robert and Biere, Armin and Lonsing, Florian}, + booktitle={Proceedings of the joint workshops of the 6th international workshop on satisfiability modulo theories and 1st international workshop on bit-precise reasoning}, + pages={33--38}, + year={2008} +} + +@inproceedings{VIS, + title={VIS: A system for verification and synthesis}, + author={Brayton, Robert K and Hachtel, Gary D and Sangiovanni-Vincentelli, Alberto and Somenzi, Fabio and Aziz, Adnan and Cheng, Szu-Tsung and Edwards, Stephen and Khatri, Sunil and Kukimoto, Yuji and Pardo, Abelardo and others}, + booktitle={Proceedings of the 8th International Conference on Computer Aided Verification}, + pages={428--432}, + year={1996}, + organization={Springer} +} diff --git a/docs/source/requirements.txt b/docs/source/requirements.txt new file mode 100644 index 000000000..d357a83b7 --- /dev/null +++ b/docs/source/requirements.txt @@ -0,0 +1,2 @@ +sphinx-press-theme +sphinxcontrib-bibtex diff --git a/docs/static/custom.css b/docs/static/custom.css new file mode 100644 index 000000000..40a8c178f --- /dev/null +++ b/docs/static/custom.css @@ -0,0 +1 @@ +/* empty */ diff --git a/docs/static/favico.png b/docs/static/favico.png new file mode 100644 index 000000000..3f5afba76 Binary files /dev/null and b/docs/static/favico.png differ diff --git a/docs/static/logo.png b/docs/static/logo.png new file mode 100644 index 000000000..8e5a507c6 Binary files /dev/null and b/docs/static/logo.png differ diff --git a/docs/static/yosyshq.css b/docs/static/yosyshq.css new file mode 100644 index 000000000..0be7f7728 --- /dev/null +++ b/docs/static/yosyshq.css @@ -0,0 +1,78 @@ +h1, h3, p.topic-title, .content li.toctree-l1 > a { + color: #d6368f !important; +} + +h2, p.admonition-title, dt, .content li.toctree-l2 > a { + color: #4b72b8; +} + +a { + color: #8857a3; +} + +a.current, a:hover, a.external { + color: #d6368f !important; +} + +a.external:hover { + text-decoration: underline; +} + +p { + text-align: justify; +} + +.vp-sidebar a { + color: #d6368f; +} + +.vp-sidebar li li a { + color: #4b72b8; +} + +.vp-sidebar li li li a { + color: #2c3e50; + font-weight: 400; +} + +.vp-sidebar h3 { + padding-left: 1.5rem !important; +} + +.vp-sidebar ul a { + padding-left: 1.5rem !important; +} + +.vp-sidebar ul ul a { + padding-left: 3rem !important; +} + +.vp-sidebar ul ul ul a { + padding-left: 4.5rem !important; +} + +.vp-sidebar .toctree-l1.current a { + border-left: 0.5rem solid #6ecbd7; +} + +.vp-sidebar .toctree-l1 a.current { + border-left: 0.5rem solid #8857a3; +} + +.injected .rst-current-version, .injected dt { + color: #6ecbd7 !important; +} + +.cmdref .highlight-yoscrypt .highlight pre { + padding: 0%; + margin: 0%; +} + +.cmdref .highlight-none .highlight pre { + padding-top: 0%; + margin-top: 0%; +} + +.width-helper { + max-width: 100%; +} diff --git a/docs/util/RtlilLexer.py b/docs/util/RtlilLexer.py new file mode 100644 index 000000000..75aa53ec8 --- /dev/null +++ b/docs/util/RtlilLexer.py @@ -0,0 +1,45 @@ +from pygments.lexer import RegexLexer, bygroups, include +from pygments.token import Comment, Keyword, Name, Number, String, Whitespace + +__all__ = ['RtlilLexer'] + +class RtlilLexer(RegexLexer): + name = 'RTLIL' + aliases = ['rtlil'] + filenames = ['*.il'] + + keyword_re = r'(always|assign|attribute|autoidx|case|cell|connect|edge|end|global|high|init|inout|input|low|memory|module|negedge|offset|output|parameter|posedge|process|real|signed|size|switch|sync|update|upto|width|wire)' + + tokens = { + 'common': [ + (r'\s+', Whitespace), + (r'#.*', Comment.Single), + (keyword_re, Keyword), + (r'([\\\$][^ \t\r\n]+|\.[0-9]+)', Name.Variable), + (r"[0-9]+'[01xzm-]*", Number), + (r'-?[0-9]+', Number.Integer), + (r'"', String, 'string'), + ], + 'root': [ + (r'cell', Keyword, 'cell_definition'), + (r'(module|wire|memory|process)', Keyword, 'definition'), + include('common'), + ], + 'definition': [ + (r'([\\\$][^ \t\r\n]+|\.[0-9]+)', Name.Entity, '#pop'), + include('common') + ], + 'cell_definition': [ + (r'(\$[^ \t\r\n]+)\b', Name.Function), + (r'(\\[^ \t\r\n]+|\.[0-9]+)', Name.Variable), + (r'$', Whitespace, '#pop'), + include('common'), + ], + 'string': [ + (r'"', String, '#pop'), + (r'\\([\\abfnrtv"\']|x[a-fA-F0-9]{2,4}|[0-7]{1,3})', String.Escape), + (r'[^\\"\n]+', String), # all other characters + (r'(\\)(\n)', bygroups(String.Escape, Whitespace)), # line continuation + (r'\\', String), # stray backslash + ] + } diff --git a/docs/util/YoscryptLexer.py b/docs/util/YoscryptLexer.py new file mode 100644 index 000000000..8cb31c81a --- /dev/null +++ b/docs/util/YoscryptLexer.py @@ -0,0 +1,73 @@ +from pygments.lexer import RegexLexer, bygroups, include +from pygments.token import (Comment, Error, Keyword, Name, Number, Operator, + String, Whitespace) + +__all__ = ['YoscryptLexer'] + +class YoscryptLexer(RegexLexer): + name = 'Yosys Script' + aliases = ['yoscrypt'] + filenames = ['*.ys'] + + + + tokens = { + 'common': [ + (r'\s+', Whitespace), + (r'#.*', Comment.Single), + (r'"', String, 'string'), + (r'(\d+)(\')([bdho]? ?\w+)', bygroups(Number, Operator, Number)), + (r'(\d+\.\d+)', Number.Float), + (r'(\d+)', Number), + (r'(\$[A-Za-z_0-9]*)', Name.Builtin), + (r'([A-Za-z_][A-Za-z_0-9\.\\/:-]*)', Name), + (r'(\[)(-\S*)(\])', # optional command + bygroups(Operator, Name.Attribute, Operator)), + (r'([\[<]\w*[\]>])', Name), # arguments + (r'[\{\}\|=\[\],]', Operator), + (r'.', Comment), + ], + 'root': [ + (r'([A-Za-z_][A-Za-z_0-9]*)', Keyword, 'command'), + (r'(-[A-Za-z_][A-Za-z_0-9]*)', Name.Attribute, 'command'), # shortcut for options + include('common'), + ], + 'command': [ + (r'(-[A-Za-z_][A-Za-z_0-9]*)', Name.Attribute), + (r'\+/[^\s]+', Name.Class), + (r'$', Whitespace, '#pop'), + (r';(?=\s)', Operator, '#pop'), + (r';{2,3}(?=\s)', Name.Class, '#pop'), + (r';{1,3}', Error, '#pop'), + (r'([ANwismctparn]:)', Keyword.Type, 'pattern'), + (r'@', Keyword.Type), + (r'%(x|ci|co)e?', Keyword.Type, 'expansion'), + (r'%[%nuidDcasmMCR]?', Keyword.Type), + (r'/', Operator), + include('common'), + ], + 'pattern': [ + (r'<<', Name), # Not an operator + (r'(=|<|<=|>|>=)', Operator), + (r':', Keyword.Type), + (r'$', Whitespace, '#pop:2'), + (r'\s+', Whitespace, '#pop'), + include('common'), + ], + 'expansion': [ + (r'$', Name.Class, '#pop:2'), + (r';(?=\s)', Operator, '#pop:2'), + (r';{2,3}(?=\s)', Name.Class, '#pop:2'), + (r'\s', Whitespace, '#pop'), + (r'[0-9\*]{1,3}', Number), + (r'[:+-,\[\]]', Operator), + include('common'), + ], + 'string': [ + (r'"', String, '#pop'), + (r'\\([\\abfnrtv"\']|x[a-fA-F0-9]{2,4}|[0-7]{1,3})', String.Escape), + (r'[^\\"\n]+', String), # all other characters + (r'(\\)(\n)', bygroups(String.Escape, Whitespace)), # line continuation + (r'\\', String), # stray backslash + ] + } -- cgit v1.2.3