mirror of
https://github.com/YosysHQ/yosys
synced 2025-07-22 20:32:07 +00:00
Move (most of) ExOth and ExAdv slides
This commit is contained in:
Krystine Sherwin
parent
7ab051778e
commit
8ade2182b0
49 changed files with 828 additions and 1027 deletions
271
docs/source/yosys_internals/flow/command_ordering.rst
Normal file
271
docs/source/yosys_internals/flow/command_ordering.rst
Normal file
|
|
@ -0,0 +1,271 @@
|
|||
Command ordering
|
||||
----------------
|
||||
|
||||
.. TODO: copypaste
|
||||
|
||||
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 ``techmap`` pass, the ``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 ``extract`` pass will replace the matching subcircuit
|
||||
with an instance of the module from the map file.
|
||||
- In a way the ``extract`` pass is the inverse of the techmap pass.
|
||||
|
||||
.. TODO: copypaste
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_simple_test_00a.*
|
||||
:class: width-helper
|
||||
|
||||
before `extract`
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_simple_test_00b.*
|
||||
:class: width-helper
|
||||
|
||||
after `extract`
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_simple_test.v
|
||||
:language: verilog
|
||||
:caption: ``docs/resources/PRESENTATION_ExAdv/macc_simple_test.v``
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_simple_xmap.v
|
||||
:language: verilog
|
||||
:caption: ``docs/resources/PRESENTATION_ExAdv/macc_simple_xmap.v``
|
||||
|
||||
.. code:: yoscrypt
|
||||
|
||||
read_verilog macc_simple_test.v
|
||||
hierarchy -check -top test
|
||||
|
||||
extract -map macc_simple_xmap.v;;
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_simple_test_01.v
|
||||
:language: verilog
|
||||
:caption: ``docs/resources/PRESENTATION_ExAdv/macc_simple_test_01.v``
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_simple_test_01a.*
|
||||
:class: width-helper
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_simple_test_01b.*
|
||||
:class: width-helper
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_simple_test_02.v
|
||||
:language: verilog
|
||||
:caption: ``docs/resources/PRESENTATION_ExAdv/macc_simple_test_02.v``
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_simple_test_02a.*
|
||||
:class: width-helper
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/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 ``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 ``extract`` command can be used to replace circuits with cells
|
||||
of the target architecture.
|
||||
|
||||
unwrap
|
||||
The remaining wrapper cell can be unwrapped using ``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: copypaste
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_xilinx_swap_map.v
|
||||
:language: verilog
|
||||
:caption: ``docs/resources/PRESENTATION_ExAdv/macc_xilinx_swap_map.v``
|
||||
|
||||
Wrapping multipliers: ``macc_xilinx_wrap_map.v``
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_xilinx_wrap_map.v
|
||||
:language: verilog
|
||||
:lines: 1-46
|
||||
:caption: ``docs/resources/PRESENTATION_ExAdv/macc_xilinx_wrap_map.v``
|
||||
|
||||
Wrapping adders: ``macc_xilinx_wrap_map.v``
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_xilinx_wrap_map.v
|
||||
:language: verilog
|
||||
:lines: 48-89
|
||||
:caption: ``docs/resources/PRESENTATION_ExAdv/macc_xilinx_wrap_map.v``
|
||||
|
||||
Extract: ``macc_xilinx_xmap.v``
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_xilinx_xmap.v
|
||||
:language: verilog
|
||||
:caption: ``docs/resources/PRESENTATION_ExAdv/macc_xilinx_xmap.v``
|
||||
|
||||
... simply use the same wrapping commands on this module as on the design to create a template for the ``extract`` command.
|
||||
|
||||
Unwrapping multipliers: ``macc_xilinx_unwrap_map.v``
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v
|
||||
:language: verilog
|
||||
:lines: 1-30
|
||||
:caption: ``docs/resources/PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v``
|
||||
|
||||
Unwrapping adders: ``macc_xilinx_unwrap_map.v``
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v
|
||||
:language: verilog
|
||||
:lines: 32-61
|
||||
:caption: ``docs/resources/PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v``
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_xilinx_test.v
|
||||
:language: verilog
|
||||
:lines: 1-6
|
||||
:caption: ``test1`` of ``docs/resources/PRESENTATION_ExAdv/macc_xilinx_test.v``
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test1a.*
|
||||
:class: width-helper
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test1b.*
|
||||
:class: width-helper
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/macc_xilinx_test.v
|
||||
:language: verilog
|
||||
:lines: 8-13
|
||||
:caption: ``test2`` of ``docs/resources/PRESENTATION_ExAdv/macc_xilinx_test.v``
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test2a.*
|
||||
:class: width-helper
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test2b.*
|
||||
:class: width-helper
|
||||
|
||||
Wrapping in ``test1``:
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test1b.*
|
||||
:class: width-helper
|
||||
|
||||
.. code:: yoscrypt
|
||||
|
||||
techmap -map macc_xilinx_wrap_map.v
|
||||
|
||||
connwrappers -unsigned $__mul_wrapper \
|
||||
Y Y_WIDTH \
|
||||
-unsigned $__add_wrapper \
|
||||
Y Y_WIDTH ;;
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test1c.*
|
||||
:class: width-helper
|
||||
|
||||
Wrapping in ``test2``:
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test2b.*
|
||||
:class: width-helper
|
||||
|
||||
.. code:: yoscrypt
|
||||
|
||||
techmap -map macc_xilinx_wrap_map.v
|
||||
|
||||
connwrappers -unsigned $__mul_wrapper \
|
||||
Y Y_WIDTH \
|
||||
-unsigned $__add_wrapper \
|
||||
Y Y_WIDTH ;;
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test2c.*
|
||||
:class: width-helper
|
||||
|
||||
Extract in ``test1``:
|
||||
|
||||
.. code:: yoscrypt
|
||||
|
||||
design -push
|
||||
read_verilog macc_xilinx_xmap.v
|
||||
techmap -map macc_xilinx_swap_map.v
|
||||
techmap -map macc_xilinx_wrap_map.v;;
|
||||
design -save __macc_xilinx_xmap
|
||||
design -pop
|
||||
|
||||
extract -constports -ignore_parameters \
|
||||
-map %__macc_xilinx_xmap \
|
||||
-swap $__add_wrapper A,B ;;
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test1c.*
|
||||
:class: width-helper
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test1d.*
|
||||
:class: width-helper
|
||||
|
||||
Extract in ``test2``:
|
||||
|
||||
.. code:: yoscrypt
|
||||
|
||||
design -push
|
||||
read_verilog macc_xilinx_xmap.v
|
||||
techmap -map macc_xilinx_swap_map.v
|
||||
techmap -map macc_xilinx_wrap_map.v;;
|
||||
design -save __macc_xilinx_xmap
|
||||
design -pop
|
||||
|
||||
extract -constports -ignore_parameters \
|
||||
-map %__macc_xilinx_xmap \
|
||||
-swap $__add_wrapper A,B ;;
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test2c.*
|
||||
:class: width-helper
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test2d.*
|
||||
:class: width-helper
|
||||
|
||||
Unwrap in ``test2``:
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test2d.*
|
||||
:class: width-helper
|
||||
|
||||
.. figure:: ../../../images/res/PRESENTATION_ExAdv/macc_xilinx_test2e.*
|
||||
:class: width-helper
|
||||
|
||||
.. code:: yoscrypt
|
||||
|
||||
techmap -map macc_xilinx_unwrap_map.v ;;
|
||||
|
|
@ -17,4 +17,6 @@ This scripts contain three types of commands:
|
|||
overview
|
||||
control_and_data
|
||||
verilog_frontend
|
||||
command_ordering
|
||||
model_checking
|
||||
|
||||
|
|
|
|||
106
docs/source/yosys_internals/flow/model_checking.rst
Normal file
106
docs/source/yosys_internals/flow/model_checking.rst
Normal file
|
|
@ -0,0 +1,106 @@
|
|||
Symbolic model checking
|
||||
-----------------------
|
||||
|
||||
.. TODO: copypaste
|
||||
|
||||
.. 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 ``sat`` command in Yosys can be used to perform Symbolic Model Checking.
|
||||
|
||||
Checking techmap
|
||||
~~~~~~~~~~~~~~~~
|
||||
|
||||
Remember the following example from :doc:`/getting_started/typical_phases`?
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExSyn/techmap_01_map.v
|
||||
:language: verilog
|
||||
:caption: ``docs/resources/PRESENTATION_ExSyn/techmap_01_map.v``
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExSyn/techmap_01.v
|
||||
:language: verilog
|
||||
:caption: ``docs/resources/PRESENTATION_ExSyn/techmap_01.v``
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExSyn/techmap_01.ys
|
||||
:language: yoscrypt
|
||||
:caption: ``docs/resources/PRESENTATION_ExSyn/techmap_01.ys``
|
||||
|
||||
Lets see if it is correct..
|
||||
|
||||
.. 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.
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExOth/axis_master.v
|
||||
:language: verilog
|
||||
:caption: ``docs/resources/PRESENTATION_ExOth/axis_master.v``
|
||||
|
||||
.. literalinclude:: ../../../resources/PRESENTATION_ExOth/axis_test.v
|
||||
:language: verilog
|
||||
:caption: ``docs/resources/PRESENTATION_ExOth/axis_test.v``
|
||||
|
||||
|
||||
.. code:: yoscrypt
|
||||
|
||||
read_verilog -sv axis_master.v axis_test.v
|
||||
hierarchy -top axis_test
|
||||
|
||||
proc; flatten;;
|
||||
sat -seq 50 -prove-asserts
|
||||
|
||||
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!
|
||||
Loading…
Add table
Add a link
Reference in a new issue