diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-19 23:49:41 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-19 23:49:41 -0800 |
commit | 7e0f7eba792e7fc854345d45f6f49bb562e63d3a (patch) | |
tree | ebe90c25e7ad750bfcbd2b5ed980b17e5783a874 /src | |
parent | 6ad7dae1aefdecbe4cdc4f4f80548004f86af451 (diff) | |
download | abc-7e0f7eba792e7fc854345d45f6f49bb562e63d3a.tar.gz abc-7e0f7eba792e7fc854345d45f6f49bb562e63d3a.tar.bz2 abc-7e0f7eba792e7fc854345d45f6f49bb562e63d3a.zip |
Changes to LUT mappers.
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaJf.c | 25 | ||||
-rw-r--r-- | src/map/if/if.h | 1 | ||||
-rw-r--r-- | src/map/if/ifDsd.c | 370 | ||||
-rw-r--r-- | src/map/if/ifMan.c | 3 | ||||
-rw-r--r-- | src/misc/vec/vecMem.h | 11 |
5 files changed, 247 insertions, 163 deletions
diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c index 0e737adc..04dfb719 100644 --- a/src/aig/gia/giaJf.c +++ b/src/aig/gia/giaJf.c @@ -371,16 +371,7 @@ Jf_Man_t * Jf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars ) p->pGia = pGia; p->pPars = pPars; if ( pPars->fCutMin && !pPars->fFuncDsd ) - { - word uTruth[JF_WORD_MAX]; - int Value, nWords = Abc_Truth6WordNum(pPars->nLutSize); - p->vTtMem = Vec_MemAlloc( nWords, 12 ); // 32 KB/page for 6-var functions - Vec_MemHashAlloc( p->vTtMem, 10000 ); - memset( uTruth, 0x00, sizeof(word) * nWords ); - Value = Vec_MemHashInsert( p->vTtMem, uTruth ); assert( Value == 0 ); - memset( uTruth, 0xAA, sizeof(word) * nWords ); - Value = Vec_MemHashInsert( p->vTtMem, uTruth ); assert( Value == 1 ); - } + p->vTtMem = Vec_MemAllocForTT( pPars->nLutSize ); else if ( pPars->fCutMin && pPars->fFuncDsd ) { p->pDsd = Sdm_ManRead(); @@ -401,18 +392,6 @@ Jf_Man_t * Jf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars ) p->clkStart = Abc_Clock(); return p; } -void Jf_ManDumpTruthTables( Jf_Man_t * p ) -{ - char pFileName[1000]; - FILE * pFile; - sprintf( pFileName, "tt_%s_%02d.txt", Gia_ManName(p->pGia), p->pPars->nLutSize ); - pFile = fopen( pFileName, "wb" ); - Vec_MemDump( pFile, p->vTtMem ); - fclose( pFile ); - printf( "Dumped %d %d-var truth tables into file \"%s\" (%.2f MB).\n", - Vec_MemEntryNum(p->vTtMem), p->pPars->nLutSize, pFileName, - 17.0 * Vec_MemEntryNum(p->vTtMem) / (1 << 20) ); -} void Jf_ManFree( Jf_Man_t * p ) { if ( p->pPars->fVerbose && p->pDsd ) @@ -1748,7 +1727,7 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) Jf_ManPropagateEla( p, 1 ); Jf_ManPrintStats( p, "Edge " ); } if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && !p->pPars->fFuncDsd ) - Jf_ManDumpTruthTables( p ); + Vec_MemDumpTruthTables( p->vTtMem, Gia_ManName(p->pGia), p->pPars->nLutSize ); if ( p->pPars->fPureAig ) pNew = Jf_ManDeriveGia(p); else if ( p->pPars->fCutMin ) diff --git a/src/map/if/if.h b/src/map/if/if.h index 205ff9e3..37728fcb 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -515,6 +515,7 @@ extern int If_CluCheckExt3( void * p, word * pTruth, int nVars, int char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 ); /*=== ifDsd.c =============================================================*/ 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 ); extern void If_DsdManFree( If_DsdMan_t * p ); extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm ); diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index 502c6000..923e188a 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -43,11 +43,8 @@ struct If_DsdObj_t_ { unsigned Id; // node ID unsigned Type : 3; // node type - unsigned nSupp : 8; // variable - unsigned iVar : 8; // variable - unsigned nWords : 6; // variable - unsigned fMark0 : 1; // user mark - unsigned fMark1 : 1; // user mark + unsigned nSupp : 5; // variable + unsigned Count : 19; // variable unsigned nFans : 5; // fanin count unsigned pFans[0]; // fanins }; @@ -92,6 +89,8 @@ static inline If_DsdObj_t * If_DsdVecConst0( Vec_Ptr_t * p ) static inline If_DsdObj_t * If_DsdVecVar( Vec_Ptr_t * p, int v ) { return If_DsdVecObj( p, v+1 ); } 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 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])); } #define If_DsdVecForEachObj( vVec, pObj, i ) \ @@ -106,6 +105,7 @@ static inline If_DsdObj_t * If_DsdObjFanin( Vec_Ptr_t * p, If_DsdObj_t * pObj, i #define If_DsdObjForEachFaninLit( vVec, pObj, iLit, i ) \ for ( i = 0; (i < If_DsdObjFaninNum(pObj)) && ((iLit) = If_DsdObjFaninLit(pObj, i)); i++ ) +extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -184,9 +184,8 @@ If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans ) If_DsdObjClean( pObj ); pObj->Type = Type; pObj->nFans = nFans; - pObj->nWords = nWords; pObj->Id = Vec_PtrSize( p->vObjs ); - pObj->iVar = 31; + pObj->Count = 0; Vec_PtrPush( p->vObjs, pObj ); Vec_IntPush( p->vNexts, 0 ); return pObj; @@ -275,6 +274,9 @@ If_DsdMan_t * If_DsdManAlloc( int nVars ) void If_DsdManFree( If_DsdMan_t * p ) { int fVerbose = 0; +// If_DsdManDump( p ); + If_DsdManPrint( p, NULL ); + Vec_MemDumpTruthTables( p->vTtMem, NULL, p->nVars ); if ( fVerbose ) { Abc_PrintTime( 1, "Time begin ", p->timeBeg ); @@ -292,7 +294,23 @@ void If_DsdManFree( If_DsdMan_t * p ) ABC_FREE( p->pBins ); ABC_FREE( p ); } -void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, int * pPermLits, int * pnSupp ) +int If_DsdManCheckNonDec_rec( If_DsdMan_t * p, int Id ) +{ + If_DsdObj_t * pObj; + int i, iFanin; + pObj = If_DsdVecObj( p->vObjs, Id ); + if ( If_DsdObjType(pObj) == IF_DSD_CONST0 ) + return 0; + if ( If_DsdObjType(pObj) == IF_DSD_VAR ) + return 0; + if ( If_DsdObjType(pObj) == IF_DSD_PRIME ) + return 1; + If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) + if ( If_DsdManCheckNonDec_rec( p, Abc_Lit2Var(iFanin) ) ) + return 1; + return 0; +} +void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, unsigned char * pPermLits, int * pnSupp ) { char OpenType[7] = {0, 0, 0, '(', '[', '<', '{'}; char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'}; @@ -304,7 +322,7 @@ void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, int * pPerm { fprintf( pFile, "0" ); return; } if ( If_DsdObjType(pObj) == IF_DSD_VAR ) { - int iPermLit = pPermLits ? pPermLits[(*pnSupp)++] : Abc_Var2Lit((*pnSupp)++, 0); + int iPermLit = pPermLits ? (int)pPermLits[(*pnSupp)++] : Abc_Var2Lit((*pnSupp)++, 0); fprintf( pFile, "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) ); return; } @@ -312,62 +330,19 @@ void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, int * pPerm Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), If_DsdObjFaninNum(pObj) ); fprintf( pFile, "%c", OpenType[If_DsdObjType(pObj)] ); If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) - { - fprintf( pFile, "%s", Abc_LitIsCompl(iFanin) ? "!":"" ); - If_DsdManPrint_rec( pFile, p, Abc_Lit2Var(iFanin), pPermLits, pnSupp ); - } + 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, int * pPermLits ) +void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char * pPermLits ) { 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" ); assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, iObjId) ); } -int If_DsdManCheckNonDec_rec( If_DsdMan_t * p, int iObj ) -{ - If_DsdObj_t * pObj; - int i, iFanin; - assert( !Abc_LitIsCompl(iObj) ); - pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iObj) ); - if ( If_DsdObjType(pObj) == IF_DSD_CONST0 ) - return 0; - if ( If_DsdObjType(pObj) == IF_DSD_VAR ) - return 0; - if ( If_DsdObjType(pObj) == IF_DSD_PRIME ) - return 1; - If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) - if ( If_DsdManCheckNonDec_rec( p, iFanin ) ) - return 1; - return 0; -} -void If_DsdManDump( If_DsdMan_t * p ) -{ - char * pFileName = "dss_tts.txt"; - FILE * pFile; - If_DsdObj_t * pObj; - int i; - pFile = fopen( pFileName, "wb" ); - if ( pFile == NULL ) - { - printf( "Cannot open file \"%s\".\n", pFileName ); - return; - } - If_DsdVecForEachObj( p->vObjs, pObj, i ) - { - if ( If_DsdObjType(pObj) != IF_DSD_PRIME ) - continue; - fprintf( pFile, "0x" ); - Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), p->nVars ); - fprintf( pFile, "\n" ); -// printf( " " ); -// If_DsdPrintFromTruth( stdout, If_DsdObjTruth(p, pObj), p->nVars ); - } - fclose( pFile ); -} void If_DsdManPrint( If_DsdMan_t * p, char * pFileName ) { If_DsdObj_t * pObj; @@ -383,7 +358,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName ) If_DsdVecForEachObj( p->vObjs, pObj, i ) { CountNonDsd += (If_DsdObjType(pObj) == IF_DSD_PRIME); - CountNonDsdStr += If_DsdManCheckNonDec_rec( p, Abc_Var2Lit(pObj->Id, 0) ); + CountNonDsdStr += If_DsdManCheckNonDec_rec( p, pObj->Id ); } 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 ); @@ -399,14 +374,39 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName ) // return; If_DsdVecForEachObj( p->vObjs, pObj, i ) { - if ( i == 50 ) - break; +// if ( i == 50 ) +// break; If_DsdManPrintOne( pFile, p, pObj->Id, NULL ); } fprintf( pFile, "\n" ); if ( pFileName ) fclose( pFile ); } +void If_DsdManDump( If_DsdMan_t * p ) +{ + char * pFileName = "dss_tts.txt"; + FILE * pFile; + If_DsdObj_t * pObj; + int i; + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\".\n", pFileName ); + return; + } + If_DsdVecForEachObj( p->vObjs, pObj, i ) + { + if ( If_DsdObjType(pObj) != IF_DSD_PRIME ) + continue; + fprintf( pFile, "0x" ); + Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), p->nVars ); + fprintf( pFile, "\n" ); + printf( " " ); + Kit_DsdPrintFromTruth( (unsigned *)If_DsdObjTruth(p, pObj), p->nVars ); + printf( "\n" ); + } + fclose( pFile ); +} /**Function************************************************************* @@ -568,17 +568,82 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi SeeAlso [] ***********************************************************************/ -int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth ) +int If_DsdManOperation2( If_DsdMan_t * p, int Type, int * pLits, int nLits ) { - If_DsdObj_t * pObj, * pFanin; + If_DsdObj_t * pObj; int nChildren = 0, pChildren[DAU_MAX_VAR]; - int i, k, Id, iFanin, fComplFan, fCompl = 0; + int i, k, Id, iFanin, fCompl = 0; + if ( Type == IF_DSD_AND ) + { + for ( k = 0; k < nLits; k++ ) + { + pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) ); + if ( Abc_LitIsCompl(pLits[k]) || If_DsdObjType(pObj) != IF_DSD_AND ) + pChildren[nChildren++] = pLits[k]; + else + If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) + pChildren[nChildren++] = iFanin; + } + If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL ); + } + else if ( Type == IF_DSD_XOR ) + { + for ( k = 0; k < nLits; k++ ) + { + fCompl ^= Abc_LitIsCompl(pLits[k]); + pObj = If_DsdVecObj( p->vObjs, Abc_LitRegular(pLits[k]) ); + if ( If_DsdObjType(pObj) != IF_DSD_XOR ) + pChildren[nChildren++] = pLits[k]; + else + If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) + { + assert( !Abc_LitIsCompl(iFanin) ); + pChildren[nChildren++] = iFanin; + } + } + If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL ); + } + else if ( Type == IF_DSD_MUX ) + { + if ( Abc_LitIsCompl(pLits[0]) ) + { + pLits[0] = Abc_LitNot(pLits[0]); + ABC_SWAP( int, pLits[1], pLits[2] ); + } + if ( Abc_LitIsCompl(pLits[1]) ) + { + pLits[1] = Abc_LitNot(pLits[1]); + pLits[2] = Abc_LitNot(pLits[2]); + fCompl ^= 1; + } + for ( k = 0; k < nLits; k++ ) + pChildren[nChildren++] = pLits[k]; + } + else assert( 0 ); + // create new graph + Id = If_DsdObjFindOrAdd( p, Type, pChildren, nChildren, NULL ); + return Abc_Var2Lit( Id, fCompl ); +} + +/**Function************************************************************* + + Synopsis [Performs DSD operation.] + + Description [] + + SideEffects [] - assert( Type == IF_DSD_AND || pPerm == NULL ); - if ( Type == IF_DSD_AND && pPerm != NULL ) + SeeAlso [] + +***********************************************************************/ +int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth ) +{ + If_DsdObj_t * pObj, * pFanin; + unsigned char pPermNew[DAU_MAX_VAR]; + int nChildren = 0, pChildren[DAU_MAX_VAR], pBegEnd[DAU_MAX_VAR]; + int i, k, j, Id, iFanin, fComplFan, fCompl = 0, nSSize = 0; + if ( Type == IF_DSD_AND ) { - int pBegEnd[DAU_MAX_VAR]; - int j, nSSize = 0; for ( k = 0; k < nLits; k++ ) { pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) ); @@ -596,8 +661,8 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iFanin) ); fComplFan = If_DsdObjIsVar(pFanin) && Abc_LitIsCompl(iFanin); pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + pFanin->nSupp); - nSSize += pFanin->nSupp; pChildren[nChildren++] = Abc_LitNotCond( iFanin, fComplFan ); + nSSize += pFanin->nSupp; } } } @@ -605,59 +670,104 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig // create permutation for ( j = i = 0; i < nChildren; i++ ) for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ ) - pPerm[j++] = (unsigned char)Abc_Var2Lit( k, (pBegEnd[i] >> 8) & 1 ); + pPermNew[j++] = (unsigned char)Abc_LitNotCond( pPerm[k], (pBegEnd[i] >> 8) & 1 ); assert( j == nSSize ); - } - else if ( Type == IF_DSD_AND ) - { - for ( k = 0; k < nLits; k++ ) - { - pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) ); - if ( Abc_LitIsCompl(pLits[k]) || If_DsdObjType(pObj) != IF_DSD_AND ) - pChildren[nChildren++] = pLits[k]; - else - If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) - pChildren[nChildren++] = iFanin; - } - If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL ); + for ( j = 0; j < nSSize; j++ ) + pPerm[j] = pPermNew[j]; } else if ( Type == IF_DSD_XOR ) { + fComplFan = 0; for ( k = 0; k < nLits; k++ ) { fCompl ^= Abc_LitIsCompl(pLits[k]); - pObj = If_DsdVecObj( p->vObjs, Abc_LitRegular(pLits[k]) ); + pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) ); if ( If_DsdObjType(pObj) != IF_DSD_XOR ) - pChildren[nChildren++] = pLits[k]; + { + pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + pObj->nSupp); + pChildren[nChildren++] = Abc_LitRegular(pLits[k]); + nSSize += pObj->nSupp; + } else + { If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) { assert( !Abc_LitIsCompl(iFanin) ); - pChildren[nChildren++] = iFanin; + pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iFanin) ); + pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + pFanin->nSupp); + pChildren[nChildren++] = Abc_LitRegular(iFanin); + nSSize += pFanin->nSupp; } + } } - If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL ); + If_DsdObjSort( p->vObjs, pChildren, nChildren, pBegEnd ); + // create permutation + for ( j = i = 0; i < nChildren; i++ ) + for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ ) + pPermNew[j++] = (unsigned char)Abc_LitNotCond( pPerm[k], (pBegEnd[i] >> 8) & 1 ); + assert( j == nSSize ); + for ( j = 0; j < nSSize; j++ ) + pPerm[j] = pPermNew[j]; } else if ( Type == IF_DSD_MUX ) { - if ( Abc_LitIsCompl(pLits[0]) ) + for ( k = 0; k < nLits; k++ ) { - pLits[0] = Abc_LitNot(pLits[0]); - ABC_SWAP( int, pLits[1], pLits[2] ); + pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) ); + fComplFan = If_DsdObjIsVar(pFanin) && Abc_LitIsCompl(pLits[k]); + pChildren[nChildren++] = Abc_LitNotCond( pLits[k], fComplFan ); + pPerm[k] = (unsigned char)Abc_LitNotCond( (int)pPerm[k], fComplFan ); + nSSize += pFanin->nSupp; } - if ( Abc_LitIsCompl(pLits[1]) ) + if ( Abc_LitIsCompl(pChildren[0]) ) { - pLits[1] = Abc_LitNot(pLits[1]); - pLits[2] = Abc_LitNot(pLits[2]); + If_DsdObj_t * pFans[3]; + pChildren[0] = Abc_LitNot(pChildren[0]); + ABC_SWAP( int, pChildren[1], pChildren[2] ); + pFans[0] = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pChildren[0]) ); + pFans[1] = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pChildren[1]) ); + pFans[2] = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pChildren[2]) ); + nSSize = pFans[0]->nSupp + pFans[1]->nSupp + pFans[2]->nSupp; + for ( j = k = 0; k < If_DsdObjSuppSize(pFans[0]); k++ ) + pPermNew[j++] = pPerm[k]; + for ( k = 0; k < If_DsdObjSuppSize(pFans[2]); k++ ) + pPermNew[j++] = pPerm[pFans[0]->nSupp + pFans[1]->nSupp + k]; + for ( k = 0; k < If_DsdObjSuppSize(pFans[1]); k++ ) + pPermNew[j++] = pPerm[pFans[0]->nSupp + k]; + assert( j == nSSize ); + for ( j = 0; j < nSSize; j++ ) + pPerm[j] = pPermNew[j]; + } + if ( Abc_LitIsCompl(pChildren[1]) ) + { + pChildren[1] = Abc_LitNot(pChildren[1]); + pChildren[2] = Abc_LitNot(pChildren[2]); fCompl ^= 1; } - for ( k = 0; k < nLits; k++ ) - pChildren[nChildren++] = pLits[k]; } else if ( Type == IF_DSD_PRIME ) { - for ( k = 0; k < nLits; k++ ) - pChildren[nChildren++] = pLits[k]; + char pCanonPerm[DAU_MAX_VAR]; + int i, uCanonPhase, pFirsts[DAU_MAX_VAR]; + uCanonPhase = Abc_TtCanonicize( pTruth, nLits, pCanonPerm ); + fCompl = ((uCanonPhase >> nLits) & 1); + for ( i = 0; i < nLits; i++ ) + { + pFirsts[i] = nSSize; + nSSize += If_DsdVecLitSuppSize(p->vObjs, pLits[i]); + } + for ( j = i = 0; i < nLits; i++ ) + { + int iLitNew = Abc_LitNotCond( pLits[(int)pCanonPerm[i]], ((uCanonPhase>>i)&1) ); + pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iLitNew) ); + fComplFan = If_DsdObjIsVar(pFanin) && Abc_LitIsCompl(iLitNew); + pChildren[nChildren++] = Abc_LitNotCond( iLitNew, fComplFan ); + for ( k = 0; k < (int)pFanin->nSupp; k++ ) + pPermNew[j++] = (unsigned char)Abc_LitNotCond( (int)pPerm[pFirsts[(int)pCanonPerm[i]] + k], fComplFan ); + } + assert( j == nSSize ); + for ( j = 0; j < nSSize; j++ ) + pPerm[j] = pPermNew[j]; } else assert( 0 ); // create new graph @@ -665,7 +775,6 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig return Abc_Var2Lit( Id, fCompl ); } - /**Function************************************************************* Synopsis [Creating DSD network from SOP.] @@ -692,31 +801,25 @@ static inline void If_DsdMergeMatches( char * pDsd, int * pMatches ) } assert( nNested == 0 ); } -int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * pMan, word * pTruth, unsigned char * pPerm ) +int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * pMan, word * pTruth, unsigned char * pPerm, int * pnSupp ) { + unsigned char * pPermStart = pPerm + *pnSupp; int iRes = -1, fCompl = 0; if ( **p == '!' ) { fCompl = 1; (*p)++; } - while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') ) - (*p)++; -/* - if ( **p == '<' ) + assert( !((**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9')) ); + if ( **p >= 'a' && **p <= 'z' ) // var { - char * q = pStr + pMatches[ *p - pStr ]; - if ( *(q+1) == '{' ) - *p = q+1; + pPerm[(*pnSupp)++] = Abc_Var2Lit( **p - 'a', fCompl ); + return 2; } -*/ - if ( **p >= 'a' && **p <= 'z' ) // var - return Abc_Var2Lit( If_DsdObjId(If_DsdVecVar(pMan->vObjs, **p - 'a')), fCompl ); if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor { - int pLits[DAU_MAX_VAR], nLits = 0; + int Type, nLits = 0, pLits[DAU_MAX_VAR]; char * q = pStr + pMatches[ *p - pStr ]; - int Type; if ( **p == '(' ) Type = DAU_DSD_AND; else if ( **p == '[' ) @@ -728,28 +831,15 @@ int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * p else assert( 0 ); assert( *q == **p + 1 + (**p != '(') ); for ( (*p)++; *p < q; (*p)++ ) - pLits[nLits++] = If_DsdManAddDsd_rec( pStr, p, pMatches, pMan, pTruth, pPerm ); + pLits[nLits++] = If_DsdManAddDsd_rec( pStr, p, pMatches, pMan, pTruth, pPerm, pnSupp ); assert( *p == q ); - if ( Type == DAU_DSD_PRIME ) - { - word pTemp[DAU_MAX_WORD]; - char pCanonPerm[DAU_MAX_VAR]; - int i, uCanonPhase, pLitsNew[DAU_MAX_VAR]; - Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nLits), 0 ); - uCanonPhase = Abc_TtCanonicize( pTemp, nLits, pCanonPerm ); - fCompl = (uCanonPhase >> nLits) & 1; - for ( i = 0; i < nLits; i++ ) - pLitsNew[i] = Abc_LitNotCond( pLits[pCanonPerm[i]], (uCanonPhase>>i)&1 ); - iRes = If_DsdManOperation( pMan, Type, pLitsNew, nLits, pPerm, pTemp ); - } - else - iRes = If_DsdManOperation( pMan, Type, pLits, nLits, pPerm, pTruth ); + iRes = If_DsdManOperation( pMan, Type, pLits, nLits, pPermStart, pTruth ); return Abc_LitNotCond( iRes, fCompl ); } assert( 0 ); return -1; } -int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char * pPerm ) +int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char * pPerm, int * pnSupp ) { int iRes = -1, fCompl = 0; if ( *pDsd == '!' ) @@ -757,12 +847,15 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char if ( Dau_DsdIsConst(pDsd) ) iRes = 0; else if ( Dau_DsdIsVar(pDsd) ) - iRes = Dau_DsdReadVar(pDsd); + { + pPerm[(*pnSupp)++] = Dau_DsdReadVar(pDsd); + iRes = 2; + } else { int pMatches[DAU_MAX_STR]; If_DsdMergeMatches( pDsd, pMatches ); - iRes = If_DsdManAddDsd_rec( pDsd, &pDsd, pMatches, p, pTruth, pPerm ); + iRes = If_DsdManAddDsd_rec( pDsd, &pDsd, pMatches, p, pTruth, pPerm, pnSupp ); } return Abc_LitNotCond( iRes, fCompl ); } @@ -782,20 +875,33 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char { word pCopy[DAU_MAX_WORD], * pRes; char pDsd[DAU_MAX_STR]; - int i, iDsdFunc, nSizeNonDec; + int iDsd, nSizeNonDec, nSupp = 0; assert( nLeaves <= DAU_MAX_VAR ); Abc_TtCopy( pCopy, pTruth, p->nWords, 0 ); nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 0, pDsd ); + if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") ) + { +// int x = 0; + } if ( nSizeNonDec > 0 ) Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars ); - for ( i = 0; i < p->nVars; i++ ) - pPerm[i] = (char)i; - iDsdFunc = If_DsdManAddDsd( p, pDsd, pCopy, pPerm ); + memset( pPerm, 0xFF, nLeaves ); + iDsd = If_DsdManAddDsd( p, pDsd, pCopy, pPerm, &nSupp ); + assert( nSupp == nLeaves ); // verify the result - pRes = If_DsdManComputeTruth( p, iDsdFunc, pPerm ); + pRes = If_DsdManComputeTruth( p, iDsd, pPerm ); if ( !Abc_TtEqual(pRes, pTruth, p->nWords) ) + { +// If_DsdManPrint( p, NULL ); + printf( "\n" ); printf( "Verification failed!\n" ); - return iDsdFunc; + Kit_DsdPrintFromTruth( (unsigned *)pTruth, nLeaves ); printf( "\n" ); + Kit_DsdPrintFromTruth( (unsigned *)pRes, nLeaves ); printf( "\n" ); + If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm ); + printf( "\n" ); + } + If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) ); + return iDsd; } //////////////////////////////////////////////////////////////////////// diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index cd8d2688..529b8cb9 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -153,10 +153,7 @@ void If_ManStop( If_Man_t * p ) if ( p->pPars->fVerbose && p->nCuts5 ) Abc_Print( 1, "Statistics about 5-cuts: Total = %d Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 ); if ( p->pPars->fUseDsd ) - { - If_DsdManPrint( p->pIfDsdMan, NULL ); If_DsdManFree( p->pIfDsdMan ); - } // Abc_PrintTime( 1, "Truth", p->timeTruth ); // Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp ); Vec_IntFreeP( &p->vCoAttrs ); diff --git a/src/misc/vec/vecMem.h b/src/misc/vec/vecMem.h index 3f1b4517..206b42d2 100644 --- a/src/misc/vec/vecMem.h +++ b/src/misc/vec/vecMem.h @@ -281,7 +281,7 @@ static inline void Vec_MemDump( FILE * pFile, Vec_Mem_t * pVec ) word * pEntry; int i, w, d; if ( pFile == stdout ) - printf( "Memory vector has %d entries: ", Vec_MemEntryNum(pVec) ); + printf( "Memory vector has %d entries: \n", Vec_MemEntryNum(pVec) ); Vec_MemForEachEntry( pVec, pEntry, i ) { for ( w = pVec->nEntrySize - 1; w >= 0; w-- ) @@ -392,12 +392,13 @@ static inline void Vec_MemDumpTruthTables( Vec_Mem_t * p, char * pName, int nLut { FILE * pFile; char pFileName[1000]; - sprintf( pFileName, "tt_%s_%02d.txt", pName, nLutSize ); - pFile = fopen( pFileName, "wb" ); + sprintf( pFileName, "tt_%s_%02d.txt", pName ? pName : NULL, nLutSize ); + pFile = pName ? fopen( pFileName, "wb" ) : stdout; Vec_MemDump( pFile, p ); - fclose( pFile ); + if ( pFile != stdout ) + fclose( pFile ); printf( "Dumped %d %d-var truth tables into file \"%s\" (%.2f MB).\n", - Vec_MemEntryNum(p), nLutSize, pFileName, + Vec_MemEntryNum(p), nLutSize, pName ? pFileName : "stdout", 8.0 * Vec_MemEntryNum(p) * Vec_MemEntrySize(p) / (1 << 20) ); } |