From dca23449bdc1c2aaed32284f8d2d16c5cfdca387 Mon Sep 17 00:00:00 2001 From: Andrew Teylu Date: Fri, 11 Sep 2026 16:21:04 +0100 Subject: [PATCH] gia: convert the AIG with an explicit stack rather than recursion 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 --- src/aig/gia/giaAig.c | 58 ++++++++++++++++++++++++++++++++++---------- 1 file changed, 45 insertions(+), 13 deletions(-) diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 07bab5fec..6c33b8502 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -54,24 +54,56 @@ static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * SeeAlso [] ***********************************************************************/ -void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) +void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pRoot ) { - Aig_Obj_t * pNext; - if ( pObj->iData ) + // Each node is pushed twice: regular means "visit", and complemented -- + // pushed first, so reached last -- means "build", by which point both + // fanins are done. The equivalence links are collected rather than + // written, since a node names a successor that is built after it. + Vec_Ptr_t * vStack, * vLinks = NULL; + Aig_Obj_t * pObj, * pNext; + int i; + if ( pRoot->iData ) return; - assert( Aig_ObjIsNode(pObj) ); - Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) ); - Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin1(pObj) ); - pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) ); - if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) ) + vStack = Vec_PtrAlloc( 100 ); + if ( p->pEquivs ) + vLinks = Vec_PtrAlloc( 100 ); + Vec_PtrPush( vStack, pRoot ); + while ( Vec_PtrSize(vStack) ) + { + pObj = (Aig_Obj_t *)Vec_PtrPop( vStack ); + if ( Aig_IsComplement(pObj) ) + { + pObj = Aig_Regular(pObj); + // an equivalence successor can build it before this is reached + if ( pObj->iData ) + continue; + pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) ); + if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) ) + { + Vec_PtrPush( vLinks, pObj ); + if ( !pNext->iData ) + Vec_PtrPush( vStack, pNext ); + } + continue; + } + if ( pObj->iData ) + continue; + assert( Aig_ObjIsNode(pObj) ); + Vec_PtrPush( vStack, Aig_Not(pObj) ); + if ( !Aig_ObjFanin1(pObj)->iData ) + Vec_PtrPush( vStack, Aig_ObjFanin1(pObj) ); + if ( !Aig_ObjFanin0(pObj)->iData ) + Vec_PtrPush( vStack, Aig_ObjFanin0(pObj) ); + } + if ( vLinks ) { - int iObjNew, iNextNew; - Gia_ManFromAig_rec( pNew, p, pNext ); - iObjNew = Abc_Lit2Var(pObj->iData); - iNextNew = Abc_Lit2Var(pNext->iData); if ( pNew->pNexts ) - pNew->pNexts[iObjNew] = iNextNew; + Vec_PtrForEachEntry( Aig_Obj_t *, vLinks, pObj, i ) + pNew->pNexts[Abc_Lit2Var(pObj->iData)] = Abc_Lit2Var(Aig_ObjEquiv(p, pObj)->iData); + Vec_PtrFree( vLinks ); } + Vec_PtrFree( vStack ); } Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ) {