mirror of https://github.com/YosysHQ/yosys.git
364 lines
11 KiB
ReStructuredText
364 lines
11 KiB
ReStructuredText
Flows, command types, and order
|
|
===============================
|
|
|
|
Command order
|
|
-------------
|
|
|
|
.. TODO:: check text is coherent
|
|
|
|
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
|
|
design and looks for sub-circuits in the design that match any of the modules
|
|
in the map file.
|
|
- If a match is found, the :cmd:ref:`extract` pass will replace the matching
|
|
subcircuit with an instance of the module from the map file.
|
|
- In a way the :cmd:ref:`extract` pass is the inverse of the techmap pass.
|
|
|
|
.. todo:: add/expand supporting text, also mention custom pattern matching and
|
|
pmgen
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_simple_test.ys
|
|
:language: yoscrypt
|
|
:lines: 1-2
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_simple_test_00a.*
|
|
:class: width-helper
|
|
|
|
before :cmd:ref:`extract`
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_simple_test.ys
|
|
:language: yoscrypt
|
|
:lines: 6
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_simple_test_00b.*
|
|
:class: width-helper
|
|
|
|
after :cmd:ref:`extract`
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_simple_test.v
|
|
:language: verilog
|
|
:caption: ``docs/source/code_examples/macc/macc_simple_test.v``
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_simple_xmap.v
|
|
:language: verilog
|
|
:caption: ``docs/source/code_examples/macc/macc_simple_xmap.v``
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_simple_test_01.v
|
|
:language: verilog
|
|
:caption: ``docs/source/code_examples/macc/macc_simple_test_01.v``
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_simple_test_01a.*
|
|
:class: width-helper
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_simple_test_01b.*
|
|
:class: width-helper
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_simple_test_02.v
|
|
:language: verilog
|
|
:caption: ``docs/source/code_examples/macc/macc_simple_test_02.v``
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_simple_test_02a.*
|
|
:class: width-helper
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_simple_test_02b.*
|
|
:class: width-helper
|
|
|
|
The wrap-extract-unwrap method
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
|
Often a coarse-grain element has a constant bit-width, but can be used to
|
|
implement operations with a smaller bit-width. For example, a 18x25-bit multiplier
|
|
can also be used to implement 16x20-bit multiplication.
|
|
|
|
A way of mapping such elements in coarse grain synthesis is the wrap-extract-unwrap method:
|
|
|
|
wrap
|
|
Identify candidate-cells in the circuit and wrap them in a cell with a
|
|
constant wider bit-width using :cmd:ref:`techmap`. The wrappers use the same
|
|
parameters as the original cell, so the information about the original width
|
|
of the ports is preserved. Then use the ``connwrappers`` command to connect up
|
|
the bit-extended in- and outputs of the wrapper cells.
|
|
|
|
extract
|
|
Now all operations are encoded using the same bit-width as the coarse grain
|
|
element. The :cmd:ref:`extract` command can be used to replace circuits with
|
|
cells of the target architecture.
|
|
|
|
unwrap
|
|
The remaining wrapper cell can be unwrapped using :cmd:ref:`techmap`.
|
|
|
|
Example: DSP48_MACC
|
|
~~~~~~~~~~~~~~~~~~~
|
|
|
|
This section details an example that shows how to map MACC operations of
|
|
arbitrary size to MACC cells with a 18x25-bit multiplier and a 48-bit adder
|
|
(such as the Xilinx DSP48 cells).
|
|
|
|
Preconditioning: ``macc_xilinx_swap_map.v``
|
|
|
|
Make sure ``A`` is the smaller port on all multipliers
|
|
|
|
.. todo:: add/expand supporting text
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_swap_map.v
|
|
:language: verilog
|
|
:caption: ``docs/source/code_examples/macc/macc_xilinx_swap_map.v``
|
|
|
|
Wrapping multipliers: ``macc_xilinx_wrap_map.v``
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_wrap_map.v
|
|
:language: verilog
|
|
:lines: 1-46
|
|
:caption: ``docs/source/code_examples/macc/macc_xilinx_wrap_map.v``
|
|
|
|
Wrapping adders: ``macc_xilinx_wrap_map.v``
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_wrap_map.v
|
|
:language: verilog
|
|
:lines: 48-89
|
|
:caption: ``docs/source/code_examples/macc/macc_xilinx_wrap_map.v``
|
|
|
|
Extract: ``macc_xilinx_xmap.v``
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_xmap.v
|
|
:language: verilog
|
|
:caption: ``docs/source/code_examples/macc/macc_xilinx_xmap.v``
|
|
|
|
... simply use the same wrapping commands on this module as on the design to
|
|
create a template for the :cmd:ref:`extract` command.
|
|
|
|
Unwrapping multipliers: ``macc_xilinx_unwrap_map.v``
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_unwrap_map.v
|
|
:language: verilog
|
|
:lines: 1-30
|
|
:caption: ``docs/source/code_examples/macc/macc_xilinx_unwrap_map.v``
|
|
|
|
Unwrapping adders: ``macc_xilinx_unwrap_map.v``
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_unwrap_map.v
|
|
:language: verilog
|
|
:lines: 32-61
|
|
:caption: ``docs/source/code_examples/macc/macc_xilinx_unwrap_map.v``
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_test.v
|
|
:language: verilog
|
|
:lines: 1-6
|
|
:caption: ``test1`` of ``docs/source/code_examples/macc/macc_xilinx_test.v``
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test1a.*
|
|
:class: width-helper
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test1b.*
|
|
:class: width-helper
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_test.v
|
|
:language: verilog
|
|
:lines: 8-13
|
|
:caption: ``test2`` of ``docs/source/code_examples/macc/macc_xilinx_test.v``
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test2a.*
|
|
:class: width-helper
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test2b.*
|
|
:class: width-helper
|
|
|
|
Wrapping in ``test1``:
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test1b.*
|
|
:class: width-helper
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_test.ys
|
|
:language: yoscrypt
|
|
:start-after: part c
|
|
:end-before: end part c
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test1c.*
|
|
:class: width-helper
|
|
|
|
Wrapping in ``test2``:
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test2b.*
|
|
:class: width-helper
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_test.ys
|
|
:language: yoscrypt
|
|
:start-after: part c
|
|
:end-before: end part c
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test2c.*
|
|
:class: width-helper
|
|
|
|
Extract in ``test1``:
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test1c.*
|
|
:class: width-helper
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_test.ys
|
|
:language: yoscrypt
|
|
:start-after: part d
|
|
:end-before: end part d
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test1d.*
|
|
:class: width-helper
|
|
|
|
Extract in ``test2``:
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test2c.*
|
|
:class: width-helper
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_test.ys
|
|
:language: yoscrypt
|
|
:start-after: part d
|
|
:end-before: end part d
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test2d.*
|
|
:class: width-helper
|
|
|
|
Unwrap in ``test2``:
|
|
|
|
.. figure:: /_images/code_examples/macc/macc_xilinx_test2d.*
|
|
:class: width-helper
|
|
|
|
.. literalinclude:: /code_examples/macc/macc_xilinx_test.ys
|
|
:language: yoscrypt
|
|
:start-after: part e
|
|
: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!
|