Simple ALU

The Simple ALU example project provides a gentle introduction to working on Boolean functions and using SMT solving in HAL Python scripts. The netlist comprises 45 combinational FPGA gates such as buffers, LUTs, and carry gates. It comes with one module, the top_module, which contains the entire ALU circuit. The inputs and outputs of the module have already been annotated, ordered, and grouped into module pin groups.

When opening the project, you should find the smt.py script already open in the Python editor. The goal of this script is to check whether the given ALU behaves like an adder under certain conditions. A strict precondition for this kind of check is that the input and output pins of the module under analysis are correctly ordered from LSB to MSB. While this is already the case in this example project, in reality, such bit-order information would need to be deduced from surrounding circuitry, e.g., from carry chains or shift registers.

Preliminaries

Preparing Boolean Functions

We now walk you through the smt.py Python script piece by piece. First, we reconstruct the Boolean function actually implemented by the ALU. Next, we compose a model of an 8-bit addition that we can compare the ALU function with. Finally, we create the respective SMT solver constraints and query the solver.

Reconstruct ALU Output Function

For the SMT check, we want to compare the Boolean function implemented by the ALU circuit (alu_func) against a predefined model, in this case of an adder (adder_func). We begin by reconstructing the 8-bit Boolean function that is implemented by the combinational logic of the ALU. To this end, we first collect 8 single-bit Boolean functions in a list, one for each of the 8 output pins of the pin group Z. In order to achieve this, we retrieve the pin group object belonging to pin group Z and store it in variable grp_z. Then, we iterate over all eight pins of that group. For each pin, we call get_subgraph_function once, providing it with the output net corresponding to the current pin of Z and the gates of the netlist every time. This function automatically reconstructs the Boolean function that determines the behavior of the given net. Internally, this function recursively explores the net's source gates until it either hits non-combinational gates (such as flip-flops) or gates that are not part of the set of gates provided to the function. The function then merges the Boolean functions of all combinational gates it comes across into one big Boolean function. This new function will have variables named net_[ID] with [ID] being the unique net ID of the respective net.

output_functions = list()
grp_z = netlist.get_top_module().get_pin_group_by_name("Z")
for pin in grp_z.get_pins():
    output_functions.append(hal_py.NetlistUtils.get_subgraph_function(pin.get_net(), netlist.get_gates()))

alu_func = hal_py.BooleanFunctionDecorator.get_boolean_function_from(output_functions)

Compose Adder Function

For this check to be successful, both the Boolean function implemented by the ALU circuit and the Boolean function representing the model of the adder need to operate on the same Boolean variables. When operating on the combined Boolean function of a sub circuit of multiple interconnected gates, HAL always uses net_[ID] as Boolean variable names for the inputs of the subcircuit that the combined Boolean function belongs to. Here, [ID] is replaced with the unique net ID of the respective input net.

grp_a = netlist.get_top_module().get_pin_group_by_name("A")
var_a = hal_py.BooleanFunctionDecorator.get_boolean_function_from(grp_a)

grp_b = netlist.get_top_module().get_pin_group_by_name("B")
var_b = hal_py.BooleanFunctionDecorator.get_boolean_function_from(grp_b)

adder_func = hal_py.BooleanFunction.Add(var_a, var_b, 8)

Create Constraints

When provided with a set of constraints, an SMT solver tries to find one valid set of inputs such that all constraints evaluate to true or rather the Boolean value 1. If such a set of inputs is found, the SMT solver will output Sat, otherwise Unsat. Given that SMT solving exhibits an exponential worst case complexity, it may not find a solution in reasonable time. Hence, on timeout, the SMT solver may also output Unknown.

When checking two Boolean functions for equality (for example when comparing our actual ALU function against the Boolean function of an adder), we therefore cannot simply query the SMT solver to find a solution for alu_func == adder_func, since it would also return 1 if this condition holds only for a single input value. For example, checking (A or B) == (A and B) would return 1 as A or B behaves the same as A and B for A = B = 1. Hence, we must always query the SMT solver with alu_func != adder_func and check whether the SMT solver returns Unsat. This way, the SMT solver will try to find a set of inputs for which alu_func behaves different than adder_func. If it cannot find such a set of input, the Boolean functions are guaranteed to be equal (unless a timeout occurred).

adder_cstr = hal_py.SMT.Constraint(hal_py.BooleanFunction.Not(hal_py.BooleanFunction.Eq(adder_func, alu_func, 1), 1))

grp_op = netlist.get_top_module().get_pin_group_by_name("op")
var_op = hal_py.BooleanFunctionDecorator.get_boolean_function_from(grp_op)
op_code_cstr = hal_py.SMT.Constraint(hal_py.BooleanFunction.Eq(var_op, hal_py.BooleanFunction.Const(0, 2), 1))

Querry the SMT Solver

solver = hal_py.SMT.Solver([adder_cstr, op_code_cstr])
res = solver.query(hal_py.SMT.QueryConfig().with_solver(hal_py.SMT.SolverType.Z3).with_local_solver().with_timeout(1000))
print(res.type)