SMT Solving

Some questions about a circuit cannot be answered by looking at it, and answering them by enumeration is hopeless: comparing two 8-bit functions means checking 65536 input pairs, and at 32 bits there are more of them than you will ever simulate. An SMT solver answers such questions the other way round — it searches for a counterexample, and when it can prove that none exists, you have a statement about all inputs at once.

HAL reaches SMT solvers through the hal_py.SMT namespace. This is part of the core API rather than a plugin, and everything it reasons about is a Boolean function. The Simple ALU example project walks through a complete proof end to end; this page describes the interface itself.

Requirements

Requirement	Type	Needed for	Availability
Z3	dependency	discharging queries (the default solver)	must be installed
Boolector	dependency	optional alternative solver	must be installed

HAL does not link the solver, it runs the binary in a subprocess and talks SMT-LIB v2 to it. The binary is looked up at three fixed locations — /usr/bin, /usr/local/bin and /opt/homebrew/bin — so a solver installed somewhere else is not found even if it is on your PATH; symlink it into one of those directories.

The three answers

A solver takes a set of constraints and looks for one assignment of the variables that satisfies all of them simultaneously:

• Sat — it found one. If you asked for a model, you can read the assignment out and use it.
• UnSat — it proved that no such assignment exists, for any input whatsoever.
• Unknown — it gave up, almost always because the timeout expired. SMT solving is exponential in the worst case.

Which of these you want depends on how you phrased the question, and phrasing is most of the work. Sat gives you an example; UnSat gives you a proof. A property that should hold everywhere is therefore stated as its own negation: constrain the thing you believe impossible, and let the solver fail to find it. Asking directly whether two functions can be equal is the classic mistake — A | B and A & B are equal for A = B = 1, so the query is Sat even though the functions are different.

Constraints

A constraint comes in two forms. Either a single Boolean function that has to evaluate to 1, or a pair of functions that have to be equal:

f = hal_py.BooleanFunction.Var("A", 8)
g = hal_py.BooleanFunction.Const(5, 8)

eq_cstr  = hal_py.SMT.Constraint(f, g)                                        # A == 5
bit_cstr = hal_py.SMT.Constraint(hal_py.BooleanFunction.Eq(f, g, 1))          # the same, written as one function

The single-function form asserts that the function equals the one-bit constant 1, so the function has to be one bit wide. Handing it a wider function does not raise — the solver rejects the generated SMT-LIB and the query comes back Unknown, which is an unhelpful way to learn about a type error. Both Eq and Not take the width of their result as the last argument, which is 1 for a comparison no matter how wide its operands are.

Several constraints are combined by conjunction: every one of them has to hold at the same time. That is what makes it easy to narrow a question down — one constraint states the property, the others pin inputs to the situation you care about.

Constraints can be inspected again with is_assignment(), get_assignment() and get_function(). Printing one is not useful; the Python object has no string representation, so print(cstr) gives you an object address.

Configuring the query

QueryConfig collects everything that is not a constraint. Its setters return the updated configuration, so they chain:

config = (hal_py.SMT.QueryConfig()
          .with_solver(hal_py.SMT.SolverType.Z3)
          .with_local_solver()
          .with_model_generation()
          .with_timeout(10))

The defaults are Z3, local execution, no model generation, and a timeout of 10. That timeout is in seconds, not milliseconds — with_timeout(1000) gives the solver a quarter of an hour, which is rarely what anyone intends.

Model generation is off by default because it costs the solver extra work: it changes the question from "does an assignment exist" to "give me one". Turn it on when you intend to read the counterexample, and leave it off when all you want is UnSat.

SolverType offers Z3 and Boolector from Python. Remote solving exists in the interface but is not implemented — with_remote_solver() will only get you an error.

Querying

Hand the constraints to a Solver and ask:

a = hal_py.BooleanFunction.Var("A", 8)
b = hal_py.BooleanFunction.Var("B", 8)

