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.

-nocleanup

Do not delete temporary files and directories. Useful for debugging.

-dump-final-smt2 <file>

Pass the --dump-smt2 option to yosys-smtbmc.

-assume-outputs

Add an "$assume" cell for the conjunction of all one-bit module output
wires.

-assume-negative-polarity

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.

-nooptimize

Ignore "\minimize" and "\maximize" attributes, do not emit
"(maximize)" or "(minimize)" in the SMT-LIBv2, and generally make no
attempt to optimize anything.

-nobisection

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.

-solver <solver>

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.

-timeout <value>

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.

-sat

Generate an error if the solver does not return "sat".

-unsat

Generate an error if the solver does not return "unsat".

-show-smtbmc

Print the output from yosys-smtbmc.

-specialize

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.