sat - solve a SAT problem in the circuit

yosys> help sat

sat [options] [selection]

This command solves a SAT problem defined over the currently selected circuit
and additional constraints passed as parameters.

-all

show all solutions to the problem (this can grow exponentially, use
-max <N> instead to get <N> solutions)

-max <N>

like -all, but limit number of solutions to <N>

-enable_undef

enable modeling of undef value (aka 'x-bits')
this option is implied by -set-def, -set-undef et. cetera

-max_undef

maximize the number of undef bits in solutions, giving a better
picture of which input bits are actually vital to the solution.

-set <signal> <value>

set the specified signal to the specified value.

-set-def <signal>

add a constraint that all bits of the given signal must be defined

-set-any-undef <signal>

add a constraint that at least one bit of the given signal is undefined

-set-all-undef <signal>

add a constraint that all bits of the given signal are undefined

-set-def-inputs

add -set-def constraints for all module inputs

-set-def-formal

add -set-def constraints for formal $anyinit, $anyconst, $anyseq cells

-show <signal>

show the model for the specified signal. if no -show option is
passed then a set of signals to be shown is automatically selected.

-show-inputs, -show-outputs, -show-ports

add all module (input/output) ports to the list of shown signals

-show-regs, -show-public, -show-all

show all registers, show signals with 'public' names, show all signals

-ignore_div_by_zero

ignore all solutions that involve a division by zero

-ignore_unknown_cells

ignore all cells that can not be matched to a SAT model

The following options can be used to set up a sequential problem:

-seq <N>

set up a sequential problem with <N> time steps. The steps will
be numbered from 1 to N.

note: for large <N> it can be significantly faster to use
-tempinduct-baseonly -maxsteps <N> instead of -seq <N>.

-set-at <N> <signal> <value>

-unset-at <N> <signal>

set or unset the specified signal to the specified value in the
given timestep. this has priority over a -set for the same signal.

-set-assumes

set all assumptions provided via $assume cells

-set-def-at <N> <signal>

-set-any-undef-at <N> <signal>

-set-all-undef-at <N> <signal>

add undef constraints in the given timestep.

-set-init <signal> <value>

set the initial value for the register driving the signal to the value

-set-init-undef

set all initial states (not set using -set-init) to undef

-set-init-def

do not force a value for the initial state but do not allow undef

-set-init-zero

set all initial states (not set using -set-init) to zero

-dump_vcd <vcd-file-name>

dump SAT model (counter example in proof) to VCD file

-dump_json <json-file-name>

dump SAT model (counter example in proof) to a WaveJSON file.

-dump_cnf <cnf-file-name>

dump CNF of SAT problem (in DIMACS format). in temporal induction
proofs this is the CNF of the first induction step.

The following additional options can be used to set up a proof. If also -seq
is passed, a temporal induction proof is performed.

-tempinduct

Perform a temporal induction proof. In a temporal induction proof it is
proven that the condition holds forever after the number of time steps
specified using -seq.

-tempinduct-def

Perform a temporal induction proof. Assume an initial state with all
registers set to defined values for the induction step.

-tempinduct-baseonly

Run only the basecase half of temporal induction (requires -maxsteps)

-tempinduct-inductonly

Run only the induction half of temporal induction

-tempinduct-skip <N>

Skip the first <N> steps of the induction proof.

note: this will assume that the base case holds for <N> steps.
this must be proven independently with "-tempinduct-baseonly
-maxsteps <N>". Use -initsteps if you just want to set a
minimal induction length.

-prove <signal> <value>

Attempt to proof that <signal> is always <value>.

-prove-x <signal> <value>

Like -prove, but an undef (x) bit in the lhs matches any value on
the right hand side. Useful for equivalence checking.

-prove-asserts

Prove that all asserts in the design hold.

-prove-skip <N>

Do not enforce the prove-condition for the first <N> time steps.

-maxsteps <N>

Set a maximum length for the induction.

-initsteps <N>

Set initial length for the induction.
This will speed up the search of the right induction length
for deep induction proofs.

-stepsize <N>

Increase the size of the induction proof in steps of <N>.
This will speed up the search of the right induction length
for deep induction proofs.

-timeout <N>

Maximum number of seconds a single SAT instance may take.

-verify

Return an error and stop the synthesis script if the proof fails.

-verify-no-timeout

Like -verify but do not return an error for timeouts.

-falsify

Return an error and stop the synthesis script if the proof succeeds.

-falsify-no-timeout

Like -falsify but do not return an error for timeouts.