gia: convert the AIG with an explicit stack rather than recursion - #13
Merged
Merged
Conversation
Gia_ManFromAig_rec() descends through an AND node's fanins with one call frame per level, so what it can convert is bounded by the process stack rather than by the manager. A chain of AND nodes -- which is the shape a bit-blasted arithmetic query takes once it has been unrolled -- overflows an 8MB stack somewhere between 170,000 and 180,000 levels. Drive the same walk from an explicit Vec_Ptr_t. Each node goes onto the stack twice: the regular pointer means "visit", and the complemented one, pushed first and so popped last, means "build", by which point both fanins carry a literal. Fanin 1 is pushed before fanin 0, so fanin 0's cone is built first, and a node's equivalence successor is pushed only once the node itself has been appended. Gia_ManAppendAnd() is therefore called in the order the recursion called it in, and the graph that comes out is the same one with the same ids. Appending the node before its successor is the part that matters. Gia_ManFromAig() hands pNexts to Gia_ManDeriveReprs(), which takes the lowest id in a chain as its representative, so building the successor first would swap representative and member. It also bounds the walk: the successor is reached with the node already built, so an equivalence leading back to it stops the way the recursion's iData test did. The link itself cannot be written where the recursion writes it, since the successor is appended after the node that names it. The nodes carrying one are collected instead and linked once the walk is done; nothing reads pNexts before Gia_ManDeriveReprs() runs over it. A 1,000,000-level chain now converts in the same process that failed at 180,000. On a four-input AIG with an equivalence class set by hand, the recursion and the walk produce the same ids, the same pNexts and the same pReprs; and dch, &choice, and dc2 followed by dch -f over a 10-bit multiplier, a 24-bit ripple-carry adder and a 12-input sorter write byte-identical AIGER. Assisted-by: Claude Opus 5 (1M context), via Claude Code
aytey
added a commit
to stp/stp
that referenced
this pull request
Sep 11, 2026
Moves ABC_GIT_TAG from bdacd8988 to b6e26a0fe -- the same revision plus one commit, the explicit-stack rewrite of Gia_ManFromAig_rec (stp/abc#13). Held by the tag stp-at-953930643-pr1109, alongside stp-at-953930643-pr1051 which holds the revision pinned until now. Gia_ManFromAig_rec() descended through an AND node's fanins with one call frame per level, so what could be converted was bounded by the process stack rather than by the AIG: a chain overflows an 8MB stack somewhere between 170,000 and 180,000 levels. It is driven from an explicit stack now, in the order the recursion used, so the graph that comes out is unchanged -- ids, pNexts and pReprs alike. STP's tests pass against it, and dch, &choice and dc2 followed by dch -f write byte-identical AIGER on the circuits checked. This started as a patch applied to the cloned source with a PATCH_COMMAND, which is the wrong place for it twice over. git apply ran only on the ExternalProject path, so a build configured with -DABC_DIR against a clone of the fork -- which is how the code guide says to work on ABC -- compiled an ABC that differed from the one CI compiled. And it did not apply on Windows at all: actions/checkout takes STP with Git for Windows, whose autocrlf leaves the patch file CRLF, while the MSYS2 git that clones ABC leaves that tree LF, and git apply then rejects the hunk. The MSVC leg passed only because both sides are CRLF there. The comment above the pin and the ABC entry in the code guide both said the pin follows the fork's `stp` branch. It does not, and has not since PR #892: `stp` sits on a newer upstream, and the pin follows the line carrying the same changes on the upstream revision taken in 2024. Both now say so, since moving the pin to `stp` would bump the upstream base with it. Assisted-by: Claude Opus 5 (1M context), via Claude Code Signed-off-by: Andrew Teylu <andrew@tey.lu>
aytey
added a commit
to stp/stp
that referenced
this pull request
Sep 11, 2026
Moves ABC_GIT_TAG from bdacd8988 to b6e26a0fe -- the same revision plus one commit, the explicit-stack rewrite of Gia_ManFromAig_rec (stp/abc#13). Held by the tag stp-at-953930643-pr1109, alongside stp-at-953930643-pr1051 which holds the revision pinned until now. Gia_ManFromAig_rec() descended through an AND node's fanins with one call frame per level, so what could be converted was bounded by the process stack rather than by the AIG: a chain overflows an 8MB stack somewhere between 170,000 and 180,000 levels. It is driven from an explicit stack now, in the order the recursion used, so the graph that comes out is unchanged -- ids, pNexts and pReprs alike. STP's tests pass against it, and dch, &choice and dc2 followed by dch -f write byte-identical AIGER on the circuits checked. This started as a patch applied to the cloned source with a PATCH_COMMAND, which is the wrong place for it twice over. git apply ran only on the ExternalProject path, so a build configured with -DABC_DIR against a clone of the fork -- which is how the code guide says to work on ABC -- compiled an ABC that differed from the one CI compiled. And it did not apply on Windows at all: actions/checkout takes STP with Git for Windows, whose autocrlf leaves the patch file CRLF, while the MSYS2 git that clones ABC leaves that tree LF, and git apply then rejects the hunk. The MSVC leg passed only because both sides are CRLF there. The comment above the pin and the ABC entry in the code guide both said the pin follows the fork's `stp` branch. It does not, and has not since PR #892: `stp` sits on a newer upstream, and the pin follows the line carrying the same changes on the upstream revision taken in 2024. Both now say so, since moving the pin to `stp` would bump the upstream base with it. Assisted-by: Claude Opus 5 (1M context), via Claude Code Signed-off-by: Andrew Teylu <andrew@tey.lu>
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.
Gia_ManFromAig_rec()descends through an AND node's fanins with one call frame per level, so what it can convert is bounded by the process stack rather than by the manager. A chain of AND nodes — the shape a bit-blasted arithmetic query takes once unrolled — overflows an 8MB stack somewhere between 170,000 and 180,000 levels. STP reaches that.The same walk is driven from an explicit
Vec_Ptr_there. Each node goes onto the stack twice: the regular pointer means "visit", the complemented one means "build". Fanin 1 is pushed before fanin 0, and a node's equivalence successor is pushed only after the node itself has been appended, soGia_ManAppendAnd()is called in exactly the order the recursion called it in.That last part is what makes the choice path safe.
Gia_ManFromAig()handspNextstoGia_ManDeriveReprs(), which takes the lowest id in a chain as its representative, so appending the successor first would swap representative and member. It also bounds the walk, since an equivalence leading back to the node meets it already built.Verified: a 1,000,000-level chain converts in the same process that failed at 180,000; on a four-input AIG with an equivalence class set by hand the recursion and the walk produce the same ids,
pNextsandpReprs; anddch,&choiceanddc2; dch -fover a 10-bit multiplier, a 24-bit ripple-carry adder and a 12-input sorter write byte-identical AIGER. STP's 178 tests pass linked against it.The same commit is on
pin-two-commitsas b6e26a0, taggedstp-at-953930643-pr1109, which is what stp/stp#1109 pins.