diff options
| author | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-07-30 15:21:57 +0200 |
|---|---|---|
| committer | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-07-30 15:21:57 +0200 |
| commit | a6352369a5583f18c8819a40fc2968f6d8dbe93c (patch) | |
| tree | be20d83defd7e16b4d04c2815a9100456fa7af43 | |
| parent | 59077dab9f099a08ed958cdcda6ddf8f22b7ed3e (diff) | |
| download | abc-a6352369a5583f18c8819a40fc2968f6d8dbe93c.tar.gz abc-a6352369a5583f18c8819a40fc2968f6d8dbe93c.tar.bz2 abc-a6352369a5583f18c8819a40fc2968f6d8dbe93c.zip | |
Depth optimal synthesis.
| -rw-r--r-- | src/base/abci/abcExact.c | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index a8ad858f..40f85b79 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -1111,8 +1111,8 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * { int l; Ses_Man_t * pSes; - char * pSol, * p; - int Delay; + char * pSol = NULL, * p; + int Delay = ABC_INFINITY, nMaxDepth = nVars - 1; abctime timeStart; /* some checks */ @@ -1120,12 +1120,25 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * timeStart = Abc_Clock(); - pSes = Ses_ManAlloc( pTruth, nVars, 1, nVars - 1, pArrTimeProfile, 1, 0 ); + *Cost = ABC_INFINITY; - if ( Ses_ManFindMinimumSize( pSes ) ) + pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, 1 /* fMakeAIG */, 0 ); + + while ( 1 ) /* there is improvement */ { - pSol = Ses_ManExtractSolution( pSes ); + if ( Ses_ManFindMinimumSize( pSes ) ) + { + if ( pSol ) + ABC_FREE( pSol ); + pSol = Ses_ManExtractSolution( pSes ); + pSes->nMaxDepth--; + } + else + break; + } + if ( pSol ) + { *Cost = pSol[ABC_EXACT_SOL_NGATES]; p = pSol + 3 + 4 * ABC_EXACT_SOL_NGATES + 1; Delay = *p++; @@ -1134,8 +1147,6 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * ABC_FREE( pSol ); } - else - *Cost = Delay = ABC_INFINITY; pSes->timeTotal = Abc_Clock() - timeStart; |