-
Notifications
You must be signed in to change notification settings - Fork 73
/
reference.rst
480 lines (376 loc) · 19.1 KB
/
reference.rst
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
Reference for .sby file format
==============================
A ``.sby`` file consists of sections. Each section start with a single-line
section header in square brackets. The order of sections in a ``.sby`` file
is for the most part irrelevant, but by convention the usual order is
``[tasks]``, ``[options]``, ``[engines]``, ``[script]``, and ``[files]``.
Tasks section
-------------
The optional ``[tasks]`` section can be used to configure multiple verification tasks in
a single ``.sby`` file. Each line in the ``[tasks]`` section configures one task. For example:
.. code-block:: text
[tasks]
task1 task_1_or_2 task_1_or_3
task2 task_1_or_2
task3 task_1_or_3
Each task can be assigned additional group aliases, such as ``task_1_or_2``
and ``task_1_or_3`` in the above example.
One or more tasks can be specified as additional command line arguments when
calling ``sby`` on a ``.sby`` file:
.. code-block:: text
sby example.sby task2
If no task is specified then all tasks in the ``[tasks]`` section are run.
After the ``[tasks]`` section individual lines can be specified for specific
tasks or task groups:
.. code-block:: text
[options]
task_1_or_2: mode bmc
task_1_or_2: depth 100
task3: mode prove
If the tag ``<taskname>:`` is used on a line by itself then the conditional string
extends until the next conditional block or ``--`` on a line by itself.
.. code-block:: text
[options]
task_1_or_2:
mode bmc
depth 100
task3:
mode prove
--
The tag ``~<taskname>:`` can be used for a line or block that should not be used when
the given task is active:
.. code-block:: text
[options]
~task3:
mode bmc
depth 100
task3:
mode prove
--
The following example demonstrates how to configure safety and liveness checks for all
combinations of some host implementations A and B and device implementations X and Y:
.. code-block:: text
[tasks]
prove_hAdX prove hostA deviceX
prove_hBdX prove hostB deviceX
prove_hAdY prove hostA deviceY
prove_hBdY prove hostB deviceY
live_hAdX live hostA deviceX
live_hBdX live hostB deviceX
live_hAdY live hostA deviceY
live_hBdY live hostB deviceY
[options]
prove: mode prove
live: mode live
[engines]
prove: abc pdr
live: aiger suprove
[script]
hostA: read -sv hostA.v
hostB: read -sv hostB.v
deviceX: read -sv deviceX.v
deviceY: read -sv deviceY.v
...
The ``[tasks]`` section must appear in the ``.sby`` file before the first
``<taskname>:`` or ``~<taskname>:`` tag.
The command ``sby --dumptasks <sby_file>`` prints the list of all tasks defined in
a given ``.sby`` file.
Options section
---------------
The ``[options]`` section contains lines with key-value pairs. The ``mode``
option is mandatory. The possible values for the ``mode`` option are:
========= ===========
Mode Description
========= ===========
``bmc`` Bounded model check to verify safety properties (``assert(...)`` statements)
``prove`` Unbounded model check to verify safety properties (``assert(...)`` statements)
``live`` Unbounded model check to verify liveness properties (``assert(s_eventually ...)`` statements)
``cover`` Generate set of shortest traces required to reach all cover() statements
========= ===========
..
``equiv`` Formal equivalence checking (usually to verify pre- and post-synthesis equivalence)
``synth`` Reactive Synthesis (synthesis of circuit from safety properties)
All other options have default values and thus are optional. The available
options are:
+------------------+------------+---------------------------------------------------------+
| Option | Modes | Description |
+==================+============+=========================================================+
| ``expect`` | All | Expected result as comma-separated list of the tokens |
| | | ``pass``, ``fail``, ``unknown``, ``error``, and |
| | | ``timeout``. Unexpected results yield a nonzero return |
| | | code . Default: ``pass`` |
+------------------+------------+---------------------------------------------------------+
| ``timeout`` | All | Timeout in seconds. Default: ``none`` (i.e. no timeout) |
+------------------+------------+---------------------------------------------------------+
| ``multiclock`` | All | Create a model with multiple clocks and/or asynchronous |
| | | logic. Values: ``on``, ``off``. Default: ``off`` |
+------------------+------------+---------------------------------------------------------+
| ``wait`` | All | Instead of terminating when the first engine returns, |
| | | wait for all engines to return and check for |
| | | consistency. Values: ``on``, ``off``. Default: ``off`` |
+------------------+------------+---------------------------------------------------------+
| ``aigsmt`` | All | Which SMT2 solver to use for converting AIGER witnesses |
| | | to counter example traces. Use ``none`` to disable |
| | | conversion of AIGER witnesses. Default: ``yices`` |
+------------------+------------+---------------------------------------------------------+
| ``tbtop`` | All | The top module for generated Verilog test benches, as |
| | | hierarchical path relative to the design top module. |
+------------------+------------+---------------------------------------------------------+
| ``make_model`` | All | Force generation of the named formal models. Takes a |
| | | comma-separated list of model names. For a model |
| | | ``<name>`` this will generate the |
| | | ``model/design_<name>.*`` files within the working |
| | | directory, even when not required to run the task. |
+------------------+------------+---------------------------------------------------------+
| ``smtc`` | ``bmc``, | Pass this ``.smtc`` file to the smtbmc engine. All |
| | ``prove``, | other engines are disabled when this option is used. |
| | ``cover`` | Default: None |
+------------------+------------+---------------------------------------------------------+
| ``depth`` | ``bmc``, | Depth of the bounded model check. Only the specified |
| | ``cover`` | number of cycles are considered. Default: ``20`` |
| +------------+---------------------------------------------------------+
| | ``prove`` | Depth for the k-induction performed by the ``smtbmc`` |
| | | engine. Other engines ignore this option in ``prove`` |
| | | mode. Default: ``20`` |
+------------------+------------+---------------------------------------------------------+
| ``skip`` | ``bmc``, | Skip the specified number of time steps. Only valid |
| | ``cover`` | with smtbmc engine. All other engines are disabled when |
| | | this option is used. Default: None |
+------------------+------------+---------------------------------------------------------+
| ``append`` | ``bmc``, | When generating a counter-example trace, add the |
| | ``prove``, | specified number of cycles at the end of the trace. |
| | ``cover`` | Default: ``0`` |
+------------------+------------+---------------------------------------------------------+
Engines section
---------------
The ``[engines]`` section configures which engines should be used to solve the
given problem. Each line in the ``[engines]`` section specifies one engine. When
more than one engine is specified then the result returned by the first engine
to finish is used.
Each engine configuration consists of an engine name followed by engine options,
usually followed by a solver name and solver options.
Example:
.. code-block:: text
[engines]
smtbmc --syn --nopresat z3 rewriter.cache_all=true opt.enable_sat=true
abc sim3 -W 15
In the first line ``smtbmc`` is the engine, ``--syn --nopresat`` are engine options,
``z3`` is the solver, and ``rewriter.cache_all=true opt.enable_sat=true`` are
solver options.
In the 2nd line ``abc`` is the engine, there are no engine options, ``sim3`` is the
solver, and ``-W 15`` are solver options.
The following mode/engine/solver combinations are currently supported:
+-----------+--------------------------+
| Mode | Engine |
+===========+==========================+
| ``bmc`` | ``smtbmc [all solvers]`` |
| | |
| | ``btor btormc`` |
| | |
| | ``btor pono`` |
| | |
| | ``abc bmc3`` |
| | |
| | ``abc sim3`` |
| | |
| | ``aiger smtbmc`` |
+-----------+--------------------------+
| ``prove`` | ``smtbmc [all solvers]`` |
| | |
| | ``abc pdr`` |
| | |
| | ``aiger avy`` |
| | |
| | ``aiger suprove`` |
+-----------+--------------------------+
| ``cover`` | ``smtbmc [all solvers]`` |
| | |
| | ``btor btormc`` |
+-----------+--------------------------+
| ``live`` | ``aiger suprove`` |
+-----------+--------------------------+
``smtbmc`` engine
~~~~~~~~~~~~~~~~~
The ``smtbmc`` engine supports the ``bmc``, ``prove``, and ``cover`` modes and supports
the following options:
+------------------+---------------------------------------------------------+
| Option | Description |
+==================+=========================================================+
| ``--nomem`` | Don't use the SMT theory of arrays to model memories. |
| | Instead synthesize memories to registers and address |
| | logic. |
+------------------+---------------------------------------------------------+
| ``--syn`` | Synthesize the circuit to a gate-level representation |
| | instead of using word-level SMT operators. This also |
| | runs some low-level logic optimization on the circuit. |
+------------------+---------------------------------------------------------+
| ``--stbv`` | Use large bit vectors (instead of uninterpreted |
| | functions) to represent the circuit state. |
+------------------+---------------------------------------------------------+
| ``--stdt`` | Use SMT-LIB 2.6 datatypes to represent states. |
+------------------+---------------------------------------------------------+
| ``--nopresat`` | Do not run "presat" SMT queries that make sure that |
| | assumptions are non-conflicting (and potentially |
| | warmup the SMT solver). |
+------------------+---------------------------------------------------------+
| ``--keep-going`` | In BMC mode, continue after the first failed assertion |
| | and report further failed assertions. |
+------------------+---------------------------------------------------------+
| ``--unroll``, | Disable/enable unrolling of the SMT problem. The |
| ``--nounroll`` | default value depends on the solver being used. |
+------------------+---------------------------------------------------------+
| ``--dumpsmt2`` | Write the SMT2 trace to an additional output file. |
| | (Useful for benchmarking and troubleshooting.) |
+------------------+---------------------------------------------------------+
| ``--progress`` | Enable Yosys-SMTBMC timer display. |
+------------------+---------------------------------------------------------+
Any SMT2 solver that is compatible with ``yosys-smtbmc`` can be passed as
argument to the ``smtbmc`` engine. The solver options are passed to the solver
as additional command line options.
The following solvers are currently supported by ``yosys-smtbmc``:
* yices
* boolector
* bitwuzla
* z3
* mathsat
* cvc4
* cvc5
Any additional options after ``--`` are passed to ``yosys-smtbmc`` as-is.
``btor`` engine
~~~~~~~~~~~~~~~
The ``btor`` engine supports hardware modelcheckers that accept btor2 files.
The engine supports no engine options and supports the following solvers:
+-------------------------------+---------------------------------+
| Solver | Modes |
+===============================+=================================+
| ``btormc`` | ``bmc``, ``cover`` |
+-------------------------------+---------------------------------+
| ``pono`` | ``bmc`` |
+-------------------------------+---------------------------------+
Solver options are passed to the solver as additional command line options.
``aiger`` engine
~~~~~~~~~~~~~~~~
The ``aiger`` engine is a generic front-end for hardware modelcheckers that are capable
of processing AIGER files. The engine supports no engine options and supports the following
solvers:
+-------------------------------+---------------------------------+
| Solver | Modes |
+===============================+=================================+
| ``suprove`` | ``prove``, ``live`` |
+-------------------------------+---------------------------------+
| ``avy`` | ``prove`` |
+-------------------------------+---------------------------------+
| ``aigbmc`` | ``bmc`` |
+-------------------------------+---------------------------------+
Solver options are passed to the solver as additional command line options.
``abc`` engine
~~~~~~~~~~~~~~
The ``abc`` engine is a front-end for the functionality in Berkeley ABC. It
currently supports no engine options and supports the following
solvers:
+------------+-----------------+---------------------------------+
| Solver | Modes | ABC Command |
+============+=================+=================================+
| ``bmc3`` | ``bmc`` | ``bmc3 -F <depth> -v`` |
+------------+-----------------+---------------------------------+
| ``sim3`` | ``bmc`` | ``sim3 -F <depth> -v`` |
+------------+-----------------+---------------------------------+
| ``pdr`` | ``prove`` | ``pdr`` |
+------------+-----------------+---------------------------------+
Solver options are passed as additional arguments to the ABC command
implementing the solver.
``none`` engine
~~~~~~~~~~~~~~~
The ``none`` engine does not run any solver. It can be used together with the
``make_model`` option to manually generate any model supported by one of the
other engines. This makes it easier to use the same models outside of sby.
Script section
--------------
The ``[script]`` section contains the Yosys script that reads and elaborates
the design under test. For example, for a simple project contained in a single
design file ``mytest.sv`` with the top-module ``mytest``:
.. code-block:: text
[script]
read -sv mytest.sv
prep -top mytest
Or explicitly using the Verific SystemVerilog parser (default for ``read -sv``
when Yosys is built with Verific support):
.. code-block:: text
[script]
verific -sv mytest.sv
verific -import mytest
prep -top mytest
Or explicitly using the native Yosys Verilog parser (default for ``read -sv``
when Yosys is not built with Verific support):
.. code-block:: text
[script]
read_verilog -sv mytest.sv
prep -top mytest
Run ``yosys`` in a terminal window and enter ``help`` on the Yosys prompt
for a command list. Run ``help <command>`` for a detailed description of the
command, for example ``help prep``.
Files section
-------------
The files section lists the source files for the proof, meaning all the
files Yosys will need to access when reading the design, including for
example data files for ``$readmemh`` and ``$readmemb``.
``sby`` copies these files to ``<outdir>/src/`` before running the Yosys
script. When the Yosys script is executed, it will use the copies in
``<outdir>/src/``. (Alternatively absolute filenames can be used in the
Yosys script for files not listed in the files section.)
For example:
.. code-block:: text
[files]
top.sv
../common/defines.vh
/data/prj42/modules/foobar.sv
Will copy these files as ``top.v``, ``defines.vh``, and ``foobar.sv``
to ``<outdir>/src/``.
If the name of the file in ``<outdir>/src/`` should be different from the
basename of the specified file, then the new file name can be specified before
the source file name. For example:
.. code-block:: text
[files]
top.sv
defines.vh ../common/defines_footest.vh
foo/bar.sv /data/prj42/modules/foobar.sv
File sections
-------------
File sections can be used to create additional files in ``<outdir>/src/`` from
the literal content of the ``[file <filename>]`` section ("here document"). For
example:
.. code-block:: text
[file params.vh]
`define RESET_LEN 42
`define FAULT_CYCLE 57
Pycode blocks
-------------
Blocks enclosed in ``--pycode-begin--`` and ``--pycode-end--`` lines are interpreted
as Python code. The function ``output(line)`` can be used to add configuration
file lines from the python code. The variable ``task`` contains the current task name,
if any, and ``None`` otherwise. The variable ``tags`` contains a set of all tags
associated with the current task.
.. code-block:: text
[tasks]
--pycode-begin--
for uut in "rotate reflect".split():
for op in "SRL SRA SLL SRO SLO ROR ROL FSR FSL".split():
output("%s_%s %s %s" % (uut, op, uut, op))
--pycode-end--
...
[script]
--pycode-begin--
for op in "SRL SRA SLL SRO SLO ROR ROL FSR FSL".split():
if op in tags:
output("read -define %s" % op)
--pycode-end--
rotate: read -define UUT=shifter_rotate
reflect: read -define UUT=shifter_reflect
read -sv test.v
read -sv shifter_reflect.v
read -sv shifter_rotate.v
prep -top test
...
The command ``sby --dumpcfg <sby_file>`` can be used to print the configuration without
specialization for any particular task, and ``sby --dumpcfg <sby_file> <task_name>`` can
be used to print the configuration with specialization for a particular task.