diff options
Diffstat (limited to 'src/aig/gia/giaSplit.c')
| -rw-r--r-- | src/aig/gia/giaSplit.c | 332 |
1 files changed, 250 insertions, 82 deletions
diff --git a/src/aig/gia/giaSplit.c b/src/aig/gia/giaSplit.c index c2e2d448..8bb5d3c0 100644 --- a/src/aig/gia/giaSplit.c +++ b/src/aig/gia/giaSplit.c @@ -35,14 +35,16 @@ struct Spl_Man_t_ Gia_Man_t * pGia; // user AIG with nodes marked int iObj; // object ID int Limit; // limit on AIG nodes - int Count; // count of AIG nodes + int fReverse; // enable reverse search // intermediate Vec_Bit_t * vMarksCIO; // CI/CO marks Vec_Bit_t * vMarksIn; // input marks Vec_Bit_t * vMarksNo; // node marks - Vec_Int_t * vNodes; // nodes used in the window + Vec_Bit_t * vMarksAnd; // AND node marks Vec_Int_t * vRoots; // nodes pointing to Nodes + Vec_Int_t * vNodes; // nodes used in the window Vec_Int_t * vLeaves; // nodes pointed by Nodes + Vec_Int_t * vAnds; // AND nodes used in the window // temporary Vec_Int_t * vFanouts; // fanouts of the node Vec_Int_t * vCands; // candidate nodes @@ -55,7 +57,48 @@ struct Spl_Man_t_ /**Function************************************************************* - Synopsis [] + Synopsis [Transforming to the internal LUT representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Spl_ManToWecMapping( Gia_Man_t * p ) +{ + Vec_Wec_t * vMapping = Vec_WecStart( Gia_ManObjNum(p) ); + int Obj, Fanin, k; + assert( Gia_ManHasMapping(p) ); + Gia_ManForEachLut( p, Obj ) + Gia_LutForEachFanin( p, Obj, Fanin, k ) + Vec_WecPush( vMapping, Obj, Fanin ); + return vMapping; +} +Vec_Int_t * Spl_ManFromWecMapping( Gia_Man_t * p, Vec_Wec_t * vMap ) +{ + Vec_Int_t * vMapping, * vVec; int i, k, Obj; + assert( Gia_ManHasMapping2(p) ); + vMapping = Vec_IntAlloc( Gia_ManObjNum(p) + Vec_WecSizeSize(vMap) + 2*Vec_WecSizeUsed(vMap) ); + Vec_IntFill( vMapping, Gia_ManObjNum(p), 0 ); + Vec_WecForEachLevel( vMap, vVec, i ) + if ( Vec_IntSize(vVec) > 0 ) + { + Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) ); + Vec_IntPush( vMapping, Vec_IntSize(vVec) ); + Vec_IntForEachEntry( vVec, Obj, k ) + Vec_IntPush( vMapping, Obj ); + Vec_IntPush( vMapping, i ); + } + assert( Vec_IntSize(vMapping) < 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) ); + return vMapping; +} + + +/**Function************************************************************* + + Synopsis [Creating manager.] Description [] @@ -64,45 +107,62 @@ struct Spl_Man_t_ SeeAlso [] ***********************************************************************/ -Spl_Man_t * Spl_ManAlloc( Gia_Man_t * pGia, int Limit ) +Spl_Man_t * Spl_ManAlloc( Gia_Man_t * pGia, int Limit, int fReverse ) { int i, iObj; Spl_Man_t * p = ABC_CALLOC( Spl_Man_t, 1 ); - assert( Gia_ManHasMapping(pGia) ); p->pGia = pGia; p->Limit = Limit; + p->fReverse = fReverse; // intermediate p->vMarksCIO = Vec_BitStart( Gia_ManObjNum(pGia) ); p->vMarksIn = Vec_BitStart( Gia_ManObjNum(pGia) ); p->vMarksNo = Vec_BitStart( Gia_ManObjNum(pGia) ); + p->vMarksAnd = Vec_BitStart( Gia_ManObjNum(pGia) ); p->vRoots = Vec_IntAlloc( 100 ); p->vNodes = Vec_IntAlloc( 100 ); p->vLeaves = Vec_IntAlloc( 100 ); + p->vAnds = Vec_IntAlloc( 100 ); // temporary p->vFanouts = Vec_IntAlloc( 100 ); p->vCands = Vec_IntAlloc( 100 ); p->vInputs = Vec_IntAlloc( 100 ); // mark CIs/COs + Vec_BitWriteEntry( p->vMarksCIO, 0, 1 ); Gia_ManForEachCiId( pGia, iObj, i ) Vec_BitWriteEntry( p->vMarksCIO, iObj, 1 ); Gia_ManForEachCoId( pGia, iObj, i ) Vec_BitWriteEntry( p->vMarksCIO, iObj, 1 ); - // prepare AIG - Gia_ManStaticFanoutStart( pGia ); - Gia_ManSetLutRefs( pGia ); + // mapping + ABC_FREE( pGia->pRefs ); Gia_ManCreateRefs( pGia ); + Gia_ManSetLutRefs( pGia ); + assert( Gia_ManHasMapping(pGia) ); + assert( !Gia_ManHasMapping2(pGia) ); + pGia->vMapping2 = Spl_ManToWecMapping( pGia ); + Vec_IntFreeP( &pGia->vMapping ); + // fanout + Gia_ManStaticFanoutStart( pGia ); return p; } void Spl_ManStop( Spl_Man_t * p ) { + // fanout Gia_ManStaticFanoutStop( p->pGia ); + // mapping + assert( !Gia_ManHasMapping(p->pGia) ); + assert( Gia_ManHasMapping2(p->pGia) ); + p->pGia->vMapping = Spl_ManFromWecMapping( p->pGia, p->pGia->vMapping2 ); + Vec_WecFreeP( &p->pGia->vMapping2 ); // intermediate Vec_BitFree( p->vMarksCIO ); Vec_BitFree( p->vMarksIn ); Vec_BitFree( p->vMarksNo ); + Vec_BitFree( p->vMarksAnd ); Vec_IntFree( p->vRoots ); Vec_IntFree( p->vNodes ); Vec_IntFree( p->vLeaves ); + Vec_IntFree( p->vAnds ); // temporary Vec_IntFree( p->vFanouts ); Vec_IntFree( p->vCands ); @@ -123,31 +183,55 @@ void Spl_ManStop( Spl_Man_t * p ) ***********************************************************************/ void Spl_ManWinFindLeavesRoots( Spl_Man_t * p ) { + Vec_Int_t * vVec; int iObj, iFan, i, k; // collect leaves +/* Vec_IntClear( p->vLeaves ); - Vec_IntForEachEntry( p->vNodes, iObj, i ) + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) { assert( Vec_BitEntry(p->vMarksNo, iObj) ); - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) + Vec_IntForEachEntry( vVec, iFan, k ) if ( !Vec_BitEntry(p->vMarksNo, iFan) ) { Vec_BitWriteEntry(p->vMarksNo, iFan, 1); Vec_IntPush( p->vLeaves, iFan ); } } - Vec_IntForEachEntry( p->vLeaves, iObj, i ) - Vec_BitWriteEntry(p->vMarksNo, iObj, 0); + Vec_IntForEachEntry( p->vLeaves, iFan, i ) + Vec_BitWriteEntry(p->vMarksNo, iFan, 0); +*/ + Vec_IntClear( p->vLeaves ); + Vec_IntForEachEntry( p->vAnds, iObj, i ) + { + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj ); + assert( Vec_BitEntry(p->vMarksAnd, iObj) ); + iFan = Gia_ObjFaninId0( pObj, iObj ); + if ( !Vec_BitEntry(p->vMarksAnd, iFan) ) + { + Vec_BitWriteEntry(p->vMarksAnd, iFan, 1); + Vec_IntPush( p->vLeaves, iFan ); + } + iFan = Gia_ObjFaninId1( pObj, iObj ); + if ( !Vec_BitEntry(p->vMarksAnd, iFan) ) + { + Vec_BitWriteEntry(p->vMarksAnd, iFan, 1); + Vec_IntPush( p->vLeaves, iFan ); + } + } + Vec_IntForEachEntry( p->vLeaves, iFan, i ) + Vec_BitWriteEntry(p->vMarksAnd, iFan, 0); + // collect roots Vec_IntClear( p->vRoots ); - Vec_IntForEachEntry( p->vNodes, iObj, i ) - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) Gia_ObjLutRefDecId( p->pGia, iFan ); - Vec_IntForEachEntry( p->vNodes, iObj, i ) + Vec_IntForEachEntry( p->vAnds, iObj, i ) if ( Gia_ObjLutRefNumId(p->pGia, iObj) ) Vec_IntPush( p->vRoots, iObj ); - Vec_IntForEachEntry( p->vNodes, iObj, i ) - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) Gia_ObjLutRefIncId( p->pGia, iFan ); } @@ -170,7 +254,7 @@ void Spl_ManLutFanouts_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_B int iFanout, i; if ( Vec_BitEntry(vMarksNo, iObj) || Vec_BitEntry(vMarksCIO, iObj) ) return; - if ( Gia_ObjIsLut(p, iObj) ) + if ( Gia_ObjIsLut2(p, iObj) ) { Vec_BitWriteEntry( vMarksCIO, iObj, 1 ); Vec_IntPush( vFanouts, iObj ); @@ -182,7 +266,7 @@ void Spl_ManLutFanouts_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_B int Spl_ManLutFanouts( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_Bit_t * vMarksNo, Vec_Bit_t * vMarksCIO ) { int i, iFanout; - assert( Gia_ObjIsLut(p, iObj) ); + assert( Gia_ObjIsLut2(p, iObj) ); Vec_IntClear( vFanouts ); Gia_ObjForEachFanoutStaticId( p, iObj, iFanout, i ) Spl_ManLutFanouts_rec( p, iFanout, vFanouts, vMarksNo, vMarksCIO ); @@ -195,30 +279,7 @@ int Spl_ManLutFanouts( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_Bit_t /**Function************************************************************* - Synopsis [Compute MFFC size of one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj ) -{ - int Res, iFan, i; - assert( Gia_ObjIsLut(p, iObj) ); - Gia_LutForEachFanin( p, iObj, iFan, i ) - Gia_ObjRefIncId( p, iFan ); - Res = Gia_NodeMffcSize( p, Gia_ManObj(p, iObj) ); - Gia_LutForEachFanin( p, iObj, iFan, i ) - Gia_ObjRefDecId( p, iFan ); - return Res; -} - -/**Function************************************************************* - - Synopsis [Returns the number of fanins not beloning to the set.] + Synopsis [Returns the number of fanins beloning to the set.] Description [] @@ -229,8 +290,9 @@ int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj ) ***********************************************************************/ int Spl_ManCountMarkedFanins( Gia_Man_t * p, int iObj, Vec_Bit_t * vMarks ) { - int k, iFan, Count = 0; - Gia_LutForEachFanin( p, iObj, iFan, k ) + int i, iFan, Count = 0; + Vec_Int_t * vFanins = Gia_ObjLutFanins2(p, iObj); + Vec_IntForEachEntry( vFanins, iFan, i ) if ( Vec_BitEntry(vMarks, iFan) ) Count++; return Count; @@ -249,27 +311,46 @@ int Spl_ManCountMarkedFanins( Gia_Man_t * p, int iObj, Vec_Bit_t * vMarks ) ***********************************************************************/ int Spl_ManFindOne( Spl_Man_t * p ) { + Vec_Int_t * vVec; int nFanouts, iObj, iFan, i, k; int Res = 0, InCount, InCountMax = -1; Vec_IntClear( p->vCands ); Vec_IntClear( p->vInputs ); // deref - Vec_IntForEachEntry( p->vNodes, iObj, i ) - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) Gia_ObjLutRefDecId( p->pGia, iFan ); // consider LUT inputs - get one that has no refs - Vec_IntForEachEntry( p->vNodes, iObj, i ) - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) - if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) ) - { - if ( !Gia_ObjLutRefNumId(p->pGia, iFan) ) + if ( p->fReverse ) + { + Gia_ManForEachLut2VecReverse( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) + if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) ) { - Res = iFan; - goto finish; + if ( !Gia_ObjLutRefNumId(p->pGia, iFan) ) + { + Res = iFan; + goto finish; + } + Vec_IntPush( p->vCands, iFan ); + Vec_IntPush( p->vInputs, iFan ); } - Vec_IntPush( p->vCands, iFan ); - Vec_IntPush( p->vInputs, iFan ); - } + } + else + { + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) + if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) ) + { + if ( !Gia_ObjLutRefNumId(p->pGia, iFan) ) + { + Res = iFan; + goto finish; + } + Vec_IntPush( p->vCands, iFan ); + Vec_IntPush( p->vInputs, iFan ); + } + } // all inputs have refs - collect external nodes Vec_IntForEachEntry( p->vNodes, iObj, i ) @@ -277,7 +358,7 @@ int Spl_ManFindOne( Spl_Man_t * p ) if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 0 ) continue; assert( Gia_ObjLutRefNumId(p->pGia, iObj) > 0 ); - if ( Gia_ObjLutRefNumId(p->pGia, iObj) >= 5 ) + if ( Gia_ObjLutRefNumId(p->pGia, iObj) >= 5 ) // skip nodes with high fanout! continue; nFanouts = Spl_ManLutFanouts( p->pGia, iObj, p->vFanouts, p->vMarksNo, p->vMarksCIO ); if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 1 && nFanouts == 1 ) @@ -310,9 +391,9 @@ int Spl_ManFindOne( Spl_Man_t * p ) Res = Vec_IntEntry( p->vCands, 0 ); finish: - // deref - Vec_IntForEachEntry( p->vNodes, iObj, i ) - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) + // ref + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) Gia_ObjLutRefIncId( p->pGia, iFan ); return Res; } @@ -321,7 +402,7 @@ finish: /**Function************************************************************* - Synopsis [] + Synopsis [Computing window for one pivot node.] Description [] @@ -330,50 +411,137 @@ finish: SeeAlso [] ***********************************************************************/ -void Spl_ManComputeOne( Spl_Man_t * p, int iPivot ) +int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj, Vec_Int_t * vTemp, Vec_Bit_t * vMarksAnd ) +{ + int iTemp, i, k = 0; + assert( Gia_ObjIsLut2(p, iObj) ); +//Vec_IntPrint( Gia_ObjLutFanins2(p, iObj) ); + Gia_ManIncrementTravId( p ); + Gia_ManCollectAnds( p, &iObj, 1, vTemp, Gia_ObjLutFanins2(p, iObj) ); + Vec_IntForEachEntry( vTemp, iTemp, i ) + if ( !Vec_BitEntry(vMarksAnd, iTemp) ) + Vec_IntWriteEntry( vTemp, k++, iTemp ); + Vec_IntShrink( vTemp, k ); + return k; +} +void Spl_ManAddNode( Spl_Man_t * p, int iPivot, Vec_Int_t * vCands ) +{ + int i, iObj; + Vec_IntPush( p->vNodes, iPivot ); + Vec_BitWriteEntry( p->vMarksNo, iPivot, 1 ); + Vec_IntAppend( p->vAnds, vCands ); + Vec_IntForEachEntry( vCands, iObj, i ) + Vec_BitWriteEntry( p->vMarksAnd, iObj, 1 ); +} +int Spl_ManComputeOne( Spl_Man_t * p, int iPivot ) { int CountAdd, iObj, i; - assert( Gia_ObjIsLut(p->pGia, iPivot) ); + assert( Gia_ObjIsLut2(p->pGia, iPivot) ); +//Gia_ManPrintCone2( p->pGia, Gia_ManObj(p->pGia, iPivot) ); // assume it was previously filled in Vec_IntForEachEntry( p->vNodes, iObj, i ) Vec_BitWriteEntry( p->vMarksNo, iObj, 0 ); + Vec_IntForEachEntry( p->vAnds, iObj, i ) + Vec_BitWriteEntry( p->vMarksAnd, iObj, 0 ); // double check that it is empty - //Gia_ManForEachLut( p->pGia, iObj ) + //Gia_ManForEachLut2( p->pGia, iObj ) // assert( !Vec_BitEntry(p->vMarksNo, iObj) ); + //Gia_ManForEachLut2( p->pGia, iObj ) + // assert( !Vec_BitEntry(p->vMarksAnd, iObj) ); + // clean arrays + Vec_IntClear( p->vNodes ); + Vec_IntClear( p->vAnds ); // add root node - Vec_IntFill( p->vNodes, 1, iPivot ); - Vec_BitWriteEntry( p->vMarksNo, iPivot, 1 ); + Spl_ManLutMffcSize( p->pGia, iPivot, p->vCands, p->vMarksAnd ); + Spl_ManAddNode( p, iPivot, p->vCands ); + if ( Vec_IntSize(p->vAnds) > p->Limit ) + return 0; //printf( "%d ", iPivot ); // add one node at a time - p->Count = Spl_ManLutMffcSize( p->pGia, iPivot ); while ( (iObj = Spl_ManFindOne(p)) ) { - assert( Gia_ObjIsLut(p->pGia, iObj) ); - CountAdd = Spl_ManLutMffcSize( p->pGia, iObj ); - if ( p->Count + CountAdd > p->Limit ) + assert( Gia_ObjIsLut2(p->pGia, iObj) ); + assert( !Vec_BitEntry(p->vMarksNo, iObj) ); + CountAdd = Spl_ManLutMffcSize( p->pGia, iObj, p->vCands, p->vMarksAnd ); + if ( Vec_IntSize(p->vAnds) + CountAdd > p->Limit ) break; - p->Count += CountAdd; - Vec_IntPush( p->vNodes, iObj ); - Vec_BitWriteEntry( p->vMarksNo, iObj, 1 ); + Spl_ManAddNode( p, iObj, p->vCands ); //printf( "+%d ", iObj ); } //printf( "\n" ); Vec_IntSort( p->vNodes, 0 ); + Vec_IntSort( p->vAnds, 0 ); + Spl_ManWinFindLeavesRoots( p ); + Vec_IntSort( p->vLeaves, 0 ); + Vec_IntSort( p->vRoots, 0 ); + return 1; } +/**Function************************************************************* + + Synopsis [External procedures.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManComputeOneWin( Gia_Man_t * pGia, int iPivot, Vec_Int_t ** pvRoots, Vec_Int_t ** pvNodes, Vec_Int_t ** pvLeaves, Vec_Int_t ** pvAnds ) +{ + Spl_Man_t * p = (Spl_Man_t *)pGia->pSatlutWinman; + assert( p != NULL ); + if ( iPivot == -1 ) + { + Spl_ManStop( p ); + pGia->pSatlutWinman = NULL; + return 0; + } + if ( !Spl_ManComputeOne( p, iPivot ) ) + { + *pvRoots = NULL; + *pvNodes = NULL; + *pvLeaves = NULL; + *pvAnds = NULL; + return 0; + } + *pvRoots = p->vRoots; + *pvNodes = p->vNodes; + *pvLeaves = p->vLeaves; + *pvAnds = p->vAnds; + // Vec_IntPrint( p->vNodes ); + return Vec_IntSize(p->vAnds); +} +void Gia_ManComputeOneWinStart( Gia_Man_t * pGia, int fReverse ) +{ + assert( pGia->pSatlutWinman == NULL ); + pGia->pSatlutWinman = Spl_ManAlloc( pGia, 64, fReverse ); +} + +/**Function************************************************************* + + Synopsis [Testing procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Spl_ManComputeOneTest( Gia_Man_t * pGia ) { - int iLut; - Spl_Man_t * p = Spl_ManAlloc( pGia, 64 ); - Gia_ManForEachLut( pGia, iLut ) + int iLut, Count; + Gia_ManComputeOneWinStart( pGia, 0 ); + Gia_ManForEachLut2( pGia, iLut ) { - Spl_ManComputeOne( p, iLut ); - Spl_ManWinFindLeavesRoots( p ); - // Vec_IntPrint( p->vNodes ); + Vec_Int_t * vRoots, * vNodes, * vLeaves, * vAnds; + Count = Gia_ManComputeOneWin( pGia, iLut, &vRoots, &vNodes, &vLeaves, &vAnds ); printf( "Obj = %6d : Leaf = %2d. Node = %2d. Root = %2d. AND = %3d.\n", - iLut, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vRoots), p->Count ); + iLut, Vec_IntSize(vLeaves), Vec_IntSize(vNodes), Vec_IntSize(vRoots), Count ); } - Spl_ManStop( p ); + Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL ); } //////////////////////////////////////////////////////////////////////// |