diff options
author | Clifford Wolf <clifford@clifford.at> | 2013-07-20 15:19:12 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2013-07-20 15:19:12 +0200 |
commit | 61ed6b32d1f5fbfda9c6effdaa678092f8156bfa (patch) | |
tree | 3a53692cbd93a09eabeb67eff5e9e4ace5cf1a3e /manual/CHAPTER_Eval.tex | |
parent | 3650fd7fbe45a00792770d9ecb9397bc27ea0845 (diff) | |
download | yosys-61ed6b32d1f5fbfda9c6effdaa678092f8156bfa.tar.gz yosys-61ed6b32d1f5fbfda9c6effdaa678092f8156bfa.tar.bz2 yosys-61ed6b32d1f5fbfda9c6effdaa678092f8156bfa.zip |
Added Yosys Manual
Diffstat (limited to 'manual/CHAPTER_Eval.tex')
-rw-r--r-- | manual/CHAPTER_Eval.tex | 209 |
1 files changed, 209 insertions, 0 deletions
diff --git a/manual/CHAPTER_Eval.tex b/manual/CHAPTER_Eval.tex new file mode 100644 index 000000000..c27a000bf --- /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. + |