Man page - yosys-smtbmc(1)

Packages contains this manual

Package:  yosys
apt-get install yosys

Manuals in package:
• yosys(1)
• yosys-smtbmc(1)
• yosys-filterlib(1)
• yosys-witness(1)
Documentations in package:
• yosys

Manual

YOSYS-SMTBMC

NAME
SYNOPSIS
OPTIONS
AUTHOR

---

NAME

yosys-smtbmc - write design to SMT2-LIBv2 file

SYNOPSIS

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

AUTHOR

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

---