riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #3907 from YosysHQ/krys/docs 

Manual rewrite and presentation merge
This commit is contained in:
N. Engelhardt 2024-03-18 17:12:57 +01:00 committed by GitHub
parent 3231c1cd93 49f1bea1d2
commit 3f54bf102c
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
261 changed files with 9085 additions and 8997 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
.github/workflows/test-docs.yml vendored Normal file
View File

@ -0,0 +1,42 @@
name: Build and test doc code samples
on:
pull_request:
branches:
- master
jobs:
test-docs:
runs-on: ubuntu-latest
steps:
- name: Install Dependencies
shell: bash
run: |
sudo apt-get update
sudo apt-get install gperf build-essential bison flex libreadline-dev gawk tcl-dev libffi-dev git graphviz xdot pkg-config python3 libboost-system-dev libboost-python-dev libboost-filesystem-dev zlib1g-dev
- name: Setup GCC
uses: Dup4/actions-setup-gcc@v1
- name: Runtime environment
shell: bash
env:
WORKSPACE: ${{ github.workspace }}
run: |
echo "GITHUB_WORKSPACE=`pwd`" >> $GITHUB_ENV
echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH
echo "procs=$(nproc)" >> $GITHUB_ENV
- name: Checkout Yosys
uses: actions/checkout@v3
- name: Build yosys
shell: bash
run: |
make config-gcc
make -j${{ env.procs }}
- name: Run tests
shell: bash
run: |
make -C docs test -j${{ env.procs }}

7
.github/workflows/test-linux.yml vendored
View File

@ -112,6 +112,13 @@ jobs:
make config-${CC%%-*} make config-${CC%%-*}
make -j${{ env.procs }} CXXSTD=${{ matrix.cpp_std }} CC=$CC CXX=$CC LD=$CC make -j${{ env.procs }} CXXSTD=${{ matrix.cpp_std }} CC=$CC CXX=$CC LD=$CC
- name: Store build artifact
if: (matrix.cpp_std == 'c++11') && (matrix.compiler == 'gcc-11')
uses: actions/upload-artifact@v4
with:
name: compiled-yosys
path: yosys
- name: Run tests - name: Run tests
if: (matrix.cpp_std == 'c++11') && (matrix.compiler == 'gcc-11') if: (matrix.cpp_std == 'c++11') && (matrix.compiler == 'gcc-11')
shell: bash shell: bash

1
CODEOWNERS
View File

@ -18,6 +18,7 @@ passes/techmap/flowmap.cc @whitequark
passes/opt/opt_lut.cc @whitequark passes/opt/opt_lut.cc @whitequark
passes/techmap/abc9*.cc @eddiehung @Ravenslofty passes/techmap/abc9*.cc @eddiehung @Ravenslofty
backends/aiger/xaiger.cc @eddiehung backends/aiger/xaiger.cc @eddiehung
docs/ @KrystalDelusion
## External Contributors ## External Contributors

18
Makefile
View File

@ -971,17 +971,27 @@ docs/source/cmd/abc.rst: $(TARGETS) $(EXTRA_TARGETS)
mkdir -p docs/source/cmd mkdir -p docs/source/cmd
./$(PROGRAM_PREFIX)yosys -p 'help -write-rst-command-reference-manual' ./$(PROGRAM_PREFIX)yosys -p 'help -write-rst-command-reference-manual'
PHONY: docs/gen_images docs/guidelines PHONY: docs/gen_examples docs/gen_images docs/guidelines docs/usage
docs/gen_examples:
$(Q) $(MAKE) -C docs examples
docs/gen_images: docs/gen_images:
$(Q) $(MAKE) -C docs/images all $(Q) $(MAKE) -C docs images
DOCS_GUIDELINE_FILES := GettingStarted CodingStyle DOCS_GUIDELINE_FILES := GettingStarted CodingStyle
docs/guidelines: docs/guidelines:
$(Q) mkdir -p docs/source/temp $(Q) mkdir -p docs/source/temp
$(Q) cp -f $(addprefix guidelines/,$(DOCS_GUIDELINE_FILES)) docs/source/temp $(Q) cp -f $(addprefix guidelines/,$(DOCS_GUIDELINE_FILES)) docs/source/temp
# many of these will return an error which can be safely ignored, so we prefix
# the command with a '-'
DOCS_USAGE_PROGS := yosys yosys-config yosys-filterlib yosys-abc yosys-smtbmc yosys-witness
docs/usage: $(addprefix docs/source/temp/,$(DOCS_USAGE_PROGS))
docs/source/temp/%: docs/guidelines
-$(Q) ./$(PROGRAM_PREFIX)$* --help > $@ 2>&1
DOC_TARGET ?= html DOC_TARGET ?= html
docs: docs/source/cmd/abc.rst docs/gen_images docs/guidelines docs: docs/source/cmd/abc.rst docs/gen_examples docs/gen_images docs/guidelines docs/usage
$(Q) $(MAKE) -C docs $(DOC_TARGET) $(Q) $(MAKE) -C docs $(DOC_TARGET)
clean: clean:
@ -1000,8 +1010,6 @@ clean:
rm -f tests/svinterfaces/*.log_stdout tests/svinterfaces/*.log_stderr tests/svinterfaces/dut_result.txt tests/svinterfaces/reference_result.txt tests/svinterfaces/a.out tests/svinterfaces/*_syn.v tests/svinterfaces/*.diff rm -f tests/svinterfaces/*.log_stdout tests/svinterfaces/*.log_stderr tests/svinterfaces/dut_result.txt tests/svinterfaces/reference_result.txt tests/svinterfaces/a.out tests/svinterfaces/*_syn.v tests/svinterfaces/*.diff
rm -f tests/tools/cmp_tbdata rm -f tests/tools/cmp_tbdata
$(MAKE) -C docs clean $(MAKE) -C docs clean
$(MAKE) -C docs/images clean
rm -rf docs/source/cmd docs/util/__pycache__
clean-abc: clean-abc:
$(MAKE) -C abc DEP= clean $(MAKE) -C abc DEP= clean

6
README.md
View File

@ -610,10 +610,12 @@ Simply visit https://yosys.readthedocs.io/en/latest/ instead.
In addition to those packages listed above for building Yosys from source, the In addition to those packages listed above for building Yosys from source, the
following are used for building the website: following are used for building the website:
$ sudo apt-get install pdf2svg faketime $ sudo apt install pdf2svg faketime
PDFLaTeX, included with most LaTeX distributions, is also needed during the PDFLaTeX, included with most LaTeX distributions, is also needed during the
build process for the website. build process for the website. Or, run the following:
$ sudo apt install texlive-latex-base texlive-latex-extra latexmk
The Python package, Sphinx, is needed along with those listed in The Python package, Sphinx, is needed along with those listed in
`docs/source/requirements.txt`: `docs/source/requirements.txt`:

14
docs/.gitignore vendored
View File

@ -1,11 +1,9 @@
/build/ /build/
/source/cmd /source/cmd
/source/temp /source/temp
/images/*.log /source/_images/**/*.log
/images/*.aux /source/_images/**/*.aux
/images/*.pdf /source/_images/**/*.pdf
/images/*.svg /source/_images/**/*.svg
/images/011/*.log /source/_images/**/*.dot
/images/011/*.aux /source/_images/code_examples
/images/011/*.pdf
/images/011/*.svg

28
docs/Makefile
View File

@ -45,8 +45,10 @@ help:
@echo " dummy to check syntax errors of document sources" @echo " dummy to check syntax errors of document sources"
.PHONY: clean .PHONY: clean
clean: clean: clean-examples
rm -rf $(BUILDDIR)/* rm -rf $(BUILDDIR)/*
rm -rf source/cmd util/__pycache__
$(MAKE) -C source/_images clean
.PHONY: html .PHONY: html
html: html:
@ -224,3 +226,27 @@ dummy:
$(SPHINXBUILD) -b dummy $(ALLSPHINXOPTS) $(BUILDDIR)/dummy $(SPHINXBUILD) -b dummy $(ALLSPHINXOPTS) $(BUILDDIR)/dummy
@echo @echo
@echo "Build finished. Dummy builder generates no files." @echo "Build finished. Dummy builder generates no files."
PYTHON ?= python3
.PHONY: test test-examples test-macros examples
test: test-examples test-macros
FORCE:
Makefile-%: FORCE
$(MAKE) -C $(@D) $(*F)
CODE_EXAMPLES := $(wildcard source/code_examples/*/Makefile)
TEST_EXAMPLES := $(addsuffix -all,$(CODE_EXAMPLES))
CLEAN_EXAMPLES := $(addsuffix -clean,$(CODE_EXAMPLES))
test-examples: $(TEST_EXAMPLES)
clean-examples: $(CLEAN_EXAMPLES)
examples: $(TEST_EXAMPLES)
test-macros:
$(PYTHON) tests/macro_commands.py
.PHONY: images
images:
$(MAKE) -C source/_images

18
docs/images/011/example_out.tex
View File

@ -1,18 +0,0 @@
\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}

19
docs/images/011/select_prod.tex
View File

@ -1,19 +0,0 @@
\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}

15
docs/images/011/splitnets_libfile.tex
View File

@ -1,15 +0,0 @@
\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}

27
docs/images/011/submod_dots.tex
View File

@ -1,27 +0,0 @@
\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}

44
docs/images/Makefile
View File

