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
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
|
.. _chapter:eval:
Evaluation, conclusion, future Work
===================================
The Yosys source tree contains over 200 test cases [1]_ which are used
in the make test make-target. Besides these there is an external Yosys
benchmark and test case package that contains a few larger designs .
This package contains the designs listed in
Tab. \ `[tab:yosys-test-designs] <#tab:yosys-test-designs>`__.
.. table:: Tests included in the yosys-tests package.
=========== ========= ================
======================================================
Test-Design Source Gates Description / Comments
=========== ========= ================
======================================================
aes_core IWLS2005 :math:`41{,}837` AES Cipher written by Rudolf Usselmann
i2c IWLS2005 :math:`1{,}072` WISHBONE compliant I2C Master by Richard Herveille
openmsp430 OpenCores :math:`7{,}173` MSP430 compatible CPU by Olivier Girard
or1200 OpenCores :math:`42{,}675` The OpenRISC 1200 CPU by Damjan Lampret
sasc IWLS2005 :math:`456` Simple Async. Serial Comm. Device by Rudolf Usselmann
simple_spi IWLS2005 :math:`690` MC68HC11E based SPI interface by Richard Herveille
spi IWLS2005 :math:`2{,}478` SPI IP core by Simon Srot
ss_pcm IWLS2005 :math:`279` PCM IO Slave by Rudolf Usselmann
systemcaes IWLS2005 :math:`6{,}893` AES core (using SystemC to Verilog) by Javier Castillo
usb_phy IWLS2005 :math:`515` USB 1.1 PHY by Rudolf Usselmann
=========== ========= ================
======================================================
Correctness of synthesis results
--------------------------------
The following measures were taken to increase the confidence in the
correctness of the Yosys synthesis results:
- Yosys comes with a large selection [2]_ of small test cases that are
evaluated when the command 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 make test to ensure better testability of the feature in
question in the future.
- The designs listed in
Tab. \ `[tab:yosys-test-designs] <#tab:yosys-test-designs>`__ where
validated using the formal verification tool Synopsys 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 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. \ `[tab:yosys-test-designs] <#tab:yosys-test-designs>`__
validate successfully using Formality.
- VlogHammer is a set of scripts that auto-generate a large collection
of test cases [3]_ and synthesize them using Yosys and the following
freely available proprietary synthesis tools.
- Xilinx Vivado WebPack (2013.2)
- Xilinx ISE (XST) WebPack (14.5)
- Altera Quartus II Web Edition (13.0)
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. [4]_ 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.
- Xilinx ISIM (from Xilinx ISE 14.5 )
- Modelsim 10.1d (from Quartus II 13.0 )
- Icarus Verilog (no specific version)
The set of tests performed by VlogHammer systematically verify the
correct behaviour of
- Yosys Verilog Frontend and RTL generation
- Yosys Gate-Level Technology Mapping
- Yosys SAT Models for RTL- and Gate-Level cells
- Yosys Constant Evaluator Models for RTL- and Gate-Level cells
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).
Although complex software can never be expected to be fully bug-free
:cite:p:`MURPHY`, it has been shown that Yosys is mature and
feature-complete enough to handle most real-world cases correctly.
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:
::
hierarchy -check
proc; opt; fsm; opt; memory; opt
techmap; opt; abc; opt
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:
::
-p artix7
-use_dsp48 NO
-iobuf NO
-ram_extract NO
-rom_extract NO
-fsm_extract YES
-fsm_encoding Auto
The results of this comparison is summarized in
Tab. \ `[tab:synth-test] <#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.
.. table:: Synthesis results (as reported by XST) for OpenMSP430 and
OpenRISC 1200
============================ ==== ==== ========== ==== =====
==========
\
Module Regs LUTs Max. Freq. Regs LUTs Max. Freq.
openMSP430 689 2210 71 MHz 719 2779 53 MHz
1em omsp_clock_module 21 30 645 MHz 21 30 644 MHz
1em 1em omsp_sync_cell 2 — 1542 MHz 2 — 1542 MHz
1em 1em omsp_sync_reset 2 — 1542 MHz 2 — 1542 MHz
1em omsp_dbg 143 344 292 MHz 149 430 353 MHz
1em 1em omsp_dbg_uart 76 135 377 MHz 79 139 389 MHz
1em omsp_execution_unit 266 911 80 MHz 266 1034 137 MHz
1em 1em omsp_alu — 202 — — 263 —
1em 1em omsp_register_file 231 478 285 MHz 231 506 293 MHz
1em omsp_frontend 115 340 178 MHz 118 527 206 MHz
1em omsp_mem_backbone 38 141 1087 MHz 38 144 1087 MHz
1em omsp_multiplier 73 397 129 MHz 102 1053 55 MHz
1em omsp_sfr 6 18 1023 MHz 6 20 1023 MHz
1em omsp_watchdog 24 53 362 MHz 24 70 360 MHz
or1200_top 7148 9969 135 MHz 7173 10238 108 MHz
1em or1200_alu — 681 — — 641 —
1em or1200_cfgr — 11 — — 11 —
1em or1200_ctrl 175 186 464 MHz 174 279 377 MHz
1em or1200_except 241 451 313 MHz 241 353 301 MHz
1em or1200_freeze 6 18 507 MHz 6 16 515 MHz
1em or1200_if 68 143 806 MHz 68 139 790 MHz
1em or1200_lsu 8 138 — 12 205 1306 MHz
1em 1em or1200_mem2reg — 60 — — 66 —
1em 1em or1200_reg2mem — 29 — — 29 —
1em or1200_mult_mac 394 2209 240 MHz 394 2230 241 MHz
1em 1em or1200_amultp2_32x32 256 1783 240 MHz 256 1770 241 MHz
1em or1200_operandmuxes 65 129 1145 MHz 65 129 1145 MHz
1em or1200_rf 1041 1722 822 MHz 1042 1722 581 MHz
1em or1200_sprs 18 432 724 MHz 18 469 722 MHz
1em or1200_wbmux 33 93 — 33 78 —
1em or1200_dc_top — 5 — — 5 —
1em or1200_dmmu_top 2445 1004 — 2445 1043 —
1em 1em or1200_dmmu_tlb 2444 975 — 2444 1013 —
1em or1200_du 67 56 859 MHz 67 56 859 MHz
1em or1200_ic_top 39 100 527 MHz 41 136 514 MHz
1em 1em or1200_ic_fsm 40 42 408 MHz 40 75 484 MHz
1em or1200_pic 38 50 1169 MHz 38 50 1177 MHz
1em or1200_tt 64 112 370 MHz 64 186 437 MHz
============================ ==== ==== ========== ==== =====
==========
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 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.
.. [1]
Most of this test cases are copied from HANA or the ASIC-WORLD
website .
.. [2]
At the time of this writing 269 test cases.
.. [3]
At the time of this writing over 6600 test cases.
.. [4]
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. \ \ `[cmd:sat] <#cmd:sat>`__ for details.
.. footbibliography::
|
