.. _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::