210 lines
13 KiB
TeX
210 lines
13 KiB
TeX
|
|
||
|
|
\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.
|
||
|
|
|