/**CFile**************************************************************** FileName [ifDec16.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [FPGA mapping based on priority cuts.] Synopsis [Fast checking procedures.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - November 21, 2006.] Revision [$Id: ifDec16.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] ***********************************************************************/ #include "if.h" #include "src/bool/kit/kit.h" ABC_NAMESPACE_IMPL_START //#define IF_USE_CASE3 //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// #define CLU_VAR_MAX 16 #define CLU_WRD_MAX (1 << ((CLU_VAR_MAX)-6)) #define CLU_MEM_MAX 1000 // 1 Gb #define CLU_UNUSED 0xff // 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]; }; // variable swapping code static word PMasks[5][3] = { { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 }, { 0xC3C3C3C3C3C3C3C3, 0x0C0C0C0C0C0C0C0C, 0x3030303030303030 }, { 0xF00FF00FF00FF00F, 0x00F000F000F000F0, 0x0F000F000F000F00 }, { 0xFF0000FFFF0000FF, 0x0000FF000000FF00, 0x00FF000000FF0000 }, { 0xFFFF00000000FFFF, 0x00000000FFFF0000, 0x0000FFFF00000000 } }; // elementary truth tables static word Truth6[6] = { 0xAAAAAAAAAAAAAAAA, 0xCCCCCCCCCCCCCCCC, 0xF0F0F0F0F0F0F0F0, 0xFF00FF00FF00FF00, 0xFFFF0000FFFF0000, 0xFFFFFFFF00000000 }; static word TruthAll[CLU_VAR_MAX][CLU_WRD_MAX] = {{0}}; extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ); extern int If_CluSupportSize( word * t, int nVars ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// static inline unsigned If_CluGrp2Uns( 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_CluUns2Grp( 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_CluPrimeCudd( 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_CluWordNum( int nVars ) { return nVars <= 6 ? 1 : 1 << (nVars-6); } static inline int If_CluCountOnes( word t ) { t = (t & 0x5555555555555555) + ((t>> 1) & 0x5555555555555555); t = (t & 0x3333333333333333) + ((t>> 2) & 0x3333333333333333); t = (t & 0x0F0F0F0F0F0F0F0F) + ((t>> 4) & 0x0F0F0F0F0F0F0F0F); t = (t & 0x00FF00FF00FF00FF) + ((t>> 8) & 0x00FF00FF00FF00FF); t = (t & 0x0000FFFF0000FFFF) + ((t>>16) & 0x0000FFFF0000FFFF); return (t & 0x00000000FFFFFFFF) + (t>>32); } void If_CluHashTableCheck( If_Man_t * p ) { int t = 1; If_Hte_t * pEntry; int i, RetValue, Status; for ( i = 0; i < p->nTableSize[t]; i++ ) { for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; pEntry = pEntry->pNext ) { Status = ((pEntry->Group & 15) > 0); RetValue = If_CutPerformCheck16( NULL, (unsigned *)pEntry->pTruth, 13, If_CluSupportSize(pEntry->pTruth, 13), "555" ); if ( RetValue != Status ) { Kit_DsdPrintFromTruth( (unsigned*)pEntry->pTruth, 13 ); printf( "\n" ); RetValue = If_CutPerformCheck16( NULL, (unsigned *)pEntry->pTruth, 13, If_CluSupportSize(pEntry->pTruth, 13), "555" ); printf( "Hash table problem!!!\n" ); } } } } void If_CluHashPrintStats( If_Man_t * p, int t ) { If_Hte_t * pEntry; int i, Counter; for ( i = 0; i < p->nTableSize[t]; i++ ) { Counter = 0; for ( pEntry = ((If_Hte_t **)p->pHashTable[t])[i]; pEntry; pEntry = pEntry->pNext ) Counter++; if ( Counter == 0 ) continue; if ( Counter < 10 ) continue; printf( "%d=%d ", i, Counter ); } } int If_CluHashFindMedian( 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_CluHashKey( 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_CluHashLookup( If_Man_t * p, word * pTruth, int t ) { If_Hte_t * pEntry, * pPrev; int nWords, HashKey; if ( p == NULL ) return NULL; nWords = If_CluWordNum(p->pPars->nLutSize); if ( p->pMemEntries == NULL ) p->pMemEntries = Mem_FixedStart( sizeof(If_Hte_t) + sizeof(word) * (If_CluWordNum(p->pPars->nLutSize) - 1) ); if ( p->pHashTable[t] == NULL ) { // decide how large should be the table int nEntriesMax1 = 4 * If_CluPrimeCudd( Vec_PtrSize(p->vObjs) * p->pPars->nCutsMax ); int nEntriesMax2 = (int)(((double)CLU_MEM_MAX * (1 << 20)) / If_CluWordNum(p->pPars->nLutSize) / 8); // int nEntriesMax2 = 10000; // create table p->nTableSize[t] = If_CluPrimeCudd( Abc_MinInt(nEntriesMax1, nEntriesMax2)/2 ); p->pHashTable[t] = ABC_CALLOC( void *, p->nTableSize[t] ); } // check if this entry exists HashKey = If_CluHashKey( 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_CluHashFindMedian( 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_CluHashKey( 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; } // variable permutation for large functions static inline void If_CluClear( word * pIn, int nVars ) { int w, nWords = If_CluWordNum( nVars ); for ( w = 0; w < nWords; w++ ) pIn[w] = 0; } static inline void If_CluFill( word * pIn, int nVars ) { int w, nWords = If_CluWordNum( nVars ); for ( w = 0; w < nWords; w++ ) pIn[w] = ~0; } static inline void If_CluCopy( word * pOut, word * pIn, int nVars ) { int w, nWords = If_CluWordNum( nVars ); for ( w = 0; w < nWords; w++ ) pOut[w] = pIn[w]; } static inline int If_CluEqual( word * pOut, word * pIn, int nVars ) { int w, nWords = If_CluWordNum( nVars ); for ( w = 0; w < nWords; w++ ) if ( pOut[w] != pIn[w] ) return 0; return 1; } static inline void If_CluAnd( word * pRes, word * pIn1, word * pIn2, int nVars ) { int w, nWords = If_CluWordNum( nVars ); for ( w = 0; w < nWords; w++ ) pRes[w] = pIn1[w] & pIn2[w]; } static inline void If_CluSharp( word * pRes, word * pIn1, word * pIn2, int nVars ) { int w, nWords = If_CluWordNum( nVars ); for ( w = 0; w < nWords; w++ ) pRes[w] = pIn1[w] & ~pIn2[w]; } static inline void If_CluOr( word * pRes, word * pIn1, word * pIn2, int nVars ) { int w, nWords = If_CluWordNum( nVars ); for ( w = 0; w < nWords; w++ ) pRes[w] = pIn1[w] | pIn2[w]; } static inline word If_CluAdjust( word t, int nVars ) { assert( nVars >= 0 && nVars <= 6 ); if ( nVars == 6 ) return t; t &= (((word)1) << (1 << nVars)) - 1; if ( nVars == 0 ) t |= t << (1<> Shift); } else if ( iVar > 5 ) { int Step = (1 << (iVar - 6)); for ( k = 0; k < nWords; k += 4*Step ) { for ( i = 0; i < Step; i++ ) pOut[i] = pIn[i]; for ( i = 0; i < Step; i++ ) pOut[Step+i] = pIn[2*Step+i]; for ( i = 0; i < Step; i++ ) pOut[2*Step+i] = pIn[Step+i]; for ( i = 0; i < Step; i++ ) pOut[3*Step+i] = pIn[3*Step+i]; pIn += 4*Step; pOut += 4*Step; } } else // if ( iVar == 5 ) { for ( i = 0; i < nWords; i += 2 ) { pOut[i] = (pIn[i] & 0x00000000FFFFFFFF) | ((pIn[i+1] & 0x00000000FFFFFFFF) << 32); pOut[i+1] = (pIn[i+1] & 0xFFFFFFFF00000000) | ((pIn[i] & 0xFFFFFFFF00000000) >> 32); } } } void If_CluChangePhase( word * pF, int nVars, int iVar ) { int nWords = If_CluWordNum( nVars ); assert( iVar < nVars ); if ( iVar < 6 ) { int i, Shift = (1 << iVar); for ( i = 0; i < nWords; i++ ) pF[i] = ((pF[i] & ~Truth6[iVar]) << Shift) | ((pF[i] & Truth6[iVar]) >> Shift); } else { word Temp; int i, k, Step = (1 << (iVar - 6)); for ( k = 0; k < nWords; k += 2*Step ) { for ( i = 0; i < Step; i++ ) { Temp = pF[i]; pF[i] = pF[Step+i]; pF[Step+i] = Temp; } pF += 2*Step; } } } void If_CluCountOnesInCofs( word * pTruth, int nVars, int * pStore ) { int nWords = If_CluWordNum( nVars ); int i, k, nOnes = 0, Limit = Abc_MinInt( nVars, 6 ); memset( pStore, 0, sizeof(int) * 2 * nVars ); // compute positive cofactors for ( k = 0; k < nWords; k++ ) for ( i = 0; i < Limit; i++ ) pStore[2*i+1] += If_CluCountOnes( pTruth[k] & Truth6[i] ); if ( nVars > 6 ) for ( k = 0; k < nWords; k++ ) for ( i = 6; i < nVars; i++ ) if ( k & (1 << (i-6)) ) pStore[2*i+1] += If_CluCountOnes( pTruth[k] ); // compute negative cofactors for ( k = 0; k < nWords; k++ ) nOnes += If_CluCountOnes( pTruth[k] ); for ( i = 0; i < nVars; i++ ) pStore[2*i] = nOnes - pStore[2*i+1]; } unsigned If_CluSemiCanonicize( word * pTruth, int nVars, int * pCanonPerm ) { word pFunc[CLU_WRD_MAX], * pIn = pTruth, * pOut = pFunc, * pTemp; int pStore[CLU_VAR_MAX*2]; unsigned uCanonPhase = 0; int i, Temp, fChange, Counter = 0; //Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" ); // collect signatures If_CluCountOnesInCofs( pTruth, nVars, pStore ); // canonicize phase for ( i = 0; i < nVars; i++ ) { if ( pStore[2*i+0] <= pStore[2*i+1] ) continue; uCanonPhase |= (1 << i); Temp = pStore[2*i+0]; pStore[2*i+0] = pStore[2*i+1]; pStore[2*i+1] = Temp; If_CluChangePhase( pIn, nVars, i ); } // compute permutation for ( i = 0; i < nVars; i++ ) pCanonPerm[i] = i; do { fChange = 0; for ( i = 0; i < nVars-1; i++ ) { if ( pStore[2*i] <= pStore[2*(i+1)] ) continue; Counter++; fChange = 1; Temp = pCanonPerm[i]; pCanonPerm[i] = pCanonPerm[i+1]; pCanonPerm[i+1] = Temp; Temp = pStore[2*i]; pStore[2*i] = pStore[2*(i+1)]; pStore[2*(i+1)] = Temp; Temp = pStore[2*i+1]; pStore[2*i+1] = pStore[2*(i+1)+1]; pStore[2*(i+1)+1] = Temp; If_CluSwapAdjacent( pOut, pIn, i, nVars ); pTemp = pIn; pIn = pOut; pOut = pTemp; } } while ( fChange ); // swap if it was moved an odd number of times if ( Counter & 1 ) If_CluCopy( pOut, pIn, nVars ); return uCanonPhase; } void If_CluSemiCanonicizeVerify( word * pTruth, word * pTruth0, int nVars, int * pCanonPerm, unsigned uCanonPhase ) { word pFunc[CLU_WRD_MAX], pGunc[CLU_WRD_MAX], * pIn = pTruth, * pOut = pFunc, * pTemp; int i, Temp, fChange, Counter = 0; If_CluCopy( pGunc, pTruth, nVars ); // undo permutation do { fChange = 0; for ( i = 0; i < nVars-1; i++ ) { if ( pCanonPerm[i] < pCanonPerm[i+1] ) continue; Counter++; fChange = 1; Temp = pCanonPerm[i]; pCanonPerm[i] = pCanonPerm[i+1]; pCanonPerm[i+1] = Temp; If_CluSwapAdjacent( pOut, pIn, i, nVars ); pTemp = pIn; pIn = pOut; pOut = pTemp; } } while ( fChange ); if ( Counter & 1 ) If_CluCopy( pOut, pIn, nVars ); // undo phase for ( i = 0; i < nVars; i++ ) if ( (uCanonPhase >> i) & 1 ) If_CluChangePhase( pTruth, nVars, i ); // compare if ( !If_CluEqual(pTruth0, pTruth, nVars) ) { Kit_DsdPrintFromTruth( (unsigned*)pTruth0, nVars ); printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)pGunc, nVars ); printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" ); printf( "SemiCanonical verification FAILED!\n" ); } } void If_CluPrintGroup( If_Grp_t * g ) { int i; printf( "Vars = %d ", g->nVars ); printf( "Myu = %d {", g->nMyu ); for ( i = 0; i < g->nVars; i++ ) printf( " %c", 'a' + g->pVars[i] ); printf( " }\n" ); } void If_CluPrintConfig( int nVars, If_Grp_t * g, If_Grp_t * r, word BStruth, word * pFStruth ) { assert( r->nVars == nVars - g->nVars + 1 + (g->nMyu > 2) ); If_CluPrintGroup( g ); if ( g->nVars < 6 ) BStruth = If_CluAdjust( BStruth, g->nVars ); Kit_DsdPrintFromTruth( (unsigned *)&BStruth, g->nVars ); printf( "\n" ); If_CluPrintGroup( r ); if ( r->nVars < 6 ) pFStruth[0] = If_CluAdjust( pFStruth[0], r->nVars ); Kit_DsdPrintFromTruth( (unsigned *)pFStruth, r->nVars ); printf( "\n" ); } void If_CluInitTruthTables() { int i, k; assert( CLU_VAR_MAX <= 16 ); for ( i = 0; i < 6; i++ ) for ( k = 0; k < CLU_WRD_MAX; k++ ) TruthAll[i][k] = Truth6[i]; for ( i = 6; i < CLU_VAR_MAX; i++ ) for ( k = 0; k < CLU_WRD_MAX; k++ ) TruthAll[i][k] = ((k >> (i-6)) & 1) ? ~0 : 0; // Extra_PrintHex( stdout, TruthAll[6], 8 ); printf( "\n" ); // Extra_PrintHex( stdout, TruthAll[7], 8 ); printf( "\n" ); } // verification static void If_CluComposeLut( int nVars, If_Grp_t * g, word * t, word f[6][CLU_WRD_MAX], word * r ) { word c[CLU_WRD_MAX]; int m, v; If_CluClear( r, nVars ); for ( m = 0; m < (1<nVars); m++ ) { if ( !((t[m >> 6] >> (m & 63)) & 1) ) continue; If_CluFill( c, nVars ); for ( v = 0; v < g->nVars; v++ ) if ( (m >> v) & 1 ) If_CluAnd( c, c, f[v], nVars ); else If_CluSharp( c, c, f[v], nVars ); If_CluOr( r, r, c, nVars ); } } void If_CluVerify( word * pF, int nVars, If_Grp_t * g, If_Grp_t * r, word BStruth, word * pFStruth ) { word pTTFans[6][CLU_WRD_MAX], pTTWire[CLU_WRD_MAX], pTTRes[CLU_WRD_MAX]; int i; assert( g->nVars <= 6 && r->nVars <= 6 ); if ( TruthAll[0][0] == 0 ) If_CluInitTruthTables(); for ( i = 0; i < g->nVars; i++ ) If_CluCopy( pTTFans[i], TruthAll[(int)g->pVars[i]], nVars ); If_CluComposeLut( nVars, g, &BStruth, pTTFans, pTTWire ); for ( i = 0; i < r->nVars; i++ ) if ( r->pVars[i] == nVars ) If_CluCopy( pTTFans[i], pTTWire, nVars ); else If_CluCopy( pTTFans[i], TruthAll[(int)r->pVars[i]], nVars ); If_CluComposeLut( nVars, r, pFStruth, pTTFans, pTTRes ); if ( !If_CluEqual(pTTRes, pF, nVars) ) { printf( "\n" ); If_CluPrintConfig( nVars, g, r, BStruth, pFStruth ); Kit_DsdPrintFromTruth( (unsigned*)pTTRes, nVars ); printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); // Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( "\n" ); printf( "Verification FAILED!\n" ); } // else // printf( "Verification succeed!\n" ); } void If_CluVerify3( word * pF, int nVars, If_Grp_t * g, If_Grp_t * g2, If_Grp_t * r, word BStruth, word BStruth2, word FStruth ) { word pTTFans[6][CLU_WRD_MAX], pTTWire[CLU_WRD_MAX], pTTWire2[CLU_WRD_MAX], pTTRes[CLU_WRD_MAX]; int i; assert( g->nVars >= 2 && g2->nVars >= 2 && r->nVars >= 2 ); assert( g->nVars <= 6 && g2->nVars <= 6 && r->nVars <= 6 ); if ( TruthAll[0][0] == 0 ) If_CluInitTruthTables(); for ( i = 0; i < g->nVars; i++ ) If_CluCopy( pTTFans[i], TruthAll[(int)g->pVars[i]], nVars ); If_CluComposeLut( nVars, g, &BStruth, pTTFans, pTTWire ); for ( i = 0; i < g2->nVars; i++ ) If_CluCopy( pTTFans[i], TruthAll[(int)g2->pVars[i]], nVars ); If_CluComposeLut( nVars, g2, &BStruth2, pTTFans, pTTWire2 ); for ( i = 0; i < r->nVars; i++ ) if ( r->pVars[i] == nVars ) If_CluCopy( pTTFans[i], pTTWire, nVars ); else if ( r->pVars[i] == nVars + 1 ) If_CluCopy( pTTFans[i], pTTWire2, nVars ); else If_CluCopy( pTTFans[i], TruthAll[(int)r->pVars[i]], nVars ); If_CluComposeLut( nVars, r, &FStruth, pTTFans, pTTRes ); if ( !If_CluEqual(pTTRes, pF, nVars) ) { printf( "%d\n", nVars ); // If_CluPrintConfig( nVars, g, r, BStruth, pFStruth ); // Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)&BStruth, g->nVars ); printf( " " ); If_CluPrintGroup(g); // printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)&BStruth2, g2->nVars ); printf( " " ); If_CluPrintGroup(g2); // printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)&FStruth, r->nVars ); printf( " " ); If_CluPrintGroup(r); // printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)pTTWire, nVars ); printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)pTTWire2, nVars ); printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)pTTRes, nVars ); printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); // Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( "\n" ); printf( "Verification FAILED!\n" ); } // else // printf( "Verification succeed!\n" ); } void If_CluSwapVars( word * pTruth, int nVars, int * V2P, int * P2V, int iVar, int jVar ) { word low2High, high2Low, temp; int nWords = If_CluWordNum(nVars); int shift, step, iStep, jStep; int w = 0, i = 0, j = 0; static word PPMasks[6][6] = { { 0x2222222222222222, 0x0A0A0A0A0A0A0A0A, 0x00AA00AA00AA00AA, 0x0000AAAA0000AAAA, 0x00000000AAAAAAAA, 0xAAAAAAAAAAAAAAAA }, { 0x0000000000000000, 0x0C0C0C0C0C0C0C0C, 0x00CC00CC00CC00CC, 0x0000CCCC0000CCCC, 0x00000000CCCCCCCC, 0xCCCCCCCCCCCCCCCC }, { 0x0000000000000000, 0x0000000000000000, 0x00F000F000F000F0, 0x0000F0F00000F0F0, 0x00000000F0F0F0F0, 0xF0F0F0F0F0F0F0F0 }, { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000FF000000FF00, 0x00000000FF00FF00, 0xFF00FF00FF00FF00 }, { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x00000000FFFF0000, 0xFFFF0000FFFF0000 }, { 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0x0000000000000000, 0xFFFFFFFF00000000 } }; if( iVar == jVar ) return; if( jVar < iVar ) { int varTemp = jVar; jVar = iVar; iVar = varTemp; } if ( iVar <= 5 && jVar <= 5 ) { shift = (1 << jVar) - (1 << iVar); for ( w = 0; w < nWords; w++ ) { low2High = (pTruth[w] & PPMasks[iVar][jVar - 1] ) << shift; pTruth[w] &= ~PPMasks[iVar][jVar - 1]; high2Low = (pTruth[w] & (PPMasks[iVar][jVar - 1] << shift )) >> shift; pTruth[w] &= ~ (PPMasks[iVar][jVar - 1] << shift); pTruth[w] = pTruth[w] | low2High | high2Low; } } else if( iVar <= 5 && jVar > 5 ) { step = If_CluWordNum(jVar + 1)/2; shift = 1 << iVar; for ( w = 0; w < nWords; w += 2*step ) { for (j = 0; j < step; j++) { low2High = (pTruth[w + j] & PPMasks[iVar][5]) >> shift; pTruth[w + j] &= ~PPMasks[iVar][5]; high2Low = (pTruth[w + step + j] & (PPMasks[iVar][5] >> shift)) << shift; pTruth[w + step + j] &= ~(PPMasks[iVar][5] >> shift); pTruth[w + j] |= high2Low; pTruth[w + step + j] |= low2High; } } } else { iStep = If_CluWordNum(iVar + 1)/2; jStep = If_CluWordNum(jVar + 1)/2; for (w = 0; w < nWords; w += 2*jStep) { for (i = 0; i < jStep; i += 2*iStep) { for (j = 0; j < iStep; j++) { temp = pTruth[w + iStep + i + j]; pTruth[w + iStep + i + j] = pTruth[w + jStep + i + j]; pTruth[w + jStep + i + j] = temp; } } } } if ( V2P && P2V ) { V2P[P2V[iVar]] = jVar; V2P[P2V[jVar]] = iVar; P2V[iVar] ^= P2V[jVar]; P2V[jVar] ^= P2V[iVar]; P2V[iVar] ^= P2V[jVar]; } } void If_CluReverseOrder( word * pTruth, int nVars, int * V2P, int * P2V, int iVarStart ) { int i, j, k; for ( k = 0; k < (nVars-iVarStart)/2 ; k++ ) { i = iVarStart + k; j = nVars - 1 - k; If_CluSwapVars( pTruth, nVars, V2P, P2V, i, j ); } } // moves one var (v) to the given position (p) void If_CluMoveVar2( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, int p ) { If_CluSwapVars( pF, nVars, Var2Pla, Pla2Var, Var2Pla[v], p ); } // moves one var (v) to the given position (p) void If_CluMoveVar( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, int p ) { word pG[CLU_WRD_MAX], * pIn = pF, * pOut = pG, * pTemp; int iPlace0, iPlace1, Count = 0; assert( v >= 0 && v < nVars ); while ( Var2Pla[v] < p ) { iPlace0 = Var2Pla[v]; iPlace1 = Var2Pla[v]+1; If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars ); pTemp = pIn; pIn = pOut, pOut = pTemp; Var2Pla[Pla2Var[iPlace0]]++; Var2Pla[Pla2Var[iPlace1]]--; Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; Count++; } while ( Var2Pla[v] > p ) { iPlace0 = Var2Pla[v]-1; iPlace1 = Var2Pla[v]; If_CluSwapAdjacent( pOut, pIn, iPlace0, nVars ); pTemp = pIn; pIn = pOut, pOut = pTemp; Var2Pla[Pla2Var[iPlace0]]++; Var2Pla[Pla2Var[iPlace1]]--; Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; Count++; } if ( Count & 1 ) If_CluCopy( pF, pIn, nVars ); assert( Pla2Var[p] == v ); } // moves vars to be the most signiticant ones (Group[0] is MSB) void If_CluMoveGroupToMsb( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g ) { int v; for ( v = 0; v < g->nVars; v++ ) If_CluMoveVar( pF, nVars, V2P, P2V, g->pVars[g->nVars - 1 - v], nVars - 1 - v ); } // reverses the variable order void If_CluReverseOrder_old( word * pF, int nVars, int * V2P, int * P2V, int iVarStart ) { word pG[CLU_WRD_MAX]; int v; If_CluCopy( pG, pF, nVars ); // for ( v = 0; v < nVars; v++ ) // printf( "%c ", 'a' + P2V[v] ); // printf( " --- " ); for ( v = iVarStart; v < nVars; v++ ) If_CluMoveVar( pF, nVars, V2P, P2V, P2V[iVarStart], nVars - 1 - (v - iVarStart) ); // for ( v = 0; v < nVars; v++ ) // printf( "%c ", 'a' + P2V[v] ); // printf( "\n" ); // if ( iVarStart > 0 ) // return; If_CluReverseOrder( pG, nVars, NULL, NULL, iVarStart ); if ( If_CluEqual( pG, pF, nVars ) ) { // printf( "+" ); } else { /* printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); Kit_DsdPrintFromTruth( (unsigned*)pG, nVars ); printf( "\n" ); */ printf( "%d ", nVars ); } } // return the number of cofactors w.r.t. the topmost vars (nBSsize) int If_CluCountCofs( word * pF, int nVars, int nBSsize, int iShift, word pCofs[3][CLU_WRD_MAX/4] ) { word iCofs[128], iCof, Result = 0; word * pCofA, * pCofB; int nMints = (1 << nBSsize); int i, c, w, nCofs; assert( nBSsize >= 2 && nBSsize <= 7 && nBSsize < nVars ); if ( nVars - nBSsize < 6 ) { int nShift = (1 << (nVars - nBSsize)); word Mask = ((((word)1) << nShift) - 1); for ( nCofs = i = 0; i < nMints; i++ ) { iCof = (pF[(iShift + i * nShift) / 64] >> ((iShift + i * nShift) & 63)) & Mask; for ( c = 0; c < nCofs; c++ ) if ( iCof == iCofs[c] ) break; if ( c == nCofs ) iCofs[nCofs++] = iCof; if ( pCofs && iCof != iCofs[0] ) Result |= (((word)1) << i); if ( nCofs == 5 ) break; } if ( nCofs <= 2 && pCofs ) { assert( nBSsize <= 6 ); pCofs[0][0] = iCofs[0]; pCofs[1][0] = (nCofs == 2) ? iCofs[1] : iCofs[0]; pCofs[2][0] = Result; } } else { int nWords = If_CluWordNum( nVars - nBSsize ); assert( nWords * nMints == If_CluWordNum(nVars) ); for ( nCofs = i = 0; i < nMints; i++ ) { pCofA = pF + i * nWords; for ( c = 0; c < nCofs; c++ ) { pCofB = pF + iCofs[c] * nWords; for ( w = 0; w < nWords; w++ ) if ( pCofA[w] != pCofB[w] ) break; if ( w == nWords ) break; } if ( c == nCofs ) iCofs[nCofs++] = i; if ( pCofs ) { assert( nBSsize <= 6 ); pCofB = pF + iCofs[0] * nWords; for ( w = 0; w < nWords; w++ ) if ( pCofA[w] != pCofB[w] ) break; if ( w != nWords ) Result |= (((word)1) << i); } if ( nCofs == 5 ) break; } if ( nCofs <= 2 && pCofs ) { If_CluCopy( pCofs[0], pF + iCofs[0] * nWords, nVars - nBSsize ); If_CluCopy( pCofs[1], pF + ((nCofs == 2) ? iCofs[1] : iCofs[0]) * nWords, nVars - nBSsize ); pCofs[2][0] = Result; } } assert( nCofs >= 1 && nCofs <= 5 ); return nCofs; } // return the number of cofactors w.r.t. the topmost vars (nBSsize) int If_CluCountCofs4( word * pF, int nVars, int nBSsize, word pCofs[6][CLU_WRD_MAX/4] ) { word iCofs[128], iCof, Result0 = 0, Result1 = 0; int nMints = (1 << nBSsize); int i, c, nCofs; assert( pCofs ); assert( nBSsize >= 2 && nBSsize <= 6 && nBSsize < nVars ); if ( nVars - nBSsize < 6 ) { int nShift = (1 << (nVars - nBSsize)); word Mask = ((((word)1) << nShift) - 1); for ( nCofs = i = 0; i < nMints; i++ ) { iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask; for ( c = 0; c < nCofs; c++ ) if ( iCof == iCofs[c] ) break; if ( c == nCofs ) iCofs[nCofs++] = iCof; if ( c == 1 || c == 3 ) Result0 |= (((word)1) << i); if ( c == 2 || c == 3 ) Result1 |= (((word)1) << i); } assert( nCofs >= 3 && nCofs <= 4 ); pCofs[0][0] = iCofs[0]; pCofs[1][0] = iCofs[1]; pCofs[2][0] = iCofs[2]; pCofs[3][0] = (nCofs == 4) ? iCofs[3] : iCofs[2]; pCofs[4][0] = Result0; pCofs[5][0] = Result1; } else assert( 0 ); return nCofs; } void If_CluCofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1 ) { int nWords = If_CluWordNum( nVars ); assert( iVar < nVars ); if ( iVar < 6 ) { int i, Shift = (1 << iVar); for ( i = 0; i < nWords; i++ ) { pCof0[i] = (pF[i] & ~Truth6[iVar]) | ((pF[i] & ~Truth6[iVar]) << Shift); pCof1[i] = (pF[i] & Truth6[iVar]) | ((pF[i] & Truth6[iVar]) >> Shift); } } else { int i, k, Step = (1 << (iVar - 6)); for ( k = 0; k < nWords; k += 2*Step ) { for ( i = 0; i < Step; i++ ) { pCof0[i] = pCof0[Step+i] = pF[i]; pCof1[i] = pCof1[Step+i] = pF[Step+i]; } pF += 2*Step; pCof0 += 2*Step; pCof1 += 2*Step; } } } // returns 1 if we have special case of cofactors; otherwise, returns 0 int If_CluDetectSpecialCaseCofs( word * pF, int nVars, int iVar ) { word Cof0, Cof1; int State[6] = {0}; int i, nWords = If_CluWordNum( nVars ); assert( iVar < nVars ); if ( iVar < 6 ) { int Shift = (1 << iVar); for ( i = 0; i < nWords; i++ ) { Cof0 = (pF[i] & ~Truth6[iVar]); Cof1 = ((pF[i] & Truth6[iVar]) >> Shift); if ( Cof0 == 0 ) State[0]++; else if ( Cof0 == ~Truth6[iVar] ) State[1]++; else if ( Cof1 == 0 ) State[2]++; else if ( Cof1 == ~Truth6[iVar] ) State[3]++; else if ( Cof0 == ~Cof1 ) State[4]++; else if ( Cof0 == Cof1 ) State[5]++; } } else { int k, Step = (1 << (iVar - 6)); for ( k = 0; k < nWords; k += 2*Step ) { for ( i = 0; i < Step; i++ ) { Cof0 = pF[i]; Cof1 = pF[Step+i]; if ( Cof0 == 0 ) State[0]++; else if ( Cof0 == ~0 ) State[1]++; else if ( Cof1 == 0 ) State[2]++; else if ( Cof1 == ~0 ) State[3]++; else if ( Cof0 == ~Cof1 ) State[4]++; else if ( Cof0 == Cof1 ) State[5]++; } pF += 2*Step; } nWords /= 2; } assert( State[5] != nWords ); for ( i = 0; i < 5; i++ ) { assert( State[i] <= nWords ); if ( State[i] == nWords ) return i; } return -1; } // returns 1 if we have special case of cofactors; otherwise, returns 0 If_Grp_t If_CluDecUsingCofs( word * pTruth, int nVars, int nLutLeaf ) { If_Grp_t G = {0}; word pF2[CLU_WRD_MAX], * pF = pF2; int Var2Pla[CLU_VAR_MAX+2], Pla2Var[CLU_VAR_MAX+2]; int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2]; int nVarsNeeded = nVars - nLutLeaf; int v, i, k, iVar, State; //Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" ); // create local copy If_CluCopy( pF, pTruth, nVars ); for ( k = 0; k < nVars; k++ ) Var2Pla[k] = Pla2Var[k] = k; // find decomposable vars for ( i = 0; i < nVarsNeeded; i++ ) { for ( v = nVars - 1; v >= 0; v-- ) { State = If_CluDetectSpecialCaseCofs( pF, nVars, v ); if ( State == -1 ) continue; // update the variable place iVar = Pla2Var[v]; while ( Var2Pla[iVar] < nVars - 1 ) { int iPlace0 = Var2Pla[iVar]; int iPlace1 = Var2Pla[iVar]+1; Var2Pla[Pla2Var[iPlace0]]++; Var2Pla[Pla2Var[iPlace1]]--; Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; Pla2Var[iPlace1] ^= Pla2Var[iPlace0]; Pla2Var[iPlace0] ^= Pla2Var[iPlace1]; } // move this variable to the top for ( k = 0; k < nVars; k++ ) V2P[k] = P2V[k] = k; //Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); If_CluMoveVar( pF, nVars, V2P, P2V, v, nVars - 1 ); //Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); // choose cofactor to follow iVar = nVars - 1; if ( State == 0 || State == 1 ) // need cof1 { if ( iVar < 6 ) pF[0] = (pF[0] & Truth6[iVar]) | ((pF[0] & Truth6[iVar]) >> (1 << iVar)); else pF += If_CluWordNum( nVars ) / 2; } else // need cof0 { if ( iVar < 6 ) pF[0] = (pF[0] & ~Truth6[iVar]) | ((pF[0] & ~Truth6[iVar]) << (1 << iVar)); } // update the variable count nVars--; break; } if ( v == -1 ) return G; } // create the resulting group G.nVars = nLutLeaf; G.nMyu = 2; for ( v = 0; v < G.nVars; v++ ) G.pVars[v] = Pla2Var[v]; return G; } // deriving decomposition word If_CluDeriveDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * r ) { word pCofs[3][CLU_WRD_MAX/4]; int i, RetValue, nFSset = nVars - g->nVars; RetValue = If_CluCountCofs( pF, nVars, g->nVars, 0, pCofs ); // assert( RetValue == 2 ); if ( nFSset < 6 ) pF[0] = (pCofs[1][0] << (1 << nFSset)) | pCofs[0][0]; else { If_CluCopy( pF, pCofs[0], nFSset ); If_CluCopy( pF + If_CluWordNum(nFSset), pCofs[1], nFSset ); } // create the resulting group if ( r ) { r->nVars = nFSset + 1; r->nMyu = 0; for ( i = 0; i < nFSset; i++ ) r->pVars[i] = P2V[i]; r->pVars[nFSset] = nVars; } return pCofs[2][0]; } void If_CluDeriveDisjoint4( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * r, word * pTruth0, word * pTruth1 ) { word pCofs[6][CLU_WRD_MAX/4]; word Cof0, Cof1; int i, RetValue, nFSset = nVars - g->nVars; assert( g->nVars <= 6 && nFSset <= 4 ); RetValue = If_CluCountCofs4( pF, nVars, g->nVars, pCofs ); if ( RetValue != 3 && RetValue != 4 ) printf( "If_CluDeriveDisjoint4(): Error!!!\n" ); Cof0 = (pCofs[1][0] << (1 << nFSset)) | pCofs[0][0]; Cof1 = (pCofs[3][0] << (1 << nFSset)) | pCofs[2][0]; pF[0] = (Cof1 << (1 << (nFSset+1))) | Cof0; pF[0] = If_CluAdjust( pF[0], nFSset + 2 ); // create the resulting group r->nVars = nFSset + 2; r->nMyu = 0; for ( i = 0; i < nFSset; i++ ) r->pVars[i] = P2V[i]; r->pVars[nFSset] = nVars; r->pVars[nFSset+1] = nVars+1; *pTruth0 = If_CluAdjust( pCofs[4][0], g->nVars ); *pTruth1 = If_CluAdjust( pCofs[5][0], g->nVars ); } word If_CluDeriveNonDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g, If_Grp_t * r ) { word pCofs[2][CLU_WRD_MAX]; word Truth0, Truth1, Truth; int i, nFSset = nVars - g->nVars, nFSset1 = nFSset + 1; If_CluCofactors( pF, nVars, nVars - 1, pCofs[0], pCofs[1] ); // Extra_PrintHex( stdout, (unsigned *)pCofs[0], nVars ); printf( "\n" ); // Extra_PrintHex( stdout, (unsigned *)pCofs[1], nVars ); printf( "\n" ); g->nVars--; Truth0 = If_CluDeriveDisjoint( pCofs[0], nVars - 1, V2P, P2V, g, NULL ); Truth1 = If_CluDeriveDisjoint( pCofs[1], nVars - 1, V2P, P2V, g, NULL ); Truth = (Truth1 << (1 << g->nVars)) | Truth0; g->nVars++; if ( nFSset1 < 6 ) pF[0] = (pCofs[1][0] << (1 << nFSset1)) | pCofs[0][0]; else { If_CluCopy( pF, pCofs[0], nFSset1 ); If_CluCopy( pF + If_CluWordNum(nFSset1), pCofs[1], nFSset1 ); } // Extra_PrintHex( stdout, (unsigned *)&Truth0, 6 ); printf( "\n" ); // Extra_PrintHex( stdout, (unsigned *)&Truth1, 6 ); printf( "\n" ); // Extra_PrintHex( stdout, (unsigned *)&pCofs[0][0], 6 ); printf( "\n" ); // Extra_PrintHex( stdout, (unsigned *)&pCofs[1][0], 6 ); printf( "\n" ); // Extra_PrintHex( stdout, (unsigned *)&Truth, 6 ); printf( "\n" ); // Extra_PrintHex( stdout, (unsigned *)&pF[0], 6 ); printf( "\n" ); // create the resulting group r->nVars = nFSset + 2; r->nMyu = 0; for ( i = 0; i < nFSset; i++ ) r->pVars[i] = P2V[i]; r->pVars[nFSset] = nVars; r->pVars[nFSset+1] = g->pVars[g->nVars - 1]; return Truth; } // check non-disjoint decomposition int If_CluCheckNonDisjointGroup( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t * g ) { int v, i, nCofsBest2; if ( (g->nMyu == 3 || g->nMyu == 4) ) { word pCofs[2][CLU_WRD_MAX]; // try cofactoring w.r.t. each variable for ( v = 0; v < g->nVars; v++ ) { If_CluCofactors( pF, nVars, V2P[(int)g->pVars[v]], pCofs[0], pCofs[1] ); nCofsBest2 = If_CluCountCofs( pCofs[0], nVars, g->nVars, 0, NULL ); if ( nCofsBest2 > 2 ) continue; nCofsBest2 = If_CluCountCofs( pCofs[1], nVars, g->nVars, 0, NULL ); if ( nCofsBest2 > 2 ) continue; // found good shared variable - move to the end If_CluMoveVar( pF, nVars, V2P, P2V, g->pVars[v], nVars-1 ); for ( i = 0; i < g->nVars; i++ ) g->pVars[i] = P2V[nVars-g->nVars+i]; return 1; } } return 0; } // finds a good var group (cof count < 6; vars are MSBs) If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int * P2V, int nBSsize, int fDisjoint ) { int fVerbose = 0; int nRounds = 2;//nBSsize; If_Grp_t G = {0}, * g = &G;//, BestG = {0}; int i, r, v, nCofs, VarBest, nCofsBest2; assert( nVars > nBSsize && nVars >= nBSsize + iVarStart && nVars <= CLU_VAR_MAX ); assert( nBSsize >= 2 && nBSsize <= 6 ); // start with the default group g->nVars = nBSsize; g->nMyu = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL ); for ( i = 0; i < nBSsize; i++ ) g->pVars[i] = P2V[nVars-nBSsize+i]; // check if good enough if ( g->nMyu == 2 ) return G; if ( !fDisjoint && If_CluCheckNonDisjointGroup( pF, nVars, V2P, P2V, g ) ) { // BestG = G; return G; } if ( nVars == nBSsize + iVarStart ) { g->nVars = 0; return G; } if ( fVerbose ) { printf( "Iter %2d ", -1 ); If_CluPrintGroup( g ); } // try to find better group for ( r = 0; r < nRounds; r++ ) { if ( nBSsize < nVars-1 ) { // find the best var to add VarBest = P2V[nVars-1-nBSsize]; nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); for ( v = nVars-2-nBSsize; v >= iVarStart; v-- ) { // If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); If_CluMoveVar2( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); if ( nCofsBest2 >= nCofs ) { nCofsBest2 = nCofs; VarBest = P2V[nVars-1-nBSsize]; } } // go back // If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); If_CluMoveVar2( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); // update best bound set nCofs = If_CluCountCofs( pF, nVars, nBSsize+1, 0, NULL ); assert( nCofs == nCofsBest2 ); } // find the best var to remove VarBest = P2V[nVars-1-nBSsize]; nCofsBest2 = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL ); for ( v = nVars-nBSsize; v < nVars; v++ ) { // If_CluMoveVar( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); If_CluMoveVar2( pF, nVars, V2P, P2V, P2V[v], nVars-1-nBSsize ); nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL ); if ( nCofsBest2 >= nCofs ) { nCofsBest2 = nCofs; VarBest = P2V[nVars-1-nBSsize]; } } // go back // If_CluMoveVar( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); If_CluMoveVar2( pF, nVars, V2P, P2V, VarBest, nVars-1-nBSsize ); // update best bound set nCofs = If_CluCountCofs( pF, nVars, nBSsize, 0, NULL ); assert( nCofs == nCofsBest2 ); if ( g->nMyu >= nCofs ) { g->nVars = nBSsize; g->nMyu = nCofs; for ( i = 0; i < nBSsize; i++ ) g->pVars[i] = P2V[nVars-nBSsize+i]; } if ( fVerbose ) { printf( "Iter %2d ", r ); If_CluPrintGroup( g ); } // check if good enough if ( g->nMyu == 2 ) return G; if ( !fDisjoint && If_CluCheckNonDisjointGroup( pF, nVars, V2P, P2V, g ) ) { // BestG = G; return G; } } assert( r == nRounds ); g->nVars = 0; return G; // return BestG; } // double check that the given group has a decomposition void If_CluCheckGroup( word * pTruth, int nVars, If_Grp_t * g ) { word pF[CLU_WRD_MAX]; int v, nCofs, V2P[CLU_VAR_MAX], P2V[CLU_VAR_MAX]; assert( g->nVars >= 2 && g->nVars <= 6 ); // vars assert( g->nMyu >= 2 && g->nMyu <= 4 ); // cofs // create permutation for ( v = 0; v < nVars; v++ ) V2P[v] = P2V[v] = v; // create truth table If_CluCopy( pF, pTruth, nVars ); // move group up If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, g ); // check the number of cofactors nCofs = If_CluCountCofs( pF, nVars, g->nVars, 0, NULL ); if ( nCofs != g->nMyu ) printf( "Group check 0 has failed.\n" ); // check compatible if ( nCofs > 2 ) { nCofs = If_CluCountCofs( pF, nVars-1, g->nVars-1, 0, NULL ); if ( nCofs > 2 ) printf( "Group check 1 has failed.\n" ); nCofs = If_CluCountCofs( pF, nVars-1, g->nVars-1, (1 << (nVars-1)), NULL ); if ( nCofs > 2 ) printf( "Group check 2 has failed.\n" ); } } // double check that the permutation derived is correct void If_CluCheckPerm( word * pTruth, word * pF, int nVars, int * V2P, int * P2V ) { int i; for ( i = 0; i < nVars; i++ ) If_CluMoveVar( pF, nVars, V2P, P2V, i, i ); if ( !If_CluEqual( pTruth, pF, nVars ) ) printf( "Permutation FAILED.\n" ); // else // printf( "Permutation successful\n" ); } static inline int If_CluSuppIsMinBase( int Supp ) { return (Supp & (Supp+1)) == 0; } static inline int If_CluHasVar( word * t, int nVars, int iVar ) { int nWords = If_CluWordNum( nVars ); assert( iVar < nVars ); if ( iVar < 6 ) { int i, Shift = (1 << iVar); for ( i = 0; i < nWords; i++ ) if ( (t[i] & ~Truth6[iVar]) != ((t[i] & Truth6[iVar]) >> Shift) ) return 1; return 0; } else { int i, k, Step = (1 << (iVar - 6)); for ( k = 0; k < nWords; k += 2*Step ) { for ( i = 0; i < Step; i++ ) if ( t[i] != t[Step+i] ) return 1; t += 2*Step; } return 0; } } static inline int If_CluSupport( word * t, int nVars ) { int v, Supp = 0; for ( v = 0; v < nVars; v++ ) if ( If_CluHasVar( t, nVars, v ) ) Supp |= (1 << v); return Supp; } int If_CluSupportSize( word * t, int nVars ) { int v, SuppSize = 0; for ( v = 0; v < nVars; v++ ) if ( If_CluHasVar( t, nVars, v ) ) SuppSize++; return SuppSize; } static inline void If_CluTruthShrink( word * pF, int nVars, int nVarsAll, unsigned Phase ) { word pG[CLU_WRD_MAX], * pIn = pF, * pOut = pG, * pTemp; int i, k, Var = 0, Counter = 0; assert( nVarsAll <= 16 ); for ( i = 0; i < nVarsAll; i++ ) if ( Phase & (1 << i) ) { for ( k = i-1; k >= Var; k-- ) { If_CluSwapAdjacent( pOut, pIn, k, nVarsAll ); pTemp = pIn; pIn = pOut, pOut = pTemp; Counter++; } Var++; } assert( Var == nVars ); // swap if it was moved an odd number of times if ( Counter & 1 ) If_CluCopy( pOut, pIn, nVarsAll ); } int If_CluMinimumBase( word * t, int * pSupp, int nVarsAll, int * pnVars ) { int v, iVar = 0, uSupp = 0; assert( nVarsAll <= 16 ); for ( v = 0; v < nVarsAll; v++ ) if ( If_CluHasVar( t, nVarsAll, v ) ) { uSupp |= (1 << v); if ( pSupp ) pSupp[iVar] = pSupp[v]; iVar++; } if ( pnVars ) *pnVars = iVar; if ( If_CluSuppIsMinBase( uSupp ) ) return 0; If_CluTruthShrink( t, iVar, nVarsAll, uSupp ); return 1; } // returns the best group found If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int iVarStart, int nLutLeaf, int nLutRoot, If_Grp_t * pR, word * pFunc0, word * pFunc1, word * pLeftOver, int fHashing ) { // int fEnableHashing = 0; If_Grp_t G1 = {0}, R = {0}; unsigned * pHashed = NULL; word Truth, pTruth[CLU_WRD_MAX], pF[CLU_WRD_MAX];//, pG[CLU_WRD_MAX]; int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2], pCanonPerm[CLU_VAR_MAX]; int i, nSupp, uCanonPhase; int nLutSize = p ? p->pPars->nLutSize : nVars; assert( nVars <= CLU_VAR_MAX ); assert( nVars <= nLutLeaf + nLutRoot - 1 ); if ( pR ) { pR->nVars = 0; *pFunc0 = 0; *pFunc1 = 0; } // canonicize truth table If_CluCopy( pTruth, pTruth0, nLutSize ); if ( 0 ) { uCanonPhase = If_CluSemiCanonicize( pTruth, nVars, pCanonPerm ); If_CluAdjustBig( pTruth, nVars, nLutSize ); } // If_CluSemiCanonicizeVerify( pTruth, pTruth0, nVars, pCanonPerm, uCanonPhase ); // If_CluCopy( pTruth, pTruth0, nLutSize ); /* { int pCanonPerm[32]; short pStore[32]; unsigned uCanonPhase; If_CluCopy( pF, pTruth, nVars ); uCanonPhase = Kit_TruthSemiCanonicize( pF, pG, nVars, pCanonPerm, pStore ); G1.nVars = 1; return G1; } */ // check minnimum base If_CluCopy( pF, pTruth, nVars ); for ( i = 0; i < nVars; i++ ) V2P[i] = P2V[i] = i; // check support nSupp = If_CluSupport( pF, nVars ); //Extra_PrintBinary( stdout, &nSupp, 16 ); printf( "\n" ); if ( !nSupp || !If_CluSuppIsMinBase(nSupp) ) { // assert( 0 ); return G1; } // check hash table if ( p && fHashing ) { pHashed = If_CluHashLookup( p, pTruth, 0 ); if ( pHashed && *pHashed != CLU_UNUSED ) If_CluUns2Grp( *pHashed, &G1 ); } if ( G1.nVars == 0 ) { // detect easy cofs if ( iVarStart == 0 ) G1 = If_CluDecUsingCofs( pTruth, nVars, nLutLeaf ); if ( G1.nVars == 0 ) { // perform testing G1 = If_CluFindGroup( pF, nVars, iVarStart, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 ); // If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V ); if ( G1.nVars == 0 ) { // perform testing with a smaller set if ( nVars < nLutLeaf + nLutRoot - 2 ) { nLutLeaf--; G1 = If_CluFindGroup( pF, nVars, iVarStart, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 ); nLutLeaf++; } // perform testing with a smaller set if ( nLutLeaf > 4 && nVars < nLutLeaf + nLutRoot - 3 ) { nLutLeaf--; nLutLeaf--; G1 = If_CluFindGroup( pF, nVars, iVarStart, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 ); nLutLeaf++; nLutLeaf++; } if ( G1.nVars == 0 ) { // perform testing with a different order If_CluReverseOrder( pF, nVars, V2P, P2V, iVarStart ); G1 = If_CluFindGroup( pF, nVars, iVarStart, V2P, P2V, nLutLeaf, nLutLeaf + nLutRoot == nVars + 1 ); // check permutation // If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V ); if ( G1.nVars == 0 ) { // remember free set, just in case // for ( i = 0; i < nVars - nLutLeaf; i++ ) /// G1.pVars[nLutLeaf+i] = P2V[i]; // if , this will not be used // if , this will not be hashed /* if ( nVars == 6 ) { Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( " " ); Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" ); if ( !If_CutPerformCheck07( (unsigned *)pF, 6, 6, NULL ) ) printf( "no\n" ); } */ if ( pHashed ) *pHashed = If_CluGrp2Uns( &G1 ); return G1; } } } } } // derive if ( pR ) { int iNewPos; If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, &G1 ); if ( G1.nMyu == 2 ) { Truth = If_CluDeriveDisjoint( pF, nVars, V2P, P2V, &G1, &R ); iNewPos = R.nVars - 1; } else { Truth = If_CluDeriveNonDisjoint( pF, nVars, V2P, P2V, &G1, &R ); iNewPos = R.nVars - 2; } assert( R.pVars[iNewPos] == nVars ); // adjust the functions Truth = If_CluAdjust( Truth, G1.nVars ); if ( R.nVars < 6 ) pF[0] = If_CluAdjust( pF[0], R.nVars ); // Kit_DsdPrintFromTruth( (unsigned*)&Truth, G1.nVars ); printf( " ...1\n" ); // Kit_DsdPrintFromTruth( (unsigned*)pF, R.nVars ); printf( " ...1\n" ); // update the variable order of R so that the new var was the first one // if ( iVarStart == 0 ) { int k, V2P2[CLU_VAR_MAX+2], P2V2[CLU_VAR_MAX+2]; assert( iNewPos >= iVarStart ); for ( k = 0; k < R.nVars; k++ ) V2P2[k] = P2V2[k] = k; If_CluMoveVar( pF, R.nVars, V2P2, P2V2, iNewPos, iVarStart ); for ( k = iNewPos; k > iVarStart; k-- ) R.pVars[k] = R.pVars[k-1]; R.pVars[iVarStart] = nVars; } // Kit_DsdPrintFromTruth( (unsigned*)pF, R.nVars ); printf( " ...2\n" ); if ( pLeftOver ) { if ( R.nVars < 6 ) *pLeftOver = If_CluAdjust( pF[0], R.nVars ); else If_CluCopy( pLeftOver, pF, R.nVars ); If_CluAdjustBig( pLeftOver, R.nVars, nLutSize ); } // perform checking if ( 0 ) { If_CluCheckGroup( pTruth, nVars, &G1 ); If_CluVerify( pTruth, nVars, &G1, &R, Truth, pF ); } // save functions *pR = R; if ( pFunc0 ) *pFunc0 = pF[0]; if ( pFunc1 ) *pFunc1 = Truth; } if ( pHashed ) *pHashed = If_CluGrp2Uns( &G1 ); return G1; } // returns the best group found If_Grp_t If_CluCheck3( If_Man_t * p, word * pTruth0, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot, If_Grp_t * pR, If_Grp_t * pG2, word * pFunc0, word * pFunc1, word * pFunc2 ) { int fEnableHashing = 1; static int Counter = 0; unsigned * pHashed = NULL; word pLeftOver[CLU_WRD_MAX], Func0, Func1, Func2; If_Grp_t G1 = {0}, G2 = {0}, R = {0}, R2 = {0}; int i; Counter++; // if ( Counter == 37590 ) // { // int ns = 0; // } // check hash table if ( p && fEnableHashing ) { pHashed = If_CluHashLookup( p, pTruth0, 1 ); if ( pHashed && *pHashed != CLU_UNUSED ) { If_CluUns2Grp( *pHashed, &G1 ); return G1; } } // check two-node decomposition G1 = If_CluCheck( p, pTruth0, nVars, 0, nLutLeaf, nLutRoot + nLutLeaf2 - 1, &R2, &Func0, &Func1, pLeftOver, 0 ); // decomposition does not exist if ( G1.nVars == 0 ) { // check for decomposition with two outputs if ( (G1.nMyu == 3 || G1.nMyu == 4) && nLutLeaf == nLutLeaf2 && nVars - nLutLeaf + 2 <= nLutRoot ) { int V2P[CLU_VAR_MAX+2], P2V[CLU_VAR_MAX+2]; word Func0, Func1, Func2; int iVar0, iVar1; G1.nVars = nLutLeaf; If_CluCopy( pLeftOver, pTruth0, nVars ); for ( i = 0; i < nVars; i++ ) V2P[i] = P2V[i] = i; If_CluMoveGroupToMsb( pLeftOver, nVars, V2P, P2V, &G1 ); If_CluDeriveDisjoint4( pLeftOver, nVars, V2P, P2V, &G1, &R, &Func1, &Func2 ); // move the two vars to the front for ( i = 0; i < R.nVars; i++ ) V2P[i] = P2V[i] = i; If_CluMoveVar( pLeftOver, R.nVars, V2P, P2V, R.nVars-2, 0 ); If_CluMoveVar( pLeftOver, R.nVars, V2P, P2V, R.nVars-1, 1 ); iVar0 = R.pVars[R.nVars-2]; iVar1 = R.pVars[R.nVars-1]; for ( i = R.nVars-1; i > 1; i-- ) R.pVars[i] = R.pVars[i-2]; R.pVars[0] = iVar0; R.pVars[1] = iVar1; Func0 = pLeftOver[0]; If_CluVerify3( pTruth0, nVars, &G1, &G1, &R, Func1, Func2, Func0 ); if ( pFunc1 && pFunc2 ) { *pFunc0 = Func0; *pFunc1 = Func1; *pFunc2 = Func2; *pG2 = G1; *pR = R; } if ( pHashed ) *pHashed = If_CluGrp2Uns( &G1 ); // Kit_DsdPrintFromTruth( (unsigned*)pTruth0, nVars ); printf( "\n" ); // If_CluPrintGroup( &G1 ); return G1; } /* // if ( nVars == 6 ) { // Extra_PrintHex( stdout, (unsigned *)pTruth0, nVars ); printf( " " ); Kit_DsdPrintFromTruth( (unsigned*)pTruth0, nVars ); printf( "\n" ); if ( p != NULL ) If_CluCheck3( NULL, pTruth0, nVars, nLutLeaf, nLutLeaf2, nLutRoot, pR, pG2, pFunc0, pFunc1, pFunc2 ); } */ if ( pHashed ) *pHashed = If_CluGrp2Uns( &G1 ); return G1; } // decomposition exists and sufficient if ( R2.nVars <= nLutRoot ) { if ( pG2 ) *pG2 = G2; if ( pR ) *pR = R2; if ( pFunc0 ) *pFunc0 = Func0; if ( pFunc1 ) *pFunc1 = Func1; if ( pFunc2 ) *pFunc2 = 0; if ( pHashed ) *pHashed = If_CluGrp2Uns( &G1 ); return G1; } // try second decomposition { int Test = 0; if ( Test ) { Kit_DsdPrintFromTruth( (unsigned*)&pLeftOver, R2.nVars ); printf( "\n" ); } } // the new variable is at the bottom - skip it (iVarStart = 1) #ifdef IF_USE_CASE3 G2 = If_CluCheck( p, pLeftOver, R2.nVars, 0, nLutLeaf2, nLutRoot, &R, &Func0, &Func2, NULL, 0 ); #else G2 = If_CluCheck( p, pLeftOver, R2.nVars, 1, nLutLeaf2, nLutRoot, &R, &Func0, &Func2, NULL, 0 ); #endif if ( G2.nVars == 0 ) { if ( pHashed ) *pHashed = If_CluGrp2Uns( &G2 ); return G2; } // remap variables for ( i = 0; i < G2.nVars; i++ ) { assert( G2.pVars[i] < R2.nVars ); G2.pVars[i] = R2.pVars[ (int)G2.pVars[i] ]; } // remap variables for ( i = 0; i < R.nVars; i++ ) { if ( R.pVars[i] == R2.nVars ) R.pVars[i] = nVars + 1; else R.pVars[i] = R2.pVars[ (int)R.pVars[i] ]; } // decomposition exist if ( pG2 ) *pG2 = G2; if ( pR ) *pR = R; if ( pFunc0 ) *pFunc0 = Func0; if ( pFunc1 ) *pFunc1 = Func1; if ( pFunc2 ) *pFunc2 = Func2; if ( pHashed ) *pHashed = If_CluGrp2Uns( &G1 ); // verify // If_CluVerify3( pTruth0, nVars, &G1, &G2, &R, Func1, Func2, Func0 ); return G1; } // returns the best group found int If_CluCheckExt( void * pMan, word * pTruth, int nVars, int nLutLeaf, int nLutRoot, char * pLut0, char * pLut1, word * pFunc0, word * pFunc1 ) { If_Man_t * p = (If_Man_t *)pMan; If_Grp_t G, R; G = If_CluCheck( p, pTruth, nVars, 0, nLutLeaf, nLutRoot, &R, pFunc0, pFunc1, NULL, 0 ); memcpy( pLut0, &R, sizeof(If_Grp_t) ); memcpy( pLut1, &G, sizeof(If_Grp_t) ); // memcpy( pLut2, &G2, sizeof(If_Grp_t) ); return (G.nVars > 0); } // returns the best group found int If_CluCheckExt3( void * pMan, word * pTruth, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot, char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 ) { If_Man_t * p = (If_Man_t *)pMan; If_Grp_t G, G2, R; G = If_CluCheck3( p, pTruth, nVars, nLutLeaf, nLutLeaf2, nLutRoot, &R, &G2, pFunc0, pFunc1, pFunc2 ); memcpy( pLut0, &R, sizeof(If_Grp_t) ); memcpy( pLut1, &G, sizeof(If_Grp_t) ); memcpy( pLut2, &G2, sizeof(If_Grp_t) ); return (G.nVars > 0); } // computes delay of the decomposition float If_CluDelayMax( If_Grp_t * g, float * pDelays ) { float Delay = 0.0; int i; for ( i = 0; i < g->nVars; i++ ) Delay = Abc_MaxFloat( Delay, pDelays[(int)g->pVars[i]] ); return Delay; } // returns delay of the decomposition; sets area of the cut as its cost float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float WireDelay ) { float Delays[CLU_VAR_MAX+2]; int fUsed[CLU_VAR_MAX+2] = {0}; If_Obj_t * pLeaf; If_Grp_t G1 = {0}, G2 = {0}, G3 = {0}; int nLeaves = If_CutLeaveNum(pCut); int i, nLutLeaf, nLutRoot; // mark the cut as user cut // pCut->fUser = 1; // quit if parameters are wrong if ( strlen(pStr) != 2 ) { printf( "Wrong LUT struct (%s)\n", pStr ); return ABC_INFINITY; } nLutLeaf = pStr[0] - '0'; if ( nLutLeaf < 3 || nLutLeaf > 6 ) { printf( "Leaf size (%d) should belong to {3,4,5,6}.\n", nLutLeaf ); return ABC_INFINITY; } nLutRoot = pStr[1] - '0'; if ( nLutRoot < 3 || nLutRoot > 6 ) { printf( "Root size (%d) should belong to {3,4,5,6}.\n", nLutRoot ); return ABC_INFINITY; } if ( nLeaves > nLutLeaf + nLutRoot - 1 ) { printf( "The cut size (%d) is too large for the LUT structure %d%d.\n", If_CutLeaveNum(pCut), nLutLeaf, nLutRoot ); return ABC_INFINITY; } // remember the delays If_CutForEachLeaf( p, pCut, pLeaf, i ) Delays[i] = If_ObjCutBest(pLeaf)->Delay; // consider easy case if ( nLeaves <= Abc_MaxInt( nLutLeaf, nLutRoot ) ) { assert( nLeaves <= 6 ); for ( i = 0; i < nLeaves; i++ ) { pCut->pPerm[i] = 1; G1.pVars[i] = i; } G1.nVars = nLeaves; return 1.0 + If_CluDelayMax( &G1, Delays ); } // derive the first group G1 = If_CluCheck( p, (word *)If_CutTruth(pCut), nLeaves, 0, nLutLeaf, nLutRoot, NULL, NULL, NULL, NULL, 1 ); if ( G1.nVars == 0 ) return ABC_INFINITY; // compute the delay Delays[nLeaves] = If_CluDelayMax( &G1, Delays ) + (WireDelay == 0.0)?1.0:WireDelay; if ( G2.nVars ) Delays[nLeaves+1] = If_CluDelayMax( &G2, Delays ) + (WireDelay == 0.0)?1.0:WireDelay; // mark used groups for ( i = 0; i < G1.nVars; i++ ) fUsed[(int)G1.pVars[i]] = 1; for ( i = 0; i < G2.nVars; i++ ) fUsed[(int)G2.pVars[i]] = 1; // mark unused groups assert( G1.nMyu >= 2 && G1.nMyu <= 4 ); if ( G1.nMyu > 2 ) fUsed[(int)G1.pVars[G1.nVars-1]] = 0; assert( !G2.nVars || (G2.nMyu >= 2 && G2.nMyu <= 4) ); if ( G2.nMyu > 2 ) fUsed[(int)G2.pVars[G2.nVars-1]] = 0; // create remaining group assert( G3.nVars == 0 ); for ( i = 0; i < nLeaves; i++ ) if ( !fUsed[i] ) G3.pVars[(int)G3.nVars++] = i; G3.pVars[(int)G3.nVars++] = nLeaves; if ( G2.nVars ) G3.pVars[(int)G3.nVars++] = nLeaves+1; assert( G1.nVars + G2.nVars + G3.nVars == nLeaves + (G1.nVars > 0) + (G2.nVars > 0) + (G1.nMyu > 2) + (G2.nMyu > 2) ); // what if both non-disjoint vars are the same??? pCut->Cost = 2 + (G2.nVars > 0); return 1.0 + If_CluDelayMax( &G3, Delays ); } /**Function************************************************************* Synopsis [Performs additional check.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int If_CutPerformCheck16( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ) { If_Grp_t G1 = {0};//, G3 = {0}; int i, nLutLeaf, nLutLeaf2, nLutRoot, Length; // if cutmin is disabled, minimize the cut if ( !p->pPars->fCutMin && If_CluSupportSize((word *)pTruth, nVars) < nLeaves ) { If_Cut_t * pCut = p->pCutTemp; pCut->nLimit = nVars; pCut->nLeaves = nLeaves; pCut->pLeaves = (int *)(pCut + 1); for ( i = 0; i < nLeaves; i++ ) pCut->pLeaves[i] = i; pCut->pTruth = (unsigned *)pCut->pLeaves + pCut->nLimit + p->nPermWords; If_CluCopy( (word *)If_CutTruth(pCut), (word *)pTruth, nVars ); if ( If_CutTruthMinimize( p, pCut ) >= 2 ) return 0; nLeaves = pCut->nLeaves; // If_CluCopy( (word *)pTruth, (word *)If_CutTruth(pCut), nVars ); pTruth = If_CutTruth(pCut); } // quit if parameters are wrong Length = strlen(pStr); if ( Length != 2 && Length != 3 ) { printf( "Wrong LUT struct (%s)\n", pStr ); return 0; } for ( i = 0; i < Length; i++ ) if ( pStr[i] - '0' < 3 || pStr[i] - '0' > 6 ) { printf( "The LUT size (%d) should belong to {3,4,5,6}.\n", pStr[i] - '0' ); return 0; } nLutLeaf = pStr[0] - '0'; nLutLeaf2 = ( Length == 3 ) ? pStr[1] - '0' : 0; nLutRoot = pStr[Length-1] - '0'; if ( nLeaves > nLutLeaf - 1 + (nLutLeaf2 ? nLutLeaf2 - 1 : 0) + nLutRoot ) { printf( "The cut size (%d) is too large for the LUT structure %s.\n", nLeaves, pStr ); return 0; } // consider easy case if ( nLeaves <= Abc_MaxInt( nLutLeaf2, Abc_MaxInt(nLutLeaf, nLutRoot) ) ) return 1; // derive the first group if ( Length == 2 ) G1 = If_CluCheck( p, (word *)pTruth, nLeaves, 0, nLutLeaf, nLutRoot, NULL, NULL, NULL, NULL, 1 ); else G1 = If_CluCheck3( p, (word *)pTruth, nLeaves, nLutLeaf, nLutLeaf2, nLutRoot, NULL, NULL, NULL, NULL, NULL ); // if ( G1.nVars > 0 ) // If_CluPrintGroup( &G1 ); return (int)(G1.nVars > 0); } // testing procedure void If_CluTest() { // word t = 0xff00f0f0ccccaaaa; // word t = 0xfedcba9876543210; // word t = 0xec64000000000000; // word t = 0x0100200000000001; // word t2[4] = { 0x0000800080008000, 0x8000000000008000, 0x8000000080008000, 0x0000000080008000 }; // word t = 0x07770FFF07770FFF; // word t = 0x002000D000D00020; // word t = 0x000F000E000F000F; // word t = 0xF7FFF7F7F7F7F7F7; // word t = 0x0234AFDE23400BCE; // word t = 0x0080008880A088FF; // word s = t; // word t = 0xFFBBBBFFF0B0B0F0; word t = 0x6DD9926D962D6996; int nVars = 6; int nLutLeaf = 4; int nLutLeaf2 = 4; int nLutRoot = 4; /* word t2[2] = { 0x7f807f807f80807f, 0x7f807f807f807f80 }; int nVars = 7; int nLutLeaf = 3; int nLutLeaf2 = 3; int nLutRoot = 3; */ If_Grp_t G; If_Grp_t G2, R; word Func0, Func1, Func2; return; /* int pCanonPerm[CLU_VAR_MAX]; int uCanonPhase; Kit_DsdPrintFromTruth( (unsigned*)&s, nVars ); printf( "\n" ); uCanonPhase = If_CluSemiCanonicize( &s, nVars, pCanonPerm ); Kit_DsdPrintFromTruth( (unsigned*)&s, nVars ); printf( "\n" ); If_CluSemiCanonicizeVerify( &s, &t, nVars, pCanonPerm, uCanonPhase ); */ Kit_DsdPrintFromTruth( (unsigned*)&t, nVars ); printf( "\n" ); G = If_CluCheck3( NULL, &t, nVars, nLutLeaf, nLutLeaf2, nLutRoot, &R, &G2, &Func0, &Func1, &Func2 ); If_CluPrintGroup( &G ); If_CluPrintGroup( &G2 ); If_CluPrintGroup( &R ); // If_CluVerify3( &t, nVars, &G, &G2, &R, Func1, Func2, Func0 ); return; // If_CutPerformCheck07( NULL, (unsigned *)&t, 6, 6, NULL ); // return; // Kit_DsdPrintFromTruth( (unsigned*)&t, nVars ); printf( "\n" ); // G = If_CluCheck( NULL, &t, nVars, 0, nLutLeaf, nLutRoot, NULL, NULL, NULL, NULL, 0 ); // If_CluPrintGroup( &G ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END