1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
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
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.
|
