Boolean Function

Boolean functions are used to represent the functionality of each gate within the netlist. HAL enables the reverse engineer to operate upon these functions by providing a set of functions to extend, simplify, and evaluate them. In general, they consist of a set of variables that are connected using Boolean operators.

Boolean functions are how you move from structure to behavior. Knowing that some gates are wired together tells you nothing about what the circuit does; composing their Boolean functions and simplifying the result tells you exactly that. This is the foundation for identifying an adder, proving that a recovered subcircuit matches a reference implementation, or showing that a suspicious path can leak a key — see the Simple ALU example project for a complete walkthrough.

Note that a Boolean function in HAL is not necessarily single-bit. Functions carry a size in bits, and multi-bit functions let you reason at the word level (A + B on 8-bit operands) rather than bit by bit.

Accessing Boolean functions

If available, the user can retrieve the Boolean functions of a gate by using get_boolean_function and get_boolean_functions respectively. While the first command requires the name of the desired Boolean function as input, the latter simply returns a dict of all available Boolean functions.

gate = netlist.get_gate_by_id(1)                # get gate with ID 1
func = gate.get_boolean_function("func_name")   # return only the Boolean function specified by "func_name"
func_map = gate.get_boolean_functions()         # return a dict of all Boolean functions of that gate

Boolean functions of a gate are named after the output pin they describe, so gate.get_boolean_function("O") gives you the function driving pin O. Calling it without an argument returns the function of the first output pin.

While for most gates the Boolean functions are actually associated with their gate type, some special gates like LUTs may feature individual functions independent of their gate type. Hence, we recommend always retrieving the Boolean function of a gate from the gate itself and not its gate type, despite the gate type offering similar functionality.

Creating Boolean functions

The reverse engineer may also create new Boolean functions by constructing them from a string as follows:

func = hal_py.BooleanFunction.from_string("(A&B)+C")   # constructs a Boolean function object from string

In general, Boolean functions support NOT ("!", "'"), AND ("&", "*", " "), OR ("|", "+"), and XOR ("^") operations as well as brackets ("(", ")") when being parsed from a string. Since " " is generally interpreted as AND, be careful with spaces in your equation!

If parsing fails, from_string logs an error and returns an empty Boolean function rather than raising — check with is_empty() if the input is not under your control.

The string representation of a Boolean function is available via the str function. To print a Boolean function, it suffices to call print on the function itself.

func_str = str(func)   # returns the string representation of the Boolean function
print(func)            # prints the Boolean function

In addition to the construction from a string, Boolean functions can also be composed by using their constructors and provided operators. Oftentimes, the size of the Boolean function (in bits) must be provided as well.

var_a = hal_py.BooleanFunction.Var("A")                                    # variable A
const_1 = hal_py.BooleanFunction.Const(hal_py.BooleanFunction.Value.ONE)   # constant 1
func = hal_py.BooleanFunction.And(var_a, const_1, 1)                       # Boolean function "A & 1" of size 1

Besides the bitwise operators, HAL provides word-level operations such as Add, Sub, Mul, Eq, Slice, and Concat, each taking the size of the resulting function as its last argument. These are what let you express a model of the behavior you expect and compare it against the circuit:

adder = hal_py.BooleanFunction.Add(var_a, var_b, 8)   # an 8-bit addition

Combining Boolean functions

Two Boolean functions can be joined using the &, |, and ^ operators and negated using the ~ operator. Most of these operations are also available in-place.

func_A = hal_py.BooleanFunction.Var("A")                                  # Boolean function containing only variable A
func_B = hal_py.BooleanFunction.Var("B")                                  # Boolean function containing only variable B
func_1 = hal_py.BooleanFunction.Const(hal_py.BooleanFunction.Value.ONE)   # constant 1
nand_func = ~(func_A & func_B)                                            # build a NAND from A and B
nand_func |= func_1                                                       # in-place OR

Additionally, two Boolean functions may also be combined by replacing a variable in one function with the other function using substitute. This allows to retrieve the combined Boolean function of gates that are connected in series. Combining two Boolean functions in this way may require the renaming of some variables before substitution. In the example below, func_1 represents the function of an OR gate, while func_2 gives the function of an AND gate. Both gates use the variables "A" and "B" as inputs, although they are not connected to the same net and may thus have different values. Therefore, when replacing "B" of func_1 with func_2, at least "A" of func_2 should be renamed.

func_1 = hal_py.BooleanFunction.from_string("A + B")   # create OR function
func_2 = hal_py.BooleanFunction.from_string("A & B")   # create AND function
func_2 = func_2.substitute("A", "C")                   # rename "A" of func_2 to "C"
func_1 = func_1.substitute("B", func_2)                # substitute "B" of func_1 with func_2
print(func_1)                                          # prints "A + (C & B)"

substitute comes in four flavors: renaming a single variable (as above), replacing a single variable with a function, and dict-based variants of both that apply many substitutions at once.

This variable-collision problem is exactly why HAL names variables after net IDs when composing functions across gates. Doing this manually for more than two gates gets unwieldy fast — use the SubgraphNetlistDecorator instead, see Decorators.

Inspecting and simplifying

A composed Boolean function is typically large and unreadable. simplify applies a full simplification, while simplify_local performs cheaper local rewriting only. Both return a new function rather than modifying in place.

simplified = func.simplify()

Simplification is not cosmetic. A subcircuit whose composed function simplifies to A ^ B is an XOR, no matter how many LUTs implement it — and a path that simplifies to a constant carries no information at all.

To inspect a function, get_variable_names returns the set of variables it depends on, get_size its bit width, and is_constant / has_constant_value / get_constant_value check whether it collapsed to a constant.

print(func.get_variable_names())   # e.g. {'net_3', 'net_7'}
print(func.get_size())             # bit width of the function

Note that after simplification, get_variable_names tells you which inputs a subcircuit actually depends on — often far fewer than the ones physically connected to it.

Evaluating

evaluate computes the output of a function for a concrete assignment of its variables. It takes a dict from variable name to BooleanFunction.Value (ZERO, ONE, X, Z), and returns a single value for single-bit functions, or a list of values when given lists as inputs.

val = func.evaluate({"A": hal_py.BooleanFunction.Value.ONE,
                     "B": hal_py.BooleanFunction.Value.ZERO})

For small functions, the complete behavior is often more informative than individual evaluations. compute_truth_table returns the truth table as a list of output value lists, and get_truth_table_as_string returns a printable version. Both accept an optional ordered_variables list to fix the column order — important when comparing two truth tables — and remove_unknown_variables to drop variables the function does not use.

print(func.get_truth_table_as_string(function_name="O"))

Truth tables are only practical up to roughly 10 input variables, since their size doubles with each one. Beyond that, use SMT solving to compare functions instead of enumerating them: query the solver with the inequality of two functions and check that the result is Unsat. The Simple ALU example project walks through exactly this, including why asking for equality directly would give you a misleading answer.

Note: For more information on how to combine multiple gates and generate a Boolean function depending on multiple gates and inputs, have a look at the Subgraph Netlist Decorator.