✨ Support sequential networks in write_aiger - #699
Open
marcelwa wants to merge 3 commits into
Open
Conversation
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #699 +/- ##
=======================================
Coverage 84.06% 84.07%
=======================================
Files 190 190
Lines 29468 29510 +42
=======================================
+ Hits 24773 24810 +37
- Misses 4695 4700 +5 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
A sequential network written by ABC could not be read back correctly. Three separate defects, all in the AIGER latch and output handling. **Omitted latch reset values were read as undefined.** Both the binary and the ASCII reader defaulted to NONDETERMINISTIC when a latch line carried no reset field. The format specifies the opposite: the original AIGER format initialized every latch to zero, and the reset field added in 1.9 is optional, so its absence means 0. ABC relies on this and omits the field for zero-initialized latches, so every zero-initialized register came back undefined. **The ASCII reader compared the wrong token.** The branch recognizing a reset value of 1 tested `tokens[1u]`, the next-state literal, instead of `tokens[2u]`. An explicit reset of 1 was therefore never recognized, and a latch whose next-state literal happened to be 1 was wrongly reported as one-initialized. **Bad state properties were dropped.** A writer emitting the AIGER 1.9 extended header moves the primary outputs into the bad-state section; ABC does this for any design with a non-zero latch initialization. `on_bad_state` was not overridden, so those outputs disappeared and the network came back with none. They are now kept as primary outputs, which is what they were, along with their names from the symbol table. Also fix an adjacent defect in the destructor: the output index only advanced for outputs that carried a name, so with a sparse symbol table every name after the first unnamed output landed on the wrong one. Verified end to end against ABC. A network with three registers initialized to 0, 1, and undefined previously returned with no outputs and a corrupted first register; it now round-trips through `resyn2` with its inputs, outputs, registers, and reset values intact. Note that AIGER constraints are still ignored. They are assumptions rather than outputs, so mapping them onto primary outputs would change the meaning of the network. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz
This was referenced Jul 28, 2026
`register_t::init` carried three different encodings of "undefined" at once.
`register_t` itself defaulted to 3, `blif_reader` used 2 for a nondeterministic
latch and 3 for an unspecified one, and `aiger_reader` produced 255 -- the
result of narrowing an `int8_t` of -1 into a `uint8_t` field rather than a
deliberate choice.
That last one corrupted output. `write_blif` emits the initialization verbatim
and the BLIF `.latch` statement accepts only 0, 1, 2, and 3, so a sequential
AIGER file with an undefined latch reset read back and written as BLIF produced
.latch li0 new_n2 255
which no BLIF consumer accepts, ABC included.
Introduce `register_init` with the four documented values, following the BLIF
`.latch` field since it is the most expressive of the supported formats, and use
it consistently across the readers and writers. AIGER has no counterpart for
`unknown`, so a latch without a defined reset maps to `dont_care`.
`register_init::is_defined` expresses the test that callers actually want,
namely whether a reset value is 0 or 1, so code stays correct if a format ever
introduces further undefined states. `register_init::sanitize` keeps `write_blif`
from emitting a value the format cannot represent.
The only value that changes is the one AIGER produced for a nondeterministic
latch, from 255 to 2. Comparisons of the form `init > 1` are unaffected; only
code testing against 255 would notice, and that value was never intentional.
Verified end to end: the AIGER file above now yields `.latch li0 new_n2 2`,
which ABC reads back as one don't-care-initialized latch.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz
`write_aiger` hardcoded a latch count of 0 and asserted that the network was combinational, so `sequential<aig_network>` could be passed in but silently lost its registers: they degraded into extra PI/PO pairs. Emit registers as AIGER latches when the network type provides `num_registers`, `foreach_ri`, and `foreach_ro`. The combinational path is unchanged and still produces byte-identical output. Reset values are always written explicitly. An omitted reset field means 0 in the AIGER format, so omitting it would silently turn an uninitialized register into a zero-initialized one; an undefined reset is instead encoded by repeating the latch's own current-state literal, as the format prescribes. Latch names are emitted as `l<n>` symbol table entries, mirroring `on_latch_name`. Because the binary format encodes CIs implicitly, PIs must be variables 1..I and register outputs I+1..I+L. That invariant is now checked by a debug assertion rather than being silently assumed. Also add the missing `<cassert>` include; the header used `assert` but only compiled because its includers happened to provide it. Verified against both readers: the output round-trips through `aiger_reader` preserving register count, reset values, and names, and ABC reads it back with the expected `Init0`/`Init1`/`InitDC` counts. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz
marcelwa
force-pushed
the
upstream-seq-write-aiger
branch
from
July 28, 2026 22:15
ac6759d to
0358a0f
Compare
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
1 participant
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.
Description
write_aigerhardcoded a latch count of0and asserted the network was combinational,so a
sequential<aig_network>could be passed in but silently lost its registers — theydegrade into extra PI/PO pairs, and the assertion is a no-op in release builds.
This adds real latch support, gated on
num_registers/foreach_ri/foreach_roviaif constexpr. The combinational path is untouched and still produces byte-identicaloutput — the two pre-existing byte-exact tests pass unchanged.
Reset values
Reset values are now always written explicitly, which matters more than it first looks:
0in the AIGER format, so omitting it for anuninitialized register would silently convert it into a zero-initialized one.
repeating the latch's own current-state literal.
Verified in both directions — ABC reports the expected
Init0 = 1. Init1 = 1. InitDC = 1.for a network carrying one register of each kind, and the output round-trips through
aiger_readerpreserving register count, reset values, and names.CI ordering
The binary format encodes CIs implicitly, requiring variables
1..Ito be the primaryinputs and
I+1..I+Lthe register outputs. That invariant was previously assumedsilently; it is now documented and checked by a debug assertion.
Drive-by
Added the missing
<cassert>include. The header usesassertbut only ever compiledbecause its includers happened to provide it — a TU that includes
write_aiger.hppfirst currently fails to build.
Testing
Five new test cases in
test/io/write_aiger.cpp(26 assertions total), passing in bothdebug and
NDEBUGbuilds:0and1aiger_readerround trip preserving PI/PO/register counts and reset valuesl<n>and surviving a round tripContext: this came out of building a Python-side ABC bridge in
aigverse, where sequential designs could not be
handed to ABC at all because there was no way to write them. Offering it upstream since
it seems generally useful.
🤖 Generated with Claude Code
https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz