Skip to content

Bitorder Propagation

Jump to bottom
julianspeith edited this page Aug 25, 2026 · 5 revisions

The bitorder_propagation plugin recovers the bit order of module pin groups by propagating known orderings through the netlist. Given one pin group whose bit order you know, it determines the order of connected pin groups whose order you do not.

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

Why this matters

Recovering a register tells you that 32 flip-flops belong together. It does not tell you which one is bit 0.

That missing piece blocks everything word-level. A 32-bit value read in the wrong bit order is a different number; a comparison against a constant becomes meaningless; an SMT check against a model of an adder fails even though the circuit is an adder. Any analysis that treats a group of nets as an integer — module identification, equivalence checks against a reference implementation, interpreting simulation output — silently produces wrong results if the bit order is wrong.

Synthesis does not preserve this information. Bit indices live in signal names, and those are exactly what gets destroyed. So the order has to be reconstructed from circuit structure: carry chains run from least to most significant bit, shift registers step one position per stage, and a comparison against a constant only works out for one assignment.

The insight this plugin builds on is that bit order propagates. Once you know the order at one point, the connectivity of the design carries it to everything that point connects to. Establishing one anchor by hand can therefore resolve the order of many pin groups automatically.

Prerequisites

The plugin operates on module pin groups, not on loose nets. Before using it you need:

  1. Modules with pin groups. Dataflow analysis creates modules for recovered registers; the pins of those modules are what gets ordered.
  2. At least one known bit order to start from — the anchor. This is the part you have to establish yourself, typically from a carry chain (see get_gate_chain in Decorators), from global inputs and outputs whose meaning is known, or from a design constant you recognize.

Usage

Source and destination are identified by a (module, pin group) pair, or by a (module ID, pin group name) pair.

from hal_plugins import bitorder_propagation

src = (known_module.get_id(), "A")
dst = (unknown_module.get_id(), "B")

known_orders = bitorder_propagation.propagate_bitorder(netlist, src, dst)

propagate_bitorder returns a BitOrderResult — the orders it derived together with the ones it was given — or None on failure. Overloads accept lists of sources and destinations to resolve several groups in one run.

A BitOrderResult holds one BitOrder per pin group, and a BitOrder is a module, a pin group, and the index of each of its nets:

for bit_order in known_orders:
    print(bit_order.module.name, bit_order.pin_group.name)
    for net, index in bit_order.order:
        print(f"  {index}: {net.name}")

# or ask about one pin group directly
bit_order = known_orders.get(unknown_module, pin_group)
if bit_order is not None and bit_order.is_continuous():
    net_of_bit_0 = bit_order.get_net_at(0)

Iterating over a result walks the bit orders by module and pin group ID, so a run reads the same from one invocation to the next.

Applying the result

Propagation computes the bit order but does not by itself rearrange anything. reorder_module_pin_groups(bit_orders) takes a BitOrderResult and reorders the actual pin groups in the netlist to match, returning True on success.

bitorder_propagation.reorder_module_pin_groups(known_orders)

After this, the pin groups are in the correct order, and word-level tooling built on them — for example BooleanFunctionDecorator.get_boolean_function_from(pin_group), see Decorators — yields correct multi-bit variables.

Further functions

propagate_module_pingroup_bitorder(src, dst, enforce_continuous_bitorders=True) is the lower-level entry point, taking the known orders as a BitOrderResult you build yourself:

anchor = bitorder_propagation.BitOrder(known_module, known_pin_group, [(net, i) for i, net in enumerate(bus_nets)])
result = bitorder_propagation.propagate_module_pingroup_bitorder(
    bitorder_propagation.BitOrderResult([anchor]), {(unknown_module, unknown_pin_group)}
)

enforce_continuous_bitorders governs what may be given, not what comes back: with it set to False an anchor whose indices leave a gap is accepted, and with it left at True such an anchor yields no order for the destination at all — quietly, with no error. What is reconstructed is continuous either way. Leaving it enabled is generally right, since an anchor that is not continuous usually means the anchor is wrong.

export_bitorder_propagation_information(src, dst, path) does not propagate anything. It writes the problem out as JSON so that something other than HAL can solve it: every pin group involved as an indexed "word", the orders already known, and how the words connect. It returns the index each pin group was given among those words, so the numbers in the file can be related back to real pin groups. Reach for it when propagation cannot reconstruct an order and you want to attack it with a solver of your own.

Practical notes

  • The anchor decides everything. Propagation faithfully spreads whatever you give it, including a wrong order. Verify your starting point before trusting the output.
  • Check for continuity. BitOrder.is_continuous() tells you whether the indices run from 0 without a gap. An anchor that is not continuous usually means the anchor or the pin grouping is off, rather than a genuinely sparse bus.
  • Run it before word-level analysis, not after. Module identification benefits directly from correctly ordered operands.

See also

Clone this wiki locally