yosys-smtbmc(1) write design to SMT2-LIBv2 file


yosys-smtbmc [options] <yosys_smt2_output>


-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)
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
enable debug output
disable timer display during solving
-d <filename>
write smt2 statements to file


This manual page was written by Sebastian Kuzminsky <[email protected]> for the Debian project (and may be used by others).