From e2e7065590ff8dbd1baa7bbfd9c91fb890428f55 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 26 Jan 2024 13:06:02 +1300 Subject: [PATCH] Docs: some restructure of advanced section - Filling out index descriptions for `using_yosys` and `using_yosys/synthesis`. - To discourage skipping over these index pages, the toctree in `using_yosys/index` is hidden and instead has inline links to the two subsections. - Tidying todos. - Moves technology mapping to `techmap_synth`, leaving the techmap by example in the internals section. `yosys_flows` gets split up, with the coarse-grain intro replaced by `synthesis/index`, the extract pass moving to `synthesis/extract` and model checking to `more_scripting/model_checking`. --- docs/source/index.rst | 17 ++- docs/source/using_yosys/index.rst | 18 ++- .../using_yosys/more_scripting/index.rst | 1 + .../more_scripting/model_checking.rst | 108 +++++++++++++ .../using_yosys/synthesis/cell_libs.rst | 4 - .../extract.rst} | 143 +----------------- docs/source/using_yosys/synthesis/index.rst | 20 ++- docs/source/using_yosys/synthesis/synth.rst | 2 + .../using_yosys/synthesis/techmap_synth.rst | 109 ++++++++++++- docs/source/yosys_internals/techmap.rst | 110 -------------- 10 files changed, 259 insertions(+), 273 deletions(-) create mode 100644 docs/source/using_yosys/more_scripting/model_checking.rst rename docs/source/using_yosys/{yosys_flows.rst => synthesis/extract.rst} (63%) diff --git a/docs/source/index.rst b/docs/source/index.rst index bbefa521f..582551f74 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -33,12 +33,13 @@ available, go to :ref:`commandindex`. ----------------- .. toctree:: - :maxdepth: 3 - - introduction - getting_started/index - using_yosys/index - yosys_internals/index - test_suites + :maxdepth: 3 + :includehidden: - appendix + introduction + getting_started/index + using_yosys/index + yosys_internals/index + test_suites + + appendix diff --git a/docs/source/using_yosys/index.rst b/docs/source/using_yosys/index.rst index 91d34bfe4..55bd5c291 100644 --- a/docs/source/using_yosys/index.rst +++ b/docs/source/using_yosys/index.rst @@ -1,11 +1,17 @@ Using Yosys (advanced) ====================== -.. todo:: brief overview for the using Yosys index +While much of Yosys is focused around synthesis, there are also a number of +other useful things that can be accomplished with Yosys scripts or in an +interactive shell. As such this section is broken into two parts: +:doc:`/using_yosys/synthesis/index` expands on the +:doc:`/getting_started/example_synth` and goes into further detail on the major +commands used in synthesis; :doc:`/using_yosys/more_scripting/index` covers the +ways Yosys can interact with designs for a deeper investigation. -.. toctree:: - :maxdepth: 2 +.. toctree:: + :maxdepth: 2 + :hidden: - synthesis/index - more_scripting/index - yosys_flows + synthesis/index + more_scripting/index diff --git a/docs/source/using_yosys/more_scripting/index.rst b/docs/source/using_yosys/more_scripting/index.rst index 2d67b6a09..490a5a7ad 100644 --- a/docs/source/using_yosys/more_scripting/index.rst +++ b/docs/source/using_yosys/more_scripting/index.rst @@ -9,5 +9,6 @@ More scripting load_design selections interactive_investigation + model_checking .. troubleshooting diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst new file mode 100644 index 000000000..f0171b14c --- /dev/null +++ b/docs/source/using_yosys/more_scripting/model_checking.rst @@ -0,0 +1,108 @@ +Symbolic model checking +----------------------- + +.. todo:: check text context + +.. note:: + + While it is possible to perform model checking directly in Yosys, it + is highly recommended to use SBY or EQY for formal hardware verification. + +Symbolic Model Checking (SMC) is used to formally prove that a circuit has (or +has not) a given property. + +One application is Formal Equivalence Checking: Proving that two circuits are +identical. For example this is a very useful feature when debugging custom +passes in Yosys. + +Other applications include checking if a module conforms to interface standards. + +The :cmd:ref:`sat` command in Yosys can be used to perform Symbolic Model +Checking. + +Checking techmap +~~~~~~~~~~~~~~~~ + +.. todo:: add/expand supporting text + +Let's look at the following example: + +.. literalinclude:: /code_examples/synth_flow/techmap_01_map.v + :language: verilog + :caption: ``docs/source/code_examples/synth_flow/techmap_01_map.v`` + +.. literalinclude:: /code_examples/synth_flow/techmap_01.v + :language: verilog + :caption: ``docs/source/code_examples/synth_flow/techmap_01.v`` + +.. literalinclude:: /code_examples/synth_flow/techmap_01.ys + :language: yoscrypt + :caption: ``docs/source/code_examples/synth_flow/techmap_01.ys`` + +To see if it is correct we can use the following code: + +.. todo:: replace inline yosys script code + +.. code:: yoscrypt + + # read test design + read_verilog techmap_01.v + hierarchy -top test + + # create two version of the design: test_orig and test_mapped + copy test test_orig + rename test test_mapped + + # apply the techmap only to test_mapped + techmap -map techmap_01_map.v test_mapped + + # create a miter circuit to test equivalence + miter -equiv -make_assert -make_outputs test_orig test_mapped miter + flatten miter + + # run equivalence check + sat -verify -prove-asserts -show-inputs -show-outputs miter + +Result: + +.. code:: + + Solving problem with 945 variables and 2505 clauses.. + SAT proof finished - no model found: SUCCESS! + +AXI4 Stream Master +~~~~~~~~~~~~~~~~~~ + +The following AXI4 Stream Master has a bug. But the bug is not exposed if the +slave keeps ``tready`` asserted all the time. (Something a test bench might do.) + +Symbolic Model Checking can be used to expose the bug and find a sequence of +values for ``tready`` that yield the incorrect behavior. + +.. todo:: add/expand supporting text + +.. literalinclude:: /code_examples/axis/axis_master.v + :language: verilog + :caption: ``docs/source/code_examples/axis/axis_master.v`` + +.. literalinclude:: /code_examples/axis/axis_test.v + :language: verilog + :caption: ``docs/source/code_examples/axis/axis_test.v`` + +.. literalinclude:: /code_examples/axis/axis_test.ys + :language: yoscrypt + :caption: ``docs/source/code_examples/axis/test.ys`` + +Result with unmodified ``axis_master.v``: + +.. code:: + + Solving problem with 159344 variables and 442126 clauses.. + SAT proof finished - model found: FAIL! + +Result with fixed ``axis_master.v``: + +.. code:: + + Solving problem with 159144 variables and 441626 clauses.. + SAT proof finished - no model found: SUCCESS! diff --git a/docs/source/using_yosys/synthesis/cell_libs.rst b/docs/source/using_yosys/synthesis/cell_libs.rst index 5f54b894f..4353b3cdc 100644 --- a/docs/source/using_yosys/synthesis/cell_libs.rst +++ b/docs/source/using_yosys/synthesis/cell_libs.rst @@ -73,8 +73,6 @@ Coarse-grain representation Logic gate mapping ~~~~~~~~~~~~~~~~~~ -.. TODO:: comment on similarities and/or differences with example_synth - .. literalinclude:: /code_examples/intro/counter.ys :language: yoscrypt :lines: 14-15 @@ -89,8 +87,6 @@ Logic gate mapping Mapping to hardware ~~~~~~~~~~~~~~~~~~~ -.. todo:: are we recalling or is this new information - For this example, we are using a Liberty file to describe a cell library which our internal cell library will be mapped to: diff --git a/docs/source/using_yosys/yosys_flows.rst b/docs/source/using_yosys/synthesis/extract.rst similarity index 63% rename from docs/source/using_yosys/yosys_flows.rst rename to docs/source/using_yosys/synthesis/extract.rst index 5bca90ade..c5a64273a 100644 --- a/docs/source/using_yosys/yosys_flows.rst +++ b/docs/source/using_yosys/synthesis/extract.rst @@ -1,35 +1,5 @@ -Flows, command types, and order -=============================== - -Command order -------------- - -.. todo:: More surrounding text (esp as it relates to command order) - -Intro to coarse-grain synthesis -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -In coarse-grain synthesis the target architecture has cells of the same -complexity or larger complexity than the internal RTL representation. - -For example: - -.. code:: verilog - - wire [15:0] a, b; - wire [31:0] c, y; - assign y = a * b + c; - -This circuit contains two cells in the RTL representation: one multiplier and -one adder. In some architectures this circuit can be implemented using -a single circuit element, for example an FPGA DSP core. Coarse grain synthesis -is this mapping of groups of circuit elements to larger components. - -Fine-grain synthesis would be matching the circuit elements to smaller -components, such as LUTs, gates, or half- and full-adders. - The extract pass -~~~~~~~~~~~~~~~~ +---------------- - Like the :cmd:ref:`techmap` pass, the :cmd:ref:`extract` pass is called with a map file. It compares the circuits inside the modules of the map file with the @@ -255,113 +225,4 @@ Unwrap in ``test2``: :end-before: end part e .. figure:: /_images/code_examples/macc/macc_xilinx_test2e.* - :class: width-helper - -Symbolic model checking ------------------------ - -.. todo:: check text context - -.. note:: - - While it is possible to perform model checking directly in Yosys, it - is highly recommended to use SBY or EQY for formal hardware verification. - -Symbolic Model Checking (SMC) is used to formally prove that a circuit has (or -has not) a given property. - -One application is Formal Equivalence Checking: Proving that two circuits are -identical. For example this is a very useful feature when debugging custom -passes in Yosys. - -Other applications include checking if a module conforms to interface standards. - -The :cmd:ref:`sat` command in Yosys can be used to perform Symbolic Model -Checking. - -Checking techmap -~~~~~~~~~~~~~~~~ - -.. todo:: add/expand supporting text - -Let's look at the following example: - -.. literalinclude:: /code_examples/synth_flow/techmap_01_map.v - :language: verilog - :caption: ``docs/source/code_examples/synth_flow/techmap_01_map.v`` - -.. literalinclude:: /code_examples/synth_flow/techmap_01.v - :language: verilog - :caption: ``docs/source/code_examples/synth_flow/techmap_01.v`` - -.. literalinclude:: /code_examples/synth_flow/techmap_01.ys - :language: yoscrypt - :caption: ``docs/source/code_examples/synth_flow/techmap_01.ys`` - -To see if it is correct we can use the following code: - -.. todo:: replace inline yosys script code - -.. code:: yoscrypt - - # read test design - read_verilog techmap_01.v - hierarchy -top test - - # create two version of the design: test_orig and test_mapped - copy test test_orig - rename test test_mapped - - # apply the techmap only to test_mapped - techmap -map techmap_01_map.v test_mapped - - # create a miter circuit to test equivalence - miter -equiv -make_assert -make_outputs test_orig test_mapped miter - flatten miter - - # run equivalence check - sat -verify -prove-asserts -show-inputs -show-outputs miter - -Result: - -.. code:: - - Solving problem with 945 variables and 2505 clauses.. - SAT proof finished - no model found: SUCCESS! - -AXI4 Stream Master -~~~~~~~~~~~~~~~~~~ - -The following AXI4 Stream Master has a bug. But the bug is not exposed if the -slave keeps ``tready`` asserted all the time. (Something a test bench might do.) - -Symbolic Model Checking can be used to expose the bug and find a sequence of -values for ``tready`` that yield the incorrect behavior. - -.. todo:: add/expand supporting text - -.. literalinclude:: /code_examples/axis/axis_master.v - :language: verilog - :caption: ``docs/source/code_examples/axis/axis_master.v`` - -.. literalinclude:: /code_examples/axis/axis_test.v - :language: verilog - :caption: ``docs/source/code_examples/axis/axis_test.v`` - -.. literalinclude:: /code_examples/axis/axis_test.ys - :language: yoscrypt - :caption: ``docs/source/code_examples/axis/test.ys`` - -Result with unmodified ``axis_master.v``: - -.. code:: - - Solving problem with 159344 variables and 442126 clauses.. - SAT proof finished - model found: FAIL! - -Result with fixed ``axis_master.v``: - -.. code:: - - Solving problem with 159144 variables and 441626 clauses.. - SAT proof finished - no model found: SUCCESS! + :class: width-helper \ No newline at end of file diff --git a/docs/source/using_yosys/synthesis/index.rst b/docs/source/using_yosys/synthesis/index.rst index 095dd4b61..c00a940da 100644 --- a/docs/source/using_yosys/synthesis/index.rst +++ b/docs/source/using_yosys/synthesis/index.rst @@ -1,7 +1,24 @@ Synthesis in detail ------------------- -.. todo:: brief overview for the synthesis index +Synthesis can generally be broken down into coarse-grain synthesis, and +fine-grain synthesis. We saw this in :doc:`/getting_started/example_synth` +where a design was loaded and elaborated and then went through a series of +coarse-grain optimizations before being mapped to hard blocks and fine-grain +cells. Most commands in Yosys will target either coarse-grain representation or +fine-grain representation, with only a select few compatible with both states. + +Commands such as :cmd:ref:`proc`, :cmd:ref:`fsm`, and :cmd:ref:`memory` rely on +the additional information in the coarse-grain representation, along with a +number of optimizations such as :cmd:ref:`wreduce`, :cmd:ref:`share`, and +:cmd:ref:`alumacc`. :cmd:ref:`opt` provides optimizations which are useful in +both states, while :cmd:ref:`techmap` is used to convert coarse-grain cells +to the corresponding fine-grain representation. + +Single-bit cells (logic gates, FFs) as well as LUTs, half-adders, and +full-adders make up the bulk of the fine-grain representation and are necessary +for commands such as :cmd:ref:`abc`\ /:cmd:ref:`abc9`, :cmd:ref:`simplemap`, +:cmd:ref:`dfflegalize`, and :cmd:ref:`memory_map`. .. toctree:: :maxdepth: 3 @@ -12,6 +29,7 @@ Synthesis in detail memory opt techmap_synth + extract abc cell_libs diff --git a/docs/source/using_yosys/synthesis/synth.rst b/docs/source/using_yosys/synthesis/synth.rst index 15d701fb4..cba7db1a7 100644 --- a/docs/source/using_yosys/synthesis/synth.rst +++ b/docs/source/using_yosys/synthesis/synth.rst @@ -1,6 +1,8 @@ Synth commands -------------- +.. todo:: comment on common ``synth_*`` options, like ``-run`` + Packaged ``synth_*`` commands ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/docs/source/using_yosys/synthesis/techmap_synth.rst b/docs/source/using_yosys/synthesis/techmap_synth.rst index db1d0c96a..dc9d8b195 100644 --- a/docs/source/using_yosys/synthesis/techmap_synth.rst +++ b/docs/source/using_yosys/synthesis/techmap_synth.rst @@ -1,4 +1,107 @@ -techmap_synth -------------- +Technology mapping +================== -.. TODO:: techmap_synth +.. todo:: less academic, check text is coherent + +Previous chapters outlined how HDL code is transformed into an RTL netlist. The +RTL netlist is still based on abstract coarse-grain cell types like arbitrary +width adders and even multipliers. This chapter covers how an RTL netlist is +transformed into a functionally equivalent netlist utilizing the cell types +available in the target architecture. + +Technology mapping is often performed in two phases. In the first phase RTL +cells are mapped to an internal library of single-bit cells (see +:ref:`sec:celllib_gates`). In the second phase this netlist of internal gate +types is transformed to a netlist of gates from the target technology library. + +When the target architecture provides coarse-grain cells (such as block ram or +ALUs), these must be mapped to directly form the RTL netlist, as information on +the coarse-grain structure of the design is lost when it is mapped to bit-width +gate types. + +Cell substitution +----------------- + +The simplest form of technology mapping is cell substitution, as performed by +the techmap pass. This pass, when provided with a Verilog file that implements +the RTL cell types using simpler cells, simply replaces the RTL cells with the +provided implementation. + +When no map file is provided, techmap uses a built-in map file that maps the +Yosys RTL cell types to the internal gate library used by Yosys. The curious +reader may find this map file as `techlibs/common/techmap.v` in the Yosys source +tree. + +Additional features have been added to techmap to allow for conditional mapping +of cells (see :doc:`/cmd/techmap`). This can for example be useful if the target +architecture supports hardware multipliers for certain bit-widths but not for +others. + +A usual synthesis flow would first use the techmap pass to directly map some RTL +cells to coarse-grain cells provided by the target architecture (if any) and +then use techmap with the built-in default file to map the remaining RTL cells +to gate logic. + +Subcircuit substitution +----------------------- + +Sometimes the target architecture provides cells that are more powerful than the +RTL cells used by Yosys. For example a cell in the target architecture that can +calculate the absolute-difference of two numbers does not match any single RTL +cell type but only combinations of cells. + +For these cases Yosys provides the extract pass that can match a given set of +modules against a design and identify the portions of the design that are +identical (i.e. isomorphic subcircuits) to any of the given modules. These +matched subcircuits are then replaced by instances of the given modules. + +The extract pass also finds basic variations of the given modules, such as +swapped inputs on commutative cell types. + +In addition to this the extract pass also has limited support for frequent +subcircuit mining, i.e. the process of finding recurring subcircuits in the +design. This has a few applications, including the design of new coarse-grain +architectures :cite:p:`intersynthFdlBookChapter`. + +The hard algorithmic work done by the extract pass (solving the isomorphic +subcircuit problem and frequent subcircuit mining) is performed using the +SubCircuit library that can also be used stand-alone without Yosys (see +:ref:`sec:SubCircuit`). + +.. _sec:techmap_extern: + +Gate-level technology mapping +----------------------------- + +.. todo:: newer techmap libraries appear to be largely ``.v`` instead of ``.lib`` + +On the gate-level the target architecture is usually described by a "Liberty +file". The Liberty file format is an industry standard format that can be used +to describe the behaviour and other properties of standard library cells . + +Mapping a design utilizing the Yosys internal gate library (e.g. as a result of +mapping it to this representation using the techmap pass) is performed in two +phases. + +First the register cells must be mapped to the registers that are available on +the target architectures. The target architecture might not provide all +variations of d-type flip-flops with positive and negative clock edge, +high-active and low-active asynchronous set and/or reset, etc. Therefore the +process of mapping the registers might add additional inverters to the design +and thus it is important to map the register cells first. + +Mapping of the register cells may be performed by using the dfflibmap pass. This +pass expects a Liberty file as argument (using the -liberty option) and only +uses the register cells from the Liberty file. + +Secondly the combinational logic must be mapped to the target architecture. This +is done using the external program ABC via the abc pass by using the -liberty +option to the pass. Note that in this case only the combinatorial cells are used +from the cell library. + +Occasionally Liberty files contain trade secrets (such as sensitive timing +information) that cannot be shared freely. This complicates processes such as +reporting bugs in the tools involved. When the information in the Liberty file +used by Yosys and ABC are not part of the sensitive information, the additional +tool yosys-filterlib (see :ref:`sec:filterlib`) can be used to strip the +sensitive information from the Liberty file. diff --git a/docs/source/yosys_internals/techmap.rst b/docs/source/yosys_internals/techmap.rst index d7186ab6c..ce40ea19c 100644 --- a/docs/source/yosys_internals/techmap.rst +++ b/docs/source/yosys_internals/techmap.rst @@ -1,113 +1,3 @@ -.. _chapter:techmap: - -.. todo:: less academic, check text is coherent - -.. TODO:: can we split some of this into synthesis/techmap ? - -Technology mapping -================== - -Previous chapters outlined how HDL code is transformed into an RTL netlist. The -RTL netlist is still based on abstract coarse-grain cell types like arbitrary -width adders and even multipliers. This chapter covers how an RTL netlist is -transformed into a functionally equivalent netlist utilizing the cell types -available in the target architecture. - -Technology mapping is often performed in two phases. In the first phase RTL -cells are mapped to an internal library of single-bit cells (see -:ref:`sec:celllib_gates`). In the second phase this netlist of internal gate -types is transformed to a netlist of gates from the target technology library. - -When the target architecture provides coarse-grain cells (such as block ram or -ALUs), these must be mapped to directly form the RTL netlist, as information on -the coarse-grain structure of the design is lost when it is mapped to bit-width -gate types. - -Cell substitution ------------------ - -The simplest form of technology mapping is cell substitution, as performed by -the techmap pass. This pass, when provided with a Verilog file that implements -the RTL cell types using simpler cells, simply replaces the RTL cells with the -provided implementation. - -When no map file is provided, techmap uses a built-in map file that maps the -Yosys RTL cell types to the internal gate library used by Yosys. The curious -reader may find this map file as `techlibs/common/techmap.v` in the Yosys source -tree. - -Additional features have been added to techmap to allow for conditional mapping -of cells (see :doc:`/cmd/techmap`). This can for example be useful if the target -architecture supports hardware multipliers for certain bit-widths but not for -others. - -A usual synthesis flow would first use the techmap pass to directly map some RTL -cells to coarse-grain cells provided by the target architecture (if any) and -then use techmap with the built-in default file to map the remaining RTL cells -to gate logic. - -Subcircuit substitution ------------------------ - -Sometimes the target architecture provides cells that are more powerful than the -RTL cells used by Yosys. For example a cell in the target architecture that can -calculate the absolute-difference of two numbers does not match any single RTL -cell type but only combinations of cells. - -For these cases Yosys provides the extract pass that can match a given set of -modules against a design and identify the portions of the design that are -identical (i.e. isomorphic subcircuits) to any of the given modules. These -matched subcircuits are then replaced by instances of the given modules. - -The extract pass also finds basic variations of the given modules, such as -swapped inputs on commutative cell types. - -In addition to this the extract pass also has limited support for frequent -subcircuit mining, i.e. the process of finding recurring subcircuits in the -design. This has a few applications, including the design of new coarse-grain -architectures :cite:p:`intersynthFdlBookChapter`. - -The hard algorithmic work done by the extract pass (solving the isomorphic -subcircuit problem and frequent subcircuit mining) is performed using the -SubCircuit library that can also be used stand-alone without Yosys (see -:ref:`sec:SubCircuit`). - -.. _sec:techmap_extern: - -Gate-level technology mapping ------------------------------ - -On the gate-level the target architecture is usually described by a "Liberty -file". The Liberty file format is an industry standard format that can be used -to describe the behaviour and other properties of standard library cells . - -Mapping a design utilizing the Yosys internal gate library (e.g. as a result of -mapping it to this representation using the techmap pass) is performed in two -phases. - -First the register cells must be mapped to the registers that are available on -the target architectures. The target architecture might not provide all -variations of d-type flip-flops with positive and negative clock edge, -high-active and low-active asynchronous set and/or reset, etc. Therefore the -process of mapping the registers might add additional inverters to the design -and thus it is important to map the register cells first. - -Mapping of the register cells may be performed by using the dfflibmap pass. This -pass expects a Liberty file as argument (using the -liberty option) and only -uses the register cells from the Liberty file. - -Secondly the combinational logic must be mapped to the target architecture. This -is done using the external program ABC via the abc pass by using the -liberty -option to the pass. Note that in this case only the combinatorial cells are used -from the cell library. - -Occasionally Liberty files contain trade secrets (such as sensitive timing -information) that cannot be shared freely. This complicates processes such as -reporting bugs in the tools involved. When the information in the Liberty file -used by Yosys and ABC are not part of the sensitive information, the additional -tool yosys-filterlib (see :ref:`sec:filterlib`) can be used to strip the -sensitive information from the Liberty file. - Techmap by example ------------------