diff options
34 files changed, 1230 insertions, 383 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7bee7f40..bb8f5658 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -4487,22 +4487,26 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) int nPlaMax; int RankCost; int fFastMode; + int fRewriting; + int fSynthesis; int fVerbose; -// extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nPlaMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose ); - extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose ); +// extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nPlaMax, bool fEsop, bool fSop, bool fInvs, bool fVerbose ); + extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nLutMax = 8; - nPlaMax = 128; - RankCost = 96000; - fFastMode = 0; - fVerbose = 0; + nLutMax = 8; + nPlaMax = 128; + RankCost = 96000; + fFastMode = 1; + fRewriting = 1; + fSynthesis = 0; + fVerbose = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfrsvh" ) ) != EOF ) { switch ( c ) { @@ -4542,6 +4546,12 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'f': fFastMode ^= 1; break; + case 'r': + fRewriting ^= 1; + break; + case 's': + fSynthesis ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -4570,8 +4580,8 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) } // run the command -// pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fUseInvs, fVerbose ); - pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fVerbose ); +// pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose ); + pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -4582,12 +4592,14 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: xyz [-L num] [-P num] [-R num] [-fvh]\n" ); + fprintf( pErr, "usage: xyz [-L num] [-P num] [-R num] [-frsvh]\n" ); fprintf( pErr, "\t specilized LUT/PLA decomposition\n" ); fprintf( pErr, "\t-L num : maximum number of LUT inputs (2<=num<=8) [default = %d]\n", nLutMax ); fprintf( pErr, "\t-P num : maximum number of PLA inputs/cubes (8<=num<=128) [default = %d]\n", nPlaMax ); fprintf( pErr, "\t-R num : maximum are of one decomposition rank [default = %d]\n", RankCost ); fprintf( pErr, "\t-f : toggle using fast LUT mapping mode [default = %s]\n", fFastMode? "yes": "no" ); + fprintf( pErr, "\t-r : toggle using one pass of AIG rewriting [default = %s]\n", fRewriting? "yes": "no" ); + fprintf( pErr, "\t-s : toggle using synthesis by AIG rewriting [default = %s]\n", fSynthesis? "yes": "no" ); fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index a3ffcf4e..380b3f8b 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -343,9 +343,11 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ) // Ivy_ManRequiredLevels( pMan ); - Pla_ManFastLutMap( pMan, 8 ); - Ivy_ManStop( pMan ); +// Pla_ManFastLutMap( pMan, 8 ); +// Ivy_ManStop( pMan ); return NULL; + + /* // convert from the AIG manager pNtkAig = Abc_NtkFromAig( pNtk, pMan ); diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index f447516f..b8491d06 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -408,7 +408,7 @@ void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNo int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax ) { // nLevelMax = ((nLevelMax)/2)*3; - assert( pObj->Level <= nLevelMax ); + assert( (int)pObj->Level <= nLevelMax ); // return (int)(100000000.0 * pow(0.999, nLevelMax - pObj->Level)); return (int)(100000000.0 * (1 + 0.01 * pObj->Level)); // return (int)(100000000.0 / ((nLevelMax)/2)*3 - pObj->Level); diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c index a40954bd..d2d731d9 100644 --- a/src/base/abci/abcTiming.c +++ b/src/base/abci/abcTiming.c @@ -647,9 +647,10 @@ void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk ) Vec_Ptr_t * vNodes; Abc_Obj_t * pObj, * pFanout; int i, k, nLevelsCur; - assert( Abc_NtkIsStrash(pNtk) ); +// assert( Abc_NtkIsStrash(pNtk) ); // remember the maximum number of direct levels - pNtk->LevelMax = Abc_AigGetLevelNum(pNtk); +// pNtk->LevelMax = Abc_AigGetLevelNum(pNtk); + pNtk->LevelMax = Abc_NtkGetLevelNum(pNtk); // start the reverse levels pNtk->vLevelsR = Vec_IntAlloc( 0 ); Vec_IntFill( pNtk->vLevelsR, Abc_NtkObjNumMax(pNtk), 0 ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index ecf77f70..5c4a0675 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -136,11 +136,11 @@ void Abc_FrameDeallocate( Abc_Frame_t * p ) { extern void Rwt_ManGlobalStop(); extern void undefine_cube_size(); - extern void Ivy_TruthManStop(); +// extern void Ivy_TruthManStop(); // Abc_HManStop(); undefine_cube_size(); Rwt_ManGlobalStop(); - Ivy_TruthManStop(); +// Ivy_TruthManStop(); if ( p->pManDec ) Dec_ManStop( p->pManDec ); if ( p->dd ) Extra_StopManager( p->dd ); Abc_FrameDeleteAllNetworks( p ); diff --git a/src/misc/nm/nmApi.c b/src/misc/nm/nmApi.c index e44d1ef9..120dbe91 100644 --- a/src/misc/nm/nmApi.c +++ b/src/misc/nm/nmApi.c @@ -46,10 +46,10 @@ Nm_Man_t * Nm_ManCreate( int nSize ) p = ALLOC( Nm_Man_t, 1 ); memset( p, 0, sizeof(Nm_Man_t) ); // set the parameters - p->nSizeFactor = 4; // determined how much larger the table should be compared to data in it - p->nGrowthFactor = 4; // determined how much the table grows after resizing + p->nSizeFactor = 2; // determined how much larger the table should be compared to data in it + p->nGrowthFactor = 3; // determined how much the table grows after resizing // allocate and clean the bins - p->nBins = Cudd_PrimeNm(p->nSizeFactor*nSize); + p->nBins = Cudd_PrimeNm(nSize); p->pBinsI2N = ALLOC( Nm_Entry_t *, p->nBins ); p->pBinsN2I = ALLOC( Nm_Entry_t *, p->nBins ); memset( p->pBinsI2N, 0, sizeof(Nm_Entry_t *) * p->nBins ); @@ -127,6 +127,7 @@ char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, char * pName, char * pSuffix nEntrySize = sizeof(Nm_Entry_t) + strlen(pName) + (pSuffix?strlen(pSuffix):0) + 1; nEntrySize = (nEntrySize / 4 + ((nEntrySize % 4) > 0)) * 4; pEntry = (Nm_Entry_t *)Extra_MmFlexEntryFetch( p->pMem, nEntrySize ); + pEntry->pNextI2N = pEntry->pNextN2I = NULL; pEntry->ObjId = ObjId; sprintf( pEntry->Name, "%s%s", pName, pSuffix? pSuffix : "" ); // add the entry to the hash table diff --git a/src/misc/nm/nmInt.h b/src/misc/nm/nmInt.h index 43901993..8356a4cb 100644 --- a/src/misc/nm/nmInt.h +++ b/src/misc/nm/nmInt.h @@ -45,6 +45,8 @@ typedef struct Nm_Entry_t_ Nm_Entry_t; struct Nm_Entry_t_ { int ObjId; // object ID + Nm_Entry_t * pNextI2N; // the next entry in the ID hash table + Nm_Entry_t * pNextN2I; // the next entry in the name hash table char Name[0]; // name of the object }; diff --git a/src/misc/nm/nmTable.c b/src/misc/nm/nmTable.c index 4243244d..4eeaf610 100644 --- a/src/misc/nm/nmTable.c +++ b/src/misc/nm/nmTable.c @@ -44,7 +44,7 @@ static unsigned Nm_HashString( char * pName, int TableSize ) }; unsigned i, Key = 0; for ( i = 0; pName[i] != '\0'; i++ ) - Key ^= s_Primes[i%10]*pName[i]*pName[i]*pName[i]; + Key ^= s_Primes[i%10]*pName[i]*pName[i]; return Key % TableSize; } @@ -67,13 +67,16 @@ static void Nm_ManResize( Nm_Man_t * p ); ***********************************************************************/ int Nm_ManTableAdd( Nm_Man_t * p, Nm_Entry_t * pEntry ) { - int i; + Nm_Entry_t ** ppSpot; +// int i; // resize the tables if needed - if ( p->nEntries * p->nSizeFactor > p->nBins ) +// if ( p->nEntries * p->nSizeFactor > p->nBins ) + if ( p->nEntries > p->nBins * p->nSizeFactor ) { // Nm_ManPrintTables( p ); Nm_ManResize( p ); } +/* // hash it by ID for ( i = Nm_HashNumber(pEntry->ObjId, p->nBins); p->pBinsI2N[i]; i = (i+1) % p->nBins ) if ( p->pBinsI2N[i] == pEntry ) @@ -86,6 +89,15 @@ int Nm_ManTableAdd( Nm_Man_t * p, Nm_Entry_t * pEntry ) return 0; assert( p->pBinsN2I[i] == NULL ); p->pBinsN2I[i] = pEntry; +*/ + ppSpot = p->pBinsI2N + Nm_HashNumber(pEntry->ObjId, p->nBins); + pEntry->pNextI2N = *ppSpot; + *ppSpot = pEntry; + + ppSpot = p->pBinsN2I + Nm_HashString(pEntry->Name, p->nBins); + pEntry->pNextN2I = *ppSpot; + *ppSpot = pEntry; + // report successfully added entry p->nEntries++; return 1; @@ -121,10 +133,16 @@ int Nm_ManTableDelete( Nm_Man_t * p, Nm_Entry_t * pEntry ) ***********************************************************************/ Nm_Entry_t * Nm_ManTableLookupId( Nm_Man_t * p, int ObjId ) { - int i; + Nm_Entry_t * pEntry; +// int i; +/* for ( i = Nm_HashNumber(ObjId, p->nBins); p->pBinsI2N[i]; i = (i+1) % p->nBins ) if ( p->pBinsI2N[i]->ObjId == ObjId ) return p->pBinsI2N[i]; +*/ + for ( pEntry = p->pBinsI2N[ Nm_HashNumber(ObjId, p->nBins) ]; pEntry; pEntry = pEntry->pNextI2N ) + if ( pEntry->ObjId == ObjId ) + return pEntry; return NULL; } @@ -141,9 +159,10 @@ Nm_Entry_t * Nm_ManTableLookupId( Nm_Man_t * p, int ObjId ) ***********************************************************************/ Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** ppSecond ) { - Nm_Entry_t * pFirst, * pSecond; - int i, Counter = 0; + Nm_Entry_t * pFirst, * pSecond, * pEntry; + int Counter = 0; pFirst = pSecond = NULL; +/* for ( i = Nm_HashString(pName, p->nBins); p->pBinsN2I[i]; i = (i+1) % p->nBins ) if ( strcmp(p->pBinsN2I[i]->Name, pName) == 0 ) { @@ -158,12 +177,60 @@ Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** pp Counter++; if ( Counter > 100 ) printf( "%d ", Counter ); +*/ + for ( pEntry = p->pBinsN2I[ Nm_HashString(pName, p->nBins) ]; pEntry; pEntry = pEntry->pNextN2I ) + if ( strcmp(pEntry->Name, pName) == 0 ) + { + if ( pFirst == NULL ) + pFirst = pEntry; + else if ( pSecond == NULL ) + pSecond = pEntry; + else + assert( 0 ); // name appears more than 2 times + } + // save the names if ( ppSecond ) *ppSecond = pSecond; return pFirst; } +/**Function************************************************************* + + Synopsis [Profiles hash tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nm_ManProfile( Nm_Man_t * p ) +{ + Nm_Entry_t * pEntry; + int Counter, e; + printf( "I2N table: " ); + for ( e = 0; e < p->nBins; e++ ) + { + Counter = 0; + for ( pEntry = p->pBinsI2N[e]; pEntry; pEntry = pEntry->pNextI2N ) + Counter++; + printf( "%d ", Counter ); + } + printf( "\n" ); + printf( "N2I table: " ); + for ( e = 0; e < p->nBins; e++ ) + { + Counter = 0; + for ( pEntry = p->pBinsN2I[e]; pEntry; pEntry = pEntry->pNextN2I ) + Counter++; + printf( "%d ", Counter ); + } + printf( "\n" ); +} + + /**Function************************************************************* @@ -178,8 +245,8 @@ Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** pp ***********************************************************************/ void Nm_ManResize( Nm_Man_t * p ) { - Nm_Entry_t ** pBinsNewI2N, ** pBinsNewN2I, * pEntry; - int nBinsNew, Counter, e, i, clk; + Nm_Entry_t ** pBinsNewI2N, ** pBinsNewN2I, * pEntry, * pEntry2, ** ppSpot; + int nBinsNew, Counter, e, clk; clk = clock(); // get the new table size @@ -192,12 +259,13 @@ clk = clock(); // rehash the entries from the old table Counter = 0; for ( e = 0; e < p->nBins; e++ ) + for ( pEntry = p->pBinsI2N[e], pEntry2 = pEntry? pEntry->pNextI2N : NULL; + pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNextI2N : NULL ) { - pEntry = p->pBinsI2N[e]; - if ( pEntry == NULL ) - continue; - Counter++; - +// pEntry = p->pBinsI2N[e]; +// if ( pEntry == NULL ) +// continue; +/* // hash it by ID for ( i = Nm_HashNumber(pEntry->ObjId, nBinsNew); pBinsNewI2N[i]; i = (i+1) % nBinsNew ) if ( pBinsNewI2N[i] == pEntry ) @@ -210,6 +278,16 @@ clk = clock(); assert( 0 ); assert( pBinsNewN2I[i] == NULL ); pBinsNewN2I[i] = pEntry; +*/ + ppSpot = pBinsNewI2N + Nm_HashNumber(pEntry->ObjId, nBinsNew); + pEntry->pNextI2N = *ppSpot; + *ppSpot = pEntry; + + ppSpot = pBinsNewN2I + Nm_HashString(pEntry->Name, nBinsNew); + pEntry->pNextN2I = *ppSpot; + *ppSpot = pEntry; + + Counter++; } assert( Counter == p->nEntries ); // printf( "Increasing the structural table size from %6d to %6d. ", p->nBins, nBinsNew ); @@ -220,10 +298,10 @@ clk = clock(); p->pBinsI2N = pBinsNewI2N; p->pBinsN2I = pBinsNewN2I; p->nBins = nBinsNew; +// Nm_ManProfile( p ); } - /**Function************************************************************* Synopsis [Returns the smallest prime larger than the number.] diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 4f193cf2..4a97fc91 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -583,6 +583,28 @@ static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry ) /**Function************************************************************* + Synopsis [Returns the pointer to the next nWords entries in the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned * Vec_IntFetch( Vec_Int_t * p, int nWords ) +{ + p->nSize += nWords; + if ( p->nSize > p->nCap ) + { +// Vec_IntGrow( p, 2 * p->nSize ); + return NULL; + } + return ((unsigned *)p->pArray) + p->nSize - nWords; +} + +/**Function************************************************************* + Synopsis [Returns the last entry and removes it from the list.] Description [] diff --git a/src/opt/cut/abcCut.c b/src/opt/cut/abcCut.c new file mode 100644 index 00000000..b4b879a3 --- /dev/null +++ b/src/opt/cut/abcCut.c @@ -0,0 +1,491 @@ +/**CFile**************************************************************** + + FileName [abcCut.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Interface to cut computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "cut.h" +#include "seqInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq ); +static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq ); + + +extern int nTotal, nGood, nEqual; + +// temporary +//Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) { return NULL; } +Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vAttrs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 ); + int i; + Abc_Obj_t * pObj; + +// Abc_NtkForEachCi( pNtk, pObj, i ) +// Vec_IntWriteEntry( vAttrs, pObj->Id, 1 ); + + Abc_NtkForEachObj( pNtk, pObj, i ) + { +// if ( Abc_ObjIsNode(pObj) && (rand() % 4 == 0) ) + if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj) && (rand() % 3 == 0) ) + Vec_IntWriteEntry( vAttrs, pObj->Id, 1 ); + } + return vAttrs; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes the cuts for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) +{ + ProgressBar * pProgress; + Cut_Man_t * p; + Abc_Obj_t * pObj, * pNode; + Vec_Ptr_t * vNodes; + Vec_Int_t * vChoices; + int i; + int clk = clock(); + + extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk ); + extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk ); + + nTotal = nGood = nEqual = 0; + + assert( Abc_NtkIsStrash(pNtk) ); + // start the manager + pParams->nIdsMax = Abc_NtkObjNumMax( pNtk ); + p = Cut_ManStart( pParams ); + // compute node attributes if local or global cuts are requested + if ( pParams->fGlobal || pParams->fLocal ) + { + extern Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ); + Cut_ManSetNodeAttrs( p, Abc_NtkGetNodeAttributes(pNtk) ); + } + // prepare for cut dropping + if ( pParams->fDrop ) + Cut_ManSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) ); + // set cuts for PIs + Abc_NtkForEachCi( pNtk, pObj, i ) + if ( Abc_ObjFanoutNum(pObj) > 0 ) + Cut_NodeSetTriv( p, pObj->Id ); + // compute cuts for internal nodes + vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs + vChoices = Vec_IntAlloc( 100 ); + pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodes) ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // when we reached a CO, it is time to deallocate the cuts + if ( Abc_ObjIsCo(pObj) ) + { + if ( pParams->fDrop ) + Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) ); + continue; + } + // skip constant node, it has no cuts + if ( Abc_NodeIsConst(pObj) ) + continue; + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // compute the cuts to the internal node + Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree ); + // consider dropping the fanins cuts + if ( pParams->fDrop ) + { + Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) ); + Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId1(pObj) ); + } + // add cuts due to choices + if ( Abc_NodeIsAigChoice(pObj) ) + { + Vec_IntClear( vChoices ); + for ( pNode = pObj; pNode; pNode = pNode->pData ) + Vec_IntPush( vChoices, pNode->Id ); + Cut_NodeUnionCuts( p, vChoices ); + } + } + Extra_ProgressBarStop( pProgress ); + Vec_PtrFree( vNodes ); + Vec_IntFree( vChoices ); +PRT( "Total", clock() - clk ); +//Abc_NtkPrintCuts( p, pNtk, 0 ); +// Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk ); + + // temporary printout of stats + if ( nTotal ) + printf( "Total cuts = %d. Good cuts = %d. Ratio = %5.2f\n", nTotal, nGood, ((double)nGood)/nTotal ); + return p; +} + +/**Function************************************************************* + + Synopsis [Cut computation using the oracle.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p ) +{ + Abc_Obj_t * pObj; + Vec_Ptr_t * vNodes; + int i, clk = clock(); + int fDrop = Cut_OracleReadDrop(p); + + assert( Abc_NtkIsStrash(pNtk) ); + + // prepare cut droppping + if ( fDrop ) + Cut_OracleSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) ); + + // set cuts for PIs + Abc_NtkForEachCi( pNtk, pObj, i ) + if ( Abc_ObjFanoutNum(pObj) > 0 ) + Cut_OracleNodeSetTriv( p, pObj->Id ); + + // compute cuts for internal nodes + vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // when we reached a CO, it is time to deallocate the cuts + if ( Abc_ObjIsCo(pObj) ) + { + if ( fDrop ) + Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId0(pObj) ); + continue; + } + // skip constant node, it has no cuts + if ( Abc_NodeIsConst(pObj) ) + continue; + // compute the cuts to the internal node + Cut_OracleComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj), + Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + // consider dropping the fanins cuts + if ( fDrop ) + { + Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId0(pObj) ); + Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId1(pObj) ); + } + } + Vec_PtrFree( vNodes ); +//PRT( "Total", clock() - clk ); +//Abc_NtkPrintCuts_( p, pNtk, 0 ); +} + + +/**Function************************************************************* + + Synopsis [Computes the cuts for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) +{ + Cut_Man_t * p; + Abc_Obj_t * pObj, * pNode; + int i, nIters, fStatus; + Vec_Int_t * vChoices; + int clk = clock(); + + assert( Abc_NtkIsSeq(pNtk) ); + assert( pParams->fSeq ); +// assert( Abc_NtkIsDfsOrdered(pNtk) ); + + // start the manager + pParams->nIdsMax = Abc_NtkObjNumMax( pNtk ); + pParams->nCutSet = Abc_NtkCutSetNodeNum( pNtk ); + p = Cut_ManStart( pParams ); + + // set cuts for the constant node and the PIs + pObj = Abc_NtkConst1(pNtk); + if ( Abc_ObjFanoutNum(pObj) > 0 ) + Cut_NodeSetTriv( p, pObj->Id ); + Abc_NtkForEachPi( pNtk, pObj, i ) + { +//printf( "Setting trivial cut %d.\n", pObj->Id ); + Cut_NodeSetTriv( p, pObj->Id ); + } + // label the cutset nodes and set their number in the array + // assign the elementary cuts to the cutset nodes + Abc_SeqForEachCutsetNode( pNtk, pObj, i ) + { + assert( pObj->fMarkC == 0 ); + pObj->fMarkC = 1; + pObj->pCopy = (Abc_Obj_t *)i; + Cut_NodeSetTriv( p, pObj->Id ); +//printf( "Setting trivial cut %d.\n", pObj->Id ); + } + + // process the nodes + vChoices = Vec_IntAlloc( 100 ); + for ( nIters = 0; nIters < 10; nIters++ ) + { +//printf( "ITERATION %d:\n", nIters ); + // compute the cuts for the internal nodes + Abc_AigForEachAnd( pNtk, pObj, i ) + { + Abc_NodeGetCutsSeq( p, pObj, nIters==0 ); + // add cuts due to choices + if ( Abc_NodeIsAigChoice(pObj) ) + { + Vec_IntClear( vChoices ); + for ( pNode = pObj; pNode; pNode = pNode->pData ) + Vec_IntPush( vChoices, pNode->Id ); + Cut_NodeUnionCutsSeq( p, vChoices, (pObj->fMarkC ? (int)pObj->pCopy : -1), nIters==0 ); + } + } + // merge the new cuts with the old cuts + Abc_NtkForEachPi( pNtk, pObj, i ) + Cut_NodeNewMergeWithOld( p, pObj->Id ); + Abc_AigForEachAnd( pNtk, pObj, i ) + Cut_NodeNewMergeWithOld( p, pObj->Id ); + // for the cutset, transfer temp cuts to new cuts + fStatus = 0; + Abc_SeqForEachCutsetNode( pNtk, pObj, i ) + fStatus |= Cut_NodeTempTransferToNew( p, pObj->Id, i ); + if ( fStatus == 0 ) + break; + } + Vec_IntFree( vChoices ); + + // if the status is not finished, transfer new to old for the cutset + Abc_SeqForEachCutsetNode( pNtk, pObj, i ) + Cut_NodeNewMergeWithOld( p, pObj->Id ); + + // transfer the old cuts to the new positions + Abc_NtkForEachObj( pNtk, pObj, i ) + Cut_NodeOldTransferToNew( p, pObj->Id ); + + // unlabel the cutset nodes + Abc_SeqForEachCutsetNode( pNtk, pObj, i ) + pObj->fMarkC = 0; +if ( pParams->fVerbose ) +{ +PRT( "Total", clock() - clk ); +printf( "Converged after %d iterations.\n", nIters ); +} +//Abc_NtkPrintCuts( p, pNtk, 1 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Computes the cuts for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree ) +{ + void * pList; + if ( pList = Abc_NodeReadCuts( p, pObj ) ) + return pList; + Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fDag, fTree ); + Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fDag, fTree ); + return Abc_NodeGetCuts( p, pObj, fDag, fTree ); +} + +/**Function************************************************************* + + Synopsis [Computes the cuts for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree ) +{ + Abc_Obj_t * pFanin; + int fDagNode, fTriv, TreeCode = 0; +// assert( Abc_NtkIsStrash(pObj->pNtk) ); + assert( Abc_ObjFaninNum(pObj) == 2 ); + + + // check if the node is a DAG node + fDagNode = (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj)); + // increment the counter of DAG nodes + if ( fDagNode ) Cut_ManIncrementDagNodes( p ); + // add the trivial cut if the node is a DAG node, or if we compute all cuts + fTriv = fDagNode || !fDag; + // check if fanins are DAG nodes + if ( fTree ) + { + pFanin = Abc_ObjFanin0(pObj); + TreeCode |= (Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin)); + pFanin = Abc_ObjFanin1(pObj); + TreeCode |= ((Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin)) << 1); + } + + + // changes due to the global/local cut computation + { + Cut_Params_t * pParams = Cut_ManReadParams(p); + if ( pParams->fLocal ) + { + Vec_Int_t * vNodeAttrs = Cut_ManReadNodeAttrs(p); + fDagNode = Vec_IntEntry( vNodeAttrs, pObj->Id ); + if ( fDagNode ) Cut_ManIncrementDagNodes( p ); +// fTriv = fDagNode || !pParams->fGlobal; + fTriv = !Vec_IntEntry( vNodeAttrs, pObj->Id ); + TreeCode = 0; + pFanin = Abc_ObjFanin0(pObj); + TreeCode |= Vec_IntEntry( vNodeAttrs, pFanin->Id ); + pFanin = Abc_ObjFanin1(pObj); + TreeCode |= (Vec_IntEntry( vNodeAttrs, pFanin->Id ) << 1); + } + } + return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj), + Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv, TreeCode ); +} + +/**Function************************************************************* + + Synopsis [Computes the cuts for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fTriv ) +{ + int CutSetNum; + assert( Abc_NtkIsSeq(pObj->pNtk) ); + assert( Abc_ObjFaninNum(pObj) == 2 ); + fTriv = pObj->fMarkC ? 0 : fTriv; + CutSetNum = pObj->fMarkC ? (int)pObj->pCopy : -1; + Cut_NodeComputeCutsSeq( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj), + Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), Seq_ObjFaninL0(pObj), Seq_ObjFaninL1(pObj), fTriv, CutSetNum ); +} + +/**Function************************************************************* + + Synopsis [Computes the cuts for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj ) +{ + return Cut_NodeReadCutsNew( p, pObj->Id ); +} + +/**Function************************************************************* + + Synopsis [Computes the cuts for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj ) +{ + Cut_NodeFreeCuts( p, pObj->Id ); +} + +/**Function************************************************************* + + Synopsis [Computes the cuts for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq ) +{ + Cut_Man_t * pMan = p; + Cut_Cut_t * pList; + Abc_Obj_t * pObj; + int i; + printf( "Cuts of the network:\n" ); + Abc_NtkForEachObj( pNtk, pObj, i ) + { + pList = Abc_NodeReadCuts( p, pObj ); + printf( "Node %s:\n", Abc_ObjName(pObj) ); + Cut_CutPrintList( pList, fSeq ); + } +} + +/**Function************************************************************* + + Synopsis [Computes the cuts for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq ) +{ + Cut_Man_t * pMan = p; + Cut_Cut_t * pList; + Abc_Obj_t * pObj; + pObj = Abc_NtkObj( pNtk, 2 * Abc_NtkObjNum(pNtk) / 3 ); + pList = Abc_NodeReadCuts( p, pObj ); + printf( "Node %s:\n", Abc_ObjName(pObj) ); + Cut_CutPrintList( pList, fSeq ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/cut/cut60720.zip b/src/opt/cut/cut60720.zip Binary files differnew file mode 100644 index 00000000..86ad6726 --- /dev/null +++ b/src/opt/cut/cut60720.zip diff --git a/src/opt/cut/cut60721.zip b/src/opt/cut/cut60721.zip Binary files differnew file mode 100644 index 00000000..d55ccfd0 --- /dev/null +++ b/src/opt/cut/cut60721.zip diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c index adff525f..1f93b14b 100644 --- a/src/opt/cut/cutNode.c +++ b/src/opt/cut/cutNode.c @@ -399,11 +399,9 @@ p->timeMerge += clock() - clk; // set the list at the node Vec_PtrFillExtra( p->vCutsNew, Node + 1, NULL ); assert( Cut_NodeReadCutsNew(p, Node) == NULL ); - ///// - pList->pNext = NULL; +// pList->pNext = NULL; ///// - Cut_NodeWriteCutsNew( p, Node, pList ); // filter the cuts //clk = clock(); diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c index f808d9bc..23925669 100644 --- a/src/sat/msat/msatActivity.c +++ b/src/sat/msat/msatActivity.c @@ -46,7 +46,7 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit ) return; Var = MSAT_LIT2VAR(Lit); if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 ) -// if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pLevel[Var])) > 1e100 ) +// if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pActLevels[Var])) > 1e100 ) Msat_SolverVarRescaleActivity( p ); Msat_OrderUpdate( p->pOrder, Var ); } diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index 15932c67..7845ec0b 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -119,7 +119,7 @@ struct Msat_Solver_t_ double dClaDecay; // INVERSE decay factor for clause activity: stores 1/decay. double * pdActivity; // A heuristic measurement of the activity of a variable. - int * pLevels; // the levels of the variables + int * pActLevels; // the levels of the variables double dVarInc; // Amount to bump next variable with. double dVarDecay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order. Msat_Order_t * pOrder; // Keeps track of the decision variable order. diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c index 8c1542df..9317dcac 100644 --- a/src/sat/msat/msatSolverApi.c +++ b/src/sat/msat/msatSolverApi.c @@ -174,11 +174,11 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, p->dVarDecay = dVarDecay; p->pdActivity = ALLOC( double, p->nVarsAlloc ); - p->pLevels = ALLOC( int, p->nVarsAlloc ); + p->pActLevels = ALLOC( int, p->nVarsAlloc ); for ( i = 0; i < p->nVarsAlloc; i++ ) { p->pdActivity[i] = 0; - p->pLevels = 0; + p->pActLevels[i] = 0; } p->pAssigns = ALLOC( int, p->nVarsAlloc ); @@ -243,7 +243,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc ) p->nVarsAlloc = nVarsAlloc; p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc ); - p->pLevels = REALLOC( int, p->pLevels, p->nVarsAlloc ); + p->pActLevels = REALLOC( int, p->pActLevels, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) p->pdActivity[i] = 0; @@ -399,7 +399,7 @@ void Msat_SolverFree( Msat_Solver_t * p ) Msat_ClauseVecFree( p->vLearned ); FREE( p->pdActivity ); - FREE( p->pLevels ); + FREE( p->pActLevels ); Msat_OrderFree( p->pOrder ); for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h index 7fb054f7..a36c795b 100644 --- a/src/temp/ivy/ivy.h +++ b/src/temp/ivy/ivy.h @@ -66,7 +66,7 @@ typedef enum { } Ivy_Init_t; // the AIG node -struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit) +struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit) // 10 words - 16 words { int Id; // integer ID int TravId; // traversal ID @@ -81,6 +81,10 @@ struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit) Ivy_Obj_t * pFanin0; // fanin Ivy_Obj_t * pFanin1; // fanin Ivy_Obj_t * pFanout; // fanout + Ivy_Obj_t * pNextFan0; // next fanout of the first fanin + Ivy_Obj_t * pNextFan1; // next fanout of the second fanin + Ivy_Obj_t * pPrevFan0; // prev fanout of the first fanin + Ivy_Obj_t * pPrevFan1; // prev fanout of the second fanin Ivy_Obj_t * pEquiv; // equivalent node }; @@ -106,7 +110,8 @@ struct Ivy_Man_t_ int nTravIds; // the traversal ID int nLevelMax; // the maximum level Vec_Int_t * vRequired; // required times - Vec_Ptr_t * vFanouts; // representation of the fanouts +// Vec_Ptr_t * vFanouts; // representation of the fanouts + int fFanout; // fanout is allocated void * pData; // the temporary data void * pCopy; // the temporary data // memory management @@ -384,6 +389,7 @@ extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * extern Ivy_Obj_t * Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init ); /*=== ivyCheck.c ========================================================*/ extern int Ivy_ManCheck( Ivy_Man_t * p ); +extern int Ivy_ManCheckFanouts( Ivy_Man_t * p ); /*=== ivyCut.c ==========================================================*/ extern void Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize ); extern Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves ); @@ -407,12 +413,10 @@ extern void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Ob extern void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ); extern void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew ); extern void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray ); -extern Ivy_Obj_t * Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj ); /*=== ivyIsop.c ==========================================================*/ -extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover ); -extern void Ivy_TruthManStop(); +extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth ); /*=== ivyMan.c ==========================================================*/ extern Ivy_Man_t * Ivy_ManStart(); extern void Ivy_ManStop( Ivy_Man_t * p ); @@ -450,6 +454,7 @@ extern Ivy_Obj_t * Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, I extern Ivy_Obj_t * Ivy_Miter( Ivy_Man_t * p, Vec_Ptr_t * vPairs ); extern Ivy_Obj_t * Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init ); /*=== ivyResyn.c =========================================================*/ +extern Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * p, int fUpdateLevel, int fVerbose ); extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbose ); /*=== ivyRewrite.c =========================================================*/ extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c index 36222f72..ebae64ff 100644 --- a/src/temp/ivy/ivyCheck.c +++ b/src/temp/ivy/ivyCheck.c @@ -115,7 +115,7 @@ int Ivy_ManCheck( Ivy_Man_t * p ) if ( Ivy_ObjRefs(pObj) == 0 ) printf( "Ivy_ManCheck: Node with ID \"%d\" has no fanouts.\n", pObj->Id ); // check fanouts - if ( p->vFanouts && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) ) + if ( p->fFanout && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) ) printf( "Ivy_ManCheck: Node with ID \"%d\" has mismatch between the number of fanouts and refs.\n", pObj->Id ); } // count the number of nodes in the table @@ -124,9 +124,95 @@ int Ivy_ManCheck( Ivy_Man_t * p ) printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" ); return 0; } +// if ( !Ivy_ManCheckFanouts(p) ) +// return 0; if ( !Ivy_ManIsAcyclic(p) ) return 0; - return 1; + return 1; +} + +/**Function************************************************************* + + Synopsis [Verifies the fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManCheckFanouts( Ivy_Man_t * p ) +{ + Vec_Ptr_t * vFanouts; + Ivy_Obj_t * pObj, * pFanout, * pFanin; + int i, k, RetValue = 1; + if ( !p->fFanout ) + return 1; + vFanouts = Vec_PtrAlloc( 100 ); + // make sure every fanin is a fanout + Ivy_ManForEachObj( p, pObj, i ) + { + pFanin = Ivy_ObjFanin0(pObj); + if ( pFanin == NULL ) + continue; + Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k ) + if ( pFanout == pObj ) + break; + if ( k == Vec_PtrSize(vFanouts) ) + { + printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id ); + RetValue = 0; + } + + pFanin = Ivy_ObjFanin1(pObj); + if ( pFanin == NULL ) + continue; + Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k ) + if ( pFanout == pObj ) + break; + if ( k == Vec_PtrSize(vFanouts) ) + { + printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id ); + RetValue = 0; + } + // check that the previous fanout has the same fanin + if ( pObj->pPrevFan0 ) + { + if ( Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && + Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) && + Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && + Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) ) + { + printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan0->Id ); + RetValue = 0; + } + } + // check that the previous fanout has the same fanin + if ( pObj->pPrevFan1 ) + { + if ( Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && + Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) && + Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && + Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) ) + { + printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan1->Id ); + RetValue = 0; + } + } + } + // make sure every fanout is a fanin + Ivy_ManForEachObj( p, pObj, i ) + { + Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, k ) + if ( Ivy_ObjFanin0(pFanout) != pObj && Ivy_ObjFanin1(pFanout) != pObj ) + { + printf( "Node %d is a fanout of node %d but the fanin is not there.\n", pFanout->Id, pObj->Id ); + RetValue = 0; + } + } + Vec_PtrFree( vFanouts ); + return RetValue; } //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c index 56f872e9..65ba4aac 100644 --- a/src/temp/ivy/ivyCut.c +++ b/src/temp/ivy/ivyCut.c @@ -867,6 +867,24 @@ void Ivy_NodePrintCuts( Ivy_Store_t * pCutStore ) SeeAlso [] ***********************************************************************/ +static inline Ivy_Obj_t * Ivy_ObjRealFanin( Ivy_Obj_t * pObj ) +{ + if ( !Ivy_ObjIsBuf(pObj) ) + return pObj; + return Ivy_ObjRealFanin( Ivy_ObjFanin0(pObj) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves ) { static Ivy_Store_t CutStore, * pCutStore = &CutStore; @@ -911,11 +929,14 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves continue; Ivy_NodeCutHash( pCutNew ); */ - iLeaf0 = Ivy_ObjFaninId0(pLeaf); - iLeaf1 = Ivy_ObjFaninId1(pLeaf); + iLeaf0 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin0(pLeaf)) ); + iLeaf1 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin1(pLeaf)) ); if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) ) continue; - Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 ); + if ( iLeaf0 > iLeaf1 ) + Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf1, iLeaf0 ); + else + Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 ); Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew ); if ( pCutStore->nCuts == IVY_CUT_LIMIT ) break; diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c index 30671baf..7246ec25 100644 --- a/src/temp/ivy/ivyDfs.c +++ b/src/temp/ivy/ivyDfs.c @@ -265,7 +265,7 @@ int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode ) { if ( Ivy_ObjIsCi(pNode) || Ivy_ObjIsConst1(pNode) ) return 1; - assert( Ivy_ObjIsNode( pNode ) ); + assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) ); // make sure the node is not visited assert( !Ivy_ObjIsTravIdPrevious(p, pNode) ); // check if the node is part of the combinational loop @@ -290,7 +290,7 @@ int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode ) } } // check if the fanin is visited - if ( !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) ) + if ( Ivy_ObjIsNode(pNode) && !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) ) { // traverse the fanin's cone searching for the loop if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pNode)) ) diff --git a/src/temp/ivy/ivyFanout.c b/src/temp/ivy/ivyFanout.c index 2295516d..3930186a 100644 --- a/src/temp/ivy/ivyFanout.c +++ b/src/temp/ivy/ivyFanout.c @@ -24,9 +24,96 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Ivy_FanoutIsArray( void * p ) { return (int )(((unsigned)p) & 01); } -static inline Vec_Ptr_t * Ivy_FanoutGetArray( void * p ) { assert( Ivy_FanoutIsArray(p) ); return (Vec_Ptr_t *)((unsigned)(p) & ~01); } -static inline Vec_Ptr_t * Ivy_FanoutSetArray( void * p ) { assert( !Ivy_FanoutIsArray(p) ); return (Vec_Ptr_t *)((unsigned)(p) ^ 01); } +// getting hold of the next fanout of the node +static inline Ivy_Obj_t * Ivy_ObjNextFanout( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +{ + assert( !Ivy_IsComplement(pObj) ); + assert( !Ivy_IsComplement(pFanout) ); + if ( pFanout == NULL ) + return NULL; + if ( Ivy_ObjFanin0(pFanout) == pObj ) + return pFanout->pNextFan0; + assert( Ivy_ObjFanin1(pFanout) == pObj ); + return pFanout->pNextFan1; +} + +// getting hold of the previous fanout of the node +static inline Ivy_Obj_t * Ivy_ObjPrevFanout( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +{ + assert( !Ivy_IsComplement(pObj) ); + assert( !Ivy_IsComplement(pFanout) ); + if ( pFanout == NULL ) + return NULL; + if ( Ivy_ObjFanin0(pFanout) == pObj ) + return pFanout->pPrevFan0; + assert( Ivy_ObjFanin1(pFanout) == pObj ); + return pFanout->pPrevFan1; +} + +// getting hold of the place where the next fanout will be attached +static inline Ivy_Obj_t ** Ivy_ObjNextFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +{ + assert( !Ivy_IsComplement(pObj) ); + assert( !Ivy_IsComplement(pFanout) ); + if ( Ivy_ObjFanin0(pFanout) == pObj ) + return &pFanout->pNextFan0; + assert( Ivy_ObjFanin1(pFanout) == pObj ); + return &pFanout->pNextFan1; +} + +// getting hold of the place where the next fanout will be attached +static inline Ivy_Obj_t ** Ivy_ObjPrevFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +{ + assert( !Ivy_IsComplement(pObj) ); + assert( !Ivy_IsComplement(pFanout) ); + if ( Ivy_ObjFanin0(pFanout) == pObj ) + return &pFanout->pPrevFan0; + assert( Ivy_ObjFanin1(pFanout) == pObj ); + return &pFanout->pPrevFan1; +} + +// getting hold of the place where the next fanout will be attached +static inline Ivy_Obj_t ** Ivy_ObjPrevNextFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +{ + Ivy_Obj_t * pTemp; + assert( !Ivy_IsComplement(pObj) ); + assert( !Ivy_IsComplement(pFanout) ); + pTemp = Ivy_ObjPrevFanout(pObj, pFanout); + if ( pTemp == NULL ) + return &pObj->pFanout; + if ( Ivy_ObjFanin0(pTemp) == pObj ) + return &pTemp->pNextFan0; + assert( Ivy_ObjFanin1(pTemp) == pObj ); + return &pTemp->pNextFan1; +} + +// getting hold of the place where the next fanout will be attached +static inline Ivy_Obj_t ** Ivy_ObjNextPrevFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +{ + Ivy_Obj_t * pTemp; + assert( !Ivy_IsComplement(pObj) ); + assert( !Ivy_IsComplement(pFanout) ); + pTemp = Ivy_ObjNextFanout(pObj, pFanout); + if ( pTemp == NULL ) + return NULL; + if ( Ivy_ObjFanin0(pTemp) == pObj ) + return &pTemp->pPrevFan0; + assert( Ivy_ObjFanin1(pTemp) == pObj ); + return &pTemp->pPrevFan1; +} + +// iterator through the fanouts of the node +#define Ivy_ObjForEachFanoutInt( pObj, pFanout ) \ + for ( pFanout = (pObj)->pFanout; pFanout; \ + pFanout = Ivy_ObjNextFanout(pObj, pFanout) ) + +// safe iterator through the fanouts of the node +#define Ivy_ObjForEachFanoutIntSafe( pObj, pFanout, pFanout2 ) \ + for ( pFanout = (pObj)->pFanout, \ + pFanout2 = Ivy_ObjNextFanout(pObj, pFanout); \ + pFanout; \ + pFanout = pFanout2, \ + pFanout2 = Ivy_ObjNextFanout(pObj, pFanout) ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -47,8 +134,8 @@ void Ivy_ManStartFanout( Ivy_Man_t * p ) { Ivy_Obj_t * pObj; int i; - assert( p->vFanouts == NULL ); - p->vFanouts = Vec_PtrStart( Ivy_ManObjIdMax(p) + 1000 ); + assert( !p->fFanout ); + p->fFanout = 1; Ivy_ManForEachObj( p, pObj, i ) { if ( Ivy_ObjFanin0(pObj) ) @@ -71,14 +158,12 @@ void Ivy_ManStartFanout( Ivy_Man_t * p ) ***********************************************************************/ void Ivy_ManStopFanout( Ivy_Man_t * p ) { - void * pTemp; + Ivy_Obj_t * pObj; int i; - assert( p->vFanouts != NULL ); - Vec_PtrForEachEntry( p->vFanouts, pTemp, i ) - if ( Ivy_FanoutIsArray(pTemp) ) - Vec_PtrFree( Ivy_FanoutGetArray(pTemp) ); - Vec_PtrFree( p->vFanouts ); - p->vFanouts = NULL; + assert( p->fFanout ); + p->fFanout = 0; + Ivy_ManForEachObj( p, pObj, i ) + pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL; } /**Function************************************************************* @@ -92,31 +177,15 @@ void Ivy_ManStopFanout( Ivy_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pFanin, Ivy_Obj_t * pFanout ) { - Vec_Ptr_t * vNodes; - void ** ppSpot; - assert( p->vFanouts != NULL ); - assert( !Ivy_IsComplement(pObj) ); - // extend the fanout array if needed - Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); - // get the pointer to the place where fanouts are stored - ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id ); - // consider several cases - if ( *ppSpot == NULL ) // no fanout - add one fanout - *ppSpot = pFanout; - else if ( Ivy_FanoutIsArray(*ppSpot) ) // array of fanouts - add one fanout + assert( p->fFanout ); + if ( pFanin->pFanout ) { - vNodes = Ivy_FanoutGetArray(*ppSpot); - Vec_PtrPush( vNodes, pFanout ); - } - else // only one fanout - create array and put both fanouts into the array - { - vNodes = Vec_PtrAlloc( 4 ); - Vec_PtrPush( vNodes, *ppSpot ); - Vec_PtrPush( vNodes, pFanout ); - *ppSpot = Ivy_FanoutSetArray( vNodes ); + *Ivy_ObjNextFanoutPlace(pFanin, pFanout) = pFanin->pFanout; + *Ivy_ObjPrevFanoutPlace(pFanin, pFanin->pFanout) = pFanout; } + pFanin->pFanout = pFanout; } /**Function************************************************************* @@ -130,30 +199,25 @@ void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) SeeAlso [] ***********************************************************************/ -void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pFanin, Ivy_Obj_t * pFanout ) { - Vec_Ptr_t * vNodes; - void ** ppSpot; - assert( p->vFanouts != NULL ); - assert( !Ivy_IsComplement(pObj) ); - // extend the fanout array if needed - Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); - ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id ); - if ( *ppSpot == NULL ) // no fanout - should not happen - { - assert( 0 ); - } - else if ( Ivy_FanoutIsArray(*ppSpot) ) // the array of fanouts - delete the fanout - { - vNodes = Ivy_FanoutGetArray(*ppSpot); - Vec_PtrRemove( vNodes, pFanout ); - } - else // only one fanout - delete the fanout - { - assert( *ppSpot == pFanout ); - *ppSpot = NULL; - } -// printf( " %d", Ivy_ObjFanoutNum(p, pObj) ); + Ivy_Obj_t ** ppPlace1, ** ppPlace2, ** ppPlaceN; + assert( pFanin->pFanout != NULL ); + + ppPlace1 = Ivy_ObjNextFanoutPlace(pFanin, pFanout); + ppPlaceN = Ivy_ObjPrevNextFanoutPlace(pFanin, pFanout); + assert( *ppPlaceN == pFanout ); + if ( ppPlaceN ) + *ppPlaceN = *ppPlace1; + + ppPlace2 = Ivy_ObjPrevFanoutPlace(pFanin, pFanout); + ppPlaceN = Ivy_ObjNextPrevFanoutPlace(pFanin, pFanout); + assert( ppPlaceN == NULL || *ppPlaceN == pFanout ); + if ( ppPlaceN ) + *ppPlaceN = *ppPlace2; + + *ppPlace1 = NULL; + *ppPlace2 = NULL; } /**Function************************************************************* @@ -167,32 +231,18 @@ void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) SeeAlso [] ***********************************************************************/ -void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew ) +void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pFanin, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew ) { - Vec_Ptr_t * vNodes; - void ** ppSpot; - int Index; - assert( p->vFanouts != NULL ); - assert( !Ivy_IsComplement(pObj) ); - // extend the fanout array if needed - Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); - ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id ); - if ( *ppSpot == NULL ) // no fanout - should not happen - { - assert( 0 ); - } - else if ( Ivy_FanoutIsArray(*ppSpot) ) // the array of fanouts - find and replace the fanout - { - vNodes = Ivy_FanoutGetArray(*ppSpot); - Index = Vec_PtrFind( vNodes, pFanoutOld ); - assert( Index >= 0 ); - Vec_PtrWriteEntry( vNodes, Index, pFanoutNew ); - } - else // only one fanout - delete the fanout - { - assert( *ppSpot == pFanoutOld ); - *ppSpot = pFanoutNew; - } + Ivy_Obj_t ** ppPlace; + ppPlace = Ivy_ObjPrevNextFanoutPlace(pFanin, pFanoutOld); + assert( *ppPlace == pFanoutOld ); + if ( ppPlace ) + *ppPlace = pFanoutNew; + ppPlace = Ivy_ObjNextPrevFanoutPlace(pFanin, pFanoutOld); + assert( ppPlace == NULL || *ppPlace == pFanoutOld ); + if ( ppPlace ) + *ppPlace = pFanoutNew; + // assuming that pFanoutNew already points to the next fanout } /**Function************************************************************* @@ -208,52 +258,12 @@ void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld ***********************************************************************/ void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray ) { - Vec_Ptr_t * vNodes; - Ivy_Obj_t * pTemp; - int i; - assert( p->vFanouts != NULL ); + Ivy_Obj_t * pFanout; + assert( p->fFanout ); assert( !Ivy_IsComplement(pObj) ); - // extend the fanout array if needed - Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); - vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id ); - // clean the resulting array Vec_PtrClear( vArray ); - if ( vNodes == NULL ) // no fanout - nothing to do - { - } - else if ( Ivy_FanoutIsArray(vNodes) ) // the array of fanouts - copy fanouts - { - vNodes = Ivy_FanoutGetArray(vNodes); - Vec_PtrForEachEntry( vNodes, pTemp, i ) - Vec_PtrPush( vArray, pTemp ); - } - else // only one fanout - add the fanout - Vec_PtrPush( vArray, vNodes ); -} - -/**Function************************************************************* - - Synopsis [Reads one fanout.] - - Description [Returns fanout if there is only one fanout.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ) -{ - Vec_Ptr_t * vNodes; - assert( p->vFanouts != NULL ); - assert( !Ivy_IsComplement(pObj) ); - // extend the fanout array if needed - Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); - vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id ); - // clean the resulting array - if ( vNodes && !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return - return (Ivy_Obj_t *)vNodes; - return NULL; + Ivy_ObjForEachFanoutInt( pObj, pFanout ) + Vec_PtrPush( vArray, pFanout ); } /**Function************************************************************* @@ -269,18 +279,7 @@ Ivy_Obj_t * Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ) ***********************************************************************/ Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { - Vec_Ptr_t * vNodes; - assert( p->vFanouts != NULL ); - assert( !Ivy_IsComplement(pObj) ); - // extend the fanout array if needed - Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); - vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id ); - // clean the resulting array - if ( vNodes == NULL ) - return NULL; - if ( !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return - return (Ivy_Obj_t *)vNodes; - return Vec_PtrEntry( Ivy_FanoutGetArray(vNodes), 0 ); + return pObj->pFanout; } /**Function************************************************************* @@ -296,21 +295,13 @@ Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ) ***********************************************************************/ int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { - Vec_Ptr_t * vNodes; - assert( p->vFanouts != NULL ); - assert( !Ivy_IsComplement(pObj) ); - // extend the fanout array if needed - Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); - vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id ); - // clean the resulting array - if ( vNodes == NULL ) - return 0; - if ( !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return - return 1; - return Vec_PtrSize( Ivy_FanoutGetArray(vNodes) ); + Ivy_Obj_t * pFanout; + int Counter = 0; + Ivy_ObjForEachFanoutInt( pObj, pFanout ) + Counter++; + return Counter; } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyIsop.c b/src/temp/ivy/ivyIsop.c index 2d0101a7..1a4fce25 100644 --- a/src/temp/ivy/ivyIsop.c +++ b/src/temp/ivy/ivyIsop.c @@ -25,6 +25,10 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +// ISOP computation fails if intermediate memory usage exceed this limit +#define IVY_ISOP_MEM_LIMIT 4096 + +// intermediate ISOP representation typedef struct Ivy_Sop_t_ Ivy_Sop_t; struct Ivy_Sop_t_ { @@ -32,10 +36,9 @@ struct Ivy_Sop_t_ int nCubes; }; -static Mem_Flex_t * s_Man = NULL; - -static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes ); -static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes ); +// static procedures to compute ISOP +static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore ); +static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -43,111 +46,60 @@ static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, I /**Function************************************************************* - Synopsis [Deallocates memory used for computing ISOPs from TTs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_TruthManStop() -{ - Mem_FlexStop( s_Man, 0 ); - s_Man = NULL; -} - -/**Function************************************************************* - Synopsis [Computes ISOP from TT.] - Description [] + Description [Returns the cover in vCover. Uses the rest of array in vCover + as an intermediate memory storage. Returns the cover with -1 cubes, if the + the computation exceeded the memory limit (IVY_ISOP_MEM_LIMIT words of + intermediate data).] SideEffects [] SeeAlso [] ***********************************************************************/ -int Ivy_TruthIsopOne( unsigned * puTruth, int nVars, Vec_Int_t * vCover ) +int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth ) { Ivy_Sop_t cRes, * pcRes = &cRes; + Ivy_Sop_t cRes2, * pcRes2 = &cRes2; unsigned * pResult; - int i; + int RetValue = 0; assert( nVars >= 0 && nVars < 16 ); // if nVars < 5, make sure it does not depend on those vars - for ( i = nVars; i < 5; i++ ) - assert( !Extra_TruthVarInSupport(puTruth, 5, i) ); +// for ( i = nVars; i < 5; i++ ) +// assert( !Extra_TruthVarInSupport(puTruth, 5, i) ); // prepare memory manager - if ( s_Man == NULL ) - s_Man = Mem_FlexStart(); - else - Mem_FlexRestart( s_Man ); - // compute ISOP - pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes ); -// Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" ); -// Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" ); - assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); -//printf( "%d ", Mem_FlexReadMemUsage(s_Man) ); -//printf( "%d ", pcRes->nCubes ); - // copy the truth table Vec_IntClear( vCover ); - for ( i = 0; i < pcRes->nCubes; i++ ) - Vec_IntPush( vCover, pcRes->pCubes[i] ); - return 0; -} - -/**Function************************************************************* - - Synopsis [Computes ISOP from TT.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover ) -{ - Ivy_Sop_t cRes, * pcRes = &cRes; - unsigned * pResult; - int i; - assert( nVars >= 0 && nVars < 16 ); - // if nVars < 5, make sure it does not depend on those vars - for ( i = nVars; i < 5; i++ ) - assert( !Extra_TruthVarInSupport(puTruth, 5, i) ); - // prepare memory manager - if ( s_Man == NULL ) - s_Man = Mem_FlexStart(); - else - Mem_FlexRestart( s_Man ); - // compute ISOP - pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes ); -// Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" ); -// Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" ); - assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); -//printf( "%d ", Mem_FlexReadMemUsage(s_Man) ); -//printf( "%d ", pcRes->nCubes ); - // copy the truth table - Vec_IntClear( vCover ); - for ( i = 0; i < pcRes->nCubes; i++ ) - Vec_IntPush( vCover, pcRes->pCubes[i] ); - - // try other polarity - Mem_FlexRestart( s_Man ); - Extra_TruthNot( puTruth, puTruth, nVars ); - pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes ); - assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); - Extra_TruthNot( puTruth, puTruth, nVars ); - if ( Vec_IntSize(vCover) < pcRes->nCubes ) + Vec_IntGrow( vCover, IVY_ISOP_MEM_LIMIT ); + // compute ISOP for the direct polarity + pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vCover ); + if ( pcRes->nCubes == -1 ) + { + vCover->nSize = -1; return 0; - - // copy the truth table - Vec_IntClear( vCover ); - for ( i = 0; i < pcRes->nCubes; i++ ) - Vec_IntPush( vCover, pcRes->pCubes[i] ); - return 1; + } + assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); + if ( fTryBoth ) + { + // compute ISOP for the complemented polarity + Extra_TruthNot( puTruth, puTruth, nVars ); + pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vCover ); + if ( pcRes2->nCubes >= 0 ) + { + assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); + if ( pcRes->nCubes > pcRes2->nCubes ) + { + RetValue = 1; + pcRes = pcRes2; + } + } + Extra_TruthNot( puTruth, puTruth, nVars ); + } +// printf( "%d ", vCover->nSize ); + // move the cover representation to the beginning of the memory buffer + memmove( vCover->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) ); + Vec_IntShrink( vCover, pcRes->nCubes ); + return RetValue; } /**Function************************************************************* @@ -161,17 +113,22 @@ int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover ) SeeAlso [] ***********************************************************************/ -unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes ) +unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore ) { Ivy_Sop_t cRes0, cRes1, cRes2; Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2; unsigned * puRes0, * puRes1, * puRes2; unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1; int i, k, Var, nWords, nWordsAll; - assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) ); +// assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) ); // allocate room for the resulting truth table nWordsAll = Extra_TruthWordNum( nVars ); - pTemp = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWordsAll ); + pTemp = Vec_IntFetch( vStore, nWordsAll ); + if ( pTemp == NULL ) + { + pcRes->nCubes = -1; + return NULL; + } // check for constants if ( Extra_TruthIsConst0( puOn, nVars ) ) { @@ -183,7 +140,12 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy if ( Extra_TruthIsConst1( puOnDc, nVars ) ) { pcRes->nCubes = 1; - pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 ); + pcRes->pCubes = Vec_IntFetch( vStore, 1 ); + if ( pcRes->pCubes == NULL ) + { + pcRes->nCubes = -1; + return NULL; + } pcRes->pCubes[0] = 0; Extra_TruthFill( pTemp, nVars ); return pTemp; @@ -198,7 +160,7 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy // consider a simple case when one-word computation can be used if ( Var < 5 ) { - unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes ); + unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore ); for ( i = 0; i < nWordsAll; i++ ) pTemp[i] = uRes; return pTemp; @@ -211,17 +173,37 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy pTemp0 = pTemp; pTemp1 = pTemp + nWords; // solve for cofactors Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var ); - puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0 ); + puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore ); + if ( pcRes0->nCubes == -1 ) + { + pcRes->nCubes = -1; + return NULL; + } Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var ); - puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1 ); + puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore ); + if ( pcRes1->nCubes == -1 ) + { + pcRes->nCubes = -1; + return NULL; + } Extra_TruthSharp( pTemp0, puOn0, puRes0, Var ); Extra_TruthSharp( pTemp1, puOn1, puRes1, Var ); Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var ); Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var ); - puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2 ); + puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore ); + if ( pcRes2->nCubes == -1 ) + { + pcRes->nCubes = -1; + return NULL; + } // create the resulting cover pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes; - pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes ); + pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes ); + if ( pcRes->pCubes == NULL ) + { + pcRes->nCubes = -1; + return NULL; + } k = 0; for ( i = 0; i < pcRes0->nCubes; i++ ) pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1)); @@ -255,7 +237,7 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy SeeAlso [] ***********************************************************************/ -unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes ) +unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore ) { unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; Ivy_Sop_t cRes0, cRes1, cRes2; @@ -273,7 +255,12 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t if ( uOnDc == 0xFFFFFFFF ) { pcRes->nCubes = 1; - pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 ); + pcRes->pCubes = Vec_IntFetch( vStore, 1 ); + if ( pcRes->pCubes == NULL ) + { + pcRes->nCubes = -1; + return 0; + } pcRes->pCubes[0] = 0; return 0xFFFFFFFF; } @@ -292,12 +279,32 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t Extra_TruthCofactor0( &uOnDc0, Var + 1, Var ); Extra_TruthCofactor1( &uOnDc1, Var + 1, Var ); // solve for cofactors - uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0 ); - uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1 ); - uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2 ); + uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore ); + if ( pcRes0->nCubes == -1 ) + { + pcRes->nCubes = -1; + return 0; + } + uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore ); + if ( pcRes1->nCubes == -1 ) + { + pcRes->nCubes = -1; + return 0; + } + uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore ); + if ( pcRes2->nCubes == -1 ) + { + pcRes->nCubes = -1; + return 0; + } // create the resulting cover pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes; - pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes ); + pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes ); + if ( pcRes->pCubes == NULL ) + { + pcRes->nCubes = -1; + return 0; + } k = 0; for ( i = 0; i < pcRes0->nCubes; i++ ) pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1)); diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c index c5b66ad0..9839567f 100644 --- a/src/temp/ivy/ivyMan.c +++ b/src/temp/ivy/ivyMan.c @@ -82,7 +82,7 @@ Ivy_Man_t * Ivy_ManStart() void Ivy_ManStop( Ivy_Man_t * p ) { // Ivy_TableProfile( p ); - if ( p->vFanouts ) Ivy_ManStopFanout( p ); +// if ( p->vFanouts ) Ivy_ManStopFanout( p ); if ( p->vChunks ) Ivy_ManStopMemory( p ); if ( p->vRequired ) Vec_IntFree( p->vRequired ); if ( p->vPis ) Vec_PtrFree( p->vPis ); @@ -156,14 +156,14 @@ int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel ) void Ivy_ManPrintStats( Ivy_Man_t * p ) { printf( "PI/PO = %d/%d ", Ivy_ManPiNum(p), Ivy_ManPoNum(p) ); - printf( "A = %d. ", Ivy_ManAndNum(p) ); - printf( "L = %d. ", Ivy_ManLatchNum(p) ); + printf( "A = %7d. ", Ivy_ManAndNum(p) ); + printf( "L = %5d. ", Ivy_ManLatchNum(p) ); // printf( "X = %d. ", Ivy_ManExorNum(p) ); - printf( "B = %d. ", Ivy_ManBufNum(p) ); - printf( "MaxID = %d. ", Ivy_ManObjIdMax(p) ); +// printf( "B = %3d. ", Ivy_ManBufNum(p) ); + printf( "MaxID = %7d. ", Ivy_ManObjIdMax(p) ); // printf( "Cre = %d. ", p->nCreated ); // printf( "Del = %d. ", p->nDeleted ); - printf( "Lev = %d. ", Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) ); + printf( "Lev = %3d. ", Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) ); printf( "\n" ); } @@ -190,7 +190,7 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits ) assert( Ivy_ManPoNum(p) == Vec_PtrSize(p->vPos) ); assert( Vec_PtrSize( p->vBufs ) == 0 ); // create fanouts - if ( p->vFanouts == NULL ) + if ( p->fFanout == 0 ) Ivy_ManStartFanout( p ); // collect the POs to be converted into latches for ( i = 0; i < nLatches; i++ ) diff --git a/src/temp/ivy/ivyMem.c b/src/temp/ivy/ivyMem.c index 01833f03..6ca33541 100644 --- a/src/temp/ivy/ivyMem.c +++ b/src/temp/ivy/ivyMem.c @@ -87,15 +87,15 @@ void Ivy_ManAddMemory( Ivy_Man_t * p ) { char * pMemory; int i, nBytes; - assert( sizeof(Ivy_Obj_t) <= 32 ); + assert( sizeof(Ivy_Obj_t) <= 64 ); assert( p->pListFree == NULL ); assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 ); // allocate new memory page - nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 32; + nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 64; pMemory = ALLOC( char, nBytes ); Vec_PtrPush( p->vChunks, pMemory ); // align memory at the 32-byte boundary - pMemory = pMemory + 32 - (((int)pMemory) & 31); + pMemory = pMemory + 64 - (((int)pMemory) & 63); // remember the manager in the first entry Vec_PtrPush( p->vPages, pMemory ); // break the memory down into nodes diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c index 735d79c3..3122c8c8 100644 --- a/src/temp/ivy/ivyObj.c +++ b/src/temp/ivy/ivyObj.c @@ -79,6 +79,7 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost ) assert( Ivy_TableLookup(p, pGhost) == NULL ); // get memory for the new object pObj = Ivy_ManFetchMemory( p ); +//printf( "Reusing %p.\n", pObj ); assert( Ivy_ObjIsNone(pObj) ); pObj->Id = Vec_PtrSize(p->vObjs); Vec_PtrPush( p->vObjs, pObj ); @@ -139,13 +140,13 @@ void Ivy_ObjConnect( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFan0, Ivy_Obj if ( Ivy_ObjFanin0(pObj) != NULL ) { Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) ); - if ( p->vFanouts ) + if ( p->fFanout ) Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj ); } if ( Ivy_ObjFanin1(pObj) != NULL ) { Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) ); - if ( p->vFanouts ) + if ( p->fFanout ) Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj ); } // add the node to the structural hash table @@ -168,23 +169,29 @@ void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj ) assert( !Ivy_IsComplement(pObj) ); assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || Ivy_ObjFanin1(pObj) != NULL ); // remove connections - if ( Ivy_ObjFanin0(pObj) != NULL ) + if ( pObj->pFanin0 != NULL ) { Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj)); - if ( p->vFanouts ) + if ( p->fFanout ) Ivy_ObjDeleteFanout( p, Ivy_ObjFanin0(pObj), pObj ); } - if ( Ivy_ObjFanin1(pObj) != NULL ) + if ( pObj->pFanin1 != NULL ) { Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj)); - if ( p->vFanouts ) + if ( p->fFanout ) Ivy_ObjDeleteFanout( p, Ivy_ObjFanin1(pObj), pObj ); } + assert( pObj->pNextFan0 == NULL ); + assert( pObj->pNextFan1 == NULL ); + assert( pObj->pPrevFan0 == NULL ); + assert( pObj->pPrevFan1 == NULL ); // remove the node from the structural hash table Ivy_TableDelete( p, pObj ); // add the first fanin pObj->pFanin0 = NULL; pObj->pFanin1 = NULL; + +// Ivy_ManCheckFanouts( p ); } /**Function************************************************************* @@ -205,14 +212,14 @@ void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew pFaninOld = Ivy_ObjFanin0(pObj); // decrement ref and remove fanout Ivy_ObjRefsDec( pFaninOld ); - if ( p->vFanouts ) + if ( p->fFanout ) Ivy_ObjDeleteFanout( p, pFaninOld, pObj ); + // update the fanin + pObj->pFanin0 = pFaninNew; // increment ref and add fanout Ivy_ObjRefsInc( Ivy_Regular(pFaninNew) ); - if ( p->vFanouts ) + if ( p->fFanout ) Ivy_ObjAddFanout( p, Ivy_Regular(pFaninNew), pObj ); - // update the fanin - pObj->pFanin0 = pFaninNew; // get rid of old fanin if ( !Ivy_ObjIsPi(pFaninOld) && Ivy_ObjRefs(pFaninOld) == 0 ) Ivy_ObjDelete_rec( p, pFaninOld, 1 ); @@ -243,7 +250,7 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ) Vec_PtrRemove( p->vPis, pObj ); else if ( Ivy_ObjIsPo(pObj) ) Vec_PtrRemove( p->vPos, pObj ); - else if ( p->vFanouts && Ivy_ObjIsBuf(pObj) ) + else if ( p->fFanout && Ivy_ObjIsBuf(pObj) ) Vec_PtrRemove( p->vBufs, pObj ); // clean and recycle the entry if ( fFreeTop ) @@ -251,11 +258,14 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ) // free the node Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); Ivy_ManRecycleMemory( p, pObj ); +//printf( "Recycling after delete %p.\n", pObj ); } else { int nRefsOld = pObj->nRefs; + Ivy_Obj_t * pFanout = pObj->pFanout; Ivy_ObjClean( pObj ); + pObj->pFanout = pFanout; pObj->nRefs = nRefsOld; } } @@ -318,7 +328,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in if ( fUpdateLevel ) { // if the new node's arrival time is different, recursively update arrival time of the fanouts - if ( p->vFanouts && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level ) + if ( p->fFanout && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level ) { assert( Ivy_ObjIsNode(pObjOld) ); pObjOld->Level = pObjNew->Level; @@ -338,16 +348,23 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in // delete the old object if ( fDeleteOld ) Ivy_ObjDelete_rec( p, pObjOld, fFreeTop ); - // make sure object is pointing to itself + // make sure object is not pointing to itself assert( Ivy_ObjFanin0(pObjNew) == NULL || pObjOld != Ivy_ObjFanin0(pObjNew) ); assert( Ivy_ObjFanin1(pObjNew) == NULL || pObjOld != Ivy_ObjFanin1(pObjNew) ); + // make sure the old node has no fanin fanout pointers + if ( p->fFanout ) + { + assert( pObjOld->pFanout != NULL ); + assert( pObjNew->pFanout == NULL ); + pObjNew->pFanout = pObjOld->pFanout; + } // transfer the old object assert( Ivy_ObjRefs(pObjNew) == 0 ); nRefsOld = pObjOld->nRefs; Ivy_ObjOverwrite( pObjOld, pObjNew ); pObjOld->nRefs = nRefsOld; // patch the fanout of the fanins - if ( p->vFanouts ) + if ( p->fFanout ) { Ivy_ObjPatchFanout( p, Ivy_ObjFanin0(pObjOld), pObjNew, pObjOld ); if ( Ivy_ObjFanin1(pObjOld) ) @@ -358,9 +375,12 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in // recycle the object that was taken over by pObjOld Vec_PtrWriteEntry( p->vObjs, pObjNew->Id, NULL ); Ivy_ManRecycleMemory( p, pObjNew ); +//printf( "Recycling after patch %p.\n", pObjNew ); // if the new node is the buffer propagate it - if ( p->vFanouts && Ivy_ObjIsBuf(pObjOld) ) + if ( p->fFanout && Ivy_ObjIsBuf(pObjOld) ) Vec_PtrPush( p->vBufs, pObjOld ); +// Ivy_ManCheckFanouts( p ); +// printf( "\n" ); } /**Function************************************************************* @@ -385,6 +405,7 @@ void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel return; pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) ); Ivy_ObjPatchFanin0( p, pNode, pFanReal0 ); +// Ivy_ManCheckFanouts( p ); return; } if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) && !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) ) diff --git a/src/temp/ivy/ivyResyn.c b/src/temp/ivy/ivyResyn.c index 804bdfb4..b2e4a4dd 100644 --- a/src/temp/ivy/ivyResyn.c +++ b/src/temp/ivy/ivyResyn.c @@ -39,6 +39,47 @@ SeeAlso [] ***********************************************************************/ +Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose ) +{ + int clk; + Ivy_Man_t * pTemp; + +if ( fVerbose ) { printf( "Original:\n" ); } +if ( fVerbose ) Ivy_ManPrintStats( pMan ); + +clk = clock(); + pMan = Ivy_ManBalance( pMan, fUpdateLevel ); +if ( fVerbose ) { printf( "\n" ); } +if ( fVerbose ) { PRT( "Balance", clock() - clk ); } +if ( fVerbose ) Ivy_ManPrintStats( pMan ); + +// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 ); +clk = clock(); + Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 ); +if ( fVerbose ) { printf( "\n" ); } +if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); } +if ( fVerbose ) Ivy_ManPrintStats( pMan ); + +clk = clock(); + pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel ); + Ivy_ManStop( pTemp ); +if ( fVerbose ) { printf( "\n" ); } +if ( fVerbose ) { PRT( "Balance", clock() - clk ); } +if ( fVerbose ) Ivy_ManPrintStats( pMan ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [Performs several passes of rewriting on the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose ) { int clk; diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c index 537b64ff..64331579 100644 --- a/src/temp/ivy/ivyRwrPre.c +++ b/src/temp/ivy/ivyRwrPre.c @@ -61,7 +61,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV if ( pManRwt == NULL ) return 0; // create fanouts - if ( fUpdateLevel && p->vFanouts == NULL ) + if ( fUpdateLevel && p->fFanout == 0 ) Ivy_ManStartFanout( p ); // compute the reverse levels if level update is requested if ( fUpdateLevel ) diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c index 8fd1b63b..7cf55b69 100644 --- a/src/temp/ivy/ivySeq.c +++ b/src/temp/ivy/ivySeq.c @@ -64,7 +64,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose ) if ( pManRwt == NULL ) return 0; // create fanouts - if ( p->vFanouts == NULL ) + if ( p->fFanout == 0 ) Ivy_ManStartFanout( p ); // resynthesize each node once nNodes = Ivy_ManObjIdMax(p); diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c index 77a55a39..a23e76c9 100644 --- a/src/temp/ivy/ivyUtil.c +++ b/src/temp/ivy/ivyUtil.c @@ -381,7 +381,7 @@ void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj ) Ivy_Obj_t * pFanout; Vec_Ptr_t * vFanouts; int i, LevelNew; - assert( p->vFanouts ); + assert( p->fFanout ); assert( Ivy_ObjIsNode(pObj) ); vFanouts = Vec_PtrAlloc( 10 ); Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i ) @@ -416,7 +416,7 @@ int Ivy_ObjLevelRNew( Ivy_Man_t * p, Ivy_Obj_t * pObj ) Ivy_Obj_t * pFanout; Vec_Ptr_t * vFanouts; int i, Required, LevelNew = 1000000; - assert( p->vFanouts && p->vRequired ); + assert( p->fFanout && p->vRequired ); vFanouts = Vec_PtrAlloc( 10 ); Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i ) { diff --git a/src/temp/player/player.h b/src/temp/player/player.h index b0bb0ec4..0213683f 100644 --- a/src/temp/player/player.h +++ b/src/temp/player/player.h @@ -86,13 +86,14 @@ static inline Pla_Obj_t * Ivy_ObjPlaStr( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { //////////////////////////////////////////////////////////////////////// /*=== playerToAbc.c ==============================================================*/ -extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose ); +extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose ); /*=== playerCore.c =============================================================*/ extern Pla_Man_t * Pla_ManDecompose( Ivy_Man_t * p, int nLutMax, int nPlaMax, int fVerbose ); /*=== playerFast.c =============================================================*/ extern void Pla_ManFastLutMap( Ivy_Man_t * pAig, int nLimit ); extern void Pla_ManFastLutMapStop( Ivy_Man_t * pAig ); extern void Pla_ManFastLutMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves ); +extern void Pla_ManFastLutMapReverseLevel( Ivy_Man_t * pAig ); /*=== playerMan.c ==============================================================*/ extern Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * p, int nLutMax, int nPlaMax ); extern void Pla_ManFree( Pla_Man_t * p ); diff --git a/src/temp/player/playerMan.c b/src/temp/player/playerMan.c index 1196d242..78b20718 100644 --- a/src/temp/player/playerMan.c +++ b/src/temp/player/playerMan.c @@ -40,7 +40,7 @@ ***********************************************************************/ Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * pAig, int nLutMax, int nPlaMax ) -{ +{ Pla_Man_t * pMan; assert( !(nLutMax < 2 || nLutMax > 8 || nPlaMax < 8 || nPlaMax > 128) ); // start the manager diff --git a/src/temp/player/playerToAbc.c b/src/temp/player/playerToAbc.c index fc5e01ea..91994ca6 100644 --- a/src/temp/player/playerToAbc.c +++ b/src/temp/player/playerToAbc.c @@ -50,9 +50,8 @@ static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId ) SeeAlso [] ***********************************************************************/ -void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose ) +void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose ) { - int fUseRewriting = 0; Pla_Man_t * p; Ivy_Man_t * pMan, * pManExt; Abc_Ntk_t * pNtkNew; @@ -69,7 +68,15 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int f } if ( fVerbose ) Ivy_ManPrintStats( pMan ); - if ( fUseRewriting ) + if ( fRewriting ) + { + // simplify + pMan = Ivy_ManResyn0( pManExt = pMan, 1, 0 ); + Ivy_ManStop( pManExt ); + if ( fVerbose ) + Ivy_ManPrintStats( pMan ); + } + if ( fSynthesis ) { // simplify pMan = Ivy_ManResyn( pManExt = pMan, 1, 0 ); @@ -261,9 +268,16 @@ Abc_Obj_t * Ivy_ManToAbc_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Pla_Man_t * pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL ); pObjAbc = Abc_NodeCreateConst0( pNtkNew ); } + else if ( Extra_TruthIsConst1(puTruth, 8) ) + { + pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL ); + pObjAbc = Abc_NodeCreateConst1( pNtkNew ); + } else { - int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes ); + int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes, 1 ); + if ( vNodes->nSize == -1 ) + printf( "Ivy_ManToAbc_rec(): Internal error.\n" ); pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes ); if ( fCompl ) Abc_SopComplement(pObjAbc->pData); // printf( "Cover contains %d cubes.\n", Vec_IntSize(vNodes) ); @@ -372,9 +386,16 @@ Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL ); pObjAbc = Abc_NodeCreateConst0( pNtkNew ); } + else if ( Extra_TruthIsConst1(puTruth, 8) ) + { + pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL ); + pObjAbc = Abc_NodeCreateConst1( pNtkNew ); + } else { - int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes ); + int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes, 1 ); + if ( vNodes->nSize == -1 ) + printf( "Ivy_ManToAbcFast_rec(): Internal error.\n" ); pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes ); if ( fCompl ) Abc_SopComplement(pObjAbc->pData); } @@ -444,32 +465,48 @@ static inline int Abc_NtkPlayerCostOne( int nCost, int RankCost ) int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose ) { Abc_Obj_t * pObj; - int nFanins, nLevels, * pLevelCosts, CostTotal, nRanksTotal, i; + int * pLevelCosts, * pLevelCostsR; + int nFanins, nLevels, LevelR, Cost, CostTotal, CostTotalR, nRanksTotal, nRanksTotalR, i; + // compute the reverse levels + Abc_NtkStartReverseLevels( pNtk ); // compute the costs for each level nLevels = Abc_NtkGetLevelNum( pNtk ); - pLevelCosts = ALLOC( int, nLevels + 1 ); - memset( pLevelCosts, 0, sizeof(int) * (nLevels + 1) ); + pLevelCosts = ALLOC( int, nLevels + 1 ); + pLevelCostsR = ALLOC( int, nLevels + 1 ); + memset( pLevelCosts, 0, sizeof(int) * (nLevels + 1) ); + memset( pLevelCostsR, 0, sizeof(int) * (nLevels + 1) ); Abc_NtkForEachNode( pNtk, pObj, i ) { nFanins = Abc_ObjFaninNum(pObj); if ( nFanins == 0 ) continue; - pLevelCosts[ pObj->Level ] += Abc_NodePlayerCost( nFanins ); + Cost = Abc_NodePlayerCost( nFanins ); + LevelR = Vec_IntEntry( pNtk->vLevelsR, pObj->Id ); + pLevelCosts[ pObj->Level ] += Cost; + pLevelCostsR[ LevelR ] += Cost; } // compute the total cost - CostTotal = nRanksTotal = 0; - for ( i = 1; i <= nLevels; i++ ) + CostTotal = CostTotalR = nRanksTotal = nRanksTotalR = 0; + for ( i = 0; i <= nLevels; i++ ) { - CostTotal += pLevelCosts[i]; - nRanksTotal += Abc_NtkPlayerCostOne( pLevelCosts[i], RankCost ); + CostTotal += pLevelCosts[i]; + CostTotalR += pLevelCostsR[i]; + nRanksTotal += Abc_NtkPlayerCostOne( pLevelCosts[i], RankCost ); + nRanksTotalR += Abc_NtkPlayerCostOne( pLevelCostsR[i], RankCost ); } + assert( CostTotal == CostTotalR ); // print out statistics if ( fVerbose ) { for ( i = 1; i <= nLevels; i++ ) - printf( "Level %2d : Cost = %6d. Ranks = %6.3f.\n", i, pLevelCosts[i], ((double)pLevelCosts[i])/RankCost ); - printf( "TOTAL : Cost = %6d. Ranks = %3d.\n", CostTotal, nRanksTotal ); + printf( "Level %2d : Cost = %7d. Ranks = %6.3f. Cost = %7d. Ranks = %6.3f.\n", i, + pLevelCosts[i], ((double)pLevelCosts[i])/RankCost, + pLevelCostsR[nLevels+1-i], ((double)pLevelCostsR[nLevels+1-i])/RankCost ); + printf( "TOTAL : Cost = %7d. Ranks = %6d. RanksR = %5d. RanksBest = %5d.\n", + CostTotal, nRanksTotal, nRanksTotalR, nLevels ); } + free( pLevelCosts ); + free( pLevelCostsR ); return nRanksTotal; } diff --git a/src/temp/vec/vecInt.h b/src/temp/vec/vecInt.h index 9db30af7..4a97fc91 100644 --- a/src/temp/vec/vecInt.h +++ b/src/temp/vec/vecInt.h @@ -289,23 +289,6 @@ static inline int Vec_IntEntry( Vec_Int_t * p, int i ) SeeAlso [] ***********************************************************************/ -static inline int * Vec_IntEntryP( Vec_Int_t * p, int i ) -{ - assert( i >= 0 && i < p->nSize ); - return p->pArray + i; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ static inline void Vec_IntWriteEntry( Vec_Int_t * p, int i, int Entry ) { assert( i >= 0 && i < p->nSize ); @@ -402,10 +385,7 @@ static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry ) int i; if ( p->nSize >= nSize ) return; - if ( p->nSize < 2 * nSize ) - Vec_IntGrow( p, 2 * nSize ); - else - Vec_IntGrow( p, p->nSize ); + Vec_IntGrow( p, nSize ); for ( i = p->nSize; i < nSize; i++ ) p->pArray[i] = Entry; p->nSize = nSize; @@ -603,6 +583,28 @@ static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry ) /**Function************************************************************* + Synopsis [Returns the pointer to the next nWords entries in the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned * Vec_IntFetch( Vec_Int_t * p, int nWords ) +{ + p->nSize += nWords; + if ( p->nSize > p->nCap ) + { +// Vec_IntGrow( p, 2 * p->nSize ); + return NULL; + } + return ((unsigned *)p->pArray) + p->nSize - nWords; +} + +/**Function************************************************************* + Synopsis [Returns the last entry and removes it from the list.] Description [] diff --git a/src/temp/vec/vecPtr.h b/src/temp/vec/vecPtr.h index 96975ff0..07ac0f17 100644 --- a/src/temp/vec/vecPtr.h +++ b/src/temp/vec/vecPtr.h @@ -293,6 +293,23 @@ static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i ) SeeAlso [] ***********************************************************************/ +static inline void ** Vec_PtrEntryP( Vec_Ptr_t * p, int i ) +{ + assert( i >= 0 && i < p->nSize ); + return p->pArray + i; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ static inline void Vec_PtrWriteEntry( Vec_Ptr_t * p, int i, void * Entry ) { assert( i >= 0 && i < p->nSize ); @@ -371,7 +388,10 @@ static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry ) int i; if ( p->nSize >= nSize ) return; - Vec_PtrGrow( p, nSize ); + if ( p->nSize < 2 * nSize ) + Vec_PtrGrow( p, 2 * nSize ); + else + Vec_PtrGrow( p, p->nSize ); for ( i = p->nSize; i < nSize; i++ ) p->pArray[i] = Entry; p->nSize = nSize; @@ -505,10 +525,18 @@ static inline int Vec_PtrFind( Vec_Ptr_t * p, void * Entry ) static inline void Vec_PtrRemove( Vec_Ptr_t * p, void * Entry ) { int i; + // delete assuming that it is closer to the end + for ( i = p->nSize - 1; i >= 0; i-- ) + if ( p->pArray[i] == Entry ) + break; + assert( i >= 0 ); +/* + // delete assuming that it is closer to the beginning for ( i = 0; i < p->nSize; i++ ) if ( p->pArray[i] == Entry ) break; assert( i < p->nSize ); +*/ for ( i++; i < p->nSize; i++ ) p->pArray[i-1] = p->pArray[i]; p->nSize--; |