write_blif: name CIs after the node, not the topological index - #704
Merged
Conversation
`topo_view` reimplements `node_to_index` as the position in the topological order,
while every other reference in this writer -- fanin lists and PO bridges -- names a
node by its raw id. The two agree only while the CI node ids happen to be
contiguous.
They are not contiguous in general. A `klut_network` produced by `lut_map` has gaps,
and so does any network where a primary input is created after a gate. There the
`.inputs` line declares names nothing reads, and the `.names` bodies reference names
that were never declared:
.inputs pi2 pi3 pi4
...
.names new_n4 pi5 new_n6
`pi4` is dead and `pi5` is undeclared. Lorina's own BLIF reader rejects that, but ABC
accepts it and ties the undeclared signal to constant 0 -- so the netlist reads back
as a well-formed circuit computing something else, with no error anywhere.
Found by combinational equivalence checking a mapped EPFL `mem_ctrl`, which came back
NOT_EQUIVALENT with 39 phantom inputs.
Fixed by deriving the name from the node, which is what the rest of the writer does.
The added test builds the smallest network with a CI gap and pins the exact output.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## master #704 +/- ##
==========================================
- Coverage 84.07% 84.06% -0.02%
==========================================
Files 190 190
Lines 29513 29513
==========================================
- Hits 24813 24810 -3
- Misses 4700 4703 +3 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
marcelwa
added a commit
to marcelwa/mockturtle
that referenced
this pull request
Aug 31, 2026
* write_blif: name CIs after the node, not the topological index (lsils#704) `topo_view` reimplements `node_to_index` as the position in the topological order, while every other reference in this writer -- fanin lists and PO bridges -- names a node by its raw id. The two agree only while the CI node ids happen to be contiguous. They are not contiguous in general. A `klut_network` produced by `lut_map` has gaps, and so does any network where a primary input is created after a gate. There the `.inputs` line declares names nothing reads, and the `.names` bodies reference names that were never declared: .inputs pi2 pi3 pi4 ... .names new_n4 pi5 new_n6 `pi4` is dead and `pi5` is undeclared. Lorina's own BLIF reader rejects that, but ABC accepts it and ties the undeclared signal to constant 0 -- so the netlist reads back as a well-formed circuit computing something else, with no error anywhere. Found by combinational equivalence checking a mapped EPFL `mem_ctrl`, which came back NOT_EQUIVALENT with 39 phantom inputs. Fixed by deriving the name from the node, which is what the rest of the writer does. The added test builds the smallest network with a CI gap and pins the exact output. * 🐛 Fix reading a latched AIGER file into a combinational network (lsils#705) * 🐛 Fix reading a latched AIGER file into a combinational network `aiger_reader::on_header` only materialized the latch outputs when the network type implements `create_ro`. For one that does not, the reader's `signals` vector was left short by exactly the latch count, while every AIGER literal above the primary inputs still assumed those slots existed. `on_and` then indexed past the end of the vector and handed the garbage it read to `create_and`. The only thing standing between that and undefined behaviour was assert( num_latches == 0 && "network type does not support the creation of latches" ); which is compiled out under `NDEBUG` -- that is, in every release build. The result was a segmentation fault on any design whose logic reaches far enough past the latch outputs, and a silently wrong network on any that does not: a one-latch file whose literals all stay in bounds parsed "successfully" into a network missing its registers entirely. Reading a latched file into a combinational network now flattens one timeframe of the design instead. Each latch output becomes a primary input, appended behind the file's own primary inputs, and each latch next-state function becomes a primary output, appended behind the file's own primary outputs. That is the transformation ABC calls `comb`; it loses no logic, keeps every literal resolving to the signal the file names, and makes the network type in this reader's own documented example -- `mig_network`, which has no registers -- work on a sequential file rather than crash on one. Recording and naming latches is no longer conditional on the network type either, since the flattened path needs both. The header and the destructor also disagreed about which trait decides whether a network can hold registers, `create_ro` in one and `create_ri` in the other; both now consult a single `has_registers` predicate, which is what let them drift apart to begin with. * Warn when flattening latched AIGER --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com> Co-authored-by: MyskYko <yoyuohlhjl@yahoo.co.jp> * Fix uninitialised read in lut_map on networks with dangling nodes `cut() = default` leaves `_length`, `_cend` and `_end` indeterminate. A default-constructed cut is reachable: `cut_set` and `lut_cut_set` hold an array of them and `best()` returns `*_pcuts[0]` whether or not any cut has been inserted. `lut_map_impl::compute_share_mapping_init` iterates over every node index and calls `best()`, and a node unreachable from the outputs is never visited by the cut enumerator, so its cut set is empty and the following `for ( auto leaf : cut )` in `compute_cut_data` walks a garbage end pointer and indexes `cuts[leaf]` with whatever it finds. Networks with unreachable nodes are not exotic: ABC's `&dch -f; &put` leaves the choice-class members in as ordinary AND nodes, so every AIG written by the standard `strash; &get; &dch -f; &put; write_aiger` front end has them (cavlc: 1271 ANDs written, 647 reachable). Give the default constructor a defined empty state, and add a lut_mapper test that maps a six-gate AIG whose last four gates drive no output.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
write_blifnames combinational inputspi{topo_ntk.node_to_index(n)}, while every other reference in the same writer — fanin lists and the PO bridges — names a node by its raw id.topo_viewreimplementsnode_to_indexas the position in the topological order, so the two agree only for as long as the CI node ids happen to be contiguous.They are not contiguous in general. A
klut_networkproduced bylut_maphas gaps in them, and so does any network where a primary input is created after a gate.What it produces
The smallest case — two PIs, an AND, then a third PI:
Why it is worth fixing rather than working around
The output is not malformed in a way anything reports.
lorina::read_blifdoes reject it, but ABC accepts it and ties the undeclared signal to constant 0 — so the file reads back as a well-formed circuit that computes a different function, silently, with the right port count.I hit this running combinational equivalence checking over LUT-mapped EPFL circuits:
mem_ctrlcame back NOT_EQUIVALENT with 39 phantom inputs, and it took a while to believe the writer rather than the mapper.The change
Two lines: derive the name from the node, which is what the rest of the writer already does. The named-network branch has the same problem — it calls
make_signal(node_to_index(n)), sohas_name/get_nameare looked up against the wrong signal — and is fixed the same way.The added test builds the smallest network with a CI gap and pins the exact output. It fails on master (both the string comparison and the
blif_read_after_write_teston top of it) and passes with the change; the rest of the suite is unaffected — 917 test cases, 133227 assertions green.