Including Chapters (part.1)

docs/source/CHAPTER_Approach.rst

@@ -0,0 +1,146 @@
+.. _chapter:approach:
+
+Approach
+========
+
+Yosys is a tool for synthesising (behavioural) Verilog HDL code to
+target architecture netlists. Yosys aims at a wide range of application
+domains and thus must be flexible and easy to adapt to new tasks. This
+chapter covers the general approach followed in the effort to implement
+this tool.
+
+Data- and Control-Flow
+----------------------
+
+The data- and control-flow of a typical synthesis tool is very similar
+to the data- and control-flow of a typical compiler: different
+subsystems are called in a predetermined order, each consuming the data
+generated by the last subsystem and generating the data for the next
+subsystem (see :numref:`Fig. %s <fig:approach_flow>`).
+
+[fig:approach_flow]
+
+The first subsystem to be called is usually called a frontend. It does
+not process the data generated by another subsystem but instead reads
+the user input—in the case of a HDL synthesis tool, the behavioural HDL
+code.
+
+The subsystems that consume data from previous subsystems and produce
+data for the next subsystems (usually in the same or a similar format)
+are called passes.
+
+The last subsystem that is executed transforms the data generated by the
+last pass into a suitable output format and writes it to a disk file.
+This subsystem is usually called the backend.
+
+In Yosys all frontends, passes and backends are directly available as
+commands in the synthesis script. Thus the user can easily create a
+custom synthesis flow just by calling passes in the right order in a
+synthesis script.
+
+Internal Formats in Yosys
+-------------------------
+
+Yosys uses two different internal formats. The first is used to store an
+abstract syntax tree (AST) of a Verilog input file. This format is
+simply called AST and is generated by the Verilog Frontend. This data
+structure is consumed by a subsystem called AST Frontend [1]_. This AST
+Frontend then generates a design in Yosys' main internal format, the
+Register-Transfer-Level-Intermediate-Language (RTLIL) representation. It
+does that by first performing a number of simplifications within the AST
+representation and then generating RTLIL from the simplified AST data
+structure.
+
+The RTLIL representation is used by all passes as input and outputs.
+This has the following advantages over using different representational
+formats between different passes:
+
+-  The passes can be rearranged in a different order and passes can be
+   removed or inserted.
+
+-  Passes can simply pass-thru the parts of the design they don't change
+   without the need to convert between formats. In fact Yosys passes
+   output the same data structure they received as input and performs
+   all changes in place.
+
+-  All passes use the same interface, thus reducing the effort required
+   to understand a pass when reading the Yosys source code, e.g. when
+   adding additional features.
+
+The RTLIL representation is basically a netlist representation with the
+following additional features:
+
+-  An internal cell library with fixed-function cells to represent RTL
+   datapath and register cells as well as logical gate-level cells
+   (single-bit gates and registers).
+
+-  Support for multi-bit values that can use individual bits from wires
+   as well as constant bits to represent coarse-grain netlists.
+
+-  Support for basic behavioural constructs (if-then-else structures and
+   multi-case switches with a sensitivity list for updating the
+   outputs).
+
+-  Support for multi-port memories.
+
+The use of RTLIL also has the disadvantage of having a very powerful
+format between all passes, even when doing gate-level synthesis where
+the more advanced features are not needed. In order to reduce complexity
+for passes that operate on a low-level representation, these passes
+check the features used in the input RTLIL and fail to run when
+unsupported high-level constructs are used. In such cases a pass that
+transforms the higher-level constructs to lower-level constructs must be
+called from the synthesis script first.
+
+.. _sec:typusecase:
+
+Typical Use Case
+----------------
+
+The following example script may be used in a synthesis flow to convert
+the behavioural Verilog code from the input file design.v to a
+gate-level netlist synth.v using the cell library described by the
+Liberty file :
+
+.. code:: sh
+   :number-lines:
+
+   # read input file to internal representation
+   read_verilog design.v
+
+   # convert high-level behavioral parts ("processes") to d-type flip-flops and muxes
+   proc
+
+   # perform some simple optimizations
+   opt
+
+   # convert high-level memory constructs to d-type flip-flops and multiplexers
+   memory
+
+   # perform some simple optimizations
+   opt
+
+   # convert design to (logical) gate-level netlists
+   techmap
+
+   # perform some simple optimizations
+   opt
+
+   # map internal register types to the ones from the cell library
+   dfflibmap -liberty cells.lib
+
+   # use ABC to map remaining logic to cells from the cell library
+   abc -liberty cells.lib
+
+   # cleanup
+   opt
+
+   # write results to output file
+   write_verilog synth.v
+
+A detailed description of the commands available in Yosys can be found
+in App. \ `[commandref] <#commandref>`__.
+
+.. [1]
+   In Yosys the term pass is only used to refer to commands that operate
+   on the RTLIL data structure.

docs/source/CHAPTER_Eval.rst

@@ -0,0 +1,231 @@
+.. _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.