-
Notifications
You must be signed in to change notification settings - Fork 97
FSM
The FSM example project is the smallest netlist shipped with HAL and the recommended place to start. It has 21 gates, which is few enough to fit on screen at once and to understand gate by gate.
This page is a guided tour rather than a reference, and it assumes you have never opened HAL before. It comes in two parts. Part 1 walks through the HAL GUI and shows you how to explore a netlist. Part 2 is the actual work: five steps that take the netlist from a flat pile of gates to the state transition graph of the finite state machine it implements.
Requirements
| Requirement | Type | Needed for | Availability |
|---|---|---|---|
netlist_preprocessing |
plugin | removing the buffers | built by default |
solve_fsm |
plugin | recovering the state transition graph | built by default |
dot_viewer |
plugin | displaying that graph inside HAL | built by default |
z3 |
dependency | solving for the state transitions | must be installed and on the path |
All three plugins are built by default but might still have to be enabled in the Plugin Manager.
solve_fsm hands the transition logic to an SMT solver, and by default that means calling the z3 binary, so it has to be installed and findable — see Building HAL. If you would rather not install it, the solver also has a brute force mode that needs no external tool; step 5 says how to switch it on.
The project ships as the zipped HAL project hal/examples/fsm.zip. Do not unpack it by hand — choose File > Import Project, point it at the archive, and pick where it should end up. HAL extracts it and opens the project for you. See import project for details.
Unlike a netlist you would get from real hardware, this one already comes with a fully annotated gate library that HAL understands. In a real-world case, you would need to provide such a gate library yourself.
Nothing in this part modifies the netlist. Try every control as you read; you cannot break anything yet.
HAL opens with the graph view in the middle and several widgets docked around it.
The Graph View is the large area in the middle. After importing, it shows the default view of a fresh netlist: a single box, the folded top_module. Every gate in the design sits inside it.
Double-click that box to unfold it and see the circuit. Because this view contains nothing but top_module, it is unfolded in place: the single box is replaced by the 21 gates inside it. Boxes are gates, lines between them are nets, and each box shows the gate name, its type, and its input and output pins.
Only unfold small modules. Twenty-one gates fit on a screen; a few thousand do not. Unfolding a large module takes a long time to lay out and leaves you with a picture too dense to read. On a real-world design you keep the hierarchy folded and focus only on the parts you are working on.
Two things are worth noticing straight away. The names are meaningless — U1, U2, U3 and so on — which is what a netlist recovered from a real chip looks like. The types, however, are real: LUT6, FFR, MUX, BUF. Type information comes from the gate library and are essential for understanding a netlist's implemented functionality.
The Modules Widget on the left shows the module hierarchy. Right now it holds a single entry, top_module, with all 21 gates directly inside it — a completely flat design. Recovering a hierarchy is a large part of what reverse engineering a netlist means, and in Part 2 you will build one by hand.
Click any gate in the graph view and the Selection Details Widget at the bottom fills up. This is where you find out what a gate actually does:
- its name, ID and type
- its pins, and which net is attached to each
- for combinational gates, the Boolean function of each output pin
Click one of the LUT6 gates and look at its Boolean function. That expression, not the gate name, is the ground truth about what the gate computes.
The Python Editor is docked on the right, the Python Console at the bottom. They both enable you to write and execute scripts that interact with the netlist using HAL's Python API. Anything you can do from the GUI you can also do from here — the GUI and the API operate on the same netlist, so a script's changes show up in the graph immediately. The editor already has this project's script open, fsm.py. Before you can actually run the script, you will have to modularize the netlist by hand in Part 2.
The Log Widget, also at the bottom, shows what HAL is doing. Most of the time you can ignore it, but it is the first place to look when something goes wrong: a plugin that fails reports the reason only here, and an error in a script shows up here as well as in the console.
Everything the Graph View shows is a view: a chosen subset of the netlist's gates, nets and modules, laid out in its own tab. A view is not the netlist — adding something to a view or removing it again changes only what you are looking at, never the design. Importing the project gave you one view, the folded top_module, and you can open as many more views as you want. They are listed in the Views Widget on the left, which is also where you can organize your views and delete the ones you no longer need. Even if you close the tab of a view in the Graph View, it will stay alive in the Views Widget.
Views are helpful to focus on what you are really interested in: you never look at the entire netlist all at once, but you focus on the gates around the part you currently care about.
There is one important thing to note: the current selection of gates, nets, and modules is not per-view. Selecting a gate selects it everywhere — in every open view, in the modules widget and in the selection details. You can select something in one view, switch to another tab, and it is still selected there.
These are the controls you will use constantly, so work through them here where the netlist is small and nothing is at stake.
Zoom and pan. Scroll to zoom. To pan, hold Shift and drag with the left mouse button; this only does something once you are zoomed in far enough that the view no longer fits on screen. Select. Click a gate to select it. Ctrl-click (⌘-click on macOS) adds a gate to the selection, and dragging a rectangle across the background selects everything inside it at once. Whatever you pick here is what the Selection Details widget describes.
Move things around. Drag a selected gate to an empty grid position to rearrange the layout. Dropping it onto an occupied position while holding Alt (⌥ on macOS) swaps the positions of the two gates within the current view.
Follow a net with the arrow keys. Select a single gate and its pins light up cyan. Press → to head towards its outputs or ← towards its inputs, use ↑ and ↓ to pick a pin, then press → or ← again to jump along the net to the gate on the other end. If the net has several destinations, a popup lets you choose. It is much faster than tracing lines by eye, and on a large netlist it is the only practical way.
Isolate and grow a cone view. Select a gate, right-click, and choose Isolate in new view. You get a new view containing only that gate. From that starting point you grow the picture outwards: the arrow-key navigation above adds gates as you walk to them, and right-clicking offers Successor/Predecessor → Add successors to view or Add predecessors to view with a depth from 1 to 5. There is also Add path to successor to view, which pulls in every gate along the way to one particular gate. This is how you usually look at a big netlist: never all at once, just a cone around whatever you care about.
Remove things again. Select what you no longer want to see in your view and right-click → Remove selected items from view. Only the view changes; the gates stay in the netlist.
Fold and unfold modules. This is how you control the level of detail: a folded module is one box, an unfolded one is everything inside it. Right-click a module and choose Unfold module to open it up, or right-click a gate and choose Fold parent module to close the module around it again.
Double-clicking a module unfolds it too, with one wrinkle: it only unfolds in place if the view contains nothing but that module, as the starting view did. Otherwise it opens the module in a view of its own instead.
Put gates into a module. Select gates, right-click and choose Move to module. A dialog lets you pick an existing module or create a new one; choosing new asks for a name and creates the module under the common parent of everything you selected. Unlike everything above, this one does change the netlist, but only its hierarchy. Gates and their interconnecting nets remain unchanged.
When you create a new module this way and all the selected gates were in the current view, the view swaps them for the new module's box, placed where the first of them sat — which is simply the folded state described above.
From here on you are changing the netlist. Each step says what to look for before it says what to do, so try to find it yourself before reading on — the tracing is the point, not the result.
The netlist is a finite state machine. Any synchronous FSM, however it was written, comes out of synthesis in three parts:
- a state register — flip-flops that hold the current state, and nothing else
- transition logic — combinational gates computing the next state from the current state and the inputs
- output logic — combinational gates computing the outputs
That is the shape you are looking for, and steps 2 to 4 find one part each. In this design the interface is:
-
CLK, and five inputsINPUT_0…INPUT_4 - two outputs
OUTPUT_0andOUTPUT_1
and the 21 gates break down as 9 buffers, 4× LUT6, 2× MUX, 2× FFR flip-flops, a LUT1, a LUT2, and a GND/VCC pair. Nine of twenty-one gates are buffers, and none of them are part of any of the three parts above. That is where to start.
A buffer computes nothing. Its output is its input: O = I. Synthesis and place-and-route insert them for electrical reasons — to drive a long wire, to sharpen a slow signal edge, to balance the delay of a clock so that every flip-flop sees the edge at the same moment. In this netlist they sit between the ports and the logic, and two of them sit in a row on the clock.
Every one of those reasons is about timing and electrical behaviour, never about logic. A buffer changes when a signal arrives, never what it is, so it contributes nothing to what the circuit computes — which is the only thing you care about here. What it does contribute is work: each one puts an extra hop in every path you trace, and tells you nothing when you arrive at it. Nine of them in a 21-gate design is a lot of noise, and on a real netlist there can be thousands. Removing them is almost always the first thing you do.
The catch is that a buffer is not always a gate called BUF. A synthesizer will happily implement one as a one-input LUT whose function is O = I0, and that gate is a buffer in everything but name. HAL's buffer removal looks at what a gate computes rather than what its type is called, so it catches those too — and it catches gates that have become buffers by accident, such as an AND2 with one input tied to constant 1.
To run it, right-click on empty space in the graph view — not on a gate — and look for the Plugin actions heading at the bottom of the menu. Under it, open Netlist Preprocessing and choose Remove buffers from netlist.
Make sure nothing is selected before you do. The menu reads the current selection, and while something is selected it offers Remove buffers from selection instead, which is what you want on a large design but not here.
The log reports what happened:
removed 10 buffer gates from netlist with ID 1.
Ten, not nine. The extra one is the LUT1, which computed O = I0 — exactly the disguised buffer described above. This is worth pausing on: nothing marked that gate as a buffer, and reading the netlist by eye you would probably have carried it around as part of the output logic. Its Boolean function gave it away.
Eleven gates are left: the four LUT6, the two MUX, the two FFR flip-flops, the LUT2, and the GND/VCC pair. Every one of them does something. Note also that removing a buffer does not remove the port it was attached to — CLK, INPUT_0 … INPUT_4, OUTPUT_0 and OUTPUT_1 are all still there, the logic simply connects to them directly now.
This changes the netlist. Unlike everything in Part 1, this deletes gates for real, and the project has no undo for it. That is fine here — the buffers carry no information — but on your own designs it is worth knowing which preprocessing steps are destructive.
The state is whatever is stored, so look for flip-flops. There are exactly two FFR gates. Select both and move them into a new module called STATE_REGISTER.
Look at their pins in the Selection Details widget while you have them selected. Both take their clock from the same net, their reset comes from the GND gate and their clock enable from VCC — so reset and enable are tied off and can be ignored. What matters is D, the next state going in, and Q, the current state coming out. Two flip-flops means two state bits, so at most four states.
Everything that computes D belongs here. Select one flip-flop, use ← to walk backwards out of its D pin, and see where you land. Repeat for the other one.
You should find a MUX in front of each flip-flop, and behind the two multiplexers four LUT6 gates. Notice what feeds them: each LUT6 takes the five inputs plus one state bit, and the two multiplexers are steered by the other state bit. So the next state depends on both state bits and all five inputs, which is exactly what transition logic is supposed to do.
Select those six gates — the four LUT6 and the two MUX — and move them into a module called TRANSITION_LOGIC.
Now walk forwards instead. Select a flip-flop and press → out of its Q pin.
The state bits go to two places: back into the transition logic you just built, and forwards to the outputs. Following them there is more interesting than it sounds, because the two outputs are reached in quite different ways.
OUTPUT_1 comes from the LUT2, which both flip-flops feed and whose Boolean function is an XOR of the two state bits. That gate is the output logic — move it into a module called OUTPUT_LOGIC.
OUTPUT_0 is the surprise: trace it back and there is no gate at all between the flip-flop and the port. The Q pin is the output. This is where the LUT1 used to sit, passing the state bit through unchanged, so with it gone the machine publishes that state bit directly. OUTPUT_LOGIC therefore holds a single gate.
While you are here, check what the outputs depend on: only the state bits, never the inputs. An FSM whose outputs depend on the state alone is a Moore machine; one whose outputs also depend on the inputs directly is a Mealy machine. You just determined which of the two this is by looking at a single gate and a wire.
Only the GND/VCC pair should be left directly in top_module, tying off the reset and enable pins of the flip-flops. Leaving the two outside the three modules is the right call — they are part of the circuit but not part of the state machine. Had you not removed the buffers in step 1, nine more gates would be sitting here, and you would have had to decide for each of them whether it belonged in a module.
Your Modules widget should now show top_module with three submodules. Note the IDs of the state register and the transition logic, because you will need them in a moment.
With the structure recovered, the analysis is worth automating. fsm.py is in the project's py/ folder and is already open in the Python Editor.
The script identifies what it needs by ID rather than by name, so that it works no matter what you called things. Two module IDs, which you read off the Modules widget, and the nets that carry the outputs, whose IDs you get by selecting a net and reading the Selection Details:
STATE_REGISTER_MODULE_ID = 2
TRANSITION_LOGIC_MODULE_ID = 3
OUTPUT_NET_IDS = [[9], [10]]If you created the modules in the order of the steps above, those are already the right values — top_module is 1 and the rest are handed out in order. The net IDs are the ones this project ships with. Then press the green triangle to run it.
It hands your modules to the solve_fsm plugin, which explores the transition logic symbolically and works out, for each reachable state, which input assignments lead to which successor state. The result is the state transition graph — the behavioral description the netlist was synthesized from.
The outputs are given as net IDs, and you provide them yourself rather than having the script derive them from your OUTPUT_LOGIC module. That is not laziness, it is forced by the circuit: only OUTPUT_1 passes through the output logic. OUTPUT_0 leaves its flip-flop and goes straight to the port, so it is not in that module. Naming the nets is the only way to describe both.
Each entry of OUTPUT_NET_IDS is one output, which is why the IDs are nested in lists — group several net IDs in one entry and they become the bits of a multi-bit output, least significant first. Here each output is a single net.
outputs = [(nets[0].name, nets) for nets in output_nets]
config = (
solve_fsm.Configuration(netlist)
.with_state_register(state_register.get_gates())
.with_transition_logic(transition_logic.get_gates())
.with_outputs(outputs)
)
graph = solve_fsm.solve_fsm(config)
print(graph.to_string())
graph.generate_dot_graph(graph_path)
dot_viewer.load_dot_file(graph_path, "solve_fsm")Everything the solver needs goes into a Configuration, and solving returns the graph without writing or printing anything on its own. Rendering it is a separate step: generate_dot_graph for the picture, to_string for the text, write_txt for the same text in a file.
Run the script and the report starts like this:
FSM with 2 state bits and 4 reachable states
state register (least significant bit first):
bit 0: 'U7' with ID 7
bit 1: 'U9' with ID 9
outputs (least significant bit first):
OUTPUT_0: 'OUTPUT_0' with ID 9
OUTPUT_1: 'OUTPUT_1' with ID 10
nets referenced in the Boolean functions below:
net_25: 'net_25' with ID 25
net_26: 'net_26' with ID 26
...
state 0
outputs:
OUTPUT_0 = 0
OUTPUT_1 = 0
transitions:
to 1 if ((net_25 | net_27) | ((! net_28) | net_29))
to 2 if (((! net_25) & net_26) & ((! net_29) & ((! net_27) & net_28)))
to 3 if (((! net_25) & (! net_26)) & ((! net_29) & ((! net_27) & net_28)))
Compare that with what you found in step 4. OUTPUT_0 has no gate of its own, so in every state its value is simply the value of one flip-flop — and reading down the states you can watch it track that flip-flop exactly. Which of the two it follows is written in the legend above, and it depends on the order in which you selected the flip-flops when you created STATE_REGISTER, because that order decides which one counts as bit 0. Your numbers may therefore differ from the ones printed here while describing the same machine.
Everything else the solver knows is in that text, with no condition cut short: a legend mapping every state bit, output and net variable back to the netlist element it stands for, then one block per state.
The net legend deserves a second look. A variable like net_25 inside a condition is built from the net ID, not its name. In this project the two happen to line up, because the nets are named after their IDs — but on a netlist from real hardware they will not, and then the legend is the only thing that tells you which wire a condition is talking about.
The states themselves are labeled in the picture too, so the graph now says what the FSM does and not only how it moves.
Troubleshooting: If the solver cannot be found, HAL says so in the log. solve_fsm calls the z3 binary by default, but it can enumerate the states instead: add .with_brute_force() to the configuration and no external tool is needed. On an FSM this small that mode is in fact the faster of the two, though its runtime doubles with every flip-flop you add, so it stops being an option on larger machines.
If the script reports that a module or a net does not exist, check the IDs at the top of it against the Modules widget and the Selection Details. If the graph does not appear but the text prints fine, the dot_viewer plugin is not enabled — the .dot file has still been written, and dot -Tpng -ofsm.png fsm.dot renders it outside HAL.
- Work out what the machine actually does: read the conditions on the transitions and see which inputs matter in which state.
graph.to_string()prints them in full, without the truncation the graph labels apply. - Try Simple ALU next. It is the point where looking at gates stops being enough and you start proving what a circuit computes instead of concluding it.