-
Notifications
You must be signed in to change notification settings - Fork 95
Simple ALU
The Simple ALU example project is where looking at a circuit stops being enough. On the FSM you worked out what the netlist did by tracing gates and reading Boolean functions. Here you will prove what it does, by handing the question to an SMT solver.
The netlist is an 8-bit ALU with a 2-bit opcode: 45 combinational gates, no flip-flops. It ships as a single top_module, and unlike the FSM project the interface is already annotated — the inputs and outputs are grouped into module pin groups named A, B, Z and op, in the right bit order.
That last part matters more than it sounds. Everything below depends on knowing which net is bit 0 and which is bit 7. Here it is given to you; on a netlist recovered from real hardware you would have to work it out first, usually from surrounding structure such as carry chains or shift registers.
Requirements
| Requirement | Type | Needed for | Availability |
|---|---|---|---|
z3 |
dependency | discharging the equivalence check | must be installed and on the path |
No plugin is needed for this project — SMT solving is part of HAL's core API rather than a plugin. HAL does shell out to a solver binary though, so z3 has to be installed and findable, see Building HAL.
The project ships as the zipped HAL project hal/examples/simple_alu.zip. Do not unpack it by hand — choose File > Import Project, point it at the archive, and pick where it should end up. See import project for the individual fields.
The script smt.py is already open in the Python Editor. The four steps below walk through it piece by piece; run it as a whole at the end.
Nothing in this section changes the netlist. Every step only reads it, so unlike the FSM project there is nothing here you can get wrong permanently.
The ALU computes something different for each of its four opcodes, and only one of them makes it an adder. That is the claim to test:
for opcode
00, this circuit computesA + B
Note what that claim is not: "the output looked like a sum for the values I tried". It has to hold for all 65536 combinations of A and B at once, and establishing that without trying them one by one is exactly the kind of job an SMT solver exists for.
Four steps get you there. Reconstruct a model of what the circuit actually computes, build a model of what it should compute, construct a constraint comparing both models, and query the solver.
Start from the output. Each of the eight pins of group Z carries one bit of the result, so collect one Boolean function per pin and combine them into a single 8-bit function.
get_subgraph_function() does the reconstruction. Given an output net and a set of gates, it walks backwards from that net through the gates, merging their Boolean functions into one, and stops when it reaches either a non-combinational gate such as a flip-flop or a gate outside the set it was given. What comes back is a Boolean function expressed in variables named net_<ID>, one per input net of the subcircuit.
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)The last line is what turns eight separate 1-bit functions into one 8-bit function. get_boolean_function_from() concatenates a list in order, and the first element becomes the most significant bit. That matches the loop above, because get_pins() hands out the pins of Z starting at Z(7), so bit 7 of alu_func really is Z(7).
This is where the bit order mentioned at the top stops being a footnote. Concatenate the same eight functions the other way round and you still get a perfectly valid 8-bit function — just not the one the circuit computes — and the proof in step 4 would fail for reasons that have nothing to do with the ALU.
Print alu_func if you like, but do not expect to learn anything from reading it — it is the flattened logic of 45 gates. That is rather the point: you do not have to understand it, the solver does.
The comparison only means something if both sides talk about the same wires. alu_func is written in net_<ID> variables, so the adder model has to be built from those same variables rather than from fresh symbols.
get_boolean_function_from() does that when handed a pin group: it takes the nets passing through the group and concatenates them into one function of the right width. Print var_a to see it — the ++ is concatenation.
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)Add() then states the model itself. It is a word-level operation — a single node meaning "add these two 8-bit values" — and the solver understands it natively. That is the whole asymmetry of this comparison: alu_func is bit-level logic scraped out of a circuit, adder_func is arithmetic, and the solver is what reconciles the two.
The trailing 8 is the bit-size of the operation. Both operands have to be 8 bits and the result is 8 bits too, so the carry out of the top bit is simply dropped and the addition wraps: 255 + 1 gives 0, not 256. That is not a shortcut, it is what the circuit does — Z is eight wires and has nowhere to put a ninth bit. Model it as a 9-bit addition and the two could never agree.
adder_func is worth printing. Unlike alu_func it is short and readable, because it says what it means rather than how it is built from gates.
A solver takes a set of constraints and looks for one assignment of the inputs that satisfies all of them at once. It answers Sat if it finds one, Unsat if it can prove none exists, and Unknown if it runs out of time — SMT solving is exponential in the worst case.
So asking alu_func == adder_func would be a mistake. The solver would happily report Sat on finding a single input where the two agree, which proves nothing. (A or B) == (A and B) is Sat too, satisfied by A = B = 1, and those functions are obviously different.
The trick is to ask for the opposite and hope to fail. Constrain the two functions to be unequal: if the solver cannot find any input that makes them differ, they are equal everywhere, which is the proof you wanted.
adder_cstr = hal_py.SMT.Constraint(hal_py.BooleanFunction.Not(hal_py.BooleanFunction.Eq(adder_func, alu_func, 1), 1))The trailing 1 on both Eq and Not is the output width. Eq compares two 8-bit functions but yields a single bit, true or false.
The claim was only ever about opcode 00, so pin the opcode down with a second constraint. Same shape: build a variable from the op pin group and require it to equal the 2-bit constant 0.
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))Hand both constraints to a solver and ask. The query configuration picks the engine — z3 here — and a timeout in milliseconds.
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)You should get:
SolverResultType.UnSat
Unsat means the solver could not find any pair of inputs for which the ALU disagrees with an adder while the opcode is 00. Not "it matched on the cases we tried" — no such input exists. For opcode 00, this circuit is an adder, and you know it for all 65536 input pairs without simulating one of them.
Now change the constant in op_code_cstr from 0 to 1, 2 or 3 and run it again. Each of them returns Sat: the solver immediately finds inputs where the ALU and an adder disagree, because under those opcodes the circuit is doing something else entirely.
- Work out what the other three opcodes do. Build a model the way you built
adder_func— subtraction, bitwise AND, whatever you suspect — and see which one comes backUnsat. - Notice what you never had to do: understand
alu_func. Comparing a circuit against a model you do understand is often far less work than reading the circuit. It is not a free lunch, though — as in step 3, solving is exponential in the worst case, so a much larger subcircuit may simply time out and answerUnknown. When that happens the usual move is to cut the problem down: prove one slice at a time, or fix more inputs to constants as the opcode was fixed here. - Try Toy Cipher next. It is the first design too large to stare at, which is where dataflow analysis and simulation start earning their keep.