diff options
Diffstat (limited to 'src/aig/aig/aigCanon.c')
| -rw-r--r-- | src/aig/aig/aigCanon.c | 694 |
1 files changed, 694 insertions, 0 deletions
diff --git a/src/aig/aig/aigCanon.c b/src/aig/aig/aigCanon.c new file mode 100644 index 00000000..febad8ae --- /dev/null +++ b/src/aig/aig/aigCanon.c @@ -0,0 +1,694 @@ +/**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 "kit.h" +#include "bdc.h" + +//////////////////////////////////////////////////////////////////////// +/// 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; + short 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 = 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 = Aig_PrimeCudd(5000); + p->pBins = 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, clk; + assert( p->pBins != NULL ); +clk = clock(); + // save the old Bins + pBinsOld = p->pBins; + nBinsOld = p->nBins; + // get the new Bins + p->nBins = Aig_PrimeCudd( 3 * nBinsOld ); + p->pBins = 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 ); +// PRT( "Time", clock() - clk ); + 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 ); + free( p->pBins ); + 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 ) +{ + short 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( short * 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(short) * 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( 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_ObjCreatePo( 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 = Aig_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<<nVars ); printf( "\n\n" ); +*/ +/* + printf( "\n" ); + printf( "%4d : ", s_pRMan->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<<nVars ); printf( "\n\n" ); + + if ( Aig_RManTableFindOrAdd( s_pRMan, s_pRMan->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<<nVars ); printf( "\n" ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |