docs/source/autotune.rst

   1 Autotune: Automatic Engine Selection
   2 ====================================
   3
   4 Selecting the best performing engine for a given verification task often
   5 requires some amount of trial and error. To reduce the manual work required for
   6 this, sby offers the ``--autotune`` option which takes an ``.sby`` file and
   7 runs it using engines and engine configurations. At the end it produces a
   8 report listing the fastest engines among these candidates.
   9
  10 Using Autotune
  11 --------------
  12
  13 To run autotune, you can add the ``--autotune`` option to your usual sby
  14 invokation. For example if you usually run ``sby demo.sby`` you would run ``sby
  15 --autotune demo.sby`` instead. When the ``.sby`` file contains multiple tasks,
  16 autotune is run for each task independently. As without ``--autotune``, it is
  17 possible to specify which tasks to run on the command line.
  18
  19 Autotune runs without requiring further interaction and will eventually print a
  20 list of engine configurations and their respective solving times. To
  21 permanently use an engine configuration you can copy if from the ``sby
  22 --autotune`` output into the ``[engines]`` section of your ``.sby`` file.
  23
  24 Autotune Log Output
  25 -------------------
  26
  27 The log output in ``--autotune`` mode differs from the usual sby log output.
  28
  29 It also starts with preparing the design (this includes running the user
  30 provided ``[script]``) so it can be passed to the solvers. This is only done
  31 once and will be reused to run every candidate engine.
  32
  33 .. code-block:: text
  34
  35    SBY [demo] model 'base': preparing now...
  36    SBY [demo] base: starting process "cd demo/src; yosys -ql ../model/design.log ../model/design.ys"
  37    SBY [demo] base: finished (returncode=0)
  38    SBY [demo] prepared model 'base'
  39
  40 This is followed by selecting the engine candidates to run. For this the design
  41 and sby configuration are analyzed to skip engines that are not compatible or
  42 unlikely to work well. When engines is skipped due to a recommendation, a
  43 corresponding log message is displayed as well as the total number of
  44 candidates to try:
  45
  46 .. code-block:: text
  47
  48    SBY [demo] checking more than 20 timesteps (100), disabling nonincremental smtbmc
  49    SBY [demo] testing 16 engine configurations...
  50
  51 After this, the candidate engine configurations are started. Depending on the
  52 configuration engines can run in parallel. The engine output itself is not
  53 logged to stdout when running autotune, so you will only see messages about
  54 starting an engine:
  55
  56 .. code-block:: text
  57
  58    SBY [demo] engine_1 (smtbmc --nopresat boolector): starting... (14 configurations pending)
  59    SBY [demo] engine_2 (smtbmc bitwuzla): starting... (13 configurations pending)
  60    SBY [demo] engine_3 (smtbmc --nopresat bitwuzla): starting... (12 configurations pending)
  61    ...
  62
  63 The engine log that would normally be printed is instead redirected to files
  64 named ``engine_*_autotune.txt`` within sby's working directory.
  65
  66 To run an engine, further preparation steps may be necessary. These are cached
  67 and will be reused for every engine requiring them, while properly accounting
  68 for the required prepration time. Below is an example of the log output
  69 produced by such a preparation step. Note that this runs in parallel, so it may
  70 be interspersed with other log output.
  71
  72 .. code-block:: text
  73
  74    SBY [demo] model 'smt2': preparing now...
  75    SBY [demo] smt2: starting process "cd demo/model; yosys -ql design_smt2.log design_smt2.ys"
  76    ...
  77    SBY [demo] smt2: finished (returncode=0)
  78    SBY [demo] prepared model 'smt2'
  79
  80 Whenever an engine finishes a log message is printed:
  81
  82 .. code-block:: text
  83
  84    SBY [demo] engine_4 (smtbmc --unroll yices): succeeded (status=PASS)
  85    SBY [demo] engine_4 (smtbmc --unroll yices): took 30 seconds (first engine to finish)
  86
  87 When an engine takes longer than the current hard timeout, it is stopped:
  88
  89 .. code-block:: text
  90
  91    SBY [demo] engine_2 (smtbmc bitwuzla): timeout (150 seconds)
  92
  93 Depending on the configuration, autotune will also stop an engine earlier when
  94 reaching a soft timeout. In that case, when no other engine finishes in less
  95 time, the engine will be retried later with a longer soft timeout:
  96
  97 .. code-block:: text
  98
  99    SBY [demo] engine_0 (smtbmc boolector): timeout (60 seconds, will be retried if necessary)
 100
 101
 102 Finally at the end a summary of all finished engines is printed, sorted by
 103 their solving time:
 104
 105 .. code-block:: text
 106
 107    SBY [demo] finished engines:
 108    SBY [demo]   #3: engine_1: smtbmc --nopresat boolector (52 seconds, status=PASS)
 109    SBY [demo]   #2: engine_5: smtbmc --nopresat --unroll yices (41 seconds, status=PASS)
 110    SBY [demo]   #1: engine_4: smtbmc --unroll yices (30 seconds, status=PASS)
 111    SBY [demo] DONE (AUTOTUNED, rc=0)
 112
 113 If any tried engine encounters an error or produces an unexpected result,
 114 autotune will also output a list of failed engines. Note that when the sby file
 115 does not contain the ``expect`` option, autotune defaults to ``expect
 116 pass,fail`` to simplify running autotune on a verification task with a
 117 currently unknown outcome.
 118
 119 Configuring Autotune
 120 --------------------
 121
 122 Autotune can be configured by adding an ``[autotune]`` section to the ``.sby``
 123 file. Each line in that section has the form ``option_name value``, the
 124 possible options and their supported values are described below. In addition
 125 the ``--autotune-config`` command line option can be used to specify a file
 126 containing further autotune options, using the same syntax. When both are used,
 127 the command line option takes precedence. This makes it easy to run autotune
 128 with existing ``.sby`` files without having to modify them.
 129
 130 Autotune Options
 131 ----------------
 132
 133 +--------------------+------------------------------------------------------+
 134 | Autotune Option    | Description                                          |
 135 +====================+======================================================+
 136 | ``timeout``        | Set a different timeout value (in seconds) used only |
 137 |                    | for autotune. The value ``none`` can be used to      |
 138 |                    | disable the timeout. Default: uses the non-autotune  |
 139 |                    | timeout option.                                      |
 140 +--------------------+------------------------------------------------------+
 141 | ``soft_timeout``   | Initial timeout value (in seconds) used to interrupt |
 142 |                    | a candidate engine when other candidates are         |
 143 |                    | pending. Increased every time a candidate is retried |
 144 |                    | to ensure progress. Default: ``60``                  |
 145 +--------------------+------------------------------------------------------+
 146 | ``wait``           | Additional time to wait past the time taken by the   |
 147 |                    | fastest finished engine candidate so far. Can be an  |
 148 |                    | absolute time in seconds, a percentage of the        |
 149 |                    | fastest candidate or a sum of both.                  |
 150 |                    | Default: ``50%+10``                                  |
 151 +--------------------+------------------------------------------------------+
 152 | ``parallel``       | Maximal number of engine candidates to try in        |
 153 |                    | parallel. When set to ``auto``, the number of        |
 154 |                    | available CPUs is used. Default: ``auto``            |
 155 +--------------------+------------------------------------------------------+
 156 | ``presat``         | Filter candidates by whether they perform a presat   |
 157 |                    | check. Values ``on``, ``off``, ``any``.              |
 158 |                    | Default: ``any``                                     |
 159 +--------------------+------------------------------------------------------+
 160 | ``incr``           | Filter candidates by whether they use incremental    |
 161 |                    | solving (when applicable). Values ``on``, ``off``,   |
 162 |                    | ``any``, ``auto`` (see next option).                 |
 163 |                    | Default: ``auto``                                    |
 164 +--------------------+------------------------------------------------------+
 165 | ``incr_threshold`` | Number of timesteps required to only consider        |
 166 |                    | incremental solving when ``incr`` is set to          |
 167 |                    | ``auto``. Default: ``20``                            |
 168 +--------------------+------------------------------------------------------+
 169 | ``mem``            | Filter candidates by whether they have native        |
 170 |                    | support for memory. Values ``on``, ``any``, ``auto`` |
 171 |                    | (see next option). Default: ``auto``                 |
 172 +--------------------+------------------------------------------------------+
 173 | ``mem_threshold``  | Number of memory bits required to only consider      |
 174 |                    | candidates with native memory support when ``mem``   |
 175 |                    | is set to ``auto``. Default: ``10240``               |
 176 +--------------------+------------------------------------------------------+
 177 | ``forall``         | Filter candidates by whether they support            |
 178 |                    | ``$allconst``/``$allseq``. Values ``on``, ``any``,   |
 179 |                    | ``auto`` (``on`` when ``$allconst``/``allseq`` are   |
 180 |                    | found in the design). Default: ``auto``              |
 181 +--------------------+------------------------------------------------------+