diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index a0e6caed4..654e53f30 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -58,6 +58,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) Vec_Wec_t * vFanins; // mfs data Vec_Str_t * vFixed; // mfs data Vec_Str_t * vEmpty; // mfs data + Vec_Str_t * vDenied; // mfs data Vec_Wrd_t * vTruths; // mfs data Vec_Int_t * vArray; Vec_Int_t * vStarts; @@ -81,9 +82,14 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) vFanins = Vec_WecStart( nMfsVars ); vFixed = Vec_StrStart( nMfsVars ); vEmpty = Vec_StrStart( nMfsVars ); + vDenied = Vec_StrStart( nMfsVars ); vTruths = Vec_WrdStart( nMfsVars ); vStarts = Vec_IntStart( nMfsVars ); vTruths2 = Vec_WrdAlloc( 10000 ); + // deny the PIs which are modeling blackbox outputs from being considered + // in substitutions + for (int i = 0; i < nBbOuts; i++) + Vec_StrWriteEntry( vDenied, i, (char)1 ); // set internal PIs Gia_ManCleanCopyArray( p ); Gia_ManForEachCiId( p, Id, i ) @@ -147,12 +153,16 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) // skip POs due to box inputs Counter += nBbIns; assert( Counter == nMfsVars ); + // add functions of the boxes if ( p->pAigExtra ) { - int iBbIn = 0, iBbOut = 0; assert( Gia_ManCiNum(p->pAigExtra) < 16 ); Gia_ObjComputeTruthTableStart( p->pAigExtra, Gia_ManCiNum(p->pAigExtra) ); + } + + { + int iBbIn = 0, iBbOut = 0; curCi = nRealPis; curCo = 0; for ( k = 0; k < nBoxes; k++ ) @@ -162,6 +172,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) // iterate through box outputs if ( !Tim_ManBoxIsBlack(pManTime, k) ) //&& Tim_ManBoxInputNum(pManTime, k) <= 6 ) { + assert(p->pAigExtra); // collect truth table leaves Vec_IntClear( vLeaves ); for ( i = 0; i < nBoxIns; i++ ) @@ -232,6 +243,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) Vec_IntFill( vArray, 1, iBbOut++ ); Vec_StrWriteEntry( vFixed, Counter, (char)1 ); Vec_StrWriteEntry( vEmpty, Counter, (char)1 ); + Vec_StrWriteEntry( vDenied, Counter, (char)1 ); Vec_WrdWriteEntry( vTruths, Counter, uTruths6[0] ); } for ( i = 0; i < nBoxIns; i++ ) @@ -240,7 +252,9 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) pObj = Gia_ManCo( p, curCo + i ); Counter = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) ); // connect it with the special primary output (iBbIn) - vArray = Vec_WecEntry( vFanins, nMfsVars - nBbIns + iBbIn++ ); + int poNum = nMfsVars - nBbIns + iBbIn++; + vArray = Vec_WecEntry( vFanins, poNum ); + Vec_StrWriteEntry( vFixed, poNum, (char)1 ); assert( Vec_IntSize(vArray) == 0 ); Vec_IntFill( vArray, 1, Counter ); } @@ -258,17 +272,21 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) curCi += nBoxOuts; } curCo += nRealPos; - Gia_ObjComputeTruthTableStop( p->pAigExtra ); // verify counts assert( curCi == Gia_ManCiNum(p) ); assert( curCo == Gia_ManCoNum(p) ); - assert( curCi - nRealPis == Gia_ManCoNum(p->pAigExtra) ); assert( iBbIn == nBbIns ); assert( iBbOut == nBbOuts ); } + + if (p->pAigExtra) { + Gia_ObjComputeTruthTableStop( p->pAigExtra ); + assert( curCi - nRealPis == Gia_ManCoNum(p->pAigExtra) ); + } + // finalize Vec_IntFree( vLeaves ); - return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vTruths, vStarts, vTruths2 ); + return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vDenied, vTruths, vStarts, vTruths2 ); } /**Function************************************************************* @@ -381,6 +399,15 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) continue; } Vec_IntClear( vLeaves ); + + // handle internal CIs first, before we go looking for vLeaves + if ( iGroup != -1 && Abc_LitIsCompl(iGroup) ) + { + //Dau_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) ); + iLitNew = Gia_ManAppendCi( pNew ); + goto done; + } + Vec_IntForEachEntry( vArray, Fanin, k ) { iLitNew = Vec_IntEntry( vMfs2Gia, Fanin ); assert( iLitNew >= 0 ); @@ -405,17 +432,13 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes ) else iLitNew = Gia_ManFromIfLogicCreateLut( pNew, pTruth, vLeaves, vCover, vMapping, vMapping2 ); } - else if ( Abc_LitIsCompl(iGroup) ) // internal CI - { - //Dau_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) ); - iLitNew = Gia_ManAppendCi( pNew ); - } else // internal CO { assert( pTruth[0] == uTruthVar || pTruth[0] == ~uTruthVar ); iLitNew = Gia_ManAppendCo( pNew, Abc_LitNotCond(Vec_IntEntry(vLeaves, 0), pTruth[0] == ~uTruthVar) ); //printf("Group = %d. po = %d\n", iGroup>>1, iMfsId ); } +done: Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew ); } Vec_IntFree( vCover ); @@ -498,11 +521,6 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ) int nFaninMax, nNodes; assert( Gia_ManRegNum(p) == 0 ); assert( p->vMapping != NULL ); - if ( p->pManTime != NULL && p->pAigExtra == NULL ) - { - Abc_Print( 1, "Timing manager is given but there is no GIA of boxes.\n" ); - return NULL; - } if ( p->pManTime != NULL && p->pAigExtra != NULL && Gia_ManCiNum(p->pAigExtra) > 15 ) { Abc_Print( 1, "Currently \"&mfs\" cannot process the network containing white-boxes with more than 15 inputs.\n" ); @@ -517,6 +535,8 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ) } // collect information pNtk = Gia_ManExtractMfs( p ); + if (pPars->fTestReimport) + goto reimport; // perform optimization nNodes = Sfm_NtkPerform( pNtk, pPars ); if ( nNodes == 0 ) @@ -529,6 +549,7 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ) } else { + reimport: pNew = Gia_ManInsertMfs( p, pNtk, pPars->fAllBoxes ); if( pPars->fVerbose ) Abc_Print( 1, "The network has %d nodes changed by \"&mfs\".\n", nNodes ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index cf5b341f3..f0fa728c2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -49096,7 +49096,7 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nDepthMax = 100; pPars->nWinSizeMax = 2000; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCNdaeblvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCNdaeblvwhr" ) ) != EOF ) { switch ( c ) { @@ -49192,6 +49192,9 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'l': pPars->fUseDcs ^= 1; break; + case 'r': + pPars->fTestReimport ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -49261,6 +49264,7 @@ usage: Abc_Print( -2, "\t-l : toggle deriving don't-cares [default = %s]\n", pPars->fUseDcs? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-r : toggle testing re-importing the network unchanged [default = %s]\n", pPars->fTestReimport? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c index 0533d189f..69c04c2c3 100644 --- a/src/base/abci/abcMfs.c +++ b/src/base/abci/abcMfs.c @@ -216,7 +216,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed ) // for ( i = Abc_NtkCiNum(pNtk); i + Abc_NtkCoNum(pNtk) < Abc_NtkObjNum(pNtk); i++ ) // if ( rand() % 10 == 0 ) // Vec_StrWriteEntry( vFixed, i, (char)1 ); - return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths, vStarts, vTruths2 ); + return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, NULL, vTruths, vStarts, vTruths2 ); } Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot ) { @@ -285,7 +285,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot ) Abc_NtkForEachNode( pNtk, pObj, i ) if ( i >= iPivot ) Vec_StrWriteEntry( vFixed, pObj->iTemp, (char)1 ); - return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths, vStarts, vTruths2 ); + return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, NULL, vTruths, vStarts, vTruths2 ); } /**Function************************************************************* diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index f9c95c83e..5fd564fce 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -73,6 +73,7 @@ struct Sfm_Par_t_ int fDelayVerbose; // enable delay stats int fVerbose; // enable basic stats int fVeryVerbose; // enable detailed stats + int fTestReimport; // enable testing of re-import }; //////////////////////////////////////////////////////////////////////// @@ -88,7 +89,7 @@ struct Sfm_Par_t_ extern void Sfm_ParSetDefault( Sfm_Par_t * pPars ); extern int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ); /*=== sfmNtk.c ==========================================================*/ -extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ); +extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Str_t * vDenied, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ); extern void Sfm_NtkFree( Sfm_Ntk_t * p ); extern Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i ); extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i ); diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c index f363e1cb0..87c11e615 100644 --- a/src/opt/sfm/sfmCore.c +++ b/src/opt/sfm/sfmCore.c @@ -58,6 +58,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars ) pPars->fAllBoxes = 0; // enable preserving all boxes pPars->fVerbose = 0; // enable basic stats pPars->fVeryVerbose = 0; // enable detailed stats + pPars->fTestReimport = 0; // enable testing of re-import } /**Function************************************************************* @@ -114,7 +115,7 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly ) int fSkipUpdate = 0; int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556; int i, iFanin, iVar = -1; - int iFaninRem = -1, iFaninSkip = -1; + int iFaninRem = -1; int nFanins = Sfm_ObjFaninNum(p, iNode); word uTruth, uSign, uMask; abctime clk; @@ -137,9 +138,6 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly ) else iFaninRem = iFanin; assert( iFaninRem != -1 ); - // find fanin to skip - if ( Sfm_ObjIsFixed(p, iFaninRem) && Sfm_ObjFaninNum(p, iFaninRem) == 1 ) - iFaninSkip = Sfm_ObjFanin(p, iFaninRem, 0); clk = Abc_Clock(); uTruth = Sfm_ComputeInterpolant( p ); p->timeSat += Abc_Clock() - clk; @@ -175,11 +173,10 @@ p->timeSat += Abc_Clock() - clk; // find the next divisor to try uMask = (~(word)0) >> (64 - p->nCexes); Vec_WrdForEachEntry( p->vDivCexes, uSign, iVar ) - if ( uSign == uMask && Vec_IntEntry(p->vDivs, iVar) != iFaninSkip ) + if ( uSign == uMask && !Sfm_ObjIsDenied(p, Vec_IntEntry(p->vDivs, iVar)) ) break; if ( iVar == Vec_IntSize(p->vDivs) ) return 0; - assert( Vec_IntEntry(p->vDivs, iVar) != iFaninSkip ); // try replacing the critical fanin Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, Vec_IntEntry(p->vDivs, iVar)) ); clk = Abc_Clock(); @@ -288,6 +285,10 @@ p->timeSat += Abc_Clock() - clk; int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode ) { int i, iFanin; + + if (Sfm_NodeReadFixed(p, iNode)) + return 0; + p->nNodesTried++; // prepare SAT solver if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) ) diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index ae4bb60a8..6f86a5c6a 100644 --- a/src/opt/sfm/sfmInt.h +++ b/src/opt/sfm/sfmInt.h @@ -81,6 +81,7 @@ struct Sfm_Ntk_t_ // user data Vec_Str_t * vFixed; // persistent objects Vec_Str_t * vEmpty; // transparent objects + Vec_Str_t * vDenied; // denied objects Vec_Wrd_t * vTruths; // truth tables Vec_Wec_t vFanins; // fanins Vec_Int_t * vStarts; // offsets @@ -157,6 +158,7 @@ static inline int Sfm_ObjIsPi( Sfm_Ntk_t * p, int i ) { return static inline int Sfm_ObjIsPo( Sfm_Ntk_t * p, int i ) { return i + p->nPos >= p->nObjs; } static inline int Sfm_ObjIsNode( Sfm_Ntk_t * p, int i ) { return i >= p->nPis && i + p->nPos < p->nObjs; } static inline int Sfm_ObjIsFixed( Sfm_Ntk_t * p, int i ) { return Vec_StrEntry(p->vFixed, i); } +static inline int Sfm_ObjIsDenied( Sfm_Ntk_t * p, int i ) { return p->vDenied && Vec_StrEntry(p->vDenied, i); } static inline int Sfm_ObjAddsLevelArray( Vec_Str_t * p, int i ) { return p == NULL || Vec_StrEntry(p, i) == 0; } static inline int Sfm_ObjAddsLevel( Sfm_Ntk_t * p, int i ) { return Sfm_ObjAddsLevelArray(p->vEmpty, i); } diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index 70afd91aa..9f32cbb58 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/src/opt/sfm/sfmNtk.c @@ -58,7 +58,7 @@ void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * assert( Fanin + nPos < Vec_WecSize(vFanins) ); // POs have one fanout if ( i + nPos >= Vec_WecSize(vFanins) ) - assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 ); + assert( Vec_IntSize(vArray) == 1 ); } } @@ -164,7 +164,7 @@ void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * v SeeAlso [] ***********************************************************************/ -Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ) +Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Str_t * vDenied, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ) { Sfm_Ntk_t * p; int i; Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed ); @@ -177,6 +177,7 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t p->vFixed = vFixed; p->vEmpty = vEmpty; p->vTruths = vTruths; + p->vDenied = vDenied; p->vFanins = *vFanins; p->vStarts = vStarts; p->vTruths2 = vTruths2; @@ -221,6 +222,7 @@ void Sfm_NtkFree( Sfm_Ntk_t * p ) // user data Vec_StrFree( p->vFixed ); Vec_StrFreeP( &p->vEmpty ); + Vec_StrFreeP( &p->vDenied ); Vec_WrdFree( p->vTruths ); Vec_WecErase( &p->vFanins ); Vec_IntFree( p->vStarts ); diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index 53f9a71ef..2e1681991 100644 --- a/src/opt/sfm/sfmWin.c +++ b/src/opt/sfm/sfmWin.c @@ -142,18 +142,19 @@ void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * v return; if ( Vec_IntEntry(vGroupMap, iNode) >= 0 ) { - int k, iGroup = Abc_Lit2Var( Vec_IntEntry(vGroupMap, iNode) ); - Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup ); - Vec_IntForEachEntry( vGroup, iNode, i ) - assert( Sfm_ObjIsNode(p, iNode) ); - Vec_IntForEachEntry( vGroup, iNode, i ) - Sfm_ObjSetTravIdCurrent( p, iNode ); - Vec_IntForEachEntry( vGroup, iNode, i ) - Sfm_ObjForEachFanin( p, iNode, iFanin, k ) - Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft ); - Vec_IntForEachEntry( vGroup, iNode, i ) - Vec_IntPush( vNodes, iNode ); - Vec_IntPush( vBoxesLeft, iGroup ); + int iGroup = Abc_Lit2Var(Vec_IntEntry(vGroupMap, iNode)); + Vec_Int_t * vGroup = Vec_WecEntry(vGroups, iGroup); + assert(Abc_LitIsCompl(Vec_IntEntry(vGroupMap, iNode))); + Vec_IntPush(vBoxesLeft, iGroup); + Vec_IntForEachEntry(vGroup, iNode, i) + { + // ignore inputs + if ( !Abc_LitIsCompl(Vec_IntEntry(vGroupMap, iNode))) + continue; + assert(Sfm_ObjIsNode(p, iNode)); + Sfm_ObjSetTravIdCurrent(p, iNode); + Vec_IntPush(vNodes, iNode); + } } else { @@ -170,14 +171,33 @@ Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMa Vec_IntClear( vBoxesLeft ); vNodes = Vec_IntAlloc( p->nObjs ); Sfm_NtkIncrementTravId( p ); - if ( fAllBoxes ) - { - Vec_Int_t * vGroup; - Vec_WecForEachLevel( vGroups, vGroup, i ) - Sfm_NtkDfs_rec( p, Vec_IntEntry(vGroup, 0), vNodes, vGroups, vGroupMap, vBoxesLeft ); + + assert(!fAllBoxes); // TODO + + Sfm_NtkForEachPo( p, i ) { + int iFanin = Sfm_ObjFanin(p, i, 0); + // detect fake PO modeling blackbox input + if (Vec_IntEntry(vGroupMap, iFanin) >= 0 && !Abc_LitIsCompl(Vec_IntEntry(vGroupMap, iFanin))) + continue; + Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft ); } - Sfm_NtkForEachPo( p, i ) - Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft ); + + for (i = 0; i < Vec_IntSize( vBoxesLeft ); i++) + { + int k, j, iNode, iFanin; + int iGroup = Vec_IntEntry( vBoxesLeft, i ); + Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup ); + Vec_IntForEachEntry( vGroup, iNode, k ) + { + // ignore outputs + if ( Abc_LitIsCompl( Vec_IntEntry(vGroupMap, iNode)) ) + continue; + Sfm_ObjForEachFanin( p, iNode, iFanin, j ) + Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft ); + Vec_IntPush( vNodes, iNode ); + } + } + return vNodes; }