diff --git a/docs/source/using_yosys/yosys_flows.rst b/docs/source/using_yosys/yosys_flows.rst index 61317f7cd..7a51385c1 100644 --- a/docs/source/using_yosys/yosys_flows.rst +++ b/docs/source/using_yosys/yosys_flows.rst @@ -1,8 +1,383 @@ Flows, command types, and order -------------------------------- +=============================== -Synthesis granularity -~~~~~~~~~~~~~~~~~~~~~ +Command order +------------- -Formal verification +.. 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 :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:: 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 :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:: 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 :cmd:ref:`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 ;; + +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 :cmd:ref:`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! diff --git a/docs/source/yosys_internals/flow/command_ordering.rst b/docs/source/yosys_internals/flow/command_ordering.rst deleted file mode 100644 index df351c486..000000000 --- a/docs/source/yosys_internals/flow/command_ordering.rst +++ /dev/null @@ -1,272 +0,0 @@ -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 :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:: 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 :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:: 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 :cmd:ref:`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 ;; diff --git a/docs/source/yosys_internals/flow/index.rst b/docs/source/yosys_internals/flow/index.rst index 3d05ea0bf..e2b5b658c 100644 --- a/docs/source/yosys_internals/flow/index.rst +++ b/docs/source/yosys_internals/flow/index.rst @@ -17,6 +17,4 @@ This scripts contain three types of commands: overview control_and_data verilog_frontend - command_ordering - model_checking diff --git a/docs/source/yosys_internals/flow/model_checking.rst b/docs/source/yosys_internals/flow/model_checking.rst deleted file mode 100644 index 3d8b35125..000000000 --- a/docs/source/yosys_internals/flow/model_checking.rst +++ /dev/null @@ -1,107 +0,0 @@ -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 :cmd:ref:`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!