From b2fd119933166ad7d9e4132ebb8aaf422bfcdb8a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 20 Nov 2012 21:34:40 -0800 Subject: DSD manager. --- src/map/if/if.h | 1 + src/map/if/ifCut.c | 2 +- src/map/if/ifMan.c | 3 ++- src/map/if/ifMap.c | 52 ++++++++++++++++++++++++++++------------------------ src/map/if/ifTruth.c | 2 ++ 5 files changed, 34 insertions(+), 26 deletions(-) (limited to 'src/map') diff --git a/src/map/if/if.h b/src/map/if/if.h index f1d78ff4..4505f6d4 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -98,6 +98,7 @@ struct If_Par_t_ int nFlowIters; // the number of iterations of area recovery int nAreaIters; // the number of iterations of area recovery int nGateSize; // the max size of the AND/OR gate to map into + int nNonDecLimit; // the max size of non-dec nodes float DelayTarget; // delay target float Epsilon; // value used in comparison floating point numbers int fPreprocess; // preprossing diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c index ca985910..ace197fb 100644 --- a/src/map/if/ifCut.c +++ b/src/map/if/ifCut.c @@ -856,7 +856,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut ) return; } - if ( (p->pPars->fUseBat || p->pPars->fEnableCheck07 || p->pPars->fEnableCheck08 || p->pPars->fEnableCheck10 || p->pPars->pLutStruct || p->pPars->fUserRecLib) && !pCut->fUseless ) + if ( (p->pPars->fUseDsd || p->pPars->fUseBat || p->pPars->fEnableCheck07 || p->pPars->fEnableCheck08 || p->pPars->fEnableCheck10 || p->pPars->pLutStruct || p->pPars->fUserRecLib) && !pCut->fUseless ) { If_Cut_t * pFirst = pCutSet->ppCuts[0]; if ( pFirst->fUseless || If_ManSortCompare(p, pFirst, pCut) == 1 ) diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 076f74d6..1cc92def 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -85,7 +85,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars ) { // p->pNamDsd = Abc_NamStart( 1000, 20 ); // p->iNamVar = Abc_NamStrFindOrAdd( p->pNamDsd, "a", NULL ); - p->pDsdMan = Dss_ManAlloc( pPars->nLutSize ); + p->pDsdMan = Dss_ManAlloc( pPars->nLutSize, pPars->nNonDecLimit ); p->iNamVar = 2; } @@ -165,6 +165,7 @@ void If_ManStop( If_Man_t * p ) // Abc_NamPrint( p->pNamDsd ); Abc_NamStop( p->pNamDsd ); */ + Dss_ManPrint( p->pDsdMan ); Dss_ManFree( p->pDsdMan ); } // Abc_PrintTime( 1, "Truth", p->timeTruth ); diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index ad50e1cc..ac606416 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -277,32 +277,36 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep } if ( p->pPars->fUseDsd ) { - int j, iDsd[2] = { Abc_LitNotCond(pCut0->iDsd, pObj->fCompl0), Abc_LitNotCond(pCut1->iDsd, pObj->fCompl1) }; - int nFans[2] = { pCut0->nLeaves, pCut1->nLeaves }; - int Fans[2][DAU_MAX_VAR], * pFans[2] = { Fans[0], Fans[1] }; -/* - char * pName = Dau_DsdMerge( - Abc_NamStr(p->pNamDsd, pCut0->iDsd), - If_CutPerm0(pCut, pCut0), - Abc_NamStr(p->pNamDsd, pCut1->iDsd), - If_CutPerm1(pCut, pCut1), - pObj->fCompl0, pObj->fCompl1, pCut->nLimit ); - pCut->iDsd = Abc_NamStrFindOrAdd( p->pNamDsd, pName, NULL ); -*/ - // create fanins - for ( j = 0; j < (int)pCut0->nLeaves; j++ ) - pFans[0][j] = Abc_Lit2Lit( p->pPerm[0], (int)pCut0->pPerm[j] ); - for ( j = 0; j < (int)pCut1->nLeaves; j++ ) - pFans[1][j] = Abc_Lit2Lit( p->pPerm[1], (int)pCut1->pPerm[j] ); - // canonicize - if ( iDsd[0] > iDsd[1] ) + if ( pCut0->iDsd < 0 || pCut1->iDsd < 0 ) + pCut->iDsd = -1; + else + { + int j, iDsd[2] = { Abc_LitNotCond(pCut0->iDsd, pObj->fCompl0), Abc_LitNotCond(pCut1->iDsd, pObj->fCompl1) }; + int nFans[2] = { pCut0->nLeaves, pCut1->nLeaves }; + int Fans[2][DAU_MAX_VAR], * pFans[2] = { Fans[0], Fans[1] }; + // create fanins + for ( j = 0; j < (int)pCut0->nLeaves; j++ ) + pFans[0][j] = Abc_Lit2Lit( p->pPerm[0], (int)pCut0->pPerm[j] ); + for ( j = 0; j < (int)pCut1->nLeaves; j++ ) + pFans[1][j] = Abc_Lit2Lit( p->pPerm[1], (int)pCut1->pPerm[j] ); + // canonicize + if ( iDsd[0] > iDsd[1] ) + { + ABC_SWAP( int, iDsd[0], iDsd[1] ); + ABC_SWAP( int, nFans[0], nFans[1] ); + ABC_SWAP( int *, pFans[0], pFans[1] ); + } + // derive new DSD + pCut->iDsd = Dss_ManMerge( p->pDsdMan, iDsd, nFans, pFans, p->uSharedMask, pCut->nLimit, pCut->pPerm, If_CutTruthW(pCut) ); + } + if ( pCut->iDsd < 0 ) { - ABC_SWAP( int, iDsd[0], iDsd[1] ); - ABC_SWAP( int, nFans[0], nFans[1] ); - ABC_SWAP( int *, pFans[0], pFans[1] ); + pCut->fUseless = 1; + p->nCutsUselessAll++; + p->nCutsUseless[pCut->nLeaves]++; } - // derive new DSD - pCut->iDsd = Dss_ManMerge( p->pDsdMan, iDsd, nFans, pFans, p->uSharedMask, pCut->nLimit, pCut->pPerm ); + p->nCutsCountAll++; + p->nCutsCount[pCut->nLeaves]++; } // compute the application-specific cost and depth diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c index 4c7a1d96..c86e4381 100644 --- a/src/map/if/ifTruth.c +++ b/src/map/if/ifTruth.c @@ -475,6 +475,7 @@ static inline int If_CutTruthMinimize6( If_Man_t * p, If_Cut_t * pCut ) // TEMPORARY if ( nSuppSize < 2 ) { +//printf( "Small supp\n" ); p->nSmallSupp++; return 2; } @@ -602,6 +603,7 @@ static inline int If_CutTruthMinimize2( If_Man_t * p, If_Cut_t * pCut ) // TEMPORARY if ( nSuppSize < 2 ) { +//printf( "Small supp\n" ); p->nSmallSupp++; return 2; } -- cgit v1.2.3