Skip to content

Module Identification

Jump to bottom
julianspeith edited this page Aug 12, 2026 · 2 revisions

The module identification plugin automatically locates groups of gates in a flat netlist that implement a recognizable word-level operation — an addition, a comparison, a counter, a multiplication with a constant — and annotates them in the netlist as modules.

This plugin is not built by default. Rebuild HAL with -DBUILD_ALL_PLUGINS=ON or -DPL_MODULE_IDENTIFICATION=ON, see Building HAL.

Why this matters

Dataflow analysis recovers the registers of a design — where data is stored. It says nothing about what happens to that data in between. Module identification closes the other half of the gap: it recovers the operations connecting those registers.

The reason this is hard is that synthesis destroys arithmetic. An 8-bit addition does not survive as an "adder" in a gate-level netlist; it becomes a pile of LUTs and carry cells indistinguishable from any other combinational logic by structure alone. Recognizing it again requires reasoning about what the logic computes rather than how it is wired — which is exactly what this plugin does, using an SMT solver to prove that a candidate subcircuit implements the operation it is suspected of implementing.

The payoff is that a design stops being a graph and starts being a datapath. Once you know that this block adds two registers and that block compares one against a constant, you can read the circuit at the level its designer wrote it.

What it can recognize

The plugin verifies candidates against a fixed library of operation types (CandidateType), mostly of arithmetic nature:

  • addition, addition_offset (addition with a constant offset), subtraction
  • counter
  • negation, absolute
  • constant_multiplication, constant_multiplication_offset
  • equal, less_than, less_equal, signed_less_than, signed_less_equal
  • value_check (comparison against a constant)

Note that some types are verified by the same procedure — selecting addition implicitly also covers subtraction, for instance. The all_checkable_candidate_types list contains the types you can select explicitly; restricting it is a performance measure, not a way to filter results by preference.

Building structural candidates is architecture-dependent and must be implemented per target technology. At present, netlists using the Xilinx UNISIM and Lattice iCE40 gate libraries are supported.

How it works

The analysis runs in four stages:

  1. Base candidates. The plugin identifies starting points for its search — small groups of gates that look like they could be part of an arithmetic structure.
  2. Structural candidates. Around each base candidate it builds variants that additionally include different subsets of the surrounding gates. This is the architecture-dependent step.
  3. Functional candidates. For each structural candidate, the plugin works out which subgraph inputs belong to which operand and in which bit order, and which signals are control rather than data. Since this information often cannot be reconstructed with certainty, it guesses — producing several functional candidates per structural candidate, each proposing a different operation on a different assignment of operands.
  4. Verification. Every functional candidate is checked with an SMT solver, which either proves that the subgraph computes the proposed operation or rules the guess out.

What survives is a set of verified candidates per base candidate. A final post-processing step picks which one to annotate, weighing metrics such as candidate size, operand widths, output width, and number of control inputs.

This guess-and-verify design is what makes the results trustworthy: a verified candidate is not a heuristic match but a proven functional equivalence. It is also why the analysis is computationally expensive — expect it to take a while on large netlists.

Running the analysis

The plugin is used from Python via the module_identification module. A run needs a Configuration and is started with execute (whole netlist) or execute_on_gates (a subset).

from hal_plugins import module_identification

config = module_identification.Configuration(netlist)
res = module_identification.execute(config)

res.create_modules_in_netlist()   # annotate every verified candidate as a HAL module

create_modules_in_netlist is usually what you want at the end: it writes the results back into the netlist as modules, so the recovered operations show up in the Modules Widget and can be folded in the graph view.

To analyze only part of a design — a recovered register's fan-in cone, say — use execute_on_gates:

res = module_identification.execute_on_gates(some_module.get_gates(), config)

Configuration

Configuration follows HAL's with_* builder style, so options can be chained:

config = (module_identification.Configuration(netlist)
          .with_known_registers(registers)
          .with_max_thread_count(8)
          .with_max_control_signals(3)
          .with_types_to_check([module_identification.CandidateType.addition,
                                module_identification.CandidateType.less_equal]))
Option Effect
with_known_registers Provide register groupings as a list of gate lists so the plugin can prioritize candidates consistent with them. The most valuable option — feed it get_group_list() from a dataflow analysis run
with_types_to_check Restrict which operation types are checked. Defaults to all checkable types; narrowing it is purely a runtime optimization
with_max_thread_count Maximum number of concurrent threads. Defaults to 1, so raise it — verification parallelizes well
with_max_control_signals Maximum number of control signals to test per candidate. Defaults to 3. Raising it broadens the search considerably at significant cost
with_multithreading_priority memory_priority (default) or time_priority. Use the latter only if you have RAM to spare
with_already_classified_candidates Gates to ignore. Candidates overlapping them are discarded, which is how you run the plugin iteratively without re-finding the same structures
with_blocked_base_candidates Base candidates to skip entirely

No prior information is required to run the plugin. However, supplying known registers noticeably improves the results, which makes the natural workflow: run dataflow analysis first, then hand its register groups to module identification.

from hal_plugins import dataflow, module_identification

dana_res = dataflow.analyze(dataflow.Configuration(netlist).with_flip_flops())
registers = dana_res.get_group_list()   # list of gate lists, one per recovered register

config = module_identification.Configuration(netlist).with_known_registers(registers)
res = module_identification.execute(config)
res.create_modules_in_netlist()

Inspecting the results

The Result object gives access to everything the run produced, whether or not you write it back into the netlist.

candidates = res.get_verified_candidates()   # dict from candidate ID to VerifiedCandidate
for cid, cand in candidates.items():
    print(cand.get_name())
    print(cand.get_candidate_info())
  • get_verified_candidates() — the verified candidates as a dict from ID to VerifiedCandidate
  • get_candidates() / get_candidate_by_id() — all candidates, including unverified ones
  • get_candidate_gates() / get_verified_candidate_gates() — the gates belonging to candidates
  • get_all_verified_gates() — every gate covered by any verified candidate, useful for measuring how much of the design was explained
  • get_timing_stats() — timing information as a JSON string, helpful when tuning the configuration

A VerifiedCandidate describes one recovered operation. get_candidate_info() returns a human-readable summary, and the individual attributes expose the details: operands, output_nets, control_signals, control_signal_mappings, gates, base_gates, total_input_nets, total_output_nets, types, and word_level_operations. is_verified() reports whether the SMT check succeeded.

cand = res.get_candidate_by_id(cid)
print(cand.types)             # the operation type(s) this candidate implements
print(len(cand.operands))     # how many operands it takes
print(cand.control_signals)   # signals identified as control rather than data

Practical notes

  • Start small. Run execute_on_gates on a module you already suspect is a datapath before launching a full-netlist run. SMT verification is expensive and a whole design can take a long time.
  • Raise the thread count. The default of 1 leaves most of the work serialized.
  • Run dataflow analysis first. Known registers improve both the quality and the speed of the results.
  • Check the coverage. Comparing get_all_verified_gates() against the netlist size tells you how much of the design the plugin could explain, and hence how much of it is arithmetic at all.

See also

Clone this wiki locally