@ -1,44 +0,0 @@
all: dots tex svg tidy
TEX_SOURCE:= $(wildcard *.tex)
DOT_LOC:= ../source/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
faketime -f '2022-01-01 00:00:00 x0,001' dot -Tpdf -o $@ $<
011/%.pdf: 011/%.tex
cd 011 && faketime -f '2022-01-01 00:00:00 x0,001' pdflatex $(<F) --interaction=nonstopmode
%.pdf: %.tex
pdflatex $< --interaction=nonstopmode
%.svg: %.pdf
pdf2svg $< $@
.PHONY: clean tidy
tidy:
rm -f *.log
rm -f *.aux
rm -f 011/*.log 011/*.aux
clean: tidy
rm -f *.pdf
rm -f *.svg
rm -f 011/*.pdf 011/*.svg

BIN
docs/images/approach_flow.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 9.5 KiB

BIN
docs/images/basics_abstractions.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 28 KiB

BIN
docs/images/basics_ast.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 9.3 KiB

BIN
docs/images/basics_flow.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 12 KiB

BIN
docs/images/basics_parsetree.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 23 KiB

BIN
docs/images/overview_flow.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 17 KiB

BIN
docs/images/overview_rtlil.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 16 KiB

BIN
docs/images/verilog_flow.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 16 KiB

34
docs/source/APPNOTE_011_Design_Investigation/cmos_00.dot
View File

@ -1,34 +0,0 @@
digraph "cmos_demo" {
rankdir="LR";
remincross=true;
n4 [ shape=octagon, label="a", color="black", fontcolor="black" ];
n5 [ shape=octagon, label="b", color="black", fontcolor="black" ];
n6 [ shape=octagon, label="y", color="black", fontcolor="black" ];
c10 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g0\nNOR|{}}" ];
c11 [ shape=record, label="{{<p7> A|<p9> Y}|$g1\nNOT|{}}" ];
c12 [ shape=record, label="{{<p7> A|<p9> Y}|$g2\nNOT|{}}" ];
c13 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g3\nNOR|{}}" ];
x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
x0:e -> c13:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
c14 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g4\nNOR|{}}" ];
x1 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
x1:e -> c14:p8:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
x2:e -> c14:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
n1 [ shape=diamond, label="$n4" ];
n1:e -> c10:p9:w [color="black", label=""];
n1:e -> c14:p7:w [color="black", label=""];
n2 [ shape=diamond, label="$n5" ];
n2:e -> c11:p9:w [color="black", label=""];
n2:e -> c13:p7:w [color="black", label=""];
n3 [ shape=diamond, label="$n6_1" ];
n3:e -> c12:p9:w [color="black", label=""];
n3:e -> c13:p8:w [color="black", label=""];
n4:e -> c10:p8:w [color="black", label=""];
n4:e -> c12:p7:w [color="black", label=""];
n5:e -> c10:p7:w [color="black", label=""];
n5:e -> c11:p7:w [color="black", label=""];
n6:e -> x0:s0:w [color="black", label=""];
n6:e -> x1:s0:w [color="black", label=""];
n6:e -> x2:s0:w [color="black", label=""];
}

23
docs/source/APPNOTE_011_Design_Investigation/cmos_01.dot
View File

@ -1,23 +0,0 @@
digraph "cmos_demo" {
rankdir="LR";
remincross=true;
n4 [ shape=octagon, label="a", color="black", fontcolor="black" ];
n5 [ shape=octagon, label="b", color="black", fontcolor="black" ];
n6 [ shape=octagon, label="y[0]", color="black", fontcolor="black" ];
n7 [ shape=octagon, label="y[1]", color="black", fontcolor="black" ];
c11 [ shape=record, label="{{<p8> A|<p9> B}|$g0\nNOR|{<p10> Y}}" ];
c12 [ shape=record, label="{{<p8> A}|$g1\nNOT|{<p10> Y}}" ];
c13 [ shape=record, label="{{<p8> A}|$g2\nNOT|{<p10> Y}}" ];
c14 [ shape=record, label="{{<p8> A|<p9> B}|$g3\nNOR|{<p10> Y}}" ];
c15 [ shape=record, label="{{<p8> A|<p9> B}|$g4\nNOR|{<p10> Y}}" ];
c11:p10:e -> c15:p8:w [color="black", label=""];
c12:p10:e -> c14:p8:w [color="black", label=""];
c13:p10:e -> c14:p9:w [color="black", label=""];
n4:e -> c11:p9:w [color="black", label=""];
n4:e -> c13:p8:w [color="black", label=""];
n5:e -> c11:p8:w [color="black", label=""];
n5:e -> c12:p8:w [color="black", label=""];
c15:p10:e -> n6:w [color="black", label=""];
c14:p10:e -> n7:w [color="black", label=""];
n7:e -> c15:p9:w [color="black", label=""];
}

11
docs/source/APPNOTE_011_Design_Investigation/example.ys
View File

@ -1,11 +0,0 @@
read_verilog example.v
show -format dot -prefix example_00
proc
show -format dot -prefix example_01
opt
show -format dot -prefix example_02
cd example
select t:$add
show -format dot -prefix example_03

23
docs/source/APPNOTE_011_Design_Investigation/example_00.dot
View File

@ -1,23 +0,0 @@
digraph "example" {
rankdir="LR";
remincross=true;
n4 [ shape=octagon, label="a", color="black", fontcolor="black" ];
n5 [ shape=octagon, label="b", color="black", fontcolor="black" ];
n6 [ shape=octagon, label="c", color="black", fontcolor="black" ];
n7 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
n8 [ shape=octagon, label="y", color="black", fontcolor="black" ];
c12 [ shape=record, label="{{<p9> A|<p10> B}|$2\n$add|{<p11> Y}}" ];
v0 [ label="2'00" ];
c14 [ shape=record, label="{{<p9> A|<p10> B|<p13> S}|$3\n$mux|{<p11> Y}}" ];
p1 [shape=box, style=rounded, label="PROC $1\nexample.v:3"];
c12:p11:e -> c14:p10:w [color="black", style="setlinewidth(3)", label=""];
c14:p11:e -> p1:w [color="black", style="setlinewidth(3)", label=""];
n4:e -> c12:p9:w [color="black", label=""];
n5:e -> c12:p10:w [color="black", label=""];
n6:e -> c14:p13:w [color="black", label=""];
n6:e -> p1:w [color="black", label=""];
n7:e -> p1:w [color="black", label=""];
p1:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
n8:e -> p1:w [color="black", style="setlinewidth(3)", label=""];
v0:e -> c14:p9:w [color="black", style="setlinewidth(3)", label=""];
}

33
docs/source/APPNOTE_011_Design_Investigation/example_01.dot
View File

@ -1,33 +0,0 @@
digraph "example" {
rankdir="LR";
remincross=true;
n6 [ shape=octagon, label="a", color="black", fontcolor="black" ];
n7 [ shape=octagon, label="b", color="black", fontcolor="black" ];
n8 [ shape=octagon, label="c", color="black", fontcolor="black" ];
n9 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
n10 [ shape=octagon, label="y", color="black", fontcolor="black" ];
c14 [ shape=record, label="{{<p11> A|<p12> B}|$2\n$add|{<p13> Y}}" ];
c18 [ shape=record, label="{{<p15> CLK|<p16> D}|$7\n$dff|{<p17> Q}}" ];
c20 [ shape=record, label="{{<p11> A|<p12> B|<p19> S}|$5\n$mux|{<p13> Y}}" ];
v0 [ label="2'00" ];
c21 [ shape=record, label="{{<p11> A|<p12> B|<p19> S}|$3\n$mux|{<p13> Y}}" ];
x1 [shape=box, style=rounded, label="BUF"];
x2 [shape=box, style=rounded, label="BUF"];
n1 [ shape=diamond, label="$0\\y[1:0]" ];
x2:e:e -> n1:w [color="black", style="setlinewidth(3)", label=""];
c18:p17:e -> n10:w [color="black", style="setlinewidth(3)", label=""];
n10:e -> c20:p11:w [color="black", style="setlinewidth(3)", label=""];
c14:p13:e -> c21:p12:w [color="black", style="setlinewidth(3)", label=""];
n3 [ shape=point ];
c20:p13:e -> n3:w [color="black", style="setlinewidth(3)", label=""];
n3:e -> c18:p16:w [color="black", style="setlinewidth(3)", label=""];
n3:e -> x2:w:w [color="black", style="setlinewidth(3)", label=""];
x1:e:e -> c20:p19:w [color="black", label=""];
c21:p13:e -> c20:p12:w [color="black", style="setlinewidth(3)", label=""];
n6:e -> c14:p11:w [color="black", label=""];
n7:e -> c14:p12:w [color="black", label=""];
n8:e -> c21:p19:w [color="black", label=""];
n8:e -> x1:w:w [color="black", label=""];
n9:e -> c18:p15:w [color="black", label=""];
v0:e -> c21:p11:w [color="black", style="setlinewidth(3)", label=""];
}

20
docs/source/APPNOTE_011_Design_Investigation/example_02.dot
View File

@ -1,20 +0,0 @@
digraph "example" {
rankdir="LR";
remincross=true;
n3 [ shape=octagon, label="a", color="black", fontcolor="black" ];
n4 [ shape=octagon, label="b", color="black", fontcolor="black" ];
n5 [ shape=octagon, label="c", color="black", fontcolor="black" ];
n6 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
n7 [ shape=octagon, label="y", color="black", fontcolor="black" ];
c11 [ shape=record, label="{{<p8> A|<p9> B}|$2\n$add|{<p10> Y}}" ];
c15 [ shape=record, label="{{<p12> CLK|<p13> D}|$7\n$dff|{<p14> Q}}" ];
c17 [ shape=record, label="{{<p8> A|<p9> B|<p16> S}|$5\n$mux|{<p10> Y}}" ];
c17:p10:e -> c15:p13:w [color="black", style="setlinewidth(3)", label=""];
c11:p10:e -> c17:p9:w [color="black", style="setlinewidth(3)", label=""];
n3:e -> c11:p8:w [color="black", label=""];
n4:e -> c11:p9:w [color="black", label=""];
n5:e -> c17:p16:w [color="black", label=""];
n6:e -> c15:p12:w [color="black", label=""];
c15:p14:e -> n7:w [color="black", style="setlinewidth(3)", label=""];
n7:e -> c17:p8:w [color="black", style="setlinewidth(3)", label=""];
}

11
docs/source/APPNOTE_011_Design_Investigation/example_03.dot
View File

@ -1,11 +0,0 @@
digraph "example" {
rankdir="LR";
remincross=true;
v0 [ label="a" ];
v1 [ label="b" ];
v2 [ label="$2_Y" ];
c4 [ shape=record, label="{{<p1> A|<p2> B}|$2\n$add|{<p3> Y}}" ];
v0:e -> c4:p1:w [color="black", label=""];
v1:e -> c4:p2:w [color="black", label=""];
c4:p3:e -> v2:w [color="black", style="setlinewidth(3)", label=""];
}

23
docs/source/APPNOTE_011_Design_Investigation/make.sh
View File

@ -1,23 +0,0 @@
#!/bin/bash
set -ex
if false; then
rm -f *.dot
../../yosys example.ys
../../yosys -p 'proc; opt; show -format dot -prefix splice' splice.v
../../yosys -p 'techmap; abc -liberty ../../techlibs/cmos/cmos_cells.lib;; show -format dot -prefix cmos_00' cmos.v
../../yosys -p 'techmap; splitnets -ports; abc -liberty ../../techlibs/cmos/cmos_cells.lib;; show -lib ../../techlibs/cmos/cmos_cells.v -format dot -prefix cmos_01' cmos.v
../../yosys -p 'opt; cd sumprod; select a:sumstuff; show -format dot -prefix sumprod_00' sumprod.v
../../yosys -p 'opt; cd sumprod; select a:sumstuff %x; show -format dot -prefix sumprod_01' sumprod.v
../../yosys -p 'opt; cd sumprod; select prod; show -format dot -prefix sumprod_02' sumprod.v
../../yosys -p 'opt; cd sumprod; select prod %ci; show -format dot -prefix sumprod_03' sumprod.v
../../yosys -p 'opt; cd sumprod; select prod %ci2; show -format dot -prefix sumprod_04' sumprod.v
../../yosys -p 'opt; cd sumprod; select prod %ci3; show -format dot -prefix sumprod_05' sumprod.v
../../yosys -p 'proc; opt; memory; opt; cd memdemo; show -format dot -prefix memdemo_00' memdemo.v
../../yosys -p 'proc; opt; memory; opt; cd memdemo; show -format dot -prefix memdemo_01 y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff' memdemo.v
../../yosys submod.ys
sed -i '/^label=/ d;' *.dot
fi
for dot_file in *.dot; do
pdf_file=${dot_file%.dot}.pdf
dot -Tpdf -o $pdf_file $dot_file
done

138
docs/source/APPNOTE_011_Design_Investigation/memdemo_00.dot
View File

@ -1,138 +0,0 @@
digraph "memdemo" {
rankdir="LR";
remincross=true;
n24 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
n25 [ shape=octagon, label="d", color="black", fontcolor="black" ];
n26 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ];
n27 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ];
n28 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ];
n29 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ];
n30 [ shape=diamond, label="s1", color="black", fontcolor="black" ];
n31 [ shape=diamond, label="s2", color="black", fontcolor="black" ];
n32 [ shape=octagon, label="y", color="black", fontcolor="black" ];
c36 [ shape=record, label="{{<p33> A|<p34> B}|$28\n$add|{<p35> Y}}" ];
c37 [ shape=record, label="{{<p33> A|<p34> B}|$31\n$add|{<p35> Y}}" ];
c38 [ shape=record, label="{{<p33> A|<p34> B}|$34\n$add|{<p35> Y}}" ];
c39 [ shape=record, label="{{<p33> A|<p34> B}|$37\n$add|{<p35> Y}}" ];
c41 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$110\n$mux|{<p35> Y}}" ];
x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
x0:e -> c41:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
c42 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$113\n$mux|{<p35> Y}}" ];
x1 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
x1:e -> c42:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
c43 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$116\n$mux|{<p35> Y}}" ];
x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
x2:e -> c43:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
v3 [ label="1'1" ];
c44 [ shape=record, label="{{<p33> A|<p34> B}|$145\n$and|{<p35> Y}}" ];
v4 [ label="1'1" ];
c45 [ shape=record, label="{{<p33> A|<p34> B}|$175\n$and|{<p35> Y}}" ];
v5 [ label="1'1" ];
c46 [ shape=record, label="{{<p33> A|<p34> B}|$205\n$and|{<p35> Y}}" ];
v6 [ label="1'1" ];
c47 [ shape=record, label="{{<p33> A|<p34> B}|$235\n$and|{<p35> Y}}" ];
v7 [ label="2'00" ];
c48 [ shape=record, label="{{<p33> A|<p34> B}|$143\n$eq|{<p35> Y}}" ];
v8 [ label="2'01" ];
c49 [ shape=record, label="{{<p33> A|<p34> B}|$173\n$eq|{<p35> Y}}" ];
v9 [ label="2'10" ];
c50 [ shape=record, label="{{<p33> A|<p34> B}|$203\n$eq|{<p35> Y}}" ];
v10 [ label="2'11" ];
c51 [ shape=record, label="{{<p33> A|<p34> B}|$233\n$eq|{<p35> Y}}" ];
c52 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$147\n$mux|{<p35> Y}}" ];
c53 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$177\n$mux|{<p35> Y}}" ];
c54 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$207\n$mux|{<p35> Y}}" ];
c55 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$237\n$mux|{<p35> Y}}" ];
c59 [ shape=record, label="{{<p56> CLK|<p57> D}|$66\n$dff|{<p58> Q}}" ];
c60 [ shape=record, label="{{<p56> CLK|<p57> D}|$68\n$dff|{<p58> Q}}" ];
c61 [ shape=record, label="{{<p56> CLK|<p57> D}|$70\n$dff|{<p58> Q}}" ];
c62 [ shape=record, label="{{<p56> CLK|<p57> D}|$72\n$dff|{<p58> Q}}" ];
c63 [ shape=record, label="{{<p56> CLK|<p57> D}|$59\n$dff|{<p58> Q}}" ];
c64 [ shape=record, label="{{<p56> CLK|<p57> D}|$63\n$dff|{<p58> Q}}" ];
c65 [ shape=record, label="{{<p56> CLK|<p57> D}|$64\n$dff|{<p58> Q}}" ];
c66 [ shape=record, label="{{<p33> A}|$39\n$reduce_bool|{<p35> Y}}" ];
v11 [ label="4'0000" ];
c67 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$40\n$mux|{<p35> Y}}" ];
x12 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 1:0 " ];
c67:p35:e -> x12:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
c68 [ shape=record, label="{{<p33> A|<p34> B}|$38\n$xor|{<p35> Y}}" ];
x13 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
x13:e -> c68:p33:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
c36:p35:e -> c52:p33:w [color="black", style="setlinewidth(3)", label=""];
c44:p35:e -> c52:p40:w [color="black", label=""];
c45:p35:e -> c53:p40:w [color="black", label=""];
c46:p35:e -> c54:p40:w [color="black", label=""];
c47:p35:e -> c55:p40:w [color="black", label=""];
c48:p35:e -> c44:p33:w [color="black", label=""];
c49:p35:e -> c45:p33:w [color="black", label=""];
c50:p35:e -> c46:p33:w [color="black", label=""];
c51:p35:e -> c47:p33:w [color="black", label=""];
c52:p35:e -> c59:p57:w [color="black", style="setlinewidth(3)", label=""];
c53:p35:e -> c60:p57:w [color="black", style="setlinewidth(3)", label=""];
c37:p35:e -> c53:p33:w [color="black", style="setlinewidth(3)", label=""];
c54:p35:e -> c61:p57:w [color="black", style="setlinewidth(3)", label=""];
c55:p35:e -> c62:p57:w [color="black", style="setlinewidth(3)", label=""];
c66:p35:e -> c67:p40:w [color="black", label=""];
c68:p35:e -> c67:p34:w [color="black", style="setlinewidth(3)", label=""];
n24:e -> c59:p56:w [color="black", label=""];
n24:e -> c60:p56:w [color="black", label=""];
n24:e -> c61:p56:w [color="black", label=""];
n24:e -> c62:p56:w [color="black", label=""];
n24:e -> c63:p56:w [color="black", label=""];
n24:e -> c64:p56:w [color="black", label=""];
n24:e -> c65:p56:w [color="black", label=""];
n25:e -> c52:p34:w [color="black", style="setlinewidth(3)", label=""];
n25:e -> c53:p34:w [color="black", style="setlinewidth(3)", label=""];
n25:e -> c54:p34:w [color="black", style="setlinewidth(3)", label=""];
n25:e -> c55:p34:w [color="black", style="setlinewidth(3)", label=""];
n25:e -> c66:p33:w [color="black", style="setlinewidth(3)", label=""];
n25:e -> c68:p34:w [color="black", style="setlinewidth(3)", label=""];
c59:p58:e -> n26:w [color="black", style="setlinewidth(3)", label=""];
n26:e -> c38:p34:w [color="black", style="setlinewidth(3)", label=""];
n26:e -> c39:p33:w [color="black", style="setlinewidth(3)", label=""];
n26:e -> c42:p33:w [color="black", style="setlinewidth(3)", label=""];
c60:p58:e -> n27:w [color="black", style="setlinewidth(3)", label=""];
n27:e -> c36:p33:w [color="black", style="setlinewidth(3)", label=""];
n27:e -> c39:p34:w [color="black", style="setlinewidth(3)", label=""];
n27:e -> c42:p34:w [color="black", style="setlinewidth(3)", label=""];
c61:p58:e -> n28:w [color="black", style="setlinewidth(3)", label=""];
n28:e -> c36:p34:w [color="black", style="setlinewidth(3)", label=""];
n28:e -> c37:p33:w [color="black", style="setlinewidth(3)", label=""];
n28:e -> c43:p33:w [color="black", style="setlinewidth(3)", label=""];
c62:p58:e -> n29:w [color="black", style="setlinewidth(3)", label=""];
n29:e -> c37:p34:w [color="black", style="setlinewidth(3)", label=""];
n29:e -> c38:p33:w [color="black", style="setlinewidth(3)", label=""];
n29:e -> c43:p34:w [color="black", style="setlinewidth(3)", label=""];
c38:p35:e -> c54:p33:w [color="black", style="setlinewidth(3)", label=""];
c63:p58:e -> n30:w [color="black", style="setlinewidth(3)", label=""];
n30:e -> x13:s1:w [color="black", style="setlinewidth(3)", label=""];
c64:p58:e -> n31:w [color="black", style="setlinewidth(3)", label=""];
n31:e -> x13:s0:w [color="black", style="setlinewidth(3)", label=""];
c65:p58:e -> n32:w [color="black", style="setlinewidth(3)", label=""];
c39:p35:e -> c55:p33:w [color="black", style="setlinewidth(3)", label=""];
n5 [ shape=point ];
x12:s0:e -> n5:w [color="black", style="setlinewidth(3)", label=""];
n5:e -> c48:p34:w [color="black", style="setlinewidth(3)", label=""];
n5:e -> c49:p34:w [color="black", style="setlinewidth(3)", label=""];
n5:e -> c50:p34:w [color="black", style="setlinewidth(3)", label=""];
n5:e -> c51:p34:w [color="black", style="setlinewidth(3)", label=""];
n5:e -> c63:p57:w [color="black", style="setlinewidth(3)", label=""];
n6 [ shape=point ];
x12:s1:e -> n6:w [color="black", style="setlinewidth(3)", label=""];
n6:e -> c64:p57:w [color="black", style="setlinewidth(3)", label=""];
n6:e -> x0:s0:w [color="black", style="setlinewidth(3)", label=""];
n6:e -> x1:s0:w [color="black", style="setlinewidth(3)", label=""];
n6:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""];
c41:p35:e -> c65:p57:w [color="black", style="setlinewidth(3)", label=""];
c42:p35:e -> c41:p33:w [color="black", style="setlinewidth(3)", label=""];
c43:p35:e -> c41:p34:w [color="black", style="setlinewidth(3)", label=""];
v10:e -> c51:p33:w [color="black", style="setlinewidth(3)", label=""];
v11:e -> c67:p33:w [color="black", style="setlinewidth(3)", label=""];
v3:e -> c44:p34:w [color="black", label=""];
v4:e -> c45:p34:w [color="black", label=""];
v5:e -> c46:p34:w [color="black", label=""];
v6:e -> c47:p34:w [color="black", label=""];
v7:e -> c48:p33:w [color="black", style="setlinewidth(3)", label=""];
v8:e -> c49:p33:w [color="black", style="setlinewidth(3)", label=""];
v9:e -> c50:p33:w [color="black", style="setlinewidth(3)", label=""];
}

29
docs/source/APPNOTE_011_Design_Investigation/memdemo_01.dot
View File

@ -1,29 +0,0 @@
digraph "memdemo" {
rankdir="LR";
remincross=true;
n4 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ];
n5 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ];
n6 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ];
n7 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ];
n8 [ shape=octagon, label="y", color="black", fontcolor="black" ];
v0 [ label="$0\\s2[1:0] [1]" ];
c13 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$110\n$mux|{<p12> Y}}" ];
v1 [ label="$0\\s2[1:0] [0]" ];
c14 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$113\n$mux|{<p12> Y}}" ];
v2 [ label="$0\\s2[1:0] [0]" ];
c15 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$116\n$mux|{<p12> Y}}" ];
v3 [ label="clk" ];
c19 [ shape=record, label="{{<p16> CLK|<p17> D}|$64\n$dff|{<p18> Q}}" ];
c13:p12:e -> c19:p17:w [color="black", style="setlinewidth(3)", label=""];
c14:p12:e -> c13:p9:w [color="black", style="setlinewidth(3)", label=""];
c15:p12:e -> c13:p10:w [color="black", style="setlinewidth(3)", label=""];
n4:e -> c14:p9:w [color="black", style="setlinewidth(3)", label=""];
n5:e -> c14:p10:w [color="black", style="setlinewidth(3)", label=""];
n6:e -> c15:p9:w [color="black", style="setlinewidth(3)", label=""];
n7:e -> c15:p10:w [color="black", style="setlinewidth(3)", label=""];
c19:p18:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
v0:e -> c13:p11:w [color="black", label=""];
v1:e -> c14:p11:w [color="black", label=""];
v2:e -> c15:p11:w [color="black", label=""];
v3:e -> c19:p16:w [color="black", label=""];
}

39
docs/source/APPNOTE_011_Design_Investigation/splice.dot
View File

@ -1,39 +0,0 @@
digraph "splice_demo" {
rankdir="LR";
remincross=true;
n1 [ shape=octagon, label="a", color="black", fontcolor="black" ];
n2 [ shape=octagon, label="b", color="black", fontcolor="black" ];
n3 [ shape=octagon, label="c", color="black", fontcolor="black" ];
n4 [ shape=octagon, label="d", color="black", fontcolor="black" ];
n5 [ shape=octagon, label="e", color="black", fontcolor="black" ];
n6 [ shape=octagon, label="f", color="black", fontcolor="black" ];
n7 [ shape=octagon, label="x", color="black", fontcolor="black" ];
n8 [ shape=octagon, label="y", color="black", fontcolor="black" ];
c11 [ shape=record, label="{{<p9> A}|$2\n$neg|{<p10> Y}}" ];
x0 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
x0:e -> c11:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
x1 [ shape=record, style=rounded, label="<s0> 3:0 - 7:4 " ];
c11:p10:e -> x1:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
c12 [ shape=record, label="{{<p9> A}|$1\n$not|{<p10> Y}}" ];
x2 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
x2:e -> c12:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
x3 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 3:2 " ];
c12:p10:e -> x3:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
x4 [ shape=record, style=rounded, label="<s1> 0:0 - 1:1 |<s0> 1:1 - 0:0 " ];
x5 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
x6 [ shape=record, style=rounded, label="<s0> 3:0 - 11:8 " ];
x5:e -> x6:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
n1:e -> x4:s0:w [color="black", style="setlinewidth(3)", label=""];
n1:e -> x4:s1:w [color="black", style="setlinewidth(3)", label=""];
n1:e -> x5:s1:w [color="black", style="setlinewidth(3)", label=""];
n2:e -> x5:s0:w [color="black", style="setlinewidth(3)", label=""];
n3:e -> x0:s1:w [color="black", style="setlinewidth(3)", label=""];
n4:e -> x0:s0:w [color="black", style="setlinewidth(3)", label=""];
n5:e -> x2:s1:w [color="black", style="setlinewidth(3)", label=""];
n6:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""];
x4:e -> n7:w [color="black", style="setlinewidth(3)", label=""];
x1:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
x3:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
x3:s1:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
x6:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
}

45
docs/source/APPNOTE_011_Design_Investigation/submod_00.dot
View File

@ -1,45 +0,0 @@
digraph "memdemo" {
rankdir="LR";
remincross=true;
n5 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
n6 [ shape=octagon, label="d", color="black", fontcolor="black" ];
n7 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ];
n8 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ];
n9 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ];
n10 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ];
n11 [ shape=diamond, label="s1", color="black", fontcolor="black" ];
n12 [ shape=diamond, label="s2", color="black", fontcolor="black" ];
n13 [ shape=octagon, label="y", color="black", fontcolor="black" ];
c17 [ shape=record, label="{{<p14> CLK|<p15> D}|$59\n$dff|{<p16> Q}}" ];
c18 [ shape=record, label="{{<p14> CLK|<p15> D}|$63\n$dff|{<p16> Q}}" ];
c20 [ shape=record, label="{{<p5> clk|<p7> mem[0]|<p8> mem[1]|<p9> mem[2]|<p10> mem[3]|<p19> n1}|outstage\noutstage|{<p13> y}}" ];
c21 [ shape=record, label="{{<p5> clk|<p6> d|<p19> n1}|scramble\nscramble|{<p7> mem[0]|<p8> mem[1]|<p9> mem[2]|<p10> mem[3]}}" ];
c23 [ shape=record, label="{{<p6> d|<p11> s1|<p12> s2}|selstage\nselstage|{<p19> n1|<p22> n2}}" ];
n1 [ shape=point ];
c23:p19:e -> n1:w [color="black", style="setlinewidth(3)", label=""];
n1:e -> c17:p15:w [color="black", style="setlinewidth(3)", label=""];
n1:e -> c21:p19:w [color="black", style="setlinewidth(3)", label=""];
c21:p10:e -> n10:w [color="black", style="setlinewidth(3)", label=""];
n10:e -> c20:p10:w [color="black", style="setlinewidth(3)", label=""];
c17:p16:e -> n11:w [color="black", style="setlinewidth(3)", label=""];
n11:e -> c23:p11:w [color="black", style="setlinewidth(3)", label=""];
c18:p16:e -> n12:w [color="black", style="setlinewidth(3)", label=""];
n12:e -> c23:p12:w [color="black", style="setlinewidth(3)", label=""];
c20:p13:e -> n13:w [color="black", style="setlinewidth(3)", label=""];
n2 [ shape=point ];
c23:p22:e -> n2:w [color="black", style="setlinewidth(3)", label=""];
n2:e -> c18:p15:w [color="black", style="setlinewidth(3)", label=""];
n2:e -> c20:p19:w [color="black", style="setlinewidth(3)", label=""];
n5:e -> c17:p14:w [color="black", label=""];
n5:e -> c18:p14:w [color="black", label=""];
n5:e -> c20:p5:w [color="black", label=""];
n5:e -> c21:p5:w [color="black", label=""];
n6:e -> c21:p6:w [color="black", style="setlinewidth(3)", label=""];
n6:e -> c23:p6:w [color="black", style="setlinewidth(3)", label=""];
c21:p7:e -> n7:w [color="black", style="setlinewidth(3)", label=""];
n7:e -> c20:p7:w [color="black", style="setlinewidth(3)", label=""];
c21:p8:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
n8:e -> c20:p8:w [color="black", style="setlinewidth(3)", label=""];
c21:p9:e -> n9:w [color="black", style="setlinewidth(3)", label=""];
n9:e -> c20:p9:w [color="black", style="setlinewidth(3)", label=""];
}

87
docs/source/APPNOTE_011_Design_Investigation/submod_01.dot
View File

@ -1,87 +0,0 @@
digraph "scramble" {
rankdir="LR";
remincross=true;
n17 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
n18 [ shape=octagon, label="d", color="black", fontcolor="black" ];
n19 [ shape=octagon, label="mem[0]", color="black", fontcolor="black" ];
n20 [ shape=octagon, label="mem[1]", color="black", fontcolor="black" ];
n21 [ shape=octagon, label="mem[2]", color="black", fontcolor="black" ];
n22 [ shape=octagon, label="mem[3]", color="black", fontcolor="black" ];
n23 [ shape=octagon, label="n1", color="black", fontcolor="black" ];
c27 [ shape=record, label="{{<p24> A|<p25> B}|$28\n$add|{<p26> Y}}" ];
c28 [ shape=record, label="{{<p24> A|<p25> B}|$31\n$add|{<p26> Y}}" ];
c29 [ shape=record, label="{{<p24> A|<p25> B}|$34\n$add|{<p26> Y}}" ];
c30 [ shape=record, label="{{<p24> A|<p25> B}|$37\n$add|{<p26> Y}}" ];
v0 [ label="1'1" ];
c31 [ shape=record, label="{{<p24> A|<p25> B}|$145\n$and|{<p26> Y}}" ];
v1 [ label="1'1" ];
c32 [ shape=record, label="{{<p24> A|<p25> B}|$175\n$and|{<p26> Y}}" ];
v2 [ label="1'1" ];
c33 [ shape=record, label="{{<p24> A|<p25> B}|$205\n$and|{<p26> Y}}" ];
v3 [ label="1'1" ];
c34 [ shape=record, label="{{<p24> A|<p25> B}|$235\n$and|{<p26> Y}}" ];
v4 [ label="2'00" ];
c35 [ shape=record, label="{{<p24> A|<p25> B}|$143\n$eq|{<p26> Y}}" ];
v5 [ label="2'01" ];
c36 [ shape=record, label="{{<p24> A|<p25> B}|$173\n$eq|{<p26> Y}}" ];
v6 [ label="2'10" ];
c37 [ shape=record, label="{{<p24> A|<p25> B}|$203\n$eq|{<p26> Y}}" ];
v7 [ label="2'11" ];
c38 [ shape=record, label="{{<p24> A|<p25> B}|$233\n$eq|{<p26> Y}}" ];
c40 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$147\n$mux|{<p26> Y}}" ];
c41 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$177\n$mux|{<p26> Y}}" ];
c42 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$207\n$mux|{<p26> Y}}" ];
c43 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$237\n$mux|{<p26> Y}}" ];
c47 [ shape=record, label="{{<p44> CLK|<p45> D}|$66\n$dff|{<p46> Q}}" ];
c48 [ shape=record, label="{{<p44> CLK|<p45> D}|$68\n$dff|{<p46> Q}}" ];
c49 [ shape=record, label="{{<p44> CLK|<p45> D}|$70\n$dff|{<p46> Q}}" ];
c50 [ shape=record, label="{{<p44> CLK|<p45> D}|$72\n$dff|{<p46> Q}}" ];
c27:p26:e -> c40:p24:w [color="black", style="setlinewidth(3)", label=""];
c36:p26:e -> c32:p24:w [color="black", label=""];
c37:p26:e -> c33:p24:w [color="black", label=""];
c38:p26:e -> c34:p24:w [color="black", label=""];
c40:p26:e -> c47:p45:w [color="black", style="setlinewidth(3)", label=""];
c41:p26:e -> c48:p45:w [color="black", style="setlinewidth(3)", label=""];
c42:p26:e -> c49:p45:w [color="black", style="setlinewidth(3)", label=""];
c43:p26:e -> c50:p45:w [color="black", style="setlinewidth(3)", label=""];
n17:e -> c47:p44:w [color="black", label=""];
n17:e -> c48:p44:w [color="black", label=""];
n17:e -> c49:p44:w [color="black", label=""];
n17:e -> c50:p44:w [color="black", label=""];
n18:e -> c40:p25:w [color="black", style="setlinewidth(3)", label=""];
n18:e -> c41:p25:w [color="black", style="setlinewidth(3)", label=""];
n18:e -> c42:p25:w [color="black", style="setlinewidth(3)", label=""];
n18:e -> c43:p25:w [color="black", style="setlinewidth(3)", label=""];
c47:p46:e -> n19:w [color="black", style="setlinewidth(3)", label=""];
n19:e -> c29:p25:w [color="black", style="setlinewidth(3)", label=""];
n19:e -> c30:p24:w [color="black", style="setlinewidth(3)", label=""];
c28:p26:e -> c41:p24:w [color="black", style="setlinewidth(3)", label=""];
c48:p46:e -> n20:w [color="black", style="setlinewidth(3)", label=""];
n20:e -> c27:p24:w [color="black", style="setlinewidth(3)", label=""];
n20:e -> c30:p25:w [color="black", style="setlinewidth(3)", label=""];
c49:p46:e -> n21:w [color="black", style="setlinewidth(3)", label=""];
n21:e -> c27:p25:w [color="black", style="setlinewidth(3)", label=""];
n21:e -> c28:p24:w [color="black", style="setlinewidth(3)", label=""];
c50:p46:e -> n22:w [color="black", style="setlinewidth(3)", label=""];
n22:e -> c28:p25:w [color="black", style="setlinewidth(3)", label=""];
n22:e -> c29:p24:w [color="black", style="setlinewidth(3)", label=""];
n23:e -> c35:p25:w [color="black", style="setlinewidth(3)", label=""];
n23:e -> c36:p25:w [color="black", style="setlinewidth(3)", label=""];
n23:e -> c37:p25:w [color="black", style="setlinewidth(3)", label=""];
n23:e -> c38:p25:w [color="black", style="setlinewidth(3)", label=""];
c29:p26:e -> c42:p24:w [color="black", style="setlinewidth(3)", label=""];
c30:p26:e -> c43:p24:w [color="black", style="setlinewidth(3)", label=""];
c31:p26:e -> c40:p39:w [color="black", label=""];
c32:p26:e -> c41:p39:w [color="black", label=""];
c33:p26:e -> c42:p39:w [color="black", label=""];
c34:p26:e -> c43:p39:w [color="black", label=""];
c35:p26:e -> c31:p24:w [color="black", label=""];
v0:e -> c31:p25:w [color="black", label=""];
v1:e -> c32:p25:w [color="black", label=""];
v2:e -> c33:p25:w [color="black", label=""];
v3:e -> c34:p25:w [color="black", label=""];
v4:e -> c35:p24:w [color="black", style="setlinewidth(3)", label=""];
v5:e -> c36:p24:w [color="black", style="setlinewidth(3)", label=""];
v6:e -> c37:p24:w [color="black", style="setlinewidth(3)", label=""];
v7:e -> c38:p24:w [color="black", style="setlinewidth(3)", label=""];
}

33
docs/source/APPNOTE_011_Design_Investigation/submod_02.dot
View File

@ -1,33 +0,0 @@
digraph "outstage" {
rankdir="LR";
remincross=true;
n4 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
n5 [ shape=octagon, label="mem[0]", color="black", fontcolor="black" ];
n6 [ shape=octagon, label="mem[1]", color="black", fontcolor="black" ];
n7 [ shape=octagon, label="mem[2]", color="black", fontcolor="black" ];
n8 [ shape=octagon, label="mem[3]", color="black", fontcolor="black" ];
n9 [ shape=octagon, label="n1", color="black", fontcolor="black" ];
n10 [ shape=octagon, label="y", color="black", fontcolor="black" ];
c15 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$110\n$mux|{<p14> Y}}" ];
x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
x0:e -> c15:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
c16 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$113\n$mux|{<p14> Y}}" ];
x1 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
x1:e -> c16:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
c17 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$116\n$mux|{<p14> Y}}" ];
x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
x2:e -> c17:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
c21 [ shape=record, label="{{<p18> CLK|<p19> D}|$64\n$dff|{<p20> Q}}" ];
c15:p14:e -> c21:p19:w [color="black", style="setlinewidth(3)", label=""];
c21:p20:e -> n10:w [color="black", style="setlinewidth(3)", label=""];
c16:p14:e -> c15:p11:w [color="black", style="setlinewidth(3)", label=""];
c17:p14:e -> c15:p12:w [color="black", style="setlinewidth(3)", label=""];
n4:e -> c21:p18:w [color="black", label=""];
n5:e -> c16:p11:w [color="black", style="setlinewidth(3)", label=""];
n6:e -> c16:p12:w [color="black", style="setlinewidth(3)", label=""];
n7:e -> c17:p11:w [color="black", style="setlinewidth(3)", label=""];
n8:e -> c17:p12:w [color="black", style="setlinewidth(3)", label=""];
n9:e -> x0:s0:w [color="black", label=""];
n9:e -> x1:s0:w [color="black", label=""];
n9:e -> x2:s0:w [color="black", label=""];
}

26
docs/source/APPNOTE_011_Design_Investigation/submod_03.dot
View File

@ -1,26 +0,0 @@
digraph "selstage" {
rankdir="LR";
remincross=true;
n3 [ shape=octagon, label="d", color="black", fontcolor="black" ];
n4 [ shape=octagon, label="n1", color="black", fontcolor="black" ];
n5 [ shape=octagon, label="n2", color="black", fontcolor="black" ];
n6 [ shape=octagon, label="s1", color="black", fontcolor="black" ];
n7 [ shape=octagon, label="s2", color="black", fontcolor="black" ];
c10 [ shape=record, label="{{<p8> A}|$39\n$reduce_bool|{<p9> Y}}" ];
v0 [ label="4'0000" ];
c13 [ shape=record, label="{{<p8> A|<p11> B|<p12> S}|$40\n$mux|{<p9> Y}}" ];
x1 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 1:0 " ];
c13:p9:e -> x1:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
c14 [ shape=record, label="{{<p8> A|<p11> B}|$38\n$xor|{<p9> Y}}" ];
x2 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
x2:e -> c14:p8:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
c10:p9:e -> c13:p12:w [color="black", label=""];
c14:p9:e -> c13:p11:w [color="black", style="setlinewidth(3)", label=""];
n3:e -> c10:p8:w [color="black", style="setlinewidth(3)", label=""];
n3:e -> c14:p11:w [color="black", style="setlinewidth(3)", label=""];
x1:s0:e -> n4:w [color="black", style="setlinewidth(3)", label=""];
x1:s1:e -> n5:w [color="black", style="setlinewidth(3)", label=""];
n6:e -> x2:s1:w [color="black", style="setlinewidth(3)", label=""];
n7:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""];
v0:e -> c13:p8:w [color="black", style="setlinewidth(3)", label=""];
}

18
docs/source/APPNOTE_011_Design_Investigation/sumprod_00.dot
View File

@ -1,18 +0,0 @@
digraph "sumprod" {
rankdir="LR";
remincross=true;
v0 [ label="a" ];
v1 [ label="b" ];
v2 [ label="$1_Y" ];
c4 [ shape=record, label="{{<p1> A|<p2> B}|$1\n$add|{<p3> Y}}" ];
v3 [ label="$1_Y" ];
v4 [ label="c" ];
v5 [ label="sum" ];
c5 [ shape=record, label="{{<p1> A|<p2> B}|$2\n$add|{<p3> Y}}" ];
v0:e -> c4:p1:w [color="black", style="setlinewidth(3)", label=""];
v1:e -> c4:p2:w [color="black", style="setlinewidth(3)", label=""];
c4:p3:e -> v2:w [color="black", style="setlinewidth(3)", label=""];
v3:e -> c5:p1:w [color="black", style="setlinewidth(3)", label=""];
v4:e -> c5:p2:w [color="black", style="setlinewidth(3)", label=""];
c5:p3:e -> v5:w [color="black", style="setlinewidth(3)", label=""];
}

15
docs/source/APPNOTE_011_Design_Investigation/sumprod_01.dot
View File

@ -1,15 +0,0 @@
digraph "sumprod" {
rankdir="LR";
remincross=true;
n2 [ shape=octagon, label="a", color="black", fontcolor="black" ];
n3 [ shape=octagon, label="b", color="black", fontcolor="black" ];
n4 [ shape=octagon, label="c", color="black", fontcolor="black" ];
n5 [ shape=octagon, label="sum", color="black", fontcolor="black" ];
c9 [ shape=record, label="{{<p6> A|<p7> B}|$1\n$add|{<p8> Y}}" ];
c10 [ shape=record, label="{{<p6> A|<p7> B}|$2\n$add|{<p8> Y}}" ];
c9:p8:e -> c10:p6:w [color="black", style="setlinewidth(3)", label=""];
n2:e -> c9:p6:w [color="black", style="setlinewidth(3)", label=""];
n3:e -> c9:p7:w [color="black", style="setlinewidth(3)", label=""];
n4:e -> c10:p7:w [color="black", style="setlinewidth(3)", label=""];
c10:p8:e -> n5:w [color="black", style="setlinewidth(3)", label=""];
}

5
docs/source/APPNOTE_011_Design_Investigation/sumprod_02.dot
View File

@ -1,5 +0,0 @@
digraph "sumprod" {
rankdir="LR";
remincross=true;
n1 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
}

11
docs/source/APPNOTE_011_Design_Investigation/sumprod_03.dot
View File

@ -1,11 +0,0 @@
digraph "sumprod" {
rankdir="LR";
remincross=true;
n1 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
v0 [ label="$3_Y" ];
v1 [ label="c" ];
c5 [ shape=record, label="{{<p2> A|<p3> B}|$4\n$mul|{<p4> Y}}" ];
c5:p4:e -> n1:w [color="black", style="setlinewidth(3)", label=""];
v0:e -> c5:p2:w [color="black", style="setlinewidth(3)", label=""];
v1:e -> c5:p3:w [color="black", style="setlinewidth(3)", label=""];
}

11
docs/source/APPNOTE_011_Design_Investigation/sumprod_04.dot
View File

@ -1,11 +0,0 @@
digraph "sumprod" {
rankdir="LR";
remincross=true;
n2 [ shape=octagon, label="c", color="black", fontcolor="black" ];
n3 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
c7 [ shape=record, label="{{<p4> A|<p5> B}|$4\n$mul|{<p6> Y}}" ];
n1 [ shape=diamond, label="$3_Y" ];
n1:e -> c7:p4:w [color="black", style="setlinewidth(3)", label=""];
n2:e -> c7:p5:w [color="black", style="setlinewidth(3)", label=""];
c7:p6:e -> n3:w [color="black", style="setlinewidth(3)", label=""];
}

15
docs/source/APPNOTE_011_Design_Investigation/sumprod_05.dot
View File

@ -1,15 +0,0 @@
digraph "sumprod" {
rankdir="LR";
remincross=true;
n2 [ shape=octagon, label="c", color="black", fontcolor="black" ];
n3 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
v0 [ label="a" ];
v1 [ label="b" ];
c7 [ shape=record, label="{{<p4> A|<p5> B}|$3\n$mul|{<p6> Y}}" ];
c8 [ shape=record, label="{{<p4> A|<p5> B}|$4\n$mul|{<p6> Y}}" ];
c7:p6:e -> c8:p4:w [color="black", style="setlinewidth(3)", label=""];
n2:e -> c8:p5:w [color="black", style="setlinewidth(3)", label=""];
c8:p6:e -> n3:w [color="black", style="setlinewidth(3)", label=""];
v0:e -> c7:p4:w [color="black", style="setlinewidth(3)", label=""];
v1:e -> c7:p5:w [color="black", style="setlinewidth(3)", label=""];
}

141
docs/source/CHAPTER_Approach.rst
View File

@ -1,141 +0,0 @@
.. _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
<fig:approach_flow>`).
.. 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.

233
docs/source/CHAPTER_Eval.rst
View File

@ -1,233 +0,0 @@
.. _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::

96
docs/source/CHAPTER_Intro.rst
View File

@ -1,96 +0,0 @@
.. _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 <chapter:intro>` is this introduction.
:numref:`Chapter %s <chapter:basics>` covers a short introduction to the world
of HDL synthesis. Basic principles and the terminology are outlined in this
chapter.
:numref:`Chapter %s <chapter:approach>` 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 <chapter:overview>` 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 <chapter:celllib>` 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 <chapter:prog>` 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 <chapter:verilog>`, :numref:`%s <chapter:opt>` and
:numref:`%s <chapter:techmap>` cover three important pieces of the synthesis
pipeline: The Verilog frontend, the optimization passes and the technology
mapping to the target architecture, respectively.
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.

330
docs/source/CHAPTER_Optimize.rst
View File

@ -1,330 +0,0 @@
.. _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 <chapter:celllib>`. 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 <tab:opt_expr_and>` 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
<sec:techmap_extern>` for details).

571
docs/source/CHAPTER_Overview.rst
View File

@ -1,571 +0,0 @@
.. _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 <fig:Overview_flow>` 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 <fig:Overview_RTLIL>` 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
<fig:Overview_RTLIL>` 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 <sec:memcells>` 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
<sec:typusecase>` 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").

46
docs/source/CHAPTER_Prog.rst
View File

@ -1,46 +0,0 @@
.. _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:: temp/GettingStarted
:language: none
:caption: guidelines/GettingStarted
.. literalinclude:: temp/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
docs/source/CHAPTER_Prog/stubnets.cc.
.. literalinclude:: CHAPTER_Prog/stubnets.cc
:language: c++
:linenos:
:caption: docs/source/CHAPTER_Prog/stubnets.cc
.. literalinclude:: CHAPTER_Prog/Makefile
:language: makefile
:linenos:
:caption: docs/source/CHAPTER_Prog/Makefile
.. literalinclude:: CHAPTER_Prog/test.v
:language: verilog
:linenos:
:caption: docs/source/CHAPTER_Prog/test.v

666
docs/source/CHAPTER_Verilog.rst
View File

@ -1,666 +0,0 @@
.. _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 <fig:Verilog_flow>`.
.. 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 <prefix>[<index>].<suffix> (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 <tab:Verilog_AstNodeType>`
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 $\ <number> \\\ <original_name> 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$<input>:4$2
connect \A \in1
connect \Y $logic_not$<input>:4$2_Y
end
cell $xor $xor$<input>:13$3
connect \A $1\out1[0:0]
connect \B \out2
connect \Y $xor$<input>:13$3_Y
end
process $proc$<input>:1$1
assign $0\out3[0:0] \out3
assign $0\out2[0:0] $1\out1[0:0]
assign $0\out1[0:0] $xor$<input>:13$3_Y
switch \in2
case 1'1
assign $1\out1[0:0] $logic_not$<input>: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
(\\\ <name>) to the current temporary signal for the same thing
(initially $0\\\ <name>).
- | ``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.

BIN
docs/source/_downloads/APPNOTE_010_Verilog_to_BLIF.pdf Normal file
View File

Binary file not shown.

BIN
docs/source/_downloads/APPNOTE_012_Verilog_to_BTOR.pdf Normal file
View File

Binary file not shown.

46
docs/source/_images/Makefile Normal file
View File

@ -0,0 +1,46 @@
all: examples all_tex tidy
# set a fake time in pdf generation to prevent unnecessary differences in output
FAKETIME := TZ='Z' faketime -f '2022-01-01 00:00:00 x0,001'
# find all code example makefiles
.PHONY: examples
CODE_EXAMPLES := ../code_examples/*/Makefile
examples: $(CODE_EXAMPLES)
# target to convert specified dot file(s)
.PHONY: convert
TARG_DOT ?=
convert: $(TARG_DOT:.dot=.pdf) $(TARG_DOT:.dot=.svg)
# use empty FORCE target because .PHONY ignores % expansion, using find allows
# us to generate everything in one pass, since we don't know all of the possible
# outputs until the sub-makes run
FORCE:
../%/Makefile: FORCE
@make -C $(@D) dots
@mkdir -p $*
@find $(@D) -name *.dot -exec cp -u {} -t $* \;
@find $* -name *.dot -printf "%p " | xargs -i make --no-print-directory convert TARG_DOT="{}"
# find and build all tex files
.PHONY: all_tex
TEX_FILES := $(wildcard **/*.tex)
all_tex: $(TEX_FILES:.tex=.pdf) $(TEX_FILES:.tex=.svg)
%.pdf: %.dot
$(FAKETIME) dot -Tpdf -o $@ $<
%.pdf: %.tex
cd $(@D) && $(FAKETIME) pdflatex $(<F) --interaction=nonstopmode
%.svg: %.pdf
pdf2svg $< $@
.PHONY: clean tidy
tidy:
rm -f **/*.log **/*.aux
clean: tidy
rm -rf code_examples
rm -f **/*.pdf **/*.svg

0
docs/images/approach_flow.tex → docs/source/_images/internals/approach_flow.tex
View File

0
docs/images/overview_flow.tex → docs/source/_images/internals/overview_flow.tex
View File

0
docs/images/overview_rtlil.tex → docs/source/_images/internals/overview_rtlil.tex
View File

20
docs/source/_images/internals/simplified_rtlil.tex Normal file
View File

@ -0,0 +1,20 @@
\documentclass[12pt,tikz]{standalone}
\pdfinfoomitdate 1
\pdfsuppressptexinfo 1
\pdftrailerid{}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{pgfplots}
\usepackage{tikz}
\pagestyle{empty}
\begin{document}
\begin{tikzpicture}[every node/.style={transform shape}]
\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] (wire) [fill=blue!10, right of=module, node distance=10em] {RTLIL::Wire} (wire.west) edge [-latex] (module);
\node[entity] (cell) [fill=blue!10, above of=wire] {RTLIL::Cell} (cell.west) edge [-latex] (module);
\end{tikzpicture}
\end{document}

0
docs/images/verilog_flow.tex → docs/source/_images/internals/verilog_flow.tex
View File

0
docs/images/basics_abstractions.tex → docs/source/_images/primer/basics_abstractions.tex
View File

0
docs/images/basics_ast.tex → docs/source/_images/primer/basics_ast.tex
View File

0
docs/images/basics_flow.tex → docs/source/_images/primer/basics_flow.tex
View File

0
docs/images/basics_parsetree.tex → docs/source/_images/primer/basics_parsetree.tex
View File

42
docs/source/_images/primer/levels_of_abstraction.tex Normal file
View File

@ -0,0 +1,42 @@
\documentclass[12pt,tikz]{standalone}
\pdfinfoomitdate 1
\pdfsuppressptexinfo 1
\pdftrailerid{}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{pgfplots}
\usepackage{tikz}
\pagestyle{empty}
\definecolor{MyBlue}{RGB}{85,130,180}
\begin{document}
\begin{tikzpicture}[scale=1.2, every node/.style={transform shape}]
\tikzstyle{lvl} = [draw, fill=MyBlue, 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) -- ++(4,0) coordinate (a);
\draw[dotted] (pgx) -- ++(4,0) coordinate (b);
\draw[|->|] (a) -- node[right] {Yosys} (b);
\end{tikzpicture}
\end{document}

20
docs/source/_static/custom.css Normal file
View File

@ -0,0 +1,20 @@
/* Reduce whitespace in cmd def pages */
.cmd.def .highlight-yoscrypt, .cmd.def .highlight pre {
padding: 0%;
margin: 0%;
}
.cmd.def .highlight-none, .cmd.def .highlight pre {
padding-top: 0%;
margin-top: 0%;
}
/* Make images full width */
.width-helper {
max-width: 100%;
}
/* Prevent code block caption text from bunching into the caption number */
.literal-block-wrapper .code-block-caption .caption-number {
padding-right: 0.5em
}

0
docs/static/favico.png → docs/source/_static/favico.png
View File

Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 33 KiB

After

Width:  |  Height:  |  Size: 33 KiB

0
docs/static/logo.png → docs/source/_static/logo.png
View File

Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 16 KiB

After

Width:  |  Height:  |  Size: 16 KiB

26
docs/source/_static/yosyshq.css Normal file
View File

@ -0,0 +1,26 @@
/* Don't hide the right sidebar as we're placing our fixed links there */
aside.no-toc {
display: block !important;
}
/* Colorful headings */
h1 {
color: var(--color-brand-primary);
}
h2, h3, h4, h5, h6 {
color: var(--color-brand-content);
}
/* Use a different color for external links */
a.external {
color: var(--color-brand-primary) !important;
}
.wy-table-responsive table td {
white-space: normal;
}
th {
text-align: left;
}

44
docs/source/_templates/page.html Normal file
View File

@ -0,0 +1,44 @@
{#
See https://github.com/pradyunsg/furo/blob/main/src/furo/theme/furo/page.html for the original
block this is overwriting.
The part that is customized is between the "begin of custom part" and "end of custom part"
comments below. It uses the same styles as the existing right sidebar code.
#}
{% extends "furo/page.html" %}
{% block right_sidebar %}
<div class="toc-sticky toc-scroll">
{# begin of custom part #}
<div class="toc-title-container">
<span class="toc-title">
YosysHQ
</span>
</div>
<div class="toc-tree-container yosyshq-links" style="padding-bottom: 0">
<div class="toc-tree">
<ul>
<li></li>
<li><a class="reference external" href="https://yosyshq.readthedocs.io">Docs</a></li>
<li><a class="reference external" href="https://blog.yosyshq.com">Blog</a></li>
<li><a class="reference external" href="https://www.yosyshq.com">Website</a></li>
</ul>
</div>
</div>
{# end of custom part #}
{% if not furo_hide_toc %}
<div class="toc-title-container">
<span class="toc-title">
{{ _("On this page") }}
</span>
</div>
<div class="toc-tree-container">
<div class="toc-tree">
{{ toc }}
</div>
</div>
{% endif %}
</div>
{% endblock %}

18
docs/source/appendix.rst Normal file
View File

@ -0,0 +1,18 @@
Appendix
========
.. toctree::
:maxdepth: 2
:includehidden:
appendix/primer
appendix/auxlibs
appendix/auxprogs
bib
.. toctree::
:maxdepth: 1
:includehidden:
cmd_ref

667
docs/source/appendix/APPNOTE_010_Verilog_to_BLIF.rst
View File

@ -1,336 +1,363 @@
:orphan:
==================================== ====================================
010: Converting Verilog to BLIF page 010: Converting Verilog to BLIF page
==================================== ====================================
Installation Abstract
============ ========
Yosys written in C++ (using features from C++11) and is tested on modern Verilog-2005 is a powerful Hardware Description Language (HDL) that can be used
Linux. It should compile fine on most UNIX systems with a C++11 to easily create complex designs from small HDL code. It is the preferred method
compiler. The README file contains useful information on building Yosys of design entry for many designers.
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 Berkeley Logic Interchange Format (BLIF) is a simple file format for
The Verilog sources used for the examples are taken from `yosys-bigsim`_, a exchanging sequential logic between programs. It is easy to generate and easy to
collection of real-world designs used for regression testing Yosys. parse and is therefore the preferred method of design entry for many authors of
logic synthesis tools.
.. _Yosys GIT: https://github.com/YosysHQ/yosys Yosys is a feature-rich Open-Source Verilog synthesis tool that can be used to
bridge the gap between the two file formats. It implements most of Verilog-2005
and thus can be used to import modern behavioral Verilog designs into BLIF-based
design flows without dependencies on proprietary synthesis tools.
.. _Rev. e216e0e: https://github.com/YosysHQ/yosys/tree/e216e0e The scope of Yosys goes of course far beyond Verilog logic synthesis. But it is
a useful and important feature and this Application Note will focus on this
aspect of Yosys.
.. _yosys-bigsim: https://github.com/YosysHQ/yosys-bigsim Download
========
Getting started This document was originally published in April 2015:
=============== :download:`Converting Verilog to BLIF PDF</_downloads/APPNOTE_010_Verilog_to_BLIF.pdf>`
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) Installation
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 Yosys written in C++ (using features from C++11) and is tested on modern
commands that operate on Yosys' internal state. For example, the -o Linux. It should compile fine on most UNIX systems with a C++11
softusb_navre.blif option just adds the command write_blif compiler. The README file contains useful information on building Yosys
softusb_navre.blif to the end of the script. Likewise a file on the and its prerequisites.
command line – softusb_navre.v in this case – adds the command
read_verilog softusb_navre.v to the beginning of the synthesis script. Yosys is a large and feature-rich program with a couple of dependencies.
In both cases the file type is detected from the file extension. 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.
Finally the option -S instantiates a built-in default synthesis script. This Application Note is based on `Yosys GIT`_ `Rev. e216e0e`_ from 2013-11-23.
Instead of using -S one could also specify the synthesis commands for The Verilog sources used for the examples are taken from `yosys-bigsim`_, a
the script on the command line using the -p option, either using collection of real-world designs used for regression testing Yosys.
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 .. _Yosys GIT: https://github.com/YosysHQ/yosys
========================
With a script file we have better control over Yosys. The following .. _Rev. e216e0e: https://github.com/YosysHQ/yosys/tree/e216e0e
script file replicates what the command from the last section did:
.. code:: yoscrypt .. _yosys-bigsim: https://github.com/YosysHQ/yosys-bigsim
read_verilog softusb_navre.v Getting started
hierarchy ===============
proc; opt; memory; opt; techmap; opt
write_blif softusb_navre.blif 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)
The first and last line obviously read the Verilog file and write the in a single design file (softusb_navre.v). It also is using only features that
BLIF file. map nicely to the BLIF format, for example it only uses synchronous resets.
The 2nd line checks the design hierarchy and instantiates parametrized .. _Navré processor: http://opencores.org/projects/navre
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 Converting softusb_navre.v to softusb_navre.blif could not be easier:
script should always contain this command as first command after reading
the input files. .. code:: sh
The 3rd line does most of the actual work: yosys -o softusb_navre.blif -S softusb_navre.v
- The command opt is the Yosys' built-in optimizer. It can perform some Behind the scenes Yosys is controlled by synthesis scripts that execute
simple optimizations such as const-folding and removing unconnected commands that operate on Yosys' internal state. For example, the -o
parts of the design. It is common practice to call opt after each softusb_navre.blif option just adds the command write_blif
major step in the synthesis procedure. In cases where too much softusb_navre.blif to the end of the script. Likewise a file on the
optimization is not appreciated (for example when analyzing a command line – softusb_navre.v in this case – adds the command
design), it is recommended to call clean instead of opt. read_verilog softusb_navre.v to the beginning of the synthesis script.
In both cases the file type is detected from the file extension.
- The command proc converts processes (Yosys' internal representation
of Verilog always- and initial-blocks) to circuits of multiplexers Finally the option -S instantiates a built-in default synthesis script.
and storage elements (various types of flip-flops). Instead of using -S one could also specify the synthesis commands for
the script on the command line using the -p option, either using
- The command memory converts Yosys' internal representations of arrays individual options for each command or by passing one big command string
and array accesses to multi-port block memories, and then maps this with a semicolon-separated list of commands. But in most cases it is
block memories to address decoders and flip-flops, unless the option more convenient to use an actual script file.
-nomap is used, in which case the multi-port block memories stay in
the design and can then be mapped to architecture-specific memory Using a synthesis script
primitives using other commands. ========================
- The command techmap turns a high-level circuit with coarse grain With a script file we have better control over Yosys. The following
cells such as wide adders and multipliers to a fine-grain circuit of script file replicates what the command from the last section did:
simple logic primitives and single-bit storage elements. The command
does that by substituting the complex cells by circuits of simpler .. code:: yoscrypt
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 read_verilog softusb_navre.v
next section. hierarchy
proc; opt; memory; opt; techmap; opt
Now Yosys can be run with the filename of the synthesis script as write_blif softusb_navre.blif
argument:
The first and last line obviously read the Verilog file and write the
.. code:: sh BLIF file.
yosys softusb_navre.ys The 2nd line checks the design hierarchy and instantiates parametrized
versions of the modules in the design, if necessary. In the case of this
Now that we are using a synthesis script we can easily modify how Yosys simple design this is a no-op. However, as a general rule a synthesis
synthesizes the design. The first thing we should customize is the call script should always contain this command as first command after reading
to the hierarchy command: the input files.
Whenever it is known that there are no implicit blackboxes in the The 3rd line does most of the actual work:
design, i.e. modules that are referenced but are not defined, the
hierarchy command should be called with the -check option. This will - The command opt is the Yosys' built-in optimizer. It can perform some
then cause synthesis to fail when implicit blackboxes are found in the simple optimizations such as const-folding and removing unconnected
design. parts of the design. It is common practice to call opt after each
major step in the synthesis procedure. In cases where too much
The 2nd thing we can improve regarding the hierarchy command is that we optimization is not appreciated (for example when analyzing a
can tell it the name of the top level module of the design hierarchy. It design), it is recommended to call clean instead of opt.
will then automatically remove all modules that are not referenced from
this top level module. - The command proc converts processes (Yosys' internal representation
of Verilog always- and initial-blocks) to circuits of multiplexers
For many designs it is also desired to optimize the encodings for the and storage elements (various types of flip-flops).
finite state machines (FSMs) in the design. The fsm command finds FSMs,
extracts them, performs some basic optimizations and then generate a - The command memory converts Yosys' internal representations of arrays
circuit from the extracted and optimized description. It would also be and array accesses to multi-port block memories, and then maps this
possible to tell the fsm command to leave the FSMs in their extracted block memories to address decoders and flip-flops, unless the option
form, so they can be further processed using custom commands. But in -nomap is used, in which case the multi-port block memories stay in
this case we don't want that. the design and can then be mapped to architecture-specific memory
primitives using other commands.
So now we have the final synthesis script for generating a BLIF file for
the Navré CPU: - The command techmap turns a high-level circuit with coarse grain
cells such as wide adders and multipliers to a fine-grain circuit of
.. code:: yoscrypt simple logic primitives and single-bit storage elements. The command
does that by substituting the complex cells by circuits of simpler
read_verilog softusb_navre.v cells. It is possible to provide a custom set of rules for this
hierarchy -check -top softusb_navre process in the form of a Verilog source file, as we will see in the
proc; opt; memory; opt; fsm; opt; techmap; opt next section.
write_blif softusb_navre.blif
Now Yosys can be run with the filename of the synthesis script as
Advanced example: The Amber23 ARMv2a CPU argument:
========================================
.. code:: sh
Our 2nd example is the `Amber23 ARMv2a CPU`_. Once again we base our example on
the Verilog code that is included in `yosys-bigsim`_. yosys softusb_navre.ys
.. _Amber23 ARMv2a CPU: http://opencores.org/projects/amber 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
.. code-block:: yoscrypt to the hierarchy command:
:caption: `amber23.ys`
:name: amber23.ys Whenever it is known that there are no implicit blackboxes in the
design, i.e. modules that are referenced but are not defined, the
read_verilog a23_alu.v hierarchy command should be called with the -check option. This will
read_verilog a23_barrel_shift_fpga.v then cause synthesis to fail when implicit blackboxes are found in the
read_verilog a23_barrel_shift.v design.
read_verilog a23_cache.v
read_verilog a23_coprocessor.v The 2nd thing we can improve regarding the hierarchy command is that we
read_verilog a23_core.v can tell it the name of the top level module of the design hierarchy. It
read_verilog a23_decode.v will then automatically remove all modules that are not referenced from
read_verilog a23_execute.v this top level module.
read_verilog a23_fetch.v
read_verilog a23_multiply.v For many designs it is also desired to optimize the encodings for the
read_verilog a23_ram_register_bank.v finite state machines (FSMs) in the design. The fsm command finds FSMs,
read_verilog a23_register_bank.v extracts them, performs some basic optimizations and then generate a
read_verilog a23_wishbone.v circuit from the extracted and optimized description. It would also be
read_verilog generic_sram_byte_en.v possible to tell the fsm command to leave the FSMs in their extracted
read_verilog generic_sram_line_en.v form, so they can be further processed using custom commands. But in
hierarchy -check -top a23_core this case we don't want that.
add -global_input globrst 1
proc -global_arst globrst So now we have the final synthesis script for generating a BLIF file for
techmap -map adff2dff.v the Navré CPU:
opt; memory; opt; fsm; opt; techmap
write_blif amber23.blif .. code:: yoscrypt
The problem with this core is that it contains no dedicated reset logic. Instead read_verilog softusb_navre.v
the coding techniques shown in :numref:`glob_arst` are used to define reset hierarchy -check -top softusb_navre
values for the global asynchronous reset in an FPGA implementation. This design proc; opt; memory; opt; fsm; opt; techmap; opt
can not be expressed in BLIF as it is. Instead we need to use a synthesis script write_blif softusb_navre.blif
that transforms this form to synchronous resets that can be expressed in BLIF.
Advanced example: The Amber23 ARMv2a CPU
(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.) Our 2nd example is the `Amber23 ARMv2a CPU`_. Once again we base our example on
the Verilog code that is included in `yosys-bigsim`_.
: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 .. _Amber23 ARMv2a CPU: http://opencores.org/projects/amber
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 .. code-block:: yoscrypt
signal is connected throughout the whole design hierarchy. :caption: `amber23.ys`
:name: amber23.ys
.. code-block:: verilog
:caption: Implicit coding of global asynchronous resets read_verilog a23_alu.v
:name: glob_arst read_verilog a23_barrel_shift_fpga.v
read_verilog a23_barrel_shift.v
reg [7:0] a = 13, b; read_verilog a23_cache.v
initial b = 37; read_verilog a23_coprocessor.v
read_verilog a23_core.v
.. code-block:: verilog read_verilog a23_decode.v
:caption: `adff2dff.v` read_verilog a23_execute.v
:name: adff2dff.v read_verilog a23_fetch.v
read_verilog a23_multiply.v
(* techmap_celltype = "$adff" *) read_verilog a23_ram_register_bank.v
module adff2dff (CLK, ARST, D, Q); read_verilog a23_register_bank.v
read_verilog a23_wishbone.v
parameter WIDTH = 1; read_verilog generic_sram_byte_en.v
parameter CLK_POLARITY = 1; read_verilog generic_sram_line_en.v
parameter ARST_POLARITY = 1; hierarchy -check -top a23_core
parameter ARST_VALUE = 0; add -global_input globrst 1
proc -global_arst globrst
input CLK, ARST; techmap -map adff2dff.v
input [WIDTH-1:0] D; opt; memory; opt; fsm; opt; techmap
output reg [WIDTH-1:0] Q; write_blif amber23.blif
wire [1023:0] _TECHMAP_DO_ = "proc"; 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
wire _TECHMAP_FAIL_ = values for the global asynchronous reset in an FPGA implementation. This design
!CLK_POLARITY || !ARST_POLARITY; 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.
always @(posedge CLK)
if (ARST) (Note that there is no problem if this coding techniques are used to model ROM,
Q <= ARST_VALUE; where the register is initialized using this syntax but is never updated
else otherwise.)
Q <= D;
:numref:`amber23.ys` shows the synthesis script for the Amber23 core. In line 17
endmodule 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
In line 18 the proc command is called. But in this script the signal design hierarchy and then all module instantiations are altered so that this new
name globrst is passed to the command as a global reset signal for signal is connected throughout the whole design hierarchy.
resetting the registers to their assigned initial values.
.. code-block:: verilog
Finally in line 19 the techmap command is used to replace all instances of :caption: Implicit coding of global asynchronous resets
flip-flops with asynchronous resets with flip-flops with synchronous resets. The :name: glob_arst
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 reg [7:0] a = 13, b;
cells to replace in the design, how the \_TECHMAP_FAIL\_ wire in lines 15 and 16 initial b = 37;
(which evaluates to a constant value) determines if the parameter set is
compatible with this replacement circuit, and how the \_TECHMAP_DO\_ wire in .. code-block:: verilog
line 13 provides a mini synthesis-script to be used to process this cell. :caption: `adff2dff.v`
:name: adff2dff.v
.. code-block:: c
:caption: Test program for the Amber23 CPU (Sieve of Eratosthenes). Compiled (* techmap_celltype = "$adff" *)
using GCC 4.6.3 for ARM with ``-Os -marm -march=armv2a module adff2dff (CLK, ARST, D, Q);
-mno-thumb-interwork -ffreestanding``, linked with ``--fix-v4bx``
set and booted with a custom setup routine written in ARM assembler. parameter WIDTH = 1;
:name: sieve parameter CLK_POLARITY = 1;
parameter ARST_POLARITY = 1;
#include <stdint.h> parameter ARST_VALUE = 0;
#include <stdbool.h>
input CLK, ARST;
#define BITMAP_SIZE 64 input [WIDTH-1:0] D;
#define OUTPORT 0x10000000 output reg [WIDTH-1:0] Q;
static uint32_t bitmap[BITMAP_SIZE/32]; wire [1023:0] _TECHMAP_DO_ = "proc";
static void bitmap_set(uint32_t idx) { bitmap[idx/32] |= 1 << (idx % 32); } wire _TECHMAP_FAIL_ =
static bool bitmap_get(uint32_t idx) { return (bitmap[idx/32] & (1 << (idx % 32))) != 0; } !CLK_POLARITY || !ARST_POLARITY;
static void output(uint32_t val) { *((volatile uint32_t*)OUTPORT) = val; }
always @(posedge CLK)
int main() { if (ARST)
uint32_t i, j, k; Q <= ARST_VALUE;
output(2); else
for (i = 0; i < BITMAP_SIZE; i++) { Q <= D;
if (bitmap_get(i)) continue;
output(3+2*i); endmodule
for (j = 2*(3+2*i);; j += 3+2*i) {
if (j%2 == 0) continue; In line 18 the :cmd:ref:`proc` command is called. But in this script the signal
k = (j-3)/2; name globrst is passed to the command as a global reset signal for resetting the
if (k >= BITMAP_SIZE) break; registers to their assigned initial values.
bitmap_set(k);
} 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
output(0); map file used for this is shown in :numref:`adff2dff.v`. Note how the
return 0; ``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
Verification of the Amber23 CPU 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.
The BLIF file for the Amber23 core, generated using :numref:`amber23.ys` and .. code-block:: c
:numref:`adff2dff.v` and the version of the Amber23 RTL source that is bundled :caption: Test program for the Amber23 CPU (Sieve of Eratosthenes). Compiled
with yosys-bigsim, was verified using the test-bench from yosys-bigsim. It using GCC 4.6.3 for ARM with ``-Os -marm -march=armv2a
successfully executed the program shown in :numref:`sieve` in the test-bench. -mno-thumb-interwork -ffreestanding``, linked with ``--fix-v4bx``
set and booted with a custom setup routine written in ARM assembler.
For simulation the BLIF file was converted back to Verilog using `ABC`_. So this :name: sieve
test includes the successful transformation of the BLIF file into ABC's internal
format as well. #include <stdint.h>
#include <stdbool.h>
.. _ABC: https://github.com/berkeley-abc/abc
#define BITMAP_SIZE 64
The only thing left to write about the simulation itself is that it #define OUTPORT 0x10000000
probably was one of the most energy inefficient and time consuming ways
of successfully calculating the first 31 primes the author has ever static uint32_t bitmap[BITMAP_SIZE/32];
conducted.
static void bitmap_set(uint32_t idx) { bitmap[idx/32] |= 1 << (idx % 32); }
Limitations 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; }
At the time of this writing Yosys does not support multi-dimensional int main() {
memories, does not support writing to individual bits of array elements, uint32_t i, j, k;
does not support initialization of arrays with $readmemb and $readmemh, output(2);
and has only limited support for tristate logic, to name just a few for (i = 0; i < BITMAP_SIZE; i++) {
limitations. if (bitmap_get(i)) continue;
output(3+2*i);
That being said, Yosys can synthesize an overwhelming majority of for (j = 2*(3+2*i);; j += 3+2*i) {
real-world Verilog RTL code. The remaining cases can usually be modified if (j%2 == 0) continue;
to be compatible with Yosys quite easily. k = (j-3)/2;
if (k >= BITMAP_SIZE) break;
The various designs in yosys-bigsim are a good place to look for bitmap_set(k);
examples of what is within the capabilities of Yosys. }
}
Conclusion output(0);
========== return 0;
}
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 Verification of the Amber23 CPU
low-level logic circuits. ===============================
The command line option -S can be used to quickly synthesize Verilog The BLIF file for the Amber23 core, generated using :numref:`amber23.ys` and
code to BLIF files without a hassle. :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
With custom synthesis scripts it becomes possible to easily perform successfully executed the program shown in :numref:`sieve` in the test-bench.
high-level optimizations, such as re-encoding FSMs. In some extreme
cases, such as the Amber23 ARMv2 CPU, the more advanced Yosys features For simulation the BLIF file was converted back to Verilog using `ABC`_. So this
can be used to change a design to fit a certain need without actually test includes the successful transformation of the BLIF file into ABC's internal
touching the RTL code. 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.

965
docs/source/appendix/APPNOTE_011_Design_Investigation.rst
View File

@ -1,965 +0,0 @@
==========================================
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
``<bit_width>'<bits>`` is used for for constants that are not 32-bit wide and/or
contain bits that are not 0 or 1 (i.e. ``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:: ../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 ``<MSB_LEFT>:<LSB_LEFT> -
<MSB_RIGHT>:<LSB_RIGHT>``. Each of this boxes has one signal per row on one side
and a common signal for all rows on the other side. The ``<MSB>:<LSB>`` 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 <filename>`` option.
Secondly it is possible to load cell libraries into the design with the
``read_verilog -lib <filename>`` command. The 2nd method has the great advantage
that the library only needs to be loaded once and can then be used in all
subsequent calls to the ``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 <integer>`` argument, which randomly assigns colors to the nets.
The integer (> 0) is used as seed value for the random color assignments.
Sometimes it is necessary it try some values to find an assignment of colors
that looks good.
The command ``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 ``<module_name>/``. 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:: ../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:: ../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:: ../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
<name>``. It can later be recalled using ``select @<name>``. In fact, the
``@<name>`` 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:: ../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.

570
docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst
View File

@ -1,333 +1,353 @@
:orphan:
==================================== ====================================
012: Converting Verilog to BTOR page 012: Converting Verilog to BTOR page
==================================== ====================================
Installation Abstract
============ ========
Yosys written in C++ (using features from C++11) and is tested on modern Linux. Verilog-2005 is a powerful Hardware Description Language (HDL) that can be used
It should compile fine on most UNIX systems with a C++11 compiler. The README to easily create complex designs from small HDL code. BTOR is a bit-precise
file contains useful information on building Yosys and its prerequisites. word-level format for model checking. It is a simple format and easy to parse.
It allows to model the model checking problem over the theory of bit-vectors
with one-dimensional arrays, thus enabling to model Verilog designs with
registers and memories. Yosys is an Open-Source Verilog synthesis tool that can
be used to convert Verilog designs with simple assertions to BTOR format.
Yosys is a large and feature-rich program with some dependencies. For this work, Download
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. This document was originally published in November 2013:
:download:`Converting Verilog to BTOR PDF</_downloads/APPNOTE_012_Verilog_to_BTOR.pdf>`
.. _Yosys GIT: https://github.com/YosysHQ/yosys ..
Installation
============
.. _Rev. 082550f: https://github.com/YosysHQ/yosys/tree/082550f 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.
Quick start 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.
We assume that the Verilog design is synthesizable and we also assume that the This Application Note is based on `Yosys GIT`_ `Rev. 082550f` from 2015-04-04.
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 .. _Yosys GIT: https://github.com/YosysHQ/yosys
Verilog design to BTOR. The script can be found in the ``backends/btor``
directory. The following example shows its usage:
.. code:: sh .. _Rev. 082550f: https://github.com/YosysHQ/yosys/tree/082550f
verilog2btor.sh fsm.v fsm.btor test Quick start
===========
The script ``verilog2btor.sh`` takes three parameters. In the above example, the We assume that the Verilog design is synthesizable and we also assume that the
first parameter ``fsm.v`` is the input design, the second parameter ``fsm.btor`` design does not have multi-dimensional memories. As BTOR implicitly initializes
is the file name of BTOR output, and the third parameter ``test`` is the name of registers to zero value and memories stay uninitialized, we assume that the
top module in the design. Verilog design does not contain initial blocks. For more details about the BTOR
format, please refer to :cite:p:`btor`.
To specify the properties (that need to be checked), we have two We provide a shell script ``verilog2btor.sh`` which can be used to convert a
options: Verilog design to BTOR. The script can be found in the ``backends/btor``
directory. The following example shows its usage:
- We can use the Verilog ``assert`` statement in the procedural block or module .. code:: sh
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 verilog2btor.sh fsm.v fsm.btor test
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 The script ``verilog2btor.sh`` takes three parameters. In the above example, the
:caption: Specifying property in Verilog design with ``assert`` first parameter ``fsm.v`` is the input design, the second parameter ``fsm.btor``
:name: specifying_property_assert is the file name of BTOR output, and the third parameter ``test`` is the name of
top module in the design.
module test(input clk, input rst, output y); To specify the properties (that need to be checked), we have two
options:
reg [2:0] state; - 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.
always @(posedge clk) begin - We can use a single-bit output wire, whose name starts with ``safety``. The
if (rst || state == 3) begin value of this output wire needs to be driven low when the property is met,
state <= 0; i.e. the solver will try to find a model that makes the safety pin go high.
end else begin This is demonstrated in :numref:`specifying_property_output`.
assert(state < 3);
state <= state + 1;
end
end
assign y = state[2]; .. code-block:: verilog
:caption: Specifying property in Verilog design with ``assert``
:name: specifying_property_assert
assert property (y !== 1'b1); module test(input clk, input rst, output y);
endmodule reg [2:0] state;
.. code-block:: verilog always @(posedge clk) begin
:caption: Specifying property in Verilog design with output wire if (rst || state == 3) begin
:name: specifying_property_output state <= 0;
end else begin
assert(state < 3);
state <= state + 1;
end
end
module test(input clk, input rst, assign y = state[2];
output y, output safety1);
reg [2:0] state; assert property (y !== 1'b1);
always @(posedge clk) begin endmodule
if (rst || state == 3)
state <= 0;
else
state <= state + 1;
end
assign y = state[2]; .. code-block:: verilog
:caption: Specifying property in Verilog design with output wire
:name: specifying_property_output
assign safety1 = !(y !== 1'b1); module test(input clk, input rst,
output y, output safety1);
endmodule reg [2:0] state;
We can run `Boolector`_ ``1.4.1`` [1]_ on the generated BTOR file: always @(posedge clk) begin
if (rst || state == 3)
state <= 0;
else
state <= state + 1;
end
.. _Boolector: http://fmv.jku.at/boolector/ assign y = state[2];
.. code:: sh assign safety1 = !(y !== 1'b1);
$ boolector fsm.btor endmodule
unsat
We can also use `nuXmv`_, but on BTOR designs it does not support memories yet. We can run `Boolector`_ ``1.4.1`` [1]_ on the generated BTOR file:
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 .. _Boolector: http://fmv.jku.at/boolector/
Detailed flow .. code:: sh
=============
Yosys is able to synthesize Verilog designs up to the gate level. We are $ boolector fsm.btor
interested in keeping registers and memories when synthesizing the design. For unsat
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 We can also use `nuXmv`_, but on BTOR designs it does not support memories yet.
:caption: Synthesis Flow for BTOR with memories With the next release of nuXmv, we will be also able to verify designs with
:name: btor_script_memory memories.
read_verilog -sv $1; .. _nuXmv: https://es-static.fbk.eu/tools/nuxmv/index.php
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 Detailed flow
line: =============
#. Reading the input file. 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``.
#. Setting the top module in the hierarchy and trying to read automatically the .. code-block:: yoscrypt
files which are given as ``include`` in the file read in first line. :caption: Synthesis Flow for BTOR with memories
:name: btor_script_memory
#. Checking the design hierarchy. 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;
#. Converting processes to multiplexers (muxs) and flip-flops. Here is short description of what is happening in the script line by
line:
#. Removing undef signals from muxs. #. Reading the input file.
#. Hiding all signal names that are not used as module ports. #. 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.
#. Explicit type conversion, by introducing slice and concat cells in the #. Checking the design hierarchy.
circuit.
#. Converting write memories to synchronous memories, and collecting the #. Converting processes to multiplexers (muxs) and flip-flops.
memories to multi-port memories.
#. Flattening the design to get only one module. #. Removing undef signals from muxs.
#. Separating read and write memories. #. Hiding all signal names that are not used as module ports.
#. Splitting the signals that are partially assigned #. Explicit type conversion, by introducing slice and concat cells in the
circuit.
#. Setting undef to zero value. #. Converting write memories to synchronous memories, and collecting the
memories to multi-port memories.
#. Final optimization pass. #. Flattening the design to get only one module.
#. Writing BTOR file. #. Separating read and write memories.
For detailed description of the commands mentioned above, please refer #. Splitting the signals that are partially assigned
to the Yosys documentation, or run ``yosys -h <command_name>``.
#. Setting undef to zero value.
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, #. Final optimization pass.
and introduces a new command ``memory`` at line number 8.
:numref:`btor_script_without_memory` shows the modified Yosys script file: #. Writing BTOR file.
.. code-block:: sh For detailed description of the commands mentioned above, please refer
:caption: Synthesis Flow for BTOR without memories to the Yosys documentation, or run ``yosys -h <command_name>``.
:name: btor_script_without_memory
The script presented earlier can be easily modified to have a BTOR file that
read_verilog -sv $1; does not contain memories. This is done by removing the line number 8 and 10,
hierarchy -top $3; hierarchy -libdir $DIR; and introduces a new command :cmd:ref:`memory` at line number 8.
hierarchy -check; :numref:`btor_script_without_memory` shows the modified Yosys script file:
proc; opt;
opt_expr -mux_undef; opt; .. code-block:: sh
rename -hide;;; :caption: Synthesis Flow for BTOR without memories
splice; opt; :name: btor_script_without_memory
memory;;
flatten;; read_verilog -sv $1;
splitnets -driver; hierarchy -top $3; hierarchy -libdir $DIR;
setundef -zero -undriven; hierarchy -check;
opt;;; proc; opt;
write_btor $2; opt_expr -mux_undef; opt;
rename -hide;;;
Example splice; opt;
======= memory;;
flatten;;
Here is an example Verilog design that we want to convert to BTOR: splitnets -driver;
setundef -zero -undriven;
.. code-block:: verilog opt;;;
:caption: Example - Verilog Design write_btor $2;
:name: example_verilog
Example
module array(input clk); =======
reg [7:0] counter; Here is an example Verilog design that we want to convert to BTOR:
reg [7:0] mem [7:0];
.. code-block:: verilog
always @(posedge clk) begin :caption: Example - Verilog Design
counter <= counter + 8'd1; :name: example_verilog
mem[counter] <= counter;
end module array(input clk);
assert property (!(counter > 8'd0) || reg [7:0] counter;
mem[counter - 8'd1] == counter - 8'd1); reg [7:0] mem [7:0];
endmodule always @(posedge clk) begin
counter <= counter + 8'd1;
The generated BTOR file that contain memories, using the script shown in mem[counter] <= counter;
:numref:`btor_memory`: end
.. code-block:: assert property (!(counter > 8'd0) ||
:caption: Example - Converted BTOR with memory mem[counter - 8'd1] == counter - 8'd1);
:name: btor_memory
endmodule
1 var 1 clk
2 array 8 3 The generated BTOR file that contain memories, using the script shown in
3 var 8 $auto$rename.cc:150:execute$20 :numref:`btor_memory`:
4 const 8 00000001
5 sub 8 3 4 .. code-block::
6 slice 3 5 2 0 :caption: Example - Converted BTOR with memory
7 read 8 2 6 :name: btor_memory
8 slice 3 3 2 0
9 add 8 3 4 1 var 1 clk
10 const 8 00000000 2 array 8 3
11 ugt 1 3 10 3 var 8 $auto$rename.cc:150:execute$20
12 not 1 11 4 const 8 00000001
13 const 8 11111111 5 sub 8 3 4
14 slice 1 13 0 0 6 slice 3 5 2 0
15 one 1 7 read 8 2 6
16 eq 1 1 15 8 slice 3 3 2 0
17 and 1 16 14 9 add 8 3 4
18 write 8 3 2 8 3 10 const 8 00000000
19 acond 8 3 17 18 2 11 ugt 1 3 10
20 anext 8 3 2 19 12 not 1 11
21 eq 1 7 5 13 const 8 11111111
22 or 1 12 21 14 slice 1 13 0 0
23 const 1 1 15 one 1
24 one 1 16 eq 1 1 15
25 eq 1 23 24 17 and 1 16 14
26 cond 1 25 22 24 18 write 8 3 2 8 3
27 root 1 -26 19 acond 8 3 17 18 2
28 cond 8 1 9 3 20 anext 8 3 2 19
29 next 8 3 28 21 eq 1 7 5
22 or 1 12 21
And the BTOR file obtained by the script shown in 23 const 1 1
:numref:`btor_without_memory`, which expands the memory into individual 24 one 1
elements: 25 eq 1 23 24
26 cond 1 25 22 24
.. code-block:: 27 root 1 -26
:caption: Example - Converted BTOR with memory 28 cond 8 1 9 3
:name: btor_without_memory 29 next 8 3 28
1 var 1 clk And the BTOR file obtained by the script shown in
2 var 8 mem[0] :numref:`btor_without_memory`, which expands the memory into individual
3 var 8 $auto$rename.cc:150:execute$20 elements:
4 slice 3 3 2 0
5 slice 1 4 0 0 .. code-block::
6 not 1 5 :caption: Example - Converted BTOR with memory
7 slice 1 4 1 1 :name: btor_without_memory
8 not 1 7
9 slice 1 4 2 2 1 var 1 clk
10 not 1 9 2 var 8 mem[0]
11 and 1 8 10 3 var 8 $auto$rename.cc:150:execute$20
12 and 1 6 11 4 slice 3 3 2 0
13 cond 8 12 3 2 5 slice 1 4 0 0
14 cond 8 1 13 2 6 not 1 5
15 next 8 2 14 7 slice 1 4 1 1
16 const 8 00000001 8 not 1 7
17 add 8 3 16 9 slice 1 4 2 2
18 const 8 00000000 10 not 1 9
19 ugt 1 3 18 11 and 1 8 10
20 not 1 19 12 and 1 6 11
21 var 8 mem[2] 13 cond 8 12 3 2
22 and 1 7 10 14 cond 8 1 13 2
23 and 1 6 22 15 next 8 2 14
24 cond 8 23 3 21 16 const 8 00000001
25 cond 8 1 24 21 17 add 8 3 16
26 next 8 21 25 18 const 8 00000000
27 sub 8 3 16 19 ugt 1 3 18
20 not 1 19
... 21 var 8 mem[2]
22 and 1 7 10
54 cond 1 53 50 52 23 and 1 6 22
55 root 1 -54 24 cond 8 23 3 21
25 cond 8 1 24 21
... 26 next 8 21 25
27 sub 8 3 16
77 cond 8 76 3 44
78 cond 8 1 77 44 ...
79 next 8 44 78
54 cond 1 53 50 52
Limitations 55 root 1 -54
===========
...
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 77 cond 8 76 3 44
be removed when converting to BTOR. It should also be kept in consideration that 78 cond 8 1 77 44
BTOR does not support the ``x`` or ``z`` values of Verilog. 79 next 8 44 78
Another thing to bear in mind is that Yosys will convert multi-dimensional Limitations
memories to one-dimensional memories and address decoders. Therefore ===========
out-of-bounds memory accesses can yield unexpected results.
BTOR does not support initialization of memories and registers, i.e. they are
Conclusion 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.
Using the described flow, we can use Yosys to generate word-level verification
benchmarks with or without memories from Verilog designs. Another thing to bear in mind is that Yosys will convert multi-dimensional
memories to one-dimensional memories and address decoders. Therefore
.. [1] out-of-bounds memory accesses can yield unexpected results.
Newer version of Boolector do not support sequential models.
Boolector 1.4.1 can be built with picosat-951. Newer versions of Conclusion
picosat have an incompatible API. ==========
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.

42
docs/source/appendix/CHAPTER_Auxlibs.rst
View File

@ -1,42 +0,0 @@
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`).

29
docs/source/appendix/CHAPTER_Auxprogs.rst
View File

@ -1,29 +0,0 @@
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 <sec:techmap_extern>` 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.

410
docs/source/appendix/CHAPTER_StateOfTheArt.rst
View File

@ -1,410 +0,0 @@
.. _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 <fig:StateOfTheArt_always12>`
and :numref:`Fig. %s <fig:StateOfTheArt_always3>`
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 <fig:StateOfTheArt_arrays>`
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 <fig:StateOfTheArt_for>` 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 <fig:StateOfTheArt_gen>` 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:`<CHAPTER_eval>` 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.)

81
docs/source/appendix/auxlibs.rst Normal file
View File

@ -0,0 +1,81 @@
Auxiliary libraries
===================
The Yosys source distribution contains some auxiliary libraries that are
compiled into Yosys and can be used in plugins.
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/
dlfcn-win32
-----------
The ``dlfcn`` library enables runtime loading of plugins without requiring
recompilation of Yosys. The files in ``libs/dlfcn-win32`` provide an
implementation of ``dlfcn`` for Windows.
See also: https://github.com/dlfcn-win32/dlfcn-win32
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 :cmd:ref:`sat` pass (see
:doc:`/cmd/sat`).
fst
---
``libfst`` files from `gtkwave`_ are included in ``libs/fst`` to support
reading/writing signal traces from/to the GTKWave developed FST format. This is
primarily used in the :cmd:ref:`sim` command.
.. _gtkwave: https://github.com/gtkwave/gtkwave
json11
------
For reading/writing designs from/to JSON, :cmd:ref:`read_json` and
:cmd:ref:`write_json` should be used. For everything else there is the `json11
library`_:
json11 is a tiny JSON library for C++11, providing JSON parsing and
serialization.
This library is used for outputting machine-readable statistics (:cmd:ref:`stat`
with ``-json`` flag), using the RPC frontend (:cmd:ref:`connect_rpc`), and the
yosys-witness ``yw`` format.
.. _json11 library: https://github.com/dropbox/json11
MiniSAT
-------
The files in ``libs/minisat`` provide a high-performance SAT solver, used by the
:cmd:ref:`sat` command.
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.
.. _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`).

63
docs/source/appendix/auxprogs.rst Normal file
View File

@ -0,0 +1,63 @@
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 :doc:`/yosys_internals/extending_yosys/extensions` for details.
.. literalinclude:: /temp/yosys-config
:start-at: Usage
.. _sec:filterlib:
yosys-filterlib
---------------
.. todo:: how does a filterlib rules-file work?
The ``yosys-filterlib`` tool is a small utility that can be used to strip or
extract information from a Liberty file. This can be useful for removing
sensitive or proprietary information such as timing or other trade secrets.
.. literalinclude:: /temp/yosys-filterlib
:start-at: Usage
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.
.. literalinclude:: /temp/yosys-abc
:start-at: usage
:end-before: UC Berkeley
yosys-smtbmc
------------
The ``yosys-smtbmc`` tool is a utility used by SBY for interacting with smt
solvers.
.. literalinclude:: /temp/yosys-smtbmc
yosys-witness
-------------
``yosys-witness`` is a new tool to inspect and convert yosys witness traces.
This is used in SBY and SCY for producing traces in a consistent format
independent of the solver.
.. literalinclude:: /temp/yosys-witness
:start-at: Usage
.. note:: ``yosys-witness`` requires `click`_ Python package for use.
.. _click: https://pypi.org/project/click/

31
docs/source/appendix/env_vars.rst Normal file
View File

@ -0,0 +1,31 @@
Yosys environment variables
===========================
``HOME``
Yosys command history is stored in :file:`$HOME/.yosys_history`. Graphics
(from :cmd:ref:`show` and :cmd:ref:`viz` commands) will output to this
directory by default. This environment variable is also used in some cases
for resolving filenames with :file:`~`.
``PATH``
May be used in OpenBSD builds for finding the location of Yosys executable.
``TMPDIR``
Used for storing temporary files.
``ABC``
When compiling Yosys with out-of-tree ABC using :makevar:`ABCEXTERNAL`, this
variable can be used to override the external ABC executable.
``YOSYS_NOVERIFIC``
If Yosys was built with Verific, this environment variable can be used to
temporarily disable Verific support.
``YOSYS_COVER_DIR`` and ``YOSYS_COVER_FILE``
When using code coverage, these environment variables control the output file
name/location.
``YOSYS_ABORT_ON_LOG_ERROR``
Can be used for debugging Yosys internals. Setting it to 1 causes abort() to
be called when Yosys terminates with an error message.

30
docs/source/CHAPTER_Basics.rst → docs/source/appendix/primer.rst
View File

@ -3,8 +3,8 @@
.. _chapter:basics: .. _chapter:basics:
Basic principles A primer on digital circuit synthesis
================ =====================================
This chapter contains a short introduction to the basic principles of digital This chapter contains a short introduction to the basic principles of digital
circuit synthesis. circuit synthesis.
@ -23,7 +23,7 @@ circuit to a functionally equivalent low-level representation of a circuit.
:numref:`Figure %s <fig:Basics_abstractions>` lists the different levels of :numref:`Figure %s <fig:Basics_abstractions>` lists the different levels of
abstraction and how they relate to different kinds of synthesis. abstraction and how they relate to different kinds of synthesis.
.. figure:: ../images/basics_abstractions.* .. figure:: /_images/primer/basics_abstractions.*
:class: width-helper :class: width-helper
:name: fig:Basics_abstractions :name: fig:Basics_abstractions
@ -161,7 +161,7 @@ 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, 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). 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 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 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 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. the most basic language constructs for instantiation and connecting of cells.
@ -172,7 +172,7 @@ good) mapping of the logic gate netlist to an equivalent netlist of physically
available gate types. available gate types.
The simplest approach to logic synthesis is two-level logic synthesis, where a 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 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 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 cannot make efficient use of physical gates other than AND/NAND-, OR/NOR-
and NOT-Gates. and NOT-Gates.
@ -196,7 +196,7 @@ Physical gate level
On the physical gate level only gates are used that are physically available on 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 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 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 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 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 representation is a netlist of LUTs with optional output registers, as these are
the basic building blocks of FPGA logic cells. the basic building blocks of FPGA logic cells.
@ -345,7 +345,7 @@ covered by the Verilog synthesis standard and when writing new designs one
should limit herself or himself to these cases. should limit herself or himself to these cases.
In behavioural modelling, blocking assignments (=) and non-blocking assignments In behavioural modelling, blocking assignments (=) and non-blocking assignments
(<=) can be used. The concept of blocking vs. non-blocking assignment is one of (<=) can be used. The concept of blocking vs. non-blocking assignment is one of
the most misunderstood constructs in Verilog :cite:p:`Cummings00`. the most misunderstood constructs in Verilog :cite:p:`Cummings00`.
The blocking assignment behaves exactly like an assignment in any imperative The blocking assignment behaves exactly like an assignment in any imperative
@ -498,7 +498,7 @@ Then the synthesizable description is transformed to lower-level representations
using a series of tools and the results are again verified using simulation. using a series of tools and the results are again verified using simulation.
This process is illustrated in :numref:`Fig. %s <fig:Basics_flow>`. This process is illustrated in :numref:`Fig. %s <fig:Basics_flow>`.
.. figure:: ../images/basics_flow.* .. figure:: /_images/primer/basics_flow.*
:class: width-helper :class: width-helper
:name: fig:Basics_flow :name: fig:Basics_flow
@ -515,8 +515,8 @@ Gate-Level Model are verified and the design process is finished.
However, in any real-world design effort there will be multiple iterations for 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 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 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 (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). order to meet the design requirements (e.g. maximum possible clock speed).
Whenever the behavioural model or the system level model is changed their 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 equivalence must be re-verified by re-running the simulations and comparing the
@ -572,7 +572,7 @@ of lexical tokens given in :numref:`Tab. %s <tab:Basics_tokens>`.
TOK_SEMICOLON \- TOK_SEMICOLON \-
============== =============== ============== ===============
The lexer is usually generated by a lexer generator (e.g. flex ) from a 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 description file that is using regular expressions to specify the text pattern
that should match the individual tokens. that should match the individual tokens.
@ -586,7 +586,7 @@ 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 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 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 parser is also typically generated by a code generator (e.g. bison) from a
grammar description in Backus-Naur Form (BNF). grammar description in Backus-Naur Form (BNF).
Let's consider the following BNF (in Bison syntax): Let's consider the following BNF (in Bison syntax):
@ -597,7 +597,7 @@ Let's consider the following BNF (in Bison syntax):
assign_stmt: TOK_ASSIGN TOK_IDENTIFIER TOK_EQ expr TOK_SEMICOLON; assign_stmt: TOK_ASSIGN TOK_IDENTIFIER TOK_EQ expr TOK_SEMICOLON;
expr: TOK_IDENTIFIER | TOK_NUMBER | expr TOK_PLUS expr; expr: TOK_IDENTIFIER | TOK_NUMBER | expr TOK_PLUS expr;
.. figure:: ../images/basics_parsetree.* .. figure:: /_images/primer/basics_parsetree.*
:class: width-helper :class: width-helper
:name: fig:Basics_parsetree :name: fig:Basics_parsetree
@ -610,7 +610,7 @@ 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 snippets (so-called reduce-functions) for all inner nodes of the parse tree in
depth-first order. depth-first order.
In some very simple applications (e.g. code generation for stack machines) it is 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 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 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 with the relevant information from the parse tree. This data structure is called
@ -626,7 +626,7 @@ 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 suitable for further processing. In compilers this is often an assembler-like
three-address-code intermediate representation. :cite:p:`Dragonbook` three-address-code intermediate representation. :cite:p:`Dragonbook`
.. figure:: ../images/basics_ast.* .. figure:: /_images/primer/basics_ast.*
:class: width-helper :class: width-helper
:name: fig:Basics_ast :name: fig:Basics_ast

1
docs/source/bib.rst
View File

@ -7,3 +7,4 @@
.. bibliography:: literature.bib .. bibliography:: literature.bib
.. todo:: see if we can get the two hanging appnotes as lit references

7
docs/source/cmd_ref.rst
View File

@ -3,9 +3,14 @@
================================================================================ ================================================================================
Command line reference Command line reference
================================================================================ ================================================================================
.. literalinclude:: /temp/yosys
:start-at: Usage
.. toctree:: .. toctree::
:caption: Command reference :caption: Command reference
:maxdepth: 1 :maxdepth: 1
:glob: :glob:
cmd/* /appendix/env_vars
/cmd/*

1
manual/PRESENTATION_ExAdv/.gitignore → docs/source/code_examples/.gitignore vendored
View File

@ -1 +1,2 @@
*.dot *.dot
*.pdf

0
manual/PRESENTATION_ExOth/axis_master.v → docs/source/code_examples/axis/axis_master.v
View File

0
manual/PRESENTATION_ExOth/axis_test.v → docs/source/code_examples/axis/axis_test.v
View File

2
manual/PRESENTATION_ExOth/axis_test.ys → docs/source/code_examples/axis/axis_test.ys
View File

@ -2,4 +2,4 @@ read_verilog -sv axis_master.v axis_test.v
hierarchy -top axis_test hierarchy -top axis_test
proc; flatten;; proc; flatten;;
sat -falsify -seq 50 -prove-asserts sat -seq 50 -prove-asserts

0
manual/PRESENTATION_Prog/.gitignore → docs/source/code_examples/extensions/.gitignore vendored
View File

32
docs/source/code_examples/extensions/Makefile Normal file
View File

@ -0,0 +1,32 @@
PROGRAM_PREFIX :=
YOSYS ?= ../../../../$(PROGRAM_PREFIX)yosys
.PHONY: all dots
all: dots test0.log test1.log test2.log
dots: test1.dot
CXXFLAGS=$(shell $(YOSYS)-config --cxxflags)
DATDIR=$(shell $(YOSYS)-config --datdir)
my_cmd.so: my_cmd.cc
$(YOSYS)-config --exec --cxx $(subst $(DATDIR),../../../../share,$(CXXFLAGS)) --ldflags -o my_cmd.so -shared my_cmd.cc --ldlibs
test0.log: my_cmd.so
$(YOSYS) -Ql test0.log_new -m ./my_cmd.so -p 'my_cmd foo bar' absval_ref.v
mv test0.log_new test0.log
test1.log: my_cmd.so
$(YOSYS) -Ql test1.log_new -m ./my_cmd.so -p 'clean; test1; dump' absval_ref.v
mv test1.log_new test1.log
test1.dot: my_cmd.so
$(YOSYS) -m ./my_cmd.so -p 'test1; show -format dot -prefix test1'
test2.log: my_cmd.so
$(YOSYS) -Ql test2.log_new -m ./my_cmd.so -p 'hierarchy -top test; test2' sigmap_test.v
mv test2.log_new test2.log
.PHONY: clean
clean:
rm -f *.d *.so *.dot

2
manual/PRESENTATION_Prog/absval_ref.v → docs/source/code_examples/extensions/absval_ref.v
View File

@ -1,3 +1,3 @@
module absval_ref(input signed [3:0] a, output [3:0] y); module absval_ref(input signed [3:0] a, output [3:0] y);
assign y = a[3] ? -a : a; assign y = a[3] ? -a : a;
endmodule endmodule

2
manual/PRESENTATION_Prog/my_cmd.cc → docs/source/code_examples/extensions/my_cmd.cc
View File

@ -14,7 +14,7 @@ struct MyPass : public Pass {
log("Modules in current design:\n"); log("Modules in current design:\n");
for (auto mod : design->modules()) for (auto mod : design->modules())
log(" %s (%zd wires, %zd cells)\n", log_id(mod), log(" %s (%d wires, %d cells)\n", log_id(mod),
GetSize(mod->wires()), GetSize(mod->cells())); GetSize(mod->wires()), GetSize(mod->cells()));
} }
} MyPass; } MyPass;

2
manual/PRESENTATION_Prog/sigmap_test.v → docs/source/code_examples/extensions/sigmap_test.v
View File

@ -1,3 +1,3 @@
module test(input a, output x, y); module test(input a, output x, y);
assign x = a, y = a; assign x = a, y = a;
endmodule endmodule

24
docs/source/code_examples/fifo/Makefile Normal file
View File

@ -0,0 +1,24 @@
PROGRAM_PREFIX :=
YOSYS ?= ../../../../$(PROGRAM_PREFIX)yosys
DOT_NAMES = addr_gen_hier addr_gen_proc addr_gen_clean
DOT_NAMES += rdata_proc rdata_flat rdata_adffe rdata_memrdv2 rdata_alumacc rdata_coarse
MAPDOT_NAMES = rdata_map_ram rdata_map_ffram rdata_map_gates
MAPDOT_NAMES += rdata_map_ffs rdata_map_luts rdata_map_cells
DOTS := $(addsuffix .dot,$(DOT_NAMES))
MAPDOTS := $(addsuffix .dot,$(MAPDOT_NAMES))
all: dots fifo.out fifo.stat
dots: $(DOTS) $(MAPDOTS)
$(DOTS) fifo.out: fifo.v fifo.ys
$(YOSYS) fifo.ys -l fifo.out -Q -T
$(MAPDOTS) fifo.stat: fifo.v fifo_map.ys
$(YOSYS) fifo_map.ys
.PHONY: clean
clean:
rm -f *.dot

65
docs/source/code_examples/fifo/fifo.libmap Normal file
View File

@ -0,0 +1,65 @@
yosys> debug memory_libmap -lib +/ice40/brams.txt -lib +/ice40/spram.txt -no-auto-huge
yosys> memory_libmap -lib +/ice40/brams.txt -lib +/ice40/spram.txt -no-auto-huge
4. Executing MEMORY_LIBMAP pass (mapping memories to cells).
Memory fifo.data mapping candidates (post-geometry):
- logic fallback
- cost: 2048.000000
- $__ICE40_RAM4K_:
- option HAS_BE 0
- emulation score: 7
- replicates (for ports): 1
- replicates (for data): 1
- mux score: 0
- demux score: 0
- cost: 78.000000
- abits 11 dbits 2 4 8 16
- chosen base width 8
- swizzle 0 1 2 3 4 5 6 7
- emulate read-first behavior
- write port 0: port group W
- widths 2 4 8
- read port 0: port group R
- widths 2 4 8 16
- emulate transparency with write port 0
- $__ICE40_RAM4K_:
- option HAS_BE 1
- emulation score: 7
- replicates (for ports): 1
- replicates (for data): 1
- mux score: 0
- demux score: 0
- cost: 78.000000
- abits 11 dbits 2 4 8 16
- byte width 1
- chosen base width 8
- swizzle 0 1 2 3 4 5 6 7
- emulate read-first behavior
- write port 0: port group W
- widths 16
- read port 0: port group R
- widths 2 4 8 16
- emulate transparency with write port 0
Memory fifo.data mapping candidates (after post-geometry prune):
- logic fallback
- cost: 2048.000000
- $__ICE40_RAM4K_:
- option HAS_BE 0
- emulation score: 7
- replicates (for ports): 1
- replicates (for data): 1
- mux score: 0
- demux score: 0
- cost: 78.000000
- abits 11 dbits 2 4 8 16
- chosen base width 8
- swizzle 0 1 2 3 4 5 6 7
- emulate read-first behavior
- write port 0: port group W
- widths 2 4 8
- read port 0: port group R
- widths 2 4 8 16
- emulate transparency with write port 0
mapping memory fifo.data via $__ICE40_RAM4K_

425
docs/source/code_examples/fifo/fifo.out Normal file
View File

@ -0,0 +1,425 @@
-- Executing script file `fifo.ys' --
$ yosys fifo.v
-- Parsing `fifo.v' using frontend ` -vlog2k' --
1. Executing Verilog-2005 frontend: fifo.v
Parsing Verilog input from `fifo.v' to AST representation.
Storing AST representation for module `$abstract\addr_gen'.
Storing AST representation for module `$abstract\fifo'.
Successfully finished Verilog frontend.
echo on
yosys> hierarchy -top addr_gen
2. Executing HIERARCHY pass (managing design hierarchy).
3. Executing AST frontend in derive mode using pre-parsed AST for module `\addr_gen'.
Generating RTLIL representation for module `\addr_gen'.
3.1. Analyzing design hierarchy..
Top module: \addr_gen
3.2. Analyzing design hierarchy..
Top module: \addr_gen
Removing unused module `$abstract\fifo'.
Removing unused module `$abstract\addr_gen'.
Removed 2 unused modules.
yosys> select -module addr_gen
yosys [addr_gen]> select -list
addr_gen
addr_gen/$1\addr[7:0]
addr_gen/$add$fifo.v:19$3_Y
addr_gen/$eq$fifo.v:16$2_Y
addr_gen/$0\addr[7:0]
addr_gen/addr
addr_gen/rst
addr_gen/clk
addr_gen/en
addr_gen/$add$fifo.v:19$3
addr_gen/$eq$fifo.v:16$2
addr_gen/$proc$fifo.v:0$4
addr_gen/$proc$fifo.v:12$1
yosys [addr_gen]> select t:*
yosys [addr_gen]*> select -list
addr_gen/$add$fifo.v:19$3
addr_gen/$eq$fifo.v:16$2
yosys [addr_gen]*> select -set new_cells %
yosys [addr_gen]*> select -clear
yosys> show -format dot -prefix addr_gen_show addr_gen
4. Generating Graphviz representation of design.
Writing dot description to `addr_gen_show.dot'.
Dumping module addr_gen to page 1.
yosys> show -format dot -prefix new_cells_show -notitle @new_cells
5. Generating Graphviz representation of design.
Writing dot description to `new_cells_show.dot'.
Dumping selected parts of module addr_gen to page 1.
yosys> show -color maroon3 @new_cells -color cornflowerblue p:* -notitle -format dot -prefix addr_gen_hier
6. Generating Graphviz representation of design.
Writing dot description to `addr_gen_hier.dot'.
Dumping module addr_gen to page 1.
yosys> proc -noopt
7. Executing PROC pass (convert processes to netlists).
yosys> proc_clean
7.1. Executing PROC_CLEAN pass (remove empty switches from decision trees).
Cleaned up 0 empty switches.
yosys> proc_rmdead
7.2. Executing PROC_RMDEAD pass (remove dead branches from decision trees).
Marked 2 switch rules as full_case in process $proc$fifo.v:12$1 in module addr_gen.
Removed a total of 0 dead cases.
yosys> proc_prune
7.3. Executing PROC_PRUNE pass (remove redundant assignments in processes).
Removed 0 redundant assignments.
Promoted 1 assignment to connection.
yosys> proc_init
7.4. Executing PROC_INIT pass (extract init attributes).
Found init rule in `\addr_gen.$proc$fifo.v:0$4'.
Set init value: \addr = 8'00000000
yosys> proc_arst
7.5. Executing PROC_ARST pass (detect async resets in processes).
Found async reset \rst in `\addr_gen.$proc$fifo.v:12$1'.
yosys> proc_rom
7.6. Executing PROC_ROM pass (convert switches to ROMs).
Converted 0 switches.
<suppressed ~2 debug messages>
yosys> proc_mux
7.7. Executing PROC_MUX pass (convert decision trees to multiplexers).
Creating decoders for process `\addr_gen.$proc$fifo.v:0$4'.
Creating decoders for process `\addr_gen.$proc$fifo.v:12$1'.
1/1: $0\addr[7:0]
yosys> proc_dlatch
7.8. Executing PROC_DLATCH pass (convert process syncs to latches).
yosys> proc_dff
7.9. Executing PROC_DFF pass (convert process syncs to FFs).
Creating register for signal `\addr_gen.\addr' using process `\addr_gen.$proc$fifo.v:12$1'.
created $adff cell `$procdff$10' with positive edge clock and positive level reset.
yosys> proc_memwr
7.10. Executing PROC_MEMWR pass (convert process memory writes to cells).
yosys> proc_clean
7.11. Executing PROC_CLEAN pass (remove empty switches from decision trees).
Removing empty process `addr_gen.$proc$fifo.v:0$4'.
Found and cleaned up 2 empty switches in `\addr_gen.$proc$fifo.v:12$1'.
Removing empty process `addr_gen.$proc$fifo.v:12$1'.
Cleaned up 2 empty switches.
yosys> select -set new_cells t:$mux t:*dff
yosys> show -color maroon3 @new_cells -notitle -format dot -prefix addr_gen_proc
8. Generating Graphviz representation of design.
Writing dot description to `addr_gen_proc.dot'.
Dumping module addr_gen to page 1.
yosys> opt_expr
9. Executing OPT_EXPR pass (perform const folding).
Optimizing module addr_gen.
yosys> clean
Removed 0 unused cells and 4 unused wires.
yosys> select -set new_cells t:$eq
yosys> show -color cornflowerblue @new_cells -notitle -format dot -prefix addr_gen_clean
10. Generating Graphviz representation of design.
Writing dot description to `addr_gen_clean.dot'.
Dumping module addr_gen to page 1.
yosys> design -reset
yosys> read_verilog fifo.v
11. Executing Verilog-2005 frontend: fifo.v
Parsing Verilog input from `fifo.v' to AST representation.
Generating RTLIL representation for module `\addr_gen'.
Generating RTLIL representation for module `\fifo'.
Successfully finished Verilog frontend.
yosys> hierarchy -check -top fifo
12. Executing HIERARCHY pass (managing design hierarchy).
12.1. Analyzing design hierarchy..
Top module: \fifo
Used module: \addr_gen
Parameter \MAX_DATA = 256
12.2. Executing AST frontend in derive mode using pre-parsed AST for module `\addr_gen'.
Parameter \MAX_DATA = 256
Generating RTLIL representation for module `$paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000'.
Parameter \MAX_DATA = 256
Found cached RTLIL representation for module `$paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000'.
12.3. Analyzing design hierarchy..
Top module: \fifo
Used module: $paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000
12.4. Analyzing design hierarchy..
Top module: \fifo
Used module: $paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000
Removing unused module `\addr_gen'.
Removed 1 unused modules.
yosys> proc
13. Executing PROC pass (convert processes to netlists).
yosys> proc_clean
13.1. Executing PROC_CLEAN pass (remove empty switches from decision trees).
Cleaned up 0 empty switches.
yosys> proc_rmdead
13.2. Executing PROC_RMDEAD pass (remove dead branches from decision trees).
Marked 2 switch rules as full_case in process $proc$fifo.v:62$24 in module fifo.
Marked 1 switch rules as full_case in process $proc$fifo.v:36$16 in module fifo.
Marked 2 switch rules as full_case in process $proc$fifo.v:12$32 in module $paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.
Removed a total of 0 dead cases.
yosys> proc_prune
13.3. Executing PROC_PRUNE pass (remove redundant assignments in processes).
Removed 0 redundant assignments.
Promoted 6 assignments to connections.
yosys> proc_init
13.4. Executing PROC_INIT pass (extract init attributes).
Found init rule in `\fifo.$proc$fifo.v:0$31'.
Set init value: \count = 9'000000000
Found init rule in `$paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.$proc$fifo.v:0$35'.
Set init value: \addr = 8'00000000
yosys> proc_arst
13.5. Executing PROC_ARST pass (detect async resets in processes).
Found async reset \rst in `\fifo.$proc$fifo.v:62$24'.
Found async reset \rst in `$paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.$proc$fifo.v:12$32'.
yosys> proc_rom
13.6. Executing PROC_ROM pass (convert switches to ROMs).
Converted 0 switches.
<suppressed ~5 debug messages>
yosys> proc_mux
13.7. Executing PROC_MUX pass (convert decision trees to multiplexers).
Creating decoders for process `\fifo.$proc$fifo.v:0$31'.
Creating decoders for process `\fifo.$proc$fifo.v:62$24'.
1/1: $0\count[8:0]
Creating decoders for process `\fifo.$proc$fifo.v:36$16'.
1/3: $1$memwr$\data$fifo.v:38$15_EN[7:0]$22
2/3: $1$memwr$\data$fifo.v:38$15_DATA[7:0]$21
3/3: $1$memwr$\data$fifo.v:38$15_ADDR[7:0]$20
Creating decoders for process `$paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.$proc$fifo.v:0$35'.
Creating decoders for process `$paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.$proc$fifo.v:12$32'.
1/1: $0\addr[7:0]
yosys> proc_dlatch
13.8. Executing PROC_DLATCH pass (convert process syncs to latches).
yosys> proc_dff
13.9. Executing PROC_DFF pass (convert process syncs to FFs).
Creating register for signal `\fifo.\count' using process `\fifo.$proc$fifo.v:62$24'.
created $adff cell `$procdff$55' with positive edge clock and positive level reset.
Creating register for signal `\fifo.\rdata' using process `\fifo.$proc$fifo.v:36$16'.
created $dff cell `$procdff$56' with positive edge clock.
Creating register for signal `\fifo.$memwr$\data$fifo.v:38$15_ADDR' using process `\fifo.$proc$fifo.v:36$16'.
created $dff cell `$procdff$57' with positive edge clock.
Creating register for signal `\fifo.$memwr$\data$fifo.v:38$15_DATA' using process `\fifo.$proc$fifo.v:36$16'.
created $dff cell `$procdff$58' with positive edge clock.
Creating register for signal `\fifo.$memwr$\data$fifo.v:38$15_EN' using process `\fifo.$proc$fifo.v:36$16'.
created $dff cell `$procdff$59' with positive edge clock.
Creating register for signal `$paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.\addr' using process `$paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.$proc$fifo.v:12$32'.
created $adff cell `$procdff$60' with positive edge clock and positive level reset.
yosys> proc_memwr
13.10. Executing PROC_MEMWR pass (convert process memory writes to cells).
yosys> proc_clean
13.11. Executing PROC_CLEAN pass (remove empty switches from decision trees).
Removing empty process `fifo.$proc$fifo.v:0$31'.
Found and cleaned up 2 empty switches in `\fifo.$proc$fifo.v:62$24'.
Removing empty process `fifo.$proc$fifo.v:62$24'.
Found and cleaned up 1 empty switch in `\fifo.$proc$fifo.v:36$16'.
Removing empty process `fifo.$proc$fifo.v:36$16'.
Removing empty process `$paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.$proc$fifo.v:0$35'.
Found and cleaned up 2 empty switches in `$paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.$proc$fifo.v:12$32'.
Removing empty process `$paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.$proc$fifo.v:12$32'.
Cleaned up 5 empty switches.
yosys> opt_expr -keepdc
13.12. Executing OPT_EXPR pass (perform const folding).
Optimizing module fifo.
Optimizing module $paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.
yosys> select -set new_cells t:$memrd
yosys> show -color maroon3 c:fifo_reader -color cornflowerblue @new_cells -notitle -format dot -prefix rdata_proc o:rdata %ci*
14. Generating Graphviz representation of design.
Writing dot description to `rdata_proc.dot'.
Dumping selected parts of module fifo to page 1.
yosys> flatten
15. Executing FLATTEN pass (flatten design).
Deleting now unused module $paramod\addr_gen\MAX_DATA=s32'00000000000000000000000100000000.
<suppressed ~2 debug messages>
yosys> clean
Removed 3 unused cells and 25 unused wires.
yosys> select -set rdata_path o:rdata %ci*
yosys> select -set new_cells @rdata_path o:rdata %ci3 %d i:* %d
yosys> show -color maroon3 @new_cells -notitle -format dot -prefix rdata_flat @rdata_path
16. Generating Graphviz representation of design.
Writing dot description to `rdata_flat.dot'.
Dumping selected parts of module fifo to page 1.
yosys> opt_dff
17. Executing OPT_DFF pass (perform DFF optimizations).
Adding EN signal on $procdff$55 ($adff) from module fifo (D = $0\count[8:0], Q = \count).
Adding EN signal on $flatten\fifo_writer.$procdff$60 ($adff) from module fifo (D = $flatten\fifo_writer.$procmux$51_Y, Q = \fifo_writer.addr).
Adding EN signal on $flatten\fifo_reader.$procdff$60 ($adff) from module fifo (D = $flatten\fifo_reader.$procmux$51_Y, Q = \fifo_reader.addr).
yosys> select -set new_cells t:$adffe
yosys> show -color maroon3 @new_cells -notitle -format dot -prefix rdata_adffe o:rdata %ci*
18. Generating Graphviz representation of design.
Writing dot description to `rdata_adffe.dot'.
Dumping selected parts of module fifo to page 1.
yosys> wreduce
19. Executing WREDUCE pass (reducing word size of cells).
Removed top 31 bits (of 32) from port B of cell fifo.$add$fifo.v:66$27 ($add).
Removed top 23 bits (of 32) from port Y of cell fifo.$add$fifo.v:66$27 ($add).
Removed top 31 bits (of 32) from port B of cell fifo.$sub$fifo.v:68$30 ($sub).
Removed top 23 bits (of 32) from port Y of cell fifo.$sub$fifo.v:68$30 ($sub).
Removed top 1 bits (of 2) from port B of cell fifo.$auto$opt_dff.cc:195:make_patterns_logic$66 ($ne).
Removed cell fifo.$flatten\fifo_writer.$procmux$53 ($mux).
Removed top 31 bits (of 32) from port B of cell fifo.$flatten\fifo_writer.$add$fifo.v:19$34 ($add).
Removed top 24 bits (of 32) from port Y of cell fifo.$flatten\fifo_writer.$add$fifo.v:19$34 ($add).
Removed cell fifo.$flatten\fifo_reader.$procmux$53 ($mux).
Removed top 31 bits (of 32) from port B of cell fifo.$flatten\fifo_reader.$add$fifo.v:19$34 ($add).
Removed top 24 bits (of 32) from port Y of cell fifo.$flatten\fifo_reader.$add$fifo.v:19$34 ($add).
Removed top 23 bits (of 32) from wire fifo.$add$fifo.v:66$27_Y.
Removed top 24 bits (of 32) from wire fifo.$flatten\fifo_reader.$add$fifo.v:19$34_Y.
yosys> show -notitle -format dot -prefix rdata_wreduce o:rdata %ci*
20. Generating Graphviz representation of design.
Writing dot description to `rdata_wreduce.dot'.
Dumping selected parts of module fifo to page 1.
yosys> opt_clean
21. Executing OPT_CLEAN pass (remove unused cells and wires).
Finding unused cells or wires in module \fifo..
Removed 0 unused cells and 4 unused wires.
<suppressed ~1 debug messages>
yosys> memory_dff
22. Executing MEMORY_DFF pass (merging $dff cells to $memrd).
Checking read port `\data'[0] in module `\fifo': merging output FF to cell.
Write port 0: non-transparent.
yosys> select -set new_cells t:$memrd_v2
yosys> show -color maroon3 @new_cells -notitle -format dot -prefix rdata_memrdv2 o:rdata %ci*
23. Generating Graphviz representation of design.
Writing dot description to `rdata_memrdv2.dot'.
Dumping selected parts of module fifo to page 1.
yosys> alumacc
24. Executing ALUMACC pass (create $alu and $macc cells).
Extracting $alu and $macc cells in module fifo:
creating $macc model for $add$fifo.v:66$27 ($add).
creating $macc model for $flatten\fifo_reader.$add$fifo.v:19$34 ($add).
creating $macc model for $flatten\fifo_writer.$add$fifo.v:19$34 ($add).
creating $macc model for $sub$fifo.v:68$30 ($sub).
creating $alu model for $macc $sub$fifo.v:68$30.
creating $alu model for $macc $flatten\fifo_writer.$add$fifo.v:19$34.
creating $alu model for $macc $flatten\fifo_reader.$add$fifo.v:19$34.
creating $alu model for $macc $add$fifo.v:66$27.
creating $alu cell for $add$fifo.v:66$27: $auto$alumacc.cc:485:replace_alu$80
creating $alu cell for $flatten\fifo_reader.$add$fifo.v:19$34: $auto$alumacc.cc:485:replace_alu$83
creating $alu cell for $flatten\fifo_writer.$add$fifo.v:19$34: $auto$alumacc.cc:485:replace_alu$86
creating $alu cell for $sub$fifo.v:68$30: $auto$alumacc.cc:485:replace_alu$89
created 4 $alu and 0 $macc cells.
yosys> select -set new_cells t:$alu t:$macc
yosys> show -color maroon3 @new_cells -notitle -format dot -prefix rdata_alumacc o:rdata %ci*
25. Generating Graphviz representation of design.
Writing dot description to `rdata_alumacc.dot'.
Dumping selected parts of module fifo to page 1.
yosys> memory_collect
26. Executing MEMORY_COLLECT pass (generating $mem cells).
yosys> select -set new_cells t:$mem_v2
yosys> select -set rdata_path @new_cells %ci*:-$mem_v2[WR_DATA,WR_ADDR,WR_EN] @new_cells %co* %%
yosys> show -color maroon3 @new_cells -notitle -format dot -prefix rdata_coarse @rdata_path
27. Generating Graphviz representation of design.
Writing dot description to `rdata_coarse.dot'.
Dumping selected parts of module fifo to page 1.

57
docs/source/code_examples/fifo/fifo.stat Normal file
View File

@ -0,0 +1,57 @@
yosys> stat
2. Printing statistics.
=== fifo ===
Number of wires: 28
Number of wire bits: 219
Number of public wires: 9
Number of public wire bits: 45
Number of memories: 1
Number of memory bits: 2048
Number of processes: 3
Number of cells: 9
$add 1
$logic_and 2
$logic_not 2
$memrd 1
$sub 1
addr_gen 2
=== addr_gen ===
Number of wires: 8
Number of wire bits: 60
Number of public wires: 4
Number of public wire bits: 11
Number of memories: 0
Number of memory bits: 0
Number of processes: 2
Number of cells: 2
$add 1
$eq 1
yosys> stat -top fifo
17. Printing statistics.
=== fifo ===
Number of wires: 94
Number of wire bits: 260
Number of public wires: 94
Number of public wire bits: 260
Number of memories: 0
Number of memory bits: 0
Number of processes: 0
Number of cells: 138
$scopeinfo 2
SB_CARRY 26
SB_DFF 26
SB_DFFER 25
SB_LUT4 58
SB_RAM40_4K 1

71
docs/source/code_examples/fifo/fifo.v Normal file
View File

@ -0,0 +1,71 @@
// address generator/counter
module addr_gen
#( parameter MAX_DATA=256,
localparam AWIDTH = $clog2(MAX_DATA)
) ( input en, clk, rst,
output reg [AWIDTH-1:0] addr
);
initial addr <= 0;
// async reset
// increment address when enabled
always @(posedge clk or posedge rst)
if (rst)
addr <= 0;
else if (en) begin
if (addr == MAX_DATA-1)
addr <= 0;
else
addr <= addr + 1;
end
endmodule //addr_gen
// Define our top level fifo entity
module fifo
#( parameter MAX_DATA=256,
localparam AWIDTH = $clog2(MAX_DATA)
) ( input wen, ren, clk, rst,
input [7:0] wdata,
output reg [7:0] rdata,
output reg [AWIDTH:0] count
);
// fifo storage
// sync read before write
wire [AWIDTH-1:0] waddr, raddr;
reg [7:0] data [MAX_DATA-1:0];
always @(posedge clk) begin
if (wen)
data[waddr] <= wdata;
rdata <= data[raddr];
end // storage
// addr_gen for both write and read addresses
addr_gen #(.MAX_DATA(MAX_DATA))
fifo_writer (
.en (wen),
.clk (clk),
.rst (rst),
.addr (waddr)
);
addr_gen #(.MAX_DATA(MAX_DATA))
fifo_reader (
.en (ren),
.clk (clk),
.rst (rst),
.addr (raddr)
);
// status signals
initial count <= 0;
always @(posedge clk or posedge rst) begin
if (rst)
count <= 0;
else if (wen && !ren)
count <= count + 1;
else if (ren && !wen)
count <= count - 1;
end
endmodule

82
docs/source/code_examples/fifo/fifo.ys Normal file
View File

@ -0,0 +1,82 @@
# ========================================================
# throw in some extra text to match what we expect if we were opening an
# interactive terminal
log $ yosys fifo.v
log
log -- Parsing `fifo.v' using frontend ` -vlog2k' --
read_verilog -defer fifo.v
# turn command echoes on to use the log output as a console session
echo on
hierarchy -top addr_gen
select -module addr_gen
select -list
select t:*
select -list
select -set new_cells %
select -clear
show -format dot -prefix addr_gen_show addr_gen
show -format dot -prefix new_cells_show -notitle @new_cells
show -color maroon3 @new_cells -color cornflowerblue p:* -notitle -format dot -prefix addr_gen_hier
# ========================================================
proc -noopt
select -set new_cells t:$mux t:*dff
show -color maroon3 @new_cells -notitle -format dot -prefix addr_gen_proc
# ========================================================
opt_expr; clean
select -set new_cells t:$eq
show -color cornflowerblue @new_cells -notitle -format dot -prefix addr_gen_clean
# ========================================================
design -reset
read_verilog fifo.v
hierarchy -check -top fifo
proc
select -set new_cells t:$memrd
show -color maroon3 c:fifo_reader -color cornflowerblue @new_cells -notitle -format dot -prefix rdata_proc o:rdata %ci*
# ========================================================
flatten;;
select -set rdata_path o:rdata %ci*
select -set new_cells @rdata_path o:rdata %ci3 %d i:* %d
show -color maroon3 @new_cells -notitle -format dot -prefix rdata_flat @rdata_path
# ========================================================
opt_dff
select -set new_cells t:$adffe
show -color maroon3 @new_cells -notitle -format dot -prefix rdata_adffe o:rdata %ci*
# ========================================================
wreduce
show -notitle -format dot -prefix rdata_wreduce o:rdata %ci*
# unclear if this is necessary or only because of bug(s)
opt_clean
# ========================================================
memory_dff
select -set new_cells t:$memrd_v2
show -color maroon3 @new_cells -notitle -format dot -prefix rdata_memrdv2 o:rdata %ci*
# ========================================================
alumacc
select -set new_cells t:$alu t:$macc
show -color maroon3 @new_cells -notitle -format dot -prefix rdata_alumacc o:rdata %ci*
# ========================================================
memory_collect
# or use the following commands:
# design -reset
# read_verilog fifo.v
# synth_ice40 -top fifo -run begin:map_ram
select -set new_cells t:$mem_v2
select -set rdata_path @new_cells %ci*:-$mem_v2[WR_DATA,WR_ADDR,WR_EN] @new_cells %co* %%
show -color maroon3 @new_cells -notitle -format dot -prefix rdata_coarse @rdata_path

57
docs/source/code_examples/fifo/fifo_map.ys Normal file
View File

@ -0,0 +1,57 @@
read_verilog fifo.v
echo on
tee -o fifo.stat stat
echo off
synth_ice40 -top fifo -run begin:map_ram
# this point should be the same as rdata_coarse
# ========================================================
echo on
tee -o fifo.libmap debug memory_libmap -lib +/ice40/brams.txt -lib +/ice40/spram.txt -no-auto-huge
echo off
synth_ice40 -top fifo -run map_ram:map_ffram
select -set mem t:SB_RAM40_4K
select -set remap @mem %ci:+SB_RAM40_4K[RADDR] @mem %co %%
select -set rdata_path t:SB_RAM40_4K %ci*:-SB_RAM40_4K[WCLKE,WDATA,WADDR,WE] t:SB_RAM40_4K %co* %%
show -color cornflowerblue @remap -notitle -format dot -prefix rdata_map_ram @rdata_path
# ========================================================
synth_ice40 -top fifo -run map_ffram:map_gates
select -set mem t:SB_RAM40_4K
select -set remap @mem %co @mem %d
select -set rdata_path t:SB_RAM40_4K %ci*:-SB_RAM40_4K[WCLKE,WDATA,WADDR,WE] t:SB_RAM40_4K %co* %%
show -color maroon3 @mem -color cornflowerblue @remap -notitle -format dot -prefix rdata_map_ffram @rdata_path
# ========================================================
synth_ice40 -top fifo -run map_gates:map_ffs
select -set rdata_path t:SB_RAM40_4K %ci*:-SB_RAM40_4K[WCLKE,WDATA,WADDR,WE] t:SB_RAM40_4K %co* %%
select -set multibit t:$_MUX_ t:$_DFFE_*_
select -set alu t:$_OR_ t:$_NOT_ t:$lut %% %ci %% w:fifo_reader.addr %d i:* %d
show -color maroon3 @multibit -color cornflowerblue @alu -notitle -format dot -prefix rdata_map_gates @rdata_path
# ========================================================
synth_ice40 -top fifo -run map_ffs:map_luts
select -set rdata_path t:SB_RAM40_4K %ci*:-SB_RAM40_4K[WCLKE,WDATA,WADDR,WE] t:SB_RAM40_4K %co* %%
select -set dff t:SB_DFFER
select -set primitives t:$_AND_ %ci i:* %d
show -color maroon3 @dff -color cornflowerblue @primitives -notitle -format dot -prefix rdata_map_ffs @rdata_path
# ========================================================
synth_ice40 -top fifo -run map_luts:map_cells
select -set rdata_path t:SB_RAM40_4K %ci*:-SB_RAM40_4K[WCLKE,WDATA,WADDR,WE] t:SB_RAM40_4K %co* %%
show -color maroon3 t:SB_CARRY -color cornflowerblue t:$lut -notitle -format dot -prefix rdata_map_luts @rdata_path
# ========================================================
synth_ice40 -top fifo -run map_cells:
select -set rdata_path t:SB_RAM40_4K %ci*:-SB_RAM40_4K[WCLKE,WDATA,WADDR,WE] t:SB_RAM40_4K %co* %%
show -color maroon3 t:SB_LUT* -notitle -format dot -prefix rdata_map_cells @rdata_path
echo on
tee -a fifo.stat stat -top fifo
echo off

1
docs/source/code_examples/intro/.gitignore vendored Normal file
View File

@ -0,0 +1 @@
synth.v

15
docs/source/code_examples/intro/Makefile Normal file
View File

@ -0,0 +1,15 @@
PROGRAM_PREFIX :=
YOSYS ?= ../../../../$(PROGRAM_PREFIX)yosys
DOTS = counter_00.dot counter_01.dot counter_02.dot counter_03.dot
all: dots
dots: $(DOTS)
$(DOTS): counter.v counter.ys mycells.lib
$(YOSYS) counter.ys
.PHONY: clean
clean:
rm -f *.dot

0
manual/PRESENTATION_Intro/counter.v → docs/source/code_examples/intro/counter.v
View File

31
docs/source/code_examples/intro/counter.ys Normal file
View File

@ -0,0 +1,31 @@
# read design
read_verilog counter.v
hierarchy -check -top counter
show -notitle -format dot -prefix counter_00
# the high-level stuff
proc; opt
memory; opt
fsm; opt
show -notitle -format dot -prefix counter_01
# mapping to internal cell library
techmap; opt
splitnets -ports;; show -notitle -format dot -prefix counter_02
# mapping flip-flops to mycells.lib
dfflibmap -liberty mycells.lib
# mapping logic to mycells.lib
abc -liberty mycells.lib
# cleanup
clean
show -notitle -lib mycells.v -format dot -prefix counter_03
# write synthesized design
write_verilog synth.v

0
manual/PRESENTATION_Intro/mycells.lib → docs/source/code_examples/intro/mycells.lib
View File

Some files were not shown because too many files have changed in this diff Show More