From 8ade2182b0fa6678aa9e255b8ffe99b4b2979d38 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 7 Aug 2023 12:58:40 +1200 Subject: [PATCH] Move (most of) ExOth and ExAdv slides --- docs/images/Makefile | 2 +- .../resources}/PRESENTATION_ExAdv/.gitignore | 1 + .../resources}/PRESENTATION_ExAdv/Makefile | 17 +- .../PRESENTATION_ExAdv/addshift_map.v | 0 .../PRESENTATION_ExAdv/addshift_test.v | 0 .../PRESENTATION_ExAdv/addshift_test.ys | 0 .../PRESENTATION_ExAdv/macc_simple_test.v | 0 .../PRESENTATION_ExAdv/macc_simple_test.ys | 0 .../PRESENTATION_ExAdv/macc_simple_test_01.v | 0 .../PRESENTATION_ExAdv/macc_simple_test_02.v | 0 .../PRESENTATION_ExAdv/macc_simple_xmap.v | 0 .../PRESENTATION_ExAdv/macc_xilinx_swap_map.v | 0 .../PRESENTATION_ExAdv/macc_xilinx_test.v | 0 .../PRESENTATION_ExAdv/macc_xilinx_test.ys | 0 .../macc_xilinx_unwrap_map.v | 0 .../PRESENTATION_ExAdv/macc_xilinx_wrap_map.v | 0 .../PRESENTATION_ExAdv/macc_xilinx_xmap.v | 0 .../PRESENTATION_ExAdv/mulshift_map.v | 0 .../PRESENTATION_ExAdv/mulshift_test.v | 0 .../PRESENTATION_ExAdv/mulshift_test.ys | 0 .../resources}/PRESENTATION_ExAdv/mymul_map.v | 0 .../PRESENTATION_ExAdv/mymul_test.v | 0 .../PRESENTATION_ExAdv/mymul_test.ys | 0 .../PRESENTATION_ExAdv/red_or3x1_cells.v | 0 .../PRESENTATION_ExAdv/red_or3x1_map.v | 0 .../PRESENTATION_ExAdv/red_or3x1_test.v | 0 .../PRESENTATION_ExAdv/red_or3x1_test.ys | 0 .../resources}/PRESENTATION_ExAdv/select.v | 0 .../resources}/PRESENTATION_ExAdv/select.ys | 0 .../PRESENTATION_ExAdv/sym_mul_cells.v | 0 .../PRESENTATION_ExAdv/sym_mul_map.v | 0 .../PRESENTATION_ExAdv/sym_mul_test.v | 0 .../PRESENTATION_ExAdv/sym_mul_test.ys | 0 docs/resources/PRESENTATION_ExOth/.gitignore | 3 + .../resources}/PRESENTATION_ExOth/Makefile | 7 +- .../PRESENTATION_ExOth/axis_master.v | 0 .../resources}/PRESENTATION_ExOth/axis_test.v | 0 .../PRESENTATION_ExOth/axis_test.ys | 0 .../resources}/PRESENTATION_ExOth/equiv.ys | 0 .../resources}/PRESENTATION_ExOth/scrambler.v | 0 .../PRESENTATION_ExOth/scrambler.ys | 0 .../using_yosys/more_scripting/selections.rst | 249 +++++- .../yosys_internals/flow/command_ordering.rst | 271 ++++++ docs/source/yosys_internals/flow/index.rst | 2 + .../yosys_internals/flow/model_checking.rst | 106 +++ docs/source/yosys_internals/techmap.rst | 185 ++++- manual/PRESENTATION_ExAdv.tex | 784 ------------------ manual/PRESENTATION_ExOth.tex | 227 ----- manual/PRESENTATION_ExOth/.gitignore | 1 - 49 files changed, 828 insertions(+), 1027 deletions(-) rename {manual => docs/resources}/PRESENTATION_ExAdv/.gitignore (50%) rename {manual => docs/resources}/PRESENTATION_ExAdv/Makefile (62%) rename {manual => docs/resources}/PRESENTATION_ExAdv/addshift_map.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/addshift_test.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/addshift_test.ys (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/macc_simple_test.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/macc_simple_test.ys (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/macc_simple_test_01.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/macc_simple_test_02.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/macc_simple_xmap.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/macc_xilinx_swap_map.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/macc_xilinx_test.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/macc_xilinx_test.ys (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/macc_xilinx_wrap_map.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/macc_xilinx_xmap.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/mulshift_map.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/mulshift_test.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/mulshift_test.ys (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/mymul_map.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/mymul_test.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/mymul_test.ys (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/red_or3x1_cells.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/red_or3x1_map.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/red_or3x1_test.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/red_or3x1_test.ys (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/select.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/select.ys (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/sym_mul_cells.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/sym_mul_map.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/sym_mul_test.v (100%) rename {manual => docs/resources}/PRESENTATION_ExAdv/sym_mul_test.ys (100%) create mode 100644 docs/resources/PRESENTATION_ExOth/.gitignore rename {manual => docs/resources}/PRESENTATION_ExOth/Makefile (69%) rename {manual => docs/resources}/PRESENTATION_ExOth/axis_master.v (100%) rename {manual => docs/resources}/PRESENTATION_ExOth/axis_test.v (100%) rename {manual => docs/resources}/PRESENTATION_ExOth/axis_test.ys (100%) rename {manual => docs/resources}/PRESENTATION_ExOth/equiv.ys (100%) rename {manual => docs/resources}/PRESENTATION_ExOth/scrambler.v (100%) rename {manual => docs/resources}/PRESENTATION_ExOth/scrambler.ys (100%) create mode 100644 docs/source/yosys_internals/flow/command_ordering.rst create mode 100644 docs/source/yosys_internals/flow/model_checking.rst delete mode 100644 manual/PRESENTATION_ExOth.tex delete mode 100644 manual/PRESENTATION_ExOth/.gitignore diff --git a/docs/images/Makefile b/docs/images/Makefile index 4c84a01db..61fa6cd70 100644 --- a/docs/images/Makefile +++ b/docs/images/Makefile @@ -1,6 +1,6 @@ all: resources dots tex svg tidy -RES_LIST:= PRESENTATION_Intro/ PRESENTATION_ExSyn/ +RES_LIST:= PRESENTATION_Intro/ PRESENTATION_ExSyn/ PRESENTATION_ExAdv/ PRESENTATION_ExOth/ RES_DIRS:= $(addprefix ../resources/,$(RES_LIST)) .PHONY: resources resources: $(RES_DIRS) diff --git a/manual/PRESENTATION_ExAdv/.gitignore b/docs/resources/PRESENTATION_ExAdv/.gitignore similarity index 50% rename from manual/PRESENTATION_ExAdv/.gitignore rename to docs/resources/PRESENTATION_ExAdv/.gitignore index cf658897d..b4a858a01 100644 --- a/manual/PRESENTATION_ExAdv/.gitignore +++ b/docs/resources/PRESENTATION_ExAdv/.gitignore @@ -1 +1,2 @@ *.dot +*.pdf diff --git a/manual/PRESENTATION_ExAdv/Makefile b/docs/resources/PRESENTATION_ExAdv/Makefile similarity index 62% rename from manual/PRESENTATION_ExAdv/Makefile rename to docs/resources/PRESENTATION_ExAdv/Makefile index 993a9d9e1..8954ee254 100644 --- a/manual/PRESENTATION_ExAdv/Makefile +++ b/docs/resources/PRESENTATION_ExAdv/Makefile @@ -1,28 +1,29 @@ +YOSYS = ../../../yosys all: select.pdf red_or3x1.pdf sym_mul.pdf mymul.pdf mulshift.pdf addshift.pdf \ macc_simple_xmap.pdf macc_xilinx_xmap.pdf select.pdf: select.v select.ys - ../../yosys select.ys + $(YOSYS) select.ys red_or3x1.pdf: red_or3x1_* - ../../yosys red_or3x1_test.ys + $(YOSYS) red_or3x1_test.ys sym_mul.pdf: sym_mul_* - ../../yosys sym_mul_test.ys + $(YOSYS) sym_mul_test.ys mymul.pdf: mymul_* - ../../yosys mymul_test.ys + $(YOSYS) mymul_test.ys mulshift.pdf: mulshift_* - ../../yosys mulshift_test.ys + $(YOSYS) mulshift_test.ys addshift.pdf: addshift_* - ../../yosys addshift_test.ys + $(YOSYS) addshift_test.ys macc_simple_xmap.pdf: macc_simple_*.v macc_simple_test.ys - ../../yosys macc_simple_test.ys + $(YOSYS) macc_simple_test.ys macc_xilinx_xmap.pdf: macc_xilinx_*.v macc_xilinx_test.ys - ../../yosys macc_xilinx_test.ys + $(YOSYS) macc_xilinx_test.ys diff --git a/manual/PRESENTATION_ExAdv/addshift_map.v b/docs/resources/PRESENTATION_ExAdv/addshift_map.v similarity index 100% rename from manual/PRESENTATION_ExAdv/addshift_map.v rename to docs/resources/PRESENTATION_ExAdv/addshift_map.v diff --git a/manual/PRESENTATION_ExAdv/addshift_test.v b/docs/resources/PRESENTATION_ExAdv/addshift_test.v similarity index 100% rename from manual/PRESENTATION_ExAdv/addshift_test.v rename to docs/resources/PRESENTATION_ExAdv/addshift_test.v diff --git a/manual/PRESENTATION_ExAdv/addshift_test.ys b/docs/resources/PRESENTATION_ExAdv/addshift_test.ys similarity index 100% rename from manual/PRESENTATION_ExAdv/addshift_test.ys rename to docs/resources/PRESENTATION_ExAdv/addshift_test.ys diff --git a/manual/PRESENTATION_ExAdv/macc_simple_test.v b/docs/resources/PRESENTATION_ExAdv/macc_simple_test.v similarity index 100% rename from manual/PRESENTATION_ExAdv/macc_simple_test.v rename to docs/resources/PRESENTATION_ExAdv/macc_simple_test.v diff --git a/manual/PRESENTATION_ExAdv/macc_simple_test.ys b/docs/resources/PRESENTATION_ExAdv/macc_simple_test.ys similarity index 100% rename from manual/PRESENTATION_ExAdv/macc_simple_test.ys rename to docs/resources/PRESENTATION_ExAdv/macc_simple_test.ys diff --git a/manual/PRESENTATION_ExAdv/macc_simple_test_01.v b/docs/resources/PRESENTATION_ExAdv/macc_simple_test_01.v similarity index 100% rename from manual/PRESENTATION_ExAdv/macc_simple_test_01.v rename to docs/resources/PRESENTATION_ExAdv/macc_simple_test_01.v diff --git a/manual/PRESENTATION_ExAdv/macc_simple_test_02.v b/docs/resources/PRESENTATION_ExAdv/macc_simple_test_02.v similarity index 100% rename from manual/PRESENTATION_ExAdv/macc_simple_test_02.v rename to docs/resources/PRESENTATION_ExAdv/macc_simple_test_02.v diff --git a/manual/PRESENTATION_ExAdv/macc_simple_xmap.v b/docs/resources/PRESENTATION_ExAdv/macc_simple_xmap.v similarity index 100% rename from manual/PRESENTATION_ExAdv/macc_simple_xmap.v rename to docs/resources/PRESENTATION_ExAdv/macc_simple_xmap.v diff --git a/manual/PRESENTATION_ExAdv/macc_xilinx_swap_map.v b/docs/resources/PRESENTATION_ExAdv/macc_xilinx_swap_map.v similarity index 100% rename from manual/PRESENTATION_ExAdv/macc_xilinx_swap_map.v rename to docs/resources/PRESENTATION_ExAdv/macc_xilinx_swap_map.v diff --git a/manual/PRESENTATION_ExAdv/macc_xilinx_test.v b/docs/resources/PRESENTATION_ExAdv/macc_xilinx_test.v similarity index 100% rename from manual/PRESENTATION_ExAdv/macc_xilinx_test.v rename to docs/resources/PRESENTATION_ExAdv/macc_xilinx_test.v diff --git a/manual/PRESENTATION_ExAdv/macc_xilinx_test.ys b/docs/resources/PRESENTATION_ExAdv/macc_xilinx_test.ys similarity index 100% rename from manual/PRESENTATION_ExAdv/macc_xilinx_test.ys rename to docs/resources/PRESENTATION_ExAdv/macc_xilinx_test.ys diff --git a/manual/PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v b/docs/resources/PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v similarity index 100% rename from manual/PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v rename to docs/resources/PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v diff --git a/manual/PRESENTATION_ExAdv/macc_xilinx_wrap_map.v b/docs/resources/PRESENTATION_ExAdv/macc_xilinx_wrap_map.v similarity index 100% rename from manual/PRESENTATION_ExAdv/macc_xilinx_wrap_map.v rename to docs/resources/PRESENTATION_ExAdv/macc_xilinx_wrap_map.v diff --git a/manual/PRESENTATION_ExAdv/macc_xilinx_xmap.v b/docs/resources/PRESENTATION_ExAdv/macc_xilinx_xmap.v similarity index 100% rename from manual/PRESENTATION_ExAdv/macc_xilinx_xmap.v rename to docs/resources/PRESENTATION_ExAdv/macc_xilinx_xmap.v diff --git a/manual/PRESENTATION_ExAdv/mulshift_map.v b/docs/resources/PRESENTATION_ExAdv/mulshift_map.v similarity index 100% rename from manual/PRESENTATION_ExAdv/mulshift_map.v rename to docs/resources/PRESENTATION_ExAdv/mulshift_map.v diff --git a/manual/PRESENTATION_ExAdv/mulshift_test.v b/docs/resources/PRESENTATION_ExAdv/mulshift_test.v similarity index 100% rename from manual/PRESENTATION_ExAdv/mulshift_test.v rename to docs/resources/PRESENTATION_ExAdv/mulshift_test.v diff --git a/manual/PRESENTATION_ExAdv/mulshift_test.ys b/docs/resources/PRESENTATION_ExAdv/mulshift_test.ys similarity index 100% rename from manual/PRESENTATION_ExAdv/mulshift_test.ys rename to docs/resources/PRESENTATION_ExAdv/mulshift_test.ys diff --git a/manual/PRESENTATION_ExAdv/mymul_map.v b/docs/resources/PRESENTATION_ExAdv/mymul_map.v similarity index 100% rename from manual/PRESENTATION_ExAdv/mymul_map.v rename to docs/resources/PRESENTATION_ExAdv/mymul_map.v diff --git a/manual/PRESENTATION_ExAdv/mymul_test.v b/docs/resources/PRESENTATION_ExAdv/mymul_test.v similarity index 100% rename from manual/PRESENTATION_ExAdv/mymul_test.v rename to docs/resources/PRESENTATION_ExAdv/mymul_test.v diff --git a/manual/PRESENTATION_ExAdv/mymul_test.ys b/docs/resources/PRESENTATION_ExAdv/mymul_test.ys similarity index 100% rename from manual/PRESENTATION_ExAdv/mymul_test.ys rename to docs/resources/PRESENTATION_ExAdv/mymul_test.ys diff --git a/manual/PRESENTATION_ExAdv/red_or3x1_cells.v b/docs/resources/PRESENTATION_ExAdv/red_or3x1_cells.v similarity index 100% rename from manual/PRESENTATION_ExAdv/red_or3x1_cells.v rename to docs/resources/PRESENTATION_ExAdv/red_or3x1_cells.v diff --git a/manual/PRESENTATION_ExAdv/red_or3x1_map.v b/docs/resources/PRESENTATION_ExAdv/red_or3x1_map.v similarity index 100% rename from manual/PRESENTATION_ExAdv/red_or3x1_map.v rename to docs/resources/PRESENTATION_ExAdv/red_or3x1_map.v diff --git a/manual/PRESENTATION_ExAdv/red_or3x1_test.v b/docs/resources/PRESENTATION_ExAdv/red_or3x1_test.v similarity index 100% rename from manual/PRESENTATION_ExAdv/red_or3x1_test.v rename to docs/resources/PRESENTATION_ExAdv/red_or3x1_test.v diff --git a/manual/PRESENTATION_ExAdv/red_or3x1_test.ys b/docs/resources/PRESENTATION_ExAdv/red_or3x1_test.ys similarity index 100% rename from manual/PRESENTATION_ExAdv/red_or3x1_test.ys rename to docs/resources/PRESENTATION_ExAdv/red_or3x1_test.ys diff --git a/manual/PRESENTATION_ExAdv/select.v b/docs/resources/PRESENTATION_ExAdv/select.v similarity index 100% rename from manual/PRESENTATION_ExAdv/select.v rename to docs/resources/PRESENTATION_ExAdv/select.v diff --git a/manual/PRESENTATION_ExAdv/select.ys b/docs/resources/PRESENTATION_ExAdv/select.ys similarity index 100% rename from manual/PRESENTATION_ExAdv/select.ys rename to docs/resources/PRESENTATION_ExAdv/select.ys diff --git a/manual/PRESENTATION_ExAdv/sym_mul_cells.v b/docs/resources/PRESENTATION_ExAdv/sym_mul_cells.v similarity index 100% rename from manual/PRESENTATION_ExAdv/sym_mul_cells.v rename to docs/resources/PRESENTATION_ExAdv/sym_mul_cells.v diff --git a/manual/PRESENTATION_ExAdv/sym_mul_map.v b/docs/resources/PRESENTATION_ExAdv/sym_mul_map.v similarity index 100% rename from manual/PRESENTATION_ExAdv/sym_mul_map.v rename to docs/resources/PRESENTATION_ExAdv/sym_mul_map.v diff --git a/manual/PRESENTATION_ExAdv/sym_mul_test.v b/docs/resources/PRESENTATION_ExAdv/sym_mul_test.v similarity index 100% rename from manual/PRESENTATION_ExAdv/sym_mul_test.v rename to docs/resources/PRESENTATION_ExAdv/sym_mul_test.v diff --git a/manual/PRESENTATION_ExAdv/sym_mul_test.ys b/docs/resources/PRESENTATION_ExAdv/sym_mul_test.ys similarity index 100% rename from manual/PRESENTATION_ExAdv/sym_mul_test.ys rename to docs/resources/PRESENTATION_ExAdv/sym_mul_test.ys diff --git a/docs/resources/PRESENTATION_ExOth/.gitignore b/docs/resources/PRESENTATION_ExOth/.gitignore new file mode 100644 index 000000000..3af2b8451 --- /dev/null +++ b/docs/resources/PRESENTATION_ExOth/.gitignore @@ -0,0 +1,3 @@ +*.dot +*.pdf +*.log diff --git a/manual/PRESENTATION_ExOth/Makefile b/docs/resources/PRESENTATION_ExOth/Makefile similarity index 69% rename from manual/PRESENTATION_ExOth/Makefile rename to docs/resources/PRESENTATION_ExOth/Makefile index 4864d8d52..4291f9976 100644 --- a/manual/PRESENTATION_ExOth/Makefile +++ b/docs/resources/PRESENTATION_ExOth/Makefile @@ -1,16 +1,17 @@ +YOSYS = ../../../yosys all: scrambler_p01.pdf scrambler_p02.pdf equiv.log axis_test.log scrambler_p01.pdf: scrambler.ys scrambler.v - ../../yosys scrambler.ys + $(YOSYS) scrambler.ys scrambler_p02.pdf: scrambler_p01.pdf equiv.log: equiv.ys - ../../yosys -l equiv.log_new equiv.ys + $(YOSYS) -l equiv.log_new equiv.ys mv equiv.log_new equiv.log axis_test.log: axis_test.ys axis_master.v axis_test.v - ../../yosys -l axis_test.log_new axis_test.ys + $(YOSYS) -l axis_test.log_new axis_test.ys mv axis_test.log_new axis_test.log diff --git a/manual/PRESENTATION_ExOth/axis_master.v b/docs/resources/PRESENTATION_ExOth/axis_master.v similarity index 100% rename from manual/PRESENTATION_ExOth/axis_master.v rename to docs/resources/PRESENTATION_ExOth/axis_master.v diff --git a/manual/PRESENTATION_ExOth/axis_test.v b/docs/resources/PRESENTATION_ExOth/axis_test.v similarity index 100% rename from manual/PRESENTATION_ExOth/axis_test.v rename to docs/resources/PRESENTATION_ExOth/axis_test.v diff --git a/manual/PRESENTATION_ExOth/axis_test.ys b/docs/resources/PRESENTATION_ExOth/axis_test.ys similarity index 100% rename from manual/PRESENTATION_ExOth/axis_test.ys rename to docs/resources/PRESENTATION_ExOth/axis_test.ys diff --git a/manual/PRESENTATION_ExOth/equiv.ys b/docs/resources/PRESENTATION_ExOth/equiv.ys similarity index 100% rename from manual/PRESENTATION_ExOth/equiv.ys rename to docs/resources/PRESENTATION_ExOth/equiv.ys diff --git a/manual/PRESENTATION_ExOth/scrambler.v b/docs/resources/PRESENTATION_ExOth/scrambler.v similarity index 100% rename from manual/PRESENTATION_ExOth/scrambler.v rename to docs/resources/PRESENTATION_ExOth/scrambler.v diff --git a/manual/PRESENTATION_ExOth/scrambler.ys b/docs/resources/PRESENTATION_ExOth/scrambler.ys similarity index 100% rename from manual/PRESENTATION_ExOth/scrambler.ys rename to docs/resources/PRESENTATION_ExOth/scrambler.ys diff --git a/docs/source/using_yosys/more_scripting/selections.rst b/docs/source/using_yosys/more_scripting/selections.rst index 3b81785dc..6b67b1691 100644 --- a/docs/source/using_yosys/more_scripting/selections.rst +++ b/docs/source/using_yosys/more_scripting/selections.rst @@ -1,6 +1,251 @@ Selections -~~~~~~~~~~ +---------- + +.. TODO: copypaste + + +Most Yosys commands make use of the "selection framework" of Yosys. It can be +used to apply commands only to part of the design. For example: + +.. code:: yoscrypt + + delete # will delete the whole design, but + + delete foobar # will only delete the module foobar. + +The ``select`` command can be used to create a selection for subsequent +commands. For example: + +.. code:: yoscrypt + + select foobar # select the module foobar + delete # delete selected objects + select -clear # reset selection (select whole design) See :doc:`/cmd/select` -Also :doc:`/cmd/show` and :doc:`/cmd/dump` +How to make a selection +~~~~~~~~~~~~~~~~~~~~~~~ + +Selection by object name +^^^^^^^^^^^^^^^^^^^^^^^^ + +The easiest way to select objects is by object name. This is usually only done +in synthesis scripts that are hand-tailored for a specific design. + +.. code:: yoscrypt + + select foobar # select module foobar + select foo* # select all modules whose names start with foo + select foo*/bar* # select all objects matching bar* from modules matching foo* + select */clk # select objects named clk from all modules + +Module and design context +^^^^^^^^^^^^^^^^^^^^^^^^^ + +Commands can be executed in *module/* or *design/* context. Until now +all commands have been executed in design context. The ``cd`` command can be +used to switch to module context. + +In module context all commands only effect the active module. Objects in the +module are selected without the ``/`` prefix. For example: + +.. code:: yoscrypt + + cd foo # switch to module foo + delete bar # delete object foo/bar + + cd mycpu # switch to module mycpu + dump reg_* # print details on all objects whose names start with reg_ + + cd .. # switch back to design + +Note: Most synthesis scripts never switch to module context. But it is a very +powerful tool for interactive design investigation. + +Selecting by object property or type +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +Special patterns can be used to select by object property or type. For example: + +.. code:: yoscrypt + + select w:reg_* # select all wires whose names start with reg_ + select a:foobar # select all objects with the attribute foobar set + select a:foobar=42 # select all objects with the attribute foobar set to 42 + select A:blabla # select all modules with the attribute blabla set + select foo/t:$add # select all $add cells from the module foo + +A complete list of this pattern expressions can be found in the command +reference to the ``select`` command. + +Combining selection +^^^^^^^^^^^^^^^^^^^ + +When more than one selection expression is used in one statement, then they are +pushed on a stack. The final elements on the stack are combined into a union: + +.. code:: yoscrypt + + select t:$dff r:WIDTH>1 # all cells of type $dff and/or with a parameter WIDTH > 1 + +Special ``%``-commands can be used to combine the elements on the stack: + +.. code:: yoscrypt + + select t:$dff r:WIDTH>1 %i # all cells of type $dff *AND* with a parameter WIDTH > 1 + +Examples for ``%``-codes (see :doc:`/cmd/select` for full list): + +- ``%u``: union of top two elements on stack -- pop 2, push 1 +- ``%d``: difference of top two elements on stack -- pop 2, push 1 +- ``%i``: intersection of top two elements on stack -- pop 2, push 1 +- ``%n``: inverse of top element on stack -- pop 1, push 1 + +Expanding selections +^^^^^^^^^^^^^^^^^^^^ + +Selections of cells and wires can be expanded along connections using +``%``-codes for selecting input cones (``%ci``), output cones (``%co``), or +both (``%x``). + +.. code:: yoscrypt + + # select all wires that are inputs to $add cells + select t:$add %ci w:* %i + +Additional constraints such as port names can be specified. + +.. code:: yoscrypt + + # select all wires that connect a "Q" output with a "D" input + select c:* %co:+[Q] w:* %i c:* %ci:+[D] w:* %i %i + + # select the multiplexer tree that drives the signal 'state' + select state %ci*:+$mux,$pmux[A,B,Y] + +See :doc:`/cmd/select` for full documentation of these expressions. + +Incremental selection +^^^^^^^^^^^^^^^^^^^^^ + +Sometimes a selection can most easily be described by a series of add/delete +operations. The commands ``select -add`` and ``select -del`` respectively add or +remove objects from the current selection instead of overwriting it. + +.. code:: yoscrypt + + select -none # start with an empty selection + select -add reg_* # select a bunch of objects + select -del reg_42 # but not this one + select -add state %ci # and add more stuff + +Within a select expression the token ``%`` can be used to push the previous selection +on the stack. + +.. code:: yoscrypt + + select t:$add t:$sub # select all $add and $sub cells + select % %ci % %d # select only the input wires to those cells + +Creating selection variables +^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +Selections can be stored under a name with the ``select -set `` +command. The stored selections can be used in later select expressions +using the syntax ``@``. + +.. code:: yoscrypt + + select -set cone_a state_a %ci*:-$dff # set @cone_a to the input cone of state_a + select -set cone_b state_b %ci*:-$dff # set @cone_b to the input cone of state_b + select @cone_a @cone_b %i # select the objects that are in both cones + +Remember that select expressions can also be used directly as arguments to most +commands. Some commands also except a single select argument to some options. +In those cases selection variables must be used to capture more complex selections. + +.. code:: yoscrypt + + dump @cone_a @cone_b + + select -set cone_ab @cone_a @cone_b %i + show -color red @cone_ab -color magenta @cone_a -color blue @cone_b + +Example: + +.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/select.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExAdv/select.v`` + +.. literalinclude:: ../../../resources/PRESENTATION_ExAdv/select.ys + :language: yoscrypt + :caption: ``docs/resources/PRESENTATION_ExAdv/select.ys`` + +.. figure:: ../../../images/res/PRESENTATION_ExAdv/select.* + :class: width-helper + +Interactive Design Investigation +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Yosys can also be used to investigate designs (or netlists created from other +tools). + +- The selection mechanism, especially patterns such as ``%ci`` and ``%co``, + can be used to figure out how parts of the design are connected. +- Commands such as ``submod``, ``expose``, and ``splice`` can be used to + transform the design into an equivalent design that is easier to analyse. +- Commands such as ``eval`` and ``sat`` can be used to investigate the behavior + of the circuit. +- :doc:`/cmd/show`. +- :doc:`/cmd/dump`. + +Reorganizing a module +^^^^^^^^^^^^^^^^^^^^^ + +.. literalinclude:: ../../../resources/PRESENTATION_ExOth/scrambler.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExOth/scrambler.v`` + + +.. code:: yoscrypt + + read_verilog scrambler.v + + hierarchy; proc;; + + cd scrambler + submod -name xorshift32 \ + xs %c %ci %D %c %ci:+[D] %D \ + %ci*:-$dff xs %co %ci %d + +.. figure:: ../../../images/res/PRESENTATION_ExOth/scrambler_p01.* + :class: width-helper + +.. figure:: ../../../images/res/PRESENTATION_ExOth/scrambler_p02.* + :class: width-helper + +Analysis of circuit behavior +^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +.. code:: text + + > read_verilog scrambler.v + > hierarchy; proc;; cd scrambler + > submod -name xorshift32 xs %c %ci %D %c %ci:+[D] %D %ci*:-$dff xs %co %ci %d + + > cd xorshift32 + > rename n2 in + > rename n1 out + + > eval -set in 1 -show out + Eval result: \out = 270369. + + > eval -set in 270369 -show out + Eval result: \out = 67634689. + + > sat -set out 632435482 + Signal Name Dec Hex Bin + -------------------- ---------- ---------- ------------------------------------- + \in 745495504 2c6f5bd0 00101100011011110101101111010000 + \out 632435482 25b2331a 00100101101100100011001100011010 diff --git a/docs/source/yosys_internals/flow/command_ordering.rst b/docs/source/yosys_internals/flow/command_ordering.rst new file mode 100644 index 000000000..1724ba5e3 --- /dev/null +++ b/docs/source/yosys_internals/flow/command_ordering.rst @@ -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 ;; diff --git a/docs/source/yosys_internals/flow/index.rst b/docs/source/yosys_internals/flow/index.rst index 195e50f64..868aa08fe 100644 --- a/docs/source/yosys_internals/flow/index.rst +++ b/docs/source/yosys_internals/flow/index.rst @@ -17,4 +17,6 @@ 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 new file mode 100644 index 000000000..3ac73fd6f --- /dev/null +++ b/docs/source/yosys_internals/flow/model_checking.rst @@ -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! diff --git a/docs/source/yosys_internals/techmap.rst b/docs/source/yosys_internals/techmap.rst index 18eec664b..745e5e2f5 100644 --- a/docs/source/yosys_internals/techmap.rst +++ b/docs/source/yosys_internals/techmap.rst @@ -31,7 +31,7 @@ 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 +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 @@ -105,3 +105,186 @@ 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 +------------------ + +.. TODO: copypaste + +As a quick recap, the ``techmap`` command replaces cells in the design with +implementations given as Verilog code (called "map files"). It can replace +Yosys' internal cell types (such as ``$or``) as well as user-defined cell +types. + +- Verilog parameters are used extensively to customize the internal cell types. +- Additional special parameters are used by techmap to communicate meta-data to + the map files. +- Special wires are used to instruct techmap how to handle a module in the map + file. +- Generate blocks and recursion are powerful tools for writing map files. + +Mapping OR3X1 +~~~~~~~~~~~~~ + +.. note:: + + This is a simple example for demonstration only. Techmap shouldn't be used + to implement basic logic optimization. + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/red_or3x1_map.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExAdv/red_or3x1_map.v`` + +.. figure:: ../../images/res/PRESENTATION_ExAdv/red_or3x1.* + :class: width-helper + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/red_or3x1_test.ys + :language: yoscrypt + :caption: ``docs/resources/PRESENTATION_ExAdv/red_or3x1_test.ys`` + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/red_or3x1_test.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExAdv/red_or3x1_test.v`` + +Conditional techmap +~~~~~~~~~~~~~~~~~~~ + +- In some cases only cells with certain properties should be substituted. +- The special wire ``_TECHMAP_FAIL_`` can be used to disable a module + in the map file for a certain set of parameters. +- The wire ``_TECHMAP_FAIL_`` must be set to a constant value. If it + is non-zero then the module is disabled for this set of parameters. +- Example use-cases: + + - coarse-grain cell types that only operate on certain bit widths + - memory resources for different memory geometries (width, depth, ports, etc.) + +Example: + +.. figure:: ../../images/res/PRESENTATION_ExAdv/sym_mul.* + :class: width-helper + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/sym_mul_map.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExAdv/sym_mul_map.v`` + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/sym_mul_test.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExAdv/sym_mul_test.v`` + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/sym_mul_test.ys + :language: yoscrypt + :caption: ``docs/resources/PRESENTATION_ExAdv/sym_mul_test.ys`` + + +Scripting in map modules +~~~~~~~~~~~~~~~~~~~~~~~~ + +- The special wires ``_TECHMAP_DO_*`` can be used to run Yosys scripts + in the context of the replacement module. +- The wire that comes first in alphabetical oder is interpreted as string (must + be connected to constants) that is executed as script. Then the wire is + removed. Repeat. +- You can even call techmap recursively! +- Example use-cases: + + - Using always blocks in map module: call ``proc`` + - Perform expensive optimizations (such as ``freduce``) on cells where + this is known to work well. + - Interacting with custom commands. + +.. note:: PROTIP: + Commands such as ``shell``, ``show -pause``, and ``dump`` can be use + in the ``_TECHMAP_DO_*`` scripts for debugging map modules. + +Example: + +.. figure:: ../../images/res/PRESENTATION_ExAdv/mymul.* + :class: width-helper + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/mymul_map.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExAdv/mymul_map.v`` + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/mymul_test.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExAdv/mymul_test.v`` + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/mymul_test.ys + :language: yoscrypt + :caption: ``docs/resources/PRESENTATION_ExAdv/mymul_test.ys`` + +Handling constant inputs +~~~~~~~~~~~~~~~~~~~~~~~~ + +- The special parameters ``_TECHMAP_CONSTMSK__`` and + ``_TECHMAP_CONSTVAL__`` can be used to handle constant input values + to cells. +- The former contains 1-bits for all constant input bits on the port. +- The latter contains the constant bits or undef (x) for non-constant bits. +- Example use-cases: + + - Converting arithmetic (for example multiply to shift). + - Identify constant addresses or enable bits in memory interfaces. + +Example: + +.. figure:: ../../images/res/PRESENTATION_ExAdv/mulshift.* + :class: width-helper + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/mulshift_map.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExAdv/mulshift_map.v`` + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/mulshift_test.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExAdv/mulshift_test.v`` + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/mulshift_test.ys + :language: yoscrypt + :caption: ``docs/resources/PRESENTATION_ExAdv/mulshift_test.ys`` + +Handling shorted inputs +~~~~~~~~~~~~~~~~~~~~~~~ + +- The special parameters ``_TECHMAP_BITS_CONNMAP_`` and + ``_TECHMAP_CONNMAP__`` can be used to handle shorted inputs. +- Each bit of the port correlates to an ``_TECHMAP_BITS_CONNMAP_`` bits wide + number in ``_TECHMAP_CONNMAP__``. +- Each unique signal bit is assigned its own number. Identical fields in the ``_TECHMAP_CONNMAP__`` parameters mean shorted signal bits. +- The numbers 0-3 are reserved for ``0``, ``1``, ``x``, and ``z`` respectively. +- Example use-cases: + + - Detecting shared clock or control signals in memory interfaces. + - In some cases this can be used for for optimization. + +Example: + +.. figure:: ../../images/res/PRESENTATION_ExAdv/addshift.* + :class: width-helper + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/addshift_map.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExAdv/addshift_map.v`` + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/addshift_test.v + :language: verilog + :caption: ``docs/resources/PRESENTATION_ExAdv/addshift_test.v`` + +.. literalinclude:: ../../resources/PRESENTATION_ExAdv/addshift_test.ys + :language: yoscrypt + :caption: ``docs/resources/PRESENTATION_ExAdv/addshift_test.ys`` + +Notes on using techmap +~~~~~~~~~~~~~~~~~~~~~~ + +- Don't use positional cell parameters in map modules. +- You can use the ``$__``-prefix for internal cell types to avoid + collisions with the user-namespace. But always use two underscores or the + internal consistency checker will trigger on this cells. +- Techmap has two major use cases: + + - Creating good logic-level representation of arithmetic functions. This + also means using dedicated hardware resources such as half- and full-adder + cells in ASICS or dedicated carry logic in FPGAs. + - Mapping of coarse-grain resources such as block memory or DSP cells. diff --git a/manual/PRESENTATION_ExAdv.tex b/manual/PRESENTATION_ExAdv.tex index 6a426ff2b..9acae2718 100644 --- a/manual/PRESENTATION_ExAdv.tex +++ b/manual/PRESENTATION_ExAdv.tex @@ -15,790 +15,6 @@ This section contains 4 subsections: \end{itemize} \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{Using selections} - -\begin{frame} -\subsectionpage -\subsectionpagesuffix -\end{frame} - -\subsubsection{Simple selections} - -\begin{frame}[fragile]{\subsubsecname} -Most Yosys commands make use of the ``selection framework'' of Yosys. It can be used -to apply commands only to part of the design. For example: - -\medskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -delete # will delete the whole design, but - -delete foobar # will only delete the module foobar. -\end{lstlisting} - -\bigskip -The {\tt select} command can be used to create a selection for subsequent -commands. For example: - -\medskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -select foobar # select the module foobar -delete # delete selected objects -select -clear # reset selection (select whole design) -\end{lstlisting} -\end{frame} - -\subsubsection{Selection by object name} - -\begin{frame}[fragile]{\subsubsecname} -The easiest way to select objects is by object name. This is usually only done -in synthesis scripts that are hand-tailored for a specific design. - -\bigskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -select foobar # select module foobar -select foo* # select all modules whose names start with foo -select foo*/bar* # select all objects matching bar* from modules matching foo* -select */clk # select objects named clk from all modules -\end{lstlisting} -\end{frame} - -\subsubsection{Module and design context} - -\begin{frame}[fragile]{\subsubsecname} -Commands can be executed in {\it module\/} or {\it design\/} context. Until now all -commands have been executed in design context. The {\tt cd} command can be used -to switch to module context. - -\bigskip -In module context all commands only effect the active module. Objects in the module -are selected without the {\tt /} prefix. For example: - -\bigskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -cd foo # switch to module foo -delete bar # delete object foo/bar - -cd mycpu # switch to module mycpu -dump reg_* # print details on all objects whose names start with reg_ - -cd .. # switch back to design -\end{lstlisting} - -\bigskip -Note: Most synthesis scripts never switch to module context. But it is a very powerful -tool for interactive design investigation. -\end{frame} - -\subsubsection{Selecting by object property or type} - -\begin{frame}[fragile]{\subsubsecname} -Special patterns can be used to select by object property or type. For example: - -\bigskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -select w:reg_* # select all wires whose names start with reg_ -select a:foobar # select all objects with the attribute foobar set -select a:foobar=42 # select all objects with the attribute foobar set to 42 -select A:blabla # select all modules with the attribute blabla set -select foo/t:$add # select all $add cells from the module foo -\end{lstlisting} - -\bigskip -A complete list of this pattern expressions can be found in the command -reference to the {\tt select} command. -\end{frame} - -\subsubsection{Combining selection} - -\begin{frame}[fragile]{\subsubsecname} -When more than one selection expression is used in one statement, then they are -pushed on a stack. The final elements on the stack are combined into a union: - -\medskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -select t:$dff r:WIDTH>1 # all cells of type $dff and/or with a parameter WIDTH > 1 -\end{lstlisting} - -\bigskip -Special \%-commands can be used to combine the elements on the stack: - -\medskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -select t:$dff r:WIDTH>1 %i # all cells of type $dff *AND* with a parameter WIDTH > 1 -\end{lstlisting} - -\medskip -\begin{block}{Examples for {\tt \%}-codes (see {\tt help select} for full list)} -{\tt \%u} \dotfill union of top two elements on stack -- pop 2, push 1 \\ -{\tt \%d} \dotfill difference of top two elements on stack -- pop 2, push 1 \\ -{\tt \%i} \dotfill intersection of top two elements on stack -- pop 2, push 1 \\ -{\tt \%n} \dotfill inverse of top element on stack -- pop 1, push 1 \\ -\end{block} -\end{frame} - -\subsubsection{Expanding selections} - -\begin{frame}[fragile]{\subsubsecname} -Selections of cells and wires can be expanded along connections using {\tt \%}-codes -for selecting input cones ({\tt \%ci}), output cones ({\tt \%co}), or both ({\tt \%x}). - -\medskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -# select all wires that are inputs to $add cells -select t:$add %ci w:* %i -\end{lstlisting} - -\bigskip -Additional constraints such as port names can be specified. - -\medskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -# select all wires that connect a "Q" output with a "D" input -select c:* %co:+[Q] w:* %i c:* %ci:+[D] w:* %i %i - -# select the multiplexer tree that drives the signal 'state' -select state %ci*:+$mux,$pmux[A,B,Y] -\end{lstlisting} - -\bigskip -See {\tt help select} for full documentation of this expressions. -\end{frame} - -\subsubsection{Incremental selection} - -\begin{frame}[fragile]{\subsubsecname} -Sometimes a selection can most easily be described by a series of add/delete operations. -The commands {\tt select -add} and {\tt select -del} respectively add or remove objects -from the current selection instead of overwriting it. - -\medskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -select -none # start with an empty selection -select -add reg_* # select a bunch of objects -select -del reg_42 # but not this one -select -add state %ci # and add mor stuff -\end{lstlisting} - -\bigskip -Within a select expression the token {\tt \%} can be used to push the previous selection -on the stack. - -\medskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -select t:$add t:$sub # select all $add and $sub cells -select % %ci % %d # select only the input wires to those cells -\end{lstlisting} -\end{frame} - -\subsubsection{Creating selection variables} - -\begin{frame}[fragile]{\subsubsecname} -Selections can be stored under a name with the {\tt select -set } -command. The stored selections can be used in later select expressions -using the syntax {\tt @}. - -\medskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -select -set cone_a state_a %ci*:-$dff # set @cone_a to the input cone of state_a -select -set cone_b state_b %ci*:-$dff # set @cone_b to the input cone of state_b -select @cone_a @cone_b %i # select the objects that are in both cones -\end{lstlisting} - -\bigskip -Remember that select expressions can also be used directly as arguments to most -commands. Some commands also except a single select argument to some options. -In those cases selection variables must be used to capture more complex selections. - -\medskip -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -dump @cone_a @cone_b - -select -set cone_ab @cone_a @cone_b %i -show -color red @cone_ab -color magenta @cone_a -color blue @cone_b -\end{lstlisting} -\end{frame} - -\begin{frame}[fragile]{\subsubsecname{} -- Example} -\begin{columns} -\column[t]{4cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{6pt}{7pt}\selectfont, language=verilog]{PRESENTATION_ExAdv/select.v} -\column[t]{7cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single]{PRESENTATION_ExAdv/select.ys} -\end{columns} -\hfil\includegraphics[width=\linewidth,trim=0 0cm 0 0cm]{PRESENTATION_ExAdv/select.pdf} -\end{frame} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{Advanced uses of techmap} - -\begin{frame} -\subsectionpage -\subsectionpagesuffix -\end{frame} - -\subsubsection{Introduction to techmap} - -\begin{frame}{\subsubsecname} -\begin{itemize} -\item -The {\tt techmap} command replaces cells in the design with implementations given -as Verilog code (called ``map files''). It can replace Yosys' internal cell -types (such as {\tt \$or}) as well as user-defined cell types. -\medskip\item -Verilog parameters are used extensively to customize the internal cell types. -\medskip\item -Additional special parameters are used by techmap to communicate meta-data to the -map files. -\medskip\item -Special wires are used to instruct techmap how to handle a module in the map file. -\medskip\item -Generate blocks and recursion are powerful tools for writing map files. -\end{itemize} -\end{frame} - -\begin{frame}[t]{\subsubsecname{} -- Example 1/2} -\vskip-0.2cm -To map the Verilog OR-reduction operator to 3-input OR gates: -\vskip-0.2cm -\begin{columns} -\column[t]{0.35\linewidth} -\lstinputlisting[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, lastline=24]{PRESENTATION_ExAdv/red_or3x1_map.v} -\column[t]{0.65\linewidth} -\lstinputlisting[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, firstline=25]{PRESENTATION_ExAdv/red_or3x1_map.v} -\end{columns} -\end{frame} - -\begin{frame}[t]{\subsubsecname{} -- Example 2/2} -\vbox to 0cm{ -\hfil\includegraphics[width=10cm,trim=0 0cm 0 0cm]{PRESENTATION_ExAdv/red_or3x1.pdf} -\vss -} -\begin{columns} -\column[t]{6cm} -\column[t]{4cm} -\vskip-0.6cm\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, firstline=4, lastline=4, frame=single]{PRESENTATION_ExAdv/red_or3x1_test.ys} -\vskip-0.2cm\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=verilog]{PRESENTATION_ExAdv/red_or3x1_test.v} -\end{columns} -\end{frame} - -\subsubsection{Conditional techmap} - -\begin{frame}{\subsubsecname} -\begin{itemize} -\item In some cases only cells with certain properties should be substituted. -\medskip -\item The special wire {\tt \_TECHMAP\_FAIL\_} can be used to disable a module -in the map file for a certain set of parameters. -\medskip -\item The wire {\tt \_TECHMAP\_FAIL\_} must be set to a constant value. If it -is non-zero then the module is disabled for this set of parameters. -\medskip -\item Example use-cases: -\begin{itemize} -\item coarse-grain cell types that only operate on certain bit widths -\item memory resources for different memory geometries (width, depth, ports, etc.) -\end{itemize} -\end{itemize} -\end{frame} - -\begin{frame}[t]{\subsubsecname{} -- Example} -\vbox to 0cm{ -\vskip-0.5cm -\hfill\includegraphics[width=6cm,trim=0 0cm 0 0cm]{PRESENTATION_ExAdv/sym_mul.pdf} -\vss -} -\vskip-0.5cm -\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=verilog]{PRESENTATION_ExAdv/sym_mul_map.v} -\begin{columns} -\column[t]{6cm} -\vskip-0.5cm\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=verilog]{PRESENTATION_ExAdv/sym_mul_test.v} -\column[t]{4cm} -\vskip-0.5cm\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=ys, lastline=4]{PRESENTATION_ExAdv/sym_mul_test.ys} -\end{columns} -\end{frame} - -\subsubsection{Scripting in map modules} - -\begin{frame}{\subsubsecname} -\begin{itemize} -\item The special wires {\tt \_TECHMAP\_DO\_*} can be used to run Yosys scripts -in the context of the replacement module. -\medskip -\item The wire that comes first in alphabetical oder is interpreted as string (must -be connected to constants) that is executed as script. Then the wire is removed. Repeat. -\medskip -\item You can even call techmap recursively! -\medskip -\item Example use-cases: -\begin{itemize} -\item Using always blocks in map module: call {\tt proc} -\item Perform expensive optimizations (such as {\tt freduce}) on cells where -this is known to work well. -\item Interacting with custom commands. -\end{itemize} -\end{itemize} - -\scriptsize -PROTIP: Commands such as {\tt shell}, {\tt show -pause}, and {\tt dump} can be use -in the {\tt \_TECHMAP\_DO\_*} scripts for debugging map modules. -\end{frame} - -\begin{frame}[t]{\subsubsecname{} -- Example} -\vbox to 0cm{ -\vskip4.2cm -\hskip0.5cm\includegraphics[width=10cm,trim=0 0cm 0 0cm]{PRESENTATION_ExAdv/mymul.pdf} -\vss -} -\vskip-0.6cm -\begin{columns} -\column[t]{6cm} -\vskip-0.6cm -\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=verilog]{PRESENTATION_ExAdv/mymul_map.v} -\column[t]{4.2cm} -\vskip-0.6cm -\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=verilog]{PRESENTATION_ExAdv/mymul_test.v} -\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=ys, lastline=5]{PRESENTATION_ExAdv/mymul_test.ys} -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, frame=single, language=ys, firstline=7, lastline=12]{PRESENTATION_ExAdv/mymul_test.ys} -\end{columns} -\end{frame} - -\subsubsection{Handling constant inputs} - -\begin{frame}{\subsubsecname} -\begin{itemize} -\item The special parameters {\tt \_TECHMAP\_CONSTMSK\_\it \tt \_} and -{\tt \_TECHMAP\_CONSTVAL\_\it \tt \_} can be used to handle constant -input values to cells. -\medskip -\item The former contains 1-bits for all constant input bits on the port. -\medskip -\item The latter contains the constant bits or undef (x) for non-constant bits. -\medskip -\item Example use-cases: -\begin{itemize} -\item Converting arithmetic (for example multiply to shift) -\item Identify constant addresses or enable bits in memory interfaces. -\end{itemize} -\end{itemize} -\end{frame} - -\begin{frame}[t]{\subsubsecname{} -- Example} -\vbox to 0cm{ -\vskip5.2cm -\hskip6.5cm\includegraphics[width=5cm,trim=0 0cm 0 0cm]{PRESENTATION_ExAdv/mulshift.pdf} -\vss -} -\vskip-0.6cm -\begin{columns} -\column[t]{6cm} -\vskip-0.4cm -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog]{PRESENTATION_ExAdv/mulshift_map.v} -\column[t]{4.2cm} -\vskip-0.6cm -\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=verilog]{PRESENTATION_ExAdv/mulshift_test.v} -\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=ys, lastline=5]{PRESENTATION_ExAdv/mulshift_test.ys} -\end{columns} -\end{frame} - -\subsubsection{Handling shorted inputs} - -\begin{frame}{\subsubsecname} -\begin{itemize} -\item The special parameters {\tt \_TECHMAP\_BITS\_CONNMAP\_} and -{\tt \_TECHMAP\_CONNMAP\_\it \tt \_} can be used to handle shorted inputs. -\medskip -\item Each bit of the port correlates to an {\tt \_TECHMAP\_BITS\_CONNMAP\_} bits wide -number in {\tt \_TECHMAP\_CONNMAP\_\it \tt \_}. -\medskip -\item Each unique signal bit is assigned its own number. Identical fields in the {\tt -\_TECHMAP\_CONNMAP\_\it \tt \_} parameters mean shorted signal bits. -\medskip -\item The numbers 0-3 are reserved for {\tt 0}, {\tt 1}, {\tt x}, and {\tt z} respectively. -\medskip -\item Example use-cases: -\begin{itemize} -\item Detecting shared clock or control signals in memory interfaces. -\item In some cases this can be used for for optimization. -\end{itemize} -\end{itemize} -\end{frame} - -\begin{frame}[t]{\subsubsecname{} -- Example} -\vbox to 0cm{ -\vskip4.5cm -\hskip6.5cm\includegraphics[width=5cm,trim=0 0cm 0 0cm]{PRESENTATION_ExAdv/addshift.pdf} -\vss -} -\vskip-0.6cm -\begin{columns} -\column[t]{6cm} -\vskip-0.4cm -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog]{PRESENTATION_ExAdv/addshift_map.v} -\column[t]{4.2cm} -\vskip-0.6cm -\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=verilog]{PRESENTATION_ExAdv/addshift_test.v} -\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=ys, lastline=5]{PRESENTATION_ExAdv/addshift_test.ys} -\end{columns} -\end{frame} - -\subsubsection{Notes on using techmap} - -\begin{frame}{\subsubsecname} -\begin{itemize} -\item Don't use positional cell parameters in map modules. -\medskip -\item Don't try to implement basic logic optimization with techmap. \\ -{\small (So the OR-reduce using OR3X1 cells map was actually a bad example.)} -\medskip -\item You can use the {\tt \$\_\,\_}-prefix for internal cell types to avoid -collisions with the user-namespace. But always use two underscores or the -internal consistency checker will trigger on this cells. -\medskip -\item Techmap has two major use cases: -\begin{itemize} -\item Creating good logic-level representation of arithmetic functions. \\ -This also means using dedicated hardware resources such as half- and full-adder -cells in ASICS or dedicated carry logic in FPGAs. -\smallskip -\item Mapping of coarse-grain resources such as block memory or DSP cells. -\end{itemize} -\end{itemize} -\end{frame} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{Coarse-grain synthesis} - -\begin{frame} -\subsectionpage -\subsectionpagesuffix -\end{frame} - -\subsubsection{Intro to coarse-grain synthesis} - -\begin{frame}[fragile]{\subsubsecname} -In coarse-grain synthesis the target architecture has cells of the same -complexity or larger complexity than the internal RTL representation. - -For example: -\begin{lstlisting}[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=verilog] - wire [15:0] a, b; - wire [31:0] c, y; - assign y = a * b + c; -\end{lstlisting} - -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. - -\bigskip -Fine-grain synthesis would be matching the circuit elements to smaller -components, such as LUTs, gates, or half- and full-adders. -\end{frame} - -\subsubsection{The extract pass} - -\begin{frame}{\subsubsecname} -\begin{itemize} -\item Like the {\tt techmap} pass, the {\tt 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. -\bigskip -\item If a match is found, the {\tt extract} pass will replace the matching -subcircuit with an instance of the module from the map file. -\bigskip -\item In a way the {\tt extract} pass is the inverse of the techmap pass. -\end{itemize} -\end{frame} - -\begin{frame}[t, fragile]{\subsubsecname{} -- Example 1/2} -\vbox to 0cm{ -\vskip2cm -\begin{tikzpicture} - \node at (0,0) {\includegraphics[width=5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_simple_test_00a.pdf}}; - \node at (3,-3) {\includegraphics[width=8cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_simple_test_00b.pdf}}; - \draw[yshift=0.2cm,thick,-latex] (1,-1) -- (2,-2); -\end{tikzpicture} -\vss} -\vskip-1.2cm -\begin{columns} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=verilog]{PRESENTATION_ExAdv/macc_simple_test.v} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=verilog]{PRESENTATION_ExAdv/macc_simple_xmap.v} -\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=ys] -read_verilog macc_simple_test.v -hierarchy -check -top test - -extract -map macc_simple_xmap.v;; -\end{lstlisting} -\end{columns} -\end{frame} - -\begin{frame}[fragile]{\subsubsecname{} -- Example 2/2} -\hfil\begin{tabular}{cc} -\fbox{\hbox to 5cm {\lstinputlisting[linewidth=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=verilog]{PRESENTATION_ExAdv/macc_simple_test_01.v}}} & -\fbox{\hbox to 5cm {\lstinputlisting[linewidth=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=verilog]{PRESENTATION_ExAdv/macc_simple_test_02.v}}} \\ -$\downarrow$ & $\downarrow$ \\ -\fbox{\includegraphics[width=5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_simple_test_01a.pdf}} & -\fbox{\includegraphics[width=5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_simple_test_02a.pdf}} \\ -$\downarrow$ & $\downarrow$ \\ -\fbox{\includegraphics[width=5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_simple_test_01b.pdf}} & -\fbox{\includegraphics[width=5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_simple_test_02b.pdf}} \\ -\end{tabular} -\end{frame} - -\subsubsection{The wrap-extract-unwrap method} - -\begin{frame}{\subsubsecname} -\scriptsize -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. - -\bigskip -A way of mapping such elements in coarse grain synthesis is the wrap-extract-unwrap method: - -\begin{itemize} -\item {\bf wrap} \\ -Identify candidate-cells in the circuit and wrap them in a cell with a constant -wider bit-width using {\tt 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 {\tt connwrappers} command to connect up the bit-extended in- and -outputs of the wrapper cells. -\item {\bf extract} \\ -Now all operations are encoded using the same bit-width as the coarse grain element. The {\tt -extract} command can be used to replace circuits with cells of the target architecture. -\item {\bf unwrap} \\ -The remaining wrapper cell can be unwrapped using {\tt techmap}. -\end{itemize} - -\bigskip -The following sides detail 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). -\end{frame} - -\subsubsection{Example: DSP48\_MACC} - -\begin{frame}[t, fragile]{\subsubsecname{} -- 1/13} -Preconditioning: {\tt macc\_xilinx\_swap\_map.v} \\ -Make sure {\tt A} is the smaller port on all multipliers - -\begin{columns} -\column{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, lastline=15]{PRESENTATION_ExAdv/macc_xilinx_swap_map.v} -\column{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, firstline=16]{PRESENTATION_ExAdv/macc_xilinx_swap_map.v} -\end{columns} -\end{frame} - -\begin{frame}[t, fragile]{\subsubsecname{} -- 2/13} -Wrapping multipliers: {\tt macc\_xilinx\_wrap\_map.v} - -\begin{columns} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, lastline=23]{PRESENTATION_ExAdv/macc_xilinx_wrap_map.v} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, firstline=24, lastline=46]{PRESENTATION_ExAdv/macc_xilinx_wrap_map.v} -\end{columns} -\end{frame} - -\begin{frame}[t, fragile]{\subsubsecname{} -- 3/13} -Wrapping adders: {\tt macc\_xilinx\_wrap\_map.v} - -\begin{columns} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, firstline=48, lastline=67]{PRESENTATION_ExAdv/macc_xilinx_wrap_map.v} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, firstline=68, lastline=89]{PRESENTATION_ExAdv/macc_xilinx_wrap_map.v} -\end{columns} -\end{frame} - -\begin{frame}[t, fragile]{\subsubsecname{} -- 4/13} -Extract: {\tt macc\_xilinx\_xmap.v} - -\lstinputlisting[xleftmargin=0.5cm, basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, firstline=1, lastline=17]{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 {\tt extract} command. -\end{frame} - -\begin{frame}[t, fragile]{\subsubsecname{} -- 5/13} -Unwrapping multipliers: {\tt macc\_xilinx\_unwrap\_map.v} - -\begin{columns} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, firstline=1, lastline=17]{PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, firstline=18, lastline=30]{PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v} -\end{columns} -\end{frame} - -\begin{frame}[t, fragile]{\subsubsecname{} -- 6/13} -Unwrapping adders: {\tt macc\_xilinx\_unwrap\_map.v} - -\begin{columns} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, firstline=32, lastline=48]{PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{7pt}{8pt}\selectfont, language=verilog, firstline=49, lastline=61]{PRESENTATION_ExAdv/macc_xilinx_unwrap_map.v} -\end{columns} -\end{frame} - -\begin{frame}[fragile]{\subsubsecname{} -- 7/13} -\hfil\begin{tabular}{cc} -{\tt test1} & {\tt test2} \\ -\fbox{\hbox to 5cm {\lstinputlisting[linewidth=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, firstline=1, lastline=6, language=verilog]{PRESENTATION_ExAdv/macc_xilinx_test.v}}} & -\fbox{\hbox to 5cm {\lstinputlisting[linewidth=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, firstline=8, lastline=13, language=verilog]{PRESENTATION_ExAdv/macc_xilinx_test.v}}} \\ -$\downarrow$ & $\downarrow$ \\ -\end{tabular} -\vskip-0.5cm -\begin{lstlisting}[linewidth=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] - read_verilog macc_xilinx_test.v - hierarchy -check -\end{lstlisting} -\vskip-0.5cm -\hfil\begin{tabular}{cc} -$\downarrow$ & $\downarrow$ \\ -\fbox{\includegraphics[width=5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test1a.pdf}} & -\fbox{\includegraphics[width=5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2a.pdf}} \\ -\end{tabular} -\end{frame} - -\begin{frame}[fragile]{\subsubsecname{} -- 8/13} -\hfil\begin{tabular}{cc} -{\tt test1} & {\tt test2} \\ -\fbox{\includegraphics[width=5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test1a.pdf}} & -\fbox{\includegraphics[width=5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2a.pdf}} \\ -$\downarrow$ & $\downarrow$ \\ -\end{tabular} -\vskip-0.2cm -\begin{lstlisting}[linewidth=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] - techmap -map macc_xilinx_swap_map.v ;; -\end{lstlisting} -\vskip-0.2cm -\hfil\begin{tabular}{cc} -$\downarrow$ & $\downarrow$ \\ -\fbox{\includegraphics[width=5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test1b.pdf}} & -\fbox{\includegraphics[width=5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2b.pdf}} \\ -\end{tabular} -\end{frame} - -\begin{frame}[t, fragile]{\subsubsecname{} -- 9/13} -Wrapping in {\tt test1}: -\begin{columns} -\column[t]{5cm} -\vbox to 0cm{\fbox{\includegraphics[width=4.5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test1b.pdf}}\vss} -\column[t]{6cm} -\begin{lstlisting}[linewidth=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -techmap -map macc_xilinx_wrap_map.v - -connwrappers -unsigned $__mul_wrapper \ - Y Y_WIDTH \ - -unsigned $__add_wrapper \ - Y Y_WIDTH ;; -\end{lstlisting} -\end{columns} - -\vskip1cm -\hfil\includegraphics[width=\linewidth,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test1c.pdf} -\end{frame} - -\begin{frame}[t, fragile]{\subsubsecname{} -- 10/13} -Wrapping in {\tt test2}: -\begin{columns} -\column[t]{5cm} -\vbox to 0cm{\fbox{\includegraphics[width=4.5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2b.pdf}}\vss} -\column[t]{6cm} -\begin{lstlisting}[linewidth=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -techmap -map macc_xilinx_wrap_map.v - -connwrappers -unsigned $__mul_wrapper \ - Y Y_WIDTH \ - -unsigned $__add_wrapper \ - Y Y_WIDTH ;; -\end{lstlisting} -\end{columns} - -\vskip1cm -\hfil\includegraphics[width=\linewidth,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2c.pdf} -\end{frame} - -\begin{frame}[t, fragile]{\subsubsecname{} -- 11/13} -Extract in {\tt test1}: -\begin{columns} -\column[t]{4.5cm} -\vbox to 0cm{ -\begin{lstlisting}[linewidth=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -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 -\end{lstlisting} -\vss} -\column[t]{5.5cm} -\vskip-1cm -\begin{lstlisting}[linewidth=5.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -extract -constports -ignore_parameters \ - -map %__macc_xilinx_xmap \ - -swap $__add_wrapper A,B ;; -\end{lstlisting} -\vbox to 0cm{\fbox{\includegraphics[width=4.5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test1c.pdf}}\vss} -\end{columns} - -\vskip2cm -\hfil\includegraphics[width=11cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test1d.pdf} -\end{frame} - -\begin{frame}[t, fragile]{\subsubsecname{} -- 12/13} -Extract in {\tt test2}: -\begin{columns} -\column[t]{4.5cm} -\vbox to 0cm{ -\begin{lstlisting}[linewidth=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -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 -\end{lstlisting} -\vss} -\column[t]{5.5cm} -\vskip-1cm -\begin{lstlisting}[linewidth=5.5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -extract -constports -ignore_parameters \ - -map %__macc_xilinx_xmap \ - -swap $__add_wrapper A,B ;; -\end{lstlisting} -\vbox to 0cm{\fbox{\includegraphics[width=4.5cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2c.pdf}}\vss} -\end{columns} - -\vskip2cm -\hfil\includegraphics[width=11cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2d.pdf} -\end{frame} - -\begin{frame}[t, fragile]{\subsubsecname{} -- 13/13} -Unwrap in {\tt test2}: - -\hfil\begin{tikzpicture} -\node at (0,0) {\includegraphics[width=11cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2d.pdf}}; -\node at (0,-4) {\includegraphics[width=8cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2e.pdf}}; -\node at (1,-1.7) {\begin{lstlisting}[linewidth=5.5cm, frame=single, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -techmap -map macc_xilinx_unwrap_map.v ;; -\end{lstlisting}}; -\draw[-latex] (4,-0.7) .. controls (5,-1.7) .. (4,-2.7); -\end{tikzpicture} -\end{frame} - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Automatic design changes} diff --git a/manual/PRESENTATION_ExOth.tex b/manual/PRESENTATION_ExOth.tex deleted file mode 100644 index 3f5113e3c..000000000 --- a/manual/PRESENTATION_ExOth.tex +++ /dev/null @@ -1,227 +0,0 @@ - -\section{Yosys by example -- Beyond Synthesis} - -\begin{frame} -\sectionpage -\end{frame} - -\begin{frame}{Overview} -This section contains 2 subsections: -\begin{itemize} -\item Interactive Design Investigation -\item Symbolic Model Checking -\end{itemize} -\end{frame} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{Interactive Design Investigation} - -\begin{frame} -\subsectionpage -\subsectionpagesuffix -\end{frame} - -\begin{frame}{\subsecname} -Yosys can also be used to investigate designs (or netlists created -from other tools). - -\begin{itemize} -\item -The selection mechanism (see slides ``Using Selections''), especially patterns such -as {\tt \%ci} and {\tt \%co}, can be used to figure out how parts of the design -are connected. - -\item -Commands such as {\tt submod}, {\tt expose}, {\tt splice}, \dots can be used -to transform the design into an equivalent design that is easier to analyse. - -\item -Commands such as {\tt eval} and {\tt sat} can be used to investigate the -behavior of the circuit. -\end{itemize} -\end{frame} - -\begin{frame}[t, fragile]{Example: Reorganizing a module} -\begin{columns} -\column[t]{4cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{6pt}{7pt}\selectfont, language=verilog]{PRESENTATION_ExOth/scrambler.v} -\column[t]{7cm} -\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single] -read_verilog scrambler.v - -hierarchy; proc;; - -cd scrambler -submod -name xorshift32 \ - xs %c %ci %D %c %ci:+[D] %D \ - %ci*:-$dff xs %co %ci %d -\end{lstlisting} -\end{columns} - -\hfil\includegraphics[width=11cm,trim=0 0cm 0 1.5cm]{PRESENTATION_ExOth/scrambler_p01.pdf} - -\hfil\includegraphics[width=11cm,trim=0 0cm 0 2cm]{PRESENTATION_ExOth/scrambler_p02.pdf} -\end{frame} - -\begin{frame}[t, fragile]{Example: Analysis of circuit behavior} -\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] -> read_verilog scrambler.v -> hierarchy; proc;; cd scrambler -> submod -name xorshift32 xs %c %ci %D %c %ci:+[D] %D %ci*:-$dff xs %co %ci %d - -> cd xorshift32 -> rename n2 in -> rename n1 out - -> eval -set in 1 -show out -Eval result: \out = 270369. - -> eval -set in 270369 -show out -Eval result: \out = 67634689. - -> sat -set out 632435482 -Signal Name Dec Hex Bin --------------------- ---------- ---------- ------------------------------------- -\in 745495504 2c6f5bd0 00101100011011110101101111010000 -\out 632435482 25b2331a 00100101101100100011001100011010 -\end{lstlisting} -\end{frame} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{Symbolic Model Checking} - -\begin{frame} -\subsectionpage -\subsectionpagesuffix -\end{frame} - -\begin{frame}{\subsecname} -Symbolic Model Checking (SMC) is used to formally prove that a circuit has -(or has not) a given property. - -\bigskip -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. - -\bigskip -Other applications include checking if a module conforms to interface -standards. - -\bigskip -The {\tt sat} command in Yosys can be used to perform Symbolic Model Checking. -\end{frame} - -\begin{frame}[t]{Example: Formal Equivalence Checking (1/2)} -Remember the following example? -\vskip1em - -\vbox to 0cm{ -\vskip-0.3cm -\lstinputlisting[basicstyle=\ttfamily\fontsize{6pt}{7pt}\selectfont, language=verilog]{PRESENTATION_ExSyn/techmap_01_map.v} -}\vbox to 0cm{ -\vskip-0.5cm -\lstinputlisting[xleftmargin=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, frame=single, language=verilog]{PRESENTATION_ExSyn/techmap_01.v} -\lstinputlisting[xleftmargin=5cm, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single]{PRESENTATION_ExSyn/techmap_01.ys}} - -\vskip5cm\hskip5cm -Lets see if it is correct.. -\end{frame} - -\begin{frame}[t, fragile]{Example: Formal Equivalence Checking (2/2)} -\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single] -# 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 -\end{lstlisting} - -\dots -\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont] -Solving problem with 945 variables and 2505 clauses.. -SAT proof finished - no model found: SUCCESS! -\end{lstlisting} -\end{frame} - -\begin{frame}[t, fragile]{Example: Symbolic Model Checking (1/2)} -\small -The following AXI4 Stream Master has a bug. But the bug is not exposed if the -slave keeps {\tt tready} asserted all the time. (Something a test bench might do.) - -\medskip -Symbolic Model Checking can be used to expose the bug and find a sequence -of values for {\tt tready} that yield the incorrect behavior. - -\vskip-1em -\begin{columns} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{5pt}{6pt}\selectfont, language=verilog]{PRESENTATION_ExOth/axis_master.v} -\column[t]{5cm} -\lstinputlisting[basicstyle=\ttfamily\fontsize{5pt}{6pt}\selectfont, language=verilog]{PRESENTATION_ExOth/axis_test.v} -\end{columns} -\end{frame} - -\begin{frame}[t, fragile]{Example: Symbolic Model Checking (2/2)} -\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys, frame=single] -read_verilog -sv axis_master.v axis_test.v -hierarchy -top axis_test - -proc; flatten;; -sat -seq 50 -prove-asserts -\end{lstlisting} - -\bigskip -\dots with unmodified {\tt axis\_master.v}: -\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont] -Solving problem with 159344 variables and 442126 clauses.. -SAT proof finished - model found: FAIL! -\end{lstlisting} - -\bigskip -\dots with fixed {\tt axis\_master.v}: -\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont] -Solving problem with 159144 variables and 441626 clauses.. -SAT proof finished - no model found: SUCCESS! -\end{lstlisting} -\end{frame} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{Summary} - -\begin{frame}{\subsecname} -\begin{itemize} -\item Yosys provides useful features beyond synthesis. -\item The commands {\tt sat} and {\tt eval} can be used to analyse the behavior of a circuit. -\item The {\tt sat} command can also be used for symbolic model checking. -\item This can be useful for debugging and testing designs and Yosys extensions alike. -\end{itemize} - -\bigskip -\bigskip -\begin{center} -Questions? -\end{center} - -\bigskip -\bigskip -\begin{center} -\url{https://yosyshq.net/yosys/} -\end{center} -\end{frame} - diff --git a/manual/PRESENTATION_ExOth/.gitignore b/manual/PRESENTATION_ExOth/.gitignore deleted file mode 100644 index cf658897d..000000000 --- a/manual/PRESENTATION_ExOth/.gitignore +++ /dev/null @@ -1 +0,0 @@ -*.dot