yosys-smtbmc1
Write design to smt2-libv2 file
Usage
yosys-smtbmc [options]
<yosys_smt2_output>
Options
-
-t [<skip_steps>:]<num_steps> -
default: skip_steps=0, num_steps=20
-
-u <start_step> -
assume asserts in skipped steps in BMC
-
-S <step_size> -
proof <step_size> time steps at once
-
-c <vcd_filename> -
write counter-example to this VCD file (hint: use 'write_smt2 -wires' for maximum coverage of signals in generated VCD file)
-
-i -
instead of BMC run temporal induction
-
-m <module_name> -
name of the top module
-
-s <solver> -
Set SMT solver: z3, cvc4, yices, mathsat. default: z3
-
-v -
enable debug output
-
-p -
disable timer display during solving
-
-d <filename> -
write smt2 statements to file
Releases
5 releases since Debian 9 (Stretch); the text changed 4 times.