1YOSYS-SMTBMC(23 May 2021)                            YOSYS-SMTBMC(23 May 2021)
2
3
4

NAME

6       yosys-smtbmc - write design to SMT2-LIBv2 file
7

SYNOPSIS

9       yosys-smtbmc [options] <yosys_smt2_output>
10
11

OPTIONS

13       -t [<skip_steps>:]<num_steps>
14              default: skip_steps=0, num_steps=20
15
16       -u <start_step>
17              assume asserts in skipped steps in BMC
18
19       -S <step_size>
20              proof <step_size> time steps at once
21
22       -c <vcd_filename>
23              write  counter-example  to  this VCD file (hint: use 'write_smt2
24              -wires' for maximum coverage of signals in generated VCD file)
25
26       -i     instead of BMC run temporal induction
27
28       -m <module_name>
29              name of the top module
30
31       -s <solver>
32              Set SMT solver: z3, cvc4, yices, mathsat. default: z3
33
34       -v     enable debug output
35
36       -p     disable timer display during solving
37
38       -d <filename>
39              write smt2 statements to file
40

AUTHOR

42       This manual page was written by Sebastian  Kuzminsky  <seb@highlab.com>
43       for the Debian project (and may be used by others).
44
45
46
47                                                     YOSYS-SMTBMC(23 May 2021)
Impressum