Solve FSM

The solve_fsm plugin extracts the state transition graph of a finite state machine from a gate-level netlist. Given the flip-flops that form the state register and the combinational gates that compute the next state, it determines every reachable state and the input condition under which each transition is taken.

The plugin is built by default, see Building HAL.

Why this matters

Controllers are where a design's behavior is decided. A datapath tells you what operations exist; the FSM driving it tells you when they happen — the protocol, the handshake, the sequence of rounds, the condition that unlocks something. Recovering it usually tells you more about a design's purpose than anything else you can extract.

Synthesis leaves nothing of that structure behind. The states become bit patterns in a handful of flip-flops, encoded in whatever scheme the tool chose (binary, one-hot, gray), and the transitions become an undifferentiated cloud of combinational logic. This plugin reconstructs the state graph from that, which is the behavioral description the netlist was synthesized from in the first place.

FSM structure is also a target for obfuscation, so being able to recover it is what lets you evaluate such schemes, see HAL in Academia.

What you have to provide

The plugin does not find the FSM for you. You must supply two sets of gates:

• state register — the flip-flops holding the current state
• transition logic — the combinational gates computing the next state from the current state and the inputs

Identifying these is the reverse engineering work. Useful starting points: dataflow analysis groups flip-flops into registers, and a state register is recognizable as a small register that feeds back into itself through combinational logic. The FSM example project ships with the modules already annotated so you can see what the input should look like.

Usage

from hal_plugins import solve_fsm

state_reg = netlist.get_module_by_id(2).get_gates()
transition_logic = netlist.get_module_by_id(3).get_gates()

transitions = solve_fsm.solve_fsm(netlist, state_reg, transition_logic,
                                  graph_path="fsm.dot")

solve_fsm takes the following arguments:

Argument	Meaning
nl	The netlist to operate on
state_reg	List of flip-flop gates forming the state register
transition_logic	List of combinational gates forming the transition logic
initial_state	Dict from state register flip-flop to its initial Boolean value. Defaults to an empty dict, in which case the initial state is all zeros
graph_path	Where to write the state transition graph in DOT format. No file is written if left empty
timeout	Timeout for the underlying SAT solver in milliseconds. Defaults to 600000 (10 minutes)

It returns a dict from each state to a dict of its successor states and the Boolean function describing the condition for that transition — or None on failure.

for state, successors in transitions.items():
    for successor, condition in successors.items():
        print(f"{state} -> {successor} when {condition}")

Brute force variant

solve_fsm_brute_force(nl, state_reg, transition_logic, graph_path="") explores the state space exhaustively instead of using the SAT solver. It takes the same gate sets but no initial state or timeout.

Use it as a cross-check on a small FSM, or when the symbolic approach struggles. It becomes impractical quickly, since the cost grows exponentially with the width of the state register.

Rendering the graph

If graph_path is set, the plugin writes the state transition graph as a DOT file. You can view it with the dot viewer plugin, or convert it outside of HAL:

dot -Tpng -ofsm.png fsm.dot

generate_dot_graph(state_reg, transitions, graph_path, max_condition_length=128, base=10) produces the same output from a transition dict you already have. max_condition_length caps how much of each transition condition is printed — worth lowering when conditions are long enough to make the graph unreadable, and base controls the numeric base used for state labels (10 by default, 16 is often more readable for wide state registers).

Practical notes

• Get the two gate sets right. Including unrelated combinational logic in transition_logic inflates the search; omitting relevant gates yields a wrong graph. Isolating the candidate FSM into modules first makes this manageable.
• Watch the state count. A state register wider than about 16 bits may have far more reachable states than you can read in a graph. Consider whether you really found a state register or a counter.
• Unreachable states are informative. States that never appear in the result are dead code — or, in an obfuscated design, deliberately planted decoys.

See also

• FSM — the example project demonstrating this plugin end to end
• Dataflow Analysis — recovering the register candidates to feed in
• Boolean Function — the representation used for transition conditions
• Dot Viewer — viewing the resulting graph inside HAL