Commit 1647addf by Alan Mishchenko

Version abc70714

parent c5277d33
......@@ -2534,6 +2534,18 @@ SOURCE=.\src\aig\dar\darMan.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darRefact.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darResub.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darScript.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darTruth.c
# End Source File
# End Group
......@@ -2722,6 +2734,10 @@ SOURCE=.\src\aig\aig\aigDfs.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigFanout.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigMan.c
# End Source File
# Begin Source File
......@@ -2746,6 +2762,10 @@ SOURCE=.\src\aig\aig\aigTable.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigTiming.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigUtil.c
# End Source File
# End Group
......
......@@ -89,6 +89,7 @@ struct Aig_Man_t_
Vec_Ptr_t * vPis; // the array of PIs
Vec_Ptr_t * vPos; // the array of POs
Vec_Ptr_t * vObjs; // the array of all nodes (optional)
Vec_Ptr_t * vBufs; // the array of buffers
Aig_Obj_t * pConst1; // the constant 1 node
Aig_Obj_t Ghost; // the ghost node
// AIG node counters
......@@ -98,9 +99,16 @@ struct Aig_Man_t_
// structural hash table
Aig_Obj_t ** pTable; // structural hash table
int nTableSize; // structural hash table size
// representation of fanouts
int * pFanData; // the database to store fanout information
int nFansAlloc; // the size of fanout representation
Vec_Vec_t * vLevels; // used to update timing information
int nBufReplaces; // the number of times replacement led to a buffer
int nBufFixes; // the number of times buffers were propagated
int nBufMax; // the maximum number of buffers during computation
// various data members
Aig_MmFixed_t * pMemObjs; // memory manager for objects
Vec_Int_t * vRequired; // the required times
Vec_Int_t * vLevelR; // the reverse level of the nodes
int nLevelMax; // maximum number of levels
void * pData; // the temporary data
int nTravIds; // the current traversal ID
......@@ -190,9 +198,10 @@ static inline Aig_Obj_t * Aig_ObjChild1( Aig_Obj_t * pObj ) { return pObj-
static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; }
static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj->nRefs; }
static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level); }
static inline int Aig_ObjFaninPhase( Aig_Obj_t * pObj ) { return Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj); }
static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
static inline int Aig_ObjFaninPhase( Aig_Obj_t * pObj ) { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 0; }
static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); }
static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); }
static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )
{
if ( Aig_ObjFanin0(pObj) == pFanin ) return 0;
......@@ -266,6 +275,15 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
#define Aig_ManForEachNode( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
// these two procedures are only here for the use inside the iterator
static inline int Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId ) { assert(ObjId < p->nFansAlloc); return p->pFanData[5*ObjId]; }
static inline int Aig_ObjFanoutNext( Aig_Man_t * p, int iFan ) { assert(iFan/2 < p->nFansAlloc); return p->pFanData[5*(iFan >> 1) + 3 + (iFan & 1)]; }
// iterator over the fanouts
#define Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i ) \
for ( assert(p->pFanData), i = 0; (i < (int)(pObj)->nRefs) && \
(((iFan) = i? Aig_ObjFanoutNext(p, iFan) : Aig_ObjFanout0Int(p, pObj->Id)), 1) && \
(((pFanout) = Aig_ManObj(p, iFan>>1)), 1); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -275,16 +293,21 @@ extern int Aig_ManCheck( Aig_Man_t * p );
/*=== aigDfs.c ==========================================================*/
extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p );
extern int Aig_ManCountLevels( Aig_Man_t * p );
extern void Aig_ManCreateRefs( Aig_Man_t * p );
extern int Aig_DagSize( Aig_Obj_t * pObj );
extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
/*=== aigFanout.c ==========================================================*/
extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
extern void Aig_ManCreateFanout( Aig_Man_t * p );
extern void Aig_ManDeleteFanout( Aig_Man_t * p );
/*=== aigMan.c ==========================================================*/
extern Aig_Man_t * Aig_ManStart();
extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered );
extern void Aig_ManStop( Aig_Man_t * p );
extern int Aig_ManCleanup( Aig_Man_t * p );
extern void Aig_ManPrintStats( Aig_Man_t * p );
......@@ -300,7 +323,7 @@ extern void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop );
extern void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew );
extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly );
extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel );
/*=== aigOper.c =========================================================*/
extern Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i );
extern Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type );
......@@ -322,6 +345,12 @@ extern void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
extern int Aig_TableCountEntries( Aig_Man_t * p );
extern void Aig_TableProfile( Aig_Man_t * p );
/*=== aigTiming.c ========================================================*/
extern int Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease );
extern void Aig_ManStopReverseLevels( Aig_Man_t * p );
extern void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
extern void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
/*=== aigUtil.c =========================================================*/
extern unsigned Aig_PrimeCudd( unsigned p );
extern void Aig_ManIncrementTravId( Aig_Man_t * p );
......
......@@ -119,6 +119,65 @@ Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
/**Function*************************************************************
Synopsis [Collects internal nodes in the reverse DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManDfsReverse_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
Aig_Obj_t * pFanout;
int iFanout, i;
assert( !Aig_IsComplement(pObj) );
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
Aig_ManDfsReverse_rec( p, pFanout, vNodes );
assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
Aig_ObjSetTravIdCurrent(p, pObj);
Vec_PtrPush( vNodes, pObj );
}
/**Function*************************************************************
Synopsis [Collects internal nodes in the reverse DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p )
{
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
Aig_ManIncrementTravId( p );
// mark POs
Aig_ManForEachPo( p, pObj, i )
Aig_ObjSetTravIdCurrent( p, pObj );
// if there are latches, mark them
if ( Aig_ManLatchNum(p) > 0 )
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjIsLatch(pObj) )
Aig_ObjSetTravIdCurrent( p, pObj );
// go through the nodes
vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) )
Aig_ManDfsReverse_rec( p, pObj, vNodes );
return vNodes;
}
/**Function*************************************************************
Synopsis [Computes the max number of levels in the manager.]
Description []
......
/**CFile****************************************************************
FileName [aigFanout.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis [Fanout manipulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: aigFanout.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
// 0: first iFan
// 1: prev iFan0
// 2: prev iFan1
// 3: next iFan0
// 4: next iFan1
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Aig_FanoutCreate( int FanId, int Num ) { assert( Num < 2 ); return (FanId << 1) | Num; }
static inline int * Aig_FanoutObj( int * pData, int ObjId ) { return pData + 5*ObjId; }
static inline int * Aig_FanoutPrev( int * pData, int iFan ) { return pData + 5*(iFan >> 1) + 1 + (iFan & 1); }
static inline int * Aig_FanoutNext( int * pData, int iFan ) { return pData + 5*(iFan >> 1) + 3 + (iFan & 1); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Adds fanout (pFanout) of node (pObj).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout )
{
int iFan, * pFirst, * pPrevC, * pNextC, * pPrev, * pNext;
assert( p->pFanData );
assert( !Aig_IsComplement(pObj) && !Aig_IsComplement(pFanout) );
assert( pFanout->Id > 0 );
if ( pObj->Id >= p->nFansAlloc || pFanout->Id >= p->nFansAlloc )
{
int nFansAlloc = 2 * AIG_MAX( pObj->Id, pFanout->Id );
p->pFanData = REALLOC( int, p->pFanData, 5 * nFansAlloc );
memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) );
p->nFansAlloc = nFansAlloc;
}
assert( pObj->Id < p->nFansAlloc && pFanout->Id < p->nFansAlloc );
iFan = Aig_FanoutCreate( pFanout->Id, Aig_ObjWhatFanin(pFanout, pObj) );
pPrevC = Aig_FanoutPrev( p->pFanData, iFan );
pNextC = Aig_FanoutNext( p->pFanData, iFan );
pFirst = Aig_FanoutObj( p->pFanData, pObj->Id );
if ( *pFirst == 0 )
{
*pFirst = iFan;
*pPrevC = iFan;
*pNextC = iFan;
}
else
{
pPrev = Aig_FanoutPrev( p->pFanData, *pFirst );
pNext = Aig_FanoutNext( p->pFanData, *pPrev );
assert( *pNext == *pFirst );
*pPrevC = *pPrev;
*pNextC = *pFirst;
*pPrev = iFan;
*pNext = iFan;
}
}
/**Function*************************************************************
Synopsis [Removes fanout (pFanout) of node (pObj).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout )
{
int iFan, * pFirst, * pPrevC, * pNextC, * pPrev, * pNext;
assert( p->pFanData && pObj->Id < p->nFansAlloc && pFanout->Id < p->nFansAlloc );
assert( !Aig_IsComplement(pObj) && !Aig_IsComplement(pFanout) );
assert( pFanout->Id > 0 );
iFan = Aig_FanoutCreate( pFanout->Id, Aig_ObjWhatFanin(pFanout, pObj) );
pPrevC = Aig_FanoutPrev( p->pFanData, iFan );
pNextC = Aig_FanoutNext( p->pFanData, iFan );
pPrev = Aig_FanoutPrev( p->pFanData, *pNextC );
pNext = Aig_FanoutNext( p->pFanData, *pPrevC );
assert( *pPrev == iFan );
assert( *pNext == iFan );
pFirst = Aig_FanoutObj( p->pFanData, pObj->Id );
assert( *pFirst > 0 );
if ( *pFirst == iFan )
{
if ( *pNextC == iFan )
{
*pFirst = 0;
*pPrev = 0;
*pNext = 0;
*pPrevC = 0;
*pNextC = 0;
return;
}
*pFirst = *pNextC;
}
*pPrev = *pPrevC;
*pNext = *pNextC;
*pPrevC = 0;
*pNextC = 0;
}
/**Function*************************************************************
Synopsis [Create fanout for all objects in the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManCreateFanout( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i;
// allocate fanout datastructure
assert( p->pFanData == NULL );
p->nFansAlloc = 2 * Aig_ManObjIdMax(p);
if ( p->nFansAlloc < (1<<12) )
p->nFansAlloc = (1<<12);
p->pFanData = ALLOC( int, 5 * p->nFansAlloc );
memset( p->pFanData, 0, sizeof(int) * 5 * p->nFansAlloc );
// add fanouts for all objects
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjChild0(pObj) )
Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj );
if ( Aig_ObjChild1(pObj) )
Aig_ObjAddFanout( p, Aig_ObjFanin1(pObj), pObj );
}
}
/**Function*************************************************************
Synopsis [Deletes fanout for all objects in the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManDeleteFanout( Aig_Man_t * p )
{
assert( p->pFanData != NULL );
FREE( p->pFanData );
p->nFansAlloc = 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......@@ -55,6 +55,7 @@ Aig_Man_t * Aig_ManStart( int nNodesMax )
p->vPis = Vec_PtrAlloc( 100 );
p->vPos = Vec_PtrAlloc( 100 );
p->vObjs = Vec_PtrAlloc( 1000 );
p->vBufs = Vec_PtrAlloc( 100 );
// prepare the internal memory manager
p->pMemObjs = Aig_MmFixedStart( sizeof(Aig_Obj_t), nNodesMax );
// create the constant node
......@@ -96,6 +97,28 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
{
if ( pObj->pData )
return pObj->pData;
Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
if ( Aig_ObjIsBuf(pObj) )
return pObj->pData = Aig_ObjChild0Copy(pObj);
Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description []
......@@ -105,7 +128,7 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
......@@ -113,15 +136,25 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
// create the new manager
pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
// duplicate internal nodes
if ( fOrdered )
{
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
pObj->pData = Aig_ObjChild0Copy(pObj);
else if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}
else
{
Aig_ManForEachObj( p, pObj, i )
if ( !Aig_ObjIsPo(pObj) )
Aig_ManDup_rec( pNew, p, pObj );
}
// add the POs
Aig_ManForEachPo( p, pObj, i )
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
......@@ -149,6 +182,9 @@ void Aig_ManStop( Aig_Man_t * p )
// print time
if ( p->time1 ) { PRT( "time1", p->time1 ); }
if ( p->time2 ) { PRT( "time2", p->time2 ); }
// delete fanout
if ( p->pFanData )
Aig_ManDeleteFanout( p );
// make sure the nodes have clean marks
Aig_ManForEachObj( p, pObj, i )
assert( !pObj->fMarkA && !pObj->fMarkB );
......@@ -157,7 +193,9 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vPis ) Vec_PtrFree( p->vPis );
if ( p->vPos ) Vec_PtrFree( p->vPos );
if ( p->vObjs ) Vec_PtrFree( p->vObjs );
if ( p->vRequired ) Vec_IntFree( p->vRequired );
if ( p->vBufs ) Vec_PtrFree( p->vBufs );
if ( p->vLevelR ) Vec_IntFree( p->vLevelR );
if ( p->vLevels ) Vec_VecFree( p->vLevels );
free( p->pTable );
free( p );
}
......@@ -205,14 +243,16 @@ int Aig_ManCleanup( Aig_Man_t * p )
void Aig_ManPrintStats( Aig_Man_t * p )
{
printf( "PI/PO/Lat = %5d/%5d/%5d ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) );
printf( "A = %6d. ", Aig_ManAndNum(p) );
printf( "A = %7d. ", Aig_ManAndNum(p) );
if ( Aig_ManExorNum(p) )
printf( "X = %5d. ", Aig_ManExorNum(p) );
// if ( Aig_ManBufNum(p) )
printf( "B = %3d. ", Aig_ManBufNum(p) );
printf( "Cre = %6d. ", p->nCreated );
printf( "Del = %6d. ", p->nDeleted );
printf( "B = %5d. ", Aig_ManBufNum(p) );
// printf( "Cre = %6d. ", p->nCreated );
// printf( "Del = %6d. ", p->nDeleted );
// printf( "Lev = %3d. ", Aig_ManCountLevels(p) );
printf( "Max = %7d. ", Aig_ManObjIdMax(p) );
printf( "Lev = %3d. ", Aig_ManLevels(p) );
printf( "\n" );
}
......
......@@ -232,7 +232,8 @@ void Aig_MmFixedRestart( Aig_MmFixed_t * p )
{
int i;
char * pTemp;
if ( p->nChunks == 0 )
return;
// deallocate all chunks except the first one
for ( i = 1; i < p->nChunks; i++ )
free( p->pChunks[i] );
......
......@@ -66,9 +66,7 @@ Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver )
pObj = Aig_ManFetchMemory( p );
pObj->Type = AIG_OBJ_PO;
Vec_PtrPush( p->vPos, pObj );
// add connections
Aig_ObjConnect( p, pObj, pDriver, NULL );
// update node counters of the manager
p->nObjs[AIG_OBJ_PO]++;
return pObj;
}
......@@ -125,23 +123,19 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj
{
assert( Aig_ObjFanin0(pObj)->Type > 0 );
Aig_ObjRef( Aig_ObjFanin0(pObj) );
if ( p->pFanData )
Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj );
}
if ( pFan1 != NULL )
{
assert( Aig_ObjFanin1(pObj)->Type > 0 );
Aig_ObjRef( Aig_ObjFanin1(pObj) );
if ( p->pFanData )
Aig_ObjAddFanout( p, Aig_ObjFanin1(pObj), pObj );
}
// set level and phase
if ( pFan1 != NULL )
{
pObj->Level = Aig_ObjLevelNew( pObj );
pObj->fPhase = Aig_ObjFaninPhase(pFan0) & Aig_ObjFaninPhase(pFan1);
}
else
{
pObj->Level = pFan0->Level;
pObj->fPhase = Aig_ObjFaninPhase(pFan0);
}
// add the node to the structural hash table
if ( Aig_ObjIsHash(pObj) )
Aig_TableInsert( p, pObj );
......@@ -163,9 +157,17 @@ void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj )
assert( !Aig_IsComplement(pObj) );
// remove connections
if ( pObj->pFanin0 != NULL )
{
if ( p->pFanData )
Aig_ObjRemoveFanout( p, Aig_ObjFanin0(pObj), pObj );
Aig_ObjDeref(Aig_ObjFanin0(pObj));
}
if ( pObj->pFanin1 != NULL )
{
if ( p->pFanData )
Aig_ObjRemoveFanout( p, Aig_ObjFanin1(pObj), pObj );
Aig_ObjDeref(Aig_ObjFanin1(pObj));
}
// remove the node from the structural hash table
if ( Aig_ObjIsHash(pObj) )
Aig_TableDelete( p, pObj );
......@@ -190,6 +192,8 @@ void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
assert( !Aig_IsComplement(pObj) );
assert( !Aig_ObjIsTerm(pObj) );
assert( Aig_ObjRefs(pObj) == 0 );
if ( p->pFanData && Aig_ObjIsBuf(pObj) )
Vec_PtrRemove( p->vBufs, pObj );
p->nObjs[pObj->Type]--;
Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
Aig_ManRecycleMemory( p, pObj );
......@@ -241,11 +245,15 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
assert( !Aig_IsComplement(pObj) );
pFaninOld = Aig_ObjFanin0(pObj);
// decrement ref and remove fanout
if ( p->pFanData )
Aig_ObjRemoveFanout( p, pFaninOld, pObj );
Aig_ObjDeref( pFaninOld );
// update the fanin
pObj->pFanin0 = pFaninNew;
// increment ref and add fanout
Aig_ObjRef( Aig_Regular(pFaninNew) );
if ( p->pFanData )
Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj );
Aig_ObjRef( Aig_ObjFanin0(pObj) );
// get rid of old fanin
if ( !Aig_ObjIsPi(pFaninOld) && !Aig_ObjIsConst1(pFaninOld) && Aig_ObjRefs(pFaninOld) == 0 )
Aig_ObjDelete_rec( p, pFaninOld, 1 );
......@@ -253,18 +261,89 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
/**Function*************************************************************
Synopsis [Replaces node with a buffer fanin by a node without them.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, int fUpdateLevel )
{
Aig_Obj_t * pFanReal0, * pFanReal1, * pResult;
p->nBufFixes++;
if ( Aig_ObjIsPo(pObj) )
{
assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) );
pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
Aig_ObjPatchFanin0( p, pObj, pFanReal0 );
return;
}
assert( Aig_ObjIsNode(pObj) );
assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) || Aig_ObjIsBuf(Aig_ObjFanin1(pObj)) );
// get the real fanins
pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
pFanReal1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
// get the new node
if ( Aig_ObjIsNode(pObj) )
pResult = Aig_Oper( p, pFanReal0, pFanReal1, Aig_ObjType(pObj) );
// else if ( Aig_ObjIsLatch(pObj) )
// pResult = Aig_Latch( p, pFanReal0, Aig_ObjInit(pObj) );
else
assert( 0 );
// replace the node with buffer by the node without buffer
Aig_ObjReplace( p, pObj, pResult, fNodesOnly, fUpdateLevel );
}
/**Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel )
{
Aig_Obj_t * pObj;
int nSteps;
assert( p->pFanData );
for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
{
// get the node with a buffer fanin
for ( pObj = Vec_PtrEntryLast(p->vBufs); Aig_ObjIsBuf(pObj); pObj = Aig_ObjFanout0(p, pObj) );
// replace this node by a node without buffer
Aig_NodeFixBufferFanins( p, pObj, fNodesOnly, fUpdateLevel );
// stop if a cycle occured
if ( nSteps > 1000000 )
{
printf( "Error: A cycle is encountered while propagating buffers.\n" );
break;
}
}
return nSteps;
}
/**Function*************************************************************
Synopsis [Replaces one object by another.]
Description [Both objects are currently in the manager. The new object
(pObjNew) should be used instead of the old object (pObjOld). If the
new object is complemented or used, the buffer is added.]
Description [The new object (pObjNew) should be used instead of the old
object (pObjOld). If the new object is complemented or used, the buffer
is added and the new object remains in the manager; otherwise, the new
object is deleted.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly )
void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel )
{
Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew);
// the object to be replaced cannot be complemented
......@@ -288,17 +367,34 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
{
pObjOld->Type = AIG_OBJ_BUF;
Aig_ObjConnect( p, pObjOld, pObjNew, NULL );
p->nBufReplaces++;
}
else
{
Aig_Obj_t * pFanin0 = pObjNew->pFanin0;
Aig_Obj_t * pFanin1 = pObjNew->pFanin1;
int LevelOld = pObjOld->Level;
pObjOld->Type = pObjNew->Type;
Aig_ObjDisconnect( p, pObjNew );
Aig_ObjConnect( p, pObjOld, pFanin0, pFanin1 );
// delete the new object
Aig_ObjDelete( p, pObjNew );
// update levels
if ( fUpdateLevel )
{
pObjOld->Level = LevelOld;
Aig_ManUpdateLevel( p, pObjOld );
Aig_ManUpdateReverseLevel( p, pObjOld );
}
}
p->nObjs[pObjOld->Type]++;
// store buffers if fanout is allocated
if ( p->pFanData && Aig_ObjIsBuf(pObjOld) )
{
Vec_PtrPush( p->vBufs, pObjOld );
p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
Aig_ManPropagateBuffers( p, fNodesOnly, fUpdateLevel );
}
}
////////////////////////////////////////////////////////////////////////
......
......@@ -43,6 +43,7 @@ void Aig_ManSeqStrashConvert( Aig_Man_t * p, int nLatches, int * pInits )
{
Aig_Obj_t * pObjLi, * pObjLo, * pLatch;
int i;
assert( Vec_PtrSize( p->vBufs ) == 0 );
// collect the POs to be converted into latches
for ( i = 0; i < nLatches; i++ )
{
......@@ -58,6 +59,8 @@ void Aig_ManSeqStrashConvert( Aig_Man_t * p, int nLatches, int * pInits )
// convert the corresponding PI to be a buffer and connect it to the latch
pObjLo->Type = AIG_OBJ_BUF;
Aig_ObjConnect( p, pObjLo, pLatch, NULL );
// save the buffer
// Vec_PtrPush( p->vBufs, pObjLo );
}
// shrink the arrays
Vec_PtrShrink( p->vPis, Aig_ManPiNum(p) - nLatches );
......@@ -353,7 +356,7 @@ int Aig_ManSeqRehashOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach
continue;
pObjNew = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
pObjNew = Aig_Latch( p, pObjNew, 0 );
Aig_ObjReplace( p, pObj, pObjNew, 1 );
Aig_ObjReplace( p, pObj, pObjNew, 1, 0 );
RetValue = 1;
Counter++;
continue;
......@@ -365,7 +368,7 @@ int Aig_ManSeqRehashOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach
pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
pObjNew = Aig_And( p, pFanin0, pFanin1 );
Aig_ObjReplace( p, pObj, pObjNew, 1 );
Aig_ObjReplace( p, pObj, pObjNew, 1, 0 );
RetValue = 1;
Counter++;
continue;
......@@ -407,7 +410,7 @@ void Aig_ManRemoveBuffers( Aig_Man_t * p )
continue;
pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
pObjNew = Aig_Latch( p, pFanin0, 0 );
Aig_ObjReplace( p, pObj, pObjNew, 0 );
Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
}
else if ( Aig_ObjIsAnd(pObj) )
{
......@@ -416,7 +419,7 @@ void Aig_ManRemoveBuffers( Aig_Man_t * p )
pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
pObjNew = Aig_And( p, pFanin0, pFanin1 );
Aig_ObjReplace( p, pObj, pObjNew, 0 );
Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
}
}
assert( Aig_ManBufNum(p) == 0 );
......
......@@ -28,8 +28,8 @@
static unsigned long Aig_Hash( Aig_Obj_t * pObj, int TableSize )
{
unsigned long Key = Aig_ObjIsExor(pObj) * 1699;
Key ^= (long)Aig_ObjFanin0(pObj) * 7937;
Key ^= (long)Aig_ObjFanin1(pObj) * 2971;
Key ^= Aig_ObjFanin0(pObj)->Id * 7937;
Key ^= Aig_ObjFanin1(pObj)->Id * 2971;
Key ^= Aig_ObjFaninC0(pObj) * 911;
Key ^= Aig_ObjFaninC1(pObj) * 353;
return Key % TableSize;
......@@ -55,15 +55,58 @@ static Aig_Obj_t ** Aig_TableFind( Aig_Man_t * p, Aig_Obj_t * pObj )
return ppEntry;
}
static void Aig_TableResize( Aig_Man_t * p );
static unsigned int Cudd_PrimeAig( unsigned int p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Resizes the table.]
Description [Typically this procedure should not be called.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_TableResize( Aig_Man_t * p )
{
Aig_Obj_t * pEntry, * pNext;
Aig_Obj_t ** pTableOld, ** ppPlace;
int nTableSizeOld, Counter, nEntries, i, clk;
clk = clock();
// save the old table
pTableOld = p->pTable;
nTableSizeOld = p->nTableSize;
// get the new table
p->nTableSize = Aig_PrimeCudd( 2 * Aig_ManNodeNum(p) );
p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
// rehash the entries from the old table
Counter = 0;
for ( i = 0; i < nTableSizeOld; i++ )
for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL;
pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL )
{
// get the place where this entry goes in the table
ppPlace = Aig_TableFind( p, pEntry );
assert( *ppPlace == NULL ); // should not be there
// add the entry to the list
*ppPlace = pEntry;
pEntry->pNext = NULL;
Counter++;
}
nEntries = Aig_ManNodeNum(p);
assert( Counter == nEntries );
printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
PRT( "Time", clock() - clk );
// replace the table and the parameters
free( pTableOld );
}
/**Function*************************************************************
Synopsis [Checks if node with the given attributes is in the hash table.]
Description []
......@@ -167,51 +210,6 @@ int Aig_TableCountEntries( Aig_Man_t * p )
return Counter;
}
/**Function*************************************************************
Synopsis [Resizes the table.]
Description [Typically this procedure should not be called.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_TableResize( Aig_Man_t * p )
{
Aig_Obj_t * pEntry, * pNext;
Aig_Obj_t ** pTableOld, ** ppPlace;
int nTableSizeOld, Counter, nEntries, i, clk;
clk = clock();
// save the old table
pTableOld = p->pTable;
nTableSizeOld = p->nTableSize;
// get the new table
p->nTableSize = Cudd_PrimeAig( 2 * Aig_ManNodeNum(p) );
p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
// rehash the entries from the old table
Counter = 0;
for ( i = 0; i < nTableSizeOld; i++ )
for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL; pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL )
{
// get the place where this entry goes in the table
ppPlace = Aig_TableFind( p, pEntry );
assert( *ppPlace == NULL ); // should not be there
// add the entry to the list
*ppPlace = pEntry;
pEntry->pNext = NULL;
Counter++;
}
nEntries = Aig_ManNodeNum(p);
assert( Counter == nEntries );
printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
PRT( "Time", clock() - clk );
// replace the table and the parameters
free( pTableOld );
}
/**Function********************************************************************
Synopsis [Profiles the hash table.]
......@@ -237,41 +235,6 @@ void Aig_TableProfile( Aig_Man_t * p )
}
}
/**Function********************************************************************
Synopsis [Returns the next prime &gt;= p.]
Description [Copied from CUDD, for stand-aloneness.]
SideEffects [None]
SeeAlso []
******************************************************************************/
unsigned int Cudd_PrimeAig( unsigned int p)
{
int i,pn;
p--;
do {
p++;
if (p&1) {
pn = 1;
i = 3;
while ((unsigned) (i * i) <= p) {
if (p % i == 0) {
pn = 0;
break;
}
i += 2;
}
} else {
pn = 0;
}
} while (!pn);
return(p);
} /* end of Cudd_Prime */
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
/**CFile****************************************************************
FileName [aigTiming.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis [Incremental updating of direct/reverse AIG levels.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: aigTiming.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns the reverse level of the node.]
Description [The reverse level is the level of the node in reverse
topological order, starting from the COs.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Aig_ObjReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj )
{
assert( p->vLevelR );
Vec_IntFillExtra( p->vLevelR, pObj->Id + 1, 0 );
return Vec_IntEntry(p->vLevelR, pObj->Id);
}
/**Function*************************************************************
Synopsis [Sets the reverse level of the node.]
Description [The reverse level is the level of the node in reverse
topological order, starting from the COs.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Aig_ObjSetReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj, int LevelR )
{
assert( p->vLevelR );
Vec_IntFillExtra( p->vLevelR, pObj->Id + 1, 0 );
Vec_IntWriteEntry( p->vLevelR, pObj->Id, LevelR );
}
/**Function*************************************************************
Synopsis [Returns required level of the node.]
Description [Converts the reverse levels of the node into its required
level as follows: ReqLevel(Node) = MaxLevels(Ntk) + 1 - LevelR(Node).]
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj )
{
assert( p->vLevelR );
return p->nLevelMax + 1 - Aig_ObjReverseLevel(p, pObj);
}
/**Function*************************************************************
Synopsis [Computes the reverse level of the node using its fanout levels.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ObjReverseLevelNew( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pFanout;
int i, iFanout, LevelCur, Level = 0;
Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
{
LevelCur = Aig_ObjReverseLevel( p, pFanout );
Level = AIG_MAX( Level, LevelCur );
}
return Level + 1;
}
/**Function*************************************************************
Synopsis [Prepares for the computation of required levels.]
Description [This procedure should be called before the required times
are used. It starts internal data structures, which records the level
from the COs of the network nodes in reverse topologogical order.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease )
{
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
assert( p->pFanData != NULL );
assert( p->vLevelR == NULL );
// remember the maximum number of direct levels
p->nLevelMax = Aig_ManLevels(p) + nMaxLevelIncrease;
// start the reverse levels
p->vLevelR = Vec_IntAlloc( 0 );
Vec_IntFill( p->vLevelR, 1 + Aig_ManObjIdMax(p), 0 );
// compute levels in reverse topological order
vNodes = Aig_ManDfsReverse( p );
Vec_PtrForEachEntry( vNodes, pObj, i )
{
assert( pObj->fMarkA == 0 );
Aig_ObjSetReverseLevel( p, pObj, Aig_ObjReverseLevelNew(p, pObj) );
}
Vec_PtrFree( vNodes );
}
/**Function*************************************************************
Synopsis [Cleans the data structures used to compute required levels.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManStopReverseLevels( Aig_Man_t * p )
{
assert( p->vLevelR != NULL );
Vec_IntFree( p->vLevelR );
p->vLevelR = NULL;
p->nLevelMax = 0;
}
/**Function*************************************************************
Synopsis [Incrementally updates level of the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
{
Aig_Obj_t * pFanout, * pTemp;
int iFanout, LevelOld, Lev, k, m;
assert( p->pFanData != NULL );
// allocate level if needed
if ( p->vLevels == NULL )
p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 );
// check if level has changed
LevelOld = Aig_ObjLevel(pObjNew);
if ( LevelOld == Aig_ObjLevelNew(pObjNew) )
return;
// start the data structure for level update
// we cannot fail to visit a node when using this structure because the
// nodes are stored by their _old_ levels, which are assumed to be correct
Vec_VecClear( p->vLevels );
Vec_VecPush( p->vLevels, LevelOld, pObjNew );
pObjNew->fMarkA = 1;
// recursively update level
Vec_VecForEachEntryStart( p->vLevels, pTemp, Lev, k, LevelOld )
{
pTemp->fMarkA = 0;
assert( Aig_ObjLevel(pTemp) == Lev );
pTemp->Level = Aig_ObjLevelNew(pTemp);
// if the level did not change, no need to check the fanout levels
if ( Aig_ObjLevel(pTemp) == Lev )
continue;
// schedule fanout for level update
Aig_ObjForEachFanout( p, pTemp, pFanout, iFanout, m )
{
if ( !Aig_ObjIsPo(pFanout) && !pFanout->fMarkA )
{
Vec_VecPush( p->vLevels, Aig_ObjLevel(pFanout), pFanout );
pFanout->fMarkA = 1;
}
}
}
}
/**Function*************************************************************
Synopsis [Incrementally updates level of the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
{
Aig_Obj_t * pFanin, * pTemp;
int LevelOld, Lev, k;
assert( p->vLevelR != NULL );
// allocate level if needed
if ( p->vLevels == NULL )
p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 );
// check if level has changed
LevelOld = Aig_ObjReverseLevel(p, pObjNew);
if ( LevelOld == Aig_ObjReverseLevelNew(p, pObjNew) )
return;
// start the data structure for level update
// we cannot fail to visit a node when using this structure because the
// nodes are stored by their _old_ levels, which are assumed to be correct
Vec_VecClear( p->vLevels );
Vec_VecPush( p->vLevels, LevelOld, pObjNew );
pObjNew->fMarkA = 1;
// recursively update level
Vec_VecForEachEntryStart( p->vLevels, pTemp, Lev, k, LevelOld )
{
pTemp->fMarkA = 0;
LevelOld = Aig_ObjReverseLevel(p, pTemp);
assert( LevelOld == Lev );
Aig_ObjSetReverseLevel( p, pTemp, Aig_ObjReverseLevelNew(p, pTemp) );
// if the level did not change, to need to check the fanout levels
if ( Aig_ObjReverseLevel(p, pTemp) == Lev )
continue;
// schedule fanins for level update
pFanin = Aig_ObjFanin0(pTemp);
if ( pFanin && !Aig_ObjIsPi(pFanin) && !pFanin->fMarkA )
{
Vec_VecPush( p->vLevels, Aig_ObjReverseLevel(p, pFanin), pFanin );
pFanin->fMarkA = 1;
}
pFanin = Aig_ObjFanin1(pTemp);
if ( pFanin && !Aig_ObjIsPi(pFanin) && !pFanin->fMarkA )
{
Vec_VecPush( p->vLevels, Aig_ObjReverseLevel(p, pFanin), pFanin );
pFanin->fMarkA = 1;
}
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigDfs.c \
src/aig/aig/aigFanout.c \
src/aig/aig/aigMan.c \
src/aig/aig/aigMem.c \
src/aig/aig/aigObj.c \
src/aig/aig/aigOper.c \
src/aig/aig/aigSeq.c \
src/aig/aig/aigTable.c \
src/aig/aig/aigTiming.c \
src/aig/aig/aigUtil.c
......@@ -49,7 +49,7 @@ static Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig
Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjNew;
Aig_Obj_t * pObj, * pDriver, * pObjNew;
Vec_Vec_t * vStore;
int i;
// create the new manager
......@@ -63,14 +63,15 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
vStore = Vec_VecAlloc( 50 );
Aig_ManForEachPo( p, pObj, i )
{
pObjNew = Dar_Balance_rec( pNew, Aig_ObjFanin0(pObj), vStore, 0, fUpdateLevel );
Aig_ObjCreatePo( pNew, Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ) );
pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
Aig_ObjCreatePo( pNew, pObjNew );
}
Vec_VecFree( vStore );
// remove dangling nodes
// Aig_ManCreateRefs( pNew );
// if ( i = Aig_ManCleanup( pNew ) )
// printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
if ( i = Aig_ManCleanup( pNew ) )
printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
// check the resulting AIG
if ( !Aig_ManCheck(pNew) )
printf( "Dar_ManBalance(): The check has failed.\n" );
......@@ -94,6 +95,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
Vec_Ptr_t * vSuper;
int i;
assert( !Aig_IsComplement(pObjOld) );
assert( !Aig_ObjIsBuf(pObjOld) );
// return if the result is known
if ( pObjOld->pData )
return pObjOld->pData;
......@@ -157,8 +159,8 @@ int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper
assert( !Aig_IsComplement(pObj) );
assert( Aig_ObjIsNode(pObj) );
// go through the branches
RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild1(pObj), vSuper );
RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
if ( RetValue1 == -1 || RetValue2 == -1 )
return -1;
// return 1 if at least one branch has a duplicate
......
......@@ -43,7 +43,7 @@ void Dar_ManDefaultParams( Dar_Par_t * pPars )
{
memset( pPars, 0, sizeof(Dar_Par_t) );
pPars->nCutsMax = 8;
pPars->nSubgMax = 4;
pPars->nSubgMax = 5; // 5 is a "magic number"
pPars->fUpdateLevel = 0;
pPars->fUseZeros = 0;
pPars->fVerbose = 0;
......@@ -69,18 +69,18 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars )
Aig_Obj_t * pObj, * pObjNew;
int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
int clk = 0, clkStart;
// prepare the library
Dar_LibPrepare( pPars->nSubgMax );
// create rewriting manager
p = Dar_ManStart( pAig, pPars );
// remove dangling nodes
Aig_ManCleanup( pAig );
// if updating levels is requested, start fanout and timing
Aig_ManCreateFanout( pAig );
if ( p->pPars->fUpdateLevel )
Aig_ManStartReverseLevels( pAig, 0 );
// set elementary cuts for the PIs
// Dar_ManSetupPis( p );
Aig_ManCleanData( pAig );
Dar_ObjPrepareCuts( p, Aig_ManConst1(pAig) );
Aig_ManForEachPi( pAig, pObj, i )
Dar_ObjPrepareCuts( p, pObj );
// if ( p->pPars->fUpdateLevel )
// Aig_NtkStartReverseLevels( p );
Dar_ManCutsStart( p );
// resynthesize each node once
clkStart = clock();
p->nNodesInit = Aig_ManNodeNum(pAig);
......@@ -93,6 +93,10 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars )
continue;
if ( i > nNodesOld )
break;
// consider freeing the cuts
// if ( (i & 0xFFF) == 0 && Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) > 100 )
// Dar_ManCutsStart( p );
// compute cuts for the node
clk = clock();
Dar_ObjComputeCuts_rec( p, pObj );
......@@ -100,7 +104,7 @@ p->timeCuts += clock() - clk;
// check if there is a trivial cut
Dar_ObjForEachCut( pObj, pCut, k )
if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id) )
if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id && Aig_ManObj(p->pAig, pCut->pLeaves[0])) )
break;
if ( k < (int)pObj->nCuts )
{
......@@ -115,10 +119,10 @@ p->timeCuts += clock() - clk;
assert( pCut->uTruth == 0xAAAA || pCut->uTruth == 0x5555 );
pObjNew = Aig_NotCond( Aig_ManObj(p->pAig, pCut->pLeaves[0]), pCut->uTruth==0x5555 );
}
// replace the node
Aig_ObjReplace( pAig, pObj, pObjNew, 1 );
// remove the old cuts
Dar_ObjSetCuts( pObj, NULL );
// replace the node
Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
continue;
}
......@@ -128,17 +132,17 @@ p->timeCuts += clock() - clk;
Dar_ObjForEachCut( pObj, pCut, k )
Dar_LibEval( p, pObj, pCut, Required );
// check the best gain
if ( !(p->GainBest > 0 || p->GainBest == 0 && p->pPars->fUseZeros) )
if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
continue;
// remove the old cuts
Dar_ObjSetCuts( pObj, NULL );
// if we end up here, a rewriting step is accepted
nNodeBefore = Aig_ManNodeNum( pAig );
pObjNew = Dar_LibBuildBest( p );
pObjNew = Aig_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
assert( (int)Aig_Regular(pObjNew)->Level <= Required );
// replace the node
Aig_ObjReplace( pAig, pObj, pObjNew, 1 );
// remove the old cuts
Dar_ObjSetCuts( pObj, NULL );
Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
// compare the gains
nNodeAfter = Aig_ManNodeNum( pAig );
assert( p->GainBest <= nNodeBefore - nNodeAfter );
......@@ -151,13 +155,14 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
Extra_ProgressBarStop( pProgress );
p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20);
Dar_ManCutsFree( p );
// stop the rewriting manager
Dar_ManStop( p );
// put the nodes into the DFS order and reassign their IDs
// Aig_NtkReassignIds( p );
// fix the levels
// if ( p->pPars->fUpdateLevel )
// Aig_NtkStopReverseLevels( p );
Aig_ManDeleteFanout( pAig );
if ( p->pPars->fUpdateLevel )
Aig_ManStopReverseLevels( pAig );
// stop the rewriting manager
Dar_ManStop( p );
// check
if ( !Aig_ManCheck( pAig ) )
{
......@@ -190,9 +195,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig )
// remove dangling nodes
Aig_ManCleanup( pAig );
// set elementary cuts for the PIs
// Dar_ManSetupPis( p );
Aig_ManForEachPi( pAig, pObj, i )
Dar_ObjPrepareCuts( p, pObj );
Dar_ManCutsStart( p );
// compute cuts for each nodes in the topological order
Aig_ManForEachObj( pAig, pObj, i )
{
......
......@@ -62,20 +62,25 @@ static inline int Dar_WordCountOnes( unsigned uWord )
static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Aig_Obj_t * pLeaf;
int i, Value;
int i, Value, nOnes;
assert( pCut->fUsed );
if ( pCut->nLeaves < 2 )
return 1001;
Value = 0;
nOnes = 0;
Dar_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
{
if ( pLeaf == NULL )
return 0;
assert( pLeaf != NULL );
Value += pLeaf->nRefs;
nOnes += (pLeaf->nRefs == 1);
}
if ( pCut->nLeaves < 2 )
return 1001;
// Value = Value * 100 / pCut->nLeaves;
if ( Value > 1000 )
Value = 1000;
if ( nOnes > 3 )
Value = 5 - nOnes;
return Value;
}
......@@ -83,7 +88,7 @@ static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut )
Synopsis [Returns the next free cut to use.]
Description []
Description [Uses the cut with the smallest value.]
SideEffects []
......@@ -114,6 +119,14 @@ static inline Dar_Cut_t * Dar_CutFindFree( Dar_Man_t * p, Aig_Obj_t * pObj )
pCutMax = pCut;
}
}
if ( pCutMax == NULL )
{
Dar_ObjForEachCutAll( pObj, pCut, i )
{
if ( pCutMax == NULL || pCutMax->Value > pCut->Value )
pCutMax = pCut;
}
}
assert( pCutMax != NULL );
pCutMax->fUsed = 0;
return pCutMax;
......@@ -466,7 +479,6 @@ static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
unsigned uPhase = 0, uTruth = 0xFFFF & pCut->uTruth;
int i, k, nLeaves;
assert( pCut->fUsed );
assert( pCut->nLeaves > 0 );
// compute the truth support of the cut's function
nLeaves = pCut->nLeaves;
for ( i = 0; i < (int)pCut->nLeaves; i++ )
......@@ -566,6 +578,28 @@ Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
void Dar_ManCutsStart( Dar_Man_t * p )
{
Aig_Obj_t * pObj;
int i;
Aig_ManCleanData( p->pAig );
Aig_MmFixedRestart( p->pMemCuts );
Dar_ObjPrepareCuts( p, Aig_ManConst1(p->pAig) );
Aig_ManForEachPi( p->pAig, pObj, i )
Dar_ObjPrepareCuts( p, pObj );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
......@@ -612,10 +646,6 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
// minimize support of the cut
if ( Dar_CutSuppMinimize( pCut ) )
{
// if a simple cut is found return immediately
if ( pCut->nLeaves < 2 )
return pCutSet;
// otherwise, filter the cuts again
RetValue = Dar_CutFilter( pObj, pCut );
assert( !RetValue );
}
......@@ -628,6 +658,8 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
p->nCutsSkipped++;
pCut->fUsed = 0;
}
else if ( pCut->nLeaves < 2 )
return pCutSet;
}
// count the number of nontrivial cuts cuts
Dar_ObjForEachCut( pObj, pCut, i )
......
......@@ -101,7 +101,7 @@ struct Dar_Man_t_
};
static inline Dar_Cut_t * Dar_ObjCuts( Aig_Obj_t * pObj ) { return pObj->pData; }
static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts ) { pObj->pData = pCuts; }
static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts ) { assert( !Aig_ObjIsNone(pObj) ); pObj->pData = pCuts; }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
......@@ -126,22 +126,24 @@ static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )
/*=== darBalance.c ========================================================*/
extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
/*=== darCore.c ========================================================*/
/*=== darCut.c ========================================================*/
extern Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
/*=== darCore.c ===========================================================*/
/*=== darCut.c ============================================================*/
extern void Dar_ManCutsStart( Dar_Man_t * p );
extern void Dar_ManCutsFree( Dar_Man_t * p );
extern Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
extern Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
/*=== darData.c ========================================================*/
/*=== darData.c ===========================================================*/
extern Vec_Int_t * Dar_LibReadNodes();
extern Vec_Int_t * Dar_LibReadOuts();
extern Vec_Int_t * Dar_LibReadPrios();
/*=== darLib.c ==========================================================*/
/*=== darLib.c ============================================================*/
extern void Dar_LibStart();
extern void Dar_LibStop();
extern void Dar_LibPrepare( int nSubgraphs );
extern void Dar_LibReturnCanonicals( unsigned * pCanons );
extern void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
extern Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p );
/*=== darMan.c ==========================================================*/
/*=== darMan.c ============================================================*/
extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars );
extern void Dar_ManStop( Dar_Man_t * p );
extern void Dar_ManPrintStats( Dar_Man_t * p );
......
......@@ -44,7 +44,7 @@ struct Dar_LibDat_t_ // library object data
Aig_Obj_t * pFunc; // the corresponding AIG node if it exists
int Level; // level of this node after it is constructured
int TravId; // traversal ID of the library object data
unsigned char Area; // area of the node
unsigned char fMffc; // set to one if node is part of MFFC
unsigned char nLats[3]; // the number of latches on the input/output stem
};
......@@ -54,9 +54,6 @@ struct Dar_Lib_t_ // library
Dar_LibObj_t * pObjs; // the set of library objects
int nObjs; // the number of objects used
int iObj; // the current object
// object data
Dar_LibDat_t * pDatas;
int nDatas;
// structures by class
int nSubgr[222]; // the number of subgraphs by class
int * pSubgr[222]; // the subgraphs for each class
......@@ -75,8 +72,24 @@ struct Dar_Lib_t_ // library
int nNodes[222]; // the number of nodes by class
int * pNodes[222]; // the nodes for each class
int * pNodesMem; // memory for nodes pointers
int pNodesTotal; // the total number of nodes
// information by NPN classes
int nNodesTotal; // the total number of nodes
// prepared library
int nSubgraphs;
int nNodes0Max;
// nodes by class
int nNodes0[222]; // the number of nodes by class
int * pNodes0[222]; // the nodes for each class
int * pNodes0Mem; // memory for nodes pointers
int nNodes0Total; // the total number of nodes
// structures by class
int nSubgr0[222]; // the number of subgraphs by class
int * pSubgr0[222]; // the subgraphs for each class
int * pSubgr0Mem; // memory for subgraph pointers
int nSubgr0Total; // the total number of subgraph
// object data
Dar_LibDat_t * pDatas;
int nDatas;
// information about NPN classes
char ** pPerms4;
unsigned short * puCanons;
char * pPhases;
......@@ -104,7 +117,7 @@ static inline int Dar_LibObjTruth( Dar_LibObj_t * pObj ) { return pOb
SeeAlso []
***********************************************************************/
Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas )
Dar_Lib_t * Dar_LibAlloc( int nObjs )
{
unsigned uTruths[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
Dar_Lib_t * p;
......@@ -115,10 +128,6 @@ Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas )
p->nObjs = nObjs;
p->pObjs = ALLOC( Dar_LibObj_t, nObjs );
memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs );
// allocate datas
p->nDatas = nDatas;
p->pDatas = ALLOC( Dar_LibDat_t, nDatas );
memset( p->pObjs, 0, sizeof(Dar_LibDat_t) * nDatas );
// allocate canonical data
p->pPerms4 = Extra_Permutations( 4 );
Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
......@@ -149,7 +158,9 @@ void Dar_LibFree( Dar_Lib_t * p )
free( p->pObjs );
free( p->pDatas );
free( p->pNodesMem );
free( p->pNodes0Mem );
free( p->pSubgrMem );
free( p->pSubgr0Mem );
free( p->pPriosMem );
FREE( p->pPlaceMem );
FREE( p->pScoreMem );
......@@ -163,6 +174,31 @@ void Dar_LibFree( Dar_Lib_t * p )
/**Function*************************************************************
Synopsis [Returns canonical truth tables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_LibReturnCanonicals( unsigned * pCanons )
{
int Visits[222] = {0};
int i, k;
// find canonical truth tables
for ( i = k = 0; i < (1<<16); i++ )
if ( !Visits[s_DarLib->pMap[i]] )
{
Visits[s_DarLib->pMap[i]] = 1;
pCanons[k++] = ((i<<16) | i);
}
assert( k == 222 );
}
/**Function*************************************************************
Synopsis [Adds one AND to the library.]
Description []
......@@ -196,14 +232,14 @@ void Dar_LibAddNode( Dar_Lib_t * p, int Id0, int Id1, int fCompl0, int fCompl1 )
SeeAlso []
***********************************************************************/
void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class )
void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect )
{
if ( pObj->fTerm || (int)pObj->Num == Class )
return;
pObj->Num = Class;
Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class );
Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class );
if ( p->pNodesMem )
Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
if ( fCollect )
p->pNodes[Class][ p->nNodes[Class]++ ] = pObj-p->pObjs;
else
p->nNodes[Class]++;
......@@ -239,10 +275,12 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
}
// allocate memory for the roots of each class
p->pSubgrMem = ALLOC( int, Vec_IntSize(vOuts) );
p->pSubgr0Mem = ALLOC( int, Vec_IntSize(vOuts) );
p->nSubgrTotal = 0;
for ( i = 0; i < 222; i++ )
{
p->pSubgr[i] = p->pSubgrMem + p->nSubgrTotal;
p->pSubgr0[i] = p->pSubgr0Mem + p->nSubgrTotal;
p->nSubgrTotal += p->nSubgr[i];
p->nSubgr[i] = 0;
}
......@@ -321,18 +359,20 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
// count nodes in each class
for ( i = 0; i < 222; i++ )
for ( k = 0; k < p->nSubgr[i]; k++ )
Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i );
Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 0 );
// count the total number of nodes
p->pNodesTotal = 0;
p->nNodesTotal = 0;
for ( i = 0; i < 222; i++ )
p->pNodesTotal += p->nNodes[i];
p->nNodesTotal += p->nNodes[i];
// allocate memory for the nodes of each class
p->pNodesMem = ALLOC( int, p->pNodesTotal );
p->pNodesTotal = 0;
p->pNodesMem = ALLOC( int, p->nNodesTotal );
p->pNodes0Mem = ALLOC( int, p->nNodesTotal );
p->nNodesTotal = 0;
for ( i = 0; i < 222; i++ )
{
p->pNodes[i] = p->pNodesMem + p->pNodesTotal;
p->pNodesTotal += p->nNodes[i];
p->pNodes[i] = p->pNodesMem + p->nNodesTotal;
p->pNodes0[i] = p->pNodes0Mem + p->nNodesTotal;
p->nNodesTotal += p->nNodes[i];
p->nNodes[i] = 0;
}
// create traversal IDs
......@@ -343,14 +383,141 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
for ( i = 0; i < 222; i++ )
{
for ( k = 0; k < p->nSubgr[i]; k++ )
Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i );
Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 1 );
nNodesTotal += p->nNodes[i];
//printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] );
}
assert( nNodesTotal == p->pNodesTotal );
assert( nNodesTotal == p->nNodesTotal );
// prepare the number of the PI nodes
for ( i = 0; i < 4; i++ )
Dar_LibObj(p, i)->Num = i;
}
/**Function*************************************************************
Synopsis [Starts the library.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_LibCreateData( Dar_Lib_t * p, int nDatas )
{
if ( p->nDatas == nDatas )
return;
FREE( p->pDatas );
// allocate datas
p->nDatas = nDatas;
p->pDatas = ALLOC( Dar_LibDat_t, nDatas );
memset( p->pDatas, 0, sizeof(Dar_LibDat_t) * nDatas );
}
/**Function*************************************************************
Synopsis [Adds one AND to the library.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_LibSetup0_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect )
{
if ( pObj->fTerm || (int)pObj->Num == Class )
return;
pObj->Num = Class;
Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
if ( fCollect )
p->pNodes0[Class][ p->nNodes0[Class]++ ] = pObj-p->pObjs;
else
p->nNodes0[Class]++;
}
/**Function*************************************************************
Synopsis [Starts the library.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_LibPrepare( int nSubgraphs )
{
Dar_Lib_t * p = s_DarLib;
int i, k, nNodes0Total;
if ( p->nSubgraphs == nSubgraphs )
return;
// favor special classes:
// 1 : F = (!d*!c*!b*!a)
// 4 : F = (!d*!c*!(b*a))
// 12 : F = (!d*!(c*!(!b*!a)))
// 20 : F = (!d*!(c*b*a))
// set the subgraph counters
p->nSubgr0Total = 0;
for ( i = 0; i < 222; i++ )
{
// if ( i == 1 || i == 4 || i == 12 || i == 20 ) // special classes
if ( i == 1 ) // special classes
p->nSubgr0[i] = p->nSubgr[i];
else
p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs );
p->nSubgr0Total += p->nSubgr0[i];
for ( k = 0; k < p->nSubgr0[i]; k++ )
p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ];
}
// count the number of nodes
// clean node counters
for ( i = 0; i < 222; i++ )
p->nNodes0[i] = 0;
// create traversal IDs
for ( i = 0; i < p->iObj; i++ )
Dar_LibObj(p, i)->Num = 0xff;
// count nodes in each class
// count the total number of nodes and the largest class
p->nNodes0Total = 0;
p->nNodes0Max = 0;
for ( i = 0; i < 222; i++ )
{
for ( k = 0; k < p->nSubgr0[i]; k++ )
Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 );
p->nNodes0Total += p->nNodes0[i];
p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] );
}
// clean node counters
for ( i = 0; i < 222; i++ )
p->nNodes0[i] = 0;
// create traversal IDs
for ( i = 0; i < p->iObj; i++ )
Dar_LibObj(p, i)->Num = 0xff;
// add the nodes to storage
nNodes0Total = 0;
for ( i = 0; i < 222; i++ )
{
for ( k = 0; k < p->nSubgr0[i]; k++ )
Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 1 );
nNodes0Total += p->nNodes0[i];
}
assert( nNodes0Total == p->nNodes0Total );
// prepare the number of the PI nodes
for ( i = 0; i < 4; i++ )
Dar_LibObj(p, i)->Num = i;
// realloc the datas
Dar_LibCreateData( p, p->nNodes0Max + 32 );
// allocated more because Dar_LibBuildBest() sometimes requires more entries
}
/**Function*************************************************************
......@@ -374,7 +541,7 @@ Dar_Lib_t * Dar_LibRead()
vOuts = Dar_LibReadOuts();
vPrios = Dar_LibReadPrios();
// create library
p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4, 6000 );
p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4 );
// create nodes
for ( i = 0; i < vObjs->nSize; i += 2 )
Dar_LibAddNode( p, vObjs->pArray[i] >> 1, vObjs->pArray[i+1] >> 1,
......@@ -383,6 +550,7 @@ Dar_Lib_t * Dar_LibRead()
Dar_LibSetup( p, vOuts, vPrios );
Vec_IntFree( vObjs );
Vec_IntFree( vOuts );
Vec_IntFree( vPrios );
return p;
}
......@@ -670,15 +838,20 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
Dar_LibDat_t * pData, * pData0, * pData1;
Aig_Obj_t * pGhost, * pFanin0, * pFanin1;
int i;
for ( i = 0; i < s_DarLib->nNodes[Class]; i++ )
for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ )
{
// get one class node, assign its temporary number and set its data
pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes[Class][i]);
pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes0[Class][i]);
pObj->Num = 4 + i;
assert( (int)pObj->Num < s_DarLib->nNodes0Max + 4 );
pData = s_DarLib->pDatas + pObj->Num;
pData->fMffc = 0;
pData->pFunc = NULL;
pData->TravId = 0xFFFF;
// explore the fanins
assert( (int)Dar_LibObj(s_DarLib, pObj->Fan0)->Num < s_DarLib->nNodes0Max + 4 );
assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 );
pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
pData->Level = 1 + AIG_MAX(pData0->Level, pData1->Level);
......@@ -704,9 +877,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
// clear the node if it is part of MFFC
if ( pData->pFunc != NULL && Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc) )
pData->pFunc = NULL;
//if ( Class == 7 )
//printf( "Evaling node %d at data %d\n", pData->pFunc? pData->pFunc->Id : -1, pObj->Num );
pData->fMffc = 1;
}
}
......@@ -729,20 +900,22 @@ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required
return 0;
assert( pObj->Num > 3 );
pData = s_DarLib->pDatas + pObj->Num;
if ( pData->pFunc )
if ( pData->pFunc && !pData->fMffc )
return 0;
if ( pData->Level > Required )
return 0xff;
if ( pData->TravId == Out )
return pData->Area;
return 0;
pData->TravId = Out;
Area = 1 + Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required );
// this is a new node - get a bound on the area of its branches
nNodesSaved--;
Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1 );
if ( Area > nNodesSaved )
return pData->Area = 0xff;
Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required );
return 0xff;
Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required+1 );
if ( Area > nNodesSaved )
return pData->Area = 0xff;
return pData->Area = Area;
return 0xff;
return Area + 1;
}
/**Function*************************************************************
......@@ -773,25 +946,27 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
Class = s_DarLib->pMap[pCut->uTruth];
Dar_LibEvalAssignNums( p, Class );
// profile outputs by their savings
p->nTotalSubgs += s_DarLib->nSubgr[Class];
p->ClassSubgs[Class] += s_DarLib->nSubgr[Class];
for ( Out = 0; Out < s_DarLib->nSubgr[Class]; Out++ )
p->nTotalSubgs += s_DarLib->nSubgr0[Class];
p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class];
for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ )
{
pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr[Class][Out]);
nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved, Required );
pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]);
if ( Aig_Regular(s_DarLib->pDatas[pObj->Num].pFunc) == pRoot )
continue;
nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required );
nNodesGained = nNodesSaved - nNodesAdded;
if ( fTraining && nNodesGained >= 0 )
Dar_LibIncrementScore( Class, Out, nNodesGained + 1 );
if ( nNodesGained <= 0 )
if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) )
continue;
if ( nNodesGained < p->GainBest ||
(nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->GainBest) )
(nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->LevelBest) )
continue;
// remember this possibility
Vec_PtrClear( p->vLeavesBest );
for ( k = 0; k < (int)pCut->nLeaves; k++ )
Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc );
p->OutBest = s_DarLib->pSubgr[Class][Out];
p->OutBest = s_DarLib->pSubgr0[Class][Out];
p->OutNumBest = Out;
p->LevelBest = s_DarLib->pDatas[pObj->Num].Level;
p->GainBest = nNodesGained;
......@@ -845,7 +1020,6 @@ Aig_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj )
pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 );
pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 );
pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 );
//printf( "Adding node %d for data %d\n", pData->pFunc->Id, pObj->Num );
return pData->pFunc;
}
......
......@@ -48,7 +48,7 @@ Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars )
p->pPars = pPars;
p->pAig = pAig;
// prepare the internal memory manager
p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 512 );
p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 1024 );
// other data
p->vLeavesBest = Vec_PtrAlloc( 4 );
return p;
......@@ -89,18 +89,27 @@ void Dar_ManStop( Dar_Man_t * p )
***********************************************************************/
void Dar_ManPrintStats( Dar_Man_t * p )
{
int i, Gain;
unsigned pCanons[222];
int Gain, i;
extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%). Cut mem = %d Mb\n",
p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed );
printf( "Cuts = %8d. Tried = %8d. Used = %8d. Bad = %5d. Skipped = %5d. Ave = %.2f.\n",
p->nCutsAll, p->nCutsTried, p->nCutsUsed, p->nCutsBad, p->nCutsSkipped,
(float)p->nCutsUsed/Aig_ManNodeNum(p->pAig) );
printf( "Bufs = %5d. BufMax = %5d. BufReplace = %6d. BufFix = %6d.\n",
Aig_ManBufNum(p->pAig), p->pAig->nBufMax, p->pAig->nBufReplaces, p->pAig->nBufFixes );
PRT( "Cuts ", p->timeCuts );
PRT( "Eval ", p->timeEval );
PRT( "Other ", p->timeOther );
PRT( "TOTAL ", p->timeTotal );
/*
if ( !p->pPars->fVeryVerbose )
return;
Dar_LibReturnCanonicals( pCanons );
for ( i = 0; i < 222; i++ )
{
if ( p->ClassGains[i] == 0 && p->ClassTimes[i] == 0 )
......@@ -109,9 +118,9 @@ void Dar_ManPrintStats( Dar_Man_t * p )
printf( "G = %6d (%5.2f %%) ", p->ClassGains[i], Gain? 100.0*p->ClassGains[i]/Gain : 0.0 );
printf( "S = %8d (%5.2f %%) ", p->ClassSubgs[i], p->nTotalSubgs? 100.0*p->ClassSubgs[i]/p->nTotalSubgs : 0.0 );
printf( "R = %7d ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 );
PRTP( "T", p->ClassTimes[i], p->timeEval );
Kit_DsdPrintFromTruth( pCanons + i, 4 );
// PRTP( "T", p->ClassTimes[i], p->timeEval );
}
*/
}
......
/**CFile****************************************************************
FileName [darRefact.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting.]
Synopsis [Refactoring.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: darRefact.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "darInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
/**CFile****************************************************************
FileName [darResub.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: darResub.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "darInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
/**CFile****************************************************************
FileName [darScript.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting.]
Synopsis [Rewriting scripts.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: darScript.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "darInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......@@ -18,7 +18,7 @@
***********************************************************************/
#include "dar.h"
#include "darInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
......
......@@ -4,4 +4,7 @@ SRC += src/aig/dar/darBalance.c \
src/aig/dar/darData.c \
src/aig/dar/darLib.c \
src/aig/dar/darMan.c \
src/aig/dar/darRefact.c \
src/aig/dar/darResub.c \
src/aig/dar/darScript.c \
src/aig/dar/darTruth.c
......@@ -45,7 +45,7 @@ Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
Aig_Man_t * pManAigNew;
int clk;
if ( Aig_ManNodeNum(pManAig) == 0 )
return Aig_ManDup(pManAig);
return Aig_ManDup(pManAig, 1);
clk = clock();
assert( Aig_ManLatchNum(pManAig) == 0 );
p = Fra_ManStart( pManAig, pPars );
......
......@@ -1532,7 +1532,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nCofLevel = 1;
fCofactor = 1;
fCofactor = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nch" ) ) != EOF )
{
......
......@@ -521,14 +521,24 @@ Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVe
***********************************************************************/
Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_Par_t * pPars )
{
Aig_Man_t * pMan;
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
int clk;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk );
if ( pMan == NULL )
return NULL;
// Aig_ManPrintStats( pMan );
Dar_ManRewrite( pMan, pPars );
// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
// Aig_ManStop( pTemp );
clk = clock();
pMan = Aig_ManDup( pTemp = pMan, 0 );
Aig_ManStop( pTemp );
PRT( "time", clock() - clk );
// Aig_ManPrintStats( pMan );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Aig_ManStop( pMan );
......
......@@ -155,7 +155,11 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
}
// put the nodes into the DFS order and reassign their IDs
{
// int clk = clock();
Abc_NtkReassignIds( pNtk );
// PRT( "time", clock() - clk );
}
// Abc_AigCheckFaninOrder( pNtk->pManFunc );
// fix the levels
if ( fUpdateLevel )
......
......@@ -811,7 +811,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
pTemp->fMarkA = 0;
assert( Abc_ObjLevel(pTemp) == Lev );
Abc_ObjSetLevel( pTemp, Abc_ObjLevelNew(pTemp) );
// if the level did not change, to need to check the fanout levels
// if the level did not change, no need to check the fanout levels
if ( Abc_ObjLevel(pTemp) == Lev )
continue;
// schedule fanout for level update
......@@ -858,7 +858,7 @@ void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
LevelOld = Abc_ObjReverseLevel(pTemp);
assert( LevelOld == Lev );
Abc_ObjSetReverseLevel( pTemp, Abc_ObjReverseLevelNew(pTemp) );
// if the level did not change, to need to check the fanout levels
// if the level did not change, no need to check the fanout levels
if ( Abc_ObjReverseLevel(pTemp) == Lev )
continue;
// schedule fanins for level update
......
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