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 set.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

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'). 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. This will make more sense when looking at the code of the example project later on.

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 Ùnsat. This way, the SMT solver will try to find a set of inputs for which alu_func behaves different thanadder_func`. If it cannot find such a set of input, the Boolean functions are guaranteed to be equal (unless a timeout occurred).