Z3 Utilities

The z3_utils plugin connects HAL to the Z3 SMT solver. It provides Z3-backed simplification of Boolean functions, extraction of subcircuit functions, and — most usefully — formal equivalence checking between nets or entire netlists.

The plugin is built by default, see Building HAL. It is also a dependency of several other plugins, so you will often have it loaded without invoking it directly.

Why this matters

Everything else in HAL tells you what a circuit looks like. A solver tells you what it is.

The distinction becomes essential the moment you want to make a claim rather than an observation. "These two subcircuits look similar" is a hypothesis; "these two subcircuits are functionally equivalent for all inputs" is a result. Structural comparison cannot give you the second, because two circuits computing the same function can be wired completely differently — and, conversely, a single changed LUT configuration can make two identical-looking circuits behave differently.

This is what makes equivalence checking the right tool for questions like: did my netlist transformation preserve behavior? Is this suspicious block really a copy of that one? Does this recovered subcircuit match a reference implementation? And, in a Trojan hunt, does the modified design still behave like the original everywhere — or is there an input for which it does not?

Equivalence checking

Comparing nets

compare_nets(netlist_a, netlist_b, net_a, net_b, fail_on_unknown=True, solver_timeout=10) checks whether two nets — possibly in two different netlists — are driven by functionally equivalent logic. It returns a bool, or None on failure.

from hal_plugins import z3_utils

equal = z3_utils.compare_nets(nl_orig, nl_modified, out_orig, out_modified)

A batch overload takes a list of net pairs instead:

pairs = [(a1, b1), (a2, b2)]
equal = z3_utils.compare_nets(nl_orig, nl_modified, pairs)

solver_timeout is per query, in seconds. fail_on_unknown decides what a timeout means: with True an inconclusive solver result counts as not equivalent, which is the conservative choice and the right default when you are verifying something.

Comparing netlists

compare_netlists(netlist_a, netlist_b, fail_on_unknown=True, solver_timeout=10) compares two netlists wholesale. It finds a corresponding partner for each sequential gate across the two designs and checks whether each pair is functionally identical.

equal = z3_utils.compare_netlists(nl_orig, nl_modified)

Because it anchors on sequential gates, this works even when the combinational logic between registers was completely restructured — which is exactly the case after synthesis with different settings, after resynthesis, or after most obfuscation transformations. It is the natural way to check whether a design and a suspected copy of it are the same circuit.

Simplification

simplify(bf) simplifies a Boolean function using Z3, returning a new function or None on failure.

simplified = z3_utils.simplify(bf)

This complements BooleanFunction.simplify() from the core, see Boolean Function. The Z3-backed version is generally stronger on large composed functions, at the cost of invoking the solver; the built-in one is faster for everyday use.

Simplification is more than cosmetic here. A subcircuit whose composed function simplifies to A ^ B is an XOR regardless of how many gates implement it, and a path that simplifies to a constant carries no information at all.

Subgraph functions

get_subgraph_function(subgraph_gates, subgraph_output) reconstructs the Boolean function driving an output net from a set of gates, computed through Z3.

bf = z3_utils.get_subgraph_function(module.get_gates(), output_net)

For everyday use prefer the core's SubgraphNetlistDecorator, see Decorators — it needs no plugin and supports caching across calls. The Z3 variant is worth reaching for when the resulting function is large enough that the solver's internal representation handles it better.

Practical notes

• Tune the timeout. The default of 10 seconds per query is fine for small comparisons and far too low for whole netlists. Raise it and expect long runtimes on real designs.
• Unsat is the good answer. Equivalence is proven by failing to find a counterexample, not by finding a witness. The Simple ALU example project explains why querying for equality directly would mislead you.
• Keep fail_on_unknown=True whenever a false "equivalent" would be worse than a false "not equivalent".

See also

• Boolean Function — the representation and HAL's own SMT interface
• Simple ALU — a worked example of proving what a circuit computes
• Decorators — the core's subgraph function extraction
• Resynthesis — a transformation worth verifying with an equivalence check