/**CFile**************************************************************** FileName [dauNpn2.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Functional enumeration.] Synopsis [Functional enumeration.] Author [Siang-Yun Lee] Affiliation [National Taiwan University] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: dauNpn2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "dauInt.h" #include "misc/util/utilTruth.h" #include "misc/extra/extra.h" #include "aig/gia/gia.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// typedef struct Dtt_Man_t_ Dtt_Man_t; struct Dtt_Man_t_ { int nVars; // variable number int nPerms; // number of permutations int nComps; // number of complementations int * pPerms; // permutations int * pComps; // complementations word * pPres; // function marks Vec_Int_t * vFanins; // node fanins Vec_Int_t * vTruths; // node truth tables Vec_Int_t * vConfigs; // configurations Vec_Int_t * vClasses; // node NPN classes Vec_Int_t * vTruthNpns; // truth tables of the classes Vec_Wec_t * vFunNodes; // nodes by NPN class Vec_Int_t * vTemp; // temporary Vec_Int_t * vTemp2; // temporary unsigned FunMask; // function mask unsigned CmpMask; // function mask unsigned BinMask; // hash mask unsigned * pBins; // hash bins Vec_Int_t * vUsedBins; // used bins int Counts[32]; // node counts int nClasses; // count of classes unsigned * pTable; // mapping of funcs into their classes int * pNodes; // the number of nodes in min-node network int * pTimes; // the number of different min-node networks char * pVisited; // visited classes Vec_Int_t * vVisited; // the number of visited classes }; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Parse one formula into a truth table.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ char * Dau_ParseFormulaEndToken( char * pForm ) { int Counter = 0; char * pThis; for ( pThis = pForm; *pThis; pThis++ ) { if ( *pThis == '~' ) continue; if ( *pThis == '(' ) Counter++; else if ( *pThis == ')' ) Counter--; if ( Counter == 0 ) return pThis + 1; } assert( 0 ); return NULL; } word Dau_ParseFormula_rec( char * pBeg, char * pEnd ) { word iFans[2], Res, Oper = -1; char * pEndNew; int fCompl = 0; while ( pBeg[0] == '~' ) { pBeg++; fCompl ^= 1; } if ( pBeg + 1 == pEnd ) { if ( pBeg[0] >= 'a' && pBeg[0] <= 'f' ) return fCompl ? ~s_Truths6[pBeg[0] - 'a'] : s_Truths6[pBeg[0] - 'a']; assert( 0 ); return -1; } if ( pBeg[0] == '(' ) { pEndNew = Dau_ParseFormulaEndToken( pBeg ); if ( pEndNew == pEnd ) { assert( pBeg[0] == '(' ); assert( pBeg[pEnd-pBeg-1] == ')' ); Res = Dau_ParseFormula_rec( pBeg + 1, pEnd - 1 ); return fCompl ? ~Res : Res; } } // get first part pEndNew = Dau_ParseFormulaEndToken( pBeg ); iFans[0] = Dau_ParseFormula_rec( pBeg, pEndNew ); iFans[0] = fCompl ? ~iFans[0] : iFans[0]; Oper = pEndNew[0]; // get second part pBeg = pEndNew + 1; pEndNew = Dau_ParseFormulaEndToken( pBeg ); iFans[1] = Dau_ParseFormula_rec( pBeg, pEndNew ); // derive the formula if ( Oper == '&' ) return iFans[0] & iFans[1]; if ( Oper == '^' ) return iFans[0] ^ iFans[1]; assert( 0 ); return -1; } word Dau_ParseFormula( char * p ) { return Dau_ParseFormula_rec( p, p + strlen(p) ); } void Dau_ParseFormulaTest() { char * p = "~((~~d&~(~~b&c))^(~(~a&~d)&~(~c^~b)))"; word r = ABC_CONST(0x037d037d037d037d); word t = Dau_ParseFormula( p ); assert( r == t ); } /**Function************************************************************* Synopsis [Parse one formula into a AIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Dau_ParseFormulaAig_rec( Gia_Man_t * p, char * pBeg, char * pEnd ) { int iFans[2], Res, Oper = -1; char * pEndNew; int fCompl = 0; while ( pBeg[0] == '~' ) { pBeg++; fCompl ^= 1; } if ( pBeg + 1 == pEnd ) { if ( pBeg[0] >= 'a' && pBeg[0] <= 'f' ) return Abc_Var2Lit( 1 + pBeg[0] - 'a', fCompl ); assert( 0 ); return -1; } if ( pBeg[0] == '(' ) { pEndNew = Dau_ParseFormulaEndToken( pBeg ); if ( pEndNew == pEnd ) { assert( pBeg[0] == '(' ); assert( pBeg[pEnd-pBeg-1] == ')' ); Res = Dau_ParseFormulaAig_rec( p, pBeg + 1, pEnd - 1 ); return Abc_LitNotCond( Res, fCompl ); } } // get first part pEndNew = Dau_ParseFormulaEndToken( pBeg ); iFans[0] = Dau_ParseFormulaAig_rec( p, pBeg, pEndNew ); iFans[0] = Abc_LitNotCond( iFans[0], fCompl ); Oper = pEndNew[0]; // get second part pBeg = pEndNew + 1; pEndNew = Dau_ParseFormulaEndToken( pBeg ); iFans[1] = Dau_ParseFormulaAig_rec( p, pBeg, pEndNew ); // derive the formula if ( Oper == '&' ) return Gia_ManHashAnd( p, iFans[0], iFans[1] ); if ( Oper == '^' ) return Gia_ManHashXor( p, iFans[0], iFans[1] ); assert( 0 ); return -1; } int Dau_ParseFormulaAig( Gia_Man_t * p, char * pStr ) { return Dau_ParseFormulaAig_rec( p, pStr, pStr + strlen(pStr) ); } Gia_Man_t * Dau_ParseFormulaAigTest() { int i; char * pStr = "~((~~d&~(~~b&c))^(~(~a&~d)&~(~c^~b)))"; Gia_Man_t * p = Gia_ManStart( 1000 ); p->pName = Abc_UtilStrsav( "func_enum_aig" ); Gia_ManHashAlloc( p ); for ( i = 0; i < 5; i++ ) Gia_ManAppendCi( p ); Gia_ManAppendCo( p, Dau_ParseFormulaAig(p, pStr) ); return p; } /**Function************************************************************* Synopsis [Verify one file.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Dau_VerifyFile( char * pFileName ) { char Buffer[1000]; unsigned uTruth, uTruth2; int nFails = 0, nLines = 0; FILE * pFile = fopen( pFileName, "rb" ); while ( fgets( Buffer, 1000, pFile ) ) { if ( Buffer[strlen(Buffer)-1] == '\n' ) Buffer[strlen(Buffer)-1] = 0; if ( Buffer[strlen(Buffer)-1] == '\r' ) Buffer[strlen(Buffer)-1] = 0; Extra_ReadHexadecimal( &uTruth2, Buffer, 5 ); uTruth = (unsigned)Dau_ParseFormula( Buffer + 11 ); if ( uTruth != uTruth2 ) printf( "Verification failed in line %d: %s\n", nLines, Buffer ), nFails++; nLines++; } printf( "Verification succeeded for %d functions and failed for %d functions.\n", nLines-nFails, nFails ); } void Dau_VerifyFileTest() { char * pFileName = "lib4var.txt"; Dau_VerifyFile( pFileName ); } /**Function************************************************************* Synopsis [Create AIG for one file.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Dau_ConstructAigFromFile( char * pFileName ) { char Buffer[1000]; int i, nLines = 0; FILE * pFile = fopen( pFileName, "rb" ); Gia_Man_t * p = Gia_ManStart( 1000 ); p->pName = Abc_UtilStrsav( "func_enum_aig" ); Gia_ManHashAlloc( p ); for ( i = 0; i < 5; i++ ) Gia_ManAppendCi( p ); while ( fgets( Buffer, 1000, pFile ) ) { if ( Buffer[strlen(Buffer)-1] == '\n' ) Buffer[strlen(Buffer)-1] = 0; if ( Buffer[strlen(Buffer)-1] == '\r' ) Buffer[strlen(Buffer)-1] = 0; Gia_ManAppendCo( p, Dau_ParseFormulaAig(p, Buffer + 11) ); nLines++; } printf( "Finish constructing AIG for %d structures.\n", nLines ); return p; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ unsigned * Dau_ReadFile2( char * pFileName, int nSizeW ) { abctime clk = Abc_Clock(); FILE * pFile = fopen( pFileName, "rb" ); unsigned * p = (unsigned *)ABC_CALLOC(word, nSizeW); int RetValue = pFile ? fread( p, sizeof(word), nSizeW, pFile ) : 0; RetValue = 0; if ( pFile ) { printf( "Finished reading file \"%s\".\n", pFileName ); fclose( pFile ); } else printf( "Cannot open input file \"%s\".\n", pFileName ); Abc_PrintTime( 1, "File reading", Abc_Clock() - clk ); return p; } void Dtt_ManRenum( int nVars, unsigned * pTable, int * pnClasses ) { unsigned i, Limit = 1 << ((1 << nVars)-1), Count = 0; for ( i = 0; i < Limit; i++ ) if ( pTable[i] == i ) pTable[i] = Count++; else { assert( pTable[i] < i ); pTable[i] = pTable[pTable[i]]; } printf( "The total number of NPN classes = %d.\n", Count ); *pnClasses = Count; } unsigned * Dtt_ManLoadClasses( int nVars, int * pnClasses ) { unsigned * pTable = NULL; if ( nVars == 4 ) pTable = Dau_ReadFile2( "tableW14.data", 1 << 14 ); else if ( nVars == 5 ) pTable = Dau_ReadFile2( "tableW30.data", 1 << 30 ); else assert( 0 ); Dtt_ManRenum( nVars, pTable, pnClasses ); return pTable; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Dtt_ManAddVisited( Dtt_Man_t * p, unsigned Truth2, int n ) { unsigned Truth = Truth2 & p->CmpMask ? ~Truth2 : Truth2; unsigned Class = p->pTable[Truth & p->FunMask]; assert( Class < (unsigned)p->nClasses ); if ( p->pNodes[Class] < n ) return; assert( p->pNodes[Class] == n ); if ( p->pVisited[Class] ) return; p->pVisited[Class] = 1; Vec_IntPush( p->vVisited, Class ); } void Dtt_ManProcessVisited( Dtt_Man_t * p ) { int i, Class; Vec_IntForEachEntry( p->vVisited, Class, i ) { assert( p->pVisited[Class] ); p->pVisited[Class] = 0; p->pTimes[Class]++; } Vec_IntClear( p->vVisited ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Dtt_Man_t * Dtt_ManAlloc( int nVars, int fMulti ) { Dtt_Man_t * p = ABC_CALLOC( Dtt_Man_t, 1 ); p->nVars = nVars; p->nPerms = Extra_Factorial( nVars ); p->nComps = 1 << nVars; p->pPerms = Extra_PermSchedule( nVars ); p->pComps = Extra_GreyCodeSchedule( nVars ); p->pPres = ABC_CALLOC( word, 1 << (p->nComps - 7) ); p->vFanins = Vec_IntAlloc( 2*617000 ); p->vTruths = Vec_IntAlloc( 617000 ); p->vConfigs = Vec_IntAlloc( 617000 ); p->vClasses = Vec_IntAlloc( 617000 ); p->vTruthNpns = Vec_IntAlloc( 617000 ); p->vFunNodes = Vec_WecStart( 16 ); p->vTemp = Vec_IntAlloc( 4000 ); p->vTemp2 = Vec_IntAlloc( 4000 ); p->FunMask = nVars == 5 ? ~0 : (nVars == 4 ? 0xFFFF : 0xFF); p->CmpMask = nVars == 5 ? 1 << 31 : (nVars == 4 ? 1 << 15 : 1 << 7); p->BinMask = 0x3FFF; p->pBins = ABC_FALLOC( unsigned, p->BinMask + 1 ); p->vUsedBins = Vec_IntAlloc( 4000 ); if ( !fMulti ) return p; p->pTable = Dtt_ManLoadClasses( p->nVars, &p->nClasses ); p->pNodes = ABC_CALLOC( int, p->nClasses ); p->pTimes = ABC_CALLOC( int, p->nClasses ); p->pVisited = ABC_CALLOC( char, p->nClasses ); p->vVisited = Vec_IntAlloc( 1000 ); return p; } void Dtt_ManFree( Dtt_Man_t * p ) { Vec_IntFreeP( &p->vVisited ); ABC_FREE( p->pTable ); ABC_FREE( p->pNodes ); ABC_FREE( p->pTimes ); ABC_FREE( p->pVisited ); Vec_IntFreeP( &p->vFanins ); Vec_IntFreeP( &p->vTruths ); Vec_IntFreeP( &p->vConfigs ); Vec_IntFreeP( &p->vClasses ); Vec_IntFreeP( &p->vTruthNpns ); Vec_WecFreeP( &p->vFunNodes ); Vec_IntFreeP( &p->vTemp ); Vec_IntFreeP( &p->vTemp2 ); Vec_IntFreeP( &p->vUsedBins ); ABC_FREE( p->pPerms ); ABC_FREE( p->pComps ); ABC_FREE( p->pPres ); ABC_FREE( p->pBins ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [Collect representatives of the same class.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline unsigned Dtt_ManHashKey( Dtt_Man_t * p, unsigned Truth ) { static unsigned s_P[4] = { 1699, 5147, 7103, 8147 }; unsigned char * pD = (unsigned char*)&Truth; return pD[0] * s_P[0] + pD[1] * s_P[1] + pD[2] * s_P[2] + pD[3] * s_P[3]; } int Dtt_ManCheckHash( Dtt_Man_t * p, unsigned Truth ) { unsigned Hash = Dtt_ManHashKey(p, Truth); unsigned * pSpot = p->pBins + (Hash & p->BinMask); for ( ; ~*pSpot; Hash++, pSpot = p->pBins + (Hash & p->BinMask) ) if ( *pSpot == Truth ) // equal return 0; Vec_IntPush( p->vUsedBins, pSpot - p->pBins ); *pSpot = Truth; return 1; } Vec_Int_t * Dtt_ManCollect( Dtt_Man_t * p, unsigned Truth, Vec_Int_t * vFuns ) { int i, k, Entry; word tCur = ((word)Truth << 32) | (word)Truth; Vec_IntClear( vFuns ); for ( i = 0; i < p->nPerms; i++ ) { for ( k = 0; k < p->nComps; k++ ) { // unsigned tTemp = (unsigned)(tCur & 1 ? ~tCur : tCur); unsigned tTemp = (unsigned)(tCur & p->CmpMask ? ~tCur : tCur); if ( Dtt_ManCheckHash( p, tTemp ) ) Vec_IntPush( vFuns, tTemp ); tCur = Abc_Tt6Flip( tCur, p->pComps[k] ); } tCur = Abc_Tt6SwapAdjacent( tCur, p->pPerms[i] ); } assert( tCur == (((word)Truth << 32) | (word)Truth) ); // clean hash table Vec_IntForEachEntry( p->vUsedBins, Entry, i ) p->pBins[Entry] = ~0; Vec_IntClear( p->vUsedBins ); //printf( "%d ", Vec_IntSize(vFuns) ); return vFuns; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Dtt_ManGetFun( Dtt_Man_t * p, unsigned tFun, int n ) { unsigned Class; tFun = tFun & p->CmpMask ? ~tFun : tFun; //return Abc_TtGetBit( p->pPres, tFun & p->FunMask ); if ( !Abc_TtGetBit( p->pPres, tFun & p->FunMask ) ) return 0; if ( p->pTable == NULL ) return 1; Class = p->pTable[tFun & p->FunMask]; assert( Class < (unsigned)p->nClasses ); if ( p->pNodes[Class] < n ) return 1; assert( p->pNodes[Class] == n ); if ( p->pVisited[Class] ) return 1; return 0; } static inline void Dtt_ManSetFun( Dtt_Man_t * p, unsigned tFun ) { tFun = tFun & p->CmpMask ? ~tFun : tFun; //assert( !Dtt_ManGetFun(p, fFun & p->FunMask ); Abc_TtSetBit( p->pPres, tFun & p->FunMask ); } void Dtt_ManAddFunction( Dtt_Man_t * p, int n, int FanI, int FanJ, int Type, unsigned Truth ) { Vec_Int_t * vFuncs = Dtt_ManCollect( p, Truth, p->vTemp2 ); unsigned Min = Vec_IntFindMin( vFuncs ); int i, nObjs = Vec_IntSize(p->vFanins)/2; int nNodesI = 0xF & (Vec_IntEntry(p->vConfigs, FanI) >> 3); int nNodesJ = 0xF & (Vec_IntEntry(p->vConfigs, FanJ) >> 3); int nNodes = nNodesI + nNodesJ + 1; assert( nObjs == Vec_IntSize(p->vTruths) ); assert( nObjs == Vec_IntSize(p->vConfigs) ); assert( nObjs == Vec_IntSize(p->vClasses) ); Vec_WecPush( p->vFunNodes, n, nObjs ); Vec_IntPushTwo( p->vFanins, FanI, FanJ ); Vec_IntPush( p->vTruths, Truth ); Vec_IntPush( p->vConfigs, (nNodes << 3) | Type ); Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) ); Vec_IntPush( p->vTruthNpns, Min ); Vec_IntForEachEntry( vFuncs, Min, i ) Dtt_ManSetFun( p, Min ); assert( nNodes < 32 ); p->Counts[nNodes]++; if ( p->pTable == NULL ) return; Truth = Truth & p->CmpMask ? ~Truth : Truth; Truth &= p->FunMask; //assert( p->pNodes[p->pTable[Truth]] == 0 ); p->pNodes[p->pTable[Truth]] = n; } int Dtt_PrintStats( int nNodes, int nVars, Vec_Wec_t * vFunNodes, word nSteps, abctime clk, int fDelay, word nMultis ) { int nNew = Vec_IntSize(Vec_WecEntry(vFunNodes, nNodes)); printf("%c =%2d | ", fDelay ? 'D':'N', nNodes ); printf("C =%12.0f | ", (double)(iword)nSteps ); printf("New%d =%10d ", nVars, nNew + (int)(nNodes==0) ); printf("All%d =%10d | ", nVars, Vec_WecSizeSize(vFunNodes)+1 ); printf("Multi =%10d | ", (int)nMultis ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); //Abc_Print(1, "%9.2f sec\n", 1.0*(Abc_Clock() - clk)/(CLOCKS_PER_SEC)); fflush(stdout); return nNew; } void Dtt_PrintDistrib( Dtt_Man_t * p ) { int i; printf( "NPN classes for each node count (N):\n" ); for ( i = 0; i < 32; i++ ) if ( p->Counts[i] ) printf( "N = %2d : NPN = %6d\n", i, p->Counts[i] ); } void Dtt_PrintMulti2( Dtt_Man_t * p ) { int i, n; for ( n = 0; n <= 7; n++ ) { printf( "n=%d : ", n); for ( i = 0; i < p->nClasses; i++ ) if ( p->pNodes[i] == n ) printf( "%d ", p->pTimes[i] ); printf( "\n" ); } } void Dtt_PrintMulti1( Dtt_Man_t * p ) { int i, n, Entry, Count, Prev; for ( n = 0; n < 16; n++ ) { Vec_Int_t * vTimes = Vec_IntAlloc( 100 ); Vec_Int_t * vUsed = Vec_IntAlloc( 100 ); for ( i = 0; i < p->nClasses; i++ ) if ( p->pNodes[i] == n ) Vec_IntPush( vTimes, p->pTimes[i] ); if ( Vec_IntSize(vTimes) == 0 ) { Vec_IntFree(vTimes); Vec_IntFree(vUsed); break; } Vec_IntSort( vTimes, 0 ); Count = 1; Prev = Vec_IntEntry( vTimes, 0 ); Vec_IntForEachEntryStart( vTimes, Entry, i, 1 ) if ( Prev == Entry ) Count++; else { assert( Prev < Entry ); Vec_IntPushTwo( vUsed, Prev, Count ); Count = 1; Prev = Entry; } if ( Count > 0 ) Vec_IntPushTwo( vUsed, Prev, Count ); printf( "n=%d : ", n); Vec_IntForEachEntryDouble( vUsed, Prev, Entry, i ) printf( "%d=%d ", Prev, Entry ); printf( "\n" ); Vec_IntFree( vTimes ); Vec_IntFree( vUsed ); } } void Dtt_PrintMulti( Dtt_Man_t * p ) { int n, Counts[13][15] = {{0}}; for ( n = 0; n < 13; n++ ) { int i, Total = 0, Count = 0; for ( i = 0; i < p->nClasses; i++ ) if ( p->pNodes[i] == n ) { int Log = Abc_Base2Log(p->pTimes[i]); assert( Log < 15 ); if ( p->pTimes[i] < 2 ) Counts[n][0]++; else Counts[n][Log]++; Total += p->pTimes[i]; Count++; } if ( Count == 0 ) break; printf( "n=%2d : ", n ); printf( "All = %7d ", Count ); printf( "Ave = %6.2f ", 1.0*Total/Count ); for ( i = 0; i < 15; i++ ) if ( Counts[n][i] ) printf( "%6d", Counts[n][i] ); else printf( "%6s", "" ); printf( "\n" ); } } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ typedef struct Dtt_FunImpl_t_ Dtt_FunImpl_t; struct Dtt_FunImpl_t_ { int Type; int NP1; // 4 bits for an input (NPPP) int FI1; // the id (in vLibFun) of the first fanin function int NP2; int FI2; // the id (in vLibFun) of the second fanin function }; void Dtt_FunImplFI2Str( int FI, int NP, Vec_Int_t* vLibFun, char* str ) { int i, P[5], N[5]; for ( i = 0; i < 5; i++ ) { P[i] = NP & 0x7; NP = NP >> 3; N[i] = NP & 0x1; NP = NP >> 1 ; } sprintf( str, "[%08x(%03d),%d%d%d%d%d,%d%d%d%d%d]", Vec_IntEntry( vLibFun, FI ), FI, P[0], P[1], P[2], P[3], P[4], N[0], N[1], N[2], N[3], N[4] ); } void Dtt_FunImpl2Str( int Type, char* sFI1, char* sFI2, char* str ) { // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2 // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2) switch( Type ) { case 0: sprintf( str, "(%s&%s)", sFI1, sFI2 ); break; case 1: sprintf( str, "(~%s&%s)", sFI1, sFI2 ); break; case 2: sprintf( str, "(%s&~%s)", sFI1, sFI2 ); break; case 3: sprintf( str, "~(~%s&~%s)", sFI1, sFI2 ); break; case 4: sprintf( str, "(%s^%s)", sFI1, sFI2 ); break; case 5: sprintf( str, "~(%s&%s)", sFI1, sFI2 ); break; case 6: sprintf( str, "~(~%s&%s)", sFI1, sFI2 ); break; case 7: sprintf( str, "~(%s&~%s)", sFI1, sFI2 ); break; case 8: sprintf( str, "(~%s&~%s)", sFI1, sFI2 ); break; case 9: sprintf( str, "~(%s^%s)", sFI1, sFI2 ); break; /*case 0: sprintf( str, " ( %s& %s)", sFI1, sFI2 ); break; case 1: sprintf( str, " (~%s& %s)", sFI1, sFI2 ); break; case 2: sprintf( str, " ( %s&~%s)", sFI1, sFI2 ); break; case 3: sprintf( str, "~(~%s&~%s)", sFI1, sFI2 ); break; case 4: sprintf( str, " ( %s^ %s)", sFI1, sFI2 ); break; case 5: sprintf( str, "~( %s& %s)", sFI1, sFI2 ); break; case 6: sprintf( str, "~(~%s& %s)", sFI1, sFI2 ); break; case 7: sprintf( str, "~( %s&~%s)", sFI1, sFI2 ); break; case 8: sprintf( str, " (~%s&~%s)", sFI1, sFI2 ); break; case 9: sprintf( str, "~( %s^ %s)", sFI1, sFI2 ); break;*/ } } int Dtt_ComposeNP( int NP1, int NP2 ) { // NP[i] = NP1[NP2[i]] int NP = 0, i; for ( i = 0; i < 5; i++ ) { NP |= ( ( NP1 >> ((NP2&0x7)<<2) ) & 0x7 ) << (i<<2); // P'[i] = P1[P2[i]] NP |= ( ( NP1 >> ((NP2&0x7)<<2) ^ NP2 ) & 0x8 ) << (i<<2); // N'[i] = N1[P2[i]] ^ N2[i] NP2 = NP2 >> 4; } return NP; } void Dtt_MakePI( int NP, char* str ) { // apply P'[i], find the i s.t. P'[i]==0, correspond to N'[i] int i; for ( i = 0; i < 5; i++ ) { if ( ( NP & 0x7 ) == 0 ) { if ( NP & 0x8 ) sprintf( str, "~%c", 'a'+i ); else sprintf( str, "%c", 'a'+i ); return; } NP = NP >> 4; } assert(0); } void Dtt_MakeFormula( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sF, int fPrint, FILE* pFile ); void Dtt_MakeFormulaFI2( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sFI1, char* sF, int fPrint, FILE* pFile ) { int j; Dtt_FunImpl_t* pImpl2; char sFI2[100] = {0}; //sprintf( sFI2, "" ); if ( pFun->FI2 == 0 ) // PI { Dtt_MakePI( Dtt_ComposeNP( pFun->NP2, NP ), sFI2 ); Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, sF ); if (fPrint) fprintf(pFile, "%08x = %s\n", tFun, sF); } else { Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pImpl2, j, pFun->FI2 ) { Dtt_MakeFormula( tFun, pImpl2, vLibImpl, Dtt_ComposeNP( pFun->NP2, NP ), sFI2, 0, pFile ); Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, sF ); if (fPrint) fprintf(pFile, "%08x = %s\n", tFun, sF); } } } void Dtt_MakeFormula( unsigned tFun, Dtt_FunImpl_t* pFun, Vec_Vec_t* vLibImpl, int NP, char* sF, int fPrint, FILE* pFile ) { int j; Dtt_FunImpl_t* pImpl1; char sFI1[100], sCopy[100] = {0}; //sprintf( sFI1, "" ); if ( pFun->FI1 == 0 ) // PI { Dtt_MakePI( Dtt_ComposeNP( pFun->NP1, NP ), sFI1 ); sprintf( sCopy, "%s", sF ); Dtt_MakeFormulaFI2( tFun, pFun, vLibImpl, NP, sFI1, sF, fPrint, pFile ); } else { Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pImpl1, j, pFun->FI1 ) { Dtt_MakeFormula( tFun, pImpl1, vLibImpl, Dtt_ComposeNP( pFun->NP1, NP ), sFI1, 0, pFile ); sprintf( sCopy, "%s", sF ); Dtt_MakeFormulaFI2( tFun, pFun, vLibImpl, NP, sFI1, sF, fPrint, pFile ); } } } void Dtt_ProcessType( int* Type, int nFanin ) { // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2 // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2) if ( nFanin == 3 ) // for output negation *Type += (*Type<5)? 5: -5; else if ( *Type == 0 || *Type == 5 ) *Type += nFanin; else if ( *Type == nFanin ) // 1,1 ; 2,2 *Type = 0; else if ( *Type + nFanin == 3 ) // 1,2 ; 2,1 *Type = 8; else if ( *Type == 3 ) *Type = (nFanin==1)? 7: 6; else if ( *Type == 4 ) *Type = 9; else if ( *Type == nFanin+5 ) // 6,1 ; 7,2 *Type = 5; else if ( *Type + nFanin == 8 ) // 6,2 ; 7,1 *Type = 3; else if ( *Type == 8 ) *Type = (nFanin==1)? 2: 1; else if ( *Type == 9 ) *Type = 4; else assert( 0 ); } int Dtt_Check( unsigned tFun, unsigned tGoal, unsigned tCur, int* pType ) { if (!tGoal) //for Fanin2 and output return ( tCur == tFun || ~tCur == tFun ); //for Fanin1: check if tFun(Type)tCur==tGoal switch (*pType) { // 0: 1&2, 1: ~1&2, 2: 1&~2, 3: 1|2 = ~(~1&~2), 4: 1^2 // 5: ~(1&2), 6: ~(~1&2), 7: ~(1&~2), 8: ~1&~2, 9: ~(1^2) case 0: case 5: if ( (~tCur & tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; } else return ( (tCur & tFun) == tGoal ); case 1: case 6: if ( (tCur & tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; } else return ( (~tCur & tFun) == tGoal ); case 2: case 7: if ( (~tCur & ~tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; } else return ( (tCur & ~tFun) == tGoal ); case 3: case 8: if ( (~tCur | tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; } else return ( (tCur | tFun) == tGoal ); case 4: case 9: if ( (~tCur ^ tFun) == tGoal ) { Dtt_ProcessType( pType, 1 ); return 1; } else return ( (tCur ^ tFun) == tGoal ); default: assert(0); } return -1; } void Dtt_FindNP( Dtt_Man_t * p, unsigned tFun, unsigned tGoal, unsigned tNpn, int * NP, int* pType, int NPout ) { int i, k, j; int P[5] = { 0, 1, 2, 3, 4 }; int N[5] = { 0, 0, 0, 0, 0 }; int temp; word tCur = ((word)tNpn << 32) | (word)tNpn; for ( i = 0; i < p->nPerms; i++ ) { for ( k = 0; k < p->nComps; k++ ) { if ( Dtt_Check( tFun, tGoal, (unsigned)tCur, pType )) { if ( !tGoal && ( tFun == (unsigned)~tCur ) ) // !tGoal: not FI1 { if (!NPout) Dtt_ProcessType( pType, 3 ); else Dtt_ProcessType( pType, 2 ); } *NP = 0; if (!NPout) { for ( j = 0; j < 5; j++ ) *NP |= ( ( ( N[j] & 0x1 ) << 3 ) | ( P[j] & 0x7 ) ) << (j<<2) ; } else { for ( j = 0; j < 5; j++ ) { *NP |= P[NPout&0x7] << (j<<2); // P'[j] = P[Pout[j]] *NP |= ( N[NPout&0x7] ^ ( (NPout>>3) & 0x1 )) << (j<<2) << 3; // N'[i] = N1[P2[i]] ^ N2[i] NPout = NPout >> 4; } } return; } tCur = Abc_Tt6Flip( tCur, p->pComps[k] ); N[p->pComps[k]] ^= 0x1; } tCur = Abc_Tt6SwapAdjacent( tCur, p->pPerms[i] ); temp = P[p->pPerms[i]]; P[p->pPerms[i]] = P[p->pPerms[i]+1]; P[p->pPerms[i]+1] = temp; } assert(0); } void Dtt_DumpLibrary( Dtt_Man_t * p ) { FILE * pFile; char FileName[100], str[100], sFI1[50], sFI2[50]; int i, j, Entry, fRepeat; Dtt_FunImpl_t * pFun, * pFun2; Vec_Int_t * vLibFun = Vec_IntDup( p->vTruthNpns ); // none-duplicating vector of NPN representitives Vec_Vec_t * vLibImpl; Vec_IntUniqify( vLibFun ); vLibImpl = Vec_VecStart( Vec_IntSize( vLibFun ) ); Vec_IntForEachEntry( p->vTruths, Entry, i ) { int NP, Fanin2, Fanin1Npn, Fanin2Npn; if (i<2) continue; // skip const 0 pFun = ABC_CALLOC( Dtt_FunImpl_t, 1 ); pFun->Type = (int)( 0x7 & Vec_IntEntry(p->vConfigs, i) ); //word Fanin1 = Vec_IntEntry( p->vTruths, Vec_IntEntry( p->vFanins, i*2 ) ); Fanin2 = Vec_IntEntry( p->vTruths, Vec_IntEntry( p->vFanins, i*2+1 ) ); Fanin1Npn = Vec_IntEntry( p->vTruthNpns, Vec_IntEntry( p->vFanins, i*2 ) ); Fanin2Npn = Vec_IntEntry( p->vTruthNpns, Vec_IntEntry( p->vFanins, i*2+1 ) ); pFun->FI1 = Vec_IntFind( vLibFun, Fanin1Npn ); pFun->FI2 = Vec_IntFind( vLibFun, Fanin2Npn ); fRepeat = 0; Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun2, j, Vec_IntFind( vLibFun, Vec_IntEntry( p->vTruthNpns, i ) ) ) { if ( ( pFun2->FI1 == pFun->FI1 && pFun2->FI2 == pFun->FI2 ) || ( pFun2->FI2 == pFun->FI1 && pFun2->FI1 == pFun->FI2 ) ) { fRepeat = 1; break; } } if (fRepeat) { ABC_FREE( pFun ); continue; } Dtt_FindNP( p, Vec_IntEntry( p->vTruthNpns, i ), 0, Entry, &NP, &(pFun->Type), 0 ); //out: tGoal=0, NPout=0 Dtt_FindNP( p, Fanin2, Entry, Fanin1Npn, &(pFun->NP1), &(pFun->Type), NP ); //FI1 Dtt_FindNP( p, Fanin2, 0, Fanin2Npn, &(pFun->NP2), &(pFun->Type), NP ); //FI2: tGoal=0 Vec_VecPush( vLibImpl, Vec_IntFind( vLibFun, Vec_IntEntry( p->vTruthNpns, i ) ), pFun ); } // print to file sprintf( FileName, "lib%dvar.txt", p->nVars ); pFile = fopen( FileName, "wb" ); if (0) Vec_IntForEachEntry( vLibFun, Entry, i ) { if (!Entry) continue; // skip const 0 fprintf( pFile, "%08x: ", (unsigned)Entry ); Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun, j, i ) { Dtt_FunImplFI2Str( pFun->FI1, pFun->NP1, vLibFun, sFI1 ); Dtt_FunImplFI2Str( pFun->FI2, pFun->NP2, vLibFun, sFI2 ); Dtt_FunImpl2Str( pFun->Type, sFI1, sFI2, str ); fprintf( pFile, "%s, ", str ); } fprintf( pFile, "\n" ); } // formula format Vec_IntForEachEntry( vLibFun, Entry, i ) { if ( i<2 ) continue; // skip const 0 and buffer Vec_VecForEachEntryLevel( Dtt_FunImpl_t*, vLibImpl, pFun, j, i ) { str[0] = 0; //sprintf( str, "" ); Dtt_MakeFormula( (unsigned)Entry, pFun, vLibImpl, (4<<16)+(3<<12)+(2<<8)+(1<<4), str, 1, pFile ); } } fclose( pFile ); printf( "Dumped file \"%s\". \n", FileName ); fflush( stdout ); } void Dtt_EnumerateLf( int nVars, int nNodeMax, int fDelay, int fMulti, int fVerbose ) { int fDump = 1; abctime clk = Abc_Clock(); word nSteps = 0, nMultis = 0; Dtt_Man_t * p = Dtt_ManAlloc( nVars, fMulti ); int n, i, j; // constant zero class Vec_IntPushTwo( p->vFanins, 0, 0 ); Vec_IntPush( p->vTruths, 0 ); Vec_IntPush( p->vConfigs, 0 ); Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) ); Vec_IntPush( p->vTruthNpns, 0 ); Dtt_ManSetFun( p, 0 ); // buffer class Vec_WecPush( p->vFunNodes, 0, Vec_IntSize(p->vFanins)/2 ); Vec_IntPushTwo( p->vFanins, 0, 0 ); Vec_IntPush( p->vTruths, (unsigned)s_Truths6[0] ); Vec_IntPush( p->vConfigs, 0 ); Vec_IntPush( p->vClasses, Vec_IntSize(p->vTruthNpns) ); Vec_IntPush( p->vTruthNpns, (unsigned)s_Truths6[0] ); for ( i = 0; i < nVars; i++ ) Dtt_ManSetFun( p, (unsigned)s_Truths6[i] ); p->Counts[0] = 2; // enumerate Dtt_PrintStats(0, nVars, p->vFunNodes, nSteps, clk, fDelay, 0); for ( n = 1; n <= nNodeMax; n++ ) { for ( i = 0, j = n - 1; i < n; i++, j = j - 1 + fDelay ) if ( i <= j ) { Vec_Int_t * vFaninI = Vec_WecEntry( p->vFunNodes, i ); Vec_Int_t * vFaninJ = Vec_WecEntry( p->vFunNodes, j ); int k, i0, j0, EntryI, EntryJ; Vec_IntForEachEntry( vFaninI, EntryI, i0 ) { unsigned TruthI = Vec_IntEntry(p->vTruths, EntryI); Vec_Int_t * vFuns = Dtt_ManCollect( p, TruthI, p->vTemp ); int Start = i == j ? i0 : 0; Vec_IntForEachEntryStart( vFaninJ, EntryJ, j0, Start ) { unsigned Truth, TruthJ = Vec_IntEntry(p->vTruths, EntryJ); Vec_IntForEachEntry( vFuns, Truth, k ) { if ( !Dtt_ManGetFun(p, TruthJ & Truth, n) ) Dtt_ManAddFunction( p, n, EntryI, EntryJ, 0, TruthJ & Truth ); if ( !Dtt_ManGetFun(p, TruthJ & ~Truth, n) ) Dtt_ManAddFunction( p, n, EntryI, EntryJ, 1, TruthJ & ~Truth ); if ( !Dtt_ManGetFun(p, ~TruthJ & Truth, n) ) Dtt_ManAddFunction( p, n, EntryI, EntryJ, 2, ~TruthJ & Truth ); if ( !Dtt_ManGetFun(p, TruthJ | Truth, n) ) Dtt_ManAddFunction( p, n, EntryI, EntryJ, 3, TruthJ | Truth ); if ( !Dtt_ManGetFun(p, TruthJ ^ Truth, n) ) Dtt_ManAddFunction( p, n, EntryI, EntryJ, 4, TruthJ ^ Truth ); nSteps += 5; if ( p->pTable ) Dtt_ManAddVisited( p, TruthJ & Truth, n ); if ( p->pTable ) Dtt_ManAddVisited( p, TruthJ & ~Truth, n ); if ( p->pTable ) Dtt_ManAddVisited( p, ~TruthJ & Truth, n ); if ( p->pTable ) Dtt_ManAddVisited( p, TruthJ | Truth, n ); if ( p->pTable ) Dtt_ManAddVisited( p, TruthJ ^ Truth, n ); } nMultis++; if ( p->pTable ) Dtt_ManProcessVisited( p ); } } } if ( Dtt_PrintStats(n, nVars, p->vFunNodes, nSteps, clk, fDelay, nMultis) == 0 ) break; } if ( fDelay ) Dtt_PrintDistrib( p ); //if ( p->pTable ) //Dtt_PrintMulti( p ); if ( !fDelay && fDump ) Dtt_DumpLibrary( p ); Dtt_ManFree( p ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END