# sat - solve a SAT problem in the circuit

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 -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.