qbfsat - solve a 2QBF-SAT problem in the circuit¶
yosys> help qbfsat¶
qbfsat [options] [selection]
This command solves an "exists-forall" 2QBF-SAT problem defined over the currently selected module. Existentially-quantified variables are declared by assigning a wire "$anyconst". Universally-quantified variables may be explicitly declared by assigning a wire "$allconst", but module inputs will be treated as universally-quantified variables by default.
Do not delete temporary files and directories. Useful for debugging.
Pass the --dump-smt2 option to yosys-smtbmc.
Add an "$assume" cell for the conjunction of all one-bit module output wires.
When adding $assume cells for one-bit module output wires, assume they are negative polarity signals and should always be low, for example like the miters created with the `miter` command.
Ignore "\minimize" and "\maximize" attributes, do not emit "(maximize)" or "(minimize)" in the SMT-LIBv2, and generally make no attempt to optimize anything.
If a wire is marked with the "\minimize" or "\maximize" attribute, do not attempt to optimize that value with the default iterated solving and threshold bisection approach. Instead, have yosys-smtbmc emit a "(minimize)" or "(maximize)" command in the SMT-LIBv2 output and hope that the solver supports optimizing quantified bitvector problems.
Use a particular solver. Choose one of: "z3", "yices", "cvc4" and "cvc5". (default: yices)
-solver-option <name> <value>
Set the specified solver option in the SMT-LIBv2 problem file.
Set the per-iteration timeout in seconds. (default: no timeout)
-O0, -O1, -O2
Control the use of ABC to simplify the QBF-SAT problem before solving.
Generate an error if the solver does not return "sat".
Generate an error if the solver does not return "unsat".
Print the output from yosys-smtbmc.
If the problem is satisfiable, replace each "$anyconst" cell with its corresponding constant value from the model produced by the solver.
-specialize-from-file <solution file>
Do not run the solver, but instead only attempt to replace each "$anyconst" cell in the current module with a constant value provided by the specified file.
-write-solution <solution file>
If the problem is satisfiable, write the corresponding constant value for each "$anyconst" cell from the model produced by the solver to the specified file.