/**CFile**************************************************************** FileName [aigCanon.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [AIG package.] Synopsis [Processing the library of semi-canonical AIGs.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - April 28, 2007.] Revision [$Id: aigCanon.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] ***********************************************************************/ #include "aig.h" #include "bool/kit/kit.h" #include "bool/bdc/bdc.h" #include "aig/ioa/ioa.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// #define RMAN_MAXVARS 12 #define RMAX_MAXWORD (RMAN_MAXVARS <= 5 ? 1 : (1 << (RMAN_MAXVARS - 5))) typedef struct Aig_VSig_t_ Aig_VSig_t; struct Aig_VSig_t_ { int nOnes; int nCofOnes[RMAN_MAXVARS]; }; typedef struct Aig_Tru_t_ Aig_Tru_t; struct Aig_Tru_t_ { Aig_Tru_t * pNext; int Id; unsigned nVisits : 27; unsigned nVars : 5; unsigned pTruth[0]; }; typedef struct Aig_RMan_t_ Aig_RMan_t; struct Aig_RMan_t_ { int nVars; // the largest variable number Aig_Man_t * pAig; // recorded subgraphs // hash table int nBins; Aig_Tru_t ** pBins; int nEntries; Aig_MmFlex_t* pMemTrus; // bidecomposion Bdc_Man_t * pBidec; // temporaries unsigned pTruthInit[RMAX_MAXWORD]; // canonical truth table unsigned pTruth[RMAX_MAXWORD]; // current truth table unsigned pTruthC[RMAX_MAXWORD]; // canonical truth table unsigned pTruthTemp[RMAX_MAXWORD]; // temporary truth table Aig_VSig_t pMints[2*RMAN_MAXVARS]; // minterm count char pPerm[RMAN_MAXVARS]; // permutation char pPermR[RMAN_MAXVARS]; // reverse permutation // statistics int nVarFuncs[RMAN_MAXVARS+1]; int nTotal; int nTtDsd; int nTtDsdPart; int nTtDsdNot; int nUniqueVars; }; static Aig_RMan_t * s_pRMan = NULL; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Allocates recording manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_RMan_t * Aig_RManStart() { static Bdc_Par_t Pars = {0}, * pPars = &Pars; Aig_RMan_t * p; p = ABC_ALLOC( Aig_RMan_t, 1 ); memset( p, 0, sizeof(Aig_RMan_t) ); p->nVars = RMAN_MAXVARS; p->pAig = Aig_ManStart( 1000000 ); Aig_IthVar( p->pAig, p->nVars-1 ); // create hash table p->nBins = Abc_PrimeCudd(5000); p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins ); p->pMemTrus = Aig_MmFlexStart(); // bi-decomposition manager pPars->nVarsMax = p->nVars; pPars->fVerbose = 0; p->pBidec = Bdc_ManAlloc( pPars ); return p; } /**Function************************************************************* Synopsis [Returns the hash key.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Aig_RManTableHash( unsigned * pTruth, int nVars, int nBins, int * pPrimes ) { int i, nWords = Kit_TruthWordNum( nVars ); unsigned uHash = 0; for ( i = 0; i < nWords; i++ ) uHash ^= pTruth[i] * pPrimes[i & 0xf]; return (int)(uHash % nBins); } /**Function************************************************************* Synopsis [Returns the given record.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_Tru_t ** Aig_RManTableLookup( Aig_RMan_t * p, unsigned * pTruth, int nVars ) { static int s_Primes[16] = { 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 }; Aig_Tru_t ** ppSpot, * pEntry; ppSpot = p->pBins + Aig_RManTableHash( pTruth, nVars, p->nBins, s_Primes ); for ( pEntry = *ppSpot; pEntry; ppSpot = &pEntry->pNext, pEntry = pEntry->pNext ) if ( Kit_TruthIsEqual( pEntry->pTruth, pTruth, nVars ) ) return ppSpot; return ppSpot; } /**Function************************************************************* Synopsis [Find or add new entry.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_RManTableResize( Aig_RMan_t * p ) { Aig_Tru_t * pEntry, * pNext; Aig_Tru_t ** pBinsOld, ** ppPlace; int nBinsOld, Counter, i; abctime clk; assert( p->pBins != NULL ); clk = Abc_Clock(); // save the old Bins pBinsOld = p->pBins; nBinsOld = p->nBins; // get the new Bins p->nBins = Abc_PrimeCudd( 3 * nBinsOld ); p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins ); // rehash the entries from the old table Counter = 0; for ( i = 0; i < nBinsOld; i++ ) for ( pEntry = pBinsOld[i], pNext = pEntry? pEntry->pNext : NULL; pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL ) { // get the place where this entry goes in the Bins ppPlace = Aig_RManTableLookup( p, pEntry->pTruth, pEntry->nVars ); assert( *ppPlace == NULL ); // should not be there // add the entry to the list *ppPlace = pEntry; pEntry->pNext = NULL; Counter++; } assert( Counter == p->nEntries ); // ABC_PRT( "Time", Abc_Clock() - clk ); ABC_FREE( pBinsOld ); } /**Function************************************************************* Synopsis [Find or add new entry.] Description [Returns 1 if this is a new entry.] SideEffects [] SeeAlso [] ***********************************************************************/ int Aig_RManTableFindOrAdd( Aig_RMan_t * p, unsigned * pTruth, int nVars ) { Aig_Tru_t ** ppSpot, * pEntry; int nBytes; ppSpot = Aig_RManTableLookup( p, pTruth, nVars ); if ( *ppSpot ) { (*ppSpot)->nVisits++; return 0; } nBytes = sizeof(Aig_Tru_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars); if ( p->nEntries == 3*p->nBins ) Aig_RManTableResize( p ); pEntry = (Aig_Tru_t *)Aig_MmFlexEntryFetch( p->pMemTrus, nBytes ); pEntry->Id = p->nEntries++; pEntry->nVars = nVars; pEntry->nVisits = 1; pEntry->pNext = NULL; memcpy( pEntry->pTruth, pTruth, sizeof(unsigned) * Kit_TruthWordNum(nVars) ); *ppSpot = pEntry; return 1; } /**Function************************************************************* Synopsis [Deallocates recording manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_RManStop( Aig_RMan_t * p ) { int i; printf( "Total funcs = %10d\n", p->nTotal ); printf( "Full DSD funcs = %10d\n", p->nTtDsd ); printf( "Part DSD funcs = %10d\n", p->nTtDsdPart ); printf( "Non- DSD funcs = %10d\n", p->nTtDsdNot ); printf( "Uniq-var funcs = %10d\n", p->nUniqueVars ); printf( "Unique funcs = %10d\n", p->nEntries ); printf( "Distribution of functions:\n" ); for ( i = 5; i <= p->nVars; i++ ) printf( "%2d = %8d\n", i, p->nVarFuncs[i] ); Aig_MmFlexStop( p->pMemTrus, 0 ); Aig_ManStop( p->pAig ); Bdc_ManFree( p->pBidec ); ABC_FREE( p->pBins ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [Stops recording.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_RManQuit() { // extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); char Buffer[20]; if ( s_pRMan == NULL ) return; // dump the library file sprintf( Buffer, "aiglib%02d.aig", s_pRMan->nVars ); Ioa_WriteAiger( s_pRMan->pAig, Buffer, 0, 1 ); // quit the manager Aig_RManStop( s_pRMan ); s_pRMan = NULL; } /**Function************************************************************* Synopsis [Returns 1 if all variables are unique.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_RManPrintVarProfile( unsigned * pTruth, int nVars, unsigned * pTruthAux ) { int pStore2[32]; int i; Kit_TruthCountOnesInCofsSlow( pTruth, nVars, pStore2, pTruthAux ); for ( i = 0; i < nVars; i++ ) printf( "%2d/%2d ", pStore2[2*i], pStore2[2*i+1] ); printf( "\n" ); } /**Function************************************************************* Synopsis [Sorts numbers in the increasing order.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_RManSortNums( int * pArray, int nVars ) { int i, j, best_i, tmp; for ( i = 0; i < nVars-1; i++ ) { best_i = i; for ( j = i+1; j < nVars; j++ ) if ( pArray[j] > pArray[best_i] ) best_i = j; tmp = pArray[i]; pArray[i] = pArray[best_i]; pArray[best_i] = tmp; } } /**Function************************************************************* Synopsis [Prints signatures for all variables.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_RManPrintSigs( Aig_VSig_t * pSigs, int nVars ) { int v, i, k; for ( v = 0; v < nVars; v++ ) { printf( "%2d : ", v ); for ( k = 0; k < 2; k++ ) { printf( "%5d ", pSigs[2*v+k].nOnes ); printf( "(" ); for ( i = 0; i < nVars; i++ ) printf( "%4d ", pSigs[2*v+k].nCofOnes[i] ); printf( ") " ); } printf( "\n" ); } } /**Function************************************************************* Synopsis [Computes signatures for all variables.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_RManComputeVSigs( unsigned * pTruth, int nVars, Aig_VSig_t * pSigs, unsigned * pAux ) { int v; for ( v = 0; v < nVars; v++ ) { Kit_TruthCofactor0New( pAux, pTruth, nVars, v ); pSigs[2*v+0].nOnes = Kit_TruthCountOnes( pAux, nVars ); Kit_TruthCountOnesInCofs0( pAux, nVars, pSigs[2*v+0].nCofOnes ); Aig_RManSortNums( pSigs[2*v+0].nCofOnes, nVars ); Kit_TruthCofactor1New( pAux, pTruth, nVars, v ); pSigs[2*v+1].nOnes = Kit_TruthCountOnes( pAux, nVars ); Kit_TruthCountOnesInCofs0( pAux, nVars, pSigs[2*v+1].nCofOnes ); Aig_RManSortNums( pSigs[2*v+1].nCofOnes, nVars ); } } /**Function************************************************************* Synopsis [Computs signatures for all variables.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Aig_RManCompareSigs( Aig_VSig_t * p0, Aig_VSig_t * p1, int nVars ) { // return memcmp( p0, p1, sizeof(int) + sizeof(int) * nVars ); return memcmp( p0, p1, sizeof(int) ); } /**Function************************************************************* Synopsis [Returns 1 if all variables are unique.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Aig_RManVarsAreUnique( Aig_VSig_t * pMints, int nVars ) { int i; for ( i = 0; i < nVars - 1; i++ ) if ( Aig_RManCompareSigs( &pMints[2*i], &pMints[2*(i+1)], nVars ) == 0 ) return 0; return 1; } /**Function************************************************************* Synopsis [Returns 1 if all variables are unique.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_RManPrintUniqueVars( Aig_VSig_t * pMints, int nVars ) { int i; for ( i = 0; i < nVars; i++ ) if ( Aig_RManCompareSigs( &pMints[2*i], &pMints[2*i+1], nVars ) == 0 ) printf( "=" ); else printf( "x" ); printf( "\n" ); printf( "0" ); for ( i = 1; i < nVars; i++ ) if ( Aig_RManCompareSigs( &pMints[2*(i-1)], &pMints[2*i], nVars ) == 0 ) printf( "-" ); else if ( i < 10 ) printf( "%c", '0' + i ); else printf( "%c", 'A' + i-10 ); printf( "\n" ); } /**Function************************************************************* Synopsis [Canonicize the truth table.] Description [Returns the phase. ] SideEffects [] SeeAlso [] ***********************************************************************/ unsigned Aig_RManSemiCanonicize( unsigned * pOut, unsigned * pIn, int nVars, char * pCanonPerm, Aig_VSig_t * pSigs, int fReturnIn ) { Aig_VSig_t TempSig; int i, Temp, fChange, Counter; unsigned * pTemp, uCanonPhase = 0; // collect signatures Aig_RManComputeVSigs( pIn, nVars, pSigs, pOut ); // canonicize phase for ( i = 0; i < nVars; i++ ) { // if ( pStore[2*i+0] <= pStore[2*i+1] ) if ( Aig_RManCompareSigs( &pSigs[2*i+0], &pSigs[2*i+1], nVars ) <= 0 ) continue; uCanonPhase |= (1 << i); TempSig = pSigs[2*i+0]; pSigs[2*i+0] = pSigs[2*i+1]; pSigs[2*i+1] = TempSig; Kit_TruthChangePhase( pIn, nVars, i ); } // permute Counter = 0; do { fChange = 0; for ( i = 0; i < nVars-1; i++ ) { // if ( pStore[2*i] <= pStore[2*(i+1)] ) if ( Aig_RManCompareSigs( &pSigs[2*i], &pSigs[2*(i+1)], nVars ) <= 0 ) continue; Counter++; fChange = 1; Temp = pCanonPerm[i]; pCanonPerm[i] = pCanonPerm[i+1]; pCanonPerm[i+1] = Temp; TempSig = pSigs[2*i]; pSigs[2*i] = pSigs[2*(i+1)]; pSigs[2*(i+1)] = TempSig; TempSig = pSigs[2*i+1]; pSigs[2*i+1] = pSigs[2*(i+1)+1]; pSigs[2*(i+1)+1] = TempSig; Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i ); pTemp = pIn; pIn = pOut; pOut = pTemp; } } while ( fChange ); // swap if it was moved an even number of times if ( fReturnIn ^ !(Counter & 1) ) Kit_TruthCopy( pOut, pIn, nVars ); return uCanonPhase; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline Aig_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Aig_NotCond( (Aig_Obj_t *)Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) ); } /**Function************************************************************* Synopsis [Records one function.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_RManSaveOne( Aig_RMan_t * p, unsigned * pTruth, int nVars ) { int i, nNodes, RetValue; Bdc_Fun_t * pFunc; Aig_Obj_t * pTerm; // perform decomposition RetValue = Bdc_ManDecompose( p->pBidec, pTruth, NULL, nVars, NULL, 1000 ); if ( RetValue < 0 ) { printf( "Decomposition failed.\n" ); return; } // convert back into HOP Bdc_FuncSetCopy( Bdc_ManFunc( p->pBidec, 0 ), Aig_ManConst1(p->pAig) ); for ( i = 0; i < nVars; i++ ) Bdc_FuncSetCopy( Bdc_ManFunc( p->pBidec, i+1 ), Aig_IthVar(p->pAig, i) ); nNodes = Bdc_ManNodeNum(p->pBidec); for ( i = nVars + 1; i < nNodes; i++ ) { pFunc = Bdc_ManFunc( p->pBidec, i ); Bdc_FuncSetCopy( pFunc, Aig_And( p->pAig, Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) ); } pTerm = Bdc_FunCopyHop( Bdc_ManRoot(p->pBidec) ); pTerm = Aig_ObjCreateCo( p->pAig, pTerm ); // assert( pTerm->fPhase == 0 ); } /**Function************************************************************* Synopsis [Records one function.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Aig_RManRecord( unsigned * pTruth, int nVarsInit ) { int fVerify = 1; Kit_DsdNtk_t * pNtk; Kit_DsdObj_t * pObj; unsigned uPhaseC; int i, nVars, nWords; int fUniqueVars; if ( nVarsInit > RMAN_MAXVARS ) { printf( "The number of variables in too large.\n" ); return; } if ( s_pRMan == NULL ) s_pRMan = Aig_RManStart(); s_pRMan->nTotal++; // canonicize the function pNtk = Kit_DsdDecompose( pTruth, nVarsInit ); pObj = Kit_DsdNonDsdPrimeMax( pNtk ); if ( pObj == NULL || pObj->nFans == 3 ) { s_pRMan->nTtDsd++; Kit_DsdNtkFree( pNtk ); return; } nVars = pObj->nFans; s_pRMan->nVarFuncs[nVars]++; if ( nVars < nVarsInit ) s_pRMan->nTtDsdPart++; else s_pRMan->nTtDsdNot++; // compute the number of words nWords = Abc_TruthWordNum( nVars ); // copy the function memcpy( s_pRMan->pTruthInit, Kit_DsdObjTruth(pObj), 4*nWords ); Kit_DsdNtkFree( pNtk ); // canonicize the output if ( s_pRMan->pTruthInit[0] & 1 ) Kit_TruthNot( s_pRMan->pTruthInit, s_pRMan->pTruthInit, nVars ); memcpy( s_pRMan->pTruth, s_pRMan->pTruthInit, 4*nWords ); // canonize the function for ( i = 0; i < nVars; i++ ) s_pRMan->pPerm[i] = i; uPhaseC = Aig_RManSemiCanonicize( s_pRMan->pTruthTemp, s_pRMan->pTruth, nVars, s_pRMan->pPerm, s_pRMan->pMints, 1 ); // check unique variables fUniqueVars = Aig_RManVarsAreUnique( s_pRMan->pMints, nVars ); s_pRMan->nUniqueVars += fUniqueVars; /* printf( "%4d : ", s_pRMan->nTotal ); printf( "%2d %2d ", nVarsInit, nVars ); Extra_PrintBinary( stdout, &uPhaseC, nVars ); printf( " " ); for ( i = 0; i < nVars; i++ ) printf( "%2d/%2d ", s_pRMan->pMints[2*i], s_pRMan->pMints[2*i+1] ); printf( "\n" ); Aig_RManPrintUniqueVars( s_pRMan->pMints, nVars ); Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<nTotal ); printf( "%2d %2d ", nVarsInit, nVars ); printf( " " ); printf( "\n" ); Aig_RManPrintUniqueVars( s_pRMan->pMints, nVars ); // Aig_RManPrintSigs( s_pRMan->pMints, nVars ); */ //Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<pTruth, nVars ) ) Aig_RManSaveOne( s_pRMan, s_pRMan->pTruth, nVars ); if ( fVerify ) { // derive reverse permutation for ( i = 0; i < nVars; i++ ) s_pRMan->pPermR[i] = s_pRMan->pPerm[i]; // implement permutation Kit_TruthPermute( s_pRMan->pTruthTemp, s_pRMan->pTruth, nVars, s_pRMan->pPermR, 1 ); // implement polarity for ( i = 0; i < nVars; i++ ) if ( uPhaseC & (1 << i) ) Kit_TruthChangePhase( s_pRMan->pTruth, nVars, i ); // perform verification if ( fUniqueVars && !Kit_TruthIsEqual( s_pRMan->pTruth, s_pRMan->pTruthInit, nVars ) ) printf( "Verification failed.\n" ); } //Aig_RManPrintVarProfile( s_pRMan->pTruth, nVars, s_pRMan->pTruthTemp ); //Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<