diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-05 12:52:40 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-05 12:52:40 -0700 |
commit | e4f9ebfa8773364e76f2493a694892e7fb2b6d95 (patch) | |
tree | 559dd045a74fc4f304d8a6ab6627940bedd63bbf /src | |
parent | eddb194ce0b2a1a505cbf445a56dcaa27abdc270 (diff) | |
download | abc-e4f9ebfa8773364e76f2493a694892e7fb2b6d95.tar.gz abc-e4f9ebfa8773364e76f2493a694892e7fb2b6d95.tar.bz2 abc-e4f9ebfa8773364e76f2493a694892e7fb2b6d95.zip |
Improved unrolling manager.
Diffstat (limited to 'src')
-rw-r--r-- | src/sat/bmc/bmcUnroll.c | 186 |
1 files changed, 92 insertions, 94 deletions
diff --git a/src/sat/bmc/bmcUnroll.c b/src/sat/bmc/bmcUnroll.c index d33132ed..c05eb66b 100644 --- a/src/sat/bmc/bmcUnroll.c +++ b/src/sat/bmc/bmcUnroll.c @@ -37,8 +37,10 @@ struct Unr_Obj_t_ unsigned fCompl1 : 1; // complemented bit unsigned uRDiff0 : 15; // rank diff of the fanin unsigned uRDiff1 : 15; // rank diff of the fanin - unsigned RankMax : 16; // max rank diff between node and its fanout - unsigned RankCur : 16; // cur rank of the node + unsigned fItIsPi : 1; // remember attributes + unsigned fItIsPo : 1; // remember attributes + unsigned RankMax : 15; // max rank diff between node and its fanout + unsigned RankCur : 15; // cur rank of the node unsigned OrigId; // original object ID unsigned Res[1]; // RankMax entries }; @@ -48,7 +50,7 @@ struct Unr_Man_t_ { // input data Gia_Man_t * pGia; // the user's AIG manager -// Gia_Man_t * pNew; // unrolling manager + Gia_Man_t * pFrames; // unrolled manager int nObjs; // the number of objects // intermediate data Vec_Int_t * vOrder; // ordering of GIA objects @@ -59,13 +61,15 @@ struct Unr_Man_t_ int * pObjs; // storage for unroling objects int * pEnd; // end of storage Vec_Int_t * vObjLim; // handle of the first object in each frame - Vec_Int_t * vResLits; // resulting literals Vec_Int_t * vCiMap; // mapping of GIA CIs into unrolling objects Vec_Int_t * vCoMap; // mapping of GIA POs into unrolling objects + Vec_Int_t * vPiLits; // storage for PI literals }; static inline Unr_Obj_t * Unr_ManObj( Unr_Man_t * p, int h ) { assert( h >= 0 && h < p->pEnd - p->pObjs ); return (Unr_Obj_t *)(p->pObjs + h); } -static inline int Unr_ObjSize( Unr_Obj_t * pObj ) { return 0x7FFFFFFE & (sizeof(Unr_Obj_t) / sizeof(int) + pObj->RankMax); } +static inline int Unr_ObjSizeInt( int Rank ) { return 0xFFFFFFFE & (sizeof(Unr_Obj_t) / sizeof(int) + Rank); } +static inline int Unr_ObjSize( Unr_Obj_t * pObj ) { return Unr_ObjSizeInt(pObj->RankMax); } + static inline int Unr_ManFanin0Value( Unr_Man_t * p, Unr_Obj_t * pObj ) { Unr_Obj_t * pFanin = Unr_ManObj( p, pObj->hFan0 ); @@ -89,7 +93,8 @@ static inline int Unr_ManObjReadValue( Unr_Obj_t * pObj ) } static inline void Unr_ManObjSetValue( Unr_Obj_t * pObj, int Value ) { - pObj->RankCur = (0xFFFF & (pObj->RankCur + 1)) % pObj->RankMax; + assert( Value >= 0 ); + pObj->RankCur = (UNR_DIFF_NULL & (pObj->RankCur + 1)) % pObj->RankMax; pObj->Res[ pObj->RankCur ] = Value; } @@ -134,10 +139,12 @@ void Unr_ManProfileRanks( Vec_Int_t * vRanks ) Vec_IntAddToEntry( vCounts, Rank, 1 ); Vec_IntForEachEntry( vCounts, Count, i ) { + if ( Count == 0 ) + continue; printf( "%2d : %8d (%6.2f %%)\n", i, Count, 100.0 * Count / Vec_IntSize(vRanks) ); nExtras += Count * i; } - printf( "Extra space = %d (%6.2f %%)\n", nExtras, 100.0 * nExtras / Vec_IntSize(vRanks) ); + printf( "Extra space = %d (%6.2f %%) ", nExtras, 100.0 * nExtras / Vec_IntSize(vRanks) ); Vec_IntFree( vCounts ); } @@ -177,15 +184,13 @@ void Unr_ManSetup_rec( Unr_Man_t * p, int iObj, int iTent, Vec_Int_t * vRoots ) } Vec_IntPush( p->vOrder, iObj ); } -void Unr_ManSetup( Unr_Man_t * p ) +void Unr_ManSetup( Unr_Man_t * p, int fVerbose ) { Vec_Int_t * vRoots, * vRoots2, * vMap; Unr_Obj_t * pUnrObj; Gia_Obj_t * pObj; - int i, k, t, iObj, Rank, nInts, * pInts; + int i, k, t, iObj, nInts, * pInts; abctime clk = Abc_Clock(); - vRoots = Vec_IntAlloc( 100 ); - vRoots2 = Vec_IntAlloc( 100 ); // create zero rank assert( Vec_IntSize(p->vOrder) == 0 ); Vec_IntPush( p->vOrder, 0 ); @@ -193,9 +198,11 @@ void Unr_ManSetup( Unr_Man_t * p ) Vec_IntWriteEntry( p->vTents, 0, 0 ); Vec_IntWriteEntry( p->vRanks, 0, 0 ); // start from the POs + vRoots = Vec_IntAlloc( 100 ); + vRoots2 = Vec_IntAlloc( 100 ); Gia_ManForEachPo( p->pGia, pObj, i ) Unr_ManSetup_rec( p, Gia_ObjId(p->pGia, pObj), 0, vRoots ); - // iterate through tents + // collect tents while ( Vec_IntSize(vRoots) > 0 ) { Vec_IntPush( p->vOrderLim, Vec_IntSize(p->vOrder) ); @@ -208,14 +215,14 @@ void Unr_ManSetup( Unr_Man_t * p ) Vec_IntFree( vRoots ); Vec_IntFree( vRoots2 ); // allocate memory - nInts = Vec_IntSize(p->vOrder) * (sizeof(Unr_Obj_t) / sizeof(int)); - Vec_IntForEachEntry( p->vRanks, Rank, i ) - nInts += 0x7FFFFFFE & (Rank + 1); + nInts = 0; + Vec_IntForEachEntry( p->vOrder, iObj, i ) + nInts += Unr_ObjSizeInt( Vec_IntEntry(p->vRanks, iObj) + 1 ); p->pObjs = pInts = ABC_CALLOC( int, nInts ); p->pEnd = p->pObjs + nInts; // create const0 node pUnrObj = Unr_ManObj( p, pInts - p->pObjs ); - pUnrObj->RankMax = 1; + pUnrObj->RankMax = Vec_IntEntry(p->vRanks, 0) + 1; pUnrObj->uRDiff0 = pUnrObj->uRDiff1 = UNR_DIFF_NULL; pUnrObj->Res[0] = 0; // const0 // map the objects @@ -241,20 +248,16 @@ void Unr_ManSetup( Unr_Man_t * p ) else if ( Gia_ObjIsRo(p->pGia, pObj) ) pUnrObj->uRDiff0 = 0; pUnrObj->RankMax = Vec_IntEntry(p->vRanks, iObj) + 1; - pUnrObj->RankCur = 0xFFFF; + pUnrObj->RankCur = UNR_DIFF_NULL; pUnrObj->OrigId = iObj; for ( k = 0; k < (int)pUnrObj->RankMax; k++ ) pUnrObj->Res[k] = -1; + assert( ((pInts - p->pObjs) & 1) == 0 ); // align for 64-bits Vec_IntWriteEntry( vMap, iObj, pInts - p->pObjs ); pInts += Unr_ObjSize( pUnrObj ); } } - assert( pInts - p->pObjs <= nInts ); -Unr_ManProfileRanks( p->vRanks ); - Vec_IntFreeP( &p->vOrder ); - Vec_IntFreeP( &p->vOrderLim ); - Vec_IntFreeP( &p->vRanks ); -// Vec_IntFreeP( &p->vTents ); + assert( pInts - p->pObjs == nInts ); // label the objects Gia_ManForEachObj( p->pGia, pObj, i ) { @@ -265,19 +268,24 @@ Unr_ManProfileRanks( p->vRanks ); { pUnrObj->hFan0 = Vec_IntEntry( vMap, Gia_ObjFaninId0(pObj, i) ); pUnrObj->fCompl0 = Gia_ObjFaninC0(pObj); - assert( pUnrObj->hFan0 != ~0 ); + pUnrObj->fItIsPo = Gia_ObjIsPo(p->pGia, pObj); } if ( Gia_ObjIsAnd(pObj) ) { pUnrObj->hFan1 = Vec_IntEntry( vMap, Gia_ObjFaninId1(pObj, i) ); pUnrObj->fCompl1 = Gia_ObjFaninC1(pObj); - assert( pUnrObj->hFan1 != ~0); } else if ( Gia_ObjIsRo(p->pGia, pObj) ) { pUnrObj->hFan0 = Vec_IntEntry( vMap, Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj)) ); pUnrObj->fCompl0 = 0; } + else if ( Gia_ObjIsPi(p->pGia, pObj) ) + { + pUnrObj->hFan0 = Gia_ObjCioId(pObj); // remember CIO id + pUnrObj->hFan1 = Vec_IntEntry(p->vTents, i); // remember tent + pUnrObj->fItIsPi = 1; + } } // store CI/PO objects; Gia_ManForEachCi( p->pGia, pObj, i ) @@ -285,9 +293,17 @@ Unr_ManProfileRanks( p->vRanks ); Gia_ManForEachCo( p->pGia, pObj, i ) Vec_IntPush( p->vCoMap, Vec_IntEntry(vMap, Gia_ObjId(p->pGia, pObj)) ); Vec_IntFreeP( &vMap ); - - printf( "Memory usage = %6.2f MB\n", 4.0 * nInts / (1<<20) ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + // print stats + if ( fVerbose ) + { + Unr_ManProfileRanks( p->vRanks ); + printf( "Memory usage = %6.2f MB ", 4.0 * nInts / (1<<20) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + Vec_IntFreeP( &p->vOrder ); + Vec_IntFreeP( &p->vOrderLim ); + Vec_IntFreeP( &p->vRanks ); + Vec_IntFreeP( &p->vTents ); } @@ -309,21 +325,22 @@ Unr_Man_t * Unr_ManAlloc( Gia_Man_t * pGia ) p = ABC_CALLOC( Unr_Man_t, 1 ); p->pGia = pGia; p->nObjs = Gia_ManObjNum(pGia); -// p->pNew = Gia_ManStart( 10000 ); p->vOrder = Vec_IntAlloc( p->nObjs ); p->vOrderLim = Vec_IntAlloc( 100 ); p->vTents = Vec_IntStartFull( p->nObjs ); p->vRanks = Vec_IntStart( p->nObjs ); p->vObjLim = Vec_IntAlloc( 100 ); - p->vResLits = Vec_IntAlloc( Gia_ManPoNum(pGia) ); p->vCiMap = Vec_IntAlloc( Gia_ManCiNum(pGia) ); p->vCoMap = Vec_IntAlloc( Gia_ManCoNum(pGia) ); + p->vPiLits = Vec_IntAlloc( 10000 ); + p->pFrames = Gia_ManStart( 10000 ); + p->pFrames->pName = Abc_UtilStrsav( pGia->pName ); + Gia_ManHashStart( p->pFrames ); return p; } void Unr_ManFree( Unr_Man_t * p ) { -// Gia_ManStop( p->pNew ); - Vec_IntFreeP( &p->vTents ); + Gia_ManStop( p->pFrames ); // intermediate data Vec_IntFreeP( &p->vOrder ); Vec_IntFreeP( &p->vOrderLim ); @@ -331,9 +348,9 @@ void Unr_ManFree( Unr_Man_t * p ) Vec_IntFreeP( &p->vRanks ); // unrolling data Vec_IntFreeP( &p->vObjLim ); - Vec_IntFreeP( &p->vResLits ); Vec_IntFreeP( &p->vCiMap ); Vec_IntFreeP( &p->vCoMap ); + Vec_IntFreeP( &p->vPiLits ); ABC_FREE( p->pObjs ); ABC_FREE( p ); } @@ -349,69 +366,53 @@ void Unr_ManFree( Unr_Man_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Unr_ManUnroll( Unr_Man_t * p, int nFrames ) +void Unr_ManUnrollStart( Unr_Man_t * p ) { - Gia_Man_t * pTemp, * pFrames; - Unr_Obj_t * pUnrObj; - Vec_Int_t * vPiLits; - int f, i, iLit, iLit0, iLit1, hStart; - pFrames = Gia_ManStart( 10000 ); - pFrames->pName = Abc_UtilStrsav( p->pGia->pName ); - Gia_ManHashAlloc( pFrames ); - // create flop values + int i, iHandle; for ( i = 0; i < Gia_ManRegNum(p->pGia); i++ ) + if ( (iHandle = Vec_IntEntry(p->vCoMap, Gia_ManPoNum(p->pGia) + i)) != -1 ) + Unr_ManObjSetValue( Unr_ManObj(p, iHandle), 0 ); +} +void Unr_ManUnrollFrame( Unr_Man_t * p, int f ) +{ + int i, iLit, iLit0, iLit1, hStart; + for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ ) + Vec_IntPush( p->vPiLits, Gia_ManAppendCi(p->pFrames) ); + hStart = Vec_IntEntry( p->vObjLim, Abc_MaxInt(0, Vec_IntSize(p->vObjLim)-1-f) ); + while ( p->pObjs + hStart < p->pEnd ) { - if ( Vec_IntEntry(p->vCoMap, Gia_ManPoNum(p->pGia) + i) == -1 ) - continue; - pUnrObj = Unr_ManObj( p, Vec_IntEntry(p->vCoMap, Gia_ManPoNum(p->pGia) + i) ); - Unr_ManObjSetValue( pUnrObj, 0 ); - } - vPiLits = Vec_IntAlloc( nFrames * Gia_ManPiNum(p->pGia) ); - for ( f = 0; f < nFrames; f++ ) - { - for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ ) - Vec_IntPush( vPiLits, Gia_ManAppendCi(pFrames) ); - hStart = Vec_IntEntry( p->vObjLim, Abc_MaxInt(0, Vec_IntSize(p->vObjLim)-1-f) ); - while ( p->pObjs + hStart < p->pEnd ) + Unr_Obj_t * pUnrObj = Unr_ManObj( p, hStart ); + if ( pUnrObj->uRDiff0 != UNR_DIFF_NULL && pUnrObj->uRDiff1 != UNR_DIFF_NULL ) // AND node + { + iLit0 = Unr_ManFanin0Value( p, pUnrObj ); + iLit1 = Unr_ManFanin1Value( p, pUnrObj ); + iLit = Gia_ManHashAnd( p->pFrames, iLit0, iLit1 ); + Unr_ManObjSetValue( pUnrObj, iLit ); + } + else if ( pUnrObj->uRDiff0 != UNR_DIFF_NULL && pUnrObj->uRDiff1 == UNR_DIFF_NULL ) // PO/RI/RO { - pUnrObj = Unr_ManObj( p, hStart ); - if ( pUnrObj->uRDiff0 != UNR_DIFF_NULL && pUnrObj->uRDiff1 != UNR_DIFF_NULL ) - { - iLit0 = Unr_ManFanin0Value( p, pUnrObj ); - iLit1 = Unr_ManFanin1Value( p, pUnrObj ); - iLit = Gia_ManHashAnd( pFrames, iLit0, iLit1 ); - assert( iLit >= 0 ); - Unr_ManObjSetValue( pUnrObj, iLit ); - } - else if ( pUnrObj->uRDiff0 != UNR_DIFF_NULL && pUnrObj->uRDiff1 == UNR_DIFF_NULL ) - { - iLit = Unr_ManFanin0Value( p, pUnrObj ); - assert( iLit >= 0 ); - Unr_ManObjSetValue( pUnrObj, iLit ); - } - else - { - Gia_Obj_t * pObj = Gia_ManObj(p->pGia, pUnrObj->OrigId); - assert( Gia_ObjIsPi(p->pGia, pObj) ); - assert( f >= Vec_IntEntry(p->vTents, pUnrObj->OrigId) ); - iLit = Vec_IntEntry( vPiLits, Gia_ManPiNum(p->pGia) * (f - Vec_IntEntry(p->vTents, pUnrObj->OrigId)) + Gia_ObjCioId(pObj) ); - Unr_ManObjSetValue( pUnrObj, iLit ); - } - hStart += Unr_ObjSize( pUnrObj ); + iLit = Unr_ManFanin0Value( p, pUnrObj ); + Unr_ManObjSetValue( pUnrObj, iLit ); + if ( pUnrObj->fItIsPo ) + Gia_ManAppendCo( p->pFrames, iLit ); } - assert( p->pObjs + hStart == p->pEnd ); - for ( i = 0; i < Gia_ManPoNum(p->pGia); i++ ) + else // PI (pUnrObj->hFan0 is CioId; pUnrObj->hFan1 is tent) { - pUnrObj = Unr_ManObj(p, Vec_IntEntry(p->vCoMap, i)); - Gia_ManAppendCo( pFrames, Unr_ManObjReadValue(pUnrObj) ); + assert( pUnrObj->fItIsPi && f >= (int)pUnrObj->hFan1 ); + iLit = Vec_IntEntry( p->vPiLits, Gia_ManPiNum(p->pGia) * (f - pUnrObj->hFan1) + pUnrObj->hFan0 ); + Unr_ManObjSetValue( pUnrObj, iLit ); } + hStart += Unr_ObjSize( pUnrObj ); } - Vec_IntFree( vPiLits ); - Gia_ManHashStop( pFrames ); - Gia_ManSetRegNum( pFrames, 0 ); - pFrames = Gia_ManCleanup( pTemp = pFrames ); - Gia_ManStop( pTemp ); - return pFrames; + assert( p->pObjs + hStart == p->pEnd ); +} +Gia_Man_t * Unr_ManUnroll( Unr_Man_t * p, int nFrames ) +{ + int f; + Unr_ManUnrollStart( p ); + for ( f = 0; f < nFrames; f++ ) + Unr_ManUnrollFrame( p, f ); + return Gia_ManCleanup( p->pFrames ); } /**Function************************************************************* @@ -470,14 +471,10 @@ Gia_Man_t * Unr_ManUnrollSimple( Gia_Man_t * pGia, int nFrames ) void Unr_ManTest( Gia_Man_t * pGia, int nFrames ) { Gia_Man_t * pFrames0, * pFrames1; - Unr_Man_t * p; - abctime clk = Abc_Clock(); + Unr_Man_t * p; p = Unr_ManAlloc( pGia ); - Unr_ManSetup( p ); - Abc_PrintTime( 1, "Prepare", Abc_Clock() - clk ); - - clk = Abc_Clock(); + Unr_ManSetup( p, 1 ); pFrames0 = Unr_ManUnroll( p, nFrames ); Abc_PrintTime( 1, "Unroll ", Abc_Clock() - clk ); @@ -491,6 +488,7 @@ Gia_ManPrintStats( pFrames0, 0, 0, 0 ); Gia_ManPrintStats( pFrames1, 0, 0, 0 ); Gia_AigerWrite( pFrames0, "frames0.aig", 0, 0 ); Gia_AigerWrite( pFrames1, "frames1.aig", 0, 0 ); + Gia_ManStop( pFrames0 ); Gia_ManStop( pFrames1 ); } |