yosys-smtbmc - write design to SMT2-LIBv2 file

       This manual page was written by Sebastian Kuzminsky <seb@highlab.com> for the Debian project (and may  be
       used by others).

                                                   04 May 2025                                   YOSYS-SMTBMC(1)

yosys-smtbmc - write design to SMT2-LIBv2 file

-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

yosys-smtbmc [options] <yosys_smt2_output>