Skip to content

A
abc
Commit a3725e44 by Alan Mishchenko
Options

Improvements in delay optimization.

parent 229ee5df
Showing with 114 additions and 16 deletions
src/base/abci/abc.c
...@@ -5194,7 +5194,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5194,7 +5194,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults // set defaults
Sfm_ParSetDefault3( pPars ); Sfm_ParSetDefault3( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "IOVFKLHRMCNPWDarmzospdlvwh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "IOVFKLHRMCNPWDarmzoespdlvwh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -5370,6 +5370,9 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5370,6 +5370,9 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'o': case 'o':
pPars->fRrOnly ^= 1; pPars->fRrOnly ^= 1;
break; break;
case 'e':
pPars->fMoreEffort ^= 1;
break;
case 's': case 's':
pPars->fUseSim ^= 1; pPars->fUseSim ^= 1;
break; break;
...@@ -5409,7 +5412,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -5409,7 +5412,7 @@ int Abc_CommandMfs3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: mfs3 [-IOVFKLHRMCNPWD <num>] [-armzospdlvwh]\n" ); Abc_Print( -2, "usage: mfs3 [-IOVFKLHRMCNPWD <num>] [-armzoespdlvwh]\n" );
Abc_Print( -2, "\t performs don't-care-based optimization of mapped networks\n" ); Abc_Print( -2, "\t performs don't-care-based optimization of mapped networks\n" );
Abc_Print( -2, "\t-I <num> : the number of levels in the TFI cone (1 <= num) [default = %d]\n", pPars->nTfiLevMax ); Abc_Print( -2, "\t-I <num> : the number of levels in the TFI cone (1 <= num) [default = %d]\n", pPars->nTfiLevMax );
Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax ); Abc_Print( -2, "\t-O <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
...@@ -5430,6 +5433,7 @@ usage: ...@@ -5430,6 +5433,7 @@ usage:
Abc_Print( -2, "\t-m : toggle detecting multi-input AND/OR gates [default = %s]\n", pPars->fUseAndOr? "yes": "no" ); Abc_Print( -2, "\t-m : toggle detecting multi-input AND/OR gates [default = %s]\n", pPars->fUseAndOr? "yes": "no" );
Abc_Print( -2, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" ); Abc_Print( -2, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" );
Abc_Print( -2, "\t-o : toggle using old implementation for comparison [default = %s]\n", pPars->fRrOnly? "yes": "no" ); Abc_Print( -2, "\t-o : toggle using old implementation for comparison [default = %s]\n", pPars->fRrOnly? "yes": "no" );
Abc_Print( -2, "\t-e : toggle using more effort [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using simulation [default = %s]\n", pPars->fUseSim? "yes": "no" ); Abc_Print( -2, "\t-s : toggle using simulation [default = %s]\n", pPars->fUseSim? "yes": "no" );
Abc_Print( -2, "\t-p : toggle printing decompositions [default = %s]\n", pPars->fPrintDecs? "yes": "no" ); Abc_Print( -2, "\t-p : toggle printing decompositions [default = %s]\n", pPars->fPrintDecs? "yes": "no" );
Abc_Print( -2, "\t-d : toggle printing delay profile statistics [default = %s]\n", pPars->fDelayVerbose? "yes": "no" ); Abc_Print( -2, "\t-d : toggle printing delay profile statistics [default = %s]\n", pPars->fDelayVerbose? "yes": "no" );
src/opt/sfm/sfmDec.c
...@@ -58,6 +58,7 @@ struct Sfm_Dec_t_ ...@@ -58,6 +58,7 @@ struct Sfm_Dec_t_
int AreaMffc; // the area of gates in MFFC int AreaMffc; // the area of gates in MFFC
int DelayMin; // temporary min delay int DelayMin; // temporary min delay
int iTarget; // target node int iTarget; // target node
int iUseThis; // next cofactoring var to try
int DeltaCrit; // critical delta int DeltaCrit; // critical delta
int AreaInv; // inverter area int AreaInv; // inverter area
int DelayInv; // inverter delay int DelayInv; // inverter delay
...@@ -87,6 +88,8 @@ struct Sfm_Dec_t_ ...@@ -87,6 +88,8 @@ struct Sfm_Dec_t_
Vec_Int_t vTemp; Vec_Int_t vTemp;
Vec_Int_t vTemp2; Vec_Int_t vTemp2;
Vec_Int_t vCands; Vec_Int_t vCands;
word Copy[4];
int nSuppVars;
// statistics // statistics
abctime timeLib; abctime timeLib;
abctime timeWin; abctime timeWin;
...@@ -116,6 +119,7 @@ struct Sfm_Dec_t_ ...@@ -116,6 +119,7 @@ struct Sfm_Dec_t_
int nSatCallsOver; int nSatCallsOver;
int nTimeOuts; int nTimeOuts;
int nNoDecs; int nNoDecs;
int nEfforts;
int nMaxDivs; int nMaxDivs;
int nMaxWin; int nMaxWin;
word nAllDivs; word nAllDivs;
...@@ -166,6 +170,7 @@ void Sfm_ParSetDefault3( Sfm_Par_t * pPars ) ...@@ -166,6 +170,7 @@ void Sfm_ParSetDefault3( Sfm_Par_t * pPars )
pPars->DeltaCrit = 0; // delta delay in picoseconds pPars->DeltaCrit = 0; // delta delay in picoseconds
pPars->fUseAndOr = 0; // enable internal detection of AND/OR gates pPars->fUseAndOr = 0; // enable internal detection of AND/OR gates
pPars->fZeroCost = 0; // enable zero-cost replacement pPars->fZeroCost = 0; // enable zero-cost replacement
pPars->fMoreEffort = 0; // enables using more effort
pPars->fUseSim = 0; // enable simulation pPars->fUseSim = 0; // enable simulation
pPars->fArea = 0; // performs optimization for area pPars->fArea = 0; // performs optimization for area
pPars->fVerbose = 0; // enable basic stats pPars->fVerbose = 0; // enable basic stats
...@@ -226,6 +231,7 @@ p->timeLib = Abc_Clock() - p->timeLib; ...@@ -226,6 +231,7 @@ p->timeLib = Abc_Clock() - p->timeLib;
for ( i = 0; i < SFM_SUPP_MAX; i++ ) for ( i = 0; i < SFM_SUPP_MAX; i++ )
p->pTtElems[i] = p->TtElems[i]; p->pTtElems[i] = p->TtElems[i];
Abc_TtElemInit( p->pTtElems, SFM_SUPP_MAX ); Abc_TtElemInit( p->pTtElems, SFM_SUPP_MAX );
p->iUseThis = -1;
return p; return p;
} }
void Sfm_DecStop( Sfm_Dec_t * p ) void Sfm_DecStop( Sfm_Dec_t * p )
...@@ -913,7 +919,8 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu ...@@ -913,7 +919,8 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
{ {
int nBTLimit = p->pPars->nBTLimit; int nBTLimit = p->pPars->nBTLimit;
// int fVerbose = p->pPars->fVeryVerbose; // int fVerbose = p->pPars->fVeryVerbose;
int c, i, d, Var, iLit, CostMin, Cost, status; int Var = -1, CostMin = ABC_INFINITY;
int c, i, d, iLit, Cost, status;
abctime clk; abctime clk;
assert( nAssump <= SFM_SUPP_MAX ); assert( nAssump <= SFM_SUPP_MAX );
if ( p->pPars->fVeryVerbose ) if ( p->pPars->fVeryVerbose )
...@@ -966,6 +973,14 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu ...@@ -966,6 +973,14 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
*Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]); *Vec_WrdEntryP(&p->vSets[c], i) |= ((word)1 << p->nPats[c]);
p->uMask[c] |= ((word)1 << p->nPats[c]++); p->uMask[c] |= ((word)1 << p->nPats[c]++);
} }
if ( p->iUseThis != -1 )
{
Var = p->iUseThis;
p->iUseThis = -1;
goto cofactor;
}
// check implications // check implications
Vec_IntClear( &p->vImpls[0] ); Vec_IntClear( &p->vImpls[0] );
Vec_IntClear( &p->vImpls[1] ); Vec_IntClear( &p->vImpls[1] );
...@@ -1103,7 +1118,6 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu ...@@ -1103,7 +1118,6 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
} }
// find the best cofactoring variable // find the best cofactoring variable
Var = -1, CostMin = ABC_INFINITY;
// if ( !fCofactor || Vec_IntSize(&p->vImpls[0]) + Vec_IntSize(&p->vImpls[1]) > 2 ) // if ( !fCofactor || Vec_IntSize(&p->vImpls[0]) + Vec_IntSize(&p->vImpls[1]) > 2 )
for ( c = 0; c < 2; c++ ) for ( c = 0; c < 2; c++ )
{ {
...@@ -1156,7 +1170,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu ...@@ -1156,7 +1170,7 @@ int Sfm_DecPeformDec_rec( Sfm_Dec_t * p, word * pTruth, int * pSupp, int * pAssu
printf( "Best var %d with weight %d. Cofactored = %s\n", Var, CostMin, Var == p->nDivs - 1 ? "yes" : "no" ); printf( "Best var %d with weight %d. Cofactored = %s\n", Var, CostMin, Var == p->nDivs - 1 ? "yes" : "no" );
printf( "\n" ); printf( "\n" );
} }
cofactor:
// cofactor the problem // cofactor the problem
if ( Var >= 0 ) if ( Var >= 0 )
{ {
...@@ -1227,6 +1241,8 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p, Abc_Obj_t * pObj ) ...@@ -1227,6 +1241,8 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p, Abc_Obj_t * pObj )
Dau_DsdPrintFromTruth( uTruth[i], nSupp[i] ); Dau_DsdPrintFromTruth( uTruth[i], nSupp[i] );
if ( nSupp[i] < 2 ) if ( nSupp[i] < 2 )
{ {
p->nSuppVars = nSupp[i];
Abc_TtCopy( p->Copy, uTruth[i], SFM_WORD_MAX, 0 );
RetValue = Sfm_LibImplementSimple( p->pLib, uTruth[i], pSupp[i], nSupp[i], &p->vObjGates, &p->vObjFanins ); RetValue = Sfm_LibImplementSimple( p->pLib, uTruth[i], pSupp[i], nSupp[i], &p->vObjGates, &p->vObjFanins );
assert( nSupp[i] <= p->pPars->nVarMax ); assert( nSupp[i] <= p->pPars->nVarMax );
p->nLuckySizes[nSupp[i]]++; p->nLuckySizes[nSupp[i]]++;
...@@ -1236,6 +1252,8 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p, Abc_Obj_t * pObj ) ...@@ -1236,6 +1252,8 @@ int Sfm_DecPeformDec2( Sfm_Dec_t * p, Abc_Obj_t * pObj )
return RetValue; return RetValue;
} }
p->nSuppVars = nSupp[i];
Abc_TtCopy( p->Copy, uTruth[i], SFM_WORD_MAX, 0 );
AreaNew = Sfm_LibFindAreaMatch( p->pLib, uTruth[i], nSupp[i], &iLibObj ); AreaNew = Sfm_LibFindAreaMatch( p->pLib, uTruth[i], nSupp[i], &iLibObj );
/* /*
uTruth[i][0] = ~uTruth[i][0]; uTruth[i][0] = ~uTruth[i][0];
...@@ -1346,6 +1364,8 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj ) ...@@ -1346,6 +1364,8 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )
} }
if ( nSupp[i] < 2 ) if ( nSupp[i] < 2 )
{ {
p->nSuppVars = nSupp[i];
Abc_TtCopy( p->Copy, uTruth[i], SFM_WORD_MAX, 0 );
RetValue = Sfm_LibImplementSimple( p->pLib, uTruth[i], pSupp[i], nSupp[i], &p->vObjGates, &p->vObjFanins ); RetValue = Sfm_LibImplementSimple( p->pLib, uTruth[i], pSupp[i], nSupp[i], &p->vObjGates, &p->vObjFanins );
assert( nSupp[i] <= p->pPars->nVarMax ); assert( nSupp[i] <= p->pPars->nVarMax );
p->nLuckySizes[nSupp[i]]++; p->nLuckySizes[nSupp[i]]++;
...@@ -1359,6 +1379,8 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj ) ...@@ -1359,6 +1379,8 @@ int Sfm_DecPeformDec3( Sfm_Dec_t * p, Abc_Obj_t * pObj )
//} //}
// try the delay // try the delay
p->nSuppVars = nSupp[i];
Abc_TtCopy( p->Copy, uTruth[i], SFM_WORD_MAX, 0 );
nMatches = Sfm_LibFindDelayMatches( p->pLib, uTruth[i], pSupp[i], nSupp[i], &p->vMatchGates, &p->vMatchFans ); nMatches = Sfm_LibFindDelayMatches( p->pLib, uTruth[i], pSupp[i], nSupp[i], &p->vMatchGates, &p->vMatchFans );
for ( k = 0; k < nMatches; k++ ) for ( k = 0; k < nMatches; k++ )
{ {
...@@ -1521,39 +1543,48 @@ void Sfm_DecMarkMffc( Abc_Obj_t * pPivot, int nLevelMin, int nMffcMax, int fVery ...@@ -1521,39 +1543,48 @@ void Sfm_DecMarkMffc( Abc_Obj_t * pPivot, int nLevelMin, int nMffcMax, int fVery
Vec_IntClear(vInMffc); Vec_IntClear(vInMffc);
Abc_ObjForEachFanin( pPivot, pFanin, i ) Abc_ObjForEachFanin( pPivot, pFanin, i )
if ( Sfm_DecNodeIsMffcInput(pFanin, nLevelMin, pTim, pPivot) ) if ( Sfm_DecNodeIsMffcInput(pFanin, nLevelMin, pTim, pPivot) )
Vec_IntPush( vInMffc, Abc_ObjId(pFanin) ); Vec_IntPushUnique( vInMffc, Abc_ObjId(pFanin) );
Abc_ObjForEachFanin( pPivot, pFanin, i ) Abc_ObjForEachFanin( pPivot, pFanin, i )
if ( Sfm_DecNodeIsMffcInput(pFanin, nLevelMin, pTim, pPivot) )
Abc_ObjForEachFanin( pFanin, pFanin2, k ) Abc_ObjForEachFanin( pFanin, pFanin2, k )
if ( Sfm_DecNodeIsMffcInput(pFanin2, nLevelMin, pTim, pPivot) ) if ( Sfm_DecNodeIsMffcInput(pFanin2, nLevelMin, pTim, pPivot) )
Vec_IntPush( vInMffc, Abc_ObjId(pFanin2) ); Vec_IntPushUnique( vInMffc, Abc_ObjId(pFanin2) );
Abc_ObjForEachFanin( pPivot, pFanin, i ) Abc_ObjForEachFanin( pPivot, pFanin, i )
if ( Sfm_DecNodeIsMffcInput(pFanin, nLevelMin, pTim, pPivot) )
Abc_ObjForEachFanin( pFanin, pFanin2, k ) Abc_ObjForEachFanin( pFanin, pFanin2, k )
if ( Sfm_DecNodeIsMffcInput(pFanin2, nLevelMin, pTim, pPivot) )
Abc_ObjForEachFanin( pFanin2, pFanin3, n ) Abc_ObjForEachFanin( pFanin2, pFanin3, n )
if ( Sfm_DecNodeIsMffcInput(pFanin3, nLevelMin, pTim, pPivot) ) if ( Sfm_DecNodeIsMffcInput(pFanin3, nLevelMin, pTim, pPivot) )
Vec_IntPush( vInMffc, Abc_ObjId(pFanin3) ); Vec_IntPushUnique( vInMffc, Abc_ObjId(pFanin3) );
/*
printf( "Node %d: (%.2f) ", pPivot->Id, MIO_NUMINV*Sfm_TimReadObjDelay(pTim, Abc_ObjId(pPivot)) );
Abc_ObjForEachFanin( pPivot, pFanin, i )
printf( "%d: %.2f ", Abc_ObjLevel(pFanin), MIO_NUMINV*Sfm_TimReadObjDelay(pTim, Abc_ObjId(pFanin)) );
printf( "\n" );
printf( "Node %d: ", pPivot->Id );
Abc_NtkForEachObjVec( vInMffc, pPivot->pNtk, pObj, i )
printf( "%d: %.2f ", Abc_ObjLevel(pObj), MIO_NUMINV*Sfm_TimReadObjDelay(pTim, Abc_ObjId(pObj)) );
printf( "\n" );
*/
} }
else else
{ {
// collect MFFC // collect MFFC
Abc_ObjForEachFanin( pPivot, pFanin, i ) Abc_ObjForEachFanin( pPivot, pFanin, i )
if ( Sfm_DecNodeIsMffc(pFanin, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) if ( Sfm_DecNodeIsMffc(pFanin, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax )
Vec_IntPush( vMffc, Abc_ObjId(pFanin) ); Vec_IntPushUnique( vMffc, Abc_ObjId(pFanin) );
Abc_ObjForEachFanin( pPivot, pFanin, i ) Abc_ObjForEachFanin( pPivot, pFanin, i )
if ( Sfm_DecNodeIsMffc(pFanin, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) if ( Sfm_DecNodeIsMffc(pFanin, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax )
Abc_ObjForEachFanin( pFanin, pFanin2, k ) Abc_ObjForEachFanin( pFanin, pFanin2, k )
if ( Sfm_DecNodeIsMffc(pFanin2, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) if ( Sfm_DecNodeIsMffc(pFanin2, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax )
Vec_IntPush( vMffc, Abc_ObjId(pFanin2) ); Vec_IntPushUnique( vMffc, Abc_ObjId(pFanin2) );
Abc_ObjForEachFanin( pPivot, pFanin, i ) Abc_ObjForEachFanin( pPivot, pFanin, i )
if ( Sfm_DecNodeIsMffc(pFanin, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) if ( Sfm_DecNodeIsMffc(pFanin, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax )
Abc_ObjForEachFanin( pFanin, pFanin2, k ) Abc_ObjForEachFanin( pFanin, pFanin2, k )
if ( Sfm_DecNodeIsMffc(pFanin2, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) if ( Sfm_DecNodeIsMffc(pFanin2, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax )
Abc_ObjForEachFanin( pFanin2, pFanin3, n ) Abc_ObjForEachFanin( pFanin2, pFanin3, n )
if ( Sfm_DecNodeIsMffc(pFanin3, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax ) if ( Sfm_DecNodeIsMffc(pFanin3, nLevelMin) && Vec_IntSize(vMffc) < nMffcMax )
Vec_IntPush( vMffc, Abc_ObjId(pFanin3) ); Vec_IntPushUnique( vMffc, Abc_ObjId(pFanin3) );
// mark MFFC // mark MFFC
assert( Vec_IntSize(vMffc) <= nMffcMax ); assert( Vec_IntSize(vMffc) <= nMffcMax );
Abc_NtkForEachObjVec( vMffc, pPivot->pNtk, pObj, i ) Abc_NtkForEachObjVec( vMffc, pPivot->pNtk, pObj, i )
...@@ -1565,6 +1596,16 @@ void Sfm_DecMarkMffc( Abc_Obj_t * pPivot, int nLevelMin, int nMffcMax, int fVery ...@@ -1565,6 +1596,16 @@ void Sfm_DecMarkMffc( Abc_Obj_t * pPivot, int nLevelMin, int nMffcMax, int fVery
Abc_ObjForEachFanin( pObj, pFanin, k ) Abc_ObjForEachFanin( pObj, pFanin, k )
if ( Abc_NodeIsTravIdCurrent(pFanin) && pFanin->iTemp == SFM_MASK_PI ) if ( Abc_NodeIsTravIdCurrent(pFanin) && pFanin->iTemp == SFM_MASK_PI )
Vec_IntPushUnique( vInMffc, Abc_ObjId(pFanin) ); Vec_IntPushUnique( vInMffc, Abc_ObjId(pFanin) );
// printf( "Node %d: ", pPivot->Id );
// Abc_ObjForEachFanin( pPivot, pFanin, i )
// printf( "%d ", Abc_ObjFanoutNum(pFanin) );
// printf( "\n" );
// Abc_NtkForEachObjVec( vInMffc, pPivot->pNtk, pObj, i )
// printf( "%d ", Abc_ObjFanoutNum(pObj) );
// printf( "\n" );
} }
} }
...@@ -1687,6 +1728,7 @@ printf( "\n" ); ...@@ -1687,6 +1728,7 @@ printf( "\n" );
// remap inputs to MFFC // remap inputs to MFFC
Abc_NtkForEachObjVec( vInMffc, pNtk, pObj, i ) Abc_NtkForEachObjVec( vInMffc, pNtk, pObj, i )
Vec_IntWriteEntry( vInMffc, i, pObj->iTemp ); Vec_IntWriteEntry( vInMffc, i, pObj->iTemp );
/* /*
// check // check
Abc_NtkForEachObjVec( vMap, pNtk, pObj, i ) Abc_NtkForEachObjVec( vMap, pNtk, pObj, i )
...@@ -1781,8 +1823,8 @@ Abc_Obj_t * Sfm_DecInsert( Abc_Ntk_t * pNtk, Abc_Obj_t * pPivot, int Limit, Vec_ ...@@ -1781,8 +1823,8 @@ Abc_Obj_t * Sfm_DecInsert( Abc_Ntk_t * pNtk, Abc_Obj_t * pPivot, int Limit, Vec_
void Sfm_DecPrintStats( Sfm_Dec_t * p ) void Sfm_DecPrintStats( Sfm_Dec_t * p )
{ {
int i; int i;
printf( "Node = %d. Try = %d. Change = %d. Const0 = %d. Const1 = %d. Buf = %d. Inv = %d. Gate = %d. AndOr = %d. NoDec = %d.\n", printf( "Node = %d. Try = %d. Change = %d. Const0 = %d. Const1 = %d. Buf = %d. Inv = %d. Gate = %d. AndOr = %d. Effort = %d. NoDec = %d.\n",
p->nTotalNodesBeg, p->nNodesTried, p->nNodesChanged, p->nNodesConst0, p->nNodesConst1, p->nNodesBuf, p->nNodesInv, p->nNodesResyn, p->nNodesAndOr, p->nNoDecs ); p->nTotalNodesBeg, p->nNodesTried, p->nNodesChanged, p->nNodesConst0, p->nNodesConst1, p->nNodesBuf, p->nNodesInv, p->nNodesResyn, p->nNodesAndOr, p->nEfforts, p->nNoDecs );
printf( "MaxDiv = %d. MaxWin = %d. AveDiv = %d. AveWin = %d. Calls = %d. (Sat = %d. Unsat = %d.) Over = %d. T/O = %d.\n", printf( "MaxDiv = %d. MaxWin = %d. AveDiv = %d. AveWin = %d. Calls = %d. (Sat = %d. Unsat = %d.) Over = %d. T/O = %d.\n",
p->nMaxDivs, p->nMaxWin, (int)(p->nAllDivs/Abc_MaxInt(1, p->nNodesTried)), (int)(p->nAllWin/Abc_MaxInt(1, p->nNodesTried)), p->nSatCalls, p->nSatCallsSat, p->nSatCallsUnsat, p->nSatCallsOver, p->nTimeOuts ); p->nMaxDivs, p->nMaxWin, (int)(p->nAllDivs/Abc_MaxInt(1, p->nNodesTried)), (int)(p->nAllWin/Abc_MaxInt(1, p->nNodesTried)), p->nSatCalls, p->nSatCallsSat, p->nSatCallsUnsat, p->nSatCallsOver, p->nTimeOuts );
...@@ -1884,6 +1926,33 @@ clk = Abc_Clock(); ...@@ -1884,6 +1926,33 @@ clk = Abc_Clock();
RetValue = Sfm_DecPeformDec( p ); RetValue = Sfm_DecPeformDec( p );
else else
RetValue = Sfm_DecPeformDec2( p, pObj ); RetValue = Sfm_DecPeformDec2( p, pObj );
if ( pPars->fMoreEffort && RetValue < 0 )
{
int Var, i;
Vec_IntForEachEntryReverse( &p->vObjInMffc, Var, i )
{
p->iUseThis = Var;
if ( pPars->fRrOnly )
RetValue = Sfm_DecPeformDec( p );
else
RetValue = Sfm_DecPeformDec2( p, pObj );
p->iUseThis = -1;
if ( RetValue < 0 )
{
//printf( "Node %d: Not found among %d.\n", Abc_ObjId(pObj), Vec_IntSize(&p->vObjInMffc) );
}
else
{
p->nEfforts++;
if ( p->pPars->fVerbose )
{
//printf( "Node %5d: (%2d out of %2d) Gate=%s ", Abc_ObjId(pObj), i, Vec_IntSize(&p->vObjInMffc), Mio_GateReadName((Mio_Gate_t*)pObj->pData) );
//Dau_DsdPrintFromTruth( p->Copy, p->nSuppVars );
}
break;
}
}
}
if ( p->pPars->fVeryVerbose ) if ( p->pPars->fVeryVerbose )
printf( "\n\n" ); printf( "\n\n" );
p->timeSat += Abc_Clock() - clk; p->timeSat += Abc_Clock() - clk;
...@@ -1997,6 +2066,30 @@ p->timeCnf += Abc_Clock() - clk; ...@@ -1997,6 +2066,30 @@ p->timeCnf += Abc_Clock() - clk;
} }
clk = Abc_Clock(); clk = Abc_Clock();
RetValue = Sfm_DecPeformDec3( p, pObj ); RetValue = Sfm_DecPeformDec3( p, pObj );
if ( pPars->fMoreEffort && RetValue < 0 )
{
int Var, i;
Vec_IntForEachEntryReverse( &p->vObjInMffc, Var, i )
{
p->iUseThis = Var;
RetValue = Sfm_DecPeformDec3( p, pObj );
p->iUseThis = -1;
if ( RetValue < 0 )
{
//printf( "Node %d: Not found among %d.\n", Abc_ObjId(pObj), Vec_IntSize(&p->vObjInMffc) );
}
else
{
p->nEfforts++;
if ( p->pPars->fVerbose )
{
//printf( "Node %5d: (%2d out of %2d) Gate=%s ", Abc_ObjId(pObj), i, Vec_IntSize(&p->vObjInMffc), Mio_GateReadName((Mio_Gate_t*)pObj->pData) );
//Dau_DsdPrintFromTruth( p->Copy, p->nSuppVars );
}
break;
}
}
}
if ( p->pPars->fVeryVerbose ) if ( p->pPars->fVeryVerbose )
printf( "\n\n" ); printf( "\n\n" );
p->timeSat += Abc_Clock() - clk; p->timeSat += Abc_Clock() - clk;
...@@ -2058,6 +2151,7 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars ) ...@@ -2058,6 +2151,7 @@ void Abc_NtkPerformMfs3( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
printf( "Delta = %.2f ps. ", MIO_NUMINV*p->DeltaCrit ); printf( "Delta = %.2f ps. ", MIO_NUMINV*p->DeltaCrit );
if ( pPars->fArea ) if ( pPars->fArea )
printf( "0-cost = %s. ", pPars->fZeroCost ? "yes" : "no" ); printf( "0-cost = %s. ", pPars->fZeroCost ? "yes" : "no" );
printf( "Effort = %s. ", pPars->fMoreEffort ? "yes" : "no" );
printf( "Sim = %s. ", pPars->fUseSim ? "yes" : "no" ); printf( "Sim = %s. ", pPars->fUseSim ? "yes" : "no" );
printf( "\n" ); printf( "\n" );
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment