From c1670d7444f040984fc0f4cca5d0c8c3bc5bb2e2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 3 Apr 2014 13:52:13 -0700 Subject: Improvements to technology mapping. --- src/map/if/if.h | 7 ++++--- src/map/if/ifCut.c | 2 +- src/map/if/ifDsd.c | 41 +++++++++++++++++------------------------ src/map/if/ifMan.c | 26 ++++++++++++++++++-------- src/map/if/ifMap.c | 19 ++++++++++--------- 5 files changed, 50 insertions(+), 45 deletions(-) (limited to 'src/map') diff --git a/src/map/if/if.h b/src/map/if/if.h index 2d1351b4..273119c0 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -233,10 +233,10 @@ struct If_Man_t_ int nCutsCountAll; int nCutsUselessAll; int nCuts5, nCuts5a; - Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table If_DsdMan_t * pIfDsdMan; // DSD manager - Vec_Int_t * vTtDsds; // mapping of truth table into DSD - Vec_Str_t * vTtPerms; // mapping of truth table into permutations + Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table + Vec_Int_t * vTtDsds[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into DSD + Vec_Str_t * vTtPerms[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into permutations Hash_IntMan_t * vPairHash; // hashing pairs of truth tables Vec_Int_t * vPairRes; // resulting truth table Vec_Str_t * vPairPerms; // resulting permutation @@ -543,6 +543,7 @@ extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLe extern char * If_DsdManFileName( If_DsdMan_t * p ); extern int If_DsdManVarNum( If_DsdMan_t * p ); extern int If_DsdManLutSize( If_DsdMan_t * p ); +extern int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd ); extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ); extern unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fHighEffort, int fVerbose ); /*=== ifLib.c =============================================================*/ diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c index d7166baf..6715f706 100644 --- a/src/map/if/ifCut.c +++ b/src/map/if/ifCut.c @@ -859,7 +859,7 @@ void If_CutPrint( If_Cut_t * pCut ) unsigned i; Abc_Print( 1, "{" ); for ( i = 0; i < pCut->nLeaves; i++ ) - Abc_Print( 1, " %s%d", ((pCut->iCutDsd >> i) & 1) ? "!":"", pCut->pLeaves[i] ); + Abc_Print( 1, " %s%d", If_CutLeafBit(pCut, i) ? "!":"", pCut->pLeaves[i] ); Abc_Print( 1, " }\n" ); } diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index ac324d13..cb1e3bd7 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -150,6 +150,10 @@ int If_DsdManLutSize( If_DsdMan_t * p ) { return p->LutSize; } +int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd ) +{ + return If_DsdVecLitSuppSize( &p->vObjs, iDsd ); +} int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ) { return If_DsdVecObjMark( &p->vObjs, Abc_Lit2Var(iDsd) ); @@ -845,10 +849,10 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word { int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem[nLits], pTruth) : -1; unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId ); -abctime clk; +//abctime clk; if ( *pSpot ) return (int)*pSpot; -clk = Abc_Clock(); +//clk = Abc_Clock(); if ( p->LutSize && truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs[nLits]) ) { Vec_Int_t * vSets = Dau_DecFindSets_int( pTruth, nLits, p->pSched ); @@ -863,7 +867,7 @@ clk = Abc_Clock(); // printf( "%d ", Gia_ManAndNum(p->pTtGia)-nObjOld ); Gia_ManAppendCo( p->pTtGia, Lit ); } -p->timeCheck += Abc_Clock() - clk; +//p->timeCheck += Abc_Clock() - clk; *pSpot = Vec_PtrSize( &p->vObjs ); objId = If_DsdObjCreate( p, Type, pLits, nLits, truthId ); if ( Vec_PtrSize(&p->vObjs) > p->nBins ) @@ -1661,13 +1665,6 @@ unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDeri { If_DsdObj_t * pObj, * pTemp; int i, Mask, iFirst; -/* - if ( 193 == iDsd ) - { - int s = 0; - If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 ); - } -*/ pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsd) ); if ( fVerbose ) If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 ); @@ -1740,7 +1737,7 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uSet = If_DsdManCheckXY_int( p, iDsd, LutSize, fDerive, fVerbose ); if ( uSet == 0 && fHighEffort ) { - abctime clk = Abc_Clock(); +// abctime clk = Abc_Clock(); int nVars = If_DsdVecLitSuppSize( &p->vObjs, iDsd ); word * pRes = If_DsdManComputeTruth( p, iDsd, NULL ); uSet = If_ManSatCheckXYall( p->pSat, LutSize, pRes, nVars, p->vTemp1 ); @@ -1749,8 +1746,7 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, // If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 ); // Dau_DecPrintSet( uSet, nVars, 1 ); } -// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - p->timeCheck2 += Abc_Clock() - clk; +// p->timeCheck2 += Abc_Clock() - clk; } return uSet; } @@ -1788,27 +1784,23 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char char pDsd[DAU_MAX_STR]; int iDsd, nSizeNonDec, nSupp = 0; int nWords = Abc_TtWordNum(nLeaves); - abctime clk; + abctime clk = 0; assert( nLeaves <= DAU_MAX_VAR ); Abc_TtCopy( pCopy, pTruth, nWords, 0 ); -clk = Abc_Clock(); +//clk = Abc_Clock(); nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 1, pDsd ); -p->timeDsd += Abc_Clock() - clk; -// if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") ) -// { -// int x = 0; -// } +//p->timeDsd += Abc_Clock() - clk; if ( nSizeNonDec > 0 ) Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars ); memset( pPerm, 0xFF, nLeaves ); -clk = Abc_Clock(); +//clk = Abc_Clock(); iDsd = If_DsdManAddDsd( p, pDsd, pCopy, pPerm, &nSupp ); -p->timeCanon += Abc_Clock() - clk; +//p->timeCanon += Abc_Clock() - clk; assert( nSupp == nLeaves ); // verify the result -clk = Abc_Clock(); +//clk = Abc_Clock(); pRes = If_DsdManComputeTruth( p, iDsd, pPerm ); -p->timeVerify += Abc_Clock() - clk; +//p->timeVerify += Abc_Clock() - clk; if ( !Abc_TtEqual(pRes, pTruth, nWords) ) { // If_DsdManPrint( p, NULL ); @@ -1821,6 +1813,7 @@ p->timeVerify += Abc_Clock() - clk; printf( "\n" ); } If_DsdVecObjIncRef( &p->vObjs, Abc_Lit2Var(iDsd) ); + assert( If_DsdVecLitSuppSize(&p->vObjs, iDsd) == nLeaves ); return iDsd; } diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 7874d7e0..7e52650d 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -92,12 +92,20 @@ If_Man_t * If_ManStart( If_Par_t * pPars ) p->puTempW = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words[p->pPars->nLutSize] ) : NULL; if ( pPars->fUseDsd ) { - p->vTtDsds = Vec_IntAlloc( 1000 ); - Vec_IntPush( p->vTtDsds, 0 ); - Vec_IntPush( p->vTtDsds, 2 ); - p->vTtPerms = Vec_StrAlloc( 10000 ); - Vec_StrFill( p->vTtPerms, 2 * p->pPars->nLutSize, IF_BIG_CHAR ); - Vec_StrWriteEntry( p->vTtPerms, p->pPars->nLutSize, 0 ); + for ( v = 6; v <= p->pPars->nLutSize; v++ ) + { + p->vTtDsds[v] = Vec_IntAlloc( 1000 ); + Vec_IntPush( p->vTtDsds[v], 0 ); + Vec_IntPush( p->vTtDsds[v], 2 ); + p->vTtPerms[v] = Vec_StrAlloc( 10000 ); + Vec_StrFill( p->vTtPerms[v], 2 * v, IF_BIG_CHAR ); + Vec_StrWriteEntry( p->vTtPerms[v], v, 0 ); + } + for ( v = 0; v < 6; v++ ) + { + p->vTtDsds[v] = p->vTtDsds[6]; + p->vTtPerms[v] = p->vTtPerms[6]; + } } if ( pPars->fUseTtPerm ) { @@ -204,8 +212,10 @@ void If_ManStop( If_Man_t * p ) Vec_PtrFreeP( &p->vObjsRev ); Vec_PtrFreeP( &p->vLatchOrder ); Vec_IntFreeP( &p->vLags ); - Vec_IntFreeP( &p->vTtDsds ); - Vec_StrFreeP( &p->vTtPerms ); + for ( i = 6; i <= p->pPars->nLutSize; i++ ) + Vec_IntFreeP( &p->vTtDsds[i] ); + for ( i = 6; i <= p->pPars->nLutSize; i++ ) + Vec_StrFreeP( &p->vTtPerms[i] ); Vec_IntFreeP( &p->vCutData ); Vec_IntFreeP( &p->vPairRes ); Vec_StrFreeP( &p->vPairPerms ); diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index f04cb201..b3bc4b70 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -208,24 +208,25 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep { extern void If_ManCacheRecord( If_Man_t * p, int iDsd0, int iDsd1, int nShared, int iDsd ); int truthId = Abc_Lit2Var(pCut->iCutFunc); - if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 ) + if ( Vec_IntSize(p->vTtDsds[pCut->nLeaves]) <= truthId || Vec_IntEntry(p->vTtDsds[pCut->nLeaves], 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->vTtDsds) <= truthId ) + while ( Vec_IntSize(p->vTtDsds[pCut->nLeaves]) <= truthId ) { - Vec_IntPush( p->vTtDsds, -1 ); - for ( v = 0; v < p->pPars->nLutSize; v++ ) - Vec_StrPush( p->vTtPerms, IF_BIG_CHAR ); + Vec_IntPush( p->vTtDsds[pCut->nLeaves], -1 ); + for ( v = 0; v < Abc_MaxInt(6, pCut->nLeaves); v++ ) + Vec_StrPush( p->vTtPerms[pCut->nLeaves], IF_BIG_CHAR ); } - Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) ); + Vec_IntWriteEntry( p->vTtDsds[pCut->nLeaves], truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) ); for ( v = 0; v < (int)pCut->nLeaves; v++ ) - Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] ); + Vec_StrWriteEntry( p->vTtPerms[pCut->nLeaves], truthId * Abc_MaxInt(6, pCut->nLeaves) + v, (char)pCut->pPerm[v] ); } else { - pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) ); + pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds[pCut->nLeaves], truthId), Abc_LitIsCompl(pCut->iCutFunc) ); for ( v = 0; v < (int)pCut->nLeaves; v++ ) - pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v ); + pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms[pCut->nLeaves], truthId * Abc_MaxInt(6, pCut->nLeaves) + v ); +// assert( If_DsdManSuppSize(p->pIfDsdMan, pCut->iCutDsd) == (int)pCut->nLeaves ); } // If_ManCacheRecord( p, pCut0->iCutDsd, pCut1->iCutDsd, nShared, pCut->iCutDsd ); } -- cgit v1.2.3