diff --git a/src/map/if/acd/ac_wrapper.cpp b/src/map/if/acd/ac_wrapper.cpp index 7268fcad4..441cb7008 100644 --- a/src/map/if/acd/ac_wrapper.cpp +++ b/src/map/if/acd/ac_wrapper.cpp @@ -70,18 +70,18 @@ int acd_decompose( word * pTruth, unsigned nVars, int lutSize, unsigned *pdelay, return 0; } -int acd66_evaluate( word * pTruth, unsigned nVars, int verify ) +int acd66_evaluate( word * pTruth, unsigned nVars, int compute_decomposition ) { using namespace acd; acd66_params ps; - ps.verify = static_cast( verify ); + ps.verify = false; acd66_impl acd( nVars, ps ); if ( acd.run( pTruth ) == 0 ) return 0; - if ( !verify ) + if ( !compute_decomposition ) return 1; int val = acd.compute_decomposition(); diff --git a/src/map/if/acd/ac_wrapper.h b/src/map/if/acd/ac_wrapper.h index 2b832c287..2e052c563 100644 --- a/src/map/if/acd/ac_wrapper.h +++ b/src/map/if/acd/ac_wrapper.h @@ -28,7 +28,7 @@ ABC_NAMESPACE_HEADER_START int acd_evaluate( word * pTruth, unsigned nVars, int lutSize, unsigned *pdelay, unsigned *cost, int try_no_late_arrival ); int acd_decompose( word * pTruth, unsigned nVars, int lutSize, unsigned *pdelay, unsigned char *decomposition ); -int acd66_evaluate( word * pTruth, unsigned nVars, int verify ); +int acd66_evaluate( word * pTruth, unsigned nVars, int compute_decomposition ); int acd66_decompose( word * pTruth, unsigned nVars, unsigned char *decomposition ); ABC_NAMESPACE_HEADER_END diff --git a/src/map/if/acd/acd66.hpp b/src/map/if/acd/acd66.hpp index a1369db83..166402ca0 100644 --- a/src/map/if/acd/acd66.hpp +++ b/src/map/if/acd/acd66.hpp @@ -54,7 +54,7 @@ struct acd66_params uint32_t max_evaluations{ 3 }; /*! \brief Run verification before returning. */ - bool verify{ true }; + bool verify{ false }; }; /*! \brief Statistics for acd66 */ diff --git a/src/map/if/ifDec66.c b/src/map/if/ifDec66.c index 932f5feb2..3a836363d 100644 --- a/src/map/if/ifDec66.c +++ b/src/map/if/ifDec66.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [ifDec16.c] + FileName [ifDec66.c] SystemName [ABC: Logic synthesis and verification system.] @@ -8,13 +8,13 @@ Synopsis [Fast checking procedures.] - Author [Alan Mishchenko] + Author [Alessandro Tempia Calvino] - Affiliation [UC Berkeley] + Affiliation [EPFL] - Date [Ver. 1.0. Started - November 21, 2006.] + Date [Ver. 1.0. Started - Feb 8, 2024.] - Revision [$Id: ifDec16.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + Revision [$Id: ifDec66.c,v 1.00 2008/02/08 00:00:00 tempia Exp $] ***********************************************************************/ @@ -24,10 +24,258 @@ ABC_NAMESPACE_IMPL_START +#define CLU_VAR_MAX 16 +#define CLU_MEM_MAX 1000 // 1 GB +#define CLU_UNUSED 0xff + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// decomposition +typedef struct If_Grp_t_ If_Grp_t; +struct If_Grp_t_ +{ + char nVars; + char nMyu; + char pVars[CLU_VAR_MAX]; +}; + +// hash table entry +typedef struct If_Hte_t_ If_Hte_t; +struct If_Hte_t_ +{ + If_Hte_t * pNext; + unsigned Group; + unsigned Counter; + word pTruth[1]; +}; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +static inline unsigned If_CluGrp2Uns2( If_Grp_t * pG ) +{ + char * pChar = (char *)pG; + unsigned Res = 0; + int i; + for ( i = 0; i < 8; i++ ) + Res |= ((pChar[i] & 15) << (i << 2)); + return Res; +} + +static inline void If_CluUns2Grp2( unsigned Group, If_Grp_t * pG ) +{ + char * pChar = (char *)pG; + int i; + for ( i = 0; i < 8; i++ ) + pChar[i] = ((Group >> (i << 2)) & 15); +} + +unsigned int If_CluPrimeCudd2( unsigned int p ) +{ + int i,pn; + + p--; + do { + p++; + if (p&1) { + pn = 1; + i = 3; + while ((unsigned) (i * i) <= p) { + if (p % i == 0) { + pn = 0; + break; + } + i += 2; + } + } else { + pn = 0; + } + } while (!pn); + return(p); + +} /* end of Cudd_Prime */ + +// hash table +static inline int If_CluWordNum2( int nVars ) +{ + return nVars <= 6 ? 1 : 1 << (nVars-6); +} + +int If_CluHashFindMedian2( If_Man_t * p, int t ) +{ + If_Hte_t * pEntry; + Vec_Int_t * vCounters; + int i, Max = 0, Total = 0, Half = 0; + vCounters = Vec_IntStart( 1000 ); + for ( i = 0; i < p->nTableSize[t]; i++ ) + { + for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; pEntry = pEntry->pNext ) + { + if ( Max < (int)pEntry->Counter ) + { + Max = pEntry->Counter; + Vec_IntSetEntry( vCounters, pEntry->Counter, 0 ); + } + Vec_IntAddToEntry( vCounters, pEntry->Counter, 1 ); + Total++; + } + } + for ( i = Max; i > 0; i-- ) + { + Half += Vec_IntEntry( vCounters, i ); + if ( Half > Total/2 ) + break; + } +/* + printf( "total = %d ", Total ); + printf( "half = %d ", Half ); + printf( "i = %d ", i ); + printf( "Max = %d.\n", Max ); +*/ + Vec_IntFree( vCounters ); + return Abc_MaxInt( i, 1 ); +} + +int If_CluHashKey2( word * pTruth, int nWords, int Size ) +{ + static unsigned BigPrimes[8] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457, 1610612741}; + unsigned Value = 0; + int i; + if ( nWords < 4 ) + { + unsigned char * s = (unsigned char *)pTruth; + for ( i = 0; i < 8 * nWords; i++ ) + Value ^= BigPrimes[i % 7] * s[i]; + } + else + { + unsigned * s = (unsigned *)pTruth; + for ( i = 0; i < 2 * nWords; i++ ) + Value ^= BigPrimes[i % 7] * s[i]; + } + return Value % Size; +} + +unsigned * If_CluHashLookup2( If_Man_t * p, word * pTruth, int t ) +{ + If_Hte_t * pEntry, * pPrev; + int nWords, HashKey; + if ( p == NULL ) + return NULL; + nWords = If_CluWordNum2(p->pPars->nLutSize); + if ( p->pMemEntries == NULL ) + p->pMemEntries = Mem_FixedStart( sizeof(If_Hte_t) + sizeof(word) * (If_CluWordNum2(p->pPars->nLutSize) - 1) ); + if ( p->pHashTable[t] == NULL ) + { + // decide how large should be the table + int nEntriesMax1 = 4 * If_CluPrimeCudd2( Vec_PtrSize(p->vObjs) * p->pPars->nCutsMax ); + int nEntriesMax2 = (int)(((double)CLU_MEM_MAX * (1 << 20)) / If_CluWordNum2(p->pPars->nLutSize) / 8); +// int nEntriesMax2 = 10000; + // create table + p->nTableSize[t] = If_CluPrimeCudd2( Abc_MinInt(nEntriesMax1, nEntriesMax2)/2 ); + p->pHashTable[t] = ABC_CALLOC( void *, p->nTableSize[t] ); + } + // check if this entry exists + HashKey = If_CluHashKey2( pTruth, nWords, p->nTableSize[t] ); + for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[HashKey]; pEntry; pEntry = pEntry->pNext ) + if ( memcmp(pEntry->pTruth, pTruth, sizeof(word) * nWords) == 0 ) + { + pEntry->Counter++; + return &pEntry->Group; + } + // resize the hash table + if ( p->nTableEntries[t] >= 2 * p->nTableSize[t] ) + { + // collect useful entries + If_Hte_t * pPrev; + Vec_Ptr_t * vUseful = Vec_PtrAlloc( p->nTableEntries[t] ); + int i, Median = If_CluHashFindMedian2( p, t ); + for ( i = 0; i < p->nTableSize[t]; i++ ) + { + for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; ) + { + if ( (int)pEntry->Counter > Median ) + { + Vec_PtrPush( vUseful, pEntry ); + pEntry = pEntry->pNext; + } + else + { + pPrev = pEntry->pNext; + Mem_FixedEntryRecycle( p->pMemEntries, (char *)pEntry ); + pEntry = pPrev; + } + } + } + // add useful entries + memset( p->pHashTable[t], 0, sizeof(void *) * p->nTableSize[t] ); + Vec_PtrForEachEntry( If_Hte_t *, vUseful, pEntry, i ) + { + HashKey = If_CluHashKey2( pEntry->pTruth, nWords, p->nTableSize[t] ); + pPrev = ((If_Hte_t **)p->pHashTable[t])[HashKey]; + if ( pPrev == NULL || pEntry->Counter >= pPrev->Counter ) + { + pEntry->pNext = pPrev; + ((If_Hte_t **)p->pHashTable[t])[HashKey] = pEntry; + } + else + { + while ( pPrev->pNext && pEntry->Counter < pPrev->pNext->Counter ) + pPrev = pPrev->pNext; + pEntry->pNext = pPrev->pNext; + pPrev->pNext = pEntry; + } + } + p->nTableEntries[t] = Vec_PtrSize( vUseful ); + Vec_PtrFree( vUseful ); + } + // create entry + p->nTableEntries[t]++; + pEntry = (If_Hte_t *)Mem_FixedEntryFetch( p->pMemEntries ); + memcpy( pEntry->pTruth, pTruth, sizeof(word) * nWords ); + pEntry->Group = CLU_UNUSED; + pEntry->Counter = 1; + // insert at the beginning +// pEntry->pNext = ((If_Hte_t **)p->pHashTable[t])[HashKey]; +// ((If_Hte_t **)p->pHashTable[t])[HashKey] = pEntry; + // insert at the end + pEntry->pNext = NULL; + for ( pPrev = ((If_Hte_t **)p->pHashTable[t])[HashKey]; pPrev && pPrev->pNext; pPrev = pPrev->pNext ); + if ( pPrev == NULL ) + ((If_Hte_t **)p->pHashTable[t])[HashKey] = pEntry; + else + pPrev->pNext = pEntry; + return &pEntry->Group; +} + +// returns if successful +int If_CluCheck66( If_Man_t * p, word * pTruth0, int nVars, int fHashing ) +{ + If_Grp_t G1 = {0}; + unsigned * pHashed = NULL; + + if ( p && fHashing ) + { + pHashed = If_CluHashLookup2( p, pTruth0, 0 ); + if ( pHashed && *pHashed != CLU_UNUSED ) + If_CluUns2Grp2( *pHashed, &G1 ); + } + + /* new entry */ + if ( G1.nVars == 0 ) + { + G1.nVars = acd66_evaluate( pTruth0, nVars, 0 ); + } + + if ( pHashed ) + *pHashed = If_CluGrp2Uns2( &G1 ); + + return G1.nVars; +} + /**Function************************************************************* Synopsis [Performs ACD into 66 cascade.] @@ -79,7 +327,7 @@ int If_CutPerformCheck66( If_Man_t * p, unsigned * pTruth0, int nVars, int nLeav return 1; // derive the decomposition - return (int)(acd66_evaluate( (word *)pTruth, nVars, 1 ) > 0 ); + return If_CluCheck66(p, (word*)pTruth, nVars, 1); } ////////////////////////////////////////////////////////////////////////