mirror of https://github.com/YosysHQ/yosys.git
234 lines
11 KiB
ReStructuredText
234 lines
11 KiB
ReStructuredText
|
.. _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::
|