diff options
Diffstat (limited to 'src/temp')
33 files changed, 2546 insertions, 1530 deletions
diff --git a/src/temp/esop/esopUtil.c b/src/temp/esop/esopUtil.c index dec6eae2..7230cc87 100644 --- a/src/temp/esop/esopUtil.c +++ b/src/temp/esop/esopUtil.c @@ -134,7 +134,7 @@ void Esop_CoverWriteFile( Esop_Cube_t * pCover, char * pName, int fEsop ) if ( Buffer[i] == '<' || Buffer[i] == '>' ) Buffer[i] = '_'; pFile = fopen( Buffer, "w" ); - fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() ); + fprintf( pFile, "# %s cover for output %s generated by ABC\n", fEsop? "ESOP":"SOP", pName ); fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 ); fprintf( pFile, ".o %d\n", 1 ); fprintf( pFile, ".p %d\n", Esop_CoverCountCubes(pCover) ); diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h index 57d8cfd2..8c5f130b 100644 --- a/src/temp/ivy/ivy.h +++ b/src/temp/ivy/ivy.h @@ -44,23 +44,17 @@ typedef struct Ivy_Man_t_ Ivy_Man_t; typedef struct Ivy_Obj_t_ Ivy_Obj_t; typedef int Ivy_Edge_t; -// constant edges -#define IVY_CONST0 1 -#define IVY_CONST1 0 - // object types typedef enum { - IVY_NONE, // 0: unused node + IVY_NONE, // 0: non-existant object IVY_PI, // 1: primary input (and constant 1 node) IVY_PO, // 2: primary output IVY_ASSERT, // 3: assertion IVY_LATCH, // 4: sequential element - IVY_AND, // 5: internal AND node - IVY_EXOR, // 6: internal EXOR node - IVY_BUF, // 7: internal buffer (temporary) - IVY_ANDM, // 8: multi-input AND (logic network only) - IVY_EXORM, // 9: multi-input EXOR (logic network only) - IVY_LUT // 10: multi-input LUT (logic network only) + IVY_AND, // 5: AND node + IVY_EXOR, // 6: EXOR node + IVY_BUF, // 7: buffer (temporary) + IVY_VOID // 8: unused object } Ivy_Type_t; // latch initial values @@ -72,56 +66,51 @@ typedef enum { } Ivy_Init_t; // the AIG node -struct Ivy_Obj_t_ // 6 words +struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit) { int Id; // integer ID int TravId; // traversal ID - int Fanin0; // fanin ID - int Fanin1; // fanin ID - int nRefs; // reference counter unsigned Type : 4; // object type unsigned fPhase : 1; // value under 000...0 pattern unsigned fMarkA : 1; // multipurpose mask unsigned fMarkB : 1; // multipurpose mask unsigned fExFan : 1; // set to 1 if last fanout added is EXOR - unsigned fComp0 : 1; // complemented attribute - unsigned fComp1 : 1; // complemented attribute unsigned Init : 2; // latch initial value - unsigned LevelR : 8; // reverse logic level - unsigned Level : 12; // logic level + unsigned Level : 22; // logic level + int nRefs; // reference counter + Ivy_Obj_t * pFanin0; // fanin + Ivy_Obj_t * pFanin1; // fanin }; // the AIG manager struct Ivy_Man_t_ { // AIG nodes - int nObjs[12]; // the number of objects by type + Vec_Ptr_t * vPis; // the array of PIs + Vec_Ptr_t * vPos; // the array of POs + Vec_Ptr_t * vBufs; // the array of buffers + Vec_Ptr_t * vObjs; // the array of objects + Ivy_Obj_t * pConst1; // the constant 1 node + Ivy_Obj_t Ghost; // the ghost node + // AIG node counters + int nObjs[IVY_VOID];// the number of objects by type int nCreated; // the number of created objects int nDeleted; // the number of deleted objects - int ObjIdNext; // the next free obj ID to assign - int nObjsAlloc; // the allocated number of nodes - Ivy_Obj_t * pObjs; // the array of all nodes - Vec_Int_t * vPis; // the array of PIs - Vec_Int_t * vPos; // the array of POs // stuctural hash table int * pTable; // structural hash table int nTableSize; // structural hash table size // various data members int fCatchExor; // set to 1 to detect EXORs - int fExtended; // set to 1 in extended mode int nTravIds; // the traversal ID int nLevelMax; // the maximum level - void * pData; // the temporary data Vec_Int_t * vRequired; // required times - // truth table of the 8-LUTs - unsigned * pMemory; // memory for truth tables - Vec_Int_t * vTruths; // offset for truth table of each node - // storage for the undo operation - Vec_Int_t * vFree; // storage for all deleted entries - Ivy_Obj_t * pUndos; // description of recently deleted nodes - int nUndos; // the number of recently deleted nodes - int nUndosAlloc; // the number of allocated cells - int fRecording; // shows that recording goes on + Vec_Ptr_t * vFanouts; // representation of the fanouts + void * pData; // the temporary data + void * pCopy; // the temporary data + // memory management + Vec_Ptr_t * vChunks; // allocated memory pieces + Vec_Ptr_t * vPages; // memory pages used by nodes + Ivy_Obj_t * pListFree; // the list of free nodes }; @@ -141,7 +130,9 @@ typedef struct Ivy_Store_t_ Ivy_Store_t; struct Ivy_Store_t_ { int nCuts; + int nCutsM; int nCutsMax; + int fSatur; Ivy_Cut_t pCuts[IVY_CUT_LIMIT]; // storage for cuts }; @@ -149,35 +140,33 @@ struct Ivy_Store_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#define IVY_SANDBOX_SIZE 1 - #define IVY_MIN(a,b) (((a) < (b))? (a) : (b)) #define IVY_MAX(a,b) (((a) > (b))? (a) : (b)) -static inline int Ivy_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } -static inline int Ivy_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } -static inline int Ivy_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } -static inline void Ivy_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } -static inline void Ivy_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } - -static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) & ~01); } -static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) ^ 01); } -static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned)(p) ^ (c)); } -static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int )(((unsigned)p) & 01); } - -static inline Ivy_Obj_t * Ivy_ManConst0( Ivy_Man_t * p ) { return Ivy_Not(p->pObjs); } -static inline Ivy_Obj_t * Ivy_ManConst1( Ivy_Man_t * p ) { return p->pObjs; } -static inline Ivy_Obj_t * Ivy_ManGhost( Ivy_Man_t * p ) { return p->pObjs - IVY_SANDBOX_SIZE; } -static inline Ivy_Obj_t * Ivy_ManPi( Ivy_Man_t * p, int i ) { return p->pObjs + Vec_IntEntry(p->vPis,i); } -static inline Ivy_Obj_t * Ivy_ManPo( Ivy_Man_t * p, int i ) { return p->pObjs + Vec_IntEntry(p->vPos,i); } -static inline Ivy_Obj_t * Ivy_ManObj( Ivy_Man_t * p, int i ) { return p->pObjs + i; } - -static inline Ivy_Edge_t Ivy_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; } -static inline int Ivy_EdgeId( Ivy_Edge_t Edge ) { return Edge >> 1; } -static inline int Ivy_EdgeIsComplement( Ivy_Edge_t Edge ) { return Edge & 1; } -static inline Ivy_Edge_t Ivy_EdgeRegular( Ivy_Edge_t Edge ) { return (Edge >> 1) << 1; } -static inline Ivy_Edge_t Ivy_EdgeNot( Ivy_Edge_t Edge ) { return Edge ^ 1; } -static inline Ivy_Edge_t Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond ) { return Edge ^ fCond; } +static inline int Ivy_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } +static inline int Ivy_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } +static inline int Ivy_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } +static inline void Ivy_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } +static inline void Ivy_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } + +static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) & ~01); } +static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) ^ 01); } +static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned)(p) ^ (c)); } +static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int )(((unsigned)p) & 01); } + +static inline Ivy_Obj_t * Ivy_ManConst0( Ivy_Man_t * p ) { return Ivy_Not(p->pConst1); } +static inline Ivy_Obj_t * Ivy_ManConst1( Ivy_Man_t * p ) { return p->pConst1; } +static inline Ivy_Obj_t * Ivy_ManGhost( Ivy_Man_t * p ) { return &p->Ghost; } +static inline Ivy_Obj_t * Ivy_ManPi( Ivy_Man_t * p, int i ) { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPis, i); } +static inline Ivy_Obj_t * Ivy_ManPo( Ivy_Man_t * p, int i ) { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPos, i); } +static inline Ivy_Obj_t * Ivy_ManObj( Ivy_Man_t * p, int i ) { return (Ivy_Obj_t *)Vec_PtrEntry(p->vObjs, i); } + +static inline Ivy_Edge_t Ivy_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; } +static inline int Ivy_EdgeId( Ivy_Edge_t Edge ) { return Edge >> 1; } +static inline int Ivy_EdgeIsComplement( Ivy_Edge_t Edge ) { return Edge & 1; } +static inline Ivy_Edge_t Ivy_EdgeRegular( Ivy_Edge_t Edge ) { return (Edge >> 1) << 1; } +static inline Ivy_Edge_t Ivy_EdgeNot( Ivy_Edge_t Edge ) { return Edge ^ 1; } +static inline Ivy_Edge_t Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond ) { return Edge ^ fCond; } static inline Ivy_Edge_t Ivy_EdgeFromNode( Ivy_Obj_t * pNode ) { return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) ); } static inline Ivy_Obj_t * Ivy_EdgeToNode( Ivy_Man_t * p, Ivy_Edge_t Edge ){ return Ivy_NotCond( Ivy_ManObj(p, Ivy_EdgeId(Edge)), Ivy_EdgeIsComplement(Edge) ); } @@ -192,13 +181,9 @@ static inline int Ivy_ManLatchNum( Ivy_Man_t * p ) { return p->nO static inline int Ivy_ManAndNum( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]; } static inline int Ivy_ManExorNum( Ivy_Man_t * p ) { return p->nObjs[IVY_EXOR]; } static inline int Ivy_ManBufNum( Ivy_Man_t * p ) { return p->nObjs[IVY_BUF]; } -static inline int Ivy_ManAndMultiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_ANDM]; } -static inline int Ivy_ManExorMultiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_EXORM]; } -static inline int Ivy_ManLutNum( Ivy_Man_t * p ) { return p->nObjs[IVY_LUT]; } static inline int Ivy_ManObjNum( Ivy_Man_t * p ) { return p->nCreated - p->nDeleted; } -static inline int Ivy_ManObjIdNext( Ivy_Man_t * p ) { return p->ObjIdNext; } -static inline int Ivy_ManObjAllocNum( Ivy_Man_t * p ) { return p->nObjsAlloc; } -static inline int Ivy_ManNodeNum( Ivy_Man_t * p ) { return p->fExtended? p->nObjs[IVY_ANDM]+p->nObjs[IVY_EXORM]+p->nObjs[IVY_LUT] : p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]; } +static inline int Ivy_ManObjIdMax( Ivy_Man_t * p ) { return Vec_PtrSize(p->vObjs)-1; } +static inline int Ivy_ManNodeNum( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR];} static inline int Ivy_ManHashObjNum( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]+p->nObjs[IVY_LATCH]; } static inline int Ivy_ManGetCost( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]+3*p->nObjs[IVY_EXOR]+8*p->nObjs[IVY_LATCH]; } @@ -221,27 +206,15 @@ static inline int Ivy_ObjIsTerm( Ivy_Obj_t * pObj ) { assert( !Ivy static inline int Ivy_ObjIsHash( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; } static inline int Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; } -static inline int Ivy_ObjIsAndMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_ANDM; } -static inline int Ivy_ObjIsExorMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXORM; } -static inline int Ivy_ObjIsLut( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_LUT; } -static inline int Ivy_ObjIsNodeExt( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type >= IVY_ANDM; } - static inline int Ivy_ObjIsMarkA( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fMarkA; } static inline void Ivy_ObjSetMarkA( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 1; } static inline void Ivy_ObjClearMarkA( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 0; } - -static inline Ivy_Man_t * Ivy_ObjMan( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return *((Ivy_Man_t **)(pObj - pObj->Id - IVY_SANDBOX_SIZE - 1)); } -static inline Ivy_Obj_t * Ivy_ObjConst0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_Not(pObj - pObj->Id); } -static inline Ivy_Obj_t * Ivy_ObjConst1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id; } -static inline Ivy_Obj_t * Ivy_ObjGhost( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id - IVY_SANDBOX_SIZE; } -static inline Ivy_Obj_t * Ivy_ObjObj( Ivy_Obj_t * pObj, int n ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id + n; } -static inline Ivy_Obj_t * Ivy_ObjNext( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id + pObj->TravId; } static inline void Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = TravId; } -static inline void Ivy_ObjSetTravIdCurrent( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = Ivy_ObjMan(pObj)->nTravIds; } -static inline void Ivy_ObjSetTravIdPrevious( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = Ivy_ObjMan(pObj)->nTravIds - 1; } -static inline int Ivy_ObjIsTravIdCurrent( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == Ivy_ObjMan(pObj)->nTravIds); } -static inline int Ivy_ObjIsTravIdPrevious( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == Ivy_ObjMan(pObj)->nTravIds - 1); } +static inline void Ivy_ObjSetTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = p->nTravIds; } +static inline void Ivy_ObjSetTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = p->nTravIds - 1; } +static inline int Ivy_ObjIsTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == p->nTravIds); } +static inline int Ivy_ObjIsTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == p->nTravIds - 1); } static inline int Ivy_ObjId( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Id; } static inline int Ivy_ObjPhase( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fPhase; } @@ -249,69 +222,53 @@ static inline int Ivy_ObjExorFanout( Ivy_Obj_t * pObj ) { assert( !Ivy static inline int Ivy_ObjRefs( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->nRefs; } static inline void Ivy_ObjRefsInc( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->nRefs++; } static inline void Ivy_ObjRefsDec( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); assert( pObj->nRefs > 0 ); pObj->nRefs--; } -static inline int Ivy_ObjFaninId0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Fanin0; } -static inline int Ivy_ObjFaninId1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Fanin1; } -static inline int Ivy_ObjFaninC0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fComp0; } -static inline int Ivy_ObjFaninC1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fComp1; } -static inline Ivy_Obj_t * Ivy_ObjFanin0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjObj(pObj, pObj->Fanin0); } -static inline Ivy_Obj_t * Ivy_ObjFanin1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjObj(pObj, pObj->Fanin1); } -static inline Ivy_Obj_t * Ivy_ObjChild0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin0(pObj), Ivy_ObjFaninC0(pObj) ); } -static inline Ivy_Obj_t * Ivy_ObjChild1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin1(pObj), Ivy_ObjFaninC1(pObj) ); } -static inline int Ivy_ObjLevelR( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->LevelR; } +static inline int Ivy_ObjFaninId0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; } +static inline int Ivy_ObjFaninId1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; } +static inline int Ivy_ObjFaninC0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_IsComplement(pObj->pFanin0); } +static inline int Ivy_ObjFaninC1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_IsComplement(pObj->pFanin1); } +static inline Ivy_Obj_t * Ivy_ObjFanin0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_Regular(pObj->pFanin0); } +static inline Ivy_Obj_t * Ivy_ObjFanin1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_Regular(pObj->pFanin1); } +static inline Ivy_Obj_t * Ivy_ObjChild0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin0; } +static inline Ivy_Obj_t * Ivy_ObjChild1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin1; } static inline int Ivy_ObjLevel( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Level; } static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); } -static inline void Ivy_ObjClean( Ivy_Obj_t * pObj ) { +static inline void Ivy_ObjClean( Ivy_Obj_t * pObj ) +{ int IdSaved = pObj->Id; memset( pObj, 0, sizeof(Ivy_Obj_t) ); pObj->Id = IdSaved; } -static inline void Ivy_ObjOverwrite( Ivy_Obj_t * pBase, Ivy_Obj_t * pData ) { int IdSaved = pBase->Id; memcpy( pBase, pData, sizeof(Ivy_Obj_t) ); pBase->Id = IdSaved; } +static inline void Ivy_ObjOverwrite( Ivy_Obj_t * pBase, Ivy_Obj_t * pData ) +{ + int IdSaved = pBase->Id; + memcpy( pBase, pData, sizeof(Ivy_Obj_t) ); + pBase->Id = IdSaved; +} static inline int Ivy_ObjWhatFanin( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin ) { - if ( Ivy_ObjFaninId0(pObj) == Ivy_ObjId(pFanin) ) return 0; - if ( Ivy_ObjFaninId1(pObj) == Ivy_ObjId(pFanin) ) return 1; + if ( Ivy_ObjFanin0(pObj) == pFanin ) return 0; + if ( Ivy_ObjFanin1(pObj) == pFanin ) return 1; assert(0); return -1; } static inline int Ivy_ObjFanoutC( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) { - if ( Ivy_ObjFaninId0(pFanout) == Ivy_ObjId(pObj) ) return Ivy_ObjFaninC0(pObj); - if ( Ivy_ObjFaninId1(pFanout) == Ivy_ObjId(pObj) ) return Ivy_ObjFaninC1(pObj); + if ( Ivy_ObjFanin0(pFanout) == pObj ) return Ivy_ObjFaninC0(pObj); + if ( Ivy_ObjFanin1(pFanout) == pObj ) return Ivy_ObjFaninC1(pObj); assert(0); return -1; } // create the ghost of the new node -static inline Ivy_Obj_t * Ivy_ObjCreateGhost( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init ) +static inline Ivy_Obj_t * Ivy_ObjCreateGhost( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init ) { - Ivy_Obj_t * pGhost; - int Temp; - pGhost = Ivy_ObjGhost(Ivy_Regular(p0)); + Ivy_Obj_t * pGhost, * pTemp; + pGhost = Ivy_ManGhost(p); pGhost->Type = Type; pGhost->Init = Init; - pGhost->fComp0 = Ivy_IsComplement(p0); - pGhost->fComp1 = Ivy_IsComplement(p1); - pGhost->Fanin0 = Ivy_ObjId(Ivy_Regular(p0)); - pGhost->Fanin1 = Ivy_ObjId(Ivy_Regular(p1)); - if ( pGhost->Fanin0 < pGhost->Fanin1 ) - { - Temp = pGhost->Fanin0, pGhost->Fanin0 = pGhost->Fanin1, pGhost->Fanin1 = Temp; - Temp = pGhost->fComp0, pGhost->fComp0 = pGhost->fComp1, pGhost->fComp1 = Temp; - } - assert( Ivy_ObjIsOneFanin(pGhost) || pGhost->Fanin0 > pGhost->Fanin1 ); - return pGhost; -} - -// create the ghost of the new node -static inline Ivy_Obj_t * Ivy_ObjCreateGhost2( Ivy_Man_t * p, Ivy_Obj_t * pObjDead ) -{ - Ivy_Obj_t * pGhost; - pGhost = Ivy_ManGhost(p); - pGhost->Type = pObjDead->Type; - pGhost->Init = pObjDead->Init; - pGhost->fComp0 = pObjDead->fComp0; - pGhost->fComp1 = pObjDead->fComp1; - pGhost->Fanin0 = pObjDead->Fanin0; - pGhost->Fanin1 = pObjDead->Fanin1; - assert( Ivy_ObjIsOneFanin(pGhost) || pGhost->Fanin0 > pGhost->Fanin1 ); + pGhost->pFanin0 = p0; + pGhost->pFanin1 = p1; + assert( Type == IVY_PI || Ivy_ObjFanin0(pGhost) != Ivy_ObjFanin1(pGhost) ); + if ( p1 && Ivy_ObjFaninId0(pGhost) > Ivy_ObjFaninId1(pGhost) ) + pTemp = pGhost->pFanin0, pGhost->pFanin0 = pGhost->pFanin1, pGhost->pFanin1 = pTemp; return pGhost; } @@ -352,48 +309,58 @@ static Ivy_Init_t Ivy_InitExor( Ivy_Init_t InitA, Ivy_Init_t InitB ) return IVY_INIT_0; } -// extended fanins -static inline Vec_Int_t * Ivy_ObjGetFanins( Ivy_Obj_t * pObj ) { assert(Ivy_ObjMan(pObj)->fExtended); return (Vec_Int_t *)*(((int*)pObj)+2); } -static inline void Ivy_ObjSetFanins( Ivy_Obj_t * pObj, Vec_Int_t * vFanins ) { assert(Ivy_ObjMan(pObj)->fExtended); assert(Ivy_ObjGetFanins(pObj)==NULL); *(Vec_Int_t **)(((int*)pObj)+2) = vFanins; } -static inline void Ivy_ObjStartFanins( Ivy_Obj_t * pObj, int nFanins ) { assert(Ivy_ObjMan(pObj)->fExtended); Ivy_ObjSetFanins( pObj, Vec_IntAlloc(nFanins) ); } -static inline void Ivy_ObjAddFanin( Ivy_Obj_t * pObj, int Fanin ) { assert(Ivy_ObjMan(pObj)->fExtended); Vec_IntPush( Ivy_ObjGetFanins(pObj), Fanin ); } -static inline int Ivy_ObjReadFanin( Ivy_Obj_t * pObj, int i ) { assert(Ivy_ObjMan(pObj)->fExtended); return Vec_IntEntry( Ivy_ObjGetFanins(pObj), i ); } -static inline int Ivy_ObjFaninNum( Ivy_Obj_t * pObj ) { assert(Ivy_ObjMan(pObj)->fExtended); return Vec_IntSize( Ivy_ObjGetFanins(pObj) ); } +// internal memory manager +static inline Ivy_Obj_t * Ivy_ManFetchMemory( Ivy_Man_t * p ) +{ + extern void Ivy_ManAddMemory( Ivy_Man_t * p ); + Ivy_Obj_t * pTemp; + if ( p->pListFree == NULL ) + Ivy_ManAddMemory( p ); + pTemp = p->pListFree; + p->pListFree = *((Ivy_Obj_t **)pTemp); + memset( pTemp, 0, sizeof(Ivy_Obj_t) ); + return pTemp; +} +static inline void Ivy_ManRecycleMemory( Ivy_Man_t * p, Ivy_Obj_t * pEntry ) +{ + pEntry->Type = IVY_NONE; // distinquishes dead node from live node + *((Ivy_Obj_t **)pEntry) = p->pListFree; + p->pListFree = pEntry; +} + //////////////////////////////////////////////////////////////////////// /// ITERATORS /// //////////////////////////////////////////////////////////////////////// -// iterator over all objects, including those currently not used -#define Ivy_ManForEachObj( p, pObj, i ) \ - for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ ) -#define Ivy_ManForEachObjReverse( p, pObj, i ) \ - for ( i = p->ObjIdNext - 1, pObj = p->pObjs + i; i >= 0; i--, pObj-- ) // iterator over the primary inputs -#define Ivy_ManForEachPi( p, pObj, i ) \ - for ( i = 0; i < Vec_IntSize(p->vPis) && ((pObj) = Ivy_ManPi(p, i)); i++ ) +#define Ivy_ManForEachPi( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vPis, pObj, i ) // iterator over the primary outputs -#define Ivy_ManForEachPo( p, pObj, i ) \ - for ( i = 0; i < Vec_IntSize(p->vPos) && ((pObj) = Ivy_ManPo(p, i)); i++ ) +#define Ivy_ManForEachPo( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vPos, pObj, i ) +// iterator over all objects, including those currently not used +#define Ivy_ManForEachObj( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else // iterator over the combinational inputs -#define Ivy_ManForEachCi( p, pObj, i ) \ - for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ ) \ - if ( !Ivy_ObjIsCi(pObj) ) {} else +#define Ivy_ManForEachCi( p, pObj, i ) \ + Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCi(pObj) ) {} else // iterator over the combinational outputs -#define Ivy_ManForEachCo( p, pObj, i ) \ - for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ ) \ - if ( !Ivy_ObjIsCo(pObj) ) {} else +#define Ivy_ManForEachCo( p, pObj, i ) \ + Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCo(pObj) ) {} else // iterator over logic nodes (AND and EXOR gates) -#define Ivy_ManForEachNode( p, pObj, i ) \ - for ( i = 1, pObj = p->pObjs+i; i < p->ObjIdNext; i++, pObj++ ) \ - if ( !Ivy_ObjIsNode(pObj) ) {} else +#define Ivy_ManForEachNode( p, pObj, i ) \ + Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsNode(pObj) ) {} else // iterator over logic latches -#define Ivy_ManForEachLatch( p, pObj, i ) \ - for ( i = 1, pObj = p->pObjs+i; i < p->ObjIdNext; i++, pObj++ ) \ - if ( !Ivy_ObjIsLatch(pObj) ) {} else +#define Ivy_ManForEachLatch( p, pObj, i ) \ + Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsLatch(pObj) ) {} else // iterator over the nodes whose IDs are stored in the array -#define Ivy_ManForEachNodeVec( p, vIds, pObj, i ) \ +#define Ivy_ManForEachNodeVec( p, vIds, pObj, i ) \ for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Ivy_ManObj(p, Vec_IntEntry(vIds,i))); i++ ) +// iterator over the fanouts of an object +#define Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, i ) \ + for ( i = 0, Ivy_ObjCollectFanouts(p, pObj, vArray); \ + i < Vec_PtrSize(vArray) && ((pFanout) = Vec_PtrEntry(vArray,i)); i++ ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// @@ -401,19 +368,19 @@ static inline int Ivy_ObjFaninNum( Ivy_Obj_t * pObj ) /*=== ivyBalance.c ========================================================*/ extern Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ); -extern Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel ); +extern Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Ivy_Man_t * p, Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel ); /*=== ivyCanon.c ========================================================*/ -extern Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); -extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); -extern Ivy_Obj_t * Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init ); +extern Ivy_Obj_t * Ivy_CanonAnd( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +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 ); /*=== ivyCut.c ==========================================================*/ -extern void Ivy_ManSeqFindCut( Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize ); -extern Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves ); +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 ); /*=== ivyDfs.c ==========================================================*/ extern Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p ); -extern Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p ); +extern Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches ); extern void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone ); extern Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p ); extern Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p ); @@ -423,61 +390,76 @@ extern void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree ); extern unsigned Ivy_TruthDsdCompute( Vec_Int_t * vTree ); extern void Ivy_TruthDsdComputePrint( unsigned uTruth ); extern Ivy_Obj_t * Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree ); +/*=== ivyFanout.c ==========================================================*/ +extern void Ivy_ManStartFanout( Ivy_Man_t * p ); +extern void Ivy_ManStopFanout( Ivy_Man_t * p ); +extern void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ); +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 ); /*=== ivyMan.c ==========================================================*/ -extern Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax ); +extern Ivy_Man_t * Ivy_ManStart(); extern void Ivy_ManStop( Ivy_Man_t * p ); -extern void Ivy_ManGrow( Ivy_Man_t * p ); extern int Ivy_ManCleanup( Ivy_Man_t * p ); +extern int Ivy_ManPropagateBuffers( Ivy_Man_t * p ); extern void Ivy_ManPrintStats( Ivy_Man_t * p ); +extern void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits ); +/*=== ivyMem.c ==========================================================*/ +extern void Ivy_ManStartMemory( Ivy_Man_t * p ); +extern void Ivy_ManStopMemory( Ivy_Man_t * p ); /*=== ivyMulti.c ==========================================================*/ -extern Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); -extern Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); -extern Ivy_Obj_t * Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ); -extern Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); -extern int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSol ); +extern Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_Multi1( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +extern int Ivy_MultiPlus( Ivy_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSol ); /*=== ivyObj.c ==========================================================*/ -extern Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost ); -extern Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type ); -extern void Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin ); -extern void Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop ); -extern void Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop ); -extern void Ivy_ObjReplace( Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop ); -extern void Ivy_NodeFixBufferFanins( Ivy_Obj_t * pNode ); +extern Ivy_Obj_t * Ivy_ObjCreatePi( Ivy_Man_t * p ); +extern Ivy_Obj_t * Ivy_ObjCreatePo( Ivy_Man_t * p, Ivy_Obj_t * pDriver ); +extern Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost ); +extern void Ivy_ObjConnect( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFan0, Ivy_Obj_t * pFan1 ); +extern void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj ); +extern void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew ); +extern void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ); +extern void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ); +extern void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop ); +extern void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode ); /*=== ivyOper.c =========================================================*/ -extern Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ); -extern Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); -extern Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); -extern Ivy_Obj_t * Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); -extern Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 ); -extern Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC ); -extern Ivy_Obj_t * Ivy_Miter( Vec_Ptr_t * vPairs ); +extern Ivy_Obj_t * Ivy_Oper( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_And( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_Or( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_Exor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_Mux( Ivy_Man_t * p, Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 ); +extern Ivy_Obj_t * Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC ); +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_ManResyn( Ivy_Man_t * p, int fUpdateLevel ); +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 ); extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); extern int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose ); /*=== ivyTable.c ========================================================*/ -extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj ); -extern void Ivy_TableInsert( Ivy_Obj_t * pObj ); -extern void Ivy_TableDelete( Ivy_Obj_t * pObj ); -extern void Ivy_TableUpdate( Ivy_Obj_t * pObj, int ObjIdNew ); +extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj ); +extern void Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj ); +extern void Ivy_TableDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj ); +extern void Ivy_TableUpdate( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ObjIdNew ); extern int Ivy_TableCountEntries( Ivy_Man_t * p ); -extern void Ivy_TableResize( Ivy_Man_t * p ); -/*=== ivyUndo.c =========================================================*/ -extern void Ivy_ManUndoStart( Ivy_Man_t * p ); -extern void Ivy_ManUndoStop( Ivy_Man_t * p ); -extern void Ivy_ManUndoRecord( Ivy_Man_t * p, Ivy_Obj_t * pObj ); -extern void Ivy_ManUndoPerform( Ivy_Man_t * p, Ivy_Obj_t * pRoot ); +extern void Ivy_TableProfile( Ivy_Man_t * p ); /*=== ivyUtil.c =========================================================*/ extern void Ivy_ManIncrementTravId( Ivy_Man_t * p ); extern void Ivy_ManCleanTravId( Ivy_Man_t * p ); +extern unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ); +extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ); +extern int Ivy_ManLevels( Ivy_Man_t * p ); +extern void Ivy_ManResetLevels( Ivy_Man_t * p ); +extern void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj ); +extern void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew ); extern int Ivy_ObjIsMuxType( Ivy_Obj_t * pObj ); extern Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObjT, Ivy_Obj_t ** ppObjE ); -extern unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ); -extern Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin ); -extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ); -extern int Ivy_ManReadLevels( Ivy_Man_t * p ); extern Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj ); #ifdef __cplusplus diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c index 2e230ed2..0303485a 100644 --- a/src/temp/ivy/ivyBalance.c +++ b/src/temp/ivy/ivyBalance.c @@ -27,7 +27,7 @@ static int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel ); static Vec_Ptr_t * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level ); static int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ); -static void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor ); +static void Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor ); static void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj ); //////////////////////////////////////////////////////////////////////// @@ -54,11 +54,11 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ) // clean the old manager Ivy_ManCleanTravId( p ); // create the new manager - pNew = Ivy_ManStart( Ivy_ManPiNum(p), Ivy_ManPoNum(p), Ivy_ManNodeNum(p) + 20000 ); + pNew = Ivy_ManStart(); // map the nodes Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) ); Ivy_ManForEachPi( p, pObj, i ) - pObj->TravId = Ivy_EdgeFromNode( Ivy_ManPi(pNew, i) ); + pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) ); // balance the AIG vStore = Vec_VecAlloc( 50 ); Ivy_ManForEachPo( p, pObj, i ) @@ -66,7 +66,7 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ) pDriver = Ivy_ObjReal( Ivy_ObjChild0(pObj) ); NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(pDriver), vStore, 0, fUpdateLevel ); NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(pDriver) ); - Ivy_ObjConnect( Ivy_ManPo(pNew, i), Ivy_EdgeToNode(pNew, NewNodeId) ); + Ivy_ObjCreatePo( pNew, Ivy_EdgeToNode(pNew, NewNodeId) ); } Vec_VecFree( vStore ); if ( i = Ivy_ManCleanup( pNew ) ) @@ -139,11 +139,12 @@ int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Vec_Vec_t * vSto vSuper->pArray[i] = Ivy_EdgeToNode( pNew, NewNodeId ); } // build the supergate - pObjNew = Ivy_NodeBalanceBuildSuper( vSuper, Ivy_ObjType(pObjOld), fUpdateLevel ); + pObjNew = Ivy_NodeBalanceBuildSuper( pNew, vSuper, Ivy_ObjType(pObjOld), fUpdateLevel ); vSuper->nSize = 0; // make sure the balanced node is not assigned assert( pObjOld->TravId == 0 ); pObjOld->TravId = Ivy_EdgeFromNode( pObjNew ); +// assert( pObjOld->Level >= Ivy_Regular(pObjNew)->Level ); return pObjOld->TravId; } @@ -158,7 +159,7 @@ int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Vec_Vec_t * vSto SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel ) +Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Ivy_Man_t * p, Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel ) { Ivy_Obj_t * pObj1, * pObj2; int LeftBound; @@ -171,11 +172,11 @@ Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int // find the left bound on the node to be paired LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vSuper ); // find the node that can be shared (if no such node, randomize choice) - Ivy_NodeBalancePermute( vSuper, LeftBound, Type == IVY_EXOR ); + Ivy_NodeBalancePermute( p, vSuper, LeftBound, Type == IVY_EXOR ); // pull out the last two nodes pObj1 = Vec_PtrPop(vSuper); pObj2 = Vec_PtrPop(vSuper); - Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(pObj1, pObj2, Type) ); + Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(p, pObj1, pObj2, Type) ); } return Vec_PtrEntry(vSuper, 0); } @@ -314,7 +315,7 @@ int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ) SeeAlso [] ***********************************************************************/ -void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor ) +void Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor ) { Ivy_Obj_t * pObj1, * pObj2, * pObj3, * pGhost; int RightBound, i; @@ -330,8 +331,8 @@ void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor ) for ( i = RightBound; i >= LeftBound; i-- ) { pObj3 = Vec_PtrEntry( vSuper, i ); - pGhost = Ivy_ObjCreateGhost( pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE ); - if ( Ivy_TableLookup( pGhost ) ) + pGhost = Ivy_ObjCreateGhost( p, pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE ); + if ( Ivy_TableLookup( p, pGhost ) ) { if ( pObj3 == pObj2 ) return; diff --git a/src/temp/ivy/ivyCanon.c b/src/temp/ivy/ivyCanon.c index c6f43d15..5768b87e 100644 --- a/src/temp/ivy/ivyCanon.c +++ b/src/temp/ivy/ivyCanon.c @@ -24,7 +24,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int fCompl0, int fCompl1, Ivy_Type_t Type ); +static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int fCompl0, int fCompl1, Ivy_Type_t Type ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -41,7 +41,7 @@ static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost ) +Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Man_t * p, Ivy_Obj_t * pGhost ) { Ivy_Obj_t * pResult, * pLat0, * pLat1; Ivy_Init_t Init, Init0, Init1; @@ -53,9 +53,9 @@ Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost ) // consider the case when the pair is canonical if ( !Ivy_ObjIsLatch(Ivy_ObjFanin0(pGhost)) || !Ivy_ObjIsLatch(Ivy_ObjFanin1(pGhost)) ) { - if ( pResult = Ivy_TableLookup( pGhost ) ) + if ( pResult = Ivy_TableLookup( p, pGhost ) ) return pResult; - return Ivy_ObjCreate( pGhost ); + return Ivy_ObjCreate( p, pGhost ); } /// remember the latches pLat0 = Ivy_ObjFanin0(pGhost); @@ -64,16 +64,13 @@ Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost ) Type = Ivy_ObjType(pGhost); fCompl0 = Ivy_ObjFaninC0(pGhost); fCompl1 = Ivy_ObjFaninC1(pGhost); - // modify the fanins to be latch fanins - pGhost->Fanin0 = Ivy_ObjFaninId0(pLat0); - pGhost->Fanin1 = Ivy_ObjFaninId0(pLat1); // call recursively - pResult = Ivy_CanonPair_rec( pGhost ); + pResult = Ivy_Oper( p, Ivy_NotCond(Ivy_ObjFanin0(pLat0), fCompl0), Ivy_NotCond(Ivy_ObjFanin0(pLat1), fCompl1), Type ); // build latch on top of this Init0 = Ivy_InitNotCond( Ivy_ObjInit(pLat0), fCompl0 ); Init1 = Ivy_InitNotCond( Ivy_ObjInit(pLat1), fCompl1 ); Init = (Type == IVY_AND)? Ivy_InitAnd(Init0, Init1) : Ivy_InitExor(Init0, Init1); - return Ivy_CanonLatch( pResult, Init ); + return Ivy_Latch( p, pResult, Init ); } /**Function************************************************************* @@ -87,11 +84,11 @@ Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) +Ivy_Obj_t * Ivy_CanonAnd( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) { Ivy_Obj_t * pGhost, * pResult; - pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_AND, IVY_INIT_NONE ); - pResult = Ivy_CanonPair_rec( pGhost ); + pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_AND, IVY_INIT_NONE ); + pResult = Ivy_CanonPair_rec( p, pGhost ); return pResult; } @@ -106,14 +103,14 @@ Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) +Ivy_Obj_t * Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) { Ivy_Obj_t * pGhost, * pResult; int fCompl = Ivy_IsComplement(pObj0) ^ Ivy_IsComplement(pObj1); pObj0 = Ivy_Regular(pObj0); pObj1 = Ivy_Regular(pObj1); - pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE ); - pResult = Ivy_CanonPair_rec( pGhost ); + pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE ); + pResult = Ivy_CanonPair_rec( p, pGhost ); return Ivy_NotCond( pResult, fCompl ); } @@ -128,15 +125,15 @@ Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init ) +Ivy_Obj_t * Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init ) { Ivy_Obj_t * pGhost, * pResult; int fCompl = Ivy_IsComplement(pObj); pObj = Ivy_Regular(pObj); - pGhost = Ivy_ObjCreateGhost( pObj, Ivy_ObjConst1(pObj), IVY_LATCH, Ivy_InitNotCond(Init, fCompl) ); - pResult = Ivy_TableLookup( pGhost ); + pGhost = Ivy_ObjCreateGhost( p, pObj, NULL, IVY_LATCH, Ivy_InitNotCond(Init, fCompl) ); + pResult = Ivy_TableLookup( p, pGhost ); if ( pResult == NULL ) - pResult = Ivy_ObjCreate( pGhost ); + pResult = Ivy_ObjCreate( p, pGhost ); return Ivy_NotCond( pResult, fCompl ); } diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c index c39eac12..4331c07e 100644 --- a/src/temp/ivy/ivyCheck.c +++ b/src/temp/ivy/ivyCheck.c @@ -39,15 +39,18 @@ SeeAlso [] ***********************************************************************/ -int Ivy_ManCheck( Ivy_Man_t * pMan ) +int Ivy_ManCheck( Ivy_Man_t * p ) { Ivy_Obj_t * pObj, * pObj2; int i; - Ivy_ManForEachObj( pMan, pObj, i ) + Ivy_ManForEachObj( p, pObj, i ) { // skip deleted nodes - if ( Ivy_ObjIsNone(pObj) ) - continue; + if ( Ivy_ObjId(pObj) != i ) + { + printf( "Ivy_ManCheck: Node with ID %d is listed as number %d in the array of objects.\n", pObj->Id, i ); + return 0; + } // consider the constant node and PIs if ( i == 0 || Ivy_ObjIsPi(pObj) ) { @@ -69,44 +72,54 @@ int Ivy_ManCheck( Ivy_Man_t * pMan ) } if ( Ivy_ObjIsBuf(pObj) ) { + if ( Ivy_ObjFanin1(pObj) ) + { + printf( "Ivy_ManCheck: The buffer with ID \"%d\" contains second fanin.\n", pObj->Id ); + return 0; + } continue; } if ( Ivy_ObjIsLatch(pObj) ) { - if ( Ivy_ObjFaninId1(pObj) != 0 ) + if ( Ivy_ObjFanin1(pObj) ) { printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id ); return 0; } - if ( Ivy_ObjInit(pObj) == 0 ) + if ( Ivy_ObjInit(pObj) == IVY_INIT_NONE ) { printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id ); return 0; } - pObj2 = Ivy_TableLookup( pObj ); + pObj2 = Ivy_TableLookup( p, pObj ); if ( pObj2 != pObj ) printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id ); continue; } // consider the AND node - if ( !Ivy_ObjFaninId0(pObj) || !Ivy_ObjFaninId1(pObj) ) + if ( !Ivy_ObjFanin0(pObj) || !Ivy_ObjFanin1(pObj) ) { - printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a constant fanin.\n", pObj->Id ); + printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a NULL fanin.\n", pObj->Id ); return 0; } - if ( Ivy_ObjFaninId0(pObj) <= Ivy_ObjFaninId1(pObj) ) + if ( Ivy_ObjFaninId0(pObj) >= Ivy_ObjFaninId1(pObj) ) { printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id ); return 0; } // if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) ) -// printf( "Ivy_ManCheck: Node with ID \"%d\" has level that does not agree with the fanin levels.\n", pObj->Id ); - pObj2 = Ivy_TableLookup( pObj ); +// printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) ); + pObj2 = Ivy_TableLookup( p, pObj ); if ( pObj2 != pObj ) printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id ); + 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) ) + 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 - if ( Ivy_TableCountEntries(pMan) != Ivy_ManAndNum(pMan) + Ivy_ManExorNum(pMan) + Ivy_ManLatchNum(pMan) ) + if ( Ivy_TableCountEntries(p) != Ivy_ManAndNum(p) + Ivy_ManExorNum(p) + Ivy_ManLatchNum(p) ) { printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" ); return 0; diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c index 71a3613c..7d1ec63a 100644 --- a/src/temp/ivy/ivyCut.c +++ b/src/temp/ivy/ivyCut.c @@ -175,7 +175,7 @@ printf( "%d", Counter ); SeeAlso [] ***********************************************************************/ -void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize ) +void Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize ) { assert( !Ivy_IsComplement(pRoot) ); assert( Ivy_ObjIsNode(pRoot) ); @@ -194,7 +194,7 @@ void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInsi Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) ); // compute the cut - while ( Ivy_ManSeqFindCut_int( Ivy_ObjMan(pRoot), vFront, vInside, nSize ) ); + while ( Ivy_ManSeqFindCut_int( p, vFront, vInside, nSize ) ); assert( Vec_IntSize(vFront) <= nSize ); } @@ -213,7 +213,7 @@ void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInsi SeeAlso [] ***********************************************************************/ -int Ivy_ManFindBoolCut_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume, Ivy_Obj_t * pPivot ) +int Ivy_ManFindBoolCut_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume, Ivy_Obj_t * pPivot ) { int RetValue0, RetValue1; if ( pObj == pPivot ) @@ -231,15 +231,15 @@ int Ivy_ManFindBoolCut_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * v if ( Ivy_ObjIsBuf(pObj) ) { - RetValue0 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot ); + RetValue0 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot ); if ( !RetValue0 ) return 0; Vec_PtrPushUnique( vVolume, pObj ); return 1; } assert( Ivy_ObjIsNode(pObj) ); - RetValue0 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot ); - RetValue1 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin1(pObj), vLeaves, vVolume, pPivot ); + RetValue0 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot ); + RetValue1 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin1(pObj), vLeaves, vVolume, pPivot ); if ( !RetValue0 && !RetValue1 ) return 0; // add new leaves @@ -296,7 +296,7 @@ int Ivy_ManFindBoolCutCost( Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -int Ivy_ManFindBoolCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolume, Vec_Ptr_t * vLeaves ) +int Ivy_ManFindBoolCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolume, Vec_Ptr_t * vLeaves ) { Ivy_Obj_t * pObj, * pFaninC, * pFanin0, * pFanin1, * pPivot; int RetValue, LevelLimit, Lev, k; @@ -405,7 +405,7 @@ int Ivy_ManFindBoolCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolu // cut exists, collect all the nodes on the shortest path to the pivot Vec_PtrClear( vLeaves ); Vec_PtrClear( vVolume ); - RetValue = Ivy_ManFindBoolCut_rec( pRoot, vLeaves, vVolume, pPivot ); + RetValue = Ivy_ManFindBoolCut_rec( p, pRoot, vLeaves, vVolume, pPivot ); assert( RetValue == 1 ); // unmark the nodes on the frontier (including the pivot) Vec_PtrForEachEntry( vFront, pObj, k ) @@ -481,7 +481,7 @@ void Ivy_ManTestCutsBool( Ivy_Man_t * p ) } if ( Ivy_ObjIsExor(pObj) ) printf( "x" ); - RetValue = Ivy_ManFindBoolCut( pObj, vFront, vVolume, vLeaves ); + RetValue = Ivy_ManFindBoolCut( p, pObj, vFront, vVolume, vLeaves ); if ( RetValue == 0 ) printf( "- " ); else @@ -783,11 +783,11 @@ void Ivy_NodePrintCuts( Ivy_Store_t * pCutStore ) SeeAlso [] ***********************************************************************/ -Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves ) +Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves ) { static Ivy_Store_t CutStore, * pCutStore = &CutStore; Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut; - Ivy_Man_t * pMan = Ivy_ObjMan(pObj); + Ivy_Man_t * pMan = p; Ivy_Obj_t * pLeaf; int i, k; @@ -815,7 +815,7 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves ) continue; for ( k = 0; k < pCut->nSize; k++ ) { - pLeaf = Ivy_ObjObj( pObj, pCut->pArray[k] ); + pLeaf = Ivy_ManObj( p, pCut->pArray[k] ); if ( Ivy_ObjIsCi(pLeaf) ) continue; *pCutNew = *pCut; @@ -859,7 +859,7 @@ void Ivy_ManTestCutsAll( Ivy_Man_t * p ) { if ( !Ivy_ObjIsNode(pObj) ) continue; - nCutsCut = Ivy_NodeFindCutsAll( pObj, 4 )->nCuts; + nCutsCut = Ivy_NodeFindCutsAll( p, pObj, 5 )->nCuts; nCutsTotal += nCutsCut; nNodeOver += (nCutsCut == IVY_CUT_LIMIT); nNodeTotal++; diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c index 2dc3bac8..fb938c42 100644 --- a/src/temp/ivy/ivyDfs.c +++ b/src/temp/ivy/ivyDfs.c @@ -69,17 +69,14 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p ) Vec_Int_t * vNodes; Ivy_Obj_t * pObj; int i; + assert( Ivy_ManLatchNum(p) == 0 ); // make sure the nodes are not marked Ivy_ManForEachObj( p, pObj, i ) assert( !pObj->fMarkA && !pObj->fMarkB ); // collect the nodes vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) ); - if ( Ivy_ManLatchNum(p) > 0 ) - Ivy_ManForEachCo( p, pObj, i ) - Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes ); - else - Ivy_ManForEachPo( p, pObj, i ) - Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes ); + Ivy_ManForEachPo( p, pObj, i ) + Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes ); // unmark the collected nodes Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) Ivy_ObjClearMarkA(pObj); @@ -90,34 +87,7 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p ) /**Function************************************************************* - Synopsis [Collects nodes in the DFS order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes ) -{ - Vec_Int_t * vFanins; - int i, Fanin; - if ( !Ivy_ObjIsNodeExt(pObj) || Ivy_ObjIsMarkA(pObj) ) - return; - // mark the node as visited - Ivy_ObjSetMarkA(pObj); - // traverse the fanins - vFanins = Ivy_ObjGetFanins( pObj ); - Vec_IntForEachEntry( vFanins, Fanin, i ) - Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_EdgeId(Fanin)), vNodes ); - // add the node - Vec_IntPush( vNodes, pObj->Id ); -} - -/**Function************************************************************* - - Synopsis [Collects nodes in the DFS order.] + Synopsis [Collects AND/EXOR nodes in the DFS order from CIs to COs.] Description [] @@ -126,25 +96,31 @@ void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p ) +Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches ) { - Vec_Int_t * vNodes; - Ivy_Obj_t * pObj, * pFanin; + Vec_Int_t * vNodes, * vLatches; + Ivy_Obj_t * pObj; int i; - assert( p->fExtended ); - assert( Ivy_ManLatchNum(p) == 0 ); - // make sure network does not have buffers - vNodes = Vec_IntAlloc( 10 ); + assert( Ivy_ManLatchNum(p) > 0 ); + // make sure the nodes are not marked + Ivy_ManForEachObj( p, pObj, i ) + assert( !pObj->fMarkA && !pObj->fMarkB ); + // collect the latches + vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) ); + Ivy_ManForEachLatch( p, pObj, i ) + Vec_IntPush( vLatches, pObj->Id ); + // collect the nodes + vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) ); Ivy_ManForEachPo( p, pObj, i ) - { - pFanin = Ivy_ManObj( p, Ivy_EdgeId( Ivy_ObjReadFanin(pObj,0) ) ); - Ivy_ManDfsExt_rec( pFanin, vNodes ); - } + Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes ); + Ivy_ManForEachNodeVec( p, vLatches, pObj, i ) + Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes ); + // unmark the collected nodes Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) Ivy_ObjClearMarkA(pObj); // make sure network does not have dangling nodes - // the network may have dangling nodes if some fanins of ESOPs do not appear in cubes -// assert( p->nNodes == Vec_PtrSize(vNodes) ); + assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) ); + *pvLatches = vLatches; return vNodes; } @@ -249,7 +225,7 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p ) int i, k, Level, LevelMax; assert( p->vRequired == NULL ); // start the required times - vLevelsR = Vec_IntStart( Ivy_ManObjIdNext(p) ); + vLevelsR = Vec_IntStart( Ivy_ManObjIdMax(p) + 1 ); // iterate through the nodes in the reverse order vNodes = Ivy_ManLevelize( p ); Vec_VecForEachEntryReverseReverse( vNodes, pObj, i, k ) @@ -262,7 +238,7 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p ) } Vec_VecFree( vNodes ); // convert it into the required times - LevelMax = Ivy_ManReadLevels( p ); + LevelMax = Ivy_ManLevels( p ); //printf( "max %5d\n",LevelMax ); Ivy_ManForEachObj( p, pObj, i ) { diff --git a/src/temp/ivy/ivyDsd.c b/src/temp/ivy/ivyDsd.c index 5dfdd30f..3b8a2e68 100644 --- a/src/temp/ivy/ivyDsd.c +++ b/src/temp/ivy/ivyDsd.c @@ -608,7 +608,7 @@ Ivy_Obj_t * Ivy_ManDsdConstruct_rec( Ivy_Man_t * p, Vec_Int_t * vFront, int iNod // Ivy_MultiEval( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR ); - pResult = Ivy_Multi( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR ); + pResult = Ivy_Multi( p, pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR ); return Ivy_NotCond( pResult, Node.fCompl ); } assert( Node.fCompl == 0 ); @@ -626,9 +626,9 @@ Ivy_Obj_t * Ivy_ManDsdConstruct_rec( Ivy_Man_t * p, Vec_Int_t * vFront, int iNod pNodes[1] = Ivy_NotCond( pNodes[1], (Var1 & 1) ); pNodes[2] = Ivy_NotCond( pNodes[2], (Var0 & 1) ); if ( Node.Type == IVY_DEC_MUX ) - return Ivy_Mux( pNodes[0], pNodes[1], pNodes[2] ); + return Ivy_Mux( p, pNodes[0], pNodes[1], pNodes[2] ); else - return Ivy_Maj( pNodes[0], pNodes[1], pNodes[2] ); + return Ivy_Maj( p, pNodes[0], pNodes[1], pNodes[2] ); } assert( 0 ); return 0; diff --git a/src/temp/ivy/ivyFanout.c b/src/temp/ivy/ivyFanout.c new file mode 100644 index 00000000..5911e051 --- /dev/null +++ b/src/temp/ivy/ivyFanout.c @@ -0,0 +1,317 @@ +/**CFile**************************************************************** + + FileName [ivyFanout.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Representation of the fanouts.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyFanout.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Ivy_FanoutIsArray( void * p ) { return (int )(((unsigned)p) & 01); } +static inline Vec_Ptr_t * Ivy_FanoutGetArray( void * p ) { assert( Ivy_FanoutIsArray(p) ); return (Vec_Ptr_t *)((unsigned)(p) & ~01); } +static inline Vec_Ptr_t * Ivy_FanoutSetArray( void * p ) { assert( !Ivy_FanoutIsArray(p) ); return (Vec_Ptr_t *)((unsigned)(p) ^ 01); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the fanout representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManStartFanout( Ivy_Man_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + assert( p->vFanouts == NULL ); + p->vFanouts = Vec_PtrStart( Ivy_ManObjIdMax(p) + 1000 ); + Ivy_ManForEachObj( p, pObj, i ) + { + if ( Ivy_ObjFanin0(pObj) ) + Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj ); + if ( Ivy_ObjFanin1(pObj) ) + Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj ); + } +} + +/**Function************************************************************* + + Synopsis [Stops the fanout representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManStopFanout( Ivy_Man_t * p ) +{ + void * pTemp; + int i; + assert( p->vFanouts != NULL ); + Vec_PtrForEachEntry( p->vFanouts, pTemp, i ) + if ( Ivy_FanoutIsArray(pTemp) ) + Vec_PtrFree( Ivy_FanoutGetArray(pTemp) ); + Vec_PtrFree( p->vFanouts ); + p->vFanouts = NULL; +} + +/**Function************************************************************* + + Synopsis [Add the fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +{ + Vec_Ptr_t * vNodes; + void ** ppSpot; + assert( p->vFanouts != NULL ); + assert( !Ivy_IsComplement(pObj) ); + // extend the fanout array if needed + Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); + // get the pointer to the place where fanouts are stored + ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id ); + // consider several cases + if ( *ppSpot == NULL ) // no fanout - add one fanout + *ppSpot = pFanout; + else if ( Ivy_FanoutIsArray(*ppSpot) ) // array of fanouts - add one fanout + { + vNodes = Ivy_FanoutGetArray(*ppSpot); + Vec_PtrPush( vNodes, pFanout ); + } + else // only one fanout - create array and put both fanouts into the array + { + vNodes = Vec_PtrAlloc( 4 ); + Vec_PtrPush( vNodes, *ppSpot ); + Vec_PtrPush( vNodes, pFanout ); + *ppSpot = Ivy_FanoutSetArray( vNodes ); + } +} + +/**Function************************************************************* + + Synopsis [Removes the fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +{ + Vec_Ptr_t * vNodes; + void ** ppSpot; + assert( p->vFanouts != NULL ); + assert( !Ivy_IsComplement(pObj) ); + // extend the fanout array if needed + Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); + ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id ); + if ( *ppSpot == NULL ) // no fanout - should not happen + { + assert( 0 ); + } + else if ( Ivy_FanoutIsArray(*ppSpot) ) // the array of fanouts - delete the fanout + { + vNodes = Ivy_FanoutGetArray(*ppSpot); + Vec_PtrRemove( vNodes, pFanout ); + } + else // only one fanout - delete the fanout + { + assert( *ppSpot == pFanout ); + *ppSpot = NULL; + } +} + +/**Function************************************************************* + + Synopsis [Replaces the fanout of pOld to be pFanoutNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew ) +{ + Vec_Ptr_t * vNodes; + void ** ppSpot; + int Index; + assert( p->vFanouts != NULL ); + assert( !Ivy_IsComplement(pObj) ); + // extend the fanout array if needed + Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); + ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id ); + if ( *ppSpot == NULL ) // no fanout - should not happen + { + assert( 0 ); + } + else if ( Ivy_FanoutIsArray(*ppSpot) ) // the array of fanouts - find and replace the fanout + { + vNodes = Ivy_FanoutGetArray(*ppSpot); + Index = Vec_PtrFind( vNodes, pFanoutOld ); + assert( Index >= 0 ); + Vec_PtrWriteEntry( vNodes, Index, pFanoutNew ); + } + else // only one fanout - delete the fanout + { + assert( *ppSpot == pFanoutOld ); + *ppSpot = pFanoutNew; + } +} + +/**Function************************************************************* + + Synopsis [Starts iteration through the fanouts.] + + Description [Copies the currently available fanouts into the array.] + + SideEffects [Can be used while the fanouts are being removed.] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray ) +{ + Vec_Ptr_t * vNodes; + Ivy_Obj_t * pTemp; + int i; + assert( p->vFanouts != NULL ); + assert( !Ivy_IsComplement(pObj) ); + // extend the fanout array if needed + Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); + vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id ); + // clean the resulting array + Vec_PtrClear( vArray ); + if ( vNodes == NULL ) // no fanout - nothing to do + { + } + else if ( Ivy_FanoutIsArray(vNodes) ) // the array of fanouts - copy fanouts + { + vNodes = Ivy_FanoutGetArray(vNodes); + Vec_PtrForEachEntry( vNodes, pTemp, i ) + Vec_PtrPush( vArray, pTemp ); + } + else // only one fanout - add the fanout + Vec_PtrPush( vArray, vNodes ); +} + +/**Function************************************************************* + + Synopsis [Reads one fanout.] + + Description [Returns fanout if there is only one fanout.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ) +{ + Vec_Ptr_t * vNodes; + assert( p->vFanouts != NULL ); + assert( !Ivy_IsComplement(pObj) ); + // extend the fanout array if needed + Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); + vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id ); + // clean the resulting array + if ( vNodes && !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return + return (Ivy_Obj_t *)vNodes; + return NULL; +} + +/**Function************************************************************* + + Synopsis [Reads one fanout.] + + Description [Returns fanout if there is only one fanout.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ) +{ + Vec_Ptr_t * vNodes; + assert( p->vFanouts != NULL ); + assert( !Ivy_IsComplement(pObj) ); + // extend the fanout array if needed + Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); + vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id ); + // clean the resulting array + if ( vNodes == NULL ) + return NULL; + if ( !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return + return (Ivy_Obj_t *)vNodes; + return Vec_PtrEntry( Ivy_FanoutGetArray(vNodes), 0 ); +} + +/**Function************************************************************* + + Synopsis [Reads one fanout.] + + Description [Returns fanout if there is only one fanout.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj ) +{ + Vec_Ptr_t * vNodes; + assert( p->vFanouts != NULL ); + assert( !Ivy_IsComplement(pObj) ); + // extend the fanout array if needed + Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL ); + vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id ); + // clean the resulting array + if ( vNodes == NULL ) + return 0; + if ( !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return + return 1; + return Vec_PtrSize( Ivy_FanoutGetArray(vNodes) ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyIsop.c b/src/temp/ivy/ivyIsop.c new file mode 100644 index 00000000..f53e513d --- /dev/null +++ b/src/temp/ivy/ivyIsop.c @@ -0,0 +1,241 @@ +/**CFile**************************************************************** + + FileName [ivyIsop.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Computing irredundant SOP using truth table.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyIsop.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Ivy_Sop_t_ Ivy_Sop_t; +struct Ivy_Sop_t_ +{ + unsigned * pCubes; + int nCubes; +}; + +static Mem_Flex_t * s_Man = NULL; + +static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthManStart() +{ + s_Man = Mem_FlexStart(); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthManStop() +{ + Mem_FlexStop( s_Man, 0 ); + s_Man = NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ivy_TruthIsop( unsigned * uTruth, int nVars ) +{ +} + +/**Function************************************************************* + + Synopsis [Computes ISOP for 5 variables or less.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes ) +{ + Ivy_Sop_t cRes0, cRes1, cRes2; + Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2; + unsigned * puRes0, * puRes1, * puRes2; + unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp0, * pTemp1; + int i, k, Var, nWords; + assert( nVars > 5 ); + assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) ); + if ( Extra_TruthIsConst0( puOn, nVars ) ) + { + pcRes->nCubes = 0; + pcRes->pCubes = NULL; + return puOn; + } + if ( Extra_TruthIsConst1( puOnDc, nVars ) ) + { + pcRes->nCubes = 1; + pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 ); + pcRes->pCubes[0] = 0; + return puOnDc; + } + // find the topmost var + for ( Var = nVars-1; Var >= 0; Var-- ) + if ( Extra_TruthVarInSupport( puOn, nVars, Var ) || + Extra_TruthVarInSupport( puOnDc, nVars, Var ) ) + break; + assert( Var >= 0 ); + if ( Var < 5 ) + { + unsigned * puRes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 ); + *puRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var + 1, pcRes ); + return puRes; + } + nWords = Extra_TruthWordNum( Var+1 ); + // cofactor + puOn0 = puOn; + puOn1 = puOn + nWords; + puOnDc0 = puOnDc; + puOnDc1 = puOnDc + nWords; + // intermediate copies + pTemp0 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords ); + pTemp1 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords ); + // solve for cofactors + Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var + 1 ); + puRes0 = Ivy_TruthIsop5_rec( pTemp0, uOnDc0, Var-1, pcRes0 ); + Extra_TruthSharp( pTemp0, puOn1, puOnDc0, Var + 1 ); + puRes1 = Ivy_TruthIsop5_rec( pTemp1, uOnDc1, Var-1, pcRes1 ); + Extra_TruthSharp( pTemp0, puOn0, puRes0, Var + 1 ); + Extra_TruthSharp( pTemp1, puOn1, puRes1, Var + 1 ); + Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var + 1 ); + Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var + 1 ); + puRes2 = Ivy_TruthIsop5_rec( pTemp0, pTemp1, Var-1, pcRes2 ); + // create the resulting cover + pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes; + pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes ); + k = 0; + for ( i = 0; i < pcRes0->nCubes; i++ ) + pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1)); + for ( i = 0; i < pcRes1->nCubes; i++ ) + pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0)); + for ( i = 0; i < pcRes1->nCubes; i++ ) + pcRes->pCubes[k++] = pcRes2->pCubes[i]; + assert( k == pcRes->nCubes ); + // create the resulting truth table + Extra_TruthSharp( pTemp0, Var, uRes0, uRes1, Var + 1 ); + Extra_TruthOr( pTemp0, pTemp0, uRes2, Var + 1 ); + return pTemp0; +} + +/**Function************************************************************* + + Synopsis [Computes ISOP for 5 variables or less.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes ) +{ + unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + Ivy_Sop_t cRes0, cRes1, cRes2; + Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2; + unsigned uRes0, uRes1, uRes2; + unsigned uOn0, uOn1, uOnDc0, uOnDc1; + int i, k, Var; + assert( nVars <= 5 ); + assert( uOn & ~uOnDc == 0 ); + if ( Extra_TruthIsConst0( uOn == 0 ) + { + pcRes->nCubes = 0; + pcRes->pCubes = NULL; + return 0; + } + if ( uOnDc == 0xFFFFFFFF ) + { + pcRes->nCubes = 1; + pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 ); + pcRes->pCubes[0] = 0; + return 0xFFFFFFFF; + } + // find the topmost var + for ( Var = nVars-1; Var >= 0; Var-- ) + if ( Extra_TruthVarInSupport( &uOn, 5, Var ) || + Extra_TruthVarInSupport( &uOnDc, 5, Var ) ) + break; + assert( Var >= 0 ); + // cofactor + uOn0 = uOn1 = uOn; + uOnDc0 = uOnDc1 = uOnDc; + Extra_TruthCofactor0( &uOn0, 5, Var ); + Extra_TruthCofactor1( &uOn1, 5, Var ); + Extra_TruthCofactor0( &uOnDc0, 5, Var ); + Extra_TruthCofactor1( &uOnDc1, 5, Var ); + // solve for cofactors + uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var-1, pcRes0 ); + uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var-1, pcRes1 ); + uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var-1, pcRes2 ); + // create the resulting cover + pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes; + pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes ); + k = 0; + for ( i = 0; i < pcRes0->nCubes; i++ ) + pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1)); + for ( i = 0; i < pcRes1->nCubes; i++ ) + pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0)); + for ( i = 0; i < pcRes1->nCubes; i++ ) + pcRes->pCubes[k++] = pcRes2->pCubes[i]; + assert( k == pcRes->nCubes ); + return (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]) | uRes2; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c index 2ff90aa9..d1aca8a6 100644 --- a/src/temp/ivy/ivyMan.c +++ b/src/temp/ivy/ivyMan.c @@ -39,53 +39,32 @@ SeeAlso [] ***********************************************************************/ -Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax ) +Ivy_Man_t * Ivy_ManStart() { Ivy_Man_t * p; - Ivy_Obj_t * pObj; - int i, nTotalSize; // start the manager p = ALLOC( Ivy_Man_t, 1 ); memset( p, 0, sizeof(Ivy_Man_t) ); + // perform initializations + p->Ghost.Id = -1; p->nTravIds = 1; p->fCatchExor = 1; - // AIG nodes - p->nObjsAlloc = 1 + nPis + nPos + nNodesMax; -// p->nObjsAlloc += (p->nObjsAlloc & 1); // make it even - nTotalSize = p->nObjsAlloc + IVY_SANDBOX_SIZE + 1; - p->pObjs = ALLOC( Ivy_Obj_t, nTotalSize ); - memset( p->pObjs, 0, sizeof(Ivy_Obj_t) * nTotalSize ); - // temporary storage for deleted entries - p->vFree = Vec_IntAlloc( 100 ); - // set the node IDs - for ( i = 0, pObj = p->pObjs; i < nTotalSize; i++, pObj++ ) - pObj->Id = i - IVY_SANDBOX_SIZE - 1; - // remember the manager in the first entry - *((Ivy_Man_t **)p->pObjs) = p; - p->pObjs += IVY_SANDBOX_SIZE + 1; + // allocate arrays for nodes + p->vPis = Vec_PtrAlloc( 100 ); + p->vPos = Vec_PtrAlloc( 100 ); + p->vBufs = Vec_PtrAlloc( 100 ); + p->vObjs = Vec_PtrAlloc( 100 ); + // prepare the internal memory manager + Ivy_ManStartMemory( p ); // create the constant node + p->pConst1 = Ivy_ManFetchMemory( p ); + p->pConst1->fPhase = 1; + Vec_PtrPush( p->vObjs, p->pConst1 ); p->nCreated = 1; - p->ObjIdNext = 1; - Ivy_ManConst1(p)->fPhase = 1; - // create PIs - pObj = Ivy_ManGhost(p); - pObj->Type = IVY_PI; - p->vPis = Vec_IntAlloc( 100 ); - for ( i = 0; i < nPis; i++ ) - Ivy_ObjCreate( pObj ); - // create POs - pObj->Type = IVY_PO; - p->vPos = Vec_IntAlloc( 100 ); - for ( i = 0; i < nPos; i++ ) - Ivy_ObjCreate( pObj ); // start the table - p->nTableSize = p->nObjsAlloc*5/2+13; + p->nTableSize = 10007; p->pTable = ALLOC( int, p->nTableSize ); memset( p->pTable, 0, sizeof(int) * p->nTableSize ); - // allocate undo storage - p->nUndosAlloc = 100; - p->pUndos = ALLOC( Ivy_Obj_t, p->nUndosAlloc ); - memset( p->pUndos, 0, sizeof(Ivy_Obj_t) * p->nUndosAlloc ); return p; } @@ -102,22 +81,15 @@ Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax ) ***********************************************************************/ void Ivy_ManStop( Ivy_Man_t * p ) { - if ( p->fExtended ) - { - Ivy_Obj_t * pObj; - int i; - Ivy_ManForEachObj( p, pObj, i ) - if ( Ivy_ObjGetFanins(pObj) ) - Vec_IntFree( Ivy_ObjGetFanins(pObj) ); - } - if ( p->vFree ) Vec_IntFree( p->vFree ); - if ( p->vTruths ) Vec_IntFree( p->vTruths ); - if ( p->vPis ) Vec_IntFree( p->vPis ); - if ( p->vPos ) Vec_IntFree( p->vPos ); - FREE( p->pMemory ); - free( p->pObjs - IVY_SANDBOX_SIZE - 1 ); +// Ivy_TableProfile( 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 ); + if ( p->vPos ) Vec_PtrFree( p->vPos ); + if ( p->vBufs ) Vec_PtrFree( p->vBufs ); + if ( p->vObjs ) Vec_PtrFree( p->vObjs ); free( p->pTable ); - free( p->pUndos ); free( p ); } @@ -132,18 +104,15 @@ void Ivy_ManStop( Ivy_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Ivy_ManGrow( Ivy_Man_t * p ) +int Ivy_ManCleanup( Ivy_Man_t * p ) { - int i; - assert( p->ObjIdNext == p->nObjsAlloc ); - if ( p->ObjIdNext != p->nObjsAlloc ) - return; -// printf( "Ivy_ObjCreate(): Reallocing the node array.\n" ); - p->nObjsAlloc = 2 * p->nObjsAlloc; - p->pObjs = REALLOC( Ivy_Obj_t, p->pObjs - IVY_SANDBOX_SIZE - 1, p->nObjsAlloc + IVY_SANDBOX_SIZE + 1 ) + IVY_SANDBOX_SIZE + 1; - memset( p->pObjs + p->ObjIdNext, 0, sizeof(Ivy_Obj_t) * p->nObjsAlloc / 2 ); - for ( i = p->nObjsAlloc / 2; i < p->nObjsAlloc; i++ ) - Ivy_ManObj( p, i )->Id = i; + Ivy_Obj_t * pNode; + int i, nNodesOld; + nNodesOld = Ivy_ManNodeNum(p); + Ivy_ManForEachNode( p, pNode, i ) + if ( Ivy_ObjRefs(pNode) == 0 ) + Ivy_ObjDelete_rec( p, pNode, 1 ); + return nNodesOld - Ivy_ManNodeNum(p); } /**Function************************************************************* @@ -157,15 +126,19 @@ void Ivy_ManGrow( Ivy_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Ivy_ManCleanup( Ivy_Man_t * p ) +int Ivy_ManPropagateBuffers( Ivy_Man_t * p ) { Ivy_Obj_t * pNode; - int i, nNodesOld; - nNodesOld = Ivy_ManNodeNum(p); - Ivy_ManForEachNode( p, pNode, i ) - if ( Ivy_ObjRefs(pNode) == 0 ) - Ivy_ObjDelete_rec( pNode, 1 ); - return nNodesOld - Ivy_ManNodeNum(p); + int nSteps; + for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ ) + { + pNode = Vec_PtrEntryLast(p->vBufs); + while ( Ivy_ObjIsBuf(pNode) ) + pNode = Ivy_ObjReadFirstFanout( p, pNode ); + Ivy_NodeFixBufferFanins( p, pNode ); + } +// printf( "Number of steps = %d\n", nSteps ); + return nSteps; } /**Function************************************************************* @@ -182,24 +155,71 @@ int Ivy_ManCleanup( Ivy_Man_t * p ) void Ivy_ManPrintStats( Ivy_Man_t * p ) { printf( "PI/PO = %d/%d ", Ivy_ManPiNum(p), Ivy_ManPoNum(p) ); - if ( p->fExtended ) - { - printf( "Am = %d. ", Ivy_ManAndMultiNum(p) ); - printf( "Xm = %d. ", Ivy_ManExorMultiNum(p) ); - printf( "Lut = %d. ", Ivy_ManLutNum(p) ); - } - else + printf( "A = %d. ", Ivy_ManAndNum(p) ); + printf( "L = %d. ", Ivy_ManLatchNum(p) ); +// printf( "X = %d. ", Ivy_ManExorNum(p) ); + printf( "B = %d. ", Ivy_ManBufNum(p) ); + printf( "MaxID = %d. ", Ivy_ManObjIdMax(p) ); +// printf( "Cre = %d. ", p->nCreated ); +// printf( "Del = %d. ", p->nDeleted ); + printf( "Lev = %d. ", Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Converts a combinational AIG manager into a sequential one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits ) +{ + Ivy_Obj_t * pObj, * pLatch; + Ivy_Init_t Init; + int i; + if ( nLatches == 0 ) + return; + assert( nLatches < Ivy_ManPiNum(p) && nLatches < Ivy_ManPoNum(p) ); + assert( Ivy_ManPiNum(p) == Vec_PtrSize(p->vPis) ); + assert( Ivy_ManPoNum(p) == Vec_PtrSize(p->vPos) ); + assert( Vec_PtrSize( p->vBufs ) == 0 ); + // create fanouts + if ( p->vFanouts == NULL ) + Ivy_ManStartFanout( p ); + // collect the POs to be converted into latches + for ( i = 0; i < nLatches; i++ ) { - printf( "A = %d. ", Ivy_ManAndNum(p) ); - printf( "X = %d. ", Ivy_ManExorNum(p) ); - printf( "B = %4d. ", Ivy_ManBufNum(p) ); + // get the latch value + Init = pInits? pInits[i] : IVY_INIT_0; + // create latch + pObj = Ivy_ManPo( p, Ivy_ManPoNum(p) - nLatches + i ); + pLatch = Ivy_Latch( p, Ivy_ObjChild0(pObj), Init ); + Ivy_ObjDisconnect( p, pObj ); + // convert the corresponding PI to a buffer and connect it to the latch + pObj = Ivy_ManPi( p, Ivy_ManPiNum(p) - nLatches + i ); + pObj->Type = IVY_BUF; + Ivy_ObjConnect( p, pObj, pLatch, NULL ); + // save the buffer + Vec_PtrPush( p->vBufs, pObj ); } -// printf( "MaxID = %d. ", p->ObjIdNext-1 ); -// printf( "All = %d. ", p->nObjsAlloc ); - printf( "Cre = %d. ", p->nCreated ); - printf( "Del = %d. ", p->nDeleted ); - printf( "Lev = %d. ", Ivy_ManReadLevels(p) ); - printf( "\n" ); + // shrink the arrays + Vec_PtrShrink( p->vPis, Ivy_ManPiNum(p) - nLatches ); + Vec_PtrShrink( p->vPos, Ivy_ManPoNum(p) - nLatches ); + // update the counters of different objects + p->nObjs[IVY_PI] -= nLatches; + p->nObjs[IVY_PO] -= nLatches; + p->nObjs[IVY_BUF] += nLatches; + p->nDeleted -= 2 * nLatches; + // perform hashing by propagating the buffers + Ivy_ManPropagateBuffers( p ); + // check the resulting network + if ( !Ivy_ManCheck(p) ) + printf( "Ivy_ManMakeSeq(): The check has failed.\n" ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyMem.c b/src/temp/ivy/ivyMem.c new file mode 100644 index 00000000..01833f03 --- /dev/null +++ b/src/temp/ivy/ivyMem.c @@ -0,0 +1,115 @@ +/**CFile**************************************************************** + + FileName [ivyMem.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Memory management for the AIG nodes.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyMem.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// memory management +#define IVY_PAGE_SIZE 12 // page size containing 2^IVY_PAGE_SIZE nodes +#define IVY_PAGE_MASK 4095 // page bitmask (2^IVY_PAGE_SIZE)-1 + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the internal memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManStartMemory( Ivy_Man_t * p ) +{ + p->vChunks = Vec_PtrAlloc( 128 ); + p->vPages = Vec_PtrAlloc( 128 ); +} + +/**Function************************************************************* + + Synopsis [Stops the internal memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManStopMemory( Ivy_Man_t * p ) +{ + void * pMemory; + int i; + Vec_PtrForEachEntry( p->vChunks, pMemory, i ) + free( pMemory ); + Vec_PtrFree( p->vChunks ); + Vec_PtrFree( p->vPages ); + p->pListFree = NULL; +} + +/**Function************************************************************* + + Synopsis [Allocates additional memory for the nodes.] + + Description [Allocates IVY_PAGE_SIZE nodes. Aligns memory by 32 bytes. + Records the pointer to the AIG manager in the -1 entry.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManAddMemory( Ivy_Man_t * p ) +{ + char * pMemory; + int i, nBytes; + assert( sizeof(Ivy_Obj_t) <= 32 ); + 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; + pMemory = ALLOC( char, nBytes ); + Vec_PtrPush( p->vChunks, pMemory ); + // align memory at the 32-byte boundary + pMemory = pMemory + 32 - (((int)pMemory) & 31); + // remember the manager in the first entry + Vec_PtrPush( p->vPages, pMemory ); + // break the memory down into nodes + p->pListFree = (Ivy_Obj_t *)pMemory; + for ( i = 1; i <= IVY_PAGE_MASK; i++ ) + { + *((char **)pMemory) = pMemory + sizeof(Ivy_Obj_t); + pMemory += sizeof(Ivy_Obj_t); + } + *((char **)pMemory) = NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c index e2a44e2d..f098332d 100644 --- a/src/temp/ivy/ivyMulti.c +++ b/src/temp/ivy/ivyMulti.c @@ -34,8 +34,8 @@ struct Ivy_Eva_t_ int Weight; // the number of covered nodes }; -static void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals ); -static int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols ); +static void Ivy_MultiPrint( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals ); +static int Ivy_MultiCover( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -52,7 +52,7 @@ static int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLim SeeAlso [] ***********************************************************************/ -int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSols ) +int Ivy_MultiPlus( Ivy_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSols ) { static Ivy_Eva_t pEvals[IVY_EVAL_LIMIT]; Ivy_Eva_t * pEval, * pFan0, * pFan1; @@ -122,7 +122,7 @@ int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int { pFan0 = pEvals + i; pFan1 = pEvals + k; - pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE)); + pTemp = Ivy_TableLookup(p, Ivy_ObjCreateGhost(p, pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE)); // skip nodes in the cone if ( pTemp == NULL || pTemp->fMarkB ) continue; @@ -149,7 +149,7 @@ int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int Outside: // Ivy_MultiPrint( pEvals, nLeaves, nEvals ); - if ( !Ivy_MultiCover( pEvals, nLeaves, nEvals, nLimit, vSols ) ) + if ( !Ivy_MultiCover( p, pEvals, nLeaves, nEvals, nLimit, vSols ) ) return 0; assert( Vec_PtrSize( vSols ) > 0 ); return 1; @@ -166,7 +166,7 @@ Outside: SeeAlso [] ***********************************************************************/ -void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals ) +void Ivy_MultiPrint( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals ) { Ivy_Eva_t * pEval; int i, k; @@ -215,7 +215,7 @@ static inline int Ivy_MultiWeight( unsigned uMask, int nMaskOnes, unsigned uFoun SeeAlso [] ***********************************************************************/ -int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols ) +int Ivy_MultiCover( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols ) { int fVerbose = 0; Ivy_Eva_t * pEval, * pEvalBest; @@ -294,6 +294,45 @@ int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec } } +/**Function************************************************************* + + Synopsis [Constructs the well-balanced tree of gates.] + + Description [Disregards levels and possible logic sharing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pObj1, * pObj2; + if ( nObjs == 1 ) + return ppObjs[0]; + pObj1 = Ivy_Multi_rec( p, ppObjs, nObjs/2, Type ); + pObj2 = Ivy_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type ); + return Ivy_Oper( p, pObj1, pObj2, Type ); +} + +/**Function************************************************************* + + Synopsis [Old code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + assert( Type == IVY_AND || Type == IVY_EXOR ); + assert( nArgs > 0 ); + return Ivy_Multi_rec( p, pArgs, nArgs, Type ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c index 703218bb..de67c560 100644 --- a/src/temp/ivy/ivyObj.c +++ b/src/temp/ivy/ivyObj.c @@ -39,36 +39,54 @@ SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost ) +Ivy_Obj_t * Ivy_ObjCreatePi( Ivy_Man_t * p ) +{ + return Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, NULL, NULL, IVY_PI, IVY_INIT_NONE) ); +} + +/**Function************************************************************* + + Synopsis [Create the new node assuming it does not exist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ObjCreatePo( Ivy_Man_t * p, Ivy_Obj_t * pDriver ) +{ + return Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pDriver, NULL, IVY_PO, IVY_INIT_NONE) ); +} + +/**Function************************************************************* + + Synopsis [Create the new node assuming it does not exist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost ) { - Ivy_Man_t * p = Ivy_ObjMan(pGhost); Ivy_Obj_t * pObj; assert( !Ivy_IsComplement(pGhost) ); assert( Ivy_ObjIsGhost(pGhost) ); - - assert( Ivy_TableLookup(pGhost) == NULL ); - - // realloc the node array - if ( p->ObjIdNext == p->nObjsAlloc ) - { - printf( "AIG manager is being resized. In the current release, it is not allowed!\n" ); - Ivy_ManGrow( p ); - pGhost = Ivy_ManGhost( p ); - } + assert( Ivy_TableLookup(p, pGhost) == NULL ); // get memory for the new object - if ( Vec_IntSize(p->vFree) > 0 ) - pObj = p->pObjs + Vec_IntPop(p->vFree); - else - pObj = p->pObjs + p->ObjIdNext++; - assert( pObj->Id == pObj - p->pObjs ); + pObj = Ivy_ManFetchMemory( p ); assert( Ivy_ObjIsNone(pObj) ); + pObj->Id = Vec_PtrSize(p->vObjs); + Vec_PtrPush( p->vObjs, pObj ); // add basic info (fanins, compls, type, init) - Ivy_ObjOverwrite( pObj, pGhost ); - // increment references of the fanins - Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) ); - Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) ); - // add the node to the structural hash table - Ivy_TableInsert( pObj ); + pObj->Type = pGhost->Type; + pObj->Init = pGhost->Init; + // add connections + Ivy_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 ); // compute level if ( Ivy_ObjIsNode(pObj) ) pObj->Level = Ivy_ObjLevelNew(pObj); @@ -86,9 +104,13 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost ) } // add PIs/POs to the arrays if ( Ivy_ObjIsPi(pObj) ) - Vec_IntPush( p->vPis, pObj->Id ); + Vec_PtrPush( p->vPis, pObj ); else if ( Ivy_ObjIsPo(pObj) ) - Vec_IntPush( p->vPos, pObj->Id ); + Vec_PtrPush( p->vPos, pObj ); +// else if ( Ivy_ObjIsBuf(pObj) ) +// Vec_PtrPush( p->vBufs, pObj ); + if ( p->vRequired && Vec_IntSize(p->vRequired) <= pObj->Id ) + Vec_IntFillExtra( p->vRequired, 2 * Vec_IntSize(p->vRequired), 1000000 ); // update node counters of the manager p->nObjs[Ivy_ObjType(pObj)]++; p->nCreated++; @@ -97,7 +119,7 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost ) /**Function************************************************************* - Synopsis [Create the new node assuming it does not exist.] + Synopsis [Connect the object to the fanin.] Description [] @@ -106,22 +128,28 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type ) +void Ivy_ObjConnect( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFan0, Ivy_Obj_t * pFan1 ) { - Ivy_Obj_t * pObj; - assert( Type == IVY_ANDM || Type == IVY_EXORM || Type == IVY_LUT ); - // realloc the node array - if ( p->ObjIdNext == p->nObjsAlloc ) - Ivy_ManGrow( p ); - // create the new node - pObj = p->pObjs + p->ObjIdNext; - assert( pObj->Id == p->ObjIdNext ); - p->ObjIdNext++; - pObj->Type = Type; - // update node counters of the manager - p->nObjs[Type]++; - p->nCreated++; - return pObj; + assert( !Ivy_IsComplement(pObj) ); + assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || pFan1 != NULL ); + // add the first fanin + pObj->pFanin0 = pFan0; + pObj->pFanin1 = pFan1; + // increment references of the fanins and add their fanouts + if ( Ivy_ObjFanin0(pObj) != NULL ) + { + Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) ); + if ( p->vFanouts ) + Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj ); + } + if ( Ivy_ObjFanin1(pObj) != NULL ) + { + Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) ); + if ( p->vFanouts ) + Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj ); + } + // add the node to the structural hash table + Ivy_TableInsert( p, pObj ); } /**Function************************************************************* @@ -135,18 +163,59 @@ Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type ) SeeAlso [] ***********************************************************************/ -void Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin ) +void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); - assert( Ivy_ObjIsOneFanin(pObj) ); - assert( Ivy_ObjFaninId0(pObj) == 0 ); + assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || Ivy_ObjFanin1(pObj) != NULL ); + // remove connections + if ( Ivy_ObjFanin0(pObj) != NULL ) + { + Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj)); + if ( p->vFanouts ) + Ivy_ObjDeleteFanout( p, Ivy_ObjFanin0(pObj), pObj ); + } + if ( Ivy_ObjFanin1(pObj) != NULL ) + { + Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj)); + if ( p->vFanouts ) + Ivy_ObjDeleteFanout( p, Ivy_ObjFanin1(pObj), pObj ); + } + // remove the node from the structural hash table + Ivy_TableDelete( p, pObj ); // add the first fanin - pObj->fComp0 = Ivy_IsComplement(pFanin); - pObj->Fanin0 = Ivy_Regular(pFanin)->Id; - // increment references of the fanins - Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) ); - // add the node to the structural hash table - Ivy_TableInsert( pObj ); + pObj->pFanin0 = NULL; + pObj->pFanin1 = NULL; +} + +/**Function************************************************************* + + Synopsis [Replaces the first fanin of the node by the new fanin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew ) +{ + Ivy_Obj_t * pFaninOld; + assert( !Ivy_IsComplement(pObj) ); + pFaninOld = Ivy_ObjFanin0(pObj); + // decrement ref and remove fanout + Ivy_ObjRefsDec( pFaninOld ); + if ( p->vFanouts ) + Ivy_ObjDeleteFanout( p, pFaninOld, pObj ); + // increment ref and add fanout + Ivy_ObjRefsInc( Ivy_Regular(pFaninNew) ); + if ( p->vFanouts ) + 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 ); } /**Function************************************************************* @@ -160,33 +229,35 @@ void Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin ) SeeAlso [] ***********************************************************************/ -void Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop ) +void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ) { - Ivy_Man_t * p; assert( !Ivy_IsComplement(pObj) ); - assert( Ivy_ObjRefs(pObj) == 0 ); - // remove connections - Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj)); - Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj)); - // remove the node from the structural hash table - Ivy_TableDelete( pObj ); + assert( Ivy_ObjRefs(pObj) == 0 || !fFreeTop ); // update node counters of the manager - p = Ivy_ObjMan(pObj); p->nObjs[pObj->Type]--; p->nDeleted++; + // remove connections + Ivy_ObjDisconnect( p, pObj ); // remove PIs/POs from the arrays if ( Ivy_ObjIsPi(pObj) ) - Vec_IntRemove( p->vPis, pObj->Id ); + Vec_PtrRemove( p->vPis, pObj ); else if ( Ivy_ObjIsPo(pObj) ) - Vec_IntRemove( p->vPos, pObj->Id ); - // recorde the deleted node - if ( p->fRecording ) - Ivy_ManUndoRecord( p, pObj ); - // clean the node's memory - Ivy_ObjClean( pObj ); - // remember the entry + Vec_PtrRemove( p->vPos, pObj ); + else if ( p->vFanouts && Ivy_ObjIsBuf(pObj) ) + Vec_PtrRemove( p->vBufs, pObj ); + // clean and recycle the entry if ( fFreeTop ) - Vec_IntPush( p->vFree, pObj->Id ); + { + // free the node + Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); + Ivy_ManRecycleMemory( p, pObj ); + } + else + { + int nRefsOld = pObj->nRefs; + Ivy_ObjClean( pObj ); + pObj->nRefs = nRefsOld; + } } /**Function************************************************************* @@ -200,20 +271,20 @@ void Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop ) SeeAlso [] ***********************************************************************/ -void Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop ) +void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ) { Ivy_Obj_t * pFanin0, * pFanin1; assert( !Ivy_IsComplement(pObj) ); - assert( !Ivy_ObjIsPo(pObj) && !Ivy_ObjIsNone(pObj) ); + assert( !Ivy_ObjIsNone(pObj) ); if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsPi(pObj) ) return; pFanin0 = Ivy_ObjFanin0(pObj); pFanin1 = Ivy_ObjFanin1(pObj); - Ivy_ObjDelete( pObj, fFreeTop ); - if ( !Ivy_ObjIsNone(pFanin0) && Ivy_ObjRefs(pFanin0) == 0 ) - Ivy_ObjDelete_rec( pFanin0, 1 ); - if ( !Ivy_ObjIsNone(pFanin1) && Ivy_ObjRefs(pFanin1) == 0 ) - Ivy_ObjDelete_rec( pFanin1, 1 ); + Ivy_ObjDelete( p, pObj, fFreeTop ); + if ( pFanin0 && !Ivy_ObjIsNone(pFanin0) && Ivy_ObjRefs(pFanin0) == 0 ) + Ivy_ObjDelete_rec( p, pFanin0, 1 ); + if ( pFanin1 && !Ivy_ObjIsNone(pFanin1) && Ivy_ObjRefs(pFanin1) == 0 ) + Ivy_ObjDelete_rec( p, pFanin1, 1 ); } /**Function************************************************************* @@ -229,66 +300,61 @@ void Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop ) SeeAlso [] ***********************************************************************/ -void Ivy_ObjReplace( Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop ) +void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop ) { int nRefsOld; // the object to be replaced cannot be complemented assert( !Ivy_IsComplement(pObjOld) ); // the object to be replaced cannot be a terminal - assert( Ivy_ObjIsNone(pObjOld) || !Ivy_ObjIsTerm(pObjOld) ); + assert( Ivy_ObjIsNone(pObjOld) || !Ivy_ObjIsPi(pObjOld) ); // the object to be used cannot be a PO or assert - assert( !Ivy_ObjIsPo(Ivy_Regular(pObjNew)) ); + assert( !Ivy_ObjIsBuf(Ivy_Regular(pObjNew)) ); // the object cannot be the same assert( pObjOld != Ivy_Regular(pObjNew) ); // if the new object is complemented or already used, add the buffer - if ( Ivy_IsComplement(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) ) - pObjNew = Ivy_ObjCreate( Ivy_ObjCreateGhost(pObjNew, Ivy_ObjConst1(pObjOld), IVY_BUF, IVY_INIT_NONE) ); + if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) ) + pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) ); assert( !Ivy_IsComplement(pObjNew) ); - // remember the reference counter - nRefsOld = pObjOld->nRefs; - pObjOld->nRefs = 0; + // 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 ) + { + assert( Ivy_ObjIsNode(pObjOld) ); + pObjOld->Level = pObjNew->Level; + Ivy_ObjUpdateLevel_rec( p, pObjOld ); + } + // if the new node's required time has changed, recursively update required time of the fanins + if ( p->vRequired ) + { + int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id); + if ( ReqNew < Vec_IntEntry(p->vRequired, pObjNew->Id) ) + { + Vec_IntWriteEntry( p->vRequired, pObjNew->Id, ReqNew ); + Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew ); + } + } // delete the old object if ( fDeleteOld ) - Ivy_ObjDelete_rec( pObjOld, fFreeTop ); + Ivy_ObjDelete_rec( p, pObjOld, fFreeTop ); // transfer the old object assert( Ivy_ObjRefs(pObjNew) == 0 ); + nRefsOld = pObjOld->nRefs; Ivy_ObjOverwrite( pObjOld, pObjNew ); pObjOld->nRefs = nRefsOld; - // update the hash table - Ivy_TableUpdate( pObjNew, pObjOld->Id ); - // create the object that was taken over by pObjOld - Ivy_ObjClean( pObjNew ); - // remember the entry - Vec_IntPush( Ivy_ObjMan(pObjOld)->vFree, pObjNew->Id ); -} - -/**Function************************************************************* - - Synopsis [Returns the first real fanins (not a buffer/inverter).] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin ) -{ - if ( iFanin == 0 ) + // patch the fanout of the fanins + if ( p->vFanouts ) { - if ( Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) ) - return Ivy_NotCond( Ivy_NodeRealFanin_rec(Ivy_ObjFanin0(pNode), 0), Ivy_ObjFaninC0(pNode) ); - else - return Ivy_ObjChild0(pNode); - } - else - { - if ( Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) ) - return Ivy_NotCond( Ivy_NodeRealFanin_rec(Ivy_ObjFanin1(pNode), 0), Ivy_ObjFaninC1(pNode) ); - else - return Ivy_ObjChild1(pNode); + Ivy_ObjPatchFanout( p, Ivy_ObjFanin0(pObjOld), pObjNew, pObjOld ); + if ( Ivy_ObjFanin1(pObjOld) ) + Ivy_ObjPatchFanout( p, Ivy_ObjFanin1(pObjOld), pObjNew, pObjOld ); } + // update the hash table + Ivy_TableUpdate( p, pObjNew, pObjOld->Id ); + // recycle the object that was taken over by pObjOld + Vec_PtrWriteEntry( p->vObjs, pObjNew->Id, NULL ); + Ivy_ManRecycleMemory( p, pObjNew ); + // if the new node is the buffer propagate it + if ( p->vFanouts && Ivy_ObjIsBuf(pObjOld) ) + Vec_PtrPush( p->vBufs, pObjOld ); } /**Function************************************************************* @@ -304,19 +370,31 @@ Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin ) SeeAlso [] ***********************************************************************/ -void Ivy_NodeFixBufferFanins( Ivy_Obj_t * pNode ) +void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode ) { Ivy_Obj_t * pFanReal0, * pFanReal1, * pResult; - assert( Ivy_ObjIsNode(pNode) ); + if ( Ivy_ObjIsPo(pNode) ) + { + if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) ) + return; + pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) ); + Ivy_ObjPatchFanin0( p, pNode, pFanReal0 ); + return; + } if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) && !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) ) return; // get the real fanins - pFanReal0 = Ivy_NodeRealFanin_rec( pNode, 0 ); - pFanReal1 = Ivy_NodeRealFanin_rec( pNode, 1 ); + pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) ); + pFanReal1 = Ivy_ObjReal( Ivy_ObjChild1(pNode) ); // get the new node - pResult = Ivy_Oper( pFanReal0, pFanReal1, Ivy_ObjType(pNode) ); + if ( Ivy_ObjIsNode(pNode) ) + pResult = Ivy_Oper( p, pFanReal0, pFanReal1, Ivy_ObjType(pNode) ); + else if ( Ivy_ObjIsLatch(pNode) ) + pResult = Ivy_Latch( p, pFanReal0, Ivy_ObjInit(pNode) ); + else + assert( 0 ); // perform the replacement - Ivy_ObjReplace( pNode, pResult, 1, 0 ); + Ivy_ObjReplace( p, pNode, pResult, 1, 0 ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyOper.c b/src/temp/ivy/ivyOper.c index 96f78165..af216e45 100644 --- a/src/temp/ivy/ivyOper.c +++ b/src/temp/ivy/ivyOper.c @@ -57,12 +57,12 @@ static inline int Ivy_ObjIsExorType( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Obj_t * SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ) +Ivy_Obj_t * Ivy_Oper( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ) { if ( Type == IVY_AND ) - return Ivy_And( p0, p1 ); + return Ivy_And( p, p0, p1 ); if ( Type == IVY_EXOR ) - return Ivy_Exor( p0, p1 ); + return Ivy_Exor( p, p0, p1 ); assert( 0 ); return NULL; } @@ -78,23 +78,22 @@ Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) +Ivy_Obj_t * Ivy_And( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) { - Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0)); // Ivy_Obj_t * pFan0, * pFan1; // check trivial cases if ( p0 == p1 ) return p0; if ( p0 == Ivy_Not(p1) ) - return Ivy_Not(pConst1); - if ( Ivy_Regular(p0) == pConst1 ) - return p0 == pConst1 ? p1 : Ivy_Not(pConst1); - if ( Ivy_Regular(p1) == pConst1 ) - return p1 == pConst1 ? p0 : Ivy_Not(pConst1); + return Ivy_Not(p->pConst1); + if ( Ivy_Regular(p0) == p->pConst1 ) + return p0 == p->pConst1 ? p1 : Ivy_Not(p->pConst1); + if ( Ivy_Regular(p1) == p->pConst1 ) + return p1 == p->pConst1 ? p0 : Ivy_Not(p->pConst1); // check if it can be an EXOR gate // if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) ) // return Ivy_CanonExor( pFan0, pFan1 ); - return Ivy_CanonAnd( p0, p1 ); + return Ivy_CanonAnd( p, p0, p1 ); } /**Function************************************************************* @@ -108,36 +107,22 @@ Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) +Ivy_Obj_t * Ivy_Exor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) { - Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0)); +/* // check trivial cases if ( p0 == p1 ) - return Ivy_Not(pConst1); + return Ivy_Not(p->pConst1); if ( p0 == Ivy_Not(p1) ) - return pConst1; - if ( Ivy_Regular(p0) == pConst1 ) - return Ivy_NotCond( p1, p0 == pConst1 ); - if ( Ivy_Regular(p1) == pConst1 ) - return Ivy_NotCond( p0, p1 == pConst1 ); + return p->pConst1; + if ( Ivy_Regular(p0) == p->pConst1 ) + return Ivy_NotCond( p1, p0 == p->pConst1 ); + if ( Ivy_Regular(p1) == p->pConst1 ) + return Ivy_NotCond( p0, p1 == p->pConst1 ); // check the table - return Ivy_CanonExor( p0, p1 ); -} - -/**Function************************************************************* - - Synopsis [Performs canonicization step.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_Latch( Ivy_Obj_t * pObj, Ivy_Init_t Init ) -{ - return Ivy_CanonLatch( pObj, Init ); + return Ivy_CanonExor( p, p0, p1 ); +*/ + return Ivy_Or( p, Ivy_And(p, p0, Ivy_Not(p1)), Ivy_And(p, Ivy_Not(p0), p1) ); } /**Function************************************************************* @@ -151,9 +136,9 @@ Ivy_Obj_t * Ivy_Latch( Ivy_Obj_t * pObj, Ivy_Init_t Init ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) +Ivy_Obj_t * Ivy_Or( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) { - return Ivy_Not( Ivy_And( Ivy_Not(p0), Ivy_Not(p1) ) ); + return Ivy_Not( Ivy_And( p, Ivy_Not(p0), Ivy_Not(p1) ) ); } /**Function************************************************************* @@ -167,43 +152,42 @@ Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 ) +Ivy_Obj_t * Ivy_Mux( Ivy_Man_t * p, Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 ) { - Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0)); Ivy_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp; int Count0, Count1; // consider trivial cases if ( p0 == Ivy_Not(p1) ) - return Ivy_Exor( pC, p0 ); + return Ivy_Exor( p, pC, p0 ); // other cases can be added // implement the first MUX (F = C * x1 + C' * x0) - pTempA1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC, p1, IVY_AND, IVY_INIT_NONE) ); - pTempA2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), p0, IVY_AND, IVY_INIT_NONE) ); + pTempA1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pC, p1, IVY_AND, IVY_INIT_NONE) ); + pTempA2 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pC), p0, IVY_AND, IVY_INIT_NONE) ); if ( pTempA1 && pTempA2 ) { - pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempA1), Ivy_Not(pTempA2), IVY_AND, IVY_INIT_NONE) ); + pTemp = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pTempA1), Ivy_Not(pTempA2), IVY_AND, IVY_INIT_NONE) ); if ( pTemp ) return Ivy_Not(pTemp); } Count0 = (pTempA1 != NULL) + (pTempA2 != NULL); // implement the second MUX (F' = C * x1' + C' * x0') - pTempB1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC, Ivy_Not(p1), IVY_AND, IVY_INIT_NONE) ); - pTempB2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), Ivy_Not(p0), IVY_AND, IVY_INIT_NONE) ); + pTempB1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pC, Ivy_Not(p1), IVY_AND, IVY_INIT_NONE) ); + pTempB2 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pC), Ivy_Not(p0), IVY_AND, IVY_INIT_NONE) ); if ( pTempB1 && pTempB2 ) { - pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempB1), Ivy_Not(pTempB2), IVY_AND, IVY_INIT_NONE) ); + pTemp = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pTempB1), Ivy_Not(pTempB2), IVY_AND, IVY_INIT_NONE) ); if ( pTemp ) return pTemp; } Count1 = (pTempB1 != NULL) + (pTempB2 != NULL); // compare and decide which one to implement if ( Count0 >= Count1 ) { - pTempA1 = pTempA1? pTempA1 : Ivy_And(pC, p1); - pTempA2 = pTempA2? pTempA2 : Ivy_And(Ivy_Not(pC), p0); - return Ivy_Or( pTempA1, pTempA2 ); + pTempA1 = pTempA1? pTempA1 : Ivy_And(p, pC, p1); + pTempA2 = pTempA2? pTempA2 : Ivy_And(p, Ivy_Not(pC), p0); + return Ivy_Or( p, pTempA1, pTempA2 ); } - pTempB1 = pTempB1? pTempB1 : Ivy_And(pC, Ivy_Not(p1)); - pTempB2 = pTempB2? pTempB2 : Ivy_And(Ivy_Not(pC), Ivy_Not(p0)); - return Ivy_Not( Ivy_Or( pTempB1, pTempB2 ) ); + pTempB1 = pTempB1? pTempB1 : Ivy_And(p, pC, Ivy_Not(p1)); + pTempB2 = pTempB2? pTempB2 : Ivy_And(p, Ivy_Not(pC), Ivy_Not(p0)); + return Ivy_Not( Ivy_Or( p, pTempB1, pTempB2 ) ); // return Ivy_Or( Ivy_And(pC, p1), Ivy_And(Ivy_Not(pC), p0) ); } @@ -219,9 +203,9 @@ Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC ) +Ivy_Obj_t * Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC ) { - return Ivy_Or( Ivy_Or(Ivy_And(pA, pB), Ivy_And(pA, pC)), Ivy_And(pB, pC) ); + return Ivy_Or( p, Ivy_Or(p, Ivy_And(p, pA, pB), Ivy_And(p, pA, pC)), Ivy_And(p, pB, pC) ); } /**Function************************************************************* @@ -235,16 +219,32 @@ Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_Miter( Vec_Ptr_t * vPairs ) +Ivy_Obj_t * Ivy_Miter( Ivy_Man_t * p, Vec_Ptr_t * vPairs ) { int i; assert( vPairs->nSize > 0 ); assert( vPairs->nSize % 2 == 0 ); // go through the cubes of the node's SOP for ( i = 0; i < vPairs->nSize; i += 2 ) - vPairs->pArray[i/2] = Ivy_Not( Ivy_Exor( vPairs->pArray[i], vPairs->pArray[i+1] ) ); + vPairs->pArray[i/2] = Ivy_Not( Ivy_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) ); vPairs->nSize = vPairs->nSize/2; - return Ivy_Not( Ivy_Multi_rec( (Ivy_Obj_t **)vPairs->pArray, vPairs->nSize, IVY_AND ) ); + return Ivy_Not( Ivy_Multi_rec( p, (Ivy_Obj_t **)vPairs->pArray, vPairs->nSize, IVY_AND ) ); +} + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init ) +{ + return Ivy_CanonLatch( p, pObj, Init ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyResyn.c b/src/temp/ivy/ivyResyn.c index 2d65e7f7..804bdfb4 100644 --- a/src/temp/ivy/ivyResyn.c +++ b/src/temp/ivy/ivyResyn.c @@ -39,50 +39,59 @@ SeeAlso [] ***********************************************************************/ -Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel ) +Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose ) { - int clk, fVerbose = 0; + 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 ); // Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 ); clk = clock(); -if ( fVerbose ) Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 ); + Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 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 ); // Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 ); clk = clock(); Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 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; diff --git a/src/temp/ivy/ivyRewrite.c b/src/temp/ivy/ivyRewrite.c deleted file mode 100644 index 031db9bc..00000000 --- a/src/temp/ivy/ivyRewrite.c +++ /dev/null @@ -1,365 +0,0 @@ -/**CFile**************************************************************** - - FileName [ivyRewrite.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [And-Inverter Graph package.] - - Synopsis [AIG rewriting.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 11, 2006.] - - Revision [$Id: ivyRewrite.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "ivy.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static unsigned Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront ); -static void Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone ); -static int Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs Boolean rewriting of sequential AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ) -{ - Vec_Int_t * vNodes, * vFront, * vInside, * vTree; - Ivy_Obj_t * pNode, * pNodeNew, * pTemp; - int i, k, nCostOld, nCostInt, nCostInt2, nCostNew, RetValue, Entry, nRefsSaved, nInputs; - int clk, clkCut = 0, clkTru = 0, clkDsd = 0, clkUpd = 0, clkStart = clock(); - unsigned uTruth; - - nInputs = 4; - vTree = Vec_IntAlloc( 8 ); - vFront = Vec_IntAlloc( 8 ); - vInside = Vec_IntAlloc( 50 ); - vNodes = Ivy_ManDfs( p ); - Ivy_ManForEachNodeVec( p, vNodes, pNode, i ) - { - if ( Ivy_ObjIsBuf(pNode) ) - continue; - // fix the fanin buffer problem - Ivy_NodeFixBufferFanins( pNode ); - if ( Ivy_ObjIsBuf(pNode) ) - continue; - - // find one sequential cut rooted at this node -clk = clock(); - Ivy_ManSeqFindCut( pNode, vFront, vInside, nInputs ); -clkCut += clock() - clk; - // compute the truth table of the cut -clk = clock(); - uTruth = Ivy_ManSeqFindTruth( pNode, vFront ); -clkTru += clock() - clk; - // decompose the truth table -clk = clock(); - RetValue = Ivy_TruthDsd( uTruth, vTree ); -clkDsd += clock() - clk; - if ( !RetValue ) - continue; // DSD does not exist -// Ivy_TruthDsdPrint( stdout, vTree ); - -clk = clock(); - // remember the cost of the current network - nCostOld = Ivy_ManGetCost(p); - // increment references of the cut variables - Vec_IntForEachEntry( vFront, Entry, k ) - { - pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); - Ivy_ObjRefsInc( pTemp ); - } - // dereference and record undo - nRefsSaved = pNode->nRefs; pNode->nRefs = 0; - Ivy_ManUndoStart( p ); - Ivy_ObjDelete_rec( pNode, 0 ); - Ivy_ManUndoStop( p ); - pNode->nRefs = nRefsSaved; - - // get the intermediate cost - nCostInt = Ivy_ManGetCost(p); - -// printf( "Removed by dereferencing = %d.\n", nCostOld - nCostInt ); - - // construct the new logic cone - pNodeNew = Ivy_ManDsdConstruct( p, vFront, vTree ); - // remember the cost - nCostNew = Ivy_ManGetCost(p); - -// printf( "Added by dereferencing = %d.\n", nCostInt - nCostNew ); -// nCostNew = nCostNew; - -/* - if ( Ivy_Regular(pNodeNew)->nRefs == 0 ) - Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 ); - // get the intermediate cost - nCostInt2 = Ivy_ManGetCost(p); - assert( nCostInt == nCostInt2 ); - - Ivy_ManUndoPerform( p, pNode ); - pNode->nRefs = nRefsSaved; - - Vec_IntForEachEntry( vFront, Entry, k ) - { -// pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); - pTemp = Ivy_ManObj(p, Entry); - Ivy_ObjRefsDec( pTemp ); - } -clkUpd += clock() - clk; - continue; -*/ - - // detect the case when they are exactly the same -// if ( pNodeNew == pNode ) -// continue; - - // compare the costs - if ( nCostOld > nCostNew || nCostOld == nCostNew && fUseZeroCost ) - { // accept the change -// printf( "NODES GAINED = %d\n", nCostOld - nCostNew ); - - Ivy_ObjReplace( pNode, pNodeNew, 0, 1 ); - pNode->nRefs = nRefsSaved; - } - else - { // reject change -// printf( "Rejected\n" ); - - if ( Ivy_Regular(pNodeNew)->nRefs == 0 ) - Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 ); - - // get the intermediate cost - nCostInt2 = Ivy_ManGetCost(p); - assert( nCostInt == nCostInt2 ); - - // reconstruct the old node - Ivy_ManUndoPerform( p, pNode ); - pNode->nRefs = nRefsSaved; - } - // decrement references of the cut variables - Vec_IntForEachEntry( vFront, Entry, k ) - { -// pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); - pTemp = Ivy_ManObj(p, Entry); - if ( Ivy_ObjIsNone(pTemp) ) - continue; - Ivy_ObjRefsDec( pTemp ); - if ( Ivy_ObjRefs(pTemp) == 0 ) - Ivy_ObjDelete_rec( pTemp, 1 ); - } - -clkUpd += clock() - clk; - } - -PRT( "Cut ", clkCut ); -PRT( "Truth ", clkTru ); -PRT( "DSD ", clkDsd ); -PRT( "Update ", clkUpd ); -PRT( "TOTAL ", clock() - clkStart ); - - Vec_IntFree( vTree ); - Vec_IntFree( vFront ); - Vec_IntFree( vInside ); - Vec_IntFree( vNodes ); - - if ( !Ivy_ManCheck(p) ) - { - printf( "Ivy_ManSeqRewrite(): The check has failed.\n" ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Computes the truth table of the sequential cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned Ivy_ManSeqFindTruth_rec( Ivy_Man_t * p, unsigned Node, Vec_Int_t * vFront ) -{ - static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; - unsigned uTruth0, uTruth1; - Ivy_Obj_t * pNode; - int nLatches, Number; - // consider the case of a constant - if ( Node == 0 ) - return ~((unsigned)0); - // try to find this node in the frontier - Number = Vec_IntFind( vFront, Node ); - if ( Number >= 0 ) - return uMasks[Number]; - // get the node - pNode = Ivy_ManObj( p, Ivy_LeafId(Node) ); - assert( !Ivy_ObjIsPi(pNode) && !Ivy_ObjIsConst1(pNode) ); - // get the number of latches - nLatches = Ivy_LeafLat(Node) + Ivy_ObjIsLatch(pNode); - // expand the first fanin - uTruth0 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId0(pNode), nLatches), vFront ); - if ( Ivy_ObjFaninC0(pNode) ) - uTruth0 = ~uTruth0; - // quit if this is the one fanin node - if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ) - return uTruth0; - assert( Ivy_ObjIsNode(pNode) ); - // expand the second fanin - uTruth1 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId1(pNode), nLatches), vFront ); - if ( Ivy_ObjFaninC1(pNode) ) - uTruth1 = ~uTruth1; - // return the truth table - return Ivy_ObjIsAnd(pNode)? uTruth0 & uTruth1 : uTruth0 ^ uTruth1; -} - -/**Function************************************************************* - - Synopsis [Computes the truth table of the sequential cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront ) -{ - assert( Ivy_ObjIsNode(pNode) ); - return Ivy_ManSeqFindTruth_rec( Ivy_ObjMan(pNode), Ivy_LeafCreate(pNode->Id, 0), vFront ); -} - - -/**Function************************************************************* - - Synopsis [Recursively dereferences the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManSeqDeref_rec( Ivy_Obj_t * pNode, Vec_Int_t * vCone ) -{ - Ivy_Obj_t * pFan; - assert( !Ivy_IsComplement(pNode) ); - assert( !Ivy_ObjIsNone(pNode) ); - if ( Ivy_ObjIsPi(pNode) ) - return; - // deref the first fanin - pFan = Ivy_ObjFanin0(pNode); - Ivy_ObjRefsDec( pFan ); - if ( Ivy_ObjRefs( pFan ) == 0 ) - Ivy_ManSeqDeref_rec( pFan, vCone ); - // deref the second fanin - pFan = Ivy_ObjFanin1(pNode); - Ivy_ObjRefsDec( pFan ); - if ( Ivy_ObjRefs( pFan ) == 0 ) - Ivy_ManSeqDeref_rec( pFan, vCone ); - // save the node - Vec_IntPush( vCone, pNode->Id ); -} - -/**Function************************************************************* - - Synopsis [Recursively references the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManSeqRef_rec( Ivy_Obj_t * pNode ) -{ - Ivy_Obj_t * pFan; - assert( !Ivy_IsComplement(pNode) ); - assert( !Ivy_ObjIsNone(pNode) ); - if ( Ivy_ObjIsPi(pNode) ) - return; - // ref the first fanin - pFan = Ivy_ObjFanin0(pNode); - if ( Ivy_ObjRefs( pFan ) == 0 ) - Ivy_ManSeqRef_rec( pFan ); - Ivy_ObjRefsInc( pFan ); - // ref the second fanin - pFan = Ivy_ObjFanin1(pNode); - if ( Ivy_ObjRefs( pFan ) == 0 ) - Ivy_ManSeqRef_rec( pFan ); - Ivy_ObjRefsInc( pFan ); -} - -/**Function************************************************************* - - Synopsis [Collect MFFC of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone ) -{ - Vec_IntClear( vCone ); - Ivy_ManSeqDeref_rec( pNode, vCone ); - Ivy_ManSeqRef_rec( pNode ); -} - -/**Function************************************************************* - - Synopsis [Computes the cost of the logic cone.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone ) -{ - Ivy_Obj_t * pObj; - int i, Cost = 0; - Ivy_ManForEachNodeVec( p, vCone, pObj, i ) - { - if ( Ivy_ObjIsAnd(pObj) ) - Cost += 1; - else if ( Ivy_ObjIsExor(pObj) ) - Cost += 2; - } - return 0; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c index 243ab261..d2a1697e 100644 --- a/src/temp/ivy/ivyRwrPre.c +++ b/src/temp/ivy/ivyRwrPre.c @@ -27,13 +27,13 @@ //////////////////////////////////////////////////////////////////////// static unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums ); -static int Ivy_NodeMffcLabel( Ivy_Obj_t * pObj ); -static int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost ); -static Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, +static int Ivy_NodeMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj ); +static int Ivy_NodeRewrite( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost ); +static Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth ); -static int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ); -static void Ivy_GraphUpdateNetwork( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain ); +static int Ivy_GraphToNetworkCount( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ); +static void Ivy_GraphUpdateNetwork( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -58,29 +58,30 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV int clk, clkStart = clock(); // start the rewriting manager pManRwt = Rwt_ManStart( 0 ); + p->pData = pManRwt; if ( pManRwt == NULL ) - return 0; + return 0; + // create fanouts + if ( fUpdateLevel && p->vFanouts == NULL ) + Ivy_ManStartFanout( p ); // compute the reverse levels if level update is requested if ( fUpdateLevel ) Ivy_ManRequiredLevels( p ); + // set the number of levels +// p->nLevelMax = Ivy_ManLevels( p ); // resynthesize each node once - nNodes = Ivy_ManObjIdNext( p ); - Ivy_ManForEachObj( p, pNode, i ) + nNodes = Ivy_ManObjIdMax(p); + Ivy_ManForEachNode( p, pNode, i ) { - if ( !Ivy_ObjIsNode(pNode) ) - continue; // fix the fanin buffer problem - Ivy_NodeFixBufferFanins( pNode ); + Ivy_NodeFixBufferFanins( p, pNode ); if ( Ivy_ObjIsBuf(pNode) ) continue; // stop if all nodes have been tried once - if ( i >= nNodes ) + if ( i > nNodes ) break; - // skip the nodes with many fanouts -// if ( Ivy_ObjRefs(pNode) > 1000 ) -// continue; // for each cut, try to resynthesize it - nGain = Rwt_NodeRewrite( pManRwt, pNode, fUpdateLevel, fUseZeroCost ); + nGain = Ivy_NodeRewrite( p, pManRwt, pNode, fUpdateLevel, fUseZeroCost ); if ( nGain > 0 || nGain == 0 && fUseZeroCost ) { Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt); @@ -104,7 +105,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV // complement the FF if needed clk = clock(); if ( fCompl ) Dec_GraphComplement( pGraph ); - Ivy_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain ); + Ivy_GraphUpdateNetwork( p, pNode, pGraph, fUpdateLevel, nGain ); if ( fCompl ) Dec_GraphComplement( pGraph ); Rwt_ManAddTimeUpdate( pManRwt, clock() - clk ); } @@ -115,9 +116,12 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart ); Rwt_ManPrintStats( pManRwt ); // delete the managers Rwt_ManStop( pManRwt ); + p->pData = NULL; // fix the levels if ( fUpdateLevel ) Vec_IntFree( p->vRequired ), p->vRequired = NULL; +// else +// Ivy_ManResetLevels( p ); // check if ( i = Ivy_ManCleanup(p) ) printf( "Cleanup after rewriting removed %d dangling nodes.\n", i ); @@ -144,7 +148,7 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart ); SeeAlso [] ***********************************************************************/ -int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost ) +int Ivy_NodeRewrite( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost ) { int fVeryVerbose = 0; Dec_Graph_t * pGraph; @@ -159,10 +163,10 @@ int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUs p->nNodesConsidered++; // get the required times - Required = fUpdateLevel? Vec_IntEntry( Ivy_ObjMan(pNode)->vRequired, pNode->Id ) : 1000000; + Required = fUpdateLevel? Vec_IntEntry( pMan->vRequired, pNode->Id ) : 1000000; // get the node's cuts clk = clock(); - pStore = Ivy_NodeFindCutsAll( pNode, 5 ); + pStore = Ivy_NodeFindCutsAll( pMan, pNode, 5 ); p->timeCut += clock() - clk; // go through the cuts @@ -175,14 +179,10 @@ clk = clock(); continue; // skip the cuts with buffers for ( i = 0; i < (int)pCut->nSize; i++ ) - if ( Ivy_ObjIsBuf( Ivy_ObjObj(pNode, pCut->pArray[i]) ) ) + if ( Ivy_ObjIsBuf( Ivy_ManObj(pMan, pCut->pArray[i]) ) ) break; if ( i != pCut->nSize ) continue; - -// if ( pNode->Id == 82 ) -// Ivy_NodePrintCut( pCut ); - // get the fanin permutation clk2 = clock(); uTruth = 0xFFFF & Ivy_NodeGetTruth( pNode, pCut->pArray, pCut->nSize ); // truth table @@ -194,7 +194,7 @@ p->timeTruth += clock() - clk2; Vec_PtrFill( p->vFaninsCur, (int)pCut->nSize, 0 ); for ( i = 0; i < (int)pCut->nSize; i++ ) { - pFanin = Ivy_ObjObj( pNode, pCut->pArray[pPerm[i]] ); + pFanin = Ivy_ManObj( pMan, pCut->pArray[pPerm[i]] ); assert( Ivy_ObjIsNode(pFanin) || Ivy_ObjIsCi(pFanin) ); pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) ); Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin ); @@ -210,8 +210,8 @@ clk2 = clock(); Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) Ivy_ObjRefsInc( Ivy_Regular(pFanin) ); // label MFFC with current ID - Ivy_ManIncrementTravId( Ivy_ObjMan(pNode) ); - nNodesSaved = Ivy_NodeMffcLabel( pNode ); + Ivy_ManIncrementTravId( pMan ); + nNodesSaved = Ivy_NodeMffcLabel( pMan, pNode ); // unmark the fanin boundary Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) Ivy_ObjRefsDec( Ivy_Regular(pFanin) ); @@ -219,7 +219,7 @@ p->timeMffc += clock() - clk2; // evaluate the cut clk2 = clock(); - pGraph = Rwt_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth ); + pGraph = Rwt_CutEvaluate( pMan, p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth ); p->timeEval += clock() - clk2; // check if the cut is better than the current best one @@ -301,13 +301,13 @@ p->timeRes += clock() - clk; SeeAlso [] ***********************************************************************/ -int Ivy_NodeRefDeref( Ivy_Obj_t * pNode, int fReference, int fLabel ) +int Ivy_NodeRefDeref( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fReference, int fLabel ) { Ivy_Obj_t * pNode0, * pNode1; int Counter; // label visited nodes if ( fLabel ) - Ivy_ObjSetTravIdCurrent( pNode ); + Ivy_ObjSetTravIdCurrent( p, pNode ); // skip the CI if ( Ivy_ObjIsCi(pNode) ) return 0; @@ -319,18 +319,18 @@ int Ivy_NodeRefDeref( Ivy_Obj_t * pNode, int fReference, int fLabel ) if ( fReference ) { if ( pNode0->nRefs++ == 0 ) - Counter += Ivy_NodeRefDeref( pNode0, fReference, fLabel ); - if ( Ivy_ObjIsNode(pNode) && pNode1->nRefs++ == 0 ) - Counter += Ivy_NodeRefDeref( pNode1, fReference, fLabel ); + Counter += Ivy_NodeRefDeref( p, pNode0, fReference, fLabel ); + if ( pNode1 && pNode1->nRefs++ == 0 ) + Counter += Ivy_NodeRefDeref( p, pNode1, fReference, fLabel ); } else { assert( pNode0->nRefs > 0 ); - assert( pNode1->nRefs > 0 ); + assert( pNode1 == NULL || pNode1->nRefs > 0 ); if ( --pNode0->nRefs == 0 ) - Counter += Ivy_NodeRefDeref( pNode0, fReference, fLabel ); - if ( Ivy_ObjIsNode(pNode) && --pNode1->nRefs == 0 ) - Counter += Ivy_NodeRefDeref( pNode1, fReference, fLabel ); + Counter += Ivy_NodeRefDeref( p, pNode0, fReference, fLabel ); + if ( pNode1 && --pNode1->nRefs == 0 ) + Counter += Ivy_NodeRefDeref( p, pNode1, fReference, fLabel ); } return Counter; } @@ -346,13 +346,13 @@ int Ivy_NodeRefDeref( Ivy_Obj_t * pNode, int fReference, int fLabel ) SeeAlso [] ***********************************************************************/ -int Ivy_NodeMffcLabel( Ivy_Obj_t * pNode ) +int Ivy_NodeMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pNode ) { int nConeSize1, nConeSize2; assert( !Ivy_IsComplement( pNode ) ); assert( Ivy_ObjIsNode( pNode ) ); - nConeSize1 = Ivy_NodeRefDeref( pNode, 0, 1 ); // dereference - nConeSize2 = Ivy_NodeRefDeref( pNode, 1, 0 ); // reference + nConeSize1 = Ivy_NodeRefDeref( p, pNode, 0, 1 ); // dereference + nConeSize2 = Ivy_NodeRefDeref( p, pNode, 1, 0 ); // reference assert( nConeSize1 == nConeSize2 ); assert( nConeSize1 > 0 ); return nConeSize1; @@ -418,7 +418,7 @@ unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums ) SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth ) +Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth ) { Vec_Ptr_t * vSubgraphs; Dec_Graph_t * pGraphBest, * pGraphCur; @@ -437,7 +437,7 @@ Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCu Vec_PtrForEachEntry( vFaninsCur, pFanin, k ) Dec_GraphNode(pGraphCur, k)->pFunc = pFanin; // detect how many unlabeled nodes will be reused - nNodesAdded = Ivy_GraphToNetworkCount( pRoot, pGraphCur, nNodesSaved, LevelMax ); + nNodesAdded = Ivy_GraphToNetworkCount( pMan, pRoot, pGraphCur, nNodesSaved, LevelMax ); if ( nNodesAdded == -1 ) continue; assert( nNodesSaved >= nNodesAdded ); @@ -469,7 +469,7 @@ Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCu SeeAlso [] ***********************************************************************/ -int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ) +int Ivy_GraphToNetworkCount( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ) { Dec_Node_t * pNode, * pNode0, * pNode1; Ivy_Obj_t * pAnd, * pAnd0, * pAnd1; @@ -495,7 +495,7 @@ int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa // if they are both present, find the resulting node pAnd0 = Ivy_NotCond( pAnd0, pNode->eEdge0.fCompl ); pAnd1 = Ivy_NotCond( pAnd1, pNode->eEdge1.fCompl ); - pAnd = Ivy_TableLookup( Ivy_ObjCreateGhost(pAnd0, pAnd1, IVY_AND, IVY_INIT_NONE) ); + pAnd = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pAnd0, pAnd1, IVY_AND, IVY_INIT_NONE) ); // return -1 if the node is the same as the original root if ( Ivy_Regular(pAnd) == pRoot ) return -1; @@ -503,7 +503,7 @@ int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa else pAnd = NULL; // count the number of added nodes - if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(Ivy_Regular(pAnd)) ) + if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(p, Ivy_Regular(pAnd)) ) { if ( ++Counter > NodeMax ) return -1; @@ -512,7 +512,7 @@ int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa LevelNew = 1 + RWT_MAX( pNode0->Level, pNode1->Level ); if ( pAnd ) { - if ( Ivy_Regular(pAnd) == Ivy_ObjConst1(pRoot) ) + if ( Ivy_Regular(pAnd) == p->pConst1 ) LevelNew = 0; else if ( Ivy_Regular(pAnd) == Ivy_Regular(pAnd0) ) LevelNew = (int)Ivy_Regular(pAnd0)->Level; @@ -541,14 +541,14 @@ int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * pMan, Dec_Graph_t * pGraph ) +Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * p, Dec_Graph_t * pGraph ) { Ivy_Obj_t * pAnd0, * pAnd1; Dec_Node_t * pNode; int i; // check for constant function if ( Dec_GraphIsConst(pGraph) ) - return Ivy_NotCond( Ivy_ManConst1(pMan), Dec_GraphIsComplement(pGraph) ); + return Ivy_NotCond( Ivy_ManConst1(p), Dec_GraphIsComplement(pGraph) ); // check for a literal if ( Dec_GraphIsVar(pGraph) ) return Ivy_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) ); @@ -557,7 +557,7 @@ Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * pMan, Dec_Graph_t * pGraph ) { pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); - pNode->pFunc = Ivy_And( pAnd0, pAnd1 ); + pNode->pFunc = Ivy_And( p, pAnd0, pAnd1 ); } // complement the result if necessary return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) ); @@ -574,18 +574,96 @@ Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * pMan, Dec_Graph_t * pGraph ) SeeAlso [] ***********************************************************************/ -void Ivy_GraphUpdateNetwork( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain ) +void Ivy_GraphUpdateNetwork( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain ) { Ivy_Obj_t * pRootNew; - int nNodesNew, nNodesOld; - nNodesOld = Ivy_ManNodeNum(Ivy_ObjMan(pRoot)); + int nNodesNew, nNodesOld, Required; + Required = fUpdateLevel? Vec_IntEntry( p->vRequired, pRoot->Id ) : 1000000; + nNodesOld = Ivy_ManNodeNum(p); // create the new structure of nodes - pRootNew = Ivy_GraphToNetwork( Ivy_ObjMan(pRoot), pGraph ); + pRootNew = Ivy_GraphToNetwork( p, pGraph ); + assert( (int)Ivy_Regular(pRootNew)->Level <= Required ); +// if ( Ivy_Regular(pRootNew)->Level == Required ) +// printf( "Difference %d.\n", Ivy_Regular(pRootNew)->Level - Required ); // remove the old nodes // Ivy_AigReplace( pMan->pManFunc, pRoot, pRootNew, fUpdateLevel ); - Ivy_ObjReplace( pRoot, pRootNew, 1, 0 ); +/* + if ( Ivy_IsComplement(pRootNew) ) + printf( "c" ); + else + printf( "d" ); + if ( Ivy_ObjRefs(Ivy_Regular(pRootNew)) > 0 ) + printf( "%d", Ivy_ObjRefs(Ivy_Regular(pRootNew)) ); + printf( " " ); +*/ + Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0 ); + // compare the gains + nNodesNew = Ivy_ManNodeNum(p); + assert( nGain <= nNodesOld - nNodesNew ); + // propagate the buffer + Ivy_ManPropagateBuffers( p ); +} + +/**Function************************************************************* + + Synopsis [Replaces MFFC of the node by the new factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_GraphUpdateNetwork3( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain ) +{ + Ivy_Obj_t * pRootNew, * pFanin; + int nNodesNew, nNodesOld, i, nRefsOld; + nNodesOld = Ivy_ManNodeNum(p); + +//printf( "Before = %d. ", Ivy_ManNodeNum(p) ); + // mark the cut + Vec_PtrForEachEntry( ((Rwt_Man_t *)p->pData)->vFanins, pFanin, i ) + Ivy_ObjRefsInc( Ivy_Regular(pFanin) ); + // deref the old cone + nRefsOld = pRoot->nRefs; + pRoot->nRefs = 0; + Ivy_ObjDelete_rec( p, pRoot, 0 ); + pRoot->nRefs = nRefsOld; + // unmark the cut + Vec_PtrForEachEntry( ((Rwt_Man_t *)p->pData)->vFanins, pFanin, i ) + Ivy_ObjRefsDec( Ivy_Regular(pFanin) ); +//printf( "Deref = %d. ", Ivy_ManNodeNum(p) ); + + // create the new structure of nodes + pRootNew = Ivy_GraphToNetwork( p, pGraph ); +//printf( "Create = %d. ", Ivy_ManNodeNum(p) ); + // remove the old nodes +// Ivy_AigReplace( pMan->pManFunc, pRoot, pRootNew, fUpdateLevel ); +/* + if ( Ivy_IsComplement(pRootNew) ) + printf( "c" ); + else + printf( "d" ); + if ( Ivy_ObjRefs(Ivy_Regular(pRootNew)) > 0 ) + printf( "%d", Ivy_ObjRefs(Ivy_Regular(pRootNew)) ); + printf( " " ); +*/ + Ivy_ObjReplace( p, pRoot, pRootNew, 0, 0 ); +//printf( "Replace = %d. ", Ivy_ManNodeNum(p) ); + + // delete remaining dangling nodes + Vec_PtrForEachEntry( ((Rwt_Man_t *)p->pData)->vFanins, pFanin, i ) + { + pFanin = Ivy_Regular(pFanin); + if ( !Ivy_ObjIsNone(pFanin) && Ivy_ObjRefs(pFanin) == 0 ) + Ivy_ObjDelete_rec( p, pFanin, 1 ); + } +//printf( "Deref = %d. ", Ivy_ManNodeNum(p) ); +//printf( "\n" ); + // compare the gains - nNodesNew = Ivy_ManNodeNum(Ivy_ObjMan(pRoot)); + nNodesNew = Ivy_ManNodeNum(p); assert( nGain <= nNodesOld - nNodesNew ); } diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c index d8fbdd9b..1cfa8c4b 100644 --- a/src/temp/ivy/ivySeq.c +++ b/src/temp/ivy/ivySeq.c @@ -24,13 +24,33 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Converts a combinational AIG manager into a sequential one.] + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + + + + + + +/**Function************************************************************* + + Synopsis [Derives new cut.] Description [] @@ -39,59 +59,360 @@ SeeAlso [] ***********************************************************************/ -void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches ) +static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 ) { - Vec_Int_t * vNodes; - Ivy_Obj_t * pObj, * pObjNew, * pFan0, * pFan1; - int i, fChanges; - assert( nLatches < Ivy_ManPiNum(p) && nLatches < Ivy_ManPoNum(p) ); - // change POs into buffers - assert( Ivy_ManPoNum(p) == Vec_IntSize(p->vPos) ); - for ( i = Ivy_ManPoNum(p) - nLatches; i < Vec_IntSize(p->vPos); i++ ) + unsigned uHash = 0; + int i, k; + assert( pCut->nSize > 0 ); + assert( IdNew0 < IdNew1 ); + for ( i = k = 0; i < pCut->nSize; i++ ) { - pObj = Ivy_ManPo(p, i); - pObj->Type = IVY_BUF; + if ( pCut->pArray[i] == IdOld ) + continue; + if ( IdNew0 >= 0 ) + { + if ( IdNew0 <= pCut->pArray[i] ) + { + if ( IdNew0 < pCut->pArray[i] ) + { + if ( k == pCut->nSizeMax ) + return 0; + pCutNew->pArray[ k++ ] = IdNew0; + uHash |= Ivy_CutHashValue( IdNew0 ); + } + IdNew0 = -1; + } + } + if ( IdNew1 >= 0 ) + { + if ( IdNew1 <= pCut->pArray[i] ) + { + if ( IdNew1 < pCut->pArray[i] ) + { + if ( k == pCut->nSizeMax ) + return 0; + pCutNew->pArray[ k++ ] = IdNew1; + uHash |= Ivy_CutHashValue( IdNew1 ); + } + IdNew1 = -1; + } + } + if ( k == pCut->nSizeMax ) + return 0; + pCutNew->pArray[ k++ ] = pCut->pArray[i]; + uHash |= Ivy_CutHashValue( pCut->pArray[i] ); } - // change PIs into latches and connect them to the corresponding POs - assert( Ivy_ManPiNum(p) == Vec_IntSize(p->vPis) ); - for ( i = Ivy_ManPiNum(p) - nLatches; i < Vec_IntSize(p->vPis); i++ ) + if ( IdNew0 >= 0 ) { - pObj = Ivy_ManPi(p, i); - pObj->Type = IVY_LATCH; - Ivy_ObjConnect( pObj, Ivy_ManPo(p, Ivy_ManPoNum(p) - Ivy_ManPiNum(p)) ); + if ( k == pCut->nSizeMax ) + return 0; + pCutNew->pArray[ k++ ] = IdNew0; + uHash |= Ivy_CutHashValue( IdNew0 ); } - // shrink the array - Vec_IntShrink( p->vPis, Ivy_ManPiNum(p) - nLatches ); - Vec_IntShrink( p->vPos, Ivy_ManPoNum(p) - nLatches ); - // update the counters of different objects - p->nObjs[IVY_PI] -= nLatches; - p->nObjs[IVY_PO] -= nLatches; - p->nObjs[IVY_BUF] += nLatches; - p->nObjs[IVY_LATCH] += nLatches; - // perform structural hashing while there are changes - fChanges = 1; - while ( fChanges ) + if ( IdNew1 >= 0 ) { - fChanges = 0; - vNodes = Ivy_ManDfs( p ); - Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) + if ( k == pCut->nSizeMax ) + return 0; + pCutNew->pArray[ k++ ] = IdNew1; + uHash |= Ivy_CutHashValue( IdNew1 ); + } + pCutNew->nSize = k; + pCutNew->uHash = uHash; + assert( pCutNew->nSize <= pCut->nSizeMax ); + for ( i = 1; i < pCutNew->nSize; i++ ) + assert( pCutNew->pArray[i-1] < pCutNew->pArray[i] ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pDom is contained in pCut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_CutCheckDominance( Ivy_Cut_t * pDom, Ivy_Cut_t * pCut ) +{ + int i, k; + for ( i = 0; i < pDom->nSize; i++ ) + { + assert( i==0 || pDom->pArray[i-1] < pDom->pArray[i] ); + for ( k = 0; k < pCut->nSize; k++ ) + if ( pDom->pArray[i] == pCut->pArray[k] ) + break; + if ( k == pCut->nSize ) // node i in pDom is not contained in pCut + return 0; + } + // every node in pDom is contained in pCut + return 1; +} + +/**Function************************************************************* + + Synopsis [Check if the cut exists.] + + Description [Returns 1 if the cut exists.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_CutFindOrAddFilter( Ivy_Store_t * pCutStore, Ivy_Cut_t * pCutNew ) +{ + Ivy_Cut_t * pCut; + int i, k; + assert( pCutNew->uHash ); + // try to find the cut + for ( i = 0; i < pCutStore->nCuts; i++ ) + { + pCut = pCutStore->pCuts + i; + if ( pCut->nSize == 0 ) + continue; + if ( pCut->nSize == pCutNew->nSize ) + { + if ( pCut->uHash == pCutNew->uHash ) + { + for ( k = 0; k < pCutNew->nSize; k++ ) + if ( pCut->pArray[k] != pCutNew->pArray[k] ) + break; + if ( k == pCutNew->nSize ) + return 1; + } + continue; + } + if ( pCut->nSize < pCutNew->nSize ) { - if ( Ivy_ObjIsBuf(pObj) ) + // skip the non-contained cuts + if ( (pCut->uHash & pCutNew->uHash) != pCut->uHash ) continue; - pFan0 = Ivy_NodeRealFanin_rec( pObj, 0 ); - pFan1 = Ivy_NodeRealFanin_rec( pObj, 1 ); - if ( Ivy_ObjIsAnd(pObj) ) - pObjNew = Ivy_And(pFan0, pFan1); - else if ( Ivy_ObjIsExor(pObj) ) - pObjNew = Ivy_Exor(pFan0, pFan1); - else assert( 0 ); - if ( pObjNew == pObj ) + // check containment seriously + if ( Ivy_CutCheckDominance( pCut, pCutNew ) ) + return 1; + continue; + } + // check potential containment of other cut + + // skip the non-contained cuts + if ( (pCut->uHash & pCutNew->uHash) != pCutNew->uHash ) + continue; + // check containment seriously + if ( Ivy_CutCheckDominance( pCutNew, pCut ) ) + { + // remove the current cut + pCut->nSize = 0; + } + } + assert( pCutStore->nCuts < pCutStore->nCutsMax ); + // add the cut + pCut = pCutStore->pCuts + pCutStore->nCuts++; + *pCut = *pCutNew; + return 0; +} + +/**Function************************************************************* + + Synopsis [Compresses the cut representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_CutCompactAll( Ivy_Store_t * pCutStore ) +{ + Ivy_Cut_t * pCut; + int i, k; + pCutStore->nCutsM = 0; + for ( i = k = 0; i < pCutStore->nCuts; i++ ) + { + pCut = pCutStore->pCuts + i; + if ( pCut->nSize == 0 ) + continue; + if ( pCut->nSize < pCut->nSizeMax ) + pCutStore->nCutsM++; + pCutStore->pCuts[k++] = *pCut; + } + pCutStore->nCuts = k; +} + +/**Function************************************************************* + + Synopsis [Print the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_CutPrintForNode( Ivy_Cut_t * pCut ) +{ + int i; + assert( pCut->nSize > 0 ); + printf( "%d : {", pCut->nSize ); + for ( i = 0; i < pCut->nSize; i++ ) + printf( " %d", pCut->pArray[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_CutPrintForNodes( Ivy_Store_t * pCutStore ) +{ + int i; + printf( "Node %d\n", pCutStore->pCuts[0].pArray[0] ); + for ( i = 0; i < pCutStore->nCuts; i++ ) + Ivy_CutPrintForNode( pCutStore->pCuts + i ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_CutReadLeaf( Ivy_Obj_t * pFanin ) +{ + assert( !Ivy_IsComplement(pFanin) ); + if ( !Ivy_ObjIsLatch(pFanin) ) + return Ivy_LeafCreate( pFanin->Id, 0 ); + return 1 + Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Store_t * Ivy_CutComputeForNode( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves ) +{ + static Ivy_Store_t CutStore, * pCutStore = &CutStore; + Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut; + Ivy_Man_t * pMan = p; + Ivy_Obj_t * pLeaf; + int i, k, Temp, nLats, iLeaf0, iLeaf1; + + assert( nLeaves <= IVY_CUT_INPUT ); + + // start the structure + pCutStore->nCuts = 0; + pCutStore->nCutsMax = IVY_CUT_LIMIT; + // start the trivial cut + pCutNew->uHash = 0; + pCutNew->nSize = 1; + pCutNew->nSizeMax = nLeaves; + pCutNew->pArray[0] = Ivy_LeafCreate( pObj->Id, 0 ); + pCutNew->uHash = Ivy_CutHashValue( pCutNew->pArray[0] ); + // add the trivial cut + pCutStore->pCuts[pCutStore->nCuts++] = *pCutNew; + assert( pCutStore->nCuts == 1 ); + + // explore the cuts + for ( i = 0; i < pCutStore->nCuts; i++ ) + { + // expand this cut + pCut = pCutStore->pCuts + i; + if ( pCut->nSize == 0 ) + continue; + for ( k = 0; k < pCut->nSize; k++ ) + { + pLeaf = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[k]) ); + if ( Ivy_ObjIsCi(pLeaf) ) continue; - Ivy_ObjReplace( pObj, pObjNew, 1, 1 ); - fChanges = 1; + assert( Ivy_ObjIsNode(pLeaf) ); + nLats = Ivy_LeafLat(pCut->pArray[k]); + // get the fanins fanins + iLeaf0 = nLats + Ivy_CutReadLeaf( Ivy_ObjFanin0(pLeaf) ); + iLeaf1 = nLats + Ivy_CutReadLeaf( Ivy_ObjFanin1(pLeaf) ); + if ( iLeaf0 > iLeaf1 ) + Temp = iLeaf0, iLeaf0 = iLeaf1, iLeaf1 = Temp; + // create the new cut + if ( !Ivy_CutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 ) ) + continue; + // add the cut + Ivy_CutFindOrAddFilter( pCutStore, pCutNew ); + if ( pCutStore->nCuts == IVY_CUT_LIMIT ) + break; } - Vec_IntFree( vNodes ); + if ( pCutStore->nCuts == IVY_CUT_LIMIT ) + break; + } + if ( pCutStore->nCuts == IVY_CUT_LIMIT ) + pCutStore->fSatur = 1; + else + pCutStore->fSatur = 0; +// printf( "%d ", pCutStore->nCuts ); + Ivy_CutCompactAll( pCutStore ); +// printf( "%d \n", pCutStore->nCuts ); +// Ivy_CutPrintForNodes( pCutStore ); + return pCutStore; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs ) +{ + Ivy_Store_t * pStore; + Ivy_Obj_t * pObj; + int i, nCutsTotal, nCutsTotalM, nNodeTotal, nNodeOver; + int clk = clock(); + if ( nInputs > IVY_CUT_INPUT ) + { + printf( "Cannot compute cuts for more than %d inputs.\n", IVY_CUT_INPUT ); + return; + } + nNodeTotal = nNodeOver = 0; + nCutsTotal = nCutsTotalM = -Ivy_ManNodeNum(p); + Ivy_ManForEachObj( p, pObj, i ) + { + if ( !Ivy_ObjIsNode(pObj) ) + continue; + pStore = Ivy_CutComputeForNode( p, pObj, nInputs ); + nCutsTotal += pStore->nCuts; + nCutsTotalM += pStore->nCutsM; + nNodeOver += pStore->fSatur; + nNodeTotal++; } + printf( "All = %6d. Minus = %6d. Triv = %6d. Node = %6d. Satur = %6d. ", + nCutsTotal, nCutsTotalM, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver ); + PRT( "Time", clock() - clk ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyTable.c b/src/temp/ivy/ivyTable.c index 815caa29..f2617699 100644 --- a/src/temp/ivy/ivyTable.c +++ b/src/temp/ivy/ivyTable.c @@ -12,7 +12,7 @@ Affiliation [UC Berkeley] - Date [Ver. 1.0. Started - May 11, 2006.] + Date [Ver. 1.0. Started - May 11, 2006. ] Revision [$Id: ivyTable.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] @@ -37,22 +37,23 @@ static unsigned Ivy_Hash( Ivy_Obj_t * pObj, int TableSize ) } // returns the place where this node is stored (or should be stored) -static int * Ivy_TableFind( Ivy_Obj_t * pObj ) +static int * Ivy_TableFind( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { - Ivy_Man_t * p; int i; assert( Ivy_ObjIsHash(pObj) ); - p = Ivy_ObjMan(pObj); for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize ) if ( p->pTable[i] == pObj->Id ) break; return p->pTable + i; } +static void Ivy_TableResize( Ivy_Man_t * p ); +static unsigned int Cudd_PrimeAig( unsigned int p ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - + /**Function************************************************************* Synopsis [Checks if node with the given attributes is in the hash table.] @@ -64,27 +65,25 @@ static int * Ivy_TableFind( Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj ) +Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { - Ivy_Man_t * p; Ivy_Obj_t * pEntry; int i; assert( !Ivy_IsComplement(pObj) ); if ( !Ivy_ObjIsHash(pObj) ) return NULL; assert( Ivy_ObjIsLatch(pObj) || Ivy_ObjFaninId0(pObj) > 0 ); - assert( Ivy_ObjFaninId0(pObj) == 0 || Ivy_ObjFaninId0(pObj) > Ivy_ObjFaninId1(pObj) ); - p = Ivy_ObjMan(pObj); + assert( Ivy_ObjFaninId1(pObj) == 0 || Ivy_ObjFaninId0(pObj) < Ivy_ObjFaninId1(pObj) ); +// if ( Ivy_ObjFanin0(pObj)->nRefs == 0 || (!Ivy_ObjIsLatch(pObj) && Ivy_ObjFanin1(pObj)->nRefs == 0) ) +// return NULL; for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize ) { - pEntry = Ivy_ObjObj( pObj, p->pTable[i] ); - if ( Ivy_ObjFaninId0(pEntry) == Ivy_ObjFaninId0(pObj) && - Ivy_ObjFaninId1(pEntry) == Ivy_ObjFaninId1(pObj) && - Ivy_ObjFaninC0(pEntry) == Ivy_ObjFaninC0(pObj) && - Ivy_ObjFaninC1(pEntry) == Ivy_ObjFaninC1(pObj) && + pEntry = Ivy_ManObj( p, p->pTable[i] ); + if ( Ivy_ObjChild0(pEntry) == Ivy_ObjChild0(pObj) && + Ivy_ObjChild1(pEntry) == Ivy_ObjChild1(pObj) && Ivy_ObjInit(pEntry) == Ivy_ObjInit(pObj) && Ivy_ObjType(pEntry) == Ivy_ObjType(pObj) ) - return Ivy_ObjObj( pObj, p->pTable[i] ); + return pEntry; } return NULL; } @@ -100,13 +99,18 @@ Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Ivy_TableInsert( Ivy_Obj_t * pObj ) +void Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { int * pPlace; assert( !Ivy_IsComplement(pObj) ); if ( !Ivy_ObjIsHash(pObj) ) return; - pPlace = Ivy_TableFind( pObj ); + if ( (pObj->Id & 63) == 0 ) + { + if ( p->nTableSize < 2 * Ivy_ManHashObjNum(p) ) + Ivy_TableResize( p ); + } + pPlace = Ivy_TableFind( p, pObj ); assert( *pPlace == 0 ); *pPlace = pObj->Id; } @@ -122,25 +126,23 @@ void Ivy_TableInsert( Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Ivy_TableDelete( Ivy_Obj_t * pObj ) +void Ivy_TableDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { - Ivy_Man_t * p; Ivy_Obj_t * pEntry; int i, * pPlace; assert( !Ivy_IsComplement(pObj) ); if ( !Ivy_ObjIsHash(pObj) ) return; - pPlace = Ivy_TableFind( pObj ); + pPlace = Ivy_TableFind( p, pObj ); assert( *pPlace == pObj->Id ); // node should be in the table *pPlace = 0; // rehash the adjacent entries - p = Ivy_ObjMan(pObj); i = pPlace - p->pTable; for ( i = (i+1) % p->nTableSize; p->pTable[i]; i = (i+1) % p->nTableSize ) { - pEntry = Ivy_ObjObj( pObj, p->pTable[i] ); + pEntry = Ivy_ManObj( p, p->pTable[i] ); p->pTable[i] = 0; - Ivy_TableInsert( pEntry ); + Ivy_TableInsert( p, pEntry ); } } @@ -157,13 +159,13 @@ void Ivy_TableDelete( Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Ivy_TableUpdate( Ivy_Obj_t * pObj, int ObjIdNew ) +void Ivy_TableUpdate( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ObjIdNew ) { int * pPlace; assert( !Ivy_IsComplement(pObj) ); if ( !Ivy_ObjIsHash(pObj) ) return; - pPlace = Ivy_TableFind( pObj ); + pPlace = Ivy_TableFind( p, pObj ); assert( *pPlace == pObj->Id ); // node should be in the table *pPlace = ObjIdNew; } @@ -202,13 +204,12 @@ void Ivy_TableResize( Ivy_Man_t * p ) { int * pTableOld, * pPlace; int nTableSizeOld, Counter, e, clk; - assert( 0 ); clk = clock(); // save the old table pTableOld = p->pTable; nTableSizeOld = p->nTableSize; // get the new table - p->nTableSize = p->nObjsAlloc*5/2+13; + p->nTableSize = Cudd_PrimeAig( 5 * Ivy_ManHashObjNum(p) ); p->pTable = ALLOC( int, p->nTableSize ); memset( p->pTable, 0, sizeof(int) * p->nTableSize ); // rehash the entries from the old table @@ -219,17 +220,79 @@ clk = clock(); continue; Counter++; // get the place where this entry goes in the table table - pPlace = Ivy_TableFind( Ivy_ManObj(p, pTableOld[e]) ); + pPlace = Ivy_TableFind( p, Ivy_ManObj(p, pTableOld[e]) ); assert( *pPlace == 0 ); // should not be in the table *pPlace = pTableOld[e]; } assert( Counter == Ivy_ManHashObjNum(p) ); -// printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew ); +// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize ); // PRT( "Time", clock() - clk ); // replace the table and the parameters - free( p->pTable ); + free( pTableOld ); +} + +/**Function******************************************************************** + + Synopsis [Profiles the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Ivy_TableProfile( Ivy_Man_t * p ) +{ + int i, Counter = 0; + for ( i = 0; i < p->nTableSize; i++ ) + { + if ( p->pTable[i] ) + Counter++; + else if ( Counter ) + { + printf( "%d ", Counter ); + Counter = 0; + } + } } +/**Function******************************************************************** + + Synopsis [Returns the next prime >= 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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyUndo.c b/src/temp/ivy/ivyUndo.c deleted file mode 100644 index 6612bf42..00000000 --- a/src/temp/ivy/ivyUndo.c +++ /dev/null @@ -1,165 +0,0 @@ -/**CFile**************************************************************** - - FileName [ivyUndo.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [And-Inverter Graph package.] - - Synopsis [Recording the results of recent deletion of logic cone.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 11, 2006.] - - Revision [$Id: ivyUndo.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "ivy.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManUndoStart( Ivy_Man_t * p ) -{ - p->fRecording = 1; - p->nUndos = 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManUndoStop( Ivy_Man_t * p ) -{ - p->fRecording = 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManUndoRecord( Ivy_Man_t * p, Ivy_Obj_t * pObj ) -{ - Ivy_Obj_t * pObjUndo; - if ( p->nUndos >= p->nUndosAlloc ) - { - printf( "Ivy_ManUndoRecord(): Not enough memory for undo.\n" ); - return; - } - pObjUndo = p->pUndos + p->nUndos++; - // required data for Ivy_ObjCreateGhost() - pObjUndo->Type = pObj->Type; - pObjUndo->Init = pObj->Init; - pObjUndo->Fanin0 = pObj->Fanin0; - pObjUndo->Fanin1 = pObj->Fanin1; - pObjUndo->fComp0 = pObj->fComp0; - pObjUndo->fComp1 = pObj->fComp1; - // additional data - pObjUndo->Id = pObj->Id; - pObjUndo->nRefs = pObj->nRefs; - pObjUndo->Level = pObj->Level; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Vec_IntPutLast( Vec_Int_t * vFree, int Last ) -{ - int Place, i; - // find the entry - Place = Vec_IntFind( vFree, Last ); - if ( Place == -1 ) - return 0; - // shift entries by one - assert( vFree->pArray[Place] == Last ); - for ( i = Place; i < Vec_IntSize(vFree) - 1; i++ ) - vFree->pArray[i] = vFree->pArray[i+1]; - // put the entry in the end - vFree->pArray[i] = Last; - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManUndoPerform( Ivy_Man_t * p, Ivy_Obj_t * pRoot ) -{ - Ivy_Obj_t * pObjUndo, * pObjNew; - int i; - assert( p->nUndos > 0 ); - assert( p->fRecording == 0 ); - for ( i = p->nUndos - 1; i >= 0; i-- ) - { - // get the undo object - pObjUndo = p->pUndos + i; - // if this is the last object - if ( i == 0 ) - Vec_IntPush( p->vFree, pRoot->Id ); - else - Vec_IntPutLast( p->vFree, pObjUndo->Id ); - // create the new object - pObjNew = Ivy_ObjCreate( Ivy_ObjCreateGhost2( p, pObjUndo) ); - pObjNew->nRefs = pObjUndo->nRefs; - pObjNew->Level = pObjUndo->Level; - // make sure the object is created in the same place as before - assert( pObjNew->Id == pObjUndo->Id ); - } - p->nUndos = 0; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c index 3d1ac335..3b77bf41 100644 --- a/src/temp/ivy/ivyUtil.c +++ b/src/temp/ivy/ivyUtil.c @@ -68,136 +68,6 @@ void Ivy_ManCleanTravId( Ivy_Man_t * p ) /**Function************************************************************* - Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode ) -{ - Ivy_Obj_t * pNode0, * pNode1; - // check that the node is regular - assert( !Ivy_IsComplement(pNode) ); - // if the node is not AND, this is not MUX - if ( !Ivy_ObjIsAnd(pNode) ) - return 0; - // if the children are not complemented, this is not MUX - if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) ) - return 0; - // get children - pNode0 = Ivy_ObjFanin0(pNode); - pNode1 = Ivy_ObjFanin1(pNode); - // if the children are not ANDs, this is not MUX - if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) ) - return 0; - // otherwise the node is MUX iff it has a pair of equal grandchildren - return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || - (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) || - (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || - (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1))); -} - -/**Function************************************************************* - - Synopsis [Recognizes what nodes are control and data inputs of a MUX.] - - Description [If the node is a MUX, returns the control variable C. - Assigns nodes T and E to be the then and else variables of the MUX. - Node C is never complemented. Nodes T and E can be complemented. - This function also recognizes EXOR/NEXOR gates as MUXes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE ) -{ - Ivy_Obj_t * pNode0, * pNode1; - assert( !Ivy_IsComplement(pNode) ); - assert( Ivy_ObjIsMuxType(pNode) ); - // get children - pNode0 = Ivy_ObjFanin0(pNode); - pNode1 = Ivy_ObjFanin1(pNode); - // find the control variable -// if ( pNode1->p1 == Fraig_Not(pNode2->p1) ) - if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) - { -// if ( Fraig_IsComplement(pNode1->p1) ) - if ( Ivy_ObjFaninC0(pNode0) ) - { // pNode2->p1 is positive phase of C - *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); - *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); - return Ivy_ObjChild0(pNode1);//pNode2->p1; - } - else - { // pNode1->p1 is positive phase of C - *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); - *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); - return Ivy_ObjChild0(pNode0);//pNode1->p1; - } - } -// else if ( pNode1->p1 == Fraig_Not(pNode2->p2) ) - else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) - { -// if ( Fraig_IsComplement(pNode1->p1) ) - if ( Ivy_ObjFaninC0(pNode0) ) - { // pNode2->p2 is positive phase of C - *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); - *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); - return Ivy_ObjChild1(pNode1);//pNode2->p2; - } - else - { // pNode1->p1 is positive phase of C - *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); - *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); - return Ivy_ObjChild0(pNode0);//pNode1->p1; - } - } -// else if ( pNode1->p2 == Fraig_Not(pNode2->p1) ) - else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) - { -// if ( Fraig_IsComplement(pNode1->p2) ) - if ( Ivy_ObjFaninC1(pNode0) ) - { // pNode2->p1 is positive phase of C - *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); - *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); - return Ivy_ObjChild0(pNode1);//pNode2->p1; - } - else - { // pNode1->p2 is positive phase of C - *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); - *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); - return Ivy_ObjChild1(pNode0);//pNode1->p2; - } - } -// else if ( pNode1->p2 == Fraig_Not(pNode2->p2) ) - else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) - { -// if ( Fraig_IsComplement(pNode1->p2) ) - if ( Ivy_ObjFaninC1(pNode0) ) - { // pNode2->p2 is positive phase of C - *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); - *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); - return Ivy_ObjChild1(pNode1);//pNode2->p2; - } - else - { // pNode1->p2 is positive phase of C - *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); - *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); - return Ivy_ObjChild1(pNode0);//pNode1->p2; - } - } - assert( 0 ); // this is not MUX - return NULL; -} - -/**Function************************************************************* - Synopsis [Computes truth table of the cut.] Description [] @@ -207,14 +77,14 @@ Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Ob SeeAlso [] ***********************************************************************/ -void Ivy_ManCollectCut_rec( Ivy_Obj_t * pNode, Vec_Int_t * vNodes ) +void Ivy_ManCollectCut_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vNodes ) { if ( pNode->fMarkA ) return; pNode->fMarkA = 1; assert( Ivy_ObjIsAnd(pNode) || Ivy_ObjIsExor(pNode) ); - Ivy_ManCollectCut_rec( Ivy_ObjFanin0(pNode), vNodes ); - Ivy_ManCollectCut_rec( Ivy_ObjFanin1(pNode), vNodes ); + Ivy_ManCollectCut_rec( p, Ivy_ObjFanin0(pNode), vNodes ); + Ivy_ManCollectCut_rec( p, Ivy_ObjFanin1(pNode), vNodes ); Vec_IntPush( vNodes, pNode->Id ); } @@ -230,7 +100,7 @@ void Ivy_ManCollectCut_rec( Ivy_Obj_t * pNode, Vec_Int_t * vNodes ) SeeAlso [] ***********************************************************************/ -void Ivy_ManCollectCut( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) +void Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) { int i, Leaf; // collect and mark the leaves @@ -238,13 +108,13 @@ void Ivy_ManCollectCut( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNod Vec_IntForEachEntry( vLeaves, Leaf, i ) { Vec_IntPush( vNodes, Leaf ); - Ivy_ObjObj(pRoot, Leaf)->fMarkA = 1; + Ivy_ManObj(p, Leaf)->fMarkA = 1; } // collect and mark the nodes - Ivy_ManCollectCut_rec( pRoot, vNodes ); + Ivy_ManCollectCut_rec( p, pRoot, vNodes ); // clean the nodes Vec_IntForEachEntry( vNodes, Leaf, i ) - Ivy_ObjObj(pRoot, Leaf)->fMarkA = 0; + Ivy_ManObj(p, Leaf)->fMarkA = 0; } /**Function************************************************************* @@ -274,7 +144,7 @@ unsigned * Ivy_ObjGetTruthStore( int ObjNum, Vec_Int_t * vTruth ) SeeAlso [] ***********************************************************************/ -void Ivy_ManCutTruthOne( Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords ) +void Ivy_ManCutTruthOne( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords ) { unsigned * pTruth, * pTruth0, * pTruth1; int i; @@ -310,7 +180,7 @@ void Ivy_ManCutTruthOne( Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords ) SeeAlso [] ***********************************************************************/ -unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ) +unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ) { static unsigned uTruths[8][8] = { // elementary truth tables { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, @@ -324,10 +194,10 @@ unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * }; int i, Leaf; // collect the cut - Ivy_ManCollectCut( pRoot, vLeaves, vNodes ); + Ivy_ManCollectCut( p, pRoot, vLeaves, vNodes ); // set the node numbers Vec_IntForEachEntry( vNodes, Leaf, i ) - Ivy_ObjObj(pRoot, Leaf)->TravId = i; + Ivy_ManObj(p, Leaf)->TravId = i; // alloc enough memory Vec_IntClear( vTruth ); Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) ); @@ -336,7 +206,7 @@ unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * memcpy( Ivy_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) ); // compute truths for other nodes Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) ) - Ivy_ManCutTruthOne( Ivy_ObjObj(pRoot, Leaf), vTruth, 8 ); + Ivy_ManCutTruthOne( p, Ivy_ManObj(p, Leaf), vTruth, 8 ); return Ivy_ObjGetTruthStore( pRoot->TravId, vTruth ); } @@ -373,21 +243,18 @@ Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Ivy_ManReadLevels( Ivy_Man_t * p ) +int Ivy_ManLevels( Ivy_Man_t * p ) { Ivy_Obj_t * pObj; int i, LevelMax = 0; Ivy_ManForEachPo( p, pObj, i ) - { - pObj = Ivy_ObjFanin0(pObj); - LevelMax = IVY_MAX( LevelMax, (int)pObj->Level ); - } + LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level ); return LevelMax; } /**Function************************************************************* - Synopsis [Returns the real fanin.] + Synopsis [Collect the latches.] Description [] @@ -396,20 +263,42 @@ int Ivy_ManReadLevels( Ivy_Man_t * p ) SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj ) +int Ivy_ManResetLevels_rec( Ivy_Obj_t * pObj ) { - Ivy_Obj_t * pFanin; - if ( !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) ) - return pObj; - pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) ); - return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) ); + if ( pObj->Level || Ivy_ObjIsCi(pObj) ) + return pObj->Level; + if ( Ivy_ObjIsBuf(pObj) ) + return pObj->Level = Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) ); + assert( Ivy_ObjIsNode(pObj) ); + Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) ); + Ivy_ManResetLevels_rec( Ivy_ObjFanin1(pObj) ); + return pObj->Level = Ivy_ObjLevelNew( pObj ); } +/**Function************************************************************* + + Synopsis [Collect the latches.] + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManResetLevels( Ivy_Man_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + Ivy_ManForEachObj( p, pObj, i ) + pObj->Level = 0; + Ivy_ManForEachPo( p, pObj, i ) + Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) ); +} /**Function************************************************************* - Synopsis [Checks if the cube has exactly one 1.] + Synopsis [Recursively updates fanout levels.] Description [] @@ -418,14 +307,33 @@ Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -static inline int Ivy_TruthHasOneOne( unsigned uCube ) +void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { - return (uCube & (uCube - 1)) == 0; + Ivy_Obj_t * pFanout; + Vec_Ptr_t * vFanouts; + int i, LevelNew; + assert( p->vFanouts ); + assert( Ivy_ObjIsNode(pObj) ); + vFanouts = Vec_PtrAlloc( 10 ); + Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i ) + { + if ( Ivy_ObjIsCo(pFanout) ) + { +// assert( (int)Ivy_ObjFanin0(pFanout)->Level <= p->nLevelMax ); + continue; + } + LevelNew = Ivy_ObjLevelNew( pFanout ); + if ( (int)pFanout->Level == LevelNew ) + continue; + pFanout->Level = LevelNew; + Ivy_ObjUpdateLevel_rec( p, pFanout ); + } + Vec_PtrFree( vFanouts ); } /**Function************************************************************* - Synopsis [Checks if two cubes are distance-1.] + Synopsis [Compute the new required level.] Description [] @@ -434,15 +342,25 @@ static inline int Ivy_TruthHasOneOne( unsigned uCube ) SeeAlso [] ***********************************************************************/ -static inline int Ivy_TruthCubesDist1( unsigned uCube1, unsigned uCube2 ) +int Ivy_ObjLevelRNew( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { - unsigned uTemp = uCube1 | uCube2; - return Ivy_TruthHasOneOne( (uTemp >> 1) & uTemp & 0x55555555 ); + Ivy_Obj_t * pFanout; + Vec_Ptr_t * vFanouts; + int i, Required, LevelNew = 1000000; + assert( p->vFanouts && p->vRequired ); + vFanouts = Vec_PtrAlloc( 10 ); + Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i ) + { + Required = Vec_IntEntry(p->vRequired, pFanout->Id); + LevelNew = IVY_MIN( LevelNew, Required ); + } + Vec_PtrFree( vFanouts ); + return LevelNew - 1; } /**Function************************************************************* - Synopsis [Checks if two cubes differ in only one literal.] + Synopsis [Recursively updates fanout levels.] Description [] @@ -451,15 +369,33 @@ static inline int Ivy_TruthCubesDist1( unsigned uCube1, unsigned uCube2 ) SeeAlso [] ***********************************************************************/ -static inline int Ivy_TruthCubesDiff1( unsigned uCube1, unsigned uCube2 ) +void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew ) { - unsigned uTemp = uCube1 ^ uCube2; - return Ivy_TruthHasOneOne( ((uTemp >> 1) | uTemp) & 0x55555555 ); + Ivy_Obj_t * pFanin; + if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) ) + return; + assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) ); + // process the first fanin + pFanin = Ivy_ObjFanin0(pObj); + if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 ) + { + Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 ); + Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 ); + } + if ( Ivy_ObjIsBuf(pObj) ) + return; + // process the second fanin + pFanin = Ivy_ObjFanin1(pObj); + if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 ) + { + Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 ); + Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 ); + } } /**Function************************************************************* - Synopsis [Combines two distance 1 cubes.] + Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] Description [] @@ -468,95 +404,128 @@ static inline int Ivy_TruthCubesDiff1( unsigned uCube1, unsigned uCube2 ) SeeAlso [] ***********************************************************************/ -static inline unsigned Ivy_TruthCubesMerge( unsigned uCube1, unsigned uCube2 ) +int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode ) { - unsigned uTemp; - uTemp = uCube1 | uCube2; - uTemp &= (uTemp >> 1) & 0x55555555; - assert( Ivy_TruthHasOneOne(uTemp) ); - uTemp |= (uTemp << 1); - return (uCube1 | uCube2) ^ uTemp; + Ivy_Obj_t * pNode0, * pNode1; + // check that the node is regular + assert( !Ivy_IsComplement(pNode) ); + // if the node is not AND, this is not MUX + if ( !Ivy_ObjIsAnd(pNode) ) + return 0; + // if the children are not complemented, this is not MUX + if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) ) + return 0; + // get children + pNode0 = Ivy_ObjFanin0(pNode); + pNode1 = Ivy_ObjFanin1(pNode); + // if the children are not ANDs, this is not MUX + if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) ) + return 0; + // otherwise the node is MUX iff it has a pair of equal grandchildren + return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || + (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) || + (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || + (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1))); } /**Function************************************************************* - Synopsis [Estimates the number of AIG nodes in the truth table.] + Synopsis [Recognizes what nodes are control and data inputs of a MUX.] - Description [] + Description [If the node is a MUX, returns the control variable C. + Assigns nodes T and E to be the then and else variables of the MUX. + Node C is never complemented. Nodes T and E can be complemented. + This function also recognizes EXOR/NEXOR gates as MUXes.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Ivy_TruthEstimateNodes( unsigned * pTruth, int nVars ) +Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE ) { - static unsigned short uResult[256]; - static unsigned short uCover[81*81]; - static char pVarCount[81*81]; - int nMints, uCube, uCubeNew, i, k, c, nCubes, nRes, Counter; - assert( nVars <= 8 ); - // create the cover - nCubes = 0; - nMints = (1 << nVars); - for ( i = 0; i < nMints; i++ ) - if ( pTruth[i/32] & (1 << (i & 31)) ) - { - uCube = 0; - for ( k = 0; k < nVars; k++ ) - if ( i & (1 << k) ) - uCube |= (1 << ((k<<1)+1)); - else - uCube |= (1 << ((k<<1)+0)); - uCover[nCubes] = uCube; - pVarCount[nCubes] = nVars; - nCubes++; -// Extra_PrintBinary( stdout, &uCube, 8 ); printf( "\n" ); + Ivy_Obj_t * pNode0, * pNode1; + assert( !Ivy_IsComplement(pNode) ); + assert( Ivy_ObjIsMuxType(pNode) ); + // get children + pNode0 = Ivy_ObjFanin0(pNode); + pNode1 = Ivy_ObjFanin1(pNode); + // find the control variable +// if ( pNode1->p1 == Fraig_Not(pNode2->p1) ) + if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Ivy_ObjFaninC0(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + return Ivy_ObjChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + return Ivy_ObjChild0(pNode0);//pNode1->p1; } - assert( nCubes <= 256 ); - // reduce the cover by building larger cubes - for ( i = 1; i < nCubes; i++ ) - for ( k = 0; k < i; k++ ) - if ( pVarCount[i] && pVarCount[i] == pVarCount[k] && Ivy_TruthCubesDist1(uCover[i], uCover[k]) ) - { - uCubeNew = Ivy_TruthCubesMerge(uCover[i], uCover[k]); - for ( c = i; c < nCubes; c++ ) - if ( uCubeNew == uCover[c] ) - break; - if ( c != nCubes ) - continue; - uCover[nCubes] = uCubeNew; - pVarCount[nCubes] = pVarCount[i] - 1; - nCubes++; - assert( nCubes < 81*81 ); -// Extra_PrintBinary( stdout, &uCubeNew, 8 ); printf( "\n" ); -// c = c; - } - // compact the cover - nRes = 0; - for ( i = nCubes -1; i >= 0; i-- ) + } +// else if ( pNode1->p1 == Fraig_Not(pNode2->p2) ) + else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) { - for ( k = 0; k < nRes; k++ ) - if ( (uCover[i] & uResult[k]) == uResult[k] ) - break; - if ( k != nRes ) - continue; - uResult[nRes++] = uCover[i]; +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Ivy_ObjFaninC0(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + return Ivy_ObjChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + return Ivy_ObjChild0(pNode0);//pNode1->p1; + } + } +// else if ( pNode1->p2 == Fraig_Not(pNode2->p1) ) + else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Ivy_ObjFaninC1(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + return Ivy_ObjChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + return Ivy_ObjChild1(pNode0);//pNode1->p2; + } } - // count the number of literals - Counter = 0; - for ( i = 0; i < nRes; i++ ) +// else if ( pNode1->p2 == Fraig_Not(pNode2->p2) ) + else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) { - for ( k = 0; k < nVars; k++ ) - if ( uResult[i] & (3 << (k<<1)) ) - Counter++; +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Ivy_ObjFaninC1(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + return Ivy_ObjChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + return Ivy_ObjChild1(pNode0);//pNode1->p2; + } } - return Counter; + assert( 0 ); // this is not MUX + return NULL; } /**Function************************************************************* - Synopsis [Tests the cover procedure.] + Synopsis [Returns the real fanin.] Description [] @@ -565,17 +534,13 @@ int Ivy_TruthEstimateNodes( unsigned * pTruth, int nVars ) SeeAlso [] ***********************************************************************/ -void Ivy_TruthEstimateNodesTest() +Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj ) { - unsigned uTruth[8]; - int i; - for ( i = 0; i < 8; i++ ) - uTruth[i] = ~(unsigned)0; - uTruth[3] ^= (1 << 13); -// uTruth[4] = 0xFFFFF; -// uTruth[0] = 0xFF; -// uTruth[0] ^= (1 << 3); - printf( "Number = %d.\n", Ivy_TruthEstimateNodes(uTruth, 8) ); + Ivy_Obj_t * pFanin; + if ( pObj == NULL || !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) ) + return pObj; + pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) ); + return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make index f697910b..a8f6a824 100644 --- a/src/temp/ivy/module.make +++ b/src/temp/ivy/module.make @@ -4,7 +4,9 @@ SRC += src/temp/ivy/ivyBalance.c \ src/temp/ivy/ivyCut.c \ src/temp/ivy/ivyDfs.c \ src/temp/ivy/ivyDsd.c \ + src/temp/ivy/ivyFanout.c \ src/temp/ivy/ivyMan.c \ + src/temp/ivy/ivyMem.c \ src/temp/ivy/ivyMulti.c \ src/temp/ivy/ivyObj.c \ src/temp/ivy/ivyOper.c \ @@ -12,5 +14,4 @@ SRC += src/temp/ivy/ivyBalance.c \ src/temp/ivy/ivyRwrPre.c \ src/temp/ivy/ivySeq.c \ src/temp/ivy/ivyTable.c \ - src/temp/ivy/ivyUndo.c \ src/temp/ivy/ivyUtil.c diff --git a/src/temp/player/module.make b/src/temp/player/module.make index 81a5d77e..5185f56e 100644 --- a/src/temp/player/module.make +++ b/src/temp/player/module.make @@ -1,5 +1,4 @@ -SRC += src/temp/player/playerAbc.c \ - src/temp/player/playerBuild.c \ +SRC += src/temp/player/playerToAbc.c \ src/temp/player/playerCore.c \ src/temp/player/playerMan.c \ src/temp/player/playerUtil.c diff --git a/src/temp/player/player.h b/src/temp/player/player.h index cf0e8e01..7f9598d8 100644 --- a/src/temp/player/player.h +++ b/src/temp/player/player.h @@ -78,27 +78,17 @@ struct Pla_Man_t_ #define PLA_EMPTY ((Esop_Cube_t *)1) -static inline Pla_Man_t * Ivy_ObjPlaMan( Ivy_Obj_t * pObj ) { return (Pla_Man_t *)Ivy_ObjMan(pObj)->pData; } -static inline Pla_Obj_t * Ivy_ObjPlaStr( Ivy_Obj_t * pObj ) { return Ivy_ObjPlaMan(pObj)->pPlaStrs + pObj->Id; } - -static inline unsigned * Ivy_ObjGetTruth( Ivy_Obj_t * pObj ) -{ - Ivy_Man_t * p = Ivy_ObjMan(pObj); - int Offset = Vec_IntEntry( p->vTruths, pObj->Id ); - return Offset < 0 ? NULL : p->pMemory + Offset; - -} +static inline Pla_Man_t * Ivy_ObjPlaMan( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return (Pla_Man_t *)p->pData; } +static inline Pla_Obj_t * Ivy_ObjPlaStr( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return ((Pla_Man_t *)p->pData)->pPlaStrs + pObj->Id; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/*=== playerAbc.c ==============================================================*/ +/*=== playerToAbc.c ==============================================================*/ extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nFaninMax, int fVerbose ); -/*=== playerBuild.c ============================================================*/ -extern Ivy_Man_t * Pla_ManToAig( Ivy_Man_t * p ); /*=== playerCore.c =============================================================*/ -extern Ivy_Man_t * Pla_ManDecompose( Ivy_Man_t * p, int nLutMax, int nPlaMax, int fVerbose ); +extern Pla_Man_t * Pla_ManDecompose( Ivy_Man_t * p, int nLutMax, int nPlaMax, int fVerbose ); /*=== playerMan.c ==============================================================*/ extern Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * p, int nLutMax, int nPlaMax ); extern void Pla_ManFree( Pla_Man_t * p ); diff --git a/src/temp/player/playerAbc.c b/src/temp/player/playerAbc.c index 24273ffe..8b045d94 100644 --- a/src/temp/player/playerAbc.c +++ b/src/temp/player/playerAbc.c @@ -32,6 +32,8 @@ static Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtkOld, Ivy_Man_t * p ); /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +#if 0 + /**Function************************************************************* Synopsis [Gives the current ABC network to PLAyer for processing.] @@ -65,7 +67,7 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int fVerbose ) if ( fUseRewriting ) { // simplify - pMan = Ivy_ManResyn( pManExt = pMan, 1 ); + pMan = Ivy_ManResyn( pManExt = pMan, 1, 0 ); Ivy_ManStop( pManExt ); if ( fVerbose ) Ivy_ManPrintStats( pMan ); @@ -217,6 +219,7 @@ Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ) return pNtkNew; } +#endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/temp/player/playerBuild.c b/src/temp/player/playerBuild.c index b23c0c16..e878f19c 100644 --- a/src/temp/player/playerBuild.c +++ b/src/temp/player/playerBuild.c @@ -33,6 +33,8 @@ static int Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld ); /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +#if 0 + /**Function************************************************************* Synopsis [Constructs the AIG manager (IVY) for the network after mapping.] @@ -93,7 +95,7 @@ Ivy_Obj_t * Pla_ManToAig_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld ) return Ivy_ManObj( pNew, pObjOld->TravId ); assert( Ivy_ObjIsAnd(pObjOld) || Ivy_ObjIsExor(pObjOld) ); // get the support and the cover - pStr = Ivy_ObjPlaStr( pObjOld ); + pStr = Ivy_ObjPlaStr( pNew, pObjOld ); if ( Vec_IntSize( &pStr->vSupp[0] ) <= p->nLutMax ) { vSupp = &pStr->vSupp[0]; @@ -246,10 +248,10 @@ int Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld ) if ( !Ivy_ObjIsLut(pObjNew) ) continue; pObjOld = Ivy_ManObj( pOld, pObjNew->TravId ); - vSupp = Ivy_ObjPlaStr(pObjOld)->vSupp; + vSupp = Ivy_ObjPlaStr(pNew, pObjOld)->vSupp; assert( Vec_IntSize(vSupp) <= 8 ); pTruth = Ivy_ObjGetTruth( pObjNew ); - pComputed = Ivy_ManCutTruth( pObjOld, vSupp, vNodes, vTemp ); + pComputed = Ivy_ManCutTruth( pNew, pObjOld, vSupp, vNodes, vTemp ); // check if the truth table is constant 0 for ( k = 0; k < 8; k++ ) if ( pComputed[k] ) @@ -272,6 +274,8 @@ int Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld ) return Counter; } +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/player/playerCore.c b/src/temp/player/playerCore.c index 258a3336..da2c6efd 100644 --- a/src/temp/player/playerCore.c +++ b/src/temp/player/playerCore.c @@ -44,10 +44,9 @@ static void Pla_NodeGetSuppsAndCovers( Pla_Man_t * p, Ivy_Obj_t * pObj, int Leve SeeAlso [] ***********************************************************************/ -Ivy_Man_t * Pla_ManDecompose( Ivy_Man_t * pAig, int nLutMax, int nPlaMax, int fVerbose ) +Pla_Man_t * Pla_ManDecompose( Ivy_Man_t * pAig, int nLutMax, int nPlaMax, int fVerbose ) { Pla_Man_t * p; - Ivy_Man_t * pAigNew; p = Pla_ManAlloc( pAig, nLutMax, nPlaMax ); if ( !Pla_ManDecomposeInt( p ) ) { @@ -55,12 +54,7 @@ Ivy_Man_t * Pla_ManDecompose( Ivy_Man_t * pAig, int nLutMax, int nPlaMax, int fV Pla_ManFree( p ); return NULL; } - pAigNew = Pla_ManToAig( pAig ); -// if ( fVerbose ) -// printf( "PLA stats: Both = %6d. Pla = %6d. Lut = %6d. Total = %6d. Deref = %6d.\n", -// p->nNodesBoth, p->nNodesPla, p->nNodesLut, p->nNodes, p->nNodesDeref ); - Pla_ManFree( p ); - return pAigNew; + return p; } /**Function************************************************************* @@ -84,7 +78,7 @@ int Pla_ManDecomposeInt( Pla_Man_t * p ) // prepare the PI structures Ivy_ManForEachPi( pAig, pObj, i ) { - pStr = Ivy_ObjPlaStr( pObj ); + pStr = Ivy_ObjPlaStr( pAig, pObj ); pStr->fFixed = 1; pStr->Depth = 0; pStr->nRefs = (unsigned)pObj->nRefs; @@ -142,9 +136,9 @@ int Pla_ManDecomposeNode( Pla_Man_t * p, Ivy_Obj_t * pObj ) p->nNodes++; // get the structures - pStr = Ivy_ObjPlaStr( pObj ); - pStr0 = Ivy_ObjPlaStr( Ivy_ObjFanin0( pObj ) ); - pStr1 = Ivy_ObjPlaStr( Ivy_ObjFanin1( pObj ) ); + pStr = Ivy_ObjPlaStr( p->pManAig, pObj ); + pStr0 = Ivy_ObjPlaStr( p->pManAig, Ivy_ObjFanin0( pObj ) ); + pStr1 = Ivy_ObjPlaStr( p->pManAig, Ivy_ObjFanin1( pObj ) ); vSupp0 = &pStr->vSupp[0]; vSupp1 = &pStr->vSupp[1]; pStr->pCover[0] = PLA_EMPTY; @@ -263,9 +257,9 @@ void Pla_NodeGetSuppsAndCovers( Pla_Man_t * p, Ivy_Obj_t * pObj, int Level, pFan0 = Ivy_ObjFanin0( pObj ); pFan1 = Ivy_ObjFanin1( pObj ); // get the structures - pStr = Ivy_ObjPlaStr( pObj ); - pStr0 = Ivy_ObjPlaStr( pFan0 ); - pStr1 = Ivy_ObjPlaStr( pFan1 ); + pStr = Ivy_ObjPlaStr( p->pManAig, pObj ); + pStr0 = Ivy_ObjPlaStr( p->pManAig, pFan0 ); + pStr1 = Ivy_ObjPlaStr( p->pManAig, pFan1 ); // make sure the fanins are processed assert( Ivy_ObjIsPi(pFan0) || pStr0->Depth > 0 ); assert( Ivy_ObjIsPi(pFan1) || pStr1->Depth > 0 ); diff --git a/src/temp/player/playerMan.c b/src/temp/player/playerMan.c index 7f2c0919..1196d242 100644 --- a/src/temp/player/playerMan.c +++ b/src/temp/player/playerMan.c @@ -58,8 +58,8 @@ Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * pAig, int nLutMax, int nPlaMax ) pMan->vTriv0 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv0, -1 ); pMan->vTriv1 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv1, -1 ); // allocate memory for object structures - pMan->pPlaStrs = ALLOC( Pla_Obj_t, sizeof(Pla_Obj_t) * Ivy_ManObjIdNext(pAig) ); - memset( pMan->pPlaStrs, 0, sizeof(Pla_Obj_t) * Ivy_ManObjIdNext(pAig) ); + pMan->pPlaStrs = ALLOC( Pla_Obj_t, sizeof(Pla_Obj_t) * (Ivy_ManObjIdMax(pAig)+1) ); + memset( pMan->pPlaStrs, 0, sizeof(Pla_Obj_t) * (Ivy_ManObjIdMax(pAig)+1) ); // create the cube manager pMan->pManMin = Esop_ManAlloc( nPlaMax ); // save the resulting manager @@ -90,7 +90,7 @@ void Pla_ManFree( Pla_Man_t * p ) Vec_IntFree( p->vComTo1 ); Vec_IntFree( p->vPairs0 ); Vec_IntFree( p->vPairs1 ); - for ( i = 0, pStr = p->pPlaStrs; i < Ivy_ManObjIdNext(p->pManAig); i++, pStr++ ) + for ( i = 0, pStr = p->pPlaStrs; i <= Ivy_ManObjIdMax(p->pManAig); i++, pStr++ ) FREE( pStr->vSupp[0].pArray ), FREE( pStr->vSupp[1].pArray ); free( p->pPlaStrs ); free( p ); diff --git a/src/temp/player/playerToAbc.c b/src/temp/player/playerToAbc.c new file mode 100644 index 00000000..09bf5088 --- /dev/null +++ b/src/temp/player/playerToAbc.c @@ -0,0 +1,316 @@ +/**CFile**************************************************************** + + FileName [playerToAbc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [PLAyer decomposition package.] + + Synopsis [Bridge between ABC and PLAyer.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 20, 2006.] + + Revision [$Id: playerToAbc.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "player.h" +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * p ); +static Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, Pla_Man_t * p ); +static Abc_Obj_t * Ivy_ManToAbc_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Pla_Man_t * p, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp ); +static Abc_Obj_t * Ivy_ManToAigCube( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Esop_Cube_t * pCube, Vec_Int_t * vSupp ); + +static inline void Abc_ObjSetIvy2Abc( Ivy_Man_t * p, int IvyId, Abc_Obj_t * pObjAbc ) { assert(Vec_PtrEntry(p->pCopy, IvyId) == NULL); assert(!Abc_ObjIsComplement(pObjAbc)); Vec_PtrWriteEntry( p->pCopy, IvyId, pObjAbc ); } +static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId ) { return Vec_PtrEntry( p->pCopy, IvyId ); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to PLAyer for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int fVerbose ) +{ + int fUseRewriting = 1; + Pla_Man_t * p; + Ivy_Man_t * pMan, * pManExt; + Abc_Ntk_t * pNtkAig; + if ( !Abc_NtkIsStrash(pNtk) ) + return NULL; + // convert to the new AIG manager + pMan = Ivy_ManFromAbc( pNtk ); + // check the correctness of conversion + if ( !Ivy_ManCheck( pMan ) ) + { + printf( "Abc_NtkPlayer: Internal AIG check has failed.\n" ); + Ivy_ManStop( pMan ); + return NULL; + } + if ( fVerbose ) + Ivy_ManPrintStats( pMan ); + if ( fUseRewriting ) + { + // simplify + pMan = Ivy_ManResyn( pManExt = pMan, 1, 0 ); + Ivy_ManStop( pManExt ); + if ( fVerbose ) + Ivy_ManPrintStats( pMan ); + } + // perform decomposition/mapping into PLAs/LUTs + p = Pla_ManDecompose( pMan, nLutMax, nPlaMax, fVerbose ); + // convert from the extended AIG manager into an SOP network + pNtkAig = Ivy_ManToAbc( pNtk, pMan, p ); + Pla_ManFree( p ); + Ivy_ManStop( pMan ); + // chech the resulting network + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkPlayer: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Converts from strashed AIG in ABC into strash AIG in IVY.] + + Description [Assumes DFS ordering of nodes in the AIG of ABC.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * pNtk ) +{ + Ivy_Man_t * pMan; + Abc_Obj_t * pObj; + int i; + // create the manager + pMan = Ivy_ManStart(); + // create the PIs + Abc_NtkConst1(pNtk)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan); + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Ivy_ObjCreatePi(pMan); + // perform the conversion of the internal nodes + Abc_AigForEachAnd( pNtk, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Ivy_And( pMan, (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj), (Ivy_Obj_t *)Abc_ObjChild1Copy(pObj) ); + // create the POs + Abc_NtkForEachCo( pNtk, pObj, i ) + Ivy_ObjCreatePo( pMan, (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj) ); + Ivy_ManCleanup( pMan ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [Constructs the ABD network after mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, Pla_Man_t * p ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObjAbc, * pObj; + Ivy_Obj_t * pObjIvy; + Vec_Int_t * vNodes, * vTemp; + int i; + // start mapping from Ivy into Abc + pMan->pCopy = Vec_PtrStart( Ivy_ManObjIdMax(pMan) + 1 ); + // start the new ABC network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // transfer the pointers to the basic nodes + Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NtkConst1(pNtkNew) ); + Abc_NtkForEachCi( pNtkNew, pObjAbc, i ) + Abc_ObjSetIvy2Abc( pMan, Ivy_ManPi(pMan, i)->Id, pObjAbc ); + // recursively construct the network + vNodes = Vec_IntAlloc( 100 ); + vTemp = Vec_IntAlloc( 100 ); + Ivy_ManForEachPo( pMan, pObjIvy, i ) + { + // get the new ABC node corresponding to the old fanin of the PO in IVY + pObjAbc = Ivy_ManToAbc_rec( pNtkNew, pMan, p, Ivy_ObjFanin0(pObjIvy), vNodes, vTemp ); + if ( Ivy_ObjFaninC0(pObjIvy) ) // complement + { + if ( Abc_ObjIsCi(pObjAbc) ) + pObjAbc = Abc_NodeCreateInv( pNtkNew, pObjAbc ); + else + { + // clone the node + pObj = Abc_NodeClone( pObjAbc ); + // set complemented functions + pObj->pData = Abc_SopRegister( pNtkNew->pManFunc, pObjAbc->pData ); + Abc_SopComplement(pObj->pData); + // return the new node + pObjAbc = pObj; + } + assert( Abc_SopGetVarNum(pObjAbc->pData) == Abc_ObjFaninNum(pObjAbc) ); + } + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjAbc ); + } + Vec_IntFree( vTemp ); + Vec_IntFree( vNodes ); + Vec_PtrFree( pMan->pCopy ); + pMan->pCopy = NULL; + // remove dangling nodes +// Abc_NtkForEachNode( pNtkNew, pObjAbc, i ) +// if ( Abc_ObjFanoutNum(pObjAbc) == 0 ) +// Abc_NtkDeleteObj(pObjAbc); + Abc_NtkCleanup( pNtkNew, 0 ); + // fix CIs feeding directly into COs + Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Recursively construct the new node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Ivy_ManToAbc_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Pla_Man_t * p, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp ) +{ + Vec_Int_t * vSupp; + Esop_Cube_t * pCover, * pCube; + Abc_Obj_t * pObjAbc, * pFaninAbc; + Pla_Obj_t * pStr; + int Entry, nCubes, i; + unsigned * puTruth; + // skip the node if it is a constant or already processed + pObjAbc = Abc_ObjGetIvy2Abc( pMan, pObjIvy->Id ); + if ( pObjAbc ) + return pObjAbc; + assert( Ivy_ObjIsAnd(pObjIvy) || Ivy_ObjIsExor(pObjIvy) ); + // get the support and the cover + pStr = Ivy_ObjPlaStr( pMan, pObjIvy ); + if ( Vec_IntSize( &pStr->vSupp[0] ) <= p->nLutMax ) + { + vSupp = &pStr->vSupp[0]; + pCover = PLA_EMPTY; + } + else + { + vSupp = &pStr->vSupp[1]; + pCover = pStr->pCover[1]; + assert( pCover != PLA_EMPTY ); + } + // create new node and its fanins + Vec_IntForEachEntry( vSupp, Entry, i ) + Ivy_ManToAbc_rec( pNtkNew, pMan, p, Ivy_ManObj(pMan, Entry), vNodes, vTemp ); + // consider the case of a LUT + if ( pCover == PLA_EMPTY ) + { + pObjAbc = Abc_NtkCreateNode( pNtkNew ); + Vec_IntForEachEntry( vSupp, Entry, i ) + Abc_ObjAddFanin( pObjAbc, Abc_ObjGetIvy2Abc(pMan, Entry) ); + // check if the truth table is constant 0 + puTruth = Ivy_ManCutTruth( pMan, pObjIvy, vSupp, vNodes, vTemp ); + for ( i = 0; i < 8; i++ ) + if ( puTruth[i] ) + break; + // create constant 0 node + if ( i == 8 ) + { + pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL ); + pObjAbc = Abc_NodeCreateConst0( pNtkNew ); + } + else + pObjAbc->pData = Abc_SopCreateFromTruth( pNtkNew->pManFunc, Vec_IntSize(vSupp), puTruth ); + } + else + { + // for each cube, construct the node + nCubes = Esop_CoverCountCubes( pCover ); + if ( nCubes == 0 ) + pObjAbc = Abc_NodeCreateConst0( pNtkNew ); + else if ( nCubes == 1 ) + pObjAbc = Ivy_ManToAigCube( pNtkNew, pMan, pObjIvy, pCover, vSupp ); + else + { + pObjAbc = Abc_NtkCreateNode( pNtkNew ); + Esop_CoverForEachCube( pCover, pCube ) + { + pFaninAbc = Ivy_ManToAigCube( pNtkNew, pMan, pObjIvy, pCube, vSupp ); + Abc_ObjAddFanin( pObjAbc, pFaninAbc ); + } + pObjAbc->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, Abc_ObjFaninNum(pObjAbc) ); + } + } + Abc_ObjSetIvy2Abc( pMan, pObjIvy->Id, pObjAbc ); + return pObjAbc; +} + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Ivy_ManToAigCube( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Esop_Cube_t * pCube, Vec_Int_t * vSupp ) +{ + int pCompls[PLAYER_FANIN_LIMIT]; + Abc_Obj_t * pObjAbc, * pFaninAbc; + int i, k, Value; + // if tautology cube, create constant 1 node + if ( pCube->nLits == 0 ) + return Abc_NodeCreateConst1(pNtkNew); + // create AND node + pObjAbc = Abc_NtkCreateNode( pNtkNew ); + for ( i = k = 0; i < (int)pCube->nVars; i++ ) + { + Value = Esop_CubeGetVar( pCube, i ); + assert( Value != 0 ); + if ( Value == 3 ) + continue; + pFaninAbc = Abc_ObjGetIvy2Abc( pMan, Vec_IntEntry(vSupp, i) ); + pFaninAbc = Abc_ObjNotCond( pFaninAbc, Value==1 ); + Abc_ObjAddFanin( pObjAbc, Abc_ObjRegular(pFaninAbc) ); + pCompls[k++] = Abc_ObjIsComplement(pFaninAbc); + } + pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Abc_ObjFaninNum(pObjAbc), pCompls ); + assert( Abc_ObjFaninNum(pObjAbc) == (int)pCube->nLits ); + return pObjAbc; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/player/playerUtil.c b/src/temp/player/playerUtil.c index ced2d6b7..1c8aeec2 100644 --- a/src/temp/player/playerUtil.c +++ b/src/temp/player/playerUtil.c @@ -281,6 +281,8 @@ Esop_Cube_t * Pla_ManExorTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_C return pCover; } +#if 0 + /**Function************************************************************* Synopsis [Computes area/delay of the mapping.] @@ -342,6 +344,8 @@ void Pla_ManComputeStats( Ivy_Man_t * p, Vec_Int_t * vNodes ) printf( "Area = %d. Delay = %d.\n", Area, Delay ); } +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/rwt/rwtMan.c b/src/temp/rwt/rwtMan.c index 5f077c8d..f7dd38a7 100644 --- a/src/temp/rwt/rwtMan.c +++ b/src/temp/rwt/rwtMan.c @@ -64,10 +64,10 @@ void Rwt_ManGlobalStart() ***********************************************************************/ void Rwt_ManGlobalStop() { - if ( s_puCanons == NULL ) free( s_puCanons ); - if ( s_pPhases == NULL ) free( s_pPhases ); - if ( s_pPerms == NULL ) free( s_pPerms ); - if ( s_pMap == NULL ) free( s_pMap ); + FREE( s_puCanons ); + FREE( s_pPhases ); + FREE( s_pPerms ); + FREE( s_pMap ); } /**Function************************************************************* diff --git a/src/temp/vec/vecInt.h b/src/temp/vec/vecInt.h index 4f193cf2..9db30af7 100644 --- a/src/temp/vec/vecInt.h +++ b/src/temp/vec/vecInt.h @@ -289,6 +289,23 @@ 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 ); @@ -385,7 +402,10 @@ static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry ) int i; if ( p->nSize >= nSize ) return; - Vec_IntGrow( p, nSize ); + if ( p->nSize < 2 * nSize ) + Vec_IntGrow( p, 2 * nSize ); + else + Vec_IntGrow( p, p->nSize ); for ( i = p->nSize; i < nSize; i++ ) p->pArray[i] = Entry; p->nSize = nSize; |