♻️ Unify how register initialization is represented - #701
Open
marcelwa wants to merge 2 commits into
Open
Conversation
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
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #701 +/- ##
==========================================
- Coverage 84.06% 84.06% -0.01%
==========================================
Files 190 190
Lines 29468 29478 +10
==========================================
+ Hits 24773 24781 +8
- Misses 4695 4697 +2 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
`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
marcelwa
force-pushed
the
upstream-register-init
branch
from
July 28, 2026 22:12
1b5d84f to
2b7d54a
Compare
This was referenced Jul 28, 2026
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
register_t::initcarries three different encodings of "undefined" at the same time:register_tdefault3blif_reader2(nondeterministic) /3(unspecified)aiger_reader255The
255is not a choice. The reader computesint8_t r = ... ? -1 : ...and assigns itinto a
uint8_tfield, so-1narrows to255.This corrupts output
write_blifemits the initialization verbatim, and the BLIF.latchstatement acceptsonly
0,1,2and3. So a sequential AIGER file with an undefined latch reset, readback and written as BLIF, produces:
which no BLIF consumer accepts — ABC included. This is reproducible on
mastertoday.Approach
Introduce
register_initwith the four documented values, following the BLIF.latchfield since it is the most expressive of the supported formats, and use it consistently
across
aiger_reader,blif_readerandwrite_blif. AIGER has no counterpart forunknown, so a latch without a defined reset maps todont_care.Two helpers come with it:
register_init::is_defined( value )expresses the test callers actually want — whethera reset is
0or1— so code stays correct if a format ever introduces furtherundefined states.
register_init::sanitize( value )keepswrite_bliffrom emitting a value the formatcannot represent, whatever a caller may have stored.
write_aigeris updated in #699 rather than here, since the latch-writing code it touchesis introduced by that PR.
Compatibility
The only value that changes is the one AIGER produced for a nondeterministic latch,
255→2. Comparisons of the forminit > 1orinit != 0 && init != 1areunaffected; only code testing against
255would notice, and that value was neverintentional API.
Verification
The AIGER file that previously produced
255now yields.latch li0 new_n2 2, whichABC reads back as
Total latches = 1. Init0 = 0. Init1 = 0. InitDC = 1.New test case covers explicit
0/1and self-literal resets, asserting each stays withinthe representable range and that
is_definedagrees.🤖 Generated with Claude Code
https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz