Rst docs conversion (#3496)

Rst docs conversion

1 files changed, 233 insertions, 0 deletions

diff --git a/docs/source/CHAPTER_Eval.rst b/docs/source/CHAPTER_Eval.rst
new file mode 100644
index 000000000..3d463d3f9
--- /dev/null
+++ b/docs/source/CHAPTER_Eval.rst
@@ -0,0 +1,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::