Commit 6b44b18e by Alan Mishchenko

Version abc60804

parent 103fa22e
......@@ -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;
......
......@@ -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 );
......
......@@ -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);
......
......@@ -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 );
......
......@@ -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 );
......
......@@ -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
......
......@@ -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
};
......
......@@ -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.]
......
......@@ -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 []
......
......@@ -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();
......
......@@ -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 );
}
......
......@@ -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.
......
......@@ -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++ )
......
......@@ -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 );
......
......@@ -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;
}
////////////////////////////////////////////////////////////////////////
......
......@@ -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;
......
......@@ -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)) )
......
......@@ -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++ )
......
......@@ -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
......
......@@ -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)) )
......
......@@ -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;
......
......@@ -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 )
......
......@@ -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);
......
......@@ -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 )
{
......
......@@ -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 );
......
......@@ -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
......
......@@ -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;
}
......
......@@ -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 []
......
......@@ -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--;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment