Removing manual files

1 files changed, 0 insertions, 209 deletions

diff --git a/manual/CHAPTER_Eval.tex b/manual/CHAPTER_Eval.tex
deleted file mode 100644
index f719618d5..000000000
--- a/manual/CHAPTER_Eval.tex
+++ /dev/null
@@ -1,209 +0,0 @@
-
-\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
-happened, an appropriate 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 proprietary 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.
-