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