/**CFile**************************************************************** FileName [ivy.h] SystemName [ABC: Logic synthesis and verification system.] PackageName [And-Inverter Graph package.] Synopsis [External declarations.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - May 11, 2006.] Revision [$Id: ivy.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] ***********************************************************************/ #ifndef __IVY_H__ #define __IVY_H__ #ifdef __cplusplus extern "C" { #endif //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include #include "extra.h" #include "vec.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// typedef struct Ivy_Man_t_ Ivy_Man_t; typedef struct Ivy_Obj_t_ Ivy_Obj_t; typedef int Ivy_Edge_t; typedef struct Ivy_FraigParams_t_ Ivy_FraigParams_t; // object types typedef enum { IVY_NONE, // 0: non-existent 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: AND node IVY_EXOR, // 6: EXOR node IVY_BUF, // 7: buffer (temporary) IVY_VOID // 8: unused object } Ivy_Type_t; // latch initial values typedef enum { IVY_INIT_NONE, // 0: not a latch IVY_INIT_0, // 1: zero IVY_INIT_1, // 2: one IVY_INIT_DC // 3: don't-care } Ivy_Init_t; // the AIG node struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit) // 10 words - 16 words { int Id; // integer ID int TravId; // traversal ID unsigned Type : 4; // object type unsigned fMarkA : 1; // multipurpose mask unsigned fMarkB : 1; // multipurpose mask unsigned fExFan : 1; // set to 1 if last fanout added is EXOR unsigned fPhase : 1; // value under 000...0 pattern unsigned fFailTfo : 1; // the TFO of the failed node unsigned Init : 2; // latch initial value unsigned Level : 21; // logic level int nRefs; // reference counter Ivy_Obj_t * pFanin0; // fanin Ivy_Obj_t * pFanin1; // fanin Ivy_Obj_t * pFanout; // fanout Ivy_Obj_t * pNextFan0; // next fanout of the first fanin Ivy_Obj_t * pNextFan1; // next fanout of the second fanin Ivy_Obj_t * pPrevFan0; // prev fanout of the first fanin Ivy_Obj_t * pPrevFan1; // prev fanout of the second fanin Ivy_Obj_t * pEquiv; // equivalent node }; // the AIG manager struct Ivy_Man_t_ { // AIG nodes 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 // 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 nTravIds; // the traversal ID int nLevelMax; // the maximum level Vec_Int_t * vRequired; // required times int fFanout; // fanout is allocated void * pData; // the temporary data void * pCopy; // the temporary data Ivy_Man_t * pHaig; // history AIG if present int nClassesSkip; // the number of skipped classes // 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 // timing statistics int time1; int time2; }; struct Ivy_FraigParams_t_ { int nSimWords; // the number of words in the simulation info double dSimSatur; // the ratio of refined classes when saturation is reached int fPatScores; // enables simulation pattern scoring int MaxScore; // max score after which resimulation is used double dActConeRatio; // the ratio of cone to be bumped double dActConeBumpMax; // the largest bump in activity int fProve; // prove the miter outputs int fVerbose; // verbose output int fDoSparse; // skip sparse functions int nBTLimitNode; // conflict limit at a node int nBTLimitMiter; // conflict limit at an output // int nBTLimitGlobal; // conflict limit global // int nInsLimitNode; // inspection limit at a node // int nInsLimitMiter; // inspection limit at an output // int nInsLimitGlobal; // inspection limit global }; #define IVY_CUT_LIMIT 256 #define IVY_CUT_INPUT 6 typedef struct Ivy_Cut_t_ Ivy_Cut_t; struct Ivy_Cut_t_ { int nLatches; short nSize; short nSizeMax; int pArray[IVY_CUT_INPUT]; unsigned uHash; }; 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 }; #define IVY_LEAF_MASK 255 #define IVY_LEAF_BITS 8 //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// #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 long)(p) & ~01); } static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned long)(p) ^ 01); } static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned long)(p) ^ (c)); } static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int)((unsigned long)(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) ); } static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << IVY_LEAF_BITS) | Lat; } static inline int Ivy_LeafId( int Leaf ) { return Leaf >> IVY_LEAF_BITS; } static inline int Ivy_LeafLat( int Leaf ) { return Leaf & IVY_LEAF_MASK; } static inline int Ivy_ManPiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PI]; } static inline int Ivy_ManPoNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PO]; } static inline int Ivy_ManAssertNum( Ivy_Man_t * p ) { return p->nObjs[IVY_ASSERT]; } static inline int Ivy_ManLatchNum( Ivy_Man_t * p ) { return p->nObjs[IVY_LATCH]; } 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_ManObjNum( Ivy_Man_t * p ) { return p->nCreated - p->nDeleted; } 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]; } static inline Ivy_Type_t Ivy_ObjType( Ivy_Obj_t * pObj ) { return pObj->Type; } static inline Ivy_Init_t Ivy_ObjInit( Ivy_Obj_t * pObj ) { return pObj->Init; } static inline int Ivy_ObjIsConst1( Ivy_Obj_t * pObj ) { return pObj->Id == 0; } static inline int Ivy_ObjIsGhost( Ivy_Obj_t * pObj ) { return pObj->Id < 0; } static inline int Ivy_ObjIsNone( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_NONE; } static inline int Ivy_ObjIsPi( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PI; } static inline int Ivy_ObjIsPo( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PO; } static inline int Ivy_ObjIsCi( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PI || pObj->Type == IVY_LATCH; } static inline int Ivy_ObjIsCo( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PO || pObj->Type == IVY_LATCH; } static inline int Ivy_ObjIsAssert( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_ASSERT; } static inline int Ivy_ObjIsLatch( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_LATCH; } static inline int Ivy_ObjIsAnd( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_AND; } static inline int Ivy_ObjIsExor( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_EXOR; } static inline int Ivy_ObjIsBuf( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_BUF; } static inline int Ivy_ObjIsNode( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; } static inline int Ivy_ObjIsTerm( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PI || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; } static inline int Ivy_ObjIsHash( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; } static inline int Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; } static inline int Ivy_ObjIsMarkA( Ivy_Obj_t * pObj ) { return pObj->fMarkA; } static inline void Ivy_ObjSetMarkA( Ivy_Obj_t * pObj ) { pObj->fMarkA = 1; } static inline void Ivy_ObjClearMarkA( Ivy_Obj_t * pObj ) { pObj->fMarkA = 0; } static inline void Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId ) { pObj->TravId = TravId; } static inline void Ivy_ObjSetTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { pObj->TravId = p->nTravIds; } static inline void Ivy_ObjSetTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1; } static inline int Ivy_ObjIsTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return (int )((int)pObj->TravId == p->nTravIds); } static inline int Ivy_ObjIsTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return (int )((int)pObj->TravId == p->nTravIds - 1); } static inline int Ivy_ObjId( Ivy_Obj_t * pObj ) { return pObj->Id; } static inline int Ivy_ObjTravId( Ivy_Obj_t * pObj ) { return pObj->TravId; } static inline int Ivy_ObjPhase( Ivy_Obj_t * pObj ) { return pObj->fPhase; } static inline int Ivy_ObjExorFanout( Ivy_Obj_t * pObj ) { return pObj->fExFan; } static inline int Ivy_ObjRefs( Ivy_Obj_t * pObj ) { return pObj->nRefs; } static inline void Ivy_ObjRefsInc( Ivy_Obj_t * pObj ) { pObj->nRefs++; } static inline void Ivy_ObjRefsDec( Ivy_Obj_t * pObj ) { assert( pObj->nRefs > 0 ); pObj->nRefs--; } static inline int Ivy_ObjFaninId0( Ivy_Obj_t * pObj ) { return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; } static inline int Ivy_ObjFaninId1( Ivy_Obj_t * pObj ) { return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; } static inline int Ivy_ObjFaninC0( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj->pFanin0); } static inline int Ivy_ObjFaninC1( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj->pFanin1); } static inline Ivy_Obj_t * Ivy_ObjFanin0( Ivy_Obj_t * pObj ) { return Ivy_Regular(pObj->pFanin0); } static inline Ivy_Obj_t * Ivy_ObjFanin1( Ivy_Obj_t * pObj ) { return Ivy_Regular(pObj->pFanin1); } static inline Ivy_Obj_t * Ivy_ObjChild0( Ivy_Obj_t * pObj ) { return pObj->pFanin0; } static inline Ivy_Obj_t * Ivy_ObjChild1( Ivy_Obj_t * pObj ) { return pObj->pFanin1; } static inline Ivy_Obj_t * Ivy_ObjChild0Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin0(pObj)? Ivy_NotCond(Ivy_ObjFanin0(pObj)->pEquiv, Ivy_ObjFaninC0(pObj)) : NULL; } static inline Ivy_Obj_t * Ivy_ObjChild1Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL; } static inline Ivy_Obj_t * Ivy_ObjEquiv( Ivy_Obj_t * pObj ) { return Ivy_Regular(pObj)->pEquiv? Ivy_NotCond(Ivy_Regular(pObj)->pEquiv, Ivy_IsComplement(pObj)) : NULL; } static inline int Ivy_ObjLevel( Ivy_Obj_t * pObj ) { return pObj->Level; } static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); } static inline int Ivy_ObjFaninPhase( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj)? !Ivy_Regular(pObj)->fPhase : pObj->fPhase; } 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 int Ivy_ObjWhatFanin( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin ) { 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_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_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init ) { Ivy_Obj_t * pGhost, * pTemp; assert( Type != IVY_AND || !Ivy_ObjIsConst1(Ivy_Regular(p0)) ); assert( p1 == NULL || !Ivy_ObjIsConst1(Ivy_Regular(p1)) ); assert( Type == IVY_PI || Ivy_Regular(p0) != Ivy_Regular(p1) ); assert( Type != IVY_LATCH || !Ivy_IsComplement(p0) ); // assert( p1 == NULL || (!Ivy_ObjIsLatch(Ivy_Regular(p0)) || !Ivy_ObjIsLatch(Ivy_Regular(p1))) ); pGhost = Ivy_ManGhost(p); pGhost->Type = Type; pGhost->Init = Init; pGhost->pFanin0 = p0; pGhost->pFanin1 = p1; if ( p1 && Ivy_ObjFaninId0(pGhost) > Ivy_ObjFaninId1(pGhost) ) pTemp = pGhost->pFanin0, pGhost->pFanin0 = pGhost->pFanin1, pGhost->pFanin1 = pTemp; return pGhost; } // get the complemented initial state static Ivy_Init_t Ivy_InitNotCond( Ivy_Init_t Init, int fCompl ) { assert( Init != IVY_INIT_NONE ); if ( fCompl == 0 ) return Init; if ( Init == IVY_INIT_0 ) return IVY_INIT_1; if ( Init == IVY_INIT_1 ) return IVY_INIT_0; return IVY_INIT_DC; } // get the initial state after forward retiming over AND gate static Ivy_Init_t Ivy_InitAnd( Ivy_Init_t InitA, Ivy_Init_t InitB ) { assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE ); if ( InitA == IVY_INIT_0 || InitB == IVY_INIT_0 ) return IVY_INIT_0; if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC ) return IVY_INIT_DC; return IVY_INIT_1; } // get the initial state after forward retiming over EXOR gate static Ivy_Init_t Ivy_InitExor( Ivy_Init_t InitA, Ivy_Init_t InitB ) { assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE ); if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC ) return IVY_INIT_DC; if ( InitA == IVY_INIT_0 && InitB == IVY_INIT_1 ) return IVY_INIT_1; if ( InitA == IVY_INIT_1 && InitB == IVY_INIT_0 ) return IVY_INIT_1; return IVY_INIT_0; } // 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 the primary inputs #define Ivy_ManForEachPi( p, pObj, i ) \ Vec_PtrForEachEntry( p->vPis, pObj, i ) // iterator over the primary outputs #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 ) \ Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCi(pObj) ) {} else // iterator over the combinational outputs #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 ) \ Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsNode(pObj) ) {} else // iterator over logic latches #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 ) \ 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 /// //////////////////////////////////////////////////////////////////////// /*=== ivyBalance.c ========================================================*/ extern Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, 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_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 ); extern int Ivy_ManCheckFanoutNums( Ivy_Man_t * p ); extern int Ivy_ManCheckFanouts( Ivy_Man_t * p ); extern int Ivy_ManCheckChoices( Ivy_Man_t * p ); /*=== ivyCut.c ==========================================================*/ extern void Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize ); extern Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves ); /*=== ivyDfs.c ==========================================================*/ extern Vec_Int_t * Ivy_ManDfs( 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 ); extern int Ivy_ManIsAcyclic( Ivy_Man_t * p ); extern int Ivy_ManSetLevels( Ivy_Man_t * p, int fHaig ); /*=== ivyDsd.c ==========================================================*/ extern int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree ); 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_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj ); /*=== ivyFastMap.c =============================================================*/ extern void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbose ); extern void Ivy_FastMapStop( Ivy_Man_t * pAig ); extern void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves ); extern void Ivy_FastMapReverseLevel( Ivy_Man_t * pAig ); /*=== ivyFraig.c ==========================================================*/ extern int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars ); extern Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); extern Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); extern void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams ); /*=== ivyHaig.c ==========================================================*/ extern void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose ); extern void Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew ); extern void Ivy_ManHaigStop( Ivy_Man_t * p ); extern void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose ); extern void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew ); extern void Ivy_ManHaigSimulate( Ivy_Man_t * p ); /*=== ivyMan.c ==========================================================*/ extern Ivy_Man_t * Ivy_ManStart(); extern Ivy_Man_t * Ivy_ManStartFrom( Ivy_Man_t * p ); extern Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p ); extern Ivy_Man_t * Ivy_ManFrames( Ivy_Man_t * pMan, int nLatches, int nFrames, int fInit, Vec_Ptr_t ** pvMapping ); extern void Ivy_ManStop( Ivy_Man_t * p ); extern int Ivy_ManCleanup( Ivy_Man_t * p ); extern int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel ); 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_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_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, int fUpdateLevel ); extern void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel ); /*=== ivyOper.c =========================================================*/ 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_ManResyn0( Ivy_Man_t * p, int fUpdateLevel, int fVerbose ); extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbose ); extern Ivy_Man_t * Ivy_ManRwsat( Ivy_Man_t * pMan, 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 ); /*=== ivySeq.c =========================================================*/ extern int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose ); /*=== ivyShow.c =========================================================*/ extern void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ); /*=== ivyTable.c ========================================================*/ 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_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 void Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ); 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 int Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj ); 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 Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj ); extern void Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig ); extern void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig ); extern int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth ); #ifdef __cplusplus } #endif #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////