Skip to content

Keep array bits and hierarchy when reconstructing a synthesized circuit

Alexander requested to merge smt-target into main

The witness-to-circuit reconstruction named signals by Signal.name, which carries neither the bit selector nor the hierarchical prefix. A 4-bit adder's a[0]..a[3] therefore became four ports all named a, flatten collapsed them onto one signal, and comparable_netlists rejected the pair on a name-set mismatch -- so equivalence_check reported a correct circuit as inequivalent, without ever building a miter. Targets written with scalar ports were unaffected, which is why only the bit-vector examples failed.

ModuleBuilder now names signals by reference -- a[0] for an array bit, ci for a scalar -- declaring one sized port per array and widening it as later bits arrive, and folds a signal's prefix into its name (fa0.f becomes fa0_f) since the circuit grammar's identifiers are plain CNAMEs with no syntax for hierarchy. flatten expands sized declarations back into per-bit signals and keys its map on full signal identity, so it now agrees with what llogic's own parser makes of the same rendered text.

Merge request reports

Loading