-
Notifications
You must be signed in to change notification settings - Fork 87
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.
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.
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.
Once we have collected all eight Boolean functions, one for each Z output pin of the ALU, we combine them into one 8-bit Boolean function called alu_func by calling get_boolean_function_from(). You can call print(alu_func) to take a look at the composed function, but you will not be able to make sense of it at this point.
top_mod = netlist.get_top_module()
nl_dec = hal_py.SubgraphNetlistDecorator(netlist)
output_functions = list()
grp_z = top_mod.get_pin_group_by_name("Z")
for pin in grp_z.get_pins():
output_functions.append(nl_dec.get_subgraph_function(top_mod.get_gates(), pin.get_net()))
alu_func = hal_py.BooleanFunctionDecorator.get_boolean_function_from(output_functions)
print(alu_func)For the final SMT check to be successful, both the alu_func implemented by the ALU and the Boolean function representing the model of the adder (adder_func) need to operate on the same variables.
As discussed before, and as you can see when printing the alu_func, HAL uses net_[ID] as Boolean variable names for the inputs of the subcircuit that a combined Boolean function belongs to.
Hence, we must first construct two 8-bit variables representing inputs A and B that use the same 1-bit variables as a foundation.
Hence, these 8-bit variables must actually correspond to eight nets in the netlist each.
To this end, HAL provides short-hand functions as part of the BooleanFunctionDecorator.
By calling get_boolean_function_from on a pin group, this function will automatically deduce the required variables from the nets passing through that pin group and concatenate them into one single 8-bit Boolean function.
Call print(var_a) to take a look at one of the respective variables.
Please note that ++ represents a concatenation operation.
Having constructed 8-bit variables var_a and var_b this way, we can now simply define an 8-bit addition with inputs A and B.
Call print(adder_func) to inspect the resulting function, it should be easier to understand than alu_func.
grp_a = top_mod.get_pin_group_by_name("A")
var_a = hal_py.BooleanFunctionDecorator.get_boolean_function_from(grp_a)
print(var_a)
grp_b = top_mod.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)
print(adder_func)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).
Therefore, we create an SMT constraint that checks whether alu_func and adder_func are not equal.
Please note that the 1 passed as the last parameter to both Eq and Not specifies the output size of the respective function.
Despite Eq taking two 8-bit functions a inputs, it produces only a single output bit.
adder_cstr = hal_py.SMT.Constraint(hal_py.BooleanFunction.Not(hal_py.BooleanFunction.Eq(adder_func, alu_func, 1), 1))Our ALU behaves differently depending on the applied opcode.
Only for a single opcode, it will behave like an adder.
This opcode that we are looking for is actually 00.
For this reason, we construct a second constraint that fixes the opcode to a constant 00.
To this end, we again create a Boolean variable for the input pin group opcode again and then construct a constraint using Eq and a constant value of 00.
Again, var_op and hal_py.BooleanFunction.Const(0, 2) are two bits wide, but Eq produces only a single-bit output.
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))Finally, we need to query the SMT solver to on both constraint such that it checks for equivalence of alu_func and adder_func when the opcode is fixed to 00.
To this end, we first create a solver and pass it the two constraints.
When querying the solver, we also specify the SMT engine (z3 in this case, but others are also supported) and define a timeout.
Currently, only local solving is supported, but SMT requests may in the future also be send to a more powerful backend server.
You can print the result of the SMT query by calling print(res.type).
It should be Unsat.
Try changing the opcode and observe how the SMT solver result changes.
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)