# is there any pair of inputs for which A + B differs from B + A?
cstr = hal_py.SMT.Constraint(
    hal_py.BooleanFunction.Not(
        hal_py.BooleanFunction.Eq(hal_py.BooleanFunction.Add(a, b, 8),
                                  hal_py.BooleanFunction.Add(b, a, 8), 1), 1))

solver = hal_py.SMT.Solver([cstr])
res = solver.query(config)

print(res.type)   # SolverResultType.UnSat

UnSat here is the proof that addition commutes on 8 bits — not that it happened to hold for the values that were tried, but that no counterexample exists.

Constraints can also be added after construction with with_constraint() and with_constraints(), which is convenient when you build a base query once and vary one condition.

If the query itself fails, query() returns None and logs why. By far the most common cause is that no solver binary was found at the three locations listed above, so a None result is a question about your installation rather than about your circuit.

Reading the result

SolverResult carries the answer type and, if you asked for it and got Sat, a model:

print(res.type)         # SolverResultType.Sat / UnSat / Unknown
res.is_sat()            # the same three, as predicates
res.is_unsat()
res.is_unknown()

The model is where a Sat answer becomes useful. model.model is a dict from variable name to a (value, bit size) tuple:

c = hal_py.BooleanFunction.Var("C", 8)
cstr = hal_py.SMT.Constraint(
    hal_py.BooleanFunction.Eq(hal_py.BooleanFunction.Add(c, hal_py.BooleanFunction.Const(3, 8), 8),
                              hal_py.BooleanFunction.Const(10, 8), 1))

res = hal_py.SMT.Solver([cstr]).query(hal_py.SMT.QueryConfig().with_model_generation())

print(res.model.model)   # {'C': (7, 8)}

model.evaluate(bf) substitutes the model into a Boolean function and simplifies, which is how you check what else was true in that particular assignment:

print(res.model.evaluate(c))   # 0b00000111

This is the move that turns a failed proof into a lead. When an equivalence check comes back Sat rather than UnSat, the model is a concrete input for which the circuit and your model of it disagree — feed it into simulation or into evaluate() on intermediate nets and you can follow the disagreement back to the gate that causes it.

When the answer is Unknown

Unknown means the timeout hit. Raising it helps only when the problem was nearly solved anyway; the useful responses are to make the question smaller:

• Pin down inputs. Every input fixed to a constant is a dimension the solver no longer has to search. Proving a claim per opcode, as the Simple ALU project does, is much easier than proving it for all opcodes at once.
• Cut the circuit up. Prove a property of one stage, then use that result as an assumption about the next.
• Simplify first. A composed subcircuit function is usually far larger than what it computes; simplify() before querying can pay for itself, see Boolean Function.
• Stay at the word level. Add, Sub, Mul and Eq are single nodes the solver understands as arithmetic. Expressing the same thing bit by bit throws that structure away, and the solver has to rediscover it.

What the Python bindings do not expose

A few parts of the C++ interface have no Python counterpart at the moment:

• SolverCall, and with it QueryConfig.with_call() and Solver.has_local_solver_for(). Both exist as methods but need a SolverCall value that Python cannot construct, so calling them raises a TypeError. Queries from Python always go through the solver binary.
• Bitwuzla, which the C++ SolverType has but the Python enum does not.
• to_smt2(), which returns the SMT-LIB v2 form of a query — useful for debugging a query by hand, and available in C++ only.

See also

• Boolean Function — building, composing and simplifying the functions you constrain.
• Symbolic Execution — the rewriting engine next door: it simplifies and propagates, but it does not search or prove.
• Simple ALU — a complete worked proof, from netlist to UnSat.
• Z3 Utilities — netlist-level equivalence checking built on top of Z3, when your question is "are these two nets equivalent" rather than "does this formula hold".
• Decorators — SubgraphNetlistDecorator composes the subcircuit functions that most queries start from.