\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.