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. Because the solver only ever searches for a single assignment, a property that should hold for all inputs has to be stated as its own negation — constrain the thing you believe impossible, and let the solver fail to find it. The most important instance of this pattern, proving two functions equal, has its own section below.

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. Eq takes the width of its result as the last argument, which is 1 no matter how wide the operands being compared 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(), or simply printed — print(eq_cstr) gives A = 0b00000101. The query configuration, the model and the solver result print the same way, which is the quickest way to see what a query was actually asked and what came back.

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:

c = hal_py.BooleanFunction.Var("C", 8)

# is there an input C for which C + 3 == 10?
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))

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

print(res.type)   # SolverResultType.Sat

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 — for the query above:

res = solver.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

Checking two functions for equality

The question HAL users bring to the solver most often is whether two Boolean functions are the same function — a subcircuit against a reference implementation, a netlist before and after an optimization, a recovered function against its specification.

Equality is a claim about every input: the functions must agree on all 2^n assignments at once. The solver, however, only ever searches for one assignment, so asking it directly whether the functions can be equal answers the wrong question:

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

wrong = hal_py.SMT.Constraint(hal_py.BooleanFunction.Or(a, b, 1),
                              hal_py.BooleanFunction.And(a, b, 1))
# Sat — for A = B = 1 the two agree. It says nothing about the other inputs.

A | B and A & B are plainly different functions, yet the query is Sat, because Sat only means they agree somewhere.

The correct query is the negation: assert that the functions differ, and let the solver hunt for the input that proves it. Now the two answers line up with what you actually want to know:

• UnSat — no input makes them differ, so they are equal on every input. This is the proof.
• Sat — the model is a concrete input on which they disagree.

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

f = hal_py.BooleanFunction.And(a, b, 8)                                # one implementation
g = hal_py.BooleanFunction.Not(                                        # another: ~(~A | ~B)
        hal_py.BooleanFunction.Or(hal_py.BooleanFunction.Not(a, 8),
                                  hal_py.BooleanFunction.Not(b, 8), 8), 8)

# assert f != g and search for a witness
neq = hal_py.SMT.Constraint(
    hal_py.BooleanFunction.Not(hal_py.BooleanFunction.Eq(f, g, 1), 1))

res = hal_py.SMT.Solver([neq]).query(hal_py.SMT.QueryConfig())
print(res.is_unsat())   # True — no input distinguishes f from g, De Morgan holds on all 8 bits

The two 1s in the constraint are result widths: Eq(f, g, 1) compares the 8-bit operands down to a single bit, and the Not negating it is one bit wide as well — like Eq, it takes the width of its result as the last argument.

When the check comes back Sat instead, the failed proof turns into a lead. Run it again with with_model_generation() and the model is the exact input on which the two functions part ways — comparing f above against A | B yields {'A': (128, 8), 'B': (0, 8)}, an input the two functions map to different values. Feed that input into simulation or into model.evaluate() on intermediate functions and you can follow the disagreement back to the gate that causes it. For a check you expect to pass, leave model generation off and save the solver the work.

The same pattern scales from formulas to circuits: compose the function of a subcircuit with the subgraph decorator and compare it against a reference, or use Z3 Utilities when the question is about two nets of a netlist rather than two functions you hold in hand.

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.

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.