| /**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 ABC__aig__ivy__ivy_h |
| #define ABC__aig__ivy__ivy_h |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// INCLUDES /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| #include <stdio.h> |
| #include "misc/extra/extra.h" |
| #include "misc/vec/vec.h" |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// PARAMETERS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| |
| ABC_NAMESPACE_HEADER_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// 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 |
| abctime time1; |
| abctime 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)) |
| |
| extern void Ivy_ManAddMemory( Ivy_Man_t * p ); |
| |
| 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 *)((ABC_PTRUINT_T)(p) & ~01); } |
| static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); } |
| static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); } |
| static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(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 (Ivy_Type_t)pObj->Type; } |
| static inline Ivy_Init_t Ivy_ObjInit( Ivy_Obj_t * pObj ) { return (Ivy_Init_t)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 ) |
| { |
| 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( Ivy_Obj_t *, p->vPis, pObj, i ) |
| // iterator over the primary outputs |
| #define Ivy_ManForEachPo( p, pObj, i ) \ |
| Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPos, pObj, i ) |
| // iterator over all objects, including those currently not used |
| #define Ivy_ManForEachObj( p, pObj, i ) \ |
| Vec_PtrForEachEntry( Ivy_Obj_t *, 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) = (Ivy_Obj_t *)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 ); |
| |
| |
| |
| ABC_NAMESPACE_HEADER_END |
| |
| |
| |
| #endif |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
