diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-25 22:41:34 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-25 22:41:34 -0800 |
commit | caa2227b1127802e4b35f296106ca19e113ea601 (patch) | |
tree | 9fb8f4f2099f829063e96b1b74ea26c803fa50eb | |
parent | 15a1c4b96507b524959d171a26b796d6263ea284 (diff) | |
download | abc-caa2227b1127802e4b35f296106ca19e113ea601.tar.gz abc-caa2227b1127802e4b35f296106ca19e113ea601.tar.bz2 abc-caa2227b1127802e4b35f296106ca19e113ea601.zip |
Changes to LUT mappers.
-rw-r--r-- | src/base/abci/abc.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcDec.c | 9 | ||||
-rw-r--r-- | src/map/if/if.h | 10 | ||||
-rw-r--r-- | src/map/if/ifDsd.c | 255 | ||||
-rw-r--r-- | src/map/if/ifMan.c | 12 | ||||
-rw-r--r-- | src/map/if/ifMap.c | 22 | ||||
-rw-r--r-- | src/opt/dau/dau.h | 5 | ||||
-rw-r--r-- | src/opt/dau/dauNonDsd.c | 29 |
8 files changed, 295 insertions, 51 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b170bfc4..6db36aa0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2201,7 +2201,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Kit_DsdTest( unsigned * pTruth, int nVars ); extern void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose ); - extern void Dau_DecTrySets( word * p, int nVars ); + extern void Dau_DecTrySets( word * p, int nVars, int fVerbose ); // set defaults nCofLevel = 1; @@ -2274,7 +2274,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) // Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) ); // Abc_Print( -1, "\n" ); if ( fPrintDec )//&&Abc_ObjFaninNum(pObj) <= 6 ) - Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj) ); + Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj), 1 ); if ( fProfile ) Kit_TruthPrintProfile( pTruth, Abc_ObjFaninNum(pObj) ); else if ( fCofactor ) diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c index 873ef876..3ed73c26 100644 --- a/src/base/abci/abcDec.c +++ b/src/base/abci/abcDec.c @@ -25,6 +25,7 @@ #include "bool/dec/dec.h" #include "bool/kit/kit.h" #include "opt/dau/dau.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -564,11 +565,13 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose ) { for ( i = 0; i < p->nFuncs; i++ ) { - extern void Dau_DecTrySets( word * pInit, int nVars ); + extern void Dau_DecTrySets( word * pInit, int nVars, int fVerbose ); + int nSuppSize = Abc_TtSupportSize( p->pFuncs[i], p->nVars ); if ( fVerbose ) printf( "%7d : ", i ); - Dau_DecTrySets( p->pFuncs[i], p->nVars ); - printf( "\n" ); + Dau_DecTrySets( p->pFuncs[i], nSuppSize, fVerbose ); + if ( fVerbose ) + printf( "\n" ); } } else assert( 0 ); diff --git a/src/map/if/if.h b/src/map/if/if.h index 8821d06f..41d30da4 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -35,9 +35,9 @@ #include "misc/mem/mem.h" #include "misc/tim/tim.h" #include "misc/util/utilNam.h" -#include "opt/dau/dau.h" #include "misc/vec/vecMem.h" #include "misc/util/utilTruth.h" +#include "opt/dau/dau.h" ABC_NAMESPACE_HEADER_START @@ -153,8 +153,8 @@ struct If_Par_t_ float * pTimesArr; // arrival times float * pTimesReq; // required times int (* pFuncCost) (If_Man_t *, If_Cut_t *); // procedure to compute the user's cost of a cut - int (* pFuncUser) (If_Man_t *, If_Obj_t *, If_Cut_t *); // procedure called for each cut when cut computation is finished - int (* pFuncCell) (If_Man_t *, unsigned *, int, int, char *); // procedure called for cut functions + int (* pFuncUser) (If_Man_t *, If_Obj_t *, If_Cut_t *); // procedure called for each cut when cut computation is finished + int (* pFuncCell) (If_Man_t *, unsigned *, int, int, char *); // procedure called for cut functions void * pReoMan; // reordering manager }; @@ -233,6 +233,7 @@ struct If_Man_t_ int nCuts5, nCuts5a; If_DsdMan_t * pIfDsdMan; Vec_Mem_t * vTtMem; // truth table memory and hash table + Vec_Int_t * vDsds; // mapping of truth table into DSD int nBestCutSmall[2]; // timing manager @@ -518,7 +519,8 @@ extern If_DsdMan_t * If_DsdManAlloc( int nLutSize ); extern void If_DsdManDump( If_DsdMan_t * p ); extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ); extern void If_DsdManFree( If_DsdMan_t * p ); -extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm ); +extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct ); +extern int If_DsdManCheckDec( If_DsdMan_t * pIfMan, int iDsd ); /*=== ifLib.c =============================================================*/ extern If_LibLut_t * If_LibLutRead( char * FileName ); extern If_LibLut_t * If_LibLutDup( If_LibLut_t * p ); diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index f387e645..5c3fecc9 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -44,7 +44,8 @@ struct If_DsdObj_t_ unsigned Id; // node ID unsigned Type : 3; // node type unsigned nSupp : 5; // variable - unsigned Count : 19; // variable + unsigned fMark : 1; // user mark + unsigned Count : 18; // variable unsigned nFans : 5; // fanin count unsigned pFans[0]; // fanins }; @@ -58,10 +59,10 @@ struct If_DsdMan_t_ Mem_Flex_t * pMem; // memory for nodes Vec_Ptr_t * vObjs; // objects Vec_Int_t * vNexts; // next pointers - Vec_Int_t * vLeaves; // temp - Vec_Int_t * vCopies; // temp + Vec_Int_t * vNodes; // temp word ** pTtElems; // elementary TTs Vec_Mem_t * vTtMem; // truth table memory and hash table + Vec_Ptr_t * vTtDecs; // truth table decompositions int nUniqueHits; // statistics int nUniqueMisses; // statistics abctime timeBeg; // statistics @@ -90,13 +91,15 @@ static inline If_DsdObj_t * If_DsdVecVar( Vec_Ptr_t * p, int v ) static inline int If_DsdVecObjSuppSize( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->nSupp; } static inline int If_DsdVecLitSuppSize( Vec_Ptr_t * p, int iLit ) { return If_DsdVecObjSuppSize( p, Abc_Lit2Var(iLit) ); } static inline int If_DsdVecObjRef( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->Count; } -static inline void If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj ) { if ( If_DsdVecObjRef(p, iObj) < 0x7FFFF ) If_DsdVecObj( p, iObj )->Count++; } +static inline void If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj ) { if ( If_DsdVecObjRef(p, iObj) < 0x3FFFF ) If_DsdVecObj( p, iObj )->Count++; } static inline If_DsdObj_t * If_DsdObjFanin( Vec_Ptr_t * p, If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return If_DsdVecObj(p, Abc_Lit2Var(pObj->pFans[i])); } +static inline int If_DsdVecObjMark( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->fMark; } +static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj ) { If_DsdVecObj( p, iObj )->fMark = 1; } #define If_DsdVecForEachObj( vVec, pObj, i ) \ Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i ) -#define If_DsdVecForEachObjVec( vLits, vVec, pObj, i ) \ - for ( i = 0; (i < Vec_IntSize(vLits)) && ((pObj) = Dss_Lit2Obj(vVec, Vec_IntEntry(vLits,i))); i++ ) +#define If_DsdVecForEachObjVec( vNodes, vVec, pObj, i ) \ + for ( i = 0; (i < Vec_IntSize(vNodes)) && ((pObj) = If_DsdVecObj(vVec, Vec_IntEntry(vNodes,i))); i++ ) #define If_DsdVecForEachNode( vVec, pObj, i ) \ Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i ) \ if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR ) {} else @@ -183,6 +186,7 @@ If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans ) pObj->Type = Type; pObj->nFans = nFans; pObj->Id = Vec_PtrSize( p->vObjs ); + pObj->fMark = 0; pObj->Count = 0; Vec_PtrPush( p->vObjs, pObj ); Vec_IntPush( p->vNexts, 0 ); @@ -263,10 +267,11 @@ If_DsdMan_t * If_DsdManAlloc( int nVars ) p->vNexts = Vec_IntAlloc( 10000 ); If_DsdObjAlloc( p, IF_DSD_CONST0, 0 ); If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1; - p->vLeaves = Vec_IntAlloc( 32 ); - p->vCopies = Vec_IntAlloc( 32 ); + p->vNodes = Vec_IntAlloc( 32 ); p->pTtElems = If_ManDsdTtElems(); - p->vTtMem = Vec_MemAllocForTT( nVars ); + p->vTtDecs = Vec_PtrAlloc( 1000 ); + p->vTtMem = Vec_MemAlloc( Abc_TtWordNum(nVars), 12 ); + Vec_MemHashAlloc( p->vTtMem, 10000 ); return p; } void If_DsdManFree( If_DsdMan_t * p ) @@ -282,10 +287,10 @@ void If_DsdManFree( If_DsdMan_t * p ) Abc_PrintTime( 1, "Time lookup", p->timeLook ); Abc_PrintTime( 1, "Time end ", p->timeEnd ); } + Vec_VecFree( (Vec_Vec_t *)p->vTtDecs ); Vec_MemHashFree( p->vTtMem ); Vec_MemFreeP( &p->vTtMem ); - Vec_IntFreeP( &p->vCopies ); - Vec_IntFreeP( &p->vLeaves ); + Vec_IntFreeP( &p->vNodes ); Vec_IntFreeP( &p->vNexts ); Vec_PtrFreeP( &p->vObjs ); Mem_FlexStop( p->pMem, 0 ); @@ -331,20 +336,21 @@ void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, unsigned ch If_DsdManPrint_rec( pFile, p, iFanin, pPermLits, pnSupp ); fprintf( pFile, "%c", CloseType[If_DsdObjType(pObj)] ); } -void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char * pPermLits ) +void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char * pPermLits, int fNewLine ) { int nSupp = 0; fprintf( pFile, "%6d : ", iObjId ); fprintf( pFile, "%2d ", If_DsdVecObjSuppSize(p->vObjs, iObjId) ); fprintf( pFile, "%8d ", If_DsdVecObjRef(p->vObjs, iObjId) ); If_DsdManPrint_rec( pFile, p, Abc_Var2Lit(iObjId, 0), pPermLits, &nSupp ); - fprintf( pFile, "\n" ); + if ( fNewLine ) + fprintf( pFile, "\n" ); assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, iObjId) ); } void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ) { If_DsdObj_t * pObj; - int CountNonDsd = 0, CountNonDsdStr = 0; + int DsdMax = 0, CountUsed = 0, CountNonDsdStr = 0; int i, clk = Abc_Clock(); FILE * pFile; pFile = pFileName ? fopen( pFileName, "wb" ) : stdout; @@ -355,17 +361,20 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ) } If_DsdVecForEachObj( p->vObjs, pObj, i ) { - CountNonDsd += (If_DsdObjType(pObj) == IF_DSD_PRIME); + if ( If_DsdObjType(pObj) == IF_DSD_PRIME ) + DsdMax = Abc_MaxInt( DsdMax, pObj->nFans ); CountNonDsdStr += If_DsdManCheckNonDec_rec( p, pObj->Id ); + CountUsed += ( If_DsdVecObjRef(p->vObjs, pObj->Id) > 0 ); } fprintf( pFile, "Total number of objects = %8d\n", Vec_PtrSize(p->vObjs) ); - fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", Vec_MemEntryNum(p->vTtMem), CountNonDsd ); + fprintf( pFile, "Externally used objects = %8d\n", CountUsed ); + fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", DsdMax, Vec_MemEntryNum(p->vTtMem) ); fprintf( pFile, "Non-DSD structures = %8d\n", CountNonDsdStr ); - fprintf( pFile, "Memory used for objects = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) ); - fprintf( pFile, "Memory used for array = %6.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) ); - fprintf( pFile, "Memory used for hash table = %6.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) ); fprintf( pFile, "Unique table hits = %8d\n", p->nUniqueHits ); fprintf( pFile, "Unique table misses = %8d\n", p->nUniqueMisses ); + fprintf( pFile, "Memory used for objects = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) ); + fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) ); + fprintf( pFile, "Memory used for array = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); // If_DsdManHashProfile( p ); // If_DsdManDump( p ); @@ -376,7 +385,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ) { // if ( i == 50 ) // break; - If_DsdManPrintOne( pFile, p, pObj->Id, NULL ); + If_DsdManPrintOne( pFile, p, pObj->Id, NULL, 1 ); } fprintf( pFile, "\n" ); if ( pFileName ) @@ -403,13 +412,39 @@ void If_DsdManDump( If_DsdMan_t * p ) fprintf( pFile, "\n" ); printf( " " ); Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars ); - printf( "\n" ); } fclose( pFile ); } /**Function************************************************************* + Synopsis [Collect nodes of the tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes ) +{ + int i, iFanin; + If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id ); + if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR ) + return; + If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) + If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes ); + Vec_IntPush( vNodes, Id ); +} +void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes ) +{ + Vec_IntClear( vNodes ); + If_DsdManCollect_rec( p, Id, vNodes ); +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -470,6 +505,12 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId ); if ( *pSpot ) return *pSpot; + if ( truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem)-1 ) + { + Vec_Int_t * vSets = Dau_DecFindSets( pTruth, nLits ); + Vec_PtrPush( p->vTtDecs, vSets ); +// Dau_DecPrintSets( vSets, nLits ); + } *pSpot = Vec_PtrSize( p->vObjs ); return If_DsdObjCreate( p, Type, pLits, nLits, truthId ); } @@ -768,6 +809,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig assert( j == nSSize ); for ( j = 0; j < nSSize; j++ ) pPerm[j] = pPermNew[j]; + Abc_TtStretch6( pTruth, nLits, p->nVars ); } else assert( 0 ); // create new graph @@ -864,6 +906,158 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char /**Function************************************************************* + Synopsis [Returns 1 if XY-decomposability holds to this LUT size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +// collect supports of the node +void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes ) +{ + If_DsdObj_t * pFanin; int i; + If_DsdObjForEachFanin( p->vObjs, pObj, pFanin, i ) + pSSizes[i] = If_DsdObjSuppSize(pFanin); +} +// checks if there is a way to package some fanins +int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize ) +{ + int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; + int nFans = If_DsdObjFaninNum(pObj); + assert( pObj->nFans > 2 ); + assert( If_DsdObjSuppSize(pObj) > LutSize ); + If_DsdManGetSuppSizes( p, pObj, pSSizes ); + LimitOut = LutSize - (nSuppAll - pObj->nSupp + 1); + assert( LimitOut < LutSize ); + for ( i[0] = 0; i[0] < nFans; i[0]++ ) + for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ ) + { + SizeIn = pSSizes[i[0]] + pSSizes[i[1]]; + SizeOut = pObj->nSupp - SizeIn; + if ( SizeIn > LutSize || SizeOut > LimitOut ) + continue; + return (1 << i[0]) | (1 << i[1]); + } + if ( pObj->nFans == 3 ) + return 0; + for ( i[0] = 0; i[0] < nFans; i[0]++ ) + for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ ) + for ( i[2] = i[1]+1; i[2] < nFans; i[2]++ ) + { + SizeIn = pSSizes[i[0]] + pSSizes[i[1]] + pSSizes[i[2]]; + SizeOut = pObj->nSupp - SizeIn; + if ( SizeIn > LutSize || SizeOut > LimitOut ) + continue; + return (1 << i[0]) | (1 << i[1]) | (1 << i[2]); + } + return 0; +} +// checks if there is a way to package some fanins +int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize ) +{ + int fVerbose = 0; + int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; + int truthId = If_DsdObjTruthId( p, pObj ); + int nFans = If_DsdObjFaninNum(pObj); + Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs, truthId); +if ( fVerbose ) +printf( "\n" ); +if ( fVerbose ) +Dau_DecPrintSets( vSets, nFans ); + assert( pObj->nFans > 2 ); + assert( If_DsdObjSuppSize(pObj) > LutSize ); + If_DsdManGetSuppSizes( p, pObj, pSSizes ); + LimitOut = LutSize - (nSuppAll - pObj->nSupp + 1); + assert( LimitOut < LutSize ); + Vec_IntForEachEntry( vSets, set, i ) + { + SizeIn = SizeOut = 0; + for ( v = 0; v < nFans; v++ ) + { + int Value = ((set >> (v << 1)) & 3); + if ( Value == 0 ) + SizeOut += pSSizes[v]; + else if ( Value == 1 ) + SizeIn += pSSizes[v]; + else if ( Value == 3 ) + { + SizeIn += pSSizes[v]; + SizeOut += pSSizes[v]; + } + else assert( Value == 0 ); + if ( SizeIn > LutSize || SizeOut > LimitOut ) + break; + } + if ( v == nFans ) + return set; + } + return 0; +} +int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize ) +{ + int fVerbose = 0; + If_DsdObj_t * pObj, * pTemp; int i, Mask; + pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) ); + if ( fVerbose ) + If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 ); + if ( If_DsdObjSuppSize(pObj) <= LutSize ) + { + if ( fVerbose ) + printf( " Trivial\n" ); + return 1; + } + If_DsdManCollect( p, pObj->Id, p->vNodes ); + If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) + if ( If_DsdObjSuppSize(pTemp) <= LutSize && If_DsdObjSuppSize(pObj) - If_DsdObjSuppSize(pTemp) <= LutSize - 1 ) + { + if ( fVerbose ) + printf( " Dec using node " ); + if ( fVerbose ) + If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 ); + return 1; + } + If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) + if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize ) + { + if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize)) ) + { + if ( fVerbose ) + printf( " " ); + if ( fVerbose ) + Abc_TtPrintBinary( (word *)&Mask, 4 ); + if ( fVerbose ) + printf( " Using multi-input AND/XOR node\n" ); + return 1; + } + } + If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) + if ( If_DsdObjType(pTemp) == IF_DSD_PRIME ) + { + if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize)) ) + { + if ( fVerbose ) + printf( " " ); + if ( fVerbose ) + Dau_DecPrintSet( Mask, If_DsdObjFaninNum(pTemp), 0 ); + if ( fVerbose ) + printf( " Using prime node\n" ); + return 1; + } + } + if ( fVerbose ) + printf( " UNDEC\n" ); + return 0; +} +int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize ) +{ + return 1; +} + +/**Function************************************************************* + Synopsis [Add the function to the DSD manager.] Description [] @@ -873,7 +1067,7 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char SeeAlso [] ***********************************************************************/ -int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm ) +int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct ) { word pCopy[DAU_MAX_WORD], * pRes; char pDsd[DAU_MAX_STR]; @@ -897,14 +1091,25 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char // If_DsdManPrint( p, NULL ); printf( "\n" ); printf( "Verification failed!\n" ); - Dau_DsdPrintFromTruth( pTruth, nLeaves ); printf( "\n" ); - Dau_DsdPrintFromTruth( pRes, nLeaves ); printf( "\n" ); - If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm ); + Dau_DsdPrintFromTruth( pTruth, nLeaves ); + Dau_DsdPrintFromTruth( pRes, nLeaves ); + If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 ); printf( "\n" ); } If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) ); + if ( pLutStruct ) + { + int LutSize = (int)(pLutStruct[0] - '0'); + assert( pLutStruct[2] == 0 ); + if ( If_DsdManCheckXY( p, iDsd, LutSize ) ) + If_DsdVecObjSetMark( p->vObjs, Abc_Lit2Var(iDsd) ); + } return iDsd; } +int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ) +{ + return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 529b8cb9..ae7552b3 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -84,7 +84,12 @@ If_Man_t * If_ManStart( If_Par_t * pPars ) p->puTemp[3] = p->puTemp[2] + p->nTruth6Words*2; p->puTempW = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words ) : NULL; if ( pPars->fUseDsd ) + { p->pIfDsdMan = If_DsdManAlloc( pPars->nLutSize ); + p->vDsds = Vec_IntAlloc( 1000 ); + Vec_IntPush( p->vDsds, 0 ); + Vec_IntPush( p->vDsds, 2 ); + } // create the constant node p->pConst1 = If_ManSetupObj( p ); p->pConst1->Type = IF_CONST1; @@ -165,9 +170,10 @@ void If_ManStop( If_Man_t * p ) Vec_WrdFreeP( &p->vAnds ); Vec_WrdFreeP( &p->vAndGate ); Vec_WrdFreeP( &p->vOrGate ); - if ( p->vObjsRev ) Vec_PtrFree( p->vObjsRev ); - if ( p->vLatchOrder ) Vec_PtrFree( p->vLatchOrder ); - if ( p->vLags ) Vec_IntFree( p->vLags ); + Vec_PtrFreeP( &p->vObjsRev ); + Vec_PtrFreeP( &p->vLatchOrder ); + Vec_IntFreeP( &p->vLags ); + Vec_IntFreeP( &p->vDsds ); Vec_MemHashFree( p->vTtMem ); Vec_MemFreeP( &p->vTtMem ); Mem_FixedStop( p->pMemObj, 0 ); diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index c22d8604..34e83139 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -217,6 +217,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep // abctime clk = Abc_Clock(); If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 ); // p->timeTruth += Abc_Clock() - clk; + // run user functions pCut->fUseless = 0; if ( p->pPars->pFuncCell ) { @@ -250,9 +251,26 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep p->nCuts5a++; } } + if ( p->pPars->fUseDsd ) + { + int truthId = Abc_Lit2Var(pCut->iCutFunc); + if ( Vec_IntSize(p->vDsds) <= truthId || Vec_IntEntry(p->vDsds, truthId) == -1 ) + { + pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct ); + while ( Vec_IntSize(p->vDsds) <= truthId ) + Vec_IntPush( p->vDsds, -1 ); + Vec_IntWriteEntry( p->vDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) ); + } + else + pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) ); + if ( p->pPars->pLutStruct ) + { + int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ); + if ( Value != (int)pCut->fUseless ) + printf( "Difference\n" ); + } + } } - if ( p->pPars->fUseDsd && Abc_Lit2Var(pCut->iCutFunc) == Vec_MemEntryNum(p->vTtMem)-1 ) - pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm ); // compute the application-specific cost and depth pCut->fUser = (p->pPars->pFuncCost != NULL); diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h index dab49bc3..2e56899b 100644 --- a/src/opt/dau/dau.h +++ b/src/opt/dau/dau.h @@ -97,6 +97,11 @@ extern void * Dsm_ManDeriveGia( void * p, int fUseMuxes ); extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches ); extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars ); +/*=== dauNonDsd.c ==========================================================*/ +extern Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars ); +extern void Dau_DecPrintSets( Vec_Int_t * vSets, int nVars ); +extern void Dau_DecPrintSet( unsigned set, int nVars, int fNewLine ); + /*=== dauTree.c ==========================================================*/ extern Dss_Man_t * Dss_ManAlloc( int nVars, int nNonDecLimit ); extern void Dss_ManFree( Dss_Man_t * p ); diff --git a/src/opt/dau/dauNonDsd.c b/src/opt/dau/dauNonDsd.c index e5cc58e1..53eafe92 100644 --- a/src/opt/dau/dauNonDsd.c +++ b/src/opt/dau/dauNonDsd.c @@ -459,7 +459,7 @@ void Dau_DecMoveFreeToLSB( word * p, int nVars, int * V2P, int * P2V, int maskB, Abc_TtMoveVar( p, nVars, V2P, P2V, v, c++ ); assert( c == nVars - sizeB ); } -Vec_Int_t * Dau_DecFindSets( word * p, int nVars ) +Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars ) { Vec_Int_t * vSets = Vec_IntAlloc( 32 ); int V2P[16], P2V[16], pVarsB[16]; @@ -467,6 +467,8 @@ Vec_Int_t * Dau_DecFindSets( word * p, int nVars ) int c, v, sizeB, sizeS, maskB, maskS; int * pSched[16] = {NULL}; unsigned setMixed; + word p[1<<10]; + memcpy( p, pInit, sizeof(word) * Abc_TtWordNum(nVars) ); for ( v = 0; v < nVars; v++ ) assert( Abc_TtHasVar( p, nVars, v ) ); for ( v = 2; v < nVars; v++ ) @@ -703,7 +705,7 @@ int Dau_DecVerify( word * pInit, int nVars, char * pDsdC, char * pDsdD ) printf( "\n" ); return 1; } -int Dau_DecPerform( word * p, int nVars, unsigned uSet ) +int Dau_DecPerform6( word * p, int nVars, unsigned uSet ) { word tComp = 0, tDec = 0, tDec0, tComp0, tComp1, FuncC, FuncD; char pDsdC[1000], pDsdD[1000]; @@ -760,7 +762,7 @@ int Dau_DecPerform( word * p, int nVars, unsigned uSet ) return 1; } -int Dau_DecPerform2( word * pInit, int nVars, unsigned uSet ) +int Dau_DecPerform( word * pInit, int nVars, unsigned uSet ) { word p[1<<10], pDec[1<<10], pComp[1<<10]; // at most 2^10 words char pDsdC[5000], pDsdD[5000]; // at most 2^12 hex digits @@ -820,15 +822,18 @@ int Dau_DecPerform2( word * pInit, int nVars, unsigned uSet ) Dau_DecVerify( pInit, nVars, pDsdC, pDsdD ); return 1; } -void Dau_DecTrySets( word * pInit, int nVars ) +void Dau_DecTrySets( word * pInit, int nVars, int fVerbose ) { - word p[1<<10]; Vec_Int_t * vSets; int i, Entry; assert( nVars <= 16 ); - memcpy( p, pInit, sizeof(word) * Abc_TtWordNum(nVars) ); - vSets = Dau_DecFindSets( p, nVars ); - Dau_DsdPrintFromTruth( p, nVars ); + vSets = Dau_DecFindSets( pInit, nVars ); + if ( !fVerbose ) + { + Vec_IntFree( vSets ); + return; + } + Dau_DsdPrintFromTruth( pInit, nVars ); printf( "This %d-variable function has %d decomposable variable sets:\n", nVars, Vec_IntSize(vSets) ); Vec_IntForEachEntry( vSets, Entry, i ) { @@ -837,12 +842,12 @@ void Dau_DecTrySets( word * pInit, int nVars ) if ( nVars > 6 ) { Dau_DecPrintSet( uSet, nVars, 0 ); - Dau_DecPerform2( pInit, nVars, uSet ); + Dau_DecPerform( pInit, nVars, uSet ); } else { Dau_DecPrintSet( uSet, nVars, 1 ); - Dau_DecPerform( pInit, nVars, uSet ); + Dau_DecPerform6( pInit, nVars, uSet ); } } Vec_IntFree( vSets ); @@ -860,7 +865,7 @@ void Dau_DecFindSetsTest3() // char * pStr = "Abcd"; // char * pStr = "ab"; unsigned uSet = Dau_DecReadSet( pStr ); - Dau_DecPerform( &t, nVars, uSet ); + Dau_DecPerform6( &t, nVars, uSet ); } void Dau_DecFindSetsTest() @@ -879,7 +884,7 @@ void Dau_DecFindSetsTest() // word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000 // word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e) // word t = ABC_CONST(0x7F00000000000000); // (!(abc)def) - Dau_DecTrySets( &t, nVars ); + Dau_DecTrySets( &t, nVars, 1 ); } |