From 83da5a038413b8062ec730eb87089e76834ec130 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 5 Nov 2015 20:37:08 -0800 Subject: Improvements to storing and reusing simulation info. --- src/opt/sfm/sfmDec.c | 119 ++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 98 insertions(+), 21 deletions(-) (limited to 'src/opt/sfm/sfmDec.c') diff --git a/src/opt/sfm/sfmDec.c b/src/opt/sfm/sfmDec.c index b12ed6e6..eb7dd1c1 100644 --- a/src/opt/sfm/sfmDec.c +++ b/src/opt/sfm/sfmDec.c @@ -82,8 +82,11 @@ struct Sfm_Dec_t_ Vec_Wrd_t vSets[2]; // onset/offset patterns int nPats[2]; // CEX count int nPatWords[2];// CEX words + int nDivWords; // div words + int nDivWordsAlloc; // div words word TtElems[SFM_SUPP_MAX][SFM_WORD_MAX]; word * pTtElems[SFM_SUPP_MAX]; + word * pDivWords[SFM_SUPP_MAX]; // temporary Vec_Int_t vTemp; Vec_Int_t vTemp2; @@ -159,7 +162,7 @@ void Sfm_ParSetDefault3( Sfm_Par_t * pPars ) memset( pPars, 0, sizeof(Sfm_Par_t) ); pPars->nTfoLevMax = 100; // the maximum fanout levels pPars->nTfiLevMax = 100; // the maximum fanin levels - pPars->nFanoutMax = 5; // the maximum number of fanoutsp + pPars->nFanoutMax = 10; // the maximum number of fanouts pPars->nMffcMin = 1; // the maximum MFFC size pPars->nMffcMax = 3; // the maximum MFFC size pPars->nVarMax = 6; // the maximum variable count @@ -233,6 +236,9 @@ void Sfm_DecStop( Sfm_Dec_t * p ) printf( "Level count mismatch at node %d.\n", i ); Sfm_LibStop( p->pLib ); if ( p->pTim ) Sfm_TimStop( p->pTim ); + // divisors + for ( i = 0; i < SFM_SUPP_MAX; i++ ) + ABC_FREE( p->pDivWords[i] ); // library Vec_IntErase( &p->vGateSizes ); Vec_WrdErase( &p->vGateFuncs ); @@ -352,11 +358,21 @@ static inline word Sfm_ObjFindCareSet( Abc_Ntk_t * pNtk, Vec_Int_t * vRoots ) } static inline void Sfm_ObjSetupSimInfo( Abc_Obj_t * pObj ) { - Sfm_Dec_t * p = Sfm_DecMan( pObj ); + Sfm_Dec_t * p = Sfm_DecMan( pObj ); int i; p->nPats[0] = p->nPats[1] = 0; p->nPatWords[0] = p->nPatWords[1] = 0; Vec_WrdFill( &p->vSets[0], p->nDivs*SFM_SIM_WORDS, 0 ); Vec_WrdFill( &p->vSets[1], p->nDivs*SFM_SIM_WORDS, 0 ); + // alloc divwords + p->nDivWords = Abc_Bit6WordNum( 4 * p->nDivs ); + if ( p->nDivWordsAlloc < p->nDivWords ) + { + p->nDivWordsAlloc = Abc_MaxInt( 16, p->nDivWords ); + for ( i = 0; i < SFM_SUPP_MAX; i++ ) + p->pDivWords[i] = ABC_REALLOC( word, p->pDivWords[i], p->nDivWordsAlloc ); + } + memset( p->pDivWords[0], 0, sizeof(word) * p->nDivWords ); + // collect simulation info if ( p->pPars->fUseSim && p->uCareSet != 0 ) { word uCareSet = p->uCareSet; @@ -565,6 +581,68 @@ void Sfm_DecPrint( Sfm_Dec_t * p, word Masks[2][SFM_SIM_WORDS] ) } } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sfm_DecVarCost( Sfm_Dec_t * p, word Masks[2][SFM_SIM_WORDS], int d, int Counts[2][2] ) +{ + int c; + for ( c = 0; c < 2; c++ ) + { + word * pPats = Sfm_DecDivPats( p, d, c ); + int Num = Abc_TtCountOnesVec( Masks[c], p->nPatWords[c] ); + Counts[c][1] = Abc_TtCountOnesVecMask( pPats, Masks[c], p->nPatWords[c], 0 ); + Counts[c][0] = Num - Counts[c][1]; + assert( Counts[c][0] >= 0 && Counts[c][1] >= 0 ); + } + //printf( "%5d %5d %5d %5d \n", Counts[0][0], Counts[0][1], Counts[1][0], Counts[1][1] ); +} +int Sfm_DecFindBestVar2( Sfm_Dec_t * p, word Masks[2][SFM_SIM_WORDS] ) +{ + int Counts[2][2]; + int d, VarBest = -1, CostBest = ABC_INFINITY, Cost; + for ( d = 0; d < p->nDivs; d++ ) + { + Sfm_DecVarCost( p, Masks, d, Counts ); + if ( (Counts[0][0] < Counts[0][1]) == (Counts[1][0] < Counts[1][1]) ) + continue; + Cost = Abc_MinInt(Counts[0][0], Counts[0][1]) + Abc_MinInt(Counts[1][0], Counts[1][1]); + if ( CostBest > Cost ) + { + CostBest = Cost; + VarBest = d; + } + } + return VarBest; +} +int Sfm_DecFindBestVar( Sfm_Dec_t * p, word Masks[2][SFM_SIM_WORDS] ) +{ + int c, i, iLit, Var = -1, Cost, CostMin = ABC_INFINITY; + for ( c = 0; c < 2; c++ ) + { + Vec_IntForEachEntry( &p->vImpls[c], iLit, i ) + { + if ( Vec_IntSize(&p->vImpls[c]) > 1 && Vec_IntFind(&p->vObjDec, Abc_Lit2Var(iLit)) >= 0 ) + continue; + Cost = Sfm_DecFindCost( p, c, iLit, Masks[!c] ); + if ( CostMin > Cost ) + { + CostMin = Cost; + Var = Abc_Lit2Var(iLit); + } + } + } + return Var; +} + /**Function************************************************************* Synopsis [] @@ -710,8 +788,8 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu { int nBTLimit = p->pPars->nBTLimit; // int fVerbose = p->pPars->fVeryVerbose; - int Var = -1, CostMin = ABC_INFINITY; - int c, i, d, iLit, Cost, status; + int c, i, d, iLit, status, Var = -1; + word * pDivWords = p->pDivWords[nAssump]; abctime clk; assert( nAssump <= SFM_SUPP_MAX ); if ( p->pPars->fVeryVerbose ) @@ -786,11 +864,19 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu int fHas1s = Abc_TtIntersect( pPats, Masks[c], p->nPatWords[c], 0 ); if ( fHas0s && fHas1s ) continue; - p->nSatCalls++; pAssump[nAssump] = Abc_Var2Lit( p->iTarget, c ); pAssump[nAssump+1] = Abc_Var2Lit( d, fHas1s ); // if there are 1s, check if 0 is SAT clk = Abc_Clock(); - status = sat_solver_solve( p->pSat, pAssump, pAssump + nAssump + 2, nBTLimit, 0, 0, 0 ); + if ( Abc_TtGetBit( pDivWords, 4*d+2*c+fHas1s ) ) + { + p->nSatCallsUnsat--; + status = l_False; + } + else + { + p->nSatCalls++; + status = sat_solver_solve( p->pSat, pAssump, pAssump + nAssump + 2, nBTLimit, 0, 0, 0 ); + } if ( status == l_Undef ) { p->nTimeOuts++; @@ -802,6 +888,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu p->timeSatUnsat += Abc_Clock() - clk; Impls[c] = Abc_LitNot(pAssump[nAssump+1]); Vec_IntPush( &p->vImpls[c], Abc_LitNot(pAssump[nAssump+1]) ); + Abc_TtSetBit( pDivWords, 4*d+2*c+fHas1s ); continue; } assert( status == l_True ); @@ -914,20 +1001,9 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu // find the best cofactoring variable // if ( !fCofactor || Vec_IntSize(&p->vImpls[0]) + Vec_IntSize(&p->vImpls[1]) > 2 ) - for ( c = 0; c < 2; c++ ) - { - Vec_IntForEachEntry( &p->vImpls[c], iLit, i ) - { - if ( Vec_IntSize(&p->vImpls[c]) > 1 && Vec_IntFind(&p->vObjDec, Abc_Lit2Var(iLit)) >= 0 ) - continue; - Cost = Sfm_DecFindCost( p, c, iLit, Masks[!c] ); - if ( CostMin > Cost ) - { - CostMin = Cost; - Var = Abc_Lit2Var(iLit); - } - } - } + Var = Sfm_DecFindBestVar( p, Masks ); +// if ( Var == -1 ) +// Var = Sfm_DecFindBestVar2( p, Masks ); /* { @@ -962,7 +1038,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu if ( p->pPars->fVeryVerbose ) { Sfm_DecPrint( p, Masks ); - printf( "Best var %d with weight %d. Cofactored = %s\n", Var, CostMin, Var == p->nDivs - 1 ? "yes" : "no" ); + printf( "Best var %d\n", Var ); printf( "\n" ); } cofactor: @@ -981,6 +1057,7 @@ cofactor: MasksNext[c][w] = 0; } pAssump[nAssump] = Abc_Var2Lit( Var, !i ); + memcpy( p->pDivWords[nAssump+1], p->pDivWords[nAssump], sizeof(word) * p->nDivWords ); nSupp[i] = Sfm_DecPeformDec_rec( p, uTruth[i], Supp[i], pAssump, nAssump+1, MasksNext, fCofactor, (i ? nSupp[0] : 0) + nSuppAdd + 1 ); if ( nSupp[i] == -2 ) return -2; -- cgit v1.2.3