summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abcExact.c80
1 files changed, 60 insertions, 20 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index 8c508b63..19b0188a 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -165,6 +165,14 @@ static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * ma
return delta;
}
+static inline void Abc_UnnormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int nDelta )
+{
+ int l;
+
+ for ( l = 0; l < nVars; ++l )
+ pArrTimeProfile[l] += nDelta;
+}
+
static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fMakeAIG, int fVerbose )
{
Ses_Store_t * pStore = ABC_CALLOC( Ses_Store_t, 1 );
@@ -262,12 +270,10 @@ static inline void Ses_StoreTimesCopy( int * pTimesDest, int * pTimesSrc, int nV
// returns 1 if and only if a new TimesEntry has been created
int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char * pSol )
{
- int i, nDelta, maxNormalized, key, fAdded;
+ int key, fAdded;
Ses_TruthEntry_t * pTEntry;
Ses_TimesEntry_t * pTiEntry;
- nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &maxNormalized );
-
key = Ses_StoreTableHash( pTruth, nVars );
pTEntry = pStore->pEntries[key];
@@ -316,8 +322,6 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr
/* item was already present */
fAdded = 0;
- for ( i = 0; i < nVars; ++i )
- pArrTimeProfile[i] += nDelta;
return fAdded;
}
@@ -325,7 +329,7 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr
// returns 0 if no solution was found
char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile )
{
- int i, nDelta, maxNormalized, key;
+ int key;
Ses_TruthEntry_t * pTEntry;
Ses_TimesEntry_t * pTiEntry;
@@ -345,8 +349,6 @@ char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int *
if ( !pTEntry )
return 0;
- nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &maxNormalized );
-
/* find times entry */
pTiEntry = pTEntry->head;
while ( pTiEntry )
@@ -357,9 +359,6 @@ char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int *
pTiEntry = pTiEntry->next;
}
- for ( i = 0; i < nVars; ++i )
- pArrTimeProfile[i] += nDelta;
-
/* no entry found? */
if ( !pTiEntry )
return 0;
@@ -738,7 +737,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
}
/* EXTRA clauses: symmetric variables */
- if ( pSes->nSpecFunc == 1 ) /* only check if there is one output function */
+ if ( pSes->nMaxDepth == -1 && pSes->nSpecFunc == 1 ) /* only check if there is one output function */
for ( q = 1; q < pSes->nSpecVars; ++q )
for ( p = 0; p < q; ++p )
if ( Extra_TruthVarsSymm( (unsigned*)( &pSes->pSpec[h << 2] ), pSes->nSpecVars, p, q ) )
@@ -982,16 +981,18 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes )
*p++ = Abc_Var2Lit( i, ( pSes->bSpecInv >> h ) & 1 );
d = 0;
if ( pSes->nMaxDepth != -1 )
- while ( d < pSes->nArrTimeMax + i && sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, d ) ) )
- ++d;
- *p++ = d + pSes->nArrTimeDelta;
+ /* while ( d < pSes->nArrTimeMax + i && sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, d ) ) ) */
+ /* ++d; */
+ for ( l = 0; l < pSes->nSpecVars; ++l )
+ d = Abc_MaxInt( d, pSes->pArrTimeProfile[l] + pPerm[i * pSes->nSpecVars + l] );
+ *p++ = d;
if ( pSes->fVeryVerbose )
- printf( "output %d points to %d and has normalized delay %d\n", h, i, d );
+ printf( "output %d points to %d and has normalized delay %d (nArrTimeDelta = %d)\n", h, i, d, pSes->nArrTimeDelta );
for ( l = 0; l < pSes->nSpecVars; ++l )
{
d = ( pSes->nMaxDepth != -1 ) ? pPerm[i * pSes->nSpecVars + l] : 0;
if ( pSes->fVeryVerbose )
- printf( " pin-to-pin arrival time from input %d is %d\n", l, d );
+ printf( " pin-to-pin arrival time from input %d is %d (pArrTimeProfile = %d)\n", l, d, pSes->pArrTimeProfile[l] );
*p++ = d;
}
}
@@ -1494,7 +1495,7 @@ void Abc_ExactStats()
// the area cost should not exceed 2048, if the cut is implementable; otherwise, it should be ABC_INFINITY
int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * pPerm, int * Cost, int AigLevel )
{
- int i, l, fExists = 0;
+ int i, nDelta, nMaxArrival, l, fExists = 0;
Ses_Man_t * pSes = NULL;
char * pSol = NULL, * p;
int Delay = ABC_INFINITY, nMaxDepth;
@@ -1520,6 +1521,18 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
return pArrTimeProfile[0];
}
+ nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &nMaxArrival );
+
+ if ( s_pSesStore->fVerbose )
+ {
+ printf( "compute delay for nontrivial truth table " );
+ Abc_TtPrintHexRev( stdout, pTruth, nVars );
+ printf( " with arrival times" );
+ for ( l = 0; l < nVars; ++l )
+ printf( " %d", pArrTimeProfile[l] );
+ printf( "\n" );
+ }
+
/* statistics */
s_pSesStore->nCutCount++;
s_pSesStore->pCutCount[nVars]++;
@@ -1527,6 +1540,8 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile );
if ( pSol )
{
+ if ( s_pSesStore->fVerbose )
+ printf( " truth table already in store\n" );
s_pSesStore->nCacheHit++;
fExists = 1;
}
@@ -1543,6 +1558,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, s_pSesStore->fMakeAIG, s_pSesStore->fVerbose );
pSes->nBTLimit = s_pSesStore->nBTLimit;
+ pSes->fVeryVerbose = 0;
while ( 1 ) /* there is improvement */
{
@@ -1576,14 +1592,36 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol );
}
- return Delay;
+ //for ( l = 0; l < nVars; ++l )
+ // printf( "pArrTimeProfile[%d] = %d\n", l, pArrTimeProfile[l] );
+
+ if ( pSol )
+ {
+ int Delay2 = 0;
+ for ( l = 0; l < nVars; ++l )
+ {
+ //printf( "%d ", pPerm[l] );
+ Delay2 = Abc_MaxInt( Delay2, pArrTimeProfile[l] + pPerm[l] );
+ }
+ //printf( " output arrival = %d recomputed = %d\n", Delay, Delay2 );
+ if ( Delay != Delay2 )
+ {
+ printf( "^--- BUG!\n" );
+ assert( 0 );
+ }
+ //Delay = Delay2;
+ }
+
+ Abc_UnnormalizeArrivalTimes( pArrTimeProfile, nVars, nDelta );
+
+ return nDelta + Delay;
}
// this procedure returns a new node whose output in terms of the given fanins
// has the smallest possible arrival time (in agreement with the above Abc_ExactDelayCost)
Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk )
{
char * pSol;
- int i, j;
+ int i, j, nDelta, nMaxArrival;
char const * p;
Abc_Obj_t * pObj;
Vec_Ptr_t * pGates;
@@ -1595,7 +1633,9 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile,
if ( nVars == 1 )
return (pTruth[0] & 1) ? Abc_NtkCreateNodeInv(pNtk, pFanins[0]) : Abc_NtkCreateNodeBuf(pNtk, pFanins[0]);
+ nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &nMaxArrival );
pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile );
+ Abc_UnnormalizeArrivalTimes( pArrTimeProfile, nVars, nDelta );
if ( !pSol )
return NULL;
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 04:04:50 +0000