Added Yosys Manual

1 files changed, 209 insertions, 0 deletions

diff --git a/manual/CHAPTER_Eval.tex b/manual/CHAPTER_Eval.tex
new file mode 100644
index 00000000..c27a000b
--- /dev/null
+++ b/manual/CHAPTER_Eval.tex
@@ -0,0 +1,209 @@
+
+\chapter{Evaluation, Conclusion, Future Work}
+\label{chapter:eval}
+
+The Yosys source tree contains over 200 test cases\footnote{Most of this test
+cases are copied from HANA \citeweblink{HANA} or the ASIC-WORLD website
+\citeweblink{ASIC-WORLD}.} which are used in the {\tt make test} make-target.
+Besides these there is an external Yosys benchmark and test case package that
+contains a few larger designs \citeweblink{YosysTestsGit}. This package
+contains the designs listed in Tab.~\ref{tab:yosys-test-designs}.
+
+\begin{table}
+	\hfil
+	\begin{tabular}{lrrp{8.5cm}}
+		Test-Design & Source & Gates\footnotemark & Description / Comments \\
+		\hline
+		{\tt aes\_core}   &  IWLS2005 & $ 41{,}837 $ & \footnotesize AES Cipher written by Rudolf Usselmann \\
+		{\tt i2c}         &  IWLS2005 & $  1{,}072 $ & \footnotesize WISHBONE compliant I2C Master by Richard Herveille \\
+		{\tt openmsp430}  & OpenCores & $  7{,}173 $ & \footnotesize MSP430 compatible CPU by Olivier Girard \\
+		{\tt or1200}      & OpenCores & $ 42{,}675 $ & \footnotesize The OpenRISC 1200 CPU by Damjan Lampret \\
+		{\tt sasc}        &  IWLS2005 & $      456 $ & \footnotesize Simple Async. Serial Comm. Device by Rudolf Usselmann \\
+		{\tt simple\_spi} &  IWLS2005 & $      690 $ & \footnotesize MC68HC11E based SPI interface by Richard Herveille \\
+		{\tt spi}         &  IWLS2005 & $  2{,}478 $ & \footnotesize SPI IP core by Simon Srot \\
+		{\tt ss\_pcm}     &  IWLS2005 & $      279 $ & \footnotesize PCM IO Slave by Rudolf Usselmann \\
+		{\tt systemcaes}  &  IWLS2005 & $  6{,}893 $ & \footnotesize AES core (using SystemC to Verilog) by Javier Castillo \\
+		{\tt usb\_phy}    &  IWLS2005 & $      515 $ & \footnotesize USB 1.1 PHY by Rudolf Usselmann \\
+	\end{tabular}
+	\caption{Tests included in the yosys-tests package.}
+	\label{tab:yosys-test-designs}
+\end{table}
+
+\footnotetext{
+Number of gates determined using the Yosys synthesis script ``{\tt hierarchy -top \$top; proc; opt; memory; opt; techmap; opt; abc; opt; flatten \$top; hierarchy -top \$top; abc; opt; select -count */c:*}''.
+}
+
+\section{Correctness of Synthesis Results}
+
+The following measures were taken to increase the confidence in the correctness of the Yosys synthesis results:
+
+\begin{itemize}
+\item Yosys comes with a large selection\footnote{At the time of this writing
+269 test cases.} of small test cases that are evaluated when the command {\tt
+make test} is executed. During development of Yosys it was shown that this
+collection of test cases is sufficient to catch most bugs. The following more
+sophisticated test procedures only caught a few additional bugs. Whenever this
+happend, an appropiate test case was added to the collection of small test
+cases for {\tt make test} to ensure better testability of the feature in
+question in the future.
+
+\item The designs listed in Tab.~\ref{tab:yosys-test-designs} where validated
+using the formal verification tool Synopsys Formality\citeweblink{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 {\tt 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.~\ref{tab:yosys-test-designs}
+validate successfully using Formality.
+
+\item VlogHammer \citeweblink{VlogHammer} is a set of scripts that
+auto-generate a large collection of test cases\footnote{At the time of this
+writing over 6600 test cases.} and synthesize them using Yosys and the
+following freely available propritary synthesis tools.
+\begin{itemize}
+\item Xilinx Vivado WebPack (2013.2) \citeweblink{XilinxWebPACK}
+\item Xilinx ISE (XST) WebPack (14.5) \citeweblink{XilinxWebPACK}
+\item Altera Quartus II Web Edition (13.0) \citeweblink{QuartusWeb}
+\end{itemize}
+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.\footnote{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.~\ref{cmd:sat} for details.}
+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.
+\begin{itemize}
+\item Xilinx ISIM (from Xilinx ISE 14.5 \citeweblink{XilinxWebPACK})
+\item Modelsim 10.1d (from Quartus II 13.0 \citeweblink{QuartusWeb})
+\item Icarus Verilog (no specific version)
+\end{itemize}
+The set of tests performed by VlogHammer systematically verify the correct
+behaviour of
+\begin{itemize}
+\item Yosys Verilog Frontend and RTL generation
+\item Yosys Gate-Level Technology Mapping
+\item Yosys SAT Models for RTL- and Gate-Level cells
+\item Yosys Constant Evaluator Models for RTL- and Gate-Level cells
+\end{itemize}
+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).
+\end{itemize}
+
+Although complex software can never be expected to be fully bug-free
+\cite{MURPHY}, it has been shown that Yosys is mature and feature-complete
+enough to handle most real-world cases correctly.
+
+\section{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:
+
+\begin{lstlisting}[numbers=left,frame=single,mathescape]
+hierarchy -check
+proc; opt; fsm; opt; memory; opt
+techmap; opt; abc; opt
+\end{lstlisting}
+
+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:
+
+\begin{lstlisting}[numbers=left,frame=single,mathescape]
+-p artix7
+-use_dsp48 NO
+-iobuf NO
+-ram_extract NO
+-rom_extract NO
+-fsm_extract YES
+-fsm_encoding Auto
+\end{lstlisting}
+
+The results of this comparison is summarized in Tab.~\ref{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.
+
+\begin{table}
+	\def\nomhz{--- \phantom{MHz}}
+	\def\P#1 {(#1\hbox to 0px{)\hss}}
+	\hfil
+	\begin{tabular}{l|rrr|rrr}
+		& \multicolumn{3}{c|}{Without Yosys} & \multicolumn{3}{c}{With Yosys} \\
+		Module & Regs & LUTs & Max. Freq. & Regs & LUTs & Max. Freq. \\
+		\hline
+		{\tt openMSP430}                                    &    689 &   2210 &   71 MHz &    719 &   2779 &   53 MHz \\
+		{\tt \hskip1em omsp\_clock\_module}                 &     21 &     30 &  645 MHz &     21 &     30 &  644 MHz \\
+		{\tt \hskip1em \hskip1em omsp\_sync\_cell}          &      2 &    --- & 1542 MHz &      2 &    --- & 1542 MHz \\
+		{\tt \hskip1em \hskip1em omsp\_sync\_reset}         &      2 &    --- & 1542 MHz &      2 &    --- & 1542 MHz \\
+		{\tt \hskip1em omsp\_dbg}                           &    143 &    344 &  292 MHz &    149 &    430 &  353 MHz \\
+		{\tt \hskip1em \hskip1em omsp\_dbg\_uart}           &     76 &    135 &  377 MHz &     79 &    139 &  389 MHz \\
+		{\tt \hskip1em omsp\_execution\_unit}               &    266 &    911 &   80 MHz &    266 &   1034 &  137 MHz \\
+		{\tt \hskip1em \hskip1em omsp\_alu}                 &    --- &    202 &   \nomhz &    --- &    263 &   \nomhz \\
+		{\tt \hskip1em \hskip1em omsp\_register\_file}      &    231 &    478 &  285 MHz &    231 &    506 &  293 MHz \\
+		{\tt \hskip1em omsp\_frontend}                      &    115 &    340 &  178 MHz &    118 &    527 &  206 MHz \\
+		{\tt \hskip1em omsp\_mem\_backbone}                 &     38 &    141 & 1087 MHz &     38 &    144 & 1087 MHz \\
+		{\tt \hskip1em omsp\_multiplier}                    &     73 &    397 &  129 MHz &    102 &   1053 &   55 MHz \\
+		{\tt \hskip1em omsp\_sfr}                           &      6 &     18 & 1023 MHz &      6 &     20 & 1023 MHz \\
+		{\tt \hskip1em omsp\_watchdog}                      &     24 &     53 &  362 MHz &     24 &     70 &  360 MHz \\
+		\hline
+		{\tt or1200\_top}                                   &   7148 &   9969 &  135 MHz &   7173 &  10238 &  108 MHz \\
+		{\tt \hskip1em or1200\_alu}                         &    --- &    681 &   \nomhz &    --- &    641 &   \nomhz \\
+		{\tt \hskip1em or1200\_cfgr}                        &    --- &     11 &   \nomhz &    --- &     11 &   \nomhz \\
+		{\tt \hskip1em or1200\_ctrl}                        &    175 &    186 &  464 MHz &    174 &    279 &  377 MHz \\
+		{\tt \hskip1em or1200\_except}                      &    241 &    451 &  313 MHz &    241 &    353 &  301 MHz \\
+		{\tt \hskip1em or1200\_freeze}                      &      6 &     18 &  507 MHz &      6 &     16 &  515 MHz \\
+		{\tt \hskip1em or1200\_if}                          &     68 &    143 &  806 MHz &     68 &    139 &  790 MHz \\
+		{\tt \hskip1em or1200\_lsu}                         &      8 &    138 &   \nomhz &     12 &    205 & 1306 MHz \\
+		{\tt \hskip1em \hskip1em or1200\_mem2reg}           &    --- &     60 &   \nomhz &    --- &     66 &   \nomhz \\
+		{\tt \hskip1em \hskip1em or1200\_reg2mem}           &    --- &     29 &   \nomhz &    --- &     29 &   \nomhz \\
+		{\tt \hskip1em or1200\_mult\_mac}                   &    394 &   2209 &  240 MHz &    394 &   2230 &  241 MHz \\
+		{\tt \hskip1em \hskip1em or1200\_amultp2\_32x32}    &    256 &   1783 &  240 MHz &    256 &   1770 &  241 MHz \\
+		{\tt \hskip1em or1200\_operandmuxes}                &     65 &    129 & 1145 MHz &     65 &    129 & 1145 MHz \\
+		{\tt \hskip1em or1200\_rf}                          &   1041 &   1722 &  822 MHz &   1042 &   1722 &  581 MHz \\
+		{\tt \hskip1em or1200\_sprs}                        &     18 &    432 &  724 MHz &     18 &    469 &  722 MHz \\
+		{\tt \hskip1em or1200\_wbmux}                       &     33 &     93 &   \nomhz &     33 &     78 &   \nomhz \\
+		{\tt \hskip1em or1200\_dc\_top}                     &    --- &      5 &   \nomhz &    --- &      5 &   \nomhz \\
+		{\tt \hskip1em or1200\_dmmu\_top}                   &   2445 &   1004 &   \nomhz &   2445 &   1043 &   \nomhz \\
+		{\tt \hskip1em \hskip1em or1200\_dmmu\_tlb}         &   2444 &    975 &   \nomhz &   2444 &   1013 &   \nomhz \\
+		{\tt \hskip1em or1200\_du}                          &     67 &     56 &  859 MHz &     67 &     56 &  859 MHz \\
+		{\tt \hskip1em or1200\_ic\_top}                     &     39 &    100 &  527 MHz &     41 &    136 &  514 MHz \\
+		{\tt \hskip1em \hskip1em or1200\_ic\_fsm}           &     40 &     42 &  408 MHz &     40 &     75 &  484 MHz \\
+		{\tt \hskip1em or1200\_pic}                         &     38 &     50 & 1169 MHz &     38 &     50 & 1177 MHz \\
+		{\tt \hskip1em or1200\_tt}                          &     64 &    112 &  370 MHz &     64 &    186 &  437 MHz \\
+	\end{tabular}
+	\caption{Synthesis results (as reported by XST) for OpenMSP430 and OpenRISC 1200}
+	\label{tab:synth-test}
+\end{table}
+
+\section{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 {\tt 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.
+