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.
show all solutions to the problem (this can grow exponentially, use -max <N> instead to get <N> solutions)
like -all, but limit number of solutions to <N>
enable modeling of undef value (aka 'x-bits') this option is implied by -set-def, -set-undef et. cetera
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.
add a constraint that all bits of the given signal must be defined
add a constraint that at least one bit of the given signal is undefined
add a constraint that all bits of the given signal are undefined
add -set-def constraints for all module inputs
add -set-def constraints for formal $anyinit, $anyconst, $anyseq cells
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 all solutions that involve a division by zero
ignore all cells that can not be matched to a SAT model
The following options can be used to set up a sequential problem:
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 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 all initial states (not set using -set-init) to undef
do not force a value for the initial state but do not allow undef
set all initial states (not set using -set-init) to zero
dump SAT model (counter example in proof) to VCD file
dump SAT model (counter example in proof) to a WaveJSON file.
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.
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.
Perform a temporal induction proof. Assume an initial state with all registers set to defined values for the induction step.
Run only the basecase half of temporal induction (requires -maxsteps)
Run only the induction half of temporal induction
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 that all asserts in the design hold.
Do not enforce the prove-condition for the first <N> time steps.
Set a maximum length for the induction.
Set initial length for the induction. This will speed up the search of the right induction length for deep induction proofs.
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.
Maximum number of seconds a single SAT instance may take.
Return an error and stop the synthesis script if the proof fails.
Like -verify but do not return an error for timeouts.
Return an error and stop the synthesis script if the proof succeeds.
Like -falsify but do not return an error for timeouts.