manual/CHAPTER_Eval.tex

   1
   2 \chapter{Evaluation, Conclusion, Future Work}
   3 \label{chapter:eval}
   4
   5 The Yosys source tree contains over 200 test cases\footnote{Most of this test
   6 cases are copied from HANA \citeweblink{HANA} or the ASIC-WORLD website
   7 \citeweblink{ASIC-WORLD}.} which are used in the {\tt make test} make-target.
   8 Besides these there is an external Yosys benchmark and test case package that
   9 contains a few larger designs \citeweblink{YosysTestsGit}. This package
  10 contains the designs listed in Tab.~\ref{tab:yosys-test-designs}.
  11
  12 \begin{table}
  13         \hfil
  14         \begin{tabular}{lrrp{8.5cm}}
  15                 Test-Design & Source & Gates\footnotemark & Description / Comments \\
  16                 \hline
  17                 {\tt aes\_core}   &  IWLS2005 & $ 41{,}837 $ & \footnotesize AES Cipher written by Rudolf Usselmann \\
  18                 {\tt i2c}         &  IWLS2005 & $  1{,}072 $ & \footnotesize WISHBONE compliant I2C Master by Richard Herveille \\
  19                 {\tt openmsp430}  & OpenCores & $  7{,}173 $ & \footnotesize MSP430 compatible CPU by Olivier Girard \\
  20                 {\tt or1200}      & OpenCores & $ 42{,}675 $ & \footnotesize The OpenRISC 1200 CPU by Damjan Lampret \\
  21                 {\tt sasc}        &  IWLS2005 & $      456 $ & \footnotesize Simple Async. Serial Comm. Device by Rudolf Usselmann \\
  22                 {\tt simple\_spi} &  IWLS2005 & $      690 $ & \footnotesize MC68HC11E based SPI interface by Richard Herveille \\
  23                 {\tt spi}         &  IWLS2005 & $  2{,}478 $ & \footnotesize SPI IP core by Simon Srot \\
  24                 {\tt ss\_pcm}     &  IWLS2005 & $      279 $ & \footnotesize PCM IO Slave by Rudolf Usselmann \\
  25                 {\tt systemcaes}  &  IWLS2005 & $  6{,}893 $ & \footnotesize AES core (using SystemC to Verilog) by Javier Castillo \\
  26                 {\tt usb\_phy}    &  IWLS2005 & $      515 $ & \footnotesize USB 1.1 PHY by Rudolf Usselmann \\
  27         \end{tabular}
  28         \caption{Tests included in the yosys-tests package.}
  29         \label{tab:yosys-test-designs}
  30 \end{table}
  31
  32 \footnotetext{
  33 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:*}''.
  34 }
  35
  36 \section{Correctness of Synthesis Results}
  37
  38 The following measures were taken to increase the confidence in the correctness of the Yosys synthesis results:
  39
  40 \begin{itemize}
  41 \item Yosys comes with a large selection\footnote{At the time of this writing
  42 269 test cases.} of small test cases that are evaluated when the command {\tt
  43 make test} is executed. During development of Yosys it was shown that this
  44 collection of test cases is sufficient to catch most bugs. The following more
  45 sophisticated test procedures only caught a few additional bugs. Whenever this
  46 happened, an appropriate test case was added to the collection of small test
  47 cases for {\tt make test} to ensure better testability of the feature in
  48 question in the future.
  49
  50 \item The designs listed in Tab.~\ref{tab:yosys-test-designs} where validated
  51 using the formal verification tool Synopsys Formality\citeweblink{Formality}.
  52 The Yosys synthesis scripts used to synthesize the individual designs for this
  53 test are slightly different per design in order to broaden the coverage of
  54 Yosys features. The large majority of all errors encountered using these tests
  55 are false-negatives, mostly related to FSM encoding or signal naming in large
  56 array logic (such as in memory blocks). Therefore the {\tt fsm\_recode} pass
  57 was extended so it can be used to generate TCL commands for Synopsys Formality
  58 that describe the relationship between old and new state encodings. Also the
  59 method used to generate signal and cell names in the Verilog backend was
  60 slightly modified in order to improve the automatic matching of net names in
  61 Synopsys Formality. With these changes in place all designs in Tab.~\ref{tab:yosys-test-designs}
  62 validate successfully using Formality.
  63
  64 \item VlogHammer \citeweblink{VlogHammer} is a set of scripts that
  65 auto-generate a large collection of test cases\footnote{At the time of this
  66 writing over 6600 test cases.} and synthesize them using Yosys and the
  67 following freely available proprietary synthesis tools.
  68 \begin{itemize}
  69 \item Xilinx Vivado WebPack (2013.2) \citeweblink{XilinxWebPACK}
  70 \item Xilinx ISE (XST) WebPack (14.5) \citeweblink{XilinxWebPACK}
  71 \item Altera Quartus II Web Edition (13.0) \citeweblink{QuartusWeb}
  72 \end{itemize}
  73 The built-in SAT solver of Yosys is used to formally
  74 verify the Yosys RTL- and Gate-Level netlists against the netlists generated by
  75 this other tools.\footnote{A SAT solver is a program that can solve the boolean
  76 satisfiability problem. The built-in SAT solver in Yosys can be used for formal
  77 equivalence checking, amongst other things. See Sec.~\ref{cmd:sat} for details.}
  78 When differences are found, the input pattern that result in
  79 different outputs are used for simulating the original Verilog code as well as
  80 the synthesis results using the following Verilog simulators.
  81 \begin{itemize}
  82 \item Xilinx ISIM (from Xilinx ISE 14.5 \citeweblink{XilinxWebPACK})
  83 \item Modelsim 10.1d (from Quartus II 13.0 \citeweblink{QuartusWeb})
  84 \item Icarus Verilog (no specific version)
  85 \end{itemize}
  86 The set of tests performed by VlogHammer systematically verify the correct
  87 behaviour of
  88 \begin{itemize}
  89 \item Yosys Verilog Frontend and RTL generation
  90 \item Yosys Gate-Level Technology Mapping
  91 \item Yosys SAT Models for RTL- and Gate-Level cells
  92 \item Yosys Constant Evaluator Models for RTL- and Gate-Level cells
  93 \end{itemize}
  94 against the reference provided by the other tools. A few bugs related to sign
  95 extensions and bit-width extensions where found (and have been fixed meanwhile)
  96 using this approach. This test also revealed a small number of bugs in the
  97 other tools (i.e.~Vivado, XST, Quartus, ISIM and Icarus Verilog; no bugs where
  98 found in Modelsim using vlogHammer so far).
  99 \end{itemize}
 100
 101 Although complex software can never be expected to be fully bug-free
 102 \cite{MURPHY}, it has been shown that Yosys is mature and feature-complete
 103 enough to handle most real-world cases correctly.
 104
 105 \section{Quality of synthesis results}
 106
 107 In this section an attempt to evaluate the quality of Yosys synthesis results is made. To this end the
 108 synthesis results of a commercial FPGA synthesis tool when presented with the original HDL code vs.~when
 109 presented with the Yosys synthesis result are compared.
 110
 111 The OpenMSP430 and the OpenRISC 1200 test cases were synthesized using the following Yosys synthesis script:
 112
 113 \begin{lstlisting}[numbers=left,frame=single,mathescape]
 114 hierarchy -check
 115 proc; opt; fsm; opt; memory; opt
 116 techmap; opt; abc; opt
 117 \end{lstlisting}
 118
 119 The original RTL and the Yosys output where both passed to the Xilinx XST 14.5
 120 FPGA synthesis tool. The following setting where used for XST:
 121
 122 \begin{lstlisting}[numbers=left,frame=single,mathescape]
 123 -p artix7
 124 -use_dsp48 NO
 125 -iobuf NO
 126 -ram_extract NO
 127 -rom_extract NO
 128 -fsm_extract YES
 129 -fsm_encoding Auto
 130 \end{lstlisting}
 131
 132 The results of this comparison is summarized in Tab.~\ref{tab:synth-test}. The
 133 used FPGA resources (registers and LUTs) and performance (maximum frequency as
 134 reported by XST) are given per module (indentation indicates module hierarchy,
 135 the numbers are including all contained modules).
 136
 137 For most modules the results are very similar between XST and Yosys. XST is
 138 used in both cases for the final mapping of logic to LUTs. So this comparison
 139 only compares the high-level synthesis functions (such as FSM extraction and
 140 encoding) of Yosys and XST.
 141
 142 \begin{table}
 143         \def\nomhz{--- \phantom{MHz}}
 144         \def\P#1 {(#1\hbox to 0px{)\hss}}
 145         \hfil
 146         \begin{tabular}{l|rrr|rrr}
 147                 & \multicolumn{3}{c|}{Without Yosys} & \multicolumn{3}{c}{With Yosys} \\
 148                 Module & Regs & LUTs & Max. Freq. & Regs & LUTs & Max. Freq. \\
 149                 \hline
 150                 {\tt openMSP430}                                    &    689 &   2210 &   71 MHz &    719 &   2779 &   53 MHz \\
 151                 {\tt \hskip1em omsp\_clock\_module}                 &     21 &     30 &  645 MHz &     21 &     30 &  644 MHz \\
 152                 {\tt \hskip1em \hskip1em omsp\_sync\_cell}          &      2 &    --- & 1542 MHz &      2 &    --- & 1542 MHz \\
 153                 {\tt \hskip1em \hskip1em omsp\_sync\_reset}         &      2 &    --- & 1542 MHz &      2 &    --- & 1542 MHz \\
 154                 {\tt \hskip1em omsp\_dbg}                           &    143 &    344 &  292 MHz &    149 &    430 &  353 MHz \\
 155                 {\tt \hskip1em \hskip1em omsp\_dbg\_uart}           &     76 &    135 &  377 MHz &     79 &    139 &  389 MHz \\
 156                 {\tt \hskip1em omsp\_execution\_unit}               &    266 &    911 &   80 MHz &    266 &   1034 &  137 MHz \\
 157                 {\tt \hskip1em \hskip1em omsp\_alu}                 &    --- &    202 &   \nomhz &    --- &    263 &   \nomhz \\
 158                 {\tt \hskip1em \hskip1em omsp\_register\_file}      &    231 &    478 &  285 MHz &    231 &    506 &  293 MHz \\
 159                 {\tt \hskip1em omsp\_frontend}                      &    115 &    340 &  178 MHz &    118 &    527 &  206 MHz \\
 160                 {\tt \hskip1em omsp\_mem\_backbone}                 &     38 &    141 & 1087 MHz &     38 &    144 & 1087 MHz \\
 161                 {\tt \hskip1em omsp\_multiplier}                    &     73 &    397 &  129 MHz &    102 &   1053 &   55 MHz \\
 162                 {\tt \hskip1em omsp\_sfr}                           &      6 &     18 & 1023 MHz &      6 &     20 & 1023 MHz \\
 163                 {\tt \hskip1em omsp\_watchdog}                      &     24 &     53 &  362 MHz &     24 &     70 &  360 MHz \\
 164                 \hline
 165                 {\tt or1200\_top}                                   &   7148 &   9969 &  135 MHz &   7173 &  10238 &  108 MHz \\
 166                 {\tt \hskip1em or1200\_alu}                         &    --- &    681 &   \nomhz &    --- &    641 &   \nomhz \\
 167                 {\tt \hskip1em or1200\_cfgr}                        &    --- &     11 &   \nomhz &    --- &     11 &   \nomhz \\
 168                 {\tt \hskip1em or1200\_ctrl}                        &    175 &    186 &  464 MHz &    174 &    279 &  377 MHz \\
 169                 {\tt \hskip1em or1200\_except}                      &    241 &    451 &  313 MHz &    241 &    353 &  301 MHz \\
 170                 {\tt \hskip1em or1200\_freeze}                      &      6 &     18 &  507 MHz &      6 &     16 &  515 MHz \\
 171                 {\tt \hskip1em or1200\_if}                          &     68 &    143 &  806 MHz &     68 &    139 &  790 MHz \\
 172                 {\tt \hskip1em or1200\_lsu}                         &      8 &    138 &   \nomhz &     12 &    205 & 1306 MHz \\
 173                 {\tt \hskip1em \hskip1em or1200\_mem2reg}           &    --- &     60 &   \nomhz &    --- &     66 &   \nomhz \\
 174                 {\tt \hskip1em \hskip1em or1200\_reg2mem}           &    --- &     29 &   \nomhz &    --- &     29 &   \nomhz \\
 175                 {\tt \hskip1em or1200\_mult\_mac}                   &    394 &   2209 &  240 MHz &    394 &   2230 &  241 MHz \\
 176                 {\tt \hskip1em \hskip1em or1200\_amultp2\_32x32}    &    256 &   1783 &  240 MHz &    256 &   1770 &  241 MHz \\
 177                 {\tt \hskip1em or1200\_operandmuxes}                &     65 &    129 & 1145 MHz &     65 &    129 & 1145 MHz \\
 178                 {\tt \hskip1em or1200\_rf}                          &   1041 &   1722 &  822 MHz &   1042 &   1722 &  581 MHz \\
 179                 {\tt \hskip1em or1200\_sprs}                        &     18 &    432 &  724 MHz &     18 &    469 &  722 MHz \\
 180                 {\tt \hskip1em or1200\_wbmux}                       &     33 &     93 &   \nomhz &     33 &     78 &   \nomhz \\
 181                 {\tt \hskip1em or1200\_dc\_top}                     &    --- &      5 &   \nomhz &    --- &      5 &   \nomhz \\
 182                 {\tt \hskip1em or1200\_dmmu\_top}                   &   2445 &   1004 &   \nomhz &   2445 &   1043 &   \nomhz \\
 183                 {\tt \hskip1em \hskip1em or1200\_dmmu\_tlb}         &   2444 &    975 &   \nomhz &   2444 &   1013 &   \nomhz \\
 184                 {\tt \hskip1em or1200\_du}                          &     67 &     56 &  859 MHz &     67 &     56 &  859 MHz \\
 185                 {\tt \hskip1em or1200\_ic\_top}                     &     39 &    100 &  527 MHz &     41 &    136 &  514 MHz \\
 186                 {\tt \hskip1em \hskip1em or1200\_ic\_fsm}           &     40 &     42 &  408 MHz &     40 &     75 &  484 MHz \\
 187                 {\tt \hskip1em or1200\_pic}                         &     38 &     50 & 1169 MHz &     38 &     50 & 1177 MHz \\
 188                 {\tt \hskip1em or1200\_tt}                          &     64 &    112 &  370 MHz &     64 &    186 &  437 MHz \\
 189         \end{tabular}
 190         \caption{Synthesis results (as reported by XST) for OpenMSP430 and OpenRISC 1200}
 191         \label{tab:synth-test}
 192 \end{table}
 193
 194 \section{Conclusion and Future Work}
 195
 196 Yosys is capable of correctly synthesizing real-world Verilog designs. The
 197 generated netlists are of a decent quality. However, in cases where dedicated
 198 hardware resources should be used for certain functions it is of course
 199 necessary to implement proper technology mapping for these functions in
 200 Yosys. This can be as easy as calling the {\tt techmap} pass with an
 201 architecture-specific mapping file in the synthesis script. As no such thing
 202 has been done in the above tests, it is only natural that the resulting designs
 203 cannot benefit from these dedicated hardware resources.
 204
 205 Therefore future work includes the implementation of architecture-specific
 206 technology mappings besides additional frontends (VHDL), backends (EDIF),
 207 and above all else, application specific passes. After all, this was
 208 the main motivation for the development of Yosys in the first place.
